creusot_std/logic/
int.rs

1use crate::{
2    ghost::Plain,
3    invariant::{InhabitedInvariant, Subset},
4    logic::ops::{AddLogic, DivLogic, MulLogic, NegLogic, RemLogic, SubLogic},
5    prelude::*,
6};
7use core::ops::{
8    Add, AddAssign, Div, DivAssign, Mul, MulAssign, Neg, Rem, RemAssign, Sub, SubAssign,
9};
10
11/// An unbounded, mathematical integer.
12///
13/// This type cannot be only be constructed in logical or ghost code.
14///
15/// # Integers in pearlite
16///
17/// Note that in pearlite, all integer literals are of type `Int`:
18/// ```
19/// # use creusot_std::prelude::*;
20/// let x = 1i32;
21/// //             ↓ need to use the view operator to convert `i32` to `Int`
22/// proof_assert!(x@ == 1);
23/// ```
24///
25/// You can use the usual operators on integers: `+`, `-`, `*`, `/` and `%`.
26///
27/// Note that those operators are _not_ available in ghost code.
28#[intrinsic("int")]
29#[builtin("int")]
30pub struct Int;
31
32impl Clone for Int {
33    #[check(ghost)]
34    #[ensures(result == *self)]
35    fn clone(&self) -> Self {
36        *self
37    }
38}
39impl Copy for Int {}
40impl Plain for Int {
41    #[trusted]
42    #[ensures(*result == *snap)]
43    #[check(ghost)]
44    #[allow(unused_variables)]
45    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
46        Ghost::conjure()
47    }
48}
49
50// Logical functions
51impl Int {
52    /// Compute `self^p`.
53    ///
54    /// # Example
55    ///
56    /// ```
57    /// # use creusot_std::prelude::*;
58    /// proof_assert!(3.pow(4) == 729);
59    /// ```
60    #[logic]
61    #[builtin("int.Power.power")]
62    #[allow(unused_variables)]
63    pub fn pow(self, p: Int) -> Int {
64        dead
65    }
66
67    /// Compute `2^p`.
68    ///
69    /// # Example
70    ///
71    /// ```
72    /// # use creusot_std::prelude::*;
73    /// proof_assert!(pow2(4) == 16);
74    /// ```
75    #[logic]
76    #[builtin("bv.Pow2int.pow2")]
77    #[allow(unused_variables)]
78    pub fn pow2(self) -> Int {
79        dead
80    }
81
82    /// Compute the maximum of `self` and `x`.
83    ///
84    /// # Example
85    ///
86    /// ```
87    /// # use creusot_std::prelude::*;
88    /// proof_assert!(10.max(2) == 10);
89    /// ```
90    #[logic]
91    #[builtin("int.MinMax.max")]
92    #[allow(unused_variables)]
93    pub fn max(self, x: Int) -> Int {
94        dead
95    }
96
97    /// Compute the minimum of `self` and `x`.
98    ///
99    /// # Example
100    ///
101    /// ```
102    /// # use creusot_std::prelude::*;
103    /// proof_assert!(10.max(2) == 2);
104    /// ```
105    #[logic]
106    #[builtin("int.MinMax.min")]
107    #[allow(unused_variables)]
108    pub fn min(self, x: Int) -> Int {
109        dead
110    }
111
112    /// Compute the euclidean division of `self` by `d`.
113    ///
114    /// # Example
115    ///
116    /// ```
117    /// # use creusot_std::prelude::*;
118    /// proof_assert!(10.div_euclid(3) == 3);
119    /// ```
120    #[logic]
121    #[builtin("int.EuclideanDivision.div")]
122    #[allow(unused_variables)]
123    pub fn div_euclid(self, d: Int) -> Int {
124        dead
125    }
126
127    /// Compute the remainder of the euclidean division of `self` by `d`.
128    ///
129    /// # Example
130    ///
131    /// ```
132    /// # use creusot_std::prelude::*;
133    ///  proof_assert!(10.rem_euclid(3) == 1);
134    /// ```
135    #[logic]
136    #[builtin("int.EuclideanDivision.mod")]
137    #[allow(unused_variables)]
138    pub fn rem_euclid(self, d: Int) -> Int {
139        dead
140    }
141
142    /// Compute the absolute difference of `self` and `x`.
143    ///
144    /// # Example
145    ///
146    /// ```
147    /// # use creusot_std::prelude::*;
148    /// proof_assert!(10.abs_diff(3) == 7);
149    /// proof_assert!(3.abs_diff(10) == 7);
150    /// proof_assert!((-5).abs_diff(5) == 10);
151    /// ```
152    #[logic(open)]
153    pub fn abs_diff(self, other: Int) -> Int {
154        if self < other { other - self } else { self - other }
155    }
156}
157
158impl AddLogic for Int {
159    type Output = Self;
160    #[logic]
161    #[builtin("int.Int.(+)")]
162    #[allow(unused_variables)]
163    fn add_logic(self, other: Self) -> Self {
164        dead
165    }
166}
167
168impl SubLogic for Int {
169    type Output = Self;
170    #[logic]
171    #[builtin("int.Int.(-)")]
172    #[allow(unused_variables)]
173    fn sub_logic(self, other: Self) -> Self {
174        dead
175    }
176}
177
178impl MulLogic for Int {
179    type Output = Self;
180    #[logic]
181    #[builtin("int.Int.(*)")]
182    #[allow(unused_variables)]
183    fn mul_logic(self, other: Self) -> Self {
184        dead
185    }
186}
187
188impl DivLogic for Int {
189    type Output = Self;
190    #[logic]
191    #[builtin("int.ComputerDivision.div")]
192    #[allow(unused_variables)]
193    fn div_logic(self, other: Self) -> Self {
194        dead
195    }
196}
197
198impl RemLogic for Int {
199    type Output = Self;
200    #[logic]
201    #[builtin("int.ComputerDivision.mod")]
202    #[allow(unused_variables)]
203    fn rem_logic(self, other: Self) -> Self {
204        dead
205    }
206}
207
208impl NegLogic for Int {
209    type Output = Self;
210    #[logic]
211    #[builtin("int.Int.(-_)")]
212    fn neg_logic(self) -> Self {
213        dead
214    }
215}
216
217// ========== Ghost operations =============
218
219// Ghost functions
220impl Int {
221    /// Create a new `Int` value
222    ///
223    /// The result is wrapped in a [`Ghost`], so that it can only be access inside a
224    /// [`ghost!`] block.
225    ///
226    /// You should not have to use this method directly: instead, use the `int` suffix
227    /// inside of a `ghost` block:
228    /// ```
229    /// # use creusot_std::prelude::*;
230    /// let x: Ghost<Int> = ghost!(1int);
231    /// ghost! {
232    ///     let y: Int = 2int;
233    /// };
234    /// ```
235    #[trusted]
236    #[check(ghost)]
237    #[ensures(*result == value@)]
238    #[allow(unreachable_code)]
239    #[allow(unused_variables)]
240    pub fn new(value: i128) -> Ghost<Self> {
241        Ghost::conjure()
242    }
243
244    #[trusted]
245    #[check(ghost)]
246    #[ensures(^self == *self + 1)]
247    pub fn incr_ghost(&mut self) {}
248
249    #[trusted]
250    #[check(ghost)]
251    #[ensures(^self == *self - 1)]
252    pub fn decr_ghost(&mut self) {}
253}
254
255impl PartialEq for Int {
256    #[trusted]
257    #[check(ghost)]
258    #[ensures(result == (*self == *other))]
259    #[allow(unused_variables)]
260    fn eq(&self, other: &Self) -> bool {
261        panic!()
262    }
263
264    #[check(ghost)]
265    #[ensures(result == (*self != *other))]
266    fn ne(&self, other: &Self) -> bool {
267        !self.eq(other)
268    }
269}
270
271impl PartialOrd for Int {
272    #[trusted]
273    #[check(ghost)]
274    #[ensures(result == Some((*self).cmp_log(*other)))]
275    #[allow(unused_variables)]
276    fn partial_cmp(&self, other: &Self) -> Option<core::cmp::Ordering> {
277        panic!()
278    }
279
280    #[trusted]
281    #[check(ghost)]
282    #[ensures(result == (*self).lt_log(*other))]
283    #[allow(unused_variables)]
284    fn lt(&self, other: &Self) -> bool {
285        panic!()
286    }
287
288    #[trusted]
289    #[check(ghost)]
290    #[ensures(result == (*self).le_log(*other))]
291    #[allow(unused_variables)]
292    fn le(&self, other: &Self) -> bool {
293        panic!()
294    }
295
296    #[trusted]
297    #[check(ghost)]
298    #[ensures(result == (*self).gt_log(*other))]
299    #[allow(unused_variables)]
300    fn gt(&self, other: &Self) -> bool {
301        panic!()
302    }
303
304    #[trusted]
305    #[check(ghost)]
306    #[ensures(result == (*self).ge_log(*other))]
307    #[allow(unused_variables)]
308    fn ge(&self, other: &Self) -> bool {
309        panic!()
310    }
311}
312
313impl Add for Int {
314    type Output = Int;
315    #[trusted]
316    #[check(ghost)]
317    #[ensures(result == self + other)]
318    #[allow(unused_variables)]
319    fn add(self, other: Int) -> Self {
320        panic!()
321    }
322}
323
324impl Sub for Int {
325    type Output = Int;
326    #[trusted]
327    #[check(ghost)]
328    #[ensures(result == self - other)]
329    #[allow(unused_variables)]
330    fn sub(self, other: Int) -> Self {
331        panic!()
332    }
333}
334
335impl Mul for Int {
336    type Output = Int;
337    #[trusted]
338    #[check(ghost)]
339    #[ensures(result == self * other)]
340    #[allow(unused_variables)]
341    fn mul(self, other: Int) -> Self {
342        panic!()
343    }
344}
345
346impl Div for Int {
347    type Output = Int;
348    #[trusted]
349    #[check(ghost)]
350    #[requires(other != 0)]
351    #[ensures(result == self / other)]
352    #[allow(unused_variables)]
353    fn div(self, other: Int) -> Self {
354        panic!()
355    }
356}
357
358impl Rem for Int {
359    type Output = Int;
360    #[trusted]
361    #[check(ghost)]
362    #[requires(other != 0)]
363    #[ensures(result == self % other)]
364    #[allow(unused_variables)]
365    fn rem(self, other: Int) -> Self {
366        panic!()
367    }
368}
369
370impl Neg for Int {
371    type Output = Int;
372    #[trusted]
373    #[check(ghost)]
374    #[ensures(result == -self)]
375    fn neg(self) -> Self {
376        panic!()
377    }
378}
379
380impl AddAssign for Int {
381    #[check(ghost)]
382    #[ensures(^self == *self + rhs)]
383    fn add_assign(&mut self, rhs: Int) {
384        *self = *self + rhs;
385    }
386}
387
388impl SubAssign for Int {
389    #[check(ghost)]
390    #[ensures(^self == *self - rhs)]
391    fn sub_assign(&mut self, rhs: Int) {
392        *self = *self - rhs;
393    }
394}
395
396impl MulAssign for Int {
397    #[check(ghost)]
398    #[ensures(^self == *self * rhs)]
399    fn mul_assign(&mut self, rhs: Int) {
400        *self = *self * rhs;
401    }
402}
403
404impl DivAssign for Int {
405    #[check(ghost)]
406    #[requires(rhs != 0)]
407    #[ensures(^self == *self / rhs)]
408    fn div_assign(&mut self, rhs: Int) {
409        *self = *self / rhs;
410    }
411}
412
413impl RemAssign for Int {
414    #[check(ghost)]
415    #[requires(rhs != 0)]
416    #[ensures(^self == *self % rhs)]
417    fn rem_assign(&mut self, rhs: Int) {
418        *self = *self % rhs;
419    }
420}
421
422struct NatInner(Int);
423
424impl Invariant for NatInner {
425    #[logic]
426    fn invariant(self) -> bool {
427        self.0 >= 0
428    }
429}
430
431impl InhabitedInvariant for NatInner {
432    #[logic]
433    #[ensures(result.invariant())]
434    fn inhabits() -> Self {
435        Self(0)
436    }
437}
438
439/// Natural numbers, i.e., integers that are greater or equal to 0.
440pub struct Nat(Subset<NatInner>);
441
442impl Nat {
443    #[logic]
444    #[ensures(result >= 0)]
445    pub fn to_int(self) -> Int {
446        pearlite! { self.0.inner().0 }
447    }
448
449    #[logic]
450    #[requires(n >= 0)]
451    #[ensures(result.to_int() == n)]
452    pub fn new(n: Int) -> Nat {
453        Nat(Subset::new_logic(NatInner(n)))
454    }
455
456    #[logic(open)]
457    #[ensures(result == (self == other))]
458    pub fn ext_eq(self, other: Self) -> bool {
459        let _ = Subset::<NatInner>::inner_inj;
460        self.to_int() == other.to_int()
461    }
462}
463
464impl AddLogic for Nat {
465    type Output = Self;
466    #[logic]
467    #[ensures(result.to_int() == self.to_int() + other.to_int())]
468    fn add_logic(self, other: Self) -> Self {
469        Self::new(self.to_int() + other.to_int())
470    }
471}
472
473impl MulLogic for Nat {
474    type Output = Self;
475    #[logic]
476    #[ensures(result.to_int() == self.to_int() * other.to_int())]
477    fn mul_logic(self, other: Self) -> Self {
478        Self::new(self.to_int() * other.to_int())
479    }
480}
creusot_std/logic/int.rs

creusot_std/logic/
int.rs
