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

creusot_std/logic/ra/
int.rs
