creusot_contracts/logic/ra/
excl.rs

1use crate::{
2    logic::ra::{RA, update::Update},
3    prelude::*,
4};
5
6/// The 'exclusive' Resource Algebra.
7///
8/// Combining those resource with [`RA::op`] **never** yields valid elements.
9/// As such, only one version of this resource (when using
10/// [`Resource`][crate::ghost::resource::Resource]) will be able to exist at a given moment.
11pub struct Excl<T>(pub T);
12
13impl<T> RA for Excl<T> {
14    #[logic(open)]
15    fn op(self, _other: Self) -> Option<Self> {
16        None
17    }
18
19    #[logic(open)]
20    #[ensures(match result {
21        Some(c) => factor.op(c) == Some(self),
22        None => forall<c: Self> factor.op(c) != Some(self),
23    })]
24    fn factor(self, factor: Self) -> Option<Self> {
25        None
26    }
27
28    #[logic(open(self), law)]
29    #[ensures(a.op(b) == b.op(a))]
30    fn commutative(a: Self, b: Self) {}
31
32    #[logic(open(self), law)]
33    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
34    fn associative(a: Self, b: Self, c: Self) {}
35
36    #[logic(open)]
37    #[ensures(match result {
38        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
39        None => true
40    })]
41    fn core(self) -> Option<Self> {
42        None
43    }
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}
54
55pub struct ExclUpdate<T>(pub Snapshot<T>);
56
57impl<T> Update<Excl<T>> for ExclUpdate<T> {
58    type Choice = ();
59
60    #[logic(open)]
61    fn premise(self, _: Excl<T>) -> bool {
62        true
63    }
64
65    #[logic(open)]
66    #[requires(self.premise(from))]
67    fn update(self, from: Excl<T>, _: ()) -> Excl<T> {
68        Excl(*self.0)
69    }
70
71    #[logic]
72    #[requires(self.premise(from))]
73    #[requires(from.op(frame) != None)]
74    #[ensures(self.update(from, result).op(frame) != None)]
75    fn frame_preserving(self, from: Excl<T>, frame: Excl<T>) {}
76}
creusot_contracts/logic/ra/excl.rs

creusot_contracts/logic/ra/
excl.rs
