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(match result {
17        Some(c) => factor.op(c) == Some(self),
18        None => forall<c: Self> factor.op(c) != Some(self),
19    })]
20    fn factor(self, factor: Self) -> Option<Self> {
21        self.op(factor)
22    }
23
24    #[logic(open(self), law)]
25    #[ensures(a.op(b) == b.op(a))]
26    fn commutative(a: Self, b: Self) {}
27
28    #[logic(open(self), law)]
29    #[ensures(a.op(b).and_then_logic(|ab : Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
30    fn associative(a: Self, b: Self, c: Self) {}
31
32    #[logic(open)]
33    fn core(self) -> Option<Self> {
34        Some(self)
35    }
36
37    #[logic]
38    #[ensures({
39        let c = self.core().unwrap_logic();
40        c.op(c) == Some(c)
41    })]
42    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
43    fn core_idemp(self) {}
44
45    #[logic]
46    #[requires(i.op(i) == Some(i))]
47    #[requires(i.op(self) == Some(self))]
48    #[ensures(match self.core() {
49        Some(c) => i.incl(c),
50        None => false,
51    })]
52    fn core_is_maximal_idemp(self, i: Self) {}
53}
creusot_std/logic/ra/agree.rs

creusot_std/logic/ra/
agree.rs
