creusot_contracts/logic/
int.rs

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

creusot_contracts/logic/
int.rs
