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

vstd/resource/
algebra.rs
