creusot_std/logic/ra/
int.rs

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

creusot_std/logic/ra/
int.rs
