vstd/resource/pcm.rs
1use super::super::prelude::*;
2use super::Loc;
3use super::algebra::ResourceAlgebra;
4use super::relations::*;
5
6#[cfg(verus_keep_ghost)]
7use super::super::modes::tracked_swap;
8
9verus! {
10
11broadcast use super::super::set::group_set_axioms;
12
13/// Interface for PCM / Resource Algebra ghost state.
14///
15/// RA-based ghost state is a well-established theory that is especially
16/// useful for verifying concurrent code. An introduction to the concept
17/// can be found in
18/// [Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning](https://iris-project.org/pdfs/2015-popl-iris1-final.pdf)
19/// or
20/// [Iris from the ground up](https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf).
21///
22/// To embed the concept into Verus, we:
23/// * Use a trait, [`PCM`], to embed the well-formedness laws of a resource algebra
24/// * use a "tracked ghost" object, `Resource<P>` (this page) to represent ownership of a resource.
25///
26/// Most operations are fairly standard, just "translated" from the usual CSL presentation into Verus.
27///
28/// * [`alloc`](Self::alloc) to allocate a resource.
29/// * [`join`](Self::join) to combine two resources via `P::op`, and [`split`](Self::split), its inverse.
30/// * [`validate`](Self::validate) to assert the validity of any held resource.
31/// * [`update`](Self::update) or [`update_nondeterministic`](Self::update_nondeterministic) to perform a frame-preserving update.
32///
33/// The interface also includes a nontrivial extension for working with _shared references_ to resources.
34/// Shared 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)).
35///
36/// ### Examples
37///
38/// See:
39/// * Any of the examples in [this directory](https://github.com/verus-lang/verus/tree/main/examples/pcm)
40/// * The source code for the [fractional resource library](super::frac::FracGhost)
41///
42/// ### See also
43///
44/// The ["storage protocol"](super::storage_protocol::StorageResource) formalism
45/// is an even more significant
46/// extension with additional capabilities for interacting with shared resources.
47///
48/// [VerusSync](https://verus-lang.github.io/verus/state_machines/intro.html) provides a higher-level
49/// "swiss army knife" for building useful ghost resources.
50// Resource must be external_body, otherwise it could be constructed directly
51#[verifier::external_body]
52#[verifier::accept_recursive_types(P)]
53pub tracked struct Resource<P: PCM> {
54 p: core::marker::PhantomData<P>,
55}
56
57/// A Partial Commutative Monoid is a special type of [`ResourceAlgebra`], where all elements have
58/// the same core (which belongs in the carrier), the unit. For this reason, they are also called
59/// unitary resource algebras[^note].
60///
61/// [^note]: This is slightly misleading. PCMs are partial in the sense that the operation is not
62/// defined for certain inputs. Because Verus does not support partial functions, we model that
63/// partiality with the validity predicate, which does make it a unitary resource algebra.
64pub trait PCM: ResourceAlgebra {
65 /// The unit of the monoid, i.e., the carrier value that composed with any other carrier value
66 /// yields the identity function
67 spec fn unit() -> Self;
68
69 /// The core of an element `a` is, by definition, some other element `x`
70 /// such that `a · x = a`
71 proof fn op_unit(self)
72 ensures
73 Self::op(self, Self::unit()) == self,
74 ;
75
76 /// The unit is always a valid element
77 proof fn unit_valid()
78 ensures
79 Self::unit().valid(),
80 ;
81}
82
83impl<P: PCM> Resource<P> {
84 /// The underlying value of the resource
85 pub uninterp spec fn value(self) -> P;
86
87 /// The location of the resource
88 pub uninterp spec fn loc(self) -> Loc;
89
90 // AXIOMS
91 /// Allocate a new resource at a fresh location
92 // GHOST-ALLOC rule
93 pub axiom fn alloc(value: P) -> (tracked out: Self)
94 requires
95 value.valid(),
96 ensures
97 out.value() == value,
98 ;
99
100 /// We can join together two resources at the same location, where we obtain the combination of
101 /// the two
102 // reverse implication in the GHOST-OP rule
103 pub axiom fn join(tracked self, tracked other: Self) -> (tracked out: Self)
104 requires
105 self.loc() == other.loc(),
106 ensures
107 out.loc() == self.loc(),
108 out.value() == P::op(self.value(), other.value()),
109 ;
110
111 /// If a resource holds the result of a composition, we can split it into the components
112 // implication in the GHOST-OP rule
113 pub axiom fn split(tracked self, left: P, right: P) -> (tracked out: (Self, Self))
114 requires
115 self.value() == P::op(left, right),
116 ensures
117 out.0.loc() == self.loc(),
118 out.1.loc() == self.loc(),
119 out.0.value() == left,
120 out.1.value() == right,
121 ;
122
123 /// Create a unit at a particular location
124 pub axiom fn create_unit(loc: Loc) -> (tracked out: Self)
125 ensures
126 out.value() == P::unit(),
127 out.loc() == loc,
128 ;
129
130 /// Whenever we have a resource, that resource is valid. This intuitively (and inductively)
131 /// holds because:
132 /// 1. We only create valid resources (either via [`alloc`] or
133 /// [`create_unit`](Self::create_unit)).
134 /// 2. We can only update the value of a resource via a [`frame_preserving_update`] (see
135 /// [`update`](Self::update) for more details. Because of the requirement of that
136 /// updates are frame preserving this means that `join`s remain valid.
137 // GHOST-VALID rule
138 pub axiom fn validate(tracked &self)
139 ensures
140 self.value().valid(),
141 ;
142
143 /// This is a more general version of [`update`](Self::update).
144 // GHOST-UPDATE rule
145 pub proof fn update_nondeterministic(tracked self, new_values: Set<P>) -> (tracked out: Self)
146 requires
147 frame_preserving_update_nondeterministic(self.value(), new_values),
148 ensures
149 out.loc() == self.loc(),
150 new_values.contains(out.value()),
151 {
152 let tracked u = Self::create_unit(self.loc());
153 PCM::op_unit(self.value());
154 assert(set_op(new_values, u.value()) =~= new_values) by {
155 assert forall|x|
156 set_op(new_values, u.value()).contains(x) <==> #[trigger] new_values.contains(
157 x,
158 ) by {
159 PCM::op_unit(x);
160 if set_op(new_values, u.value()).contains(x) {
161 let q = choose|q| #[trigger] new_values.contains(q) && x == P::op(q, u.value());
162 PCM::op_unit(q);
163 }
164 }
165 };
166 self.update_nondeterministic_with_shared(&u, new_values)
167 }
168
169 // VERIFIED
170 /// Update a resource to a new value. This can only be done if the update is frame preserving
171 /// (i.e., any value that could be composed with the original value can still be composed with
172 /// the new value).
173 ///
174 /// See [`frame_preserving_update`] for more information.
175 // variant of the GHOST-UPDATE rule
176 pub proof fn update(tracked self, new_value: P) -> (tracked out: Self)
177 requires
178 frame_preserving_update(self.value(), new_value),
179 ensures
180 out.loc() == self.loc(),
181 out.value() == new_value,
182 {
183 let new_values = set![new_value];
184 assert(new_values.contains(new_value));
185 self.update_nondeterministic(new_values)
186 }
187
188 /// Extracts the resource from `r`, leaving `r` unspecified and returning
189 /// a new resource holding the previous value of `r`.
190 pub proof fn extract(tracked &mut self) -> (tracked other: Self)
191 ensures
192 other.loc() == old(self).loc(),
193 other.value() == old(self).value(),
194 {
195 self.validate();
196 let tracked mut other = Self::alloc(self.value());
197 tracked_swap(self, &mut other);
198 other
199 }
200
201 // Operations with shared references
202 // AXIOMS on shared references
203 /// This is useful when you have two (or more) shared resources and want to learn
204 /// that they agree, as you can combine this validate, e.g., `x.join_shared(y).validate()`.
205 pub axiom fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out:
206 &'a Self)
207 requires
208 self.loc() == other.loc(),
209 ensures
210 out.loc() == self.loc(),
211 incl(self.value(), out.value()),
212 incl(other.value(), out.value()),
213 ;
214
215 /// Extract a shared reference to a preceding element in the extension order from a shared reference.
216 pub axiom fn weaken<'a>(tracked &'a self, target: P) -> (tracked out: &'a Self)
217 requires
218 incl(target, self.value()),
219 ensures
220 out.loc() == self.loc(),
221 out.value() == target,
222 ;
223
224 /// Validate two items at once. If we have two resources at the same location then its
225 /// composition is valid.
226 pub axiom fn validate_2(tracked &mut self, tracked other: &Self)
227 requires
228 old(self).loc() == other.loc(),
229 ensures
230 *final(self) == *old(self),
231 P::op(final(self).value(), other.value()).valid(),
232 ;
233
234 /// We can do a similar update to [`update_with_shared`](Self::update_with_shared) for non-deterministic updates
235 pub axiom fn update_nondeterministic_with_shared(
236 tracked self,
237 tracked other: &Self,
238 new_values: Set<P>,
239 ) -> (tracked out: Self)
240 requires
241 self.loc() == other.loc(),
242 frame_preserving_update_nondeterministic(
243 P::op(self.value(), other.value()),
244 set_op(new_values, other.value()),
245 ),
246 ensures
247 out.loc() == self.loc(),
248 new_values.contains(out.value()),
249 ;
250
251 // VERIFIED facts about shared references
252 /// We can do a similar update to [`update_with_shared`](Self::update_with_shared) for non-deterministic updates
253 pub proof fn join_shared_to_target<'a>(
254 tracked &'a self,
255 tracked other: &'a Self,
256 target: P,
257 ) -> (tracked out: &'a Self)
258 requires
259 self.loc() == other.loc(),
260 conjunct_shared(self.value(), other.value(), target),
261 ensures
262 out.loc() == self.loc(),
263 out.value() == target,
264 {
265 let tracked j = self.join_shared(other);
266 j.validate();
267 j.weaken(target)
268 }
269
270 /// If `x · y --> x · z` is a frame-perserving update, and we have a shared reference to `x`,
271 /// we can update the `y` resource to `z`.
272 pub proof fn update_with_shared(
273 tracked self,
274 tracked other: &Self,
275 new_value: P,
276 ) -> (tracked out: Self)
277 requires
278 self.loc() == other.loc(),
279 frame_preserving_update(
280 P::op(self.value(), other.value()),
281 P::op(new_value, other.value()),
282 ),
283 ensures
284 out.loc() == self.loc(),
285 out.value() == new_value,
286 {
287 let new_values = set![new_value];
288 let so = set_op(new_values, other.value());
289 assert(so.contains(P::op(new_value, other.value())));
290 self.update_nondeterministic_with_shared(other, new_values)
291 }
292
293 /// If `x --> x · y` is a frame-perserving update, and we have a shared reference to `x`,
294 /// we can create a resource to y
295 pub proof fn duplicate_previous(tracked &self, value: P) -> (tracked out: Self)
296 requires
297 frame_preserving_update(self.value(), P::op(value, self.value())),
298 ensures
299 out.loc() == self.loc(),
300 out.value() == value,
301 {
302 let tracked mut unit = Self::create_unit(self.loc());
303 self.value().op_unit();
304 P::commutative(self.value(), unit.value());
305 unit.update_with_shared(self, value)
306 }
307}
308
309} // verus!