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

creusot_std/logic/
int.rs
