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

creusot_std/logic/
int.rs
