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(law)]
29    #[ensures(a.op(b) == b.op(a))]
30    fn commutative(a: Self, b: Self) {}
31
32    #[logic]
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
60/// Apply an [update](Update) to the content of an [exclusive](Excl) resource.
61///
62/// This changes the content of the resource. Because it is exclusive, no
63/// premise is needed.
64///
65/// # Example
66///
67/// ```
68/// use creusot_std::{prelude::*, logic::ra::excl::{Excl, ExclUpdate}, ghost::resource::Resource};
69/// let mut res = Resource::alloc(snapshot!(Excl(1)));
70/// ghost! { res.update(ExclUpdate(snapshot!(2))) };
71/// proof_assert!(res@ == Excl(2));
72/// ```
73pub struct ExclUpdate<T>(pub Snapshot<T>);
74
75impl<T> Update<Excl<T>> for ExclUpdate<T> {
76    type Choice = ();
77
78    #[logic(open, inline)]
79    fn premise(self, _: Excl<T>) -> bool {
80        true
81    }
82
83    #[logic(open, inline)]
84    #[requires(self.premise(from))]
85    fn update(self, from: Excl<T>, _: ()) -> Excl<T> {
86        Excl(*self.0)
87    }
88
89    #[logic]
90    #[requires(self.premise(from))]
91    #[requires(from.op(frame) != None)]
92    #[ensures(self.update(from, result).op(frame) != None)]
93    fn frame_preserving(self, from: Excl<T>, frame: Excl<T>) {}
94}
creusot_std/logic/ra/excl.rs

creusot_std/logic/ra/
excl.rs
