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/// See [`StorageResource`] for more information.
39pub trait Protocol<K, V>: Sized {
40    spec fn op(self, other: Self) -> Self;
41
42    /// Note that `rel`, in contrast to [`PCM::valid`](crate::resource::algebra::ResourceAlgebra::valid), is not
43    /// necessarily closed under inclusion.
44    spec fn rel(self, s: IMap<K, V>) -> bool;
45
46    spec fn unit() -> Self;
47
48    proof fn commutative(a: Self, b: Self)
49        ensures
50            Self::op(a, b) == Self::op(b, a),
51    ;
52
53    proof fn associative(a: Self, b: Self, c: Self)
54        ensures
55            Self::op(a, Self::op(b, c)) == Self::op(Self::op(a, b), c),
56    ;
57
58    proof fn op_unit(a: Self)
59        ensures
60            Self::op(a, Self::unit()) == a,
61    ;
62}
63
64pub open spec fn incl<K, V, P: Protocol<K, V>>(a: P, b: P) -> bool {
65    exists|c| P::op(a, c) == b
66}
67
68pub open spec fn guards<K, V, P: Protocol<K, V>>(p: P, b: IMap<K, V>) -> bool {
69    forall|q: P, t: IMap<K, V>| #![all_triggers] P::rel(P::op(p, q), t) ==> b.submap_of(t)
70}
71
72pub open spec fn exchanges<K, V, P: Protocol<K, V>>(
73    p1: P,
74    b1: IMap<K, V>,
75    p2: P,
76    b2: IMap<K, V>,
77) -> bool {
78    forall|q: P, t1: IMap<K, V>|
79        #![all_triggers]
80        P::rel(P::op(p1, q), t1) ==> {
81            &&& P::rel(P::op(p2, q), t1.union_prefer_right(b1).remove_keys(b2.dom()))
82            &&& t1.dom().disjoint(b1.dom())
83            &&& b2.submap_of(t1.union_prefer_right(b1))
84        }
85}
86
87pub open spec fn exchanges_nondeterministic<K, V, P: Protocol<K, V>>(
88    p1: P,
89    s1: IMap<K, V>,
90    new_values: ISet<(P, IMap<K, V>)>,
91) -> bool {
92    forall|q: P, t1: IMap<K, V>|
93        #![all_triggers]
94        P::rel(P::op(p1, q), t1) ==> exists|p2: P, s2: IMap<K, V>, t2: IMap<K, V>|
95            #![all_triggers]
96            {
97                &&& new_values.contains((p2, s2))
98                &&& P::rel(P::op(p2, q), t2)
99                &&& t1.dom().disjoint(s1.dom())
100                &&& t2.dom().disjoint(s2.dom())
101                &&& t1.union_prefer_right(s1) =~= t2.union_prefer_right(s2)
102            }
103}
104
105pub open spec fn deposits<K, V, P: Protocol<K, V>>(p1: P, b1: IMap<K, V>, p2: P) -> bool {
106    forall|q: P, t1: IMap<K, V>|
107        #![all_triggers]
108        P::rel(P::op(p1, q), t1) ==> {
109            &&& P::rel(P::op(p2, q), t1.union_prefer_right(b1))
110            &&& t1.dom().disjoint(b1.dom())
111        }
112}
113
114pub open spec fn withdraws<K, V, P: Protocol<K, V>>(p1: P, p2: P, b2: IMap<K, V>) -> bool {
115    forall|q: P, t1: IMap<K, V>|
116        #![all_triggers]
117        P::rel(P::op(p1, q), t1) ==> {
118            &&& P::rel(P::op(p2, q), t1.remove_keys(b2.dom()))
119            &&& b2.submap_of(t1)
120        }
121}
122
123pub open spec fn updates<K, V, P: Protocol<K, V>>(p1: P, p2: P) -> bool {
124    forall|q: P, t1: IMap<K, V>|
125        #![all_triggers]
126        P::rel(P::op(p1, q), t1) ==> P::rel(P::op(p2, q), t1)
127}
128
129pub open spec fn set_op<K, V, P: Protocol<K, V>>(s: ISet<(P, IMap<K, V>)>, t: P) -> ISet<
130    (P, IMap<K, V>),
131> {
132    s.map(|q: (P, IMap<K, V>)| (P::op(q.0, t), q.1))
133}
134
135impl<K, V, P: Protocol<K, V>> StorageResource<K, V, P> {
136    pub uninterp spec fn value(self) -> P;
137
138    pub uninterp spec fn loc(self) -> Loc;
139
140    pub axiom fn alloc(p: P, tracked s: IMap<K, V>) -> (tracked out: Self)
141        requires
142            P::rel(p, s),
143        ensures
144            out.value() == p,
145    ;
146
147    pub axiom fn join(tracked a: Self, tracked b: Self) -> (tracked out: Self)
148        requires
149            a.loc() == b.loc(),
150        ensures
151            out.loc() == a.loc(),
152            out.value() == P::op(a.value(), b.value()),
153    ;
154
155    pub axiom fn split(tracked self, a_value: P, b_value: P) -> (tracked out: (Self, Self))
156        requires
157            self.value() == P::op(a_value, b_value),
158        ensures
159            out.0.loc() == self.loc(),
160            out.1.loc() == self.loc(),
161            out.0.value() == a_value,
162            out.1.value() == b_value,
163    ;
164
165    /// Since `inv` isn't closed under inclusion, validity for an element
166    /// is defined as the inclusion-closure of invariant, i.e., an element
167    /// is valid if there exists another element `x` that, added to it,
168    /// meets the invariant.
169    pub axiom fn validate(tracked self: &Self) -> (out: (P, IMap<K, V>))
170        ensures
171            ({
172                let (q, t) = out;
173                P::rel(P::op(self.value(), q), t)
174            }),
175    ;
176
177    // Helper lemma saying that unioning with an empty map is a no-op.
178    proof fn lemma_union_prefer_right_empty_is_noop_forall()
179        ensures
180            forall|m: IMap<K, V>| #[trigger] m.union_prefer_right(IMap::empty()) == m,
181    {
182        assert forall|m: IMap<K, V>| #[trigger] m.union_prefer_right(IMap::empty()) == m by {
183            assert(m.union_prefer_right(IMap::empty()) =~= m);
184        }
185    }
186
187    // Helper lemma saying that removing the empty set of keys from a map is a no-op.
188    proof fn lemma_removing_empty_keys_is_noop_forall()
189        ensures
190            forall|m: IMap<K, V>| #[trigger] m.remove_keys(ISet::empty()) == m,
191    {
192        assert forall|m: IMap<K, V>| m.remove_keys(ISet::empty()) == m by {
193            assert(m.remove_keys(ISet::empty()) =~= m);
194        }
195    }
196
197    // Updates and guards
198    /// Most general kind of update, potentially depositing and withdrawing
199    pub proof fn exchange(
200        tracked p: Self,
201        tracked s: IMap<K, V>,
202        new_p_value: P,
203        new_s_value: IMap<K, V>,
204    ) -> (tracked out: (Self, IMap<K, V>))
205        requires
206            exchanges(p.value(), s, new_p_value, new_s_value),
207        ensures
208            ({
209                let (new_p, new_s) = out;
210                new_p.loc() == p.loc() && new_p.value() == new_p_value && new_s == new_s_value
211            }),
212    {
213        let se = iset![(new_p_value, new_s_value)];
214        Self::exchange_nondeterministic(p, s, se)
215    }
216
217    pub proof fn deposit(tracked self, tracked base: IMap<K, V>, new_value: P) -> (tracked out:
218        Self)
219        requires
220            deposits(self.value(), base, new_value),
221        ensures
222            out.loc() == self.loc(),
223            out.value() == new_value,
224    {
225        Self::lemma_removing_empty_keys_is_noop_forall();
226        Self::exchange(self, base, new_value, IMap::empty()).0
227    }
228
229    pub proof fn withdraw(tracked self, new_value: P, new_base: IMap<K, V>) -> (tracked out: (
230        Self,
231        IMap<K, V>,
232    ))
233        requires
234            withdraws(self.value(), new_value, new_base),
235        ensures
236            out.0.loc() == self.loc(),
237            out.0.value() == new_value,
238            out.1 == new_base,
239    {
240        Self::lemma_union_prefer_right_empty_is_noop_forall();
241        Self::exchange(self, IMap::tracked_empty(), new_value, new_base)
242    }
243
244    /// "Normal" update, no depositing or withdrawing
245    pub proof fn update(tracked self, new_value: P) -> (tracked out: Self)
246        requires
247            updates(self.value(), new_value),
248        ensures
249            out.loc() == self.loc(),
250            out.value() == new_value,
251    {
252        Self::lemma_union_prefer_right_empty_is_noop_forall();
253        Self::lemma_removing_empty_keys_is_noop_forall();
254        Self::exchange(self, IMap::tracked_empty(), new_value, IMap::empty()).0
255    }
256
257    pub proof fn exchange_nondeterministic(
258        tracked p: Self,
259        tracked s: IMap<K, V>,
260        new_values: ISet<(P, IMap<K, V>)>,
261    ) -> (tracked out: (Self, IMap<K, V>))
262        requires
263            exchanges_nondeterministic(p.value(), s, new_values),
264        ensures
265            ({
266                let (new_p, new_s) = out;
267                new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
268            }),
269    {
270        P::op_unit(p.value());
271        let tracked (selff, unit) = p.split(p.value(), P::unit());
272        let new_values0 = set_op(new_values, P::unit());
273        super::super::iset_lib::assert_isets_equal!(new_values0, new_values, v => {
274            P::op_unit(v.0);
275            if new_values.contains(v) {
276                assert(new_values0.contains(v));
277            }
278            if new_values0.contains(v) {
279                let q = choose |q| #[trigger] new_values.contains(q) && v == (P::op(q.0, P::unit()), q.1);
280                assert(P::op(q.0, P::unit()) == q.0) by { P::op_unit(q.0) }
281                assert(v =~= q);
282                assert(new_values.contains(v));
283            }
284        });
285        Self::exchange_nondeterministic_with_shared(selff, &unit, s, new_values)
286    }
287
288    pub axiom fn guard(tracked p: &Self, s_value: IMap<K, V>) -> (tracked s: &IMap<K, V>)
289        requires
290            guards(p.value(), s_value),
291        ensures
292            s == s_value,
293    ;
294
295    // Operations with shared references
296    pub axiom fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out:
297        &'a Self)
298        requires
299            self.loc() == other.loc(),
300        ensures
301            out.loc() == self.loc(),
302            incl(self.value(), out.value()),
303            incl(other.value(), out.value()),
304    ;
305
306    pub axiom fn weaken<'a>(tracked &'a self, target: P) -> (tracked out: &'a Self)
307        requires
308            incl(target, self.value()),
309        ensures
310            out.loc() == self.loc(),
311            out.value() == target,
312    ;
313
314    pub axiom fn validate_with_shared(tracked self: &mut Self, tracked x: &Self) -> (res: (
315        P,
316        IMap<K, V>,
317    ))
318        requires
319            old(self).loc() == x.loc(),
320        ensures
321            *final(self) == *old(self),
322            ({
323                let (q, t) = res;
324                { P::rel(P::op(P::op(final(self).value(), x.value()), q), t) }
325            }),
326    ;
327
328    // See `logic_exchange_with_extra_guard`
329    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L720
330    pub proof fn exchange_with_shared(
331        tracked p: Self,
332        tracked x: &Self,
333        tracked s: IMap<K, V>,
334        new_p_value: P,
335        new_s_value: IMap<K, V>,
336    ) -> (tracked out: (Self, IMap<K, V>))
337        requires
338            p.loc() == x.loc(),
339            exchanges(P::op(p.value(), x.value()), s, P::op(new_p_value, x.value()), new_s_value),
340        ensures
341            out.0.loc() == p.loc(),
342            out.0.value() == new_p_value,
343            out.1 == new_s_value,
344    {
345        let se = iset![(new_p_value, new_s_value)];
346        assert(exchanges_nondeterministic(P::op(p.value(), x.value()), s, set_op(se, x.value())))
347            by {
348            let new_values = set_op(se, x.value());
349            assert(se.contains((new_p_value, new_s_value)));
350            assert(new_values.contains((P::op(new_p_value, x.value()), new_s_value)));
351        }
352        Self::exchange_nondeterministic_with_shared(p, x, s, se)
353    }
354
355    // See `logic_exchange_with_extra_guard_nondeterministic`
356    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L834
357    /// Most general kind of update, potentially depositing and withdrawing
358    pub axiom fn exchange_nondeterministic_with_shared(
359        tracked p: Self,
360        tracked x: &Self,
361        tracked s: IMap<K, V>,
362        new_values: ISet<(P, IMap<K, V>)>,
363    ) -> (tracked out: (Self, IMap<K, V>))
364        requires
365            p.loc() == x.loc(),
366            exchanges_nondeterministic(
367                P::op(p.value(), x.value()),
368                s,
369                set_op(new_values, x.value()),
370            ),
371        ensures
372            ({
373                let (new_p, new_s) = out;
374                new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
375            }),
376    ;
377}
378
379} // verus!
vstd/resource/storage_protocol.rs

vstd/resource/
storage_protocol.rs
