creusot_std/logic/ra/
lattice.rs

1use crate::{logic::ra::RA, prelude::*};
2
3/// The 'lattice' Resource Algebra.
4
5pub trait SemiLattice: PartialOrdLogic + Sized {
6    #[logic]
7    #[ensures(self <= result)]
8    #[ensures(other <= result)]
9    #[ensures(forall<r> self <= r ==> other <= r ==> result <= r)]
10    fn join(self, other: Self) -> Self;
11}
12
13impl<T: SemiLattice> RA for T {
14    #[logic(open, inline)]
15    fn op(self, other: Self) -> Option<Self> {
16        Some(self.join(other))
17    }
18
19    #[logic(open)]
20    #[ensures(result == (exists<factor> self.op(factor) == Some(other)))]
21    fn incl(self, other: Self) -> bool {
22        self <= other
23    }
24
25    #[logic(law)]
26    #[ensures(a.op(b) == b.op(a))]
27    fn commutative(a: Self, b: Self) {}
28
29    #[logic]
30    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
31    fn associative(a: Self, b: Self, c: Self) {}
32
33    #[logic]
34    fn core(self) -> Option<Self> {
35        Some(self)
36    }
37
38    #[logic]
39    #[requires(self.core() != None)]
40    #[ensures({
41        let c = self.core().unwrap_logic();
42        c.op(c) == Some(c)
43    })]
44    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
45    fn core_idemp(self) {}
46
47    #[logic]
48    #[requires(i.op(i) == Some(i))]
49    #[requires(i.op(self) == Some(self))]
50    #[ensures(match self.core() {
51        Some(c) => i.incl(c),
52        None => false,
53    })]
54    fn core_is_maximal_idemp(self, i: Self) {}
55}
creusot_std/logic/ra/lattice.rs

creusot_std/logic/ra/
lattice.rs
