vstd/
storage_protocol.rs

Help
1use super::pcm::Loc;
2use super::prelude::*;
3
4verus! {
5
6broadcast use {super::set::group_set_axioms, super::map::group_map_axioms};
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::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 [`Map<K, V>`](crate::map::Map).
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::state_machine_internal::SyncSendIfSyncSend<Map<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::pcm::PCM::valid), is not
43    /// necessarily closed under inclusion.
44    spec fn rel(self, s: Map<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: Map<K, V>) -> bool {
69    forall|q: P, t: Map<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: Map<K, V>,
75    p2: P,
76    b2: Map<K, V>,
77) -> bool {
78    forall|q: P, t1: Map<K, V>|
79        #![all_triggers]
80        P::rel(P::op(p1, q), t1) ==> exists|t2: Map<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: Map<K, V>,
89    new_values: Set<(P, Map<K, V>)>,
90) -> bool {
91    forall|q: P, t1: Map<K, V>|
92        #![all_triggers]
93        P::rel(P::op(p1, q), t1) ==> exists|p2: P, s2: Map<K, V>, t2: Map<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: Map<K, V>, p2: P) -> bool {
101    forall|q: P, t1: Map<K, V>|
102        #![all_triggers]
103        P::rel(P::op(p1, q), t1) ==> exists|t2: Map<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: Map<K, V>) -> bool {
110    forall|q: P, t1: Map<K, V>|
111        #![all_triggers]
112        P::rel(P::op(p1, q), t1) ==> exists|t2: Map<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: Map<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: Set<(P, Map<K, V>)>, t: P) -> Set<
126    (P, Map<K, V>),
127> {
128    Set::new(|v: (P, Map<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: Map<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, Map<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: Map<K, V>,
178        new_p_value: P,
179        new_s_value: Map<K, V>,
180    ) -> (tracked out: (Self, Map<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 = set![(new_p_value, new_s_value)];
190        Self::exchange_nondeterministic(p, s, se)
191    }
192
193    pub proof fn deposit(tracked self, tracked base: Map<K, V>, new_value: P) -> (tracked out: Self)
194        requires
195            deposits(self.value(), base, new_value),
196        ensures
197            out.loc() == self.loc(),
198            out.value() == new_value,
199    {
200        Self::exchange(self, base, new_value, Map::empty()).0
201    }
202
203    pub proof fn withdraw(tracked self, new_value: P, new_base: Map<K, V>) -> (tracked out: (
204        Self,
205        Map<K, V>,
206    ))
207        requires
208            withdraws(self.value(), new_value, new_base),
209        ensures
210            out.0.loc() == self.loc(),
211            out.0.value() == new_value,
212            out.1 == new_base,
213    {
214        Self::exchange(self, Map::tracked_empty(), new_value, new_base)
215    }
216
217    /// "Normal" update, no depositing or withdrawing
218    pub proof fn update(tracked self, new_value: P) -> (tracked out: Self)
219        requires
220            updates(self.value(), new_value),
221        ensures
222            out.loc() == self.loc(),
223            out.value() == new_value,
224    {
225        Self::exchange(self, Map::tracked_empty(), new_value, Map::empty()).0
226    }
227
228    pub proof fn exchange_nondeterministic(
229        tracked p: Self,
230        tracked s: Map<K, V>,
231        new_values: Set<(P, Map<K, V>)>,
232    ) -> (tracked out: (Self, Map<K, V>))
233        requires
234            exchanges_nondeterministic(p.value(), s, new_values),
235        ensures
236            ({
237                let (new_p, new_s) = out;
238                new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
239            }),
240    {
241        P::op_unit(p.value());
242        let tracked (selff, unit) = p.split(p.value(), P::unit());
243        let new_values0 = set_op(new_values, P::unit());
244        super::set_lib::assert_sets_equal!(new_values0, new_values, v => {
245            P::op_unit(v.0);
246            if new_values.contains(v) {
247                assert(new_values0.contains(v));
248            }
249            if new_values0.contains(v) {
250                let q = choose |q| new_values.contains((q, v.1)) && v.0 == #[trigger] P::op(q, P::unit());
251                P::op_unit(q);
252                assert(new_values.contains(v));
253            }
254        });
255        Self::exchange_nondeterministic_with_shared(selff, &unit, s, new_values)
256    }
257
258    pub axiom fn guard(tracked p: &Self, s_value: Map<K, V>) -> (tracked s: &Map<K, V>)
259        requires
260            guards(p.value(), s_value),
261        ensures
262            s == s_value,
263    ;
264
265    // Operations with shared references
266    pub axiom fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out:
267        &'a Self)
268        requires
269            self.loc() == other.loc(),
270        ensures
271            out.loc() == self.loc(),
272            incl(self.value(), out.value()),
273            incl(other.value(), out.value()),
274    ;
275
276    pub axiom fn weaken<'a>(tracked &'a self, target: P) -> (tracked out: &'a Self)
277        requires
278            incl(target, self.value()),
279        ensures
280            out.loc() == self.loc(),
281            out.value() == target,
282    ;
283
284    pub axiom fn validate_with_shared(tracked self: &mut Self, tracked x: &Self) -> (res: (
285        P,
286        Map<K, V>,
287    ))
288        requires
289            old(self).loc() == x.loc(),
290        ensures
291            *self == *old(self),
292            ({
293                let (q, t) = res;
294                { P::rel(P::op(P::op(self.value(), x.value()), q), t) }
295            }),
296    ;
297
298    // See `logic_exchange_with_extra_guard`
299    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L720
300    pub proof fn exchange_with_shared(
301        tracked p: Self,
302        tracked x: &Self,
303        tracked s: Map<K, V>,
304        new_p_value: P,
305        new_s_value: Map<K, V>,
306    ) -> (tracked out: (Self, Map<K, V>))
307        requires
308            p.loc() == x.loc(),
309            exchanges(P::op(p.value(), x.value()), s, P::op(new_p_value, x.value()), new_s_value),
310        ensures
311            out.0.loc() == p.loc(),
312            out.0.value() == new_p_value,
313            out.1 == new_s_value,
314    {
315        let se = set![(new_p_value, new_s_value)];
316        Self::exchange_nondeterministic_with_shared(p, x, s, se)
317    }
318
319    // See `logic_exchange_with_extra_guard_nondeterministic`
320    // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L834
321    /// Most general kind of update, potentially depositing and withdrawing
322    pub axiom fn exchange_nondeterministic_with_shared(
323        tracked p: Self,
324        tracked x: &Self,
325        tracked s: Map<K, V>,
326        new_values: Set<(P, Map<K, V>)>,
327    ) -> (tracked out: (Self, Map<K, V>))
328        requires
329            p.loc() == x.loc(),
330            exchanges_nondeterministic(
331                P::op(p.value(), x.value()),
332                s,
333                set_op(new_values, x.value()),
334            ),
335        ensures
336            ({
337                let (new_p, new_s) = out;
338                new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s))
339            }),
340    ;
341}
342
343} // verus!
vstd/storage_protocol.rs

vstd/
storage_protocol.rs
