creusot_std/logic/ra/
agree.rs

1use crate::{logic::ra::RA, prelude::*};
2
3/// The 'agreement' Resource Algebra.
4///
5/// This has the property that all resource with the same id have the same value
6/// (they 'agree').
7pub struct Ag<T>(pub T);
8
9impl<T> RA for Ag<T> {
10    #[logic(open)]
11    fn op(self, other: Self) -> Option<Self> {
12        if self.0 == other.0 { Some(self) } else { None }
13    }
14
15    #[logic(open)]
16    #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
17    fn incl(self, other: Self) -> bool {
18        self.0 == other.0
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)]
30    fn core(self) -> Option<Self> {
31        Some(self)
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    #[logic(open)]
52    #[ensures(result == (forall<x, y> self.op(x) != None ==>
53        self.op(x) == self.op(y) ==> x == y))]
54    fn cancelable(self) -> bool {
55        true
56    }
57}
creusot_std/logic/ra/agree.rs

creusot_std/logic/ra/
agree.rs
