creusot_contracts/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    #[ensures(match result {
34        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
35        None => true
36    })]
37    fn core(self) -> Option<Self> {
38        Some(self)
39    }
40
41    #[logic]
42    #[requires(i.op(i) == Some(i))]
43    #[requires(i.op(self) == Some(self))]
44    #[ensures(match self.core() {
45        Some(c) => i.incl(c),
46        None => false,
47    })]
48    fn core_is_maximal_idemp(self, i: Self) {}
49}
creusot_contracts/logic/ra/agree.rs

creusot_contracts/logic/ra/
agree.rs
