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

vstd/resource/
storage_protocol.rs
