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

creusot_std/logic/
int.rs
