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(result == (exists<factor> self.op(factor) == Some(other)))]
21    fn incl(self, other: Self) -> bool {
22        false
23    }
24
25    #[logic(law)]
26    #[ensures(a.op(b) == b.op(a))]
27    fn commutative(a: Self, b: Self) {}
28
29    #[logic]
30    #[ensures(a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc)))]
31    fn associative(a: Self, b: Self, c: Self) {}
32
33    #[logic(open)]
34    fn core(self) -> Option<Self> {
35        None
36    }
37
38    #[logic]
39    #[requires(self.core() != None)]
40    #[ensures({
41        let c = self.core().unwrap_logic();
42        c.op(c) == Some(c)
43    })]
44    #[ensures(self.core().unwrap_logic().op(self) == Some(self))]
45    fn core_idemp(self) {}
46
47    #[logic]
48    #[requires(i.op(i) == Some(i))]
49    #[requires(i.op(self) == Some(self))]
50    #[ensures(match self.core() {
51        Some(c) => i.incl(c),
52        None => false,
53    })]
54    fn core_is_maximal_idemp(self, i: Self) {}
55
56    #[logic(open)]
57    #[ensures(result == (forall<x, y> self.op(x) != None ==>
58        self.op(x) == self.op(y) ==> x == y))]
59    fn cancelable(self) -> bool {
60        true
61    }
62}
63
64/// Apply an [update](Update) to the content of an [exclusive](Excl) resource.
65///
66/// This changes the content of the resource. Because it is exclusive, no
67/// premise is needed.
68///
69/// # Example
70///
71/// ```
72/// use creusot_std::{prelude::*, logic::ra::excl::{Excl, ExclUpdate}, ghost::resource::Resource};
73/// let mut res = Resource::alloc(snapshot!(Excl(1)));
74/// ghost! { res.update(ExclUpdate(snapshot!(2))) };
75/// proof_assert!(res@ == Excl(2));
76/// ```
77pub struct ExclUpdate<T>(pub Snapshot<T>);
78
79impl<T> Update<Excl<T>> for ExclUpdate<T> {
80    type Choice = ();
81
82    #[logic(open, inline)]
83    fn premise(self, _: Excl<T>) -> bool {
84        true
85    }
86
87    #[logic(open, inline)]
88    #[requires(self.premise(from))]
89    fn update(self, from: Excl<T>, _: ()) -> Excl<T> {
90        Excl(*self.0)
91    }
92
93    #[logic]
94    #[requires(self.premise(from))]
95    #[requires(from.op(frame) != None)]
96    #[ensures(self.update(from, result).op(frame) != None)]
97    fn frame_preserving(self, from: Excl<T>, frame: Excl<T>) {}
98}
creusot_std/logic/ra/excl.rs

creusot_std/logic/ra/
excl.rs
