vstd/resource/
algebra.rs

1use super::super::modes::*;
2use super::super::prelude::*;
3use super::super::set::*;
4use super::Loc;
5use super::option::*;
6use super::pcm;
7use super::pcm::PCM;
8use super::relations::*;
9
10verus! {
11
12broadcast use super::super::set::group_set_axioms;
13
14/// Interface for Resource Algebra ghost state.
15#[verifier::accept_recursive_types(RA)]
16pub tracked struct Resource<RA: ResourceAlgebra> {
17    pcm: pcm::Resource<Option<RA>>,
18}
19
20/// A Resource Algebra operating on a type T
21///
22/// This construction is based off the [Iris from the Ground Up](https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf)
23/// report.
24///
25/// A striking difference is that we do not need a core for elements (the core is interesting in
26/// Iris because of the persistent modality, which Verus does not have).
27///
28/// See [`Resource`] for more information.
29// TODO(bsdinis): it should probably not be required that ghost things be sized, but that sounds
30// like a relatively complicated change -- needs to be done across the codebase
31pub trait ResourceAlgebra: Sized {
32    /// Whether an element is valid
33    spec fn valid(self) -> bool;
34
35    /// Compose two elements
36    ///
37    /// Sometimes the notation `a · b` is used to represent `RA::op(a, b)`
38    spec fn op(a: Self, b: Self) -> Self;
39
40    /// The operation is associative
41    proof fn associative(a: Self, b: Self, c: Self)
42        ensures
43            Self::op(a, Self::op(b, c)) == Self::op(Self::op(a, b), c),
44    ;
45
46    /// The operation is commutative
47    proof fn commutative(a: Self, b: Self)
48        ensures
49            Self::op(a, b) == Self::op(b, a),
50    ;
51
52    /// The operation is closed under inclusion
53    /// (i.e., if the result of the operation is valid then its parts are also valid)
54    proof fn valid_op(a: Self, b: Self)
55        requires
56            Self::op(a, b).valid(),
57        ensures
58            a.valid(),
59    ;
60}
61
62/// Implementation of a [`Resource`] based on a [`ResourceAlgebra`]
63// This follows roughly the Iris from the Ground up construction
64impl<RA: ResourceAlgebra> Resource<RA> {
65    #[verifier::type_invariant]
66    spec fn inv(self) -> bool {
67        self.pcm.value() is Some
68    }
69
70    /// The underlying value of the resource
71    pub closed spec fn value(self) -> RA {
72        self.pcm.value()->Some_0
73    }
74
75    /// The location of the resource
76    pub closed spec fn loc(self) -> Loc {
77        self.pcm.loc()
78    }
79
80    /// Allocate a new resource at a fresh location
81    // GHOST-ALLOC rule
82    pub proof fn alloc(value: RA) -> (tracked out: Self)
83        requires
84            value.valid(),
85        ensures
86            out.value() == value,
87    {
88        let tracked pcm = pcm::Resource::alloc(Some(value));
89        Resource { pcm }
90    }
91
92    /// We can join together two resources at the same location, where we obtain the combination of
93    /// the two
94    // reverse implication in the GHOST-OP rule
95    pub proof fn join(tracked self, tracked other: Self) -> (tracked out: Self)
96        requires
97            self.loc() == other.loc(),
98        ensures
99            out.loc() == self.loc(),
100            out.value() == RA::op(self.value(), other.value()),
101    {
102        use_type_invariant(&self);
103        use_type_invariant(&other);
104        let tracked pcm = self.pcm.join(other.pcm);
105        Resource { pcm }
106    }
107
108    /// If a resource holds the result of a composition, we can split it into the components
109    // implication in the GHOST-OP rule
110    pub proof fn split(tracked self, left: RA, right: RA) -> (tracked out: (Self, Self))
111        requires
112            self.value() == RA::op(left, right),
113        ensures
114            out.0.loc() == self.loc(),
115            out.1.loc() == self.loc(),
116            out.0.value() == left,
117            out.1.value() == right,
118    {
119        use_type_invariant(&self);
120        let tracked (left, right) = self.pcm.split(Some(left), Some(right));
121        (Resource { pcm: left }, Resource { pcm: right })
122    }
123
124    /// Whenever we have a resource, that resource is valid. This intuitively (and inductively)
125    /// holds because:
126    ///     1. We only create valid resources (via [`alloc`]);
127    ///     2. We can only update the value of a resource via a [`frame_preserving_update_opt`] (see
128    ///        [`update`](Self::update) for more details. Because of the requirement of that
129    ///        updates are frame preserving this means that `join`s remain valid.
130    pub proof fn validate(tracked &self)
131        ensures
132            self.value().valid(),
133    {
134        use_type_invariant(self);
135        self.pcm.validate();
136    }
137
138    /// This is a more general version of [`update`](Self::update).
139    // GHOST-UPDATE rule
140    pub proof fn update_nondeterministic(tracked self, new_values: Set<RA>) -> (tracked out: Self)
141        requires
142            frame_preserving_update_nondeterministic_opt(self.value(), new_values),
143        ensures
144            out.loc() == self.loc(),
145            new_values.contains(out.value()),
146    {
147        use_type_invariant(&self);
148        let opt_new_values = new_values.map(|v| Some(v));
149        lemma_frame_preserving_update_nondeterministic_opt(self.value(), new_values);
150        let tracked pcm = self.pcm.update_nondeterministic(opt_new_values);
151        Resource { pcm }
152    }
153
154    /// Update a resource to a new value. This can only be done if the update is frame preserving
155    /// (i.e., any value that could be composed with the original value can still be composed with
156    /// the new value).
157    ///
158    /// See [`frame_preserving_update`] for more information.
159    // variant of the GHOST-UPDATE rule
160    pub proof fn update(tracked self, new_value: RA) -> (tracked out: Self)
161        requires
162            frame_preserving_update_opt(self.value(), new_value),
163        ensures
164            out.loc() == self.loc(),
165            out.value() == new_value,
166    {
167        let new_values = set![new_value];
168        assert(new_values.contains(new_value));
169        self.update_nondeterministic(new_values)
170    }
171
172    /// Extracts the resource from `r`, leaving `r` unspecified and returning
173    /// a new resource holding the previous value of `r`.
174    pub proof fn extract(tracked &mut self) -> (tracked other: Self)
175        ensures
176            other.loc() == old(self).loc(),
177            other.value() == old(self).value(),
178    {
179        self.validate();
180        let tracked mut other = Self::alloc(self.value());
181        tracked_swap(self, &mut other);
182        other
183    }
184
185    /// Validate two items at once. If we have two resources at the same location then its
186    /// composition is valid.
187    pub proof fn validate_2(tracked &mut self, tracked other: &Resource<RA>)
188        requires
189            old(self).loc() == other.loc(),
190        ensures
191            *final(self) == *old(self),
192            RA::op(final(self).value(), other.value()).valid(),
193    {
194        use_type_invariant(&*self);
195        use_type_invariant(other);
196        self.pcm.validate_2(&other.pcm);
197    }
198
199    /// We can do a similar update to [`update_with_shared`](Self::update_with_shared) for non-deterministic updates
200    pub proof fn update_nondeterministic_with_shared(
201        tracked self,
202        tracked other: &Resource<RA>,
203        new_values: Set<RA>,
204    ) -> (tracked out: Self)
205        requires
206            self.loc() == other.loc(),
207            frame_preserving_update_nondeterministic_opt(
208                RA::op(self.value(), other.value()),
209                set_op(new_values, other.value()),
210            ),
211        ensures
212            out.loc() == self.loc(),
213            new_values.contains(out.value()),
214    {
215        use_type_invariant(&self);
216        use_type_invariant(other);
217        let a = RA::op(self.value(), other.value());
218        let bs = set_op(new_values, other.value());
219
220        lemma_frame_preserving_update_nondeterministic_opt(a, bs);
221        lemma_set_op_opt(new_values, other.value());
222
223        let new_values_opt = new_values.map(|v| Some(v));
224        let tracked pcm = self.pcm.update_nondeterministic_with_shared(&other.pcm, new_values_opt);
225        Resource { pcm }
226    }
227
228    /// If `x · y --> x · z` is a frame-perserving update, and we have a shared reference to `x`,
229    /// we can update the `y` resource to `z`.
230    pub proof fn update_with_shared(
231        tracked self,
232        tracked other: &Resource<RA>,
233        new_value: RA,
234    ) -> (tracked out: Self)
235        requires
236            self.loc() == other.loc(),
237            frame_preserving_update_opt(
238                RA::op(self.value(), other.value()),
239                RA::op(new_value, other.value()),
240            ),
241        ensures
242            out.loc() == self.loc(),
243            out.value() == new_value,
244    {
245        let new_values = set![new_value];
246        let so = set_op(new_values, other.value());
247        assert(new_values.contains(new_value));
248        assert(so == set![new_value].map(|n| RA::op(new_value, other.value())));
249        assert(so.contains(RA::op(new_value, other.value())));
250        self.update_nondeterministic_with_shared(other, new_values)
251    }
252
253    /// This is useful when you have two (or more) shared resources and want to learn
254    /// that they agree, as you can combine this validate, e.g., `x.join_shared(y).validate()`.
255    pub proof fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out:
256        &'a Self)
257        requires
258            self.loc() == other.loc(),
259        ensures
260            out.loc() == self.loc(),
261            incl(self.value(), out.value()) || self.value() == out.value(),
262            incl(other.value(), out.value()) || other.value() == out.value(),
263    {
264        use_type_invariant(self);
265        use_type_invariant(other);
266        let tracked pcm = self.pcm.join_shared(&other.pcm);
267        assert(pcm.value() is Some);
268        assert(incl(Some(self.value()), pcm.value()));
269        assert(incl(Some(other.value()), pcm.value()));
270        lemma_incl_opt_rev(self.value(), pcm.value()->Some_0);
271        lemma_incl_opt_rev(other.value(), pcm.value()->Some_0);
272        Self::mk_ref(pcm)
273    }
274
275    /// Extract a shared reference to a preceding element in the extension order from a shared reference.
276    pub proof fn weaken(tracked &self, target: RA) -> (tracked out: &Self)
277        requires
278            incl(target, self.value()),
279        ensures
280            out.loc() == self.loc(),
281            out.value() == target,
282    {
283        use_type_invariant(self);
284        lemma_incl_opt(target, self.value());
285        let tracked pcm = self.pcm.weaken(Some(target));
286        Self::mk_ref(pcm)
287    }
288
289    /// If `x --> x · y` is a frame-perserving update, and we have a shared reference to `x`,
290    /// we can create a resource to y
291    pub proof fn duplicate_previous(tracked &self, value: RA) -> (tracked out: Self)
292        requires
293            frame_preserving_update_opt(self.value(), RA::op(value, self.value())),
294        ensures
295            out.loc() == self.loc(),
296            out.value() == value,
297    {
298        use_type_invariant(self);
299        let b = RA::op(value, self.value());
300        lemma_frame_preserving_opt(self.value(), b);
301        let tracked pcm = self.pcm.duplicate_previous(Some(value));
302        Resource { pcm }
303    }
304
305    /// We can do a similar update to [`update_with_shared`](Resource::update_with_shared) for non-deterministic updates
306    pub proof fn join_shared_to_target<'a>(
307        tracked &'a self,
308        tracked other: &'a Self,
309        target: RA,
310    ) -> (tracked out: &'a Self)
311        requires
312            self.loc() == other.loc(),
313            conjunct_shared(Some(self.value()), Some(other.value()), Some(target)),
314        ensures
315            out.loc() == self.loc(),
316            out.value() == target,
317    {
318        let tracked joined = self.join_shared(other);
319        joined.validate();
320        assert(Some(joined.value()).valid());
321        if self.value() == joined.value() {
322            Some(self.value()).op_unit();
323            assert(incl(Some(self.value()), Some(joined.value())));
324        } else {
325            lemma_incl_opt(self.value(), joined.value());
326        }
327        if other.value() == joined.value() {
328            Some(other.value()).op_unit();
329            assert(incl(Some(other.value()), Some(joined.value())));
330        } else {
331            lemma_incl_opt(other.value(), joined.value());
332        }
333        assert(incl(Some(target), Some(joined.value())));
334        lemma_incl_opt_rev(target, joined.value());
335        if joined.value() == target {
336            joined
337        } else {
338            joined.weaken(target)
339        }
340    }
341
342    proof fn mk_ref<'a>(tracked pcm: &'a pcm::Resource<Option<RA>>) -> (tracked res: &'a Self)
343        requires
344            pcm.value() is Some,
345        ensures
346            res.pcm == pcm,
347    {
348        shr_ref_struct_wrap(pcm, &Self { pcm: arbitrary() }, "", "pcm")
349    }
350}
351
352} // verus!
vstd/resource/algebra.rs

vstd/resource/
algebra.rs
