creusot_std/logic/ra/
nat.rs

1use crate::{
2    logic::{
3        Nat,
4        ra::{RA, UnitRA},
5    },
6    prelude::*,
7};
8
9impl RA for Nat {
10    #[logic(open, inline)]
11    fn op(self, other: Self) -> Option<Nat> {
12        Some(self + other)
13    }
14
15    #[logic(open)]
16    #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
17    fn incl(self, other: Self) -> bool {
18        let _ = Self::ext_eq;
19        let r = self.to_int() <= other.to_int();
20        proof_assert!(r ==> self.op(Self::new(other.to_int() - self.to_int())) == Some(other));
21        r
22    }
23
24    #[logic(open, inline)]
25    #[ensures(#[trigger(self == other)]result == (self == other))]
26    fn eq(self, other: Self) -> bool {
27        self.ext_eq(other)
28    }
29
30    #[logic(law)]
31    #[ensures(a.op(b) == b.op(a))]
32    fn commutative(a: Self, b: Self) {
33        let _ = Nat::ext_eq;
34    }
35
36    #[logic]
37    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
38    fn associative(a: Self, b: Self, c: Self) {
39        let _ = Nat::ext_eq;
40    }
41
42    #[logic(open, inline)]
43    fn core(self) -> Option<Self> {
44        Some(Nat::new(0))
45    }
46
47    #[logic]
48    #[ensures({
49        let c = self.core().unwrap_logic();
50        c.op(c) == Some(c)
51    })]
52    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
53    fn core_idemp(self) {
54        let _ = Nat::ext_eq;
55    }
56
57    #[logic]
58    #[requires(i.op(i) == Some(i))]
59    #[requires(i.op(self) == Some(self))]
60    #[ensures(match self.core() {
61        Some(c) => i.incl(c),
62        None => false,
63    })]
64    fn core_is_maximal_idemp(self, i: Self) {}
65
66    #[logic(open)]
67    #[ensures(result == (forall<x, y> self.op(x) != None ==>
68        self.op(x) == self.op(y) ==> x == y))]
69    fn cancelable(self) -> bool {
70        let _ = Nat::ext_eq;
71        true
72    }
73}
74
75impl UnitRA for Nat {
76    #[logic(open, inline)]
77    #[ensures(forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x))]
78    fn unit() -> Self {
79        let _ = Nat::ext_eq;
80        Nat::new(0)
81    }
82
83    #[logic(open, inline)]
84    #[ensures(self.core() == Some(result))]
85    fn core_total(self) -> Self {
86        Nat::new(0)
87    }
88
89    #[logic]
90    #[ensures(self.core_total().op(self.core_total()) == Some(self.core_total()))]
91    #[ensures(self.core_total().op(self) == Some(self))]
92    fn core_total_idemp(self) {
93        let _ = Nat::ext_eq;
94    }
95}
creusot_std/logic/ra/nat.rs

creusot_std/logic/ra/
nat.rs
