creusot_std/logic/
int.rs

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

creusot_std/logic/
int.rs
