vstd/resource/
storage_protocol.rs

1use super::super::prelude::*;
2use super::Loc;
3
4verus! {
5
6broadcast use {super::super::iset::group_iset_lemmas, super::super::imap::group_imap_lemmas};
7
8/// Interface for "storage protocol" ghost state.
9/// This is an extension-slash-variant on the more well-known concept
10/// of "PCM" ghost state, which we also have an interface for [here](crate::resource::pcm::Resource).
11/// The unique feature of a storage protocol is the ability to use [`guard`](StorageResource::guard)
12/// to manipulate _shared_ references of ghost state.
13///
14/// Storage protocols are based on
15/// [_Leaf: Modularity for Temporary Sharing in Separation Logic_](https://dl.acm.org/doi/10.1145/3622798).
16///
17/// The reference for the laws and operations we're embedding here can be found at:
18/// <https://github.com/secure-foundations/leaf/blob/9d72b880feb6af0a7e752b2b2a43806a0812ad56/src/guarding/protocol_relational.v>
19///
20/// The reference version requires two monoids, the "protocol monoid" and the "base monoid".
21/// In this interface, we fix the base monoid to be of the form [`IMap<K, V>`](crate::imap::IMap).
22/// (with composition of overlapping maps being undefined), which has all the necessary properties.
23/// Note that there's no `create_unit` (it's not sound to do this for an arbitrary location unless you
24/// already know a protocol was initialized at that location).
25///
26/// For applications, I generally advise using the
27/// [`tokenized_state_machine!` system](https://verus-lang.github.io/verus/state_machines/),
28/// rather than using this interface directly.
29#[verifier::external_body]
30#[verifier::accept_recursive_types(K)]
31#[verifier::accept_recursive_types(P)]
32#[verifier::accept_recursive_types(V)]
33pub tracked struct StorageResource<K, V, P> {
34    _p: core::marker::PhantomData<(K, V, P)>,
35    _send_sync: super::super::state_machine_internal::SyncSendIfSyncSend<IMap<K, V>>,
36}
37
38#[cfg(verus_keep_ghost)]
39#[verifier::external]
40impl<K, V, P> !Copy for StorageResource<K, V, P> {
41
42}
43
44#[verifier::external_body]
45#[verifier::accept_recursive_types(K)]
46#[verifier::accept_recursive_types(P)]
47#[verifier::accept_recursive_types(V)]
48pub tracked struct CopyableStorageResource<K, V, P> {
49    _p: core::marker::PhantomData<(K, V, P)>,
50    _send_sync: super::super::state_machine_internal::SyncSendIfSyncSend<IMap<K, V>>,
51}
52
53impl<K, V, P> Copy for CopyableStorageResource<K, V, P> {
54
55}
56
57impl<K, V, P> Clone for CopyableStorageResource<K, V, P> {
58    #[verifier::external_body]
59    fn clone(&self) -> Self {
60        CopyableStorageResource {
61            _p: core::marker::PhantomData,
62            _send_sync: self._send_sync.clone(),
63        }
64    }
65}
66
67/// See [`StorageResource`] for more information.
68pub trait Protocol<K, V>: Sized {
69    spec fn op(self, other: Self) -> Self;
70
71    /// Note that `rel`, in contrast to [`PCM::valid`](crate::resource::algebra::ResourceAlgebra::valid), is not
72    /// necessarily closed under inclusion.
73    spec fn rel(self, s: IMap<K, V>) -> bool;
74
75    spec fn unit() -> Self;
76
77    proof fn commutative(a: Self, b: Self)
78        ensures
79            Self::op(a, b) == Self::op(b, a),
80    ;
81
82    proof fn associative(a: Self, b: Self, c: Self)
83        ensures
84            Self::op(a, Self::op(b, c)) == Self::op(Self::op(a, b), c),
85    ;
86
87    proof fn op_unit(a: Self)
88        ensures
89            Self::op(a, Self::unit()) == a,
90    ;
91}
92
93pub open spec fn incl<K, V, P: Protocol<K, V>>(a: P, b: P) -> bool {
94    exists|c| P::op(a, c) == b
95}
96
97pub open spec fn guards<K, V, P: Protocol<K, V>>(p: P, b: IMap<K, V>) -> bool {
98    forall|q: P, t: IMap<K, V>| #![all_triggers] P::rel(P::op(p, q), t) ==> b.submap_of(t)
99}
100
101pub open spec fn exchanges<K, V, P: Protocol<K, V>>(
102    p1: P,
103    b1: IMap<K, V>,
104    p2: P,
105    b2: IMap<K, V>,
106) -> bool {
107    forall|q: P, t1: IMap<K, V>|
108        #![all_triggers]
109        P::rel(P::op(p1, q), t1) ==> {
110            &&& P::rel(P::op(p2, q), t1.union_prefer_right(b1).remove_keys(b2.dom()))
111            &&& t1.dom().disjoint(b1.dom())
112            &&& b2.submap_of(t1.union_prefer_right(b1))
113        }
114}
115
116pub open spec fn exchanges_nondeterministic<K, V, P: Protocol<K, V>>(
117    p1: P,
118    s1: IMap<K, V>,
119    new_values: ISet<(P, IMap<K, V>)>,
120) -> bool {
121    forall|q: P, t1: IMap<K, V>|
122        #![all_triggers]
123        P::rel(P::op(p1, q), t1) ==> exists|p2: P, s2: IMap<K, V>, t2: IMap<K, V>|
124            #![all_triggers]
125            {
126                &&& new_values.contains((p2, s2))
127                &&& P::rel(P::op(p2, q), t2)
128                &&& t1.dom().disjoint(s1.dom())
129                &&& t2.dom().disjoint(s2.dom())
130                &&& t1.union_prefer_right(s1) =~= t2.union_prefer_right(s2)
131            }
132}
133
134pub open spec fn deposits<K, V, P: Protocol<K, V>>(p1: P, b1: IMap<K, V>, p2: P) -> bool {
135    forall|q: P, t1: IMap<K, V>|
136        #![all_triggers]
137        P::rel(P::op(p1, q), t1) ==> {
138            &&& P::rel(P::op(p2, q), t1.union_prefer_right(b1))
139            &&& t1.dom().disjoint(b1.dom())
140        }
141}
142
143pub open spec fn withdraws<K, V, P: Protocol<K, V>>(p1: P, p2: P, b2: IMap<K, V>) -> bool {
144    forall|q: P, t1: IMap<K, V>|
145        #![all_triggers]
146        P::rel(P::op(p1, q), t1) ==> {
147            &&& P::rel(P::op(p2, q), t1.remove_keys(b2.dom()))
148            &&& b2.submap_of(t1)
149        }
150}
151
152pub open spec fn updates<K, V, P: Protocol<K, V>>(p1: P, p2: P) -> bool {
153    forall|q: P, t1: IMap<K, V>|
154        #![all_triggers]
155        P::rel(P::op(p1, q), t1) ==> P::rel(P::op(p2, q), t1)
156}
157
158pub open spec fn set_op<K, V, P: Protocol<K, V>>(s: ISet<(P, IMap<K, V>)>, t: P) -> ISet<
159    (P, IMap<K, V>),
160> {
161    s.map(|q: (P, IMap<K, V>)| (P::op(q.0, t), q.1))
162}
163
164impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
165    pub uninterp spec fn value(self) -> P;
166
167    pub uninterp spec fn loc(self) -> Loc;
168
169    pub axiom fn alloc(p: P, tracked s: IMap<K, V>) -> (tracked out: Self)
170        requires
171            P::rel(p, s),
172        ensures
173            out.value() == p,
174    ;
175
176    pub axiom fn join(tracked a: Self, tracked b: Self) -> (tracked out: Self)
177        requires
178            a.loc() == b.loc(),
179        ensures
180            out.loc() == a.loc(),
181            out.value() == P::op(a.value(), b.value()),
182    ;
183
184    pub axiom fn split(tracked self, a_value: P, b_value: P) -> (tracked out: (Self, Self))
185        requires
186            self.value() == P::op(a_value, b_value),
187        ensures
188            out.0.loc() == self.loc(),
189            out.1.loc() == self.loc(),
190            out.0.value() == a_value,
191            out.1.value() == b_value,
192    ;
193
194    /// Since `inv` isn't closed under inclusion, validity for an element
195    /// is defined as the inclusion-closure of invariant, i.e., an element
196    /// is valid if there exists another element `x` that, added to it,
197    /// meets the invariant.
198    pub axiom fn validate(tracked self: &Self) -> (out: (P, IMap<K, V>))
199        ensures
200            ({
201                let (q, t) = out;
202                P::rel(P::op(self.value(), q), t)
203            }),
204    ;
205
206    // Helper lemma saying that unioning with an empty map is a no-op.
207    proof fn lemma_union_prefer_right_empty_is_noop_forall()
208        ensures
209            forall|m: IMap<K, V>| #[trigger] m.union_prefer_right(IMap::empty()) == m,
210    {
211        assert forall|m: IMap<K, V>| #[trigger] m.union_prefer_right(IMap::empty()) == m by {
212            assert(m.union_prefer_right(IMap::empty()) =~= m);
213        }
214    }
215
216    // Helper lemma saying that removing the empty set of keys from a map is a no-op.
217    proof fn lemma_removing_empty_keys_is_noop_forall()
218        ensures
219            forall|m: IMap<K, V>| #[trigger] m.remove_keys(ISet::empty()) == m,
220    {
221        assert forall|m: IMap<K, V>| m.remove_keys(ISet::empty()) == m by {
222            assert(m.remove_keys(ISet::empty()) =~= m);
223        }
224    }
225
226    // Updates and guards
227    /// Most general kind of update, potentially depositing and withdrawing
228    pub proof fn exchange(
229        tracked p: Self,
230        tracked s: IMap<K, V>,
231        new_p_value: P,
232        new_s_value: IMap<K, V>,
233    ) -> (tracked out: (Self, IMap<K, V>))
234        requires
235            exchanges(p.value(), s, new_p_value, new_s_value),
236        ensures
237            ({
238                let (new_p, new_s) = out;
239                new_p.loc() == p.loc() && new_p.value() == new_p_value && new_s == new_s_value
240            }),
241    {
242        let se = iset![(new_p_value, new_s_value)];
243        Self::exchange_nondeterministic(p, s, se)
244    }
245
246    pub proof fn deposit(tracked self, tracked base: IMap<K, V>, new_value: P) -> (tracked out:
247        Self)
248        requires
249            deposits(self.value(), base, new_value),
250        ensures
251            out.loc() == self.loc(),
252            out.value() == new_value,
253    {
254        Self::lemma_removing_empty_keys_is_noop_forall();
255        Self::exchange(self, base, new_value, IMap::empty()).0
256    }
257
258    pub proof fn withdraw(tracked self, new_value: P, new_base: IMap<K, V>) -> (tracked out: (
259        Self,
260        IMap<K, V>,
261    ))
262        requires
263            withdraws(self.value(), new_value, new_base),
264        ensures
265            out.0.loc() == self.loc(),
266            out.0.value() == new_value,
267            out.1 == new_base,
268    {
269        Self::lemma_union_prefer_right_empty_is_noop_forall();
270        Self::exchange(self, IMap::tracked_empty(), new_value, new_base)
271    }
272
273    /// "Normal" update, no depositing or withdrawing
274    pub proof fn update(tracked self, new_value: P) -> (tracked out: Self)
275        requires
276            updates(self.value(), new_value),
277        ensures
278            out.loc() == self.loc(),
279            out.value() == new_value,
280    {
281        Self::lemma_union_prefer_right_empty_is_noop_forall();
282        Self::lemma_removing_empty_keys_is_noop_forall();
283        Self::exchange(self, IMap::tracked_empty(), new_value, IMap::empty()).0
284    }
285
286    pub proof fn exchange_nondeterministic(
287        tracked p: Self,
288        tracked s: IMap<K, V>,
289        new_values: ISet<(P, IMap<K, V>)>,
290    ) -> (tracked out: (Self, IMap<K, V>))
291        requires
292            exchanges_nondeterministic(p.value(), s, new_values),
293        ensures
294            ({
295                let (new_p, new_s) = out;
296                new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
297            }),
298    {
299        P::op_unit(p.value());
300        let tracked (selff, unit) = p.split(p.value(), P::unit());
301        let new_values0 = set_op(new_values, P::unit());
302        super::super::iset_lib::assert_isets_equal!(new_values0, new_values, v => {
303            P::op_unit(v.0);
304            if new_values.contains(v) {
305                assert(new_values0.contains(v));
306            }
307            if new_values0.contains(v) {
308                let q = choose |q| #[trigger] new_values.contains(q) && v == (P::op(q.0, P::unit()), q.1);
309                assert(P::op(q.0, P::unit()) == q.0) by { P::op_unit(q.0) }
310                assert(v =~= q);
311                assert(new_values.contains(v));
312            }
313        });
314        Self::exchange_nondeterministic_with_shared(selff, &unit, s, new_values)
315    }
316
317    pub axiom fn guard(tracked p: &Self, s_value: IMap<K, V>) -> (tracked s: &IMap<K, V>)
318        requires
319            guards(p.value(), s_value),
320        ensures
321            s == s_value,
322    ;
323
324    // Operations with shared references
325    pub axiom fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out:
326        &'a Self)
327        requires
328            self.loc() == other.loc(),
329        ensures
330            out.loc() == self.loc(),
331            incl(self.value(), out.value()),
332            incl(other.value(), out.value()),
333    ;
334
335    pub axiom fn weaken<'a>(tracked &'a self, target: P) -> (tracked out: &'a Self)
336        requires
337            incl(target, self.value()),
338        ensures
339            out.loc() == self.loc(),
340            out.value() == target,
341    ;
342
343    pub axiom fn validate_with_shared(tracked self: &mut Self, tracked x: &Self) -> (res: (
344        P,
345        IMap<K, V>,
346    ))
347        requires
348            old(self).loc() == x.loc(),
349        ensures
350            *final(self) == *old(self),
351            ({
352                let (q, t) = res;
353                { P::rel(P::op(P::op(final(self).value(), x.value()), q), t) }
354            }),
355    ;
356
357    // See `logic_exchange_with_extra_guard`
358    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L720
359    pub proof fn exchange_with_shared(
360        tracked p: Self,
361        tracked x: &Self,
362        tracked s: IMap<K, V>,
363        new_p_value: P,
364        new_s_value: IMap<K, V>,
365    ) -> (tracked out: (Self, IMap<K, V>))
366        requires
367            p.loc() == x.loc(),
368            exchanges(P::op(p.value(), x.value()), s, P::op(new_p_value, x.value()), new_s_value),
369        ensures
370            out.0.loc() == p.loc(),
371            out.0.value() == new_p_value,
372            out.1 == new_s_value,
373    {
374        let se = iset![(new_p_value, new_s_value)];
375        assert(exchanges_nondeterministic(P::op(p.value(), x.value()), s, set_op(se, x.value())))
376            by {
377            let new_values = set_op(se, x.value());
378            assert(se.contains((new_p_value, new_s_value)));
379            assert(new_values.contains((P::op(new_p_value, x.value()), new_s_value)));
380        }
381        Self::exchange_nondeterministic_with_shared(p, x, s, se)
382    }
383
384    // See `logic_exchange_with_extra_guard_nondeterministic`
385    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L834
386    /// Most general kind of update, potentially depositing and withdrawing
387    pub axiom fn exchange_nondeterministic_with_shared(
388        tracked p: Self,
389        tracked x: &Self,
390        tracked s: IMap<K, V>,
391        new_values: ISet<(P, IMap<K, V>)>,
392    ) -> (tracked out: (Self, IMap<K, V>))
393        requires
394            p.loc() == x.loc(),
395            exchanges_nondeterministic(
396                P::op(p.value(), x.value()),
397                s,
398                set_op(new_values, x.value()),
399            ),
400        ensures
401            ({
402                let (new_p, new_s) = out;
403                new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
404            }),
405    ;
406
407    /// Wrap this resource in a type that implements `Copy`,
408    /// given that the resource is duplicable.
409    pub axiom fn into_copyable(self, p: P) -> (r: CopyableStorageResource<K, V, P>)
410        requires
411            P::op(P::op(self.value(), self.value()), p) == self.value(),
412        ensures
413            r.loc() == self.loc(),
414            r.value() == self.value(),
415    ;
416}
417
418/// A variant of [`StorageResource`] that implements `Copy`.
419///
420/// Use [`Self::into_resource`] to get the underlying resource.
421impl<K, V, P: Protocol<K, V>> CopyableStorageResource<K, V, P> {
422    /// The underlying value of the resource
423    pub uninterp spec fn value(self) -> P;
424
425    /// The location of the resource
426    pub uninterp spec fn loc(self) -> Loc;
427
428    pub axiom fn into_resource(self) -> (r: StorageResource<K, V, P>)
429        ensures
430            r.loc() == self.loc(),
431            r.value() == self.value(),
432    ;
433}
434
435} // verus!
vstd/resource/storage_protocol.rs

vstd/resource/
storage_protocol.rs
