creusot_std/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    fn core(self) -> Option<Self> {
38        None
39    }
40
41    #[logic]
42    #[requires(self.core() != None)]
43    #[ensures({
44        let c = self.core().unwrap_logic();
45        c.op(c) == Some(c)
46    })]
47    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
48    fn core_idemp(self) {}
49
50    #[logic]
51    #[requires(i.op(i) == Some(i))]
52    #[requires(i.op(self) == Some(self))]
53    #[ensures(match self.core() {
54        Some(c) => i.incl(c),
55        None => false,
56    })]
57    fn core_is_maximal_idemp(self, i: Self) {}
58}
59
60pub struct ExclUpdate<T>(pub Snapshot<T>);
61
62impl<T> Update<Excl<T>> for ExclUpdate<T> {
63    type Choice = ();
64
65    #[logic(open)]
66    fn premise(self, _: Excl<T>) -> bool {
67        true
68    }
69
70    #[logic(open)]
71    #[requires(self.premise(from))]
72    fn update(self, from: Excl<T>, _: ()) -> Excl<T> {
73        Excl(*self.0)
74    }
75
76    #[logic]
77    #[requires(self.premise(from))]
78    #[requires(from.op(frame) != None)]
79    #[ensures(self.update(from, result).op(frame) != None)]
80    fn frame_preserving(self, from: Excl<T>, frame: Excl<T>) {}
81}
creusot_std/logic/ra/excl.rs

creusot_std/logic/ra/
excl.rs
