creusot_std/logic/ra/
lattice.rs

1use crate::{
2    logic::{ord, ra::RA},
3    prelude::*,
4};
5
6/// The 'lattice' Resource Algebra.
7pub struct SemiLattice<T>(pub T);
8
9impl<T: ord::SemiLattice> RA for SemiLattice<T> {
10    #[logic(open, inline)]
11    fn op(self, other: Self) -> Option<Self> {
12        Some(Self(self.0.join(other.0)))
13    }
14
15    #[logic(open, inline)]
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, inline)]
30    fn core(self) -> Option<Self> {
31        Some(self)
32    }
33
34    #[logic]
35    #[requires(self.core() != None)]
36    #[ensures({
37        let c = self.core().unwrap_logic();
38        c.op(c) == Some(c)
39    })]
40    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
41    fn core_idemp(self) {}
42
43    #[logic]
44    #[requires(i.op(i) == Some(i))]
45    #[requires(i.op(self) == Some(self))]
46    #[ensures(match self.core() {
47        Some(c) => i.incl(c),
48        None => false,
49    })]
50    fn core_is_maximal_idemp(self, i: Self) {}
51}
creusot_std/logic/ra/lattice.rs

creusot_std/logic/ra/
lattice.rs
