creusot_contracts/logic/
int.rs

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

creusot_contracts/logic/
int.rs
