vstd/
pcm.rs

Help
1use super::prelude::*;
2use super::set::*;
3
4verus! {
5
6broadcast use super::set::group_set_axioms;
7/** Interface for PCM / Resource Algebra ghost state.
8
9RA-based ghost state is a well-established theory that is especially
10useful for verifying concurrent code. An introduction to the concept
11can be found in
12[Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning](https://iris-project.org/pdfs/2015-popl-iris1-final.pdf)
13or
14[Iris from the ground up](https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf).
15
16To embed the concept into Verus, we:
17 * Use a trait, [`PCM`], to embed the well-formedness laws of a resource algebra
18 * use a "tracked ghost" object, `Resource<P>` (this page) to represent ownership of a resource.
19
20Most operations are fairly standard, just "translated" from the usual CSL presentation into Verus.
21
22 * [`alloc`](Self::alloc) to allocate a resource.
23 * [`join`](Self::join) to combine two resources via `P::op`, and [`split`](Self::split), its inverse.
24 * [`validate`](Self::validate) to assert the validity of any held resource.
25 * [`update`](Self::update) or [`update_nondeterministic`](Self::update_nondeterministic) to perform a frame-preserving update.
26
27The interface also includes a nontrivial extension for working with _shared references_ to resources.
28Shared resources do not compose in a "separating" way via `P::op`, but rather, in a "potentially overlapping" way ([`join_shared`](Self::join_shared)). Shared resources can also be used to "help" perform frame-preserving updates, as long as they themselves do not change ([`update_with_shared`](Self::update_with_shared)).
29
30### Examples
31
32See:
33 * Any of the examples in [this directory](https://github.com/verus-lang/verus/tree/main/examples/pcm)
34 * The source code for the [fractional resource library](super::tokens::frac::FracGhost)
35
36### See also
37
38The ["storage protocol"](super::storage_protocol::StorageResource) formalism
39is an even more significant
40extension with additional capabilities for interacting with shared resources.
41
42[VerusSync](https://verus-lang.github.io/verus/state_machines/intro.html) provides a higher-level
43"swiss army knife" for building useful ghost resources.
44*/
45
46#[verifier::external_body]
47#[verifier::accept_recursive_types(P)]
48pub tracked struct Resource<P> {
49    p: core::marker::PhantomData<P>,
50}
51
52pub type Loc = int;
53
54/// See [`Resource`] for more information.
55pub trait PCM: Sized {
56    spec fn valid(self) -> bool;
57
58    spec fn op(self, other: Self) -> Self;
59
60    spec fn unit() -> Self;
61
62    proof fn closed_under_incl(a: Self, b: Self)
63        requires
64            Self::op(a, b).valid(),
65        ensures
66            a.valid(),
67    ;
68
69    proof fn commutative(a: Self, b: Self)
70        ensures
71            Self::op(a, b) == Self::op(b, a),
72    ;
73
74    proof fn associative(a: Self, b: Self, c: Self)
75        ensures
76            Self::op(a, Self::op(b, c)) == Self::op(Self::op(a, b), c),
77    ;
78
79    proof fn op_unit(a: Self)
80        ensures
81            Self::op(a, Self::unit()) == a,
82    ;
83
84    proof fn unit_valid()
85        ensures
86            Self::valid(Self::unit()),
87    ;
88}
89
90pub open spec fn incl<P: PCM>(a: P, b: P) -> bool {
91    exists|c| P::op(a, c) == b
92}
93
94pub open spec fn conjunct_shared<P: PCM>(a: P, b: P, c: P) -> bool {
95    forall|p: P| p.valid() && incl(a, p) && incl(b, p) ==> #[trigger] incl(c, p)
96}
97
98pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool {
99    forall|c| #![trigger P::op(a, c), P::op(b, c)] P::op(a, c).valid() ==> P::op(b, c).valid()
100}
101
102pub open spec fn frame_preserving_update_nondeterministic<P: PCM>(a: P, bs: Set<P>) -> bool {
103    forall|c|
104        #![trigger P::op(a, c)]
105        P::op(a, c).valid() ==> exists|b| #[trigger] bs.contains(b) && P::op(b, c).valid()
106}
107
108pub open spec fn set_op<P: PCM>(s: Set<P>, t: P) -> Set<P> {
109    Set::new(|v| exists|q| s.contains(q) && v == P::op(q, t))
110}
111
112impl<P: PCM> Resource<P> {
113    pub uninterp spec fn value(self) -> P;
114
115    pub uninterp spec fn loc(self) -> Loc;
116
117    pub axiom fn alloc(value: P) -> (tracked out: Self)
118        requires
119            value.valid(),
120        ensures
121            out.value() == value,
122    ;
123
124    pub axiom fn join(tracked self, tracked other: Self) -> (tracked out: Self)
125        requires
126            self.loc() == other.loc(),
127        ensures
128            out.loc() == self.loc(),
129            out.value() == P::op(self.value(), other.value()),
130    ;
131
132    pub axiom fn split(tracked self, left: P, right: P) -> (tracked out: (Self, Self))
133        requires
134            self.value() == P::op(left, right),
135        ensures
136            out.0.loc() == self.loc(),
137            out.1.loc() == self.loc(),
138            out.0.value() == left,
139            out.1.value() == right,
140    ;
141
142    pub axiom fn create_unit(loc: Loc) -> (tracked out: Self)
143        ensures
144            out.value() == P::unit(),
145            out.loc() == loc,
146    ;
147
148    pub axiom fn validate(tracked &self)
149        ensures
150            self.value().valid(),
151    ;
152
153    pub proof fn update(tracked self, new_value: P) -> (tracked out: Self)
154        requires
155            frame_preserving_update(self.value(), new_value),
156        ensures
157            out.loc() == self.loc(),
158            out.value() == new_value,
159    {
160        let new_values = set![new_value];
161        assert(new_values.contains(new_value));
162        self.update_nondeterministic(new_values)
163    }
164
165    pub axiom fn update_nondeterministic(tracked self, new_values: Set<P>) -> (tracked out: Self)
166        requires
167            frame_preserving_update_nondeterministic(self.value(), new_values),
168        ensures
169            out.loc() == self.loc(),
170            new_values.contains(out.value()),
171    ;
172
173    // Operations with shared references
174    /// This is useful when you have two (or more) shared resources and want to learn
175    /// that they agree, as you can combine this validate, e.g., `x.join_shared(y).validate()`.
176    pub axiom fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out:
177        &'a Self)
178        requires
179            self.loc() == other.loc(),
180        ensures
181            out.loc() == self.loc(),
182            incl(self.value(), out.value()),
183            incl(other.value(), out.value()),
184    ;
185
186    pub proof fn join_shared_to_target<'a>(
187        tracked &'a self,
188        tracked other: &'a Self,
189        target: P,
190    ) -> (tracked out: &'a Self)
191        requires
192            self.loc() == other.loc(),
193            conjunct_shared(self.value(), other.value(), target),
194        ensures
195            out.loc() == self.loc(),
196            out.value() == target,
197    {
198        let tracked j = self.join_shared(other);
199        j.validate();
200        j.weaken(target)
201    }
202
203    pub axiom fn weaken<'a>(tracked &'a self, target: P) -> (tracked out: &'a Self)
204        requires
205            incl(target, self.value()),
206        ensures
207            out.loc() == self.loc(),
208            out.value() == target,
209    ;
210
211    pub axiom fn validate_2(tracked &mut self, tracked other: &Self)
212        requires
213            old(self).loc() == other.loc(),
214        ensures
215            *self == *old(self),
216            P::op(self.value(), other.value()).valid(),
217    ;
218
219    /// If `x · y --> x · z` is a frame-perserving update, and we have a shared reference to `x`,
220    /// we can update the `y` resource to `z`.
221    pub proof fn update_with_shared(
222        tracked self,
223        tracked other: &Self,
224        new_value: P,
225    ) -> (tracked out: Self)
226        requires
227            self.loc() == other.loc(),
228            frame_preserving_update(
229                P::op(self.value(), other.value()),
230                P::op(new_value, other.value()),
231            ),
232        ensures
233            out.loc() == self.loc(),
234            out.value() == new_value,
235    {
236        let new_values = set![new_value];
237        let so = set_op(new_values, other.value());
238        assert(so.contains(P::op(new_value, other.value())));
239        self.update_nondeterministic_with_shared(other, new_values)
240    }
241
242    pub axiom fn update_nondeterministic_with_shared(
243        tracked self,
244        tracked other: &Self,
245        new_values: Set<P>,
246    ) -> (tracked out: Self)
247        requires
248            self.loc() == other.loc(),
249            frame_preserving_update_nondeterministic(
250                P::op(self.value(), other.value()),
251                set_op(new_values, other.value()),
252            ),
253        ensures
254            out.loc() == self.loc(),
255            new_values.contains(out.value()),
256    ;
257}
258
259} // verus!
vstd/pcm.rs

vstd/
pcm.rs
