vstd/tokens/
map.rs

1use super::super::map::*;
2use super::super::map_lib::*;
3use super::super::modes::*;
4use super::super::pcm::*;
5use super::super::prelude::*;
6
7// This implements a resource for ownership of subsets of keys in a map.
8
9verus! {
10
11broadcast use super::super::group_vstd_default;
12
13#[verifier::reject_recursive_types(K)]
14#[verifier::ext_equal]
15struct MapCarrier<K, V> {
16    auth: Option<Option<Map<K, V>>>,
17    frac: Option<Map<K, V>>,
18}
19
20impl<K, V> PCM for MapCarrier<K, V> {
21    closed spec fn valid(self) -> bool {
22        match self.frac {
23            None => false,
24            Some(f) => match self.auth {
25                None => true,
26                Some(None) => false,
27                Some(Some(a)) => f.submap_of(a),
28            },
29        }
30    }
31
32    closed spec fn op(self, other: Self) -> Self {
33        MapCarrier {
34            auth: if self.auth is Some {
35                if other.auth is Some {
36                    Some(None)
37                } else {
38                    self.auth
39                }
40            } else {
41                other.auth
42            },
43            frac: match self.frac {
44                None => None,
45                Some(sfr) => match other.frac {
46                    None => None,
47                    Some(ofr) => {
48                        if sfr.dom().disjoint(ofr.dom()) {
49                            Some(sfr.union_prefer_right(ofr))
50                        } else {
51                            None
52                        }
53                    },
54                },
55            },
56        }
57    }
58
59    closed spec fn unit() -> Self {
60        MapCarrier { auth: None, frac: Some(Map::empty()) }
61    }
62
63    proof fn closed_under_incl(a: Self, b: Self) {
64        broadcast use lemma_submap_of_trans;
65        broadcast use lemma_op_frac_submap_of;
66
67    }
68
69    proof fn commutative(a: Self, b: Self) {
70        let ab = Self::op(a, b);
71        let ba = Self::op(b, a);
72        assert(ab == ba);
73    }
74
75    proof fn associative(a: Self, b: Self, c: Self) {
76        let bc = Self::op(b, c);
77        let ab = Self::op(a, b);
78        let a_bc = Self::op(a, bc);
79        let ab_c = Self::op(ab, c);
80        assert(a_bc == ab_c);
81    }
82
83    proof fn op_unit(a: Self) {
84        let x = Self::op(a, Self::unit());
85        assert(a == x);
86    }
87
88    proof fn unit_valid() {
89    }
90}
91
92broadcast proof fn lemma_op_frac_submap_of<K, V>(a: MapCarrier<K, V>, b: MapCarrier<K, V>)
93    requires
94        #[trigger] MapCarrier::op(a, b).valid(),
95    ensures
96        a.frac.unwrap() <= MapCarrier::op(a, b).frac.unwrap(),
97        b.frac.unwrap() <= MapCarrier::op(a, b).frac.unwrap(),
98{
99}
100
101#[verifier::reject_recursive_types(K)]
102pub struct GhostMapAuth<K, V> {
103    r: Resource<MapCarrier<K, V>>,
104}
105
106#[verifier::reject_recursive_types(K)]
107pub struct GhostSubmap<K, V> {
108    r: Resource<MapCarrier<K, V>>,
109}
110
111/** An implementation of a resource for owning a subset of keys in a map.
112
113`GhostMapAuth<K, T>` represents authoritative ownership of the entire
114map, and `GhostSubmap<K, T>` represents client ownership of some subset
115of keys in the map.  Updating the authoritative `GhostMapAuth<K, T>`
116requires a `GhostSubmap<K, T>` containing the keys being updated.
117`GhostSubmap<K, T>`s can be combined or split.
118
119### Example
120
121```
122fn example_use() {
123    let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]);
124
125    // Allocate some more keys in the auth map, receiving a new submap.
126    let tracked sub2 = auth.insert(map![4u8 => 4u64, 5u8 => 5u64]);
127    proof { sub.combine(sub2); }
128
129    // Delete some keys in the auth map, by returning corresponding submap.
130    let tracked sub3 = sub.split(set![3u8, 4u8]);
131    proof { auth.delete(sub3); }
132
133    // Split the submap into a multiple submaps.
134    let tracked sub4 = sub.split(set![1u8, 5u8]);
135
136    // In general, we might need to call agree() to establish the fact that
137    // a submap has the same values as the auth map.  Here, Verus doesn't need
138    // agree because it can track where both the auth and submap came from.
139    proof { sub.agree(&auth); }
140    proof { sub4.agree(&auth); }
141
142    assert(sub4[1u8] == auth[1u8]);
143    assert(sub4[5u8] == auth[5u8]);
144    assert(sub[2u8] == auth[2u8]);
145
146    // Update keys using ownership of submaps.
147    proof { sub.update(&mut auth, map![2u8 => 22u64]); }
148    proof { sub4.update(&mut auth, map![1u8 => 11u64]); }
149    assert(auth[1u8] == 11u64);
150    assert(auth[2u8] == 22u64);
151
152    // Not shown in this simple example is the main use case of this resource:
153    // maintaining an invariant between GhostMapAuth<K, V> and some exec-mode
154    // shared state with a map view (e.g., HashMap<K, V>), which states that
155    // the Map<K, V> view of GhostMapAuth<K, V> is the same as the view of the
156    // HashMap<K, V>, and then handing out a GhostSubmap<K, V> to different
157    // clients that might need to operate on different keys in this map.
158}
159```
160*/
161
162impl<K, V> GhostMapAuth<K, V> {
163    #[verifier::type_invariant]
164    spec fn inv(self) -> bool {
165        &&& self.r.value().auth is Some
166        &&& self.r.value().auth.unwrap() is Some
167        &&& self.r.value().frac == Some(Map::<K, V>::empty())
168    }
169
170    pub closed spec fn id(self) -> Loc {
171        self.r.loc()
172    }
173
174    pub closed spec fn view(self) -> Map<K, V> {
175        self.r.value().auth.unwrap().unwrap()
176    }
177
178    pub open spec fn dom(self) -> Set<K> {
179        self@.dom()
180    }
181
182    pub open spec fn spec_index(self, key: K) -> V
183        recommends
184            self.dom().contains(key),
185    {
186        self@[key]
187    }
188
189    pub proof fn dummy() -> (tracked result: GhostMapAuth<K, V>) {
190        let tracked (auth, submap) = GhostMapAuth::<K, V>::new(Map::empty());
191        auth
192    }
193
194    pub proof fn take(tracked &mut self) -> (tracked result: GhostMapAuth<K, V>)
195        ensures
196            result == *old(self),
197    {
198        use_type_invariant(&*self);
199        let tracked mut r = Self::dummy();
200        tracked_swap(self, &mut r);
201        r
202    }
203
204    pub proof fn empty(tracked &self) -> (tracked result: GhostSubmap<K, V>)
205        ensures
206            result.id() == self.id(),
207            result@ == Map::<K, V>::empty(),
208    {
209        use_type_invariant(self);
210        GhostSubmap::<K, V>::empty(self.id())
211    }
212
213    pub proof fn insert(tracked &mut self, m: Map<K, V>) -> (tracked result: GhostSubmap<K, V>)
214        requires
215            old(self)@.dom().disjoint(m.dom()),
216        ensures
217            self.id() == old(self).id(),
218            self@ == old(self)@.union_prefer_right(m),
219            result.id() == self.id(),
220            result@ == m,
221    {
222        broadcast use lemma_submap_of_trans;
223        broadcast use lemma_op_frac_submap_of;
224
225        let tracked mut mself = Self::dummy();
226        tracked_swap(self, &mut mself);
227
228        use_type_invariant(&mself);
229        assert(mself.inv());
230        let tracked mut r = mself.r;
231
232        let rr = MapCarrier {
233            auth: Some(Some(r.value().auth.unwrap().unwrap().union_prefer_right(m))),
234            frac: Some(m),
235        };
236
237        let tracked r_upd = r.update(rr);
238
239        let arr = MapCarrier { auth: r_upd.value().auth, frac: Some(Map::empty()) };
240
241        let frr = MapCarrier { auth: None, frac: r_upd.value().frac };
242
243        assert(r_upd.value() == MapCarrier::op(arr, frr));
244        let tracked (ar, fr) = r_upd.split(arr, frr);
245        self.r = ar;
246        GhostSubmap { r: fr }
247    }
248
249    pub proof fn delete(tracked &mut self, tracked f: GhostSubmap<K, V>)
250        requires
251            f.id() == old(self).id(),
252        ensures
253            self.id() == old(self).id(),
254            self@ == old(self)@.remove_keys(f@.dom()),
255    {
256        broadcast use lemma_submap_of_trans;
257        broadcast use lemma_op_frac_submap_of;
258
259        use_type_invariant(&*self);
260        use_type_invariant(&f);
261
262        let tracked mut mself = Self::dummy();
263        tracked_swap(self, &mut mself);
264        let tracked mut r = mself.r;
265
266        r = r.join(f.r);
267
268        let ra = r.value().auth.unwrap().unwrap();
269        let ra_new = ra.remove_keys(f@.dom());
270
271        let rnew = MapCarrier { auth: Some(Some(ra_new)), frac: Some(Map::empty()) };
272
273        self.r = r.update(rnew);
274    }
275
276    pub proof fn new(m: Map<K, V>) -> (tracked result: (GhostMapAuth<K, V>, GhostSubmap<K, V>))
277        ensures
278            result.0.id() == result.1.id(),
279            result.0@ == m,
280            result.1@ == m,
281    {
282        let tracked rr = Resource::alloc(MapCarrier { auth: Some(Some(m)), frac: Some(m) });
283
284        let arr = MapCarrier { auth: Some(Some(m)), frac: Some(Map::empty()) };
285
286        let frr = MapCarrier { auth: None, frac: Some(m) };
287
288        assert(rr.value() == MapCarrier::op(arr, frr));
289        let tracked (ar, fr) = rr.split(arr, frr);
290        (GhostMapAuth { r: ar }, GhostSubmap { r: fr })
291    }
292}
293
294impl<K, V> GhostSubmap<K, V> {
295    #[verifier::type_invariant]
296    spec fn inv(self) -> bool {
297        &&& self.r.value().auth is None
298        &&& self.r.value().frac is Some
299    }
300
301    pub closed spec fn id(self) -> Loc {
302        self.r.loc()
303    }
304
305    pub closed spec fn view(self) -> Map<K, V> {
306        self.r.value().frac.unwrap()
307    }
308
309    pub open spec fn dom(self) -> Set<K> {
310        self@.dom()
311    }
312
313    pub open spec fn spec_index(self, key: K) -> V
314        recommends
315            self.dom().contains(key),
316    {
317        self@[key]
318    }
319
320    pub proof fn dummy() -> (tracked result: GhostSubmap<K, V>) {
321        let tracked (auth, submap) = GhostMapAuth::<K, V>::new(Map::empty());
322        submap
323    }
324
325    pub proof fn empty(id: int) -> (tracked result: GhostSubmap<K, V>)
326        ensures
327            result.id() == id,
328            result@ == Map::<K, V>::empty(),
329    {
330        let tracked r = Resource::create_unit(id);
331        GhostSubmap { r }
332    }
333
334    pub proof fn take(tracked &mut self) -> (tracked result: GhostSubmap<K, V>)
335        ensures
336            result == *old(self),
337    {
338        use_type_invariant(&*self);
339
340        let tracked mut r = Self::dummy();
341        tracked_swap(self, &mut r);
342        r
343    }
344
345    pub proof fn agree(tracked self: &GhostSubmap<K, V>, tracked auth: &GhostMapAuth<K, V>)
346        requires
347            self.id() == auth.id(),
348        ensures
349            self@ <= auth@,
350    {
351        broadcast use lemma_submap_of_trans;
352
353        use_type_invariant(self);
354        use_type_invariant(auth);
355
356        let tracked joined = self.r.join_shared(&auth.r);
357        joined.validate();
358        assert(self.r.value().frac.unwrap() <= joined.value().frac.unwrap());
359    }
360
361    pub proof fn combine(tracked &mut self, tracked other: GhostSubmap<K, V>)
362        requires
363            old(self).id() == other.id(),
364        ensures
365            self.id() == old(self).id(),
366            self@ == old(self)@.union_prefer_right(other@),
367            old(self)@.dom().disjoint(other@.dom()),
368    {
369        use_type_invariant(&*self);
370        use_type_invariant(&other);
371
372        let tracked mut r = Resource::alloc(MapCarrier::unit());
373        tracked_swap(&mut self.r, &mut r);
374        r.validate_2(&other.r);
375        self.r = r.join(other.r);
376    }
377
378    pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubmap<K, V>)
379        requires
380            old(self).id() == other.id(),
381        ensures
382            self.id() == old(self).id(),
383            self@ == old(self)@,
384            self@.dom().disjoint(other@.dom()),
385    {
386        use_type_invariant(&*self);
387        use_type_invariant(other);
388        self.r.validate_2(&other.r);
389    }
390
391    pub proof fn split(tracked &mut self, s: Set<K>) -> (tracked result: GhostSubmap<K, V>)
392        requires
393            s <= old(self)@.dom(),
394        ensures
395            self.id() == old(self).id(),
396            result.id() == self.id(),
397            old(self)@ == self@.union_prefer_right(result@),
398            result@.dom() =~= s,
399            self@.dom() =~= old(self)@.dom() - s,
400    {
401        use_type_invariant(&*self);
402
403        let tracked mut r = Resource::alloc(MapCarrier::<K, V>::unit());
404        tracked_swap(&mut self.r, &mut r);
405
406        let rr1 = MapCarrier { auth: None, frac: Some(r.value().frac.unwrap().remove_keys(s)) };
407
408        let rr2 = MapCarrier { auth: None, frac: Some(r.value().frac.unwrap().restrict(s)) };
409
410        assert(r.value().frac == MapCarrier::op(rr1, rr2).frac);
411        let tracked (r1, r2) = r.split(rr1, rr2);
412        self.r = r1;
413        GhostSubmap { r: r2 }
414    }
415
416    pub proof fn update(tracked &mut self, tracked auth: &mut GhostMapAuth<K, V>, m: Map<K, V>)
417        requires
418            m.dom() <= old(self)@.dom(),
419            old(self).id() == old(auth).id(),
420        ensures
421            self.id() == old(self).id(),
422            auth.id() == old(auth).id(),
423            self@ == old(self)@.union_prefer_right(m),
424            auth@ == old(auth)@.union_prefer_right(m),
425    {
426        broadcast use lemma_submap_of_trans;
427        broadcast use lemma_op_frac_submap_of;
428
429        use_type_invariant(&*self);
430        use_type_invariant(&*auth);
431
432        let tracked mut mself = Self::dummy();
433        tracked_swap(self, &mut mself);
434        let tracked mut fr = mself.r;
435
436        let tracked mut mauth = GhostMapAuth::<K, V>::dummy();
437        tracked_swap(auth, &mut mauth);
438        let tracked mut ar = mauth.r;
439
440        fr.validate_2(&ar);
441        let tracked mut r = fr.join(ar);
442
443        assert(r.value().frac == fr.value().frac);
444
445        let rr = MapCarrier {
446            auth: Some(Some(r.value().auth.unwrap().unwrap().union_prefer_right(m))),
447            frac: Some(r.value().frac.unwrap().union_prefer_right(m)),
448        };
449
450        let tracked r_upd = r.update(rr);
451
452        let arr = MapCarrier { auth: r_upd.value().auth, frac: Some(Map::empty()) };
453
454        let frr = MapCarrier { auth: None, frac: r_upd.value().frac };
455
456        assert(r_upd.value().frac == MapCarrier::op(arr, frr).frac);
457        let tracked (ar, fr) = r_upd.split(arr, frr);
458        auth.r = ar;
459        self.r = fr;
460    }
461}
462
463} // verus!
vstd/tokens/map.rs

vstd/tokens/
map.rs
