vstd/resource/impls/
imap.rs

1//! IMaps that support ownership of keys
2//!
3//! - [`GhostIMapAuth<K, V>`] represents authoritative ownership of the entire map;
4//! - [`GhostISubmap<K, V>`] represents client ownership of a submap;
5//! - [`GhostPersistentISubmap<K, V>`] represents duplicable client knowledge of a submap which will never change;
6//! - [`GhostIPointsTo<K, V>`] represents client ownership of a single key-value pair.
7//! - [`GhostPersistentIPointsTo<K, V>`] represents duplicable client knowledge of a single key-value pair which will never change.
8//!
9//! Updating the authoritative `GhostIMapAuth<K, V>` requires a `GhostISubmap<K, V>` containing the keys being updated.
10//!
11//! `GhostISubmap<K, V>`s can be combined or split.
12//! Whenever a `GhostISubmap<K, V>` can be used, we can instead use a `GhostIPointsTo<K, V>` (but not vice-versa).
13//!
14//! `GhostPersistentISubmap<K, V>`s can be combined or split.
15//! Whenever a `GhostPersistentISubmap<K, V>` can be used, we can instead use a `GhostPersistentIPointsTo<K, V>` (but not vice-versa).
16//!
17//! ### Example
18//!
19//! ```
20//! fn example_use() {
21//!     let tracked (mut auth, mut sub) = GhostIMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]);
22//!
23//!     // Allocate some more keys in the auth map, receiving a new submap.
24//!     let tracked sub2 = auth.insert_map(map![4u8 => 4u64, 5u8 => 5u64]);
25//!     proof { sub.combine(sub2); }
26//!
27//!     // Allocate a single key in the auth map, receiving a points to
28//!     let tracked pt1 = auth.insert(6u8, 6u64);
29//!     proof { sub.combine_points_to(pt1); }
30//!
31//!     // Delete some keys in the auth map, by returning corresponding submap.
32//!     let tracked sub3 = sub.split(set![3u8, 4u8]);
33//!     proof { auth.delete(sub3); }
34//!
35//!     // Split the submap into a points to and a submap
36//!     let tracked pt2 = sub.split_points_to(1u8);
37//!     let tracked sub4 = sub.split(set![5u8, 6u8]);
38//!
39//!     // In general, we might need to call agree() to establish the fact that
40//!     // a points-to/submap has the same values as the auth map.  Here, Verus
41//!     // doesn't need agree because it can track where both the auth, points-to
42//!     // and submap came from.
43//!     proof { sub.agree(&auth); }
44//!     proof { pt2.agree(&auth); }
45//!     proof { sub4.agree(&auth); }
46//!
47//!     assert(pt2.key() == 1u8);
48//!     assert(pt2.value() == auth[1u8]);
49//!     assert(sub4[5u8] == auth[5u8]);
50//!     assert(sub4[6u8] == auth[6u8]);
51//!     assert(sub[2u8] == auth[2u8]);
52//!
53//!     // Update keys using ownership of submaps.
54//!     proof { sub.update(&mut auth, map![2u8 => 22u64]); }
55//!     proof { pt2.update(&mut auth, 11u64); }
56//!     proof { sub4.update(&mut auth, map![5u8 => 55u64, 6u8 => 66u8]); }
57//!     assert(auth[1u8] == 11u64);
58//!     assert(auth[2u8] == 22u64);
59//!     assert(auth[5u8] == 55u64);
60//!     assert(auth[6u8] == 66u64);
61//!
62//!     // Persist and duplicate the submap
63//!     let mut psub1 = sub.persist();
64//!     assert(psub1[2u8] == 22u64);
65//!     let psub2 = psub1.duplicate();
66//!     assert(psub2[2u8] == 22u64);
67//!
68//!     // Not shown in this simple example is the main use case of this resource:
69//!     // maintaining an invariant between GhostIMapAuth<K, V> and some exec-mode
70//!     // shared state with a map view (e.g., HashIMap<K, V>), which states that
71//!     // the IMap<K, V> view of GhostIMapAuth<K, V> is the same as the view of the
72//!     // HashIMap<K, V>, and then handing out a GhostISubmap<K, V> to different
73//!     // clients that might need to operate on different keys in this map.
74//! }
75//! ```
76use super::super::super::imap::*;
77use super::super::super::imap_lib::*;
78use super::super::super::iset_lib::*;
79use super::super::super::modes::*;
80use super::super::super::prelude::*;
81use super::super::Loc;
82use super::super::algebra::ResourceAlgebra;
83#[cfg(verus_keep_ghost)]
84use super::super::incorporate;
85use super::super::pcm::PCM;
86use super::super::pcm::Resource;
87#[cfg(verus_keep_ghost)]
88use super::super::split_mut;
89
90verus! {
91
92broadcast use {
93    super::super::super::group_vstd_default,
94    super::super::super::imap::group_imap_lemmas,
95};
96
97#[verifier::reject_recursive_types(K)]
98#[verifier::ext_equal]
99enum AuthCarrier<K, V> {
100    Auth(IMap<K, V>),
101    Frac,
102    Invalid,
103}
104
105#[verifier::reject_recursive_types(K)]
106#[verifier::ext_equal]
107enum FracCarrier<K, V> {
108    Frac { owning: IMap<K, V>, dup: IMap<K, V> },
109    Invalid,
110}
111
112impl<K, V> AuthCarrier<K, V> {
113    spec fn valid(self) -> bool {
114        !(self is Invalid)
115    }
116
117    spec fn map(self) -> IMap<K, V>
118        recommends
119            self.valid(),
120    {
121        match self {
122            AuthCarrier::Auth(m) => m,
123            AuthCarrier::Frac => IMap::empty(),
124            AuthCarrier::Invalid => IMap::empty(),
125        }
126    }
127}
128
129impl<K, V> FracCarrier<K, V> {
130    spec fn valid(self) -> bool {
131        match self {
132            FracCarrier::Invalid => false,
133            FracCarrier::Frac { owning, dup } => owning.dom().disjoint(dup.dom()),
134        }
135    }
136
137    spec fn owning_map(self) -> IMap<K, V> {
138        match self {
139            FracCarrier::Frac { owning, .. } => owning,
140            FracCarrier::Invalid => IMap::empty(),
141        }
142    }
143
144    spec fn dup_map(self) -> IMap<K, V> {
145        match self {
146            FracCarrier::Frac { dup, .. } => dup,
147            FracCarrier::Invalid => IMap::empty(),
148        }
149    }
150}
151
152#[verifier::reject_recursive_types(K)]
153#[verifier::ext_equal]
154// This struct represents the underlying resource algebra for GhostIMaps
155tracked struct IMapCarrier<K, V> {
156    auth: AuthCarrier<K, V>,
157    frac: FracCarrier<K, V>,
158}
159
160impl<K, V> ResourceAlgebra for IMapCarrier<K, V> {
161    closed spec fn valid(self) -> bool {
162        match (self.auth, self.frac) {
163            (AuthCarrier::Invalid, _) => false,
164            (_, FracCarrier::Invalid) => false,
165            (AuthCarrier::Auth(auth), FracCarrier::Frac { owning, dup }) => {
166                &&& owning <= auth
167                &&& dup <= auth
168                &&& owning.dom().disjoint(dup.dom())
169            },
170            (AuthCarrier::Frac, FracCarrier::Frac { owning, dup }) => owning.dom().disjoint(
171                dup.dom(),
172            ),
173        }
174    }
175
176    closed spec fn op(a: Self, b: Self) -> Self {
177        let auth = match (a.auth, b.auth) {
178            // Invalid carriers absorb
179            (AuthCarrier::Invalid, _) => AuthCarrier::Invalid,
180            (_, AuthCarrier::Invalid) => AuthCarrier::Invalid,
181            // There can't be two auths
182            (AuthCarrier::Auth(_), AuthCarrier::Auth(_)) => AuthCarrier::Invalid,
183            // Fracs remain the same
184            (AuthCarrier::Frac, AuthCarrier::Frac) => AuthCarrier::Frac,
185            // Whoever is the auth has precedence
186            (AuthCarrier::Auth(_), _) => a.auth,
187            (_, AuthCarrier::Auth(_)) => b.auth,
188        };
189
190        let frac = match (a.frac, b.frac) {
191            // Invalid fracs remain invalid
192            (FracCarrier::Invalid, _) => FracCarrier::Invalid,
193            (_, FracCarrier::Invalid) => FracCarrier::Invalid,
194            // We can mix two owning fracs iff they are disjoint -- we get the union
195            // There is a tricky element here:
196            //  - one of the fracs may be invalid due to their maps overlapping
197            //  - there is no real way to express this in the typesystem
198            //  - we need to allow that through (because it does not equal Invalid)
199            (
200                FracCarrier::Frac { owning: a_owning, dup: a_dup },
201                FracCarrier::Frac { owning: b_owning, dup: b_dup },
202            ) => {
203                let non_overlapping = {
204                    &&& a_owning.dom().disjoint(b_dup.dom())
205                    &&& b_owning.dom().disjoint(a_dup.dom())
206                    &&& a_owning.dom().disjoint(b_owning.dom())
207                };
208                let aggreement = a_dup.agrees(b_dup);
209                if non_overlapping && aggreement {
210                    FracCarrier::Frac {
211                        owning: a_owning.union_prefer_right(b_owning),
212                        dup: a_dup.union_prefer_right(b_dup),
213                    }
214                } else {
215                    FracCarrier::Invalid
216                }
217            },
218        };
219
220        IMapCarrier { auth, frac }
221    }
222
223    proof fn valid_op(a: Self, b: Self) {
224        broadcast use lemma_submap_of_trans;
225
226        let ab = IMapCarrier::op(a, b);
227        lemma_submap_of_op_frac(a, b);
228        // derive contradiction that the items are disjoint
229        if !a.frac.owning_map().dom().disjoint(a.frac.dup_map().dom()) {
230            // The intersection is not empty
231            lemma_iset_disjoint_iff_empty_intersection(
232                a.frac.owning_map().dom(),
233                a.frac.dup_map().dom(),
234            );
235            let a_k = choose|k: K|
236                a.frac.owning_map().dom().intersect(a.frac.dup_map().dom()).contains(k);
237            assert(ab.frac.owning_map().dom().intersect(ab.frac.dup_map().dom()).contains(a_k));  // CONTRADICTION
238        };
239    }
240
241    proof fn commutative(a: Self, b: Self) {
242        let ab = Self::op(a, b);
243        let ba = Self::op(b, a);
244        assert(ab == ba);
245    }
246
247    proof fn associative(a: Self, b: Self, c: Self) {
248        let bc = Self::op(b, c);
249        let ab = Self::op(a, b);
250        let a_bc = Self::op(a, bc);
251        let ab_c = Self::op(ab, c);
252        assert(a_bc == ab_c);
253    }
254}
255
256impl<K, V> PCM for IMapCarrier<K, V> {
257    closed spec fn unit() -> Self {
258        IMapCarrier {
259            auth: AuthCarrier::Frac,
260            frac: FracCarrier::Frac { owning: IMap::empty(), dup: IMap::empty() },
261        }
262    }
263
264    proof fn op_unit(self) {
265        let x = Self::op(self, Self::unit());
266        assert(self == x);
267    }
268
269    proof fn unit_valid() {
270    }
271}
272
273proof fn lemma_submap_of_op_frac<K, V>(a: IMapCarrier<K, V>, b: IMapCarrier<K, V>)
274    requires
275        IMapCarrier::op(a, b).valid(),
276    ensures
277        a.frac.owning_map() <= IMapCarrier::op(a, b).frac.owning_map(),
278        a.frac.dup_map() <= IMapCarrier::op(a, b).frac.dup_map(),
279        b.frac.owning_map() <= IMapCarrier::op(a, b).frac.owning_map(),
280        b.frac.dup_map() <= IMapCarrier::op(a, b).frac.dup_map(),
281{
282    let ab = IMapCarrier::op(a, b);
283    assert(ab.frac.owning_map() == a.frac.owning_map().union_prefer_right(b.frac.owning_map()));
284    assert(ab.frac.dup_map() == a.frac.dup_map().union_prefer_right(b.frac.dup_map()));
285    assert(a.frac.owning_map().dom().disjoint(b.frac.owning_map().dom()));
286}
287
288broadcast proof fn lemma_submap_of_op<K, V>(a: IMapCarrier<K, V>, b: IMapCarrier<K, V>)
289    requires
290        #[trigger] IMapCarrier::op(a, b).valid(),
291    ensures
292        a.frac.owning_map() <= IMapCarrier::op(a, b).frac.owning_map(),
293        a.frac.dup_map() <= IMapCarrier::op(a, b).frac.dup_map(),
294        a.auth.map() <= IMapCarrier::op(a, b).auth.map(),
295        b.frac.owning_map() <= IMapCarrier::op(a, b).frac.owning_map(),
296        b.frac.dup_map() <= IMapCarrier::op(a, b).frac.dup_map(),
297        b.auth.map() <= IMapCarrier::op(a, b).auth.map(),
298        a.valid(),
299        b.valid(),
300{
301    lemma_submap_of_op_frac(a, b);
302    IMapCarrier::valid_op(a, b);
303    IMapCarrier::commutative(a, b);
304    IMapCarrier::valid_op(b, a);
305    let ab = IMapCarrier::op(a, b);
306    assert(ab.auth.map() == a.auth.map().union_prefer_right(b.auth.map()));
307}
308
309/// A resource that has the authoritative ownership on the entire map
310#[verifier::reject_recursive_types(K)]
311pub tracked struct GhostIMapAuth<K, V> {
312    r: Resource<IMapCarrier<K, V>>,
313}
314
315/// A resource that asserts client ownership of a submap.
316///
317/// The existence of a [`GhostISubmap`] implies that:
318///  - Those keys will remain in the map (unless the onwer of the [`GhostISubmap`] deletes it using [`GhostIMapAuth::delete`]);
319///  - Those keys will remain pointing to the same values (unless the onwer of the [`GhostISubmap`] updates them using [`GhostISubmap::update`])
320///  - All other [`GhostISubmap`]/[`GhostIPointsTo`]/[`GhostPersistentISubmap`]/[`GhostPersistentIPointsTo`] are disjoint subsets of the domain
321#[verifier::reject_recursive_types(K)]
322pub tracked struct GhostISubmap<K, V> {
323    r: Resource<IMapCarrier<K, V>>,
324}
325
326/// A resource representing duplicable client knowledge of a persistent submap.
327///
328/// The existence of a [`GhostPersistentISubmap`] implies that:
329///  - Those keys will remain in the map, pointing to the same values, forever;
330///  - All other [`GhostISubmap`]/[`GhostIPointsTo`] are disjoint subsets of the domain
331#[verifier::reject_recursive_types(K)]
332pub tracked struct GhostPersistentISubmap<K, V> {
333    r: Resource<IMapCarrier<K, V>>,
334}
335
336/// A resource that asserts client ownership over a single key in the map.
337///
338/// The existence of a [`GhostIPointsTo`] implies that:
339///  - Those key will remain in the map (unless the onwer of the [`GhostIPointsTo`] deletes it using [`GhostIMapAuth::delete_points_to`]);
340///  - Those key will remain pointing to the same value (unless the onwer of the [`GhostIPointsTo`] updates them using [`GhostIPointsTo::update`])
341///  - All other [`GhostISubmap`]/[`GhostIPointsTo`]/[`GhostPersistentISubmap`]/[`GhostPersistentIPointsTo`] are disjoint subsets of the domain
342#[verifier::reject_recursive_types(K)]
343pub tracked struct GhostIPointsTo<K, V> {
344    submap: GhostISubmap<K, V>,
345}
346
347/// A resource representing duplicable client knowledge of a single key in the map.
348///
349/// The existence of a [`GhostPersistentIPointsTo`] implies that:
350///  - The key-value pair will remain in the map, forever;
351///  - All other [`GhostISubmap`]/[`GhostIPointsTo`] are disjoint subsets of the domain
352#[verifier::reject_recursive_types(K)]
353pub tracked struct GhostPersistentIPointsTo<K, V> {
354    submap: GhostPersistentISubmap<K, V>,
355}
356
357impl<K, V> GhostIMapAuth<K, V> {
358    #[verifier::type_invariant]
359    spec fn inv(self) -> bool {
360        &&& self.r.value().auth is Auth
361        &&& self.r.value().frac == FracCarrier::Frac {
362            owning: IMap::<K, V>::empty(),
363            dup: IMap::<K, V>::empty(),
364        }
365    }
366
367    /// Resource location
368    pub closed spec fn id(self) -> Loc {
369        self.r.loc()
370    }
371
372    /// Logically underlying [`IMap`]
373    pub closed spec fn view(self) -> IMap<K, V> {
374        self.r.value().auth.map()
375    }
376
377    /// Domain of the [`GhostIMapAuth`]
378    pub open spec fn dom(self) -> ISet<K> {
379        self@.dom()
380    }
381
382    /// Indexing operation `auth[key]`
383    pub open spec fn spec_index(self, key: K) -> V
384        recommends
385            self.dom().contains(key),
386    {
387        self@[key]
388    }
389
390    /// Instantiate a dummy [`GhostIMapAuth`]
391    pub proof fn dummy() -> (tracked result: GhostIMapAuth<K, V>) {
392        let tracked (auth, submap) = GhostIMapAuth::<K, V>::new(IMap::empty());
393        auth
394    }
395
396    /// Extract the [`GhostIMapAuth`] from a mutable reference
397    pub proof fn take(tracked &mut self) -> (tracked result: GhostIMapAuth<K, V>)
398        ensures
399            result == *old(self),
400    {
401        use_type_invariant(&*self);
402        let tracked mut r = Self::dummy();
403        tracked_swap(self, &mut r);
404        r
405    }
406
407    /// Create an empty [`GhostISubmap`]
408    pub proof fn empty(tracked &self) -> (tracked result: GhostISubmap<K, V>)
409        ensures
410            result.id() == self.id(),
411            result@ == IMap::<K, V>::empty(),
412    {
413        use_type_invariant(self);
414        let tracked r = Resource::<IMapCarrier<_, _>>::create_unit(self.r.loc());
415        GhostISubmap { r }
416    }
417
418    /// Insert an [`IMap`] of values, receiving the [`GhostISubmap`] that asserts ownership over the key
419    /// domain inserted.
420    ///
421    /// ```
422    /// proof fn insert_map_example(tracked mut m: GhostIMapAuth<int, int>) -> (tracked r: GhostISubmap<int, int>)
423    ///     requires
424    ///         !m.dom().contains(1int),
425    ///         !m.dom().contains(2int),
426    /// {
427    ///     let tracked submap = m.insert_map(map![1int => 1int, 2int => 4int]);
428    ///     // do something with the submap
429    ///     submap
430    /// }
431    /// ```
432    pub proof fn insert_map(tracked &mut self, m: IMap<K, V>) -> (tracked result: GhostISubmap<
433        K,
434        V,
435    >)
436        requires
437            old(self)@.dom().disjoint(m.dom()),
438        ensures
439            final(self).id() == old(self).id(),
440            final(self)@ == old(self)@.union_prefer_right(m),
441            result.id() == final(self).id(),
442            result@ == m,
443    {
444        broadcast use lemma_submap_of_trans;
445        broadcast use lemma_submap_of_op;
446
447        let tracked mut mself = Self::dummy();
448        tracked_swap(self, &mut mself);
449
450        use_type_invariant(&mself);
451        assert(mself.inv());
452        let tracked mut self_r = mself.r;
453
454        let full_carrier = IMapCarrier {
455            auth: AuthCarrier::Auth(self_r.value().auth.map().union_prefer_right(m)),
456            frac: FracCarrier::Frac { owning: m, dup: IMap::empty() },
457        };
458
459        assert(full_carrier.valid());
460        let tracked updated_r = self_r.update(full_carrier);
461
462        let auth_carrier = IMapCarrier {
463            auth: updated_r.value().auth,
464            frac: FracCarrier::Frac { owning: IMap::empty(), dup: IMap::empty() },
465        };
466        let frac_carrier = IMapCarrier { auth: AuthCarrier::Frac, frac: updated_r.value().frac };
467
468        assert(updated_r.value() == IMapCarrier::op(auth_carrier, frac_carrier));
469        let tracked (auth_r, frac_r) = updated_r.split(auth_carrier, frac_carrier);
470        self.r = auth_r;
471        GhostISubmap { r: frac_r }
472    }
473
474    /// Insert a key-value pair, receiving the [`GhostIPointsTo`] that asserts ownerships over the key.
475    ///
476    /// ```
477    /// proof fn insert_example(tracked mut m: GhostIMapAuth<int, int>) -> (tracked r: GhostIPointsTo<int, int>)
478    ///     requires
479    ///         !m.dom().contains(1int),
480    /// {
481    ///     let tracked points_to = m.insert(1, 1);
482    ///     // do something with the points_to
483    ///     points_to
484    /// }
485    /// ```
486    pub proof fn insert(tracked &mut self, k: K, v: V) -> (tracked result: GhostIPointsTo<K, V>)
487        requires
488            !old(self)@.contains_key(k),
489        ensures
490            final(self).id() == old(self).id(),
491            final(self)@ == old(self)@.insert(k, v),
492            result.id() == final(self).id(),
493            result@ == (k, v),
494    {
495        let tracked submap = self.insert_map(imap![k => v]);
496        GhostIPointsTo { submap }
497    }
498
499    /// Delete a set of keys
500    /// ```
501    /// proof fn delete(tracked mut auth: GhostIMapAuth<int, int>)
502    ///     requires
503    ///         auth.dom().contains(1int),
504    ///         auth.dom().contains(2int),
505    ///     ensures
506    ///         old(auth)@ == auth@
507    /// {
508    ///     let tracked submap = auth.insert_map(map![1int => 1int, 2int => 4int]);
509    ///     // do something with the submap
510    ///     auth.delete(submap)
511    /// }
512    /// ```
513    pub proof fn delete(tracked &mut self, tracked submap: GhostISubmap<K, V>)
514        requires
515            submap.id() == old(self).id(),
516        ensures
517            final(self).id() == old(self).id(),
518            final(self)@ == old(self)@.remove_keys(submap@.dom()),
519    {
520        broadcast use lemma_submap_of_trans;
521        broadcast use lemma_submap_of_op;
522
523        use_type_invariant(&*self);
524        use_type_invariant(&submap);
525
526        let tracked mut mself = Self::dummy();
527        tracked_swap(self, &mut mself);
528        let tracked mut self_r = mself.r;
529
530        // join the resource with the original carrier
531        self_r = self_r.join(submap.r);
532
533        // remove keys from the map
534        let auth_map = self_r.value().auth.map();
535        let new_auth_map = auth_map.remove_keys(submap@.dom());
536
537        let new_r = IMapCarrier {
538            auth: AuthCarrier::Auth(new_auth_map),
539            frac: FracCarrier::Frac { owning: IMap::empty(), dup: IMap::empty() },
540        };
541
542        // update the resource
543        self.r = self_r.update(new_r);
544    }
545
546    /// Delete a single key from the map
547    /// ```
548    /// proof fn delete_key(tracked mut auth: GhostIMapAuth<int, int>)
549    ///     requires
550    ///         auth.dom().contains(1int),
551    ///     ensures
552    ///         old(auth)@ == auth@
553    /// {
554    ///     let tracked points_to = auth.insert(1, 1);
555    ///     // do something with the submap
556    ///     auth.delete_points_to(points_to)
557    /// }
558    /// ```
559    pub proof fn delete_points_to(tracked &mut self, tracked p: GhostIPointsTo<K, V>)
560        requires
561            p.id() == old(self).id(),
562        ensures
563            final(self).id() == old(self).id(),
564            final(self)@ == old(self)@.remove(p.key()),
565    {
566        use_type_invariant(&p);
567        p.lemma_map_view();
568        self.delete(p.submap);
569    }
570
571    /// Create a new [`GhostIMapAuth`] from an [`IMap`].
572    /// Gives the other half of ownership in the form of a [`GhostISubmap`].
573    ///
574    /// ```
575    /// fn example() {
576    ///     let m = map![1int => 1int, 2int => 4int, 3int => 9int];
577    ///     let tracked (auth, sub) = GhostIMapAuth::new(m);
578    ///     assert(auth@ == m);
579    ///     assert(sub.dom() == m.dom());
580    /// }
581    /// ```
582    pub proof fn new(m: IMap<K, V>) -> (tracked result: (GhostIMapAuth<K, V>, GhostISubmap<K, V>))
583        ensures
584            result.0.id() == result.1.id(),
585            result.0@ == m,
586            result.1@ == m,
587    {
588        let tracked full_r = Resource::alloc(
589            IMapCarrier {
590                auth: AuthCarrier::Auth(m),
591                frac: FracCarrier::Frac { owning: m, dup: IMap::empty() },
592            },
593        );
594
595        let auth_carrier = IMapCarrier {
596            auth: AuthCarrier::Auth(m),
597            frac: FracCarrier::Frac { owning: IMap::empty(), dup: IMap::empty() },
598        };
599
600        let frac_carrier = IMapCarrier {
601            auth: AuthCarrier::Frac,
602            frac: FracCarrier::Frac { owning: m, dup: IMap::empty() },
603        };
604
605        assert(full_r.value() == IMapCarrier::op(auth_carrier, frac_carrier));
606        let tracked (auth_r, frac_r) = full_r.split(auth_carrier, frac_carrier);
607        (GhostIMapAuth { r: auth_r }, GhostISubmap { r: frac_r })
608    }
609}
610
611impl<K, V> GhostISubmap<K, V> {
612    #[verifier::type_invariant]
613    spec fn inv(self) -> bool {
614        &&& self.r.value().auth is Frac
615        &&& self.r.value().frac is Frac
616        &&& self.r.value().frac.dup_map().is_empty()
617    }
618
619    /// Checks whether the [`GhostISubmap`] refers to a single key (and thus can be converted to a
620    /// [`GhostIPointsTo`]).
621    pub open spec fn is_points_to(self) -> bool {
622        &&& self@.len() == 1
623        &&& self.dom().finite()
624        &&& !self@.is_empty()
625    }
626
627    /// Resource location
628    pub closed spec fn id(self) -> Loc {
629        self.r.loc()
630    }
631
632    /// Logically underlying [`IMap`]
633    pub closed spec fn view(self) -> IMap<K, V> {
634        self.r.value().frac.owning_map()
635    }
636
637    /// Domain of the [`GhostISubmap`]
638    pub open spec fn dom(self) -> ISet<K> {
639        self@.dom()
640    }
641
642    /// Indexing operation `submap[key]`
643    pub open spec fn spec_index(self, key: K) -> V
644        recommends
645            self.dom().contains(key),
646    {
647        self@[key]
648    }
649
650    /// Instantiate a dummy [`GhostISubmap`]
651    pub proof fn dummy() -> (tracked result: GhostISubmap<K, V>) {
652        let tracked (auth, submap) = GhostIMapAuth::<K, V>::new(IMap::empty());
653        submap
654    }
655
656    /// Create an empty [`GhostISubmap`]
657    pub proof fn empty(tracked &self) -> (tracked result: GhostISubmap<K, V>)
658        ensures
659            result.id() == self.id(),
660            result@ == IMap::<K, V>::empty(),
661    {
662        use_type_invariant(self);
663        let tracked r = Resource::<IMapCarrier<_, _>>::create_unit(self.r.loc());
664        GhostISubmap { r }
665    }
666
667    /// Extract the [`GhostISubmap`] from a mutable reference, leaving behind an empty map.
668    pub proof fn take(tracked &mut self) -> (tracked result: GhostISubmap<K, V>)
669        ensures
670            old(self).id() == final(self).id(),
671            final(self)@.is_empty(),
672            result == *old(self),
673            result.id() == final(self).id(),
674    {
675        use_type_invariant(&*self);
676
677        let tracked mut r = self.empty();
678        tracked_swap(self, &mut r);
679        r
680    }
681
682    /// Agreement between a [`GhostISubmap`] and a corresponding [`GhostIMapAuth`]
683    ///
684    /// Verus might not have full context of the [`GhostIMapAuth`] and a corresponding [`GhostISubmap`].
685    /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
686    /// can assert that the [`GhostISubmap`] is a submap of the [`GhostIMapAuth`].
687    /// ```
688    /// proof fn test(tracked &auth: GhostIMapAuth<int, int>, tracked &sub: GhostISubmap<int, int>)
689    ///     requires
690    ///         auth.id() == sub.id(),
691    ///         sub.dom().contains(1int),
692    ///         sub[1int] == 1int,
693    ///     ensures
694    ///         auth[1int] == 1int
695    /// {
696    ///     sub.agree(auth);
697    ///     assert(sub@ <= auth@);
698    ///     assert(auth[1int] == 1int);
699    /// }
700    /// ```
701    pub proof fn agree(tracked self: &GhostISubmap<K, V>, tracked auth: &GhostIMapAuth<K, V>)
702        requires
703            self.id() == auth.id(),
704        ensures
705            self@ <= auth@,
706    {
707        broadcast use lemma_submap_of_trans;
708
709        use_type_invariant(self);
710        use_type_invariant(auth);
711
712        let tracked joined = self.r.join_shared(&auth.r);
713        joined.validate();
714        assert(self.r.value().frac.owning_map() <= joined.value().frac.owning_map());
715    }
716
717    /// Combining two [`GhostISubmap`]s is possible.
718    /// We consume the input [`GhostISubmap`] and merge it into the first.
719    /// We also learn that they were disjoint.
720    pub proof fn combine(tracked &mut self, tracked other: GhostISubmap<K, V>)
721        requires
722            old(self).id() == other.id(),
723        ensures
724            final(self).id() == old(self).id(),
725            final(self)@ == old(self)@.union_prefer_right(other@),
726            old(self)@.dom().disjoint(other@.dom()),
727    {
728        use_type_invariant(&*self);
729        use_type_invariant(&other);
730
731        self.r.validate_2(&other.r);
732        incorporate(&mut self.r, other.r);
733    }
734
735    /// Combining a [`GhostIPointsTo`] into [`GhostISubmap`] is possible, in a similar way to the way to combine
736    /// [`GhostISubmap`]s.
737    pub proof fn combine_points_to(tracked &mut self, tracked other: GhostIPointsTo<K, V>)
738        requires
739            old(self).id() == other.id(),
740        ensures
741            final(self).id() == old(self).id(),
742            final(self)@ == old(self)@.insert(other.key(), other.value()),
743            !old(self)@.contains_key(other.key()),
744    {
745        use_type_invariant(&*self);
746        use_type_invariant(&other);
747
748        other.lemma_map_view();
749        self.combine(other.submap);
750    }
751
752    /// When we have two [`GhostISubmap`]s we can prove that they have disjoint domains.
753    pub proof fn disjoint(tracked &mut self, tracked other: &GhostISubmap<K, V>)
754        requires
755            old(self).id() == other.id(),
756        ensures
757            final(self).id() == old(self).id(),
758            final(self)@ == old(self)@,
759            final(self)@.dom().disjoint(other@.dom()),
760    {
761        use_type_invariant(&*self);
762        use_type_invariant(other);
763        self.r.validate_2(&other.r);
764    }
765
766    /// When we have a [`GhostISubmap`] and a [`GhostPersistentISubmap`] we can prove that they are in disjoint
767    /// domains.
768    pub proof fn disjoint_persistent(
769        tracked &mut self,
770        tracked other: &GhostPersistentISubmap<K, V>,
771    )
772        requires
773            old(self).id() == other.id(),
774        ensures
775            final(self).id() == old(self).id(),
776            final(self)@ == old(self)@,
777            final(self)@.dom().disjoint(other@.dom()),
778    {
779        use_type_invariant(&*self);
780        use_type_invariant(other);
781        self.r.validate_2(&other.r);
782    }
783
784    /// When we have a [`GhostISubmap`] and a [`GhostIPointsTo`] we can prove that they are in disjoint
785    /// domains.
786    pub proof fn disjoint_points_to(tracked &mut self, tracked other: &GhostIPointsTo<K, V>)
787        requires
788            old(self).id() == other.id(),
789        ensures
790            final(self).id() == old(self).id(),
791            final(self)@ == old(self)@,
792            !final(self)@.contains_key(other.key()),
793    {
794        use_type_invariant(&*self);
795        use_type_invariant(other);
796        self.disjoint(&other.submap);
797    }
798
799    /// When we have a [`GhostISubmap`] and a [`GhostPersistentIPointsTo`] we can prove that they are in disjoint
800    /// domains.
801    pub proof fn disjoint_persistent_points_to(
802        tracked &mut self,
803        tracked other: &GhostPersistentIPointsTo<K, V>,
804    )
805        requires
806            old(self).id() == other.id(),
807        ensures
808            final(self).id() == old(self).id(),
809            final(self)@ == old(self)@,
810            !final(self)@.contains_key(other.key()),
811    {
812        use_type_invariant(&*self);
813        use_type_invariant(other);
814        self.disjoint_persistent(&other.submap);
815    }
816
817    /// We can split a [`GhostISubmap`] based on a set of keys in its domain.
818    pub proof fn split(tracked &mut self, s: ISet<K>) -> (tracked result: GhostISubmap<K, V>)
819        requires
820            s <= old(self)@.dom(),
821        ensures
822            final(self).id() == old(self).id(),
823            result.id() == final(self).id(),
824            old(self)@ == final(self)@.union_prefer_right(result@),
825            result@.dom() =~= s,
826            final(self)@.dom() =~= old(self)@.dom() - s,
827    {
828        use_type_invariant(&*self);
829
830        let self_carrier = IMapCarrier {
831            auth: AuthCarrier::Frac,
832            frac: FracCarrier::Frac {
833                owning: self.r.value().frac.owning_map().remove_keys(s),
834                dup: self.r.value().frac.dup_map(),
835            },
836        };
837
838        let res_carrier = IMapCarrier {
839            auth: AuthCarrier::Frac,
840            frac: FracCarrier::Frac {
841                owning: self.r.value().frac.owning_map().restrict(s),
842                dup: self.r.value().frac.dup_map(),
843            },
844        };
845
846        assert(self.r.value().frac == IMapCarrier::op(self_carrier, res_carrier).frac);
847        let tracked r = split_mut(&mut self.r, self_carrier, res_carrier);
848        GhostISubmap { r }
849    }
850
851    pub proof fn split_with_olddom(
852        tracked &mut self,
853        s: ISet<K>,
854        olddom: ISet<K>,
855    ) -> (tracked result: GhostISubmap<K, V>)
856        requires
857            olddom == old(self)@.dom(),
858            s <= olddom,
859        ensures
860            final(self).id() == old(self).id(),
861            result.id() == final(self).id(),
862            old(self)@ == final(self)@.union_prefer_right(result@),
863            result@.dom() == s,
864            final(self)@.dom() == olddom - s,
865    {
866        let tracked out = self.split(s);
867        assert(olddom == old(self)@.dom());
868        assert(self@.dom() == old(self)@.dom() - s);
869        assert(self@.dom() == olddom - s);
870        assert(out@.dom() == s);
871        out
872    }
873
874    /// We can separate a single key out of a [`GhostISubmap`]
875    pub proof fn split_points_to(tracked &mut self, k: K) -> (tracked result: GhostIPointsTo<K, V>)
876        requires
877            old(self)@.contains_key(k),
878        ensures
879            final(self).id() == old(self).id(),
880            result.id() == final(self).id(),
881            old(self)@ == final(self)@.insert(result.key(), result.value()),
882            result.key() == k,
883            final(self)@ == old(self)@.remove(k),
884    {
885        use_type_invariant(&*self);
886
887        let tracked submap = self.split(iset![k]);
888        GhostIPointsTo { submap }
889    }
890
891    /// When we have both the [`GhostIMapAuth`] and a [`GhostISubmap`] we can update the values for a
892    /// subset of keys in our submap.
893    /// ```
894    /// proof fn test(tracked auth: &mut GhostIMapAuth<int, int>, tracked sub: &mut GhostISubmap<int, int>)
895    ///     requires
896    ///         auth.id() == sub.id(),
897    ///         sub.dom() == set![1int, 2int, 3int]
898    ///     ensures
899    ///         auth[1int] == 9int
900    ///         auth[2int] == 10int
901    ///         auth[3int] == 11int
902    /// {
903    ///     // need to agree on the subset
904    ///     sub.agree(auth);
905    ///     assert(sub@ <= auth@);
906    ///     sub.update(map![1int => 9int, 2int => 10int, 3int => 11int]);
907    /// }
908    /// ```
909    pub proof fn update(tracked &mut self, tracked auth: &mut GhostIMapAuth<K, V>, m: IMap<K, V>)
910        requires
911            m.dom() <= old(self)@.dom(),
912            old(self).id() == old(auth).id(),
913        ensures
914            final(self).id() == old(self).id(),
915            final(auth).id() == old(auth).id(),
916            final(self)@ == old(self)@.union_prefer_right(m),
917            final(auth)@ == old(auth)@.union_prefer_right(m),
918    {
919        broadcast use lemma_submap_of_trans;
920        broadcast use lemma_submap_of_op;
921
922        use_type_invariant(&*self);
923        use_type_invariant(&*auth);
924
925        let tracked mut mself = Self::dummy();
926        tracked_swap(self, &mut mself);
927        let tracked mut frac_r = mself.r;
928
929        let tracked mut mauth = GhostIMapAuth::<K, V>::dummy();
930        tracked_swap(auth, &mut mauth);
931        let tracked mut auth_r = mauth.r;
932
933        frac_r.validate_2(&auth_r);
934        let tracked mut full_r = frac_r.join(auth_r);
935
936        assert(full_r.value().frac.owning_map() == frac_r.value().frac.owning_map());
937
938        let auth_carrier = AuthCarrier::Auth(full_r.value().auth.map().union_prefer_right(m));
939        let frac_carrier = FracCarrier::Frac {
940            owning: full_r.value().frac.owning_map().union_prefer_right(m),
941            dup: IMap::empty(),
942        };
943        let new_full_carrier = IMapCarrier { auth: auth_carrier, frac: frac_carrier };
944
945        assert(new_full_carrier.valid());
946        let tracked r_upd = full_r.update(new_full_carrier);
947
948        let new_auth_carrier = IMapCarrier {
949            auth: r_upd.value().auth,
950            frac: FracCarrier::Frac { owning: IMap::empty(), dup: IMap::empty() },
951        };
952        let new_frac_carrier = IMapCarrier { auth: AuthCarrier::Frac, frac: r_upd.value().frac };
953        assert(r_upd.value().frac == IMapCarrier::op(new_auth_carrier, new_frac_carrier).frac);
954        assert(r_upd.value() == IMapCarrier::op(new_auth_carrier, new_frac_carrier));
955
956        let tracked (new_auth_r, new_frac_r) = r_upd.split(new_auth_carrier, new_frac_carrier);
957        auth.r = new_auth_r;
958        self.r = new_frac_r;
959    }
960
961    /// Converting a [`GhostISubmap`] into a [`GhostIPointsTo`]
962    pub proof fn points_to(tracked self) -> (tracked r: GhostIPointsTo<K, V>)
963        requires
964            self.is_points_to(),
965        ensures
966            self@ == imap![r.key() => r.value()],
967            self.id() == r.id(),
968    {
969        let tracked r = GhostIPointsTo { submap: self };
970        r.lemma_map_view();
971        r
972    }
973
974    /// Convert a [`GhostISubmap`] into a [`GhostPersistentISubmap`]
975    pub proof fn persist(tracked self) -> (tracked r: GhostPersistentISubmap<K, V>)
976        ensures
977            self@ == r@,
978            self.id() == r.id(),
979    {
980        broadcast use lemma_submap_of_trans;
981        broadcast use lemma_submap_of_op;
982
983        use_type_invariant(&self);
984
985        let tracked mut r = self.r;
986
987        let self_carrier = IMapCarrier {
988            auth: AuthCarrier::Frac,
989            frac: FracCarrier::Frac {
990                owning: self.r.value().frac.owning_map(),
991                dup: self.r.value().frac.dup_map(),
992            },
993        };
994
995        let res_carrier = IMapCarrier {
996            auth: AuthCarrier::Frac,
997            frac: FracCarrier::Frac {
998                owning: self.r.value().frac.dup_map(),
999                dup: self.r.value().frac.owning_map(),
1000            },
1001        };
1002
1003        let tracked r = r.update(res_carrier);
1004        GhostPersistentISubmap { r }
1005    }
1006}
1007
1008impl<K, V> GhostPersistentISubmap<K, V> {
1009    #[verifier::type_invariant]
1010    spec fn inv(self) -> bool {
1011        &&& self.r.value().auth is Frac
1012        &&& self.r.value().frac is Frac
1013        &&& self.r.value().frac.owning_map().is_empty()
1014    }
1015
1016    /// Checks whether the [`GhostPersistentISubmap`] refers to a single key (and thus can be converted to a
1017    /// [`GhostPersistentIPointsTo`]).
1018    pub open spec fn is_points_to(self) -> bool {
1019        &&& self@.len() == 1
1020        &&& self.dom().finite()
1021        &&& !self@.is_empty()
1022    }
1023
1024    /// Resource location
1025    pub closed spec fn id(self) -> Loc {
1026        self.r.loc()
1027    }
1028
1029    /// Logically underlying [`IMap`]
1030    pub closed spec fn view(self) -> IMap<K, V> {
1031        self.r.value().frac.dup_map()
1032    }
1033
1034    /// Domain of the [`GhostPersistentISubmap`]
1035    pub open spec fn dom(self) -> ISet<K> {
1036        self@.dom()
1037    }
1038
1039    /// Indexing operation `submap[key]`
1040    pub open spec fn spec_index(self, key: K) -> V
1041        recommends
1042            self.dom().contains(key),
1043    {
1044        self@[key]
1045    }
1046
1047    /// Instantiate a dummy [`GhostPersistentISubmap`]
1048    pub proof fn dummy() -> (tracked result: GhostPersistentISubmap<K, V>) {
1049        let tracked owned = GhostISubmap::<K, V>::dummy();
1050        owned.persist()
1051    }
1052
1053    /// Create an empty [`GhostPersistentISubmap`]
1054    pub proof fn empty(tracked &self) -> (tracked result: GhostPersistentISubmap<K, V>)
1055        ensures
1056            result.id() == self.id(),
1057            result@ == IMap::<K, V>::empty(),
1058    {
1059        use_type_invariant(self);
1060        let tracked r = Resource::<IMapCarrier<_, _>>::create_unit(self.r.loc());
1061        GhostISubmap { r }.persist()
1062    }
1063
1064    /// Duplicate the [`GhostPersistentISubmap`]
1065    pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentISubmap<K, V>)
1066        ensures
1067            result.id() == self.id(),
1068            result@ == self@,
1069    {
1070        use_type_invariant(&*self);
1071
1072        assert(IMapCarrier::op(self.r.value(), self.r.value()) == self.r.value());
1073        let tracked r = super::super::lib::duplicate(&self.r);
1074
1075        GhostPersistentISubmap { r }
1076    }
1077
1078    /// Agreement between a [`GhostPersistentISubmap`] and a corresponding [`GhostIMapAuth`]
1079    ///
1080    /// Verus might not have full context of the [`GhostIMapAuth`] and a corresponding [`GhostPersistentISubmap`].
1081    /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
1082    /// can assert that the [`GhostPersistentISubmap`] is a submap of the [`GhostIMapAuth`].
1083    /// ```
1084    /// proof fn test(tracked &auth: GhostIMapAuth<int, int>, tracked &sub: GhostPersistentISubmap<int, int>)
1085    ///     requires
1086    ///         auth.id() == sub.id(),
1087    ///         sub.dom().contains(1int),
1088    ///         sub[1int] == 1int,
1089    ///     ensures
1090    ///         auth[1int] == 1int
1091    /// {
1092    ///     sub.agree(auth);
1093    ///     assert(sub@ <= auth@);
1094    ///     assert(auth[1int] == 1int);
1095    /// }
1096    /// ```
1097    pub proof fn agree(
1098        tracked self: &GhostPersistentISubmap<K, V>,
1099        tracked auth: &GhostIMapAuth<K, V>,
1100    )
1101        requires
1102            self.id() == auth.id(),
1103        ensures
1104            self@ <= auth@,
1105    {
1106        broadcast use lemma_submap_of_trans;
1107
1108        use_type_invariant(self);
1109        use_type_invariant(auth);
1110
1111        let tracked joined = self.r.join_shared(&auth.r);
1112        joined.validate();
1113        assert(self.r.value().frac.dup_map() <= joined.value().frac.dup_map());
1114    }
1115
1116    /// Combining two [`GhostPersistentISubmap`]s is possible.
1117    /// We consume the input [`GhostPersistentISubmap`] and merge it into the first.
1118    /// We also learn that they agreed
1119    pub proof fn combine(tracked &mut self, tracked other: GhostPersistentISubmap<K, V>)
1120        requires
1121            old(self).id() == other.id(),
1122        ensures
1123            final(self).id() == old(self).id(),
1124            final(self)@ == old(self)@.union_prefer_right(other@),
1125            old(self)@.agrees(other@),
1126    {
1127        use_type_invariant(&*self);
1128        use_type_invariant(&other);
1129
1130        self.r.validate_2(&other.r);
1131        incorporate(&mut self.r, other.r);
1132    }
1133
1134    /// Combining a [`GhostPersistentIPointsTo`] into [`GhostPersistentISubmap`] is possible, in a similar way to the way to combine
1135    /// [`GhostPersistentISubmap`]s.
1136    pub proof fn combine_points_to(tracked &mut self, tracked other: GhostPersistentIPointsTo<K, V>)
1137        requires
1138            old(self).id() == other.id(),
1139        ensures
1140            final(self).id() == old(self).id(),
1141            final(self)@ == old(self)@.insert(other.key(), other.value()),
1142            old(self)@.contains_key(other.key()) ==> old(self)@[other.key()] == other.value(),
1143    {
1144        use_type_invariant(&*self);
1145        use_type_invariant(&other);
1146
1147        other.lemma_map_view();
1148        self.combine(other.submap);
1149    }
1150
1151    /// When we have a [`GhostPersistentISubmap`] and a [`GhostISubmap`] we can prove that they have disjoint domains.
1152    pub proof fn disjoint(tracked &mut self, tracked other: &GhostISubmap<K, V>)
1153        requires
1154            old(self).id() == other.id(),
1155        ensures
1156            final(self).id() == old(self).id(),
1157            final(self)@ == old(self)@,
1158            final(self)@.dom().disjoint(other@.dom()),
1159    {
1160        use_type_invariant(&*self);
1161        use_type_invariant(other);
1162        self.r.validate_2(&other.r);
1163    }
1164
1165    /// When we have two [`GhostPersistentISubmap`]s we can prove that they agree on their intersection.
1166    pub proof fn intersection_agrees(
1167        tracked &mut self,
1168        tracked other: &GhostPersistentISubmap<K, V>,
1169    )
1170        requires
1171            old(self).id() == other.id(),
1172        ensures
1173            final(self).id() == old(self).id(),
1174            final(self)@ == old(self)@,
1175            final(self)@.agrees(other@),
1176    {
1177        use_type_invariant(&*self);
1178        use_type_invariant(other);
1179        self.r.validate_2(&other.r);
1180    }
1181
1182    /// When we have a [`GhostPersistentISubmap`] and a [`GhostIPointsTo`] we can prove that they are in disjoint
1183    /// domains.
1184    pub proof fn disjoint_points_to(tracked &mut self, tracked other: &GhostIPointsTo<K, V>)
1185        requires
1186            old(self).id() == other.id(),
1187        ensures
1188            final(self).id() == old(self).id(),
1189            final(self)@ == old(self)@,
1190            !final(self)@.contains_key(other.key()),
1191    {
1192        use_type_invariant(&*self);
1193        use_type_invariant(other);
1194        self.disjoint(&other.submap);
1195    }
1196
1197    /// When we have a [`GhostPersistentISubmap`] and a [`GhostPersistentIPointsTo`],
1198    /// we can prove that either they are disjoint domains or the key-value pair is in the
1199    /// persistent submap.
1200    pub proof fn intersection_agrees_points_to(
1201        tracked &mut self,
1202        tracked other: &GhostPersistentIPointsTo<K, V>,
1203    )
1204        requires
1205            old(self).id() == other.id(),
1206        ensures
1207            final(self).id() == old(self).id(),
1208            final(self)@ == old(self)@,
1209            final(self)@.contains_key(other.key()) ==> final(self)@[other.key()] == other.value(),
1210    {
1211        use_type_invariant(&*self);
1212        use_type_invariant(other);
1213        self.intersection_agrees(&other.submap);
1214    }
1215
1216    /// We can split a [`GhostPersistentISubmap`] based on a set of keys in its domain.
1217    pub proof fn split(tracked &mut self, s: ISet<K>) -> (tracked result: GhostPersistentISubmap<
1218        K,
1219        V,
1220    >)
1221        requires
1222            s <= old(self)@.dom(),
1223        ensures
1224            final(self).id() == old(self).id(),
1225            result.id() == final(self).id(),
1226            old(self)@ == final(self)@.union_prefer_right(result@),
1227            result@.dom() =~= s,
1228            final(self)@.dom() =~= old(self)@.dom() - s,
1229    {
1230        use_type_invariant(&*self);
1231
1232        let tracked mut r = Resource::alloc(IMapCarrier::<K, V>::unit());
1233        tracked_swap(&mut self.r, &mut r);
1234
1235        let self_carrier = IMapCarrier {
1236            auth: AuthCarrier::Frac,
1237            frac: FracCarrier::Frac {
1238                owning: r.value().frac.owning_map(),
1239                dup: r.value().frac.dup_map().remove_keys(s),
1240            },
1241        };
1242
1243        let res_carrier = IMapCarrier {
1244            auth: AuthCarrier::Frac,
1245            frac: FracCarrier::Frac {
1246                owning: r.value().frac.owning_map(),
1247                dup: r.value().frac.dup_map().restrict(s),
1248            },
1249        };
1250
1251        assert(r.value().frac == IMapCarrier::op(self_carrier, res_carrier).frac);
1252        let tracked (self_r, res_r) = r.split(self_carrier, res_carrier);
1253        self.r = self_r;
1254        GhostPersistentISubmap { r: res_r }
1255    }
1256
1257    /// We can separate a single key out of a [`GhostPersistentISubmap`]
1258    pub proof fn split_points_to(tracked &mut self, k: K) -> (tracked result:
1259        GhostPersistentIPointsTo<K, V>)
1260        requires
1261            old(self)@.contains_key(k),
1262        ensures
1263            final(self).id() == old(self).id(),
1264            result.id() == final(self).id(),
1265            old(self)@ == final(self)@.insert(result.key(), result.value()),
1266            result.key() == k,
1267            final(self)@ == old(self)@.remove(k),
1268    {
1269        use_type_invariant(&*self);
1270
1271        let tracked submap = self.split(iset![k]);
1272        GhostPersistentIPointsTo { submap }
1273    }
1274
1275    /// Convert a [`GhostPersistentISubmap`] into a [`GhostPersistentIPointsTo`]
1276    pub proof fn points_to(tracked self) -> (tracked r: GhostPersistentIPointsTo<K, V>)
1277        requires
1278            self.is_points_to(),
1279        ensures
1280            self@ == imap![r.key() => r.value()],
1281            self.id() == r.id(),
1282    {
1283        let tracked r = GhostPersistentIPointsTo { submap: self };
1284        r.lemma_map_view();
1285        r
1286    }
1287}
1288
1289impl<K, V> GhostIPointsTo<K, V> {
1290    #[verifier::type_invariant]
1291    spec fn inv(self) -> bool {
1292        self.submap.is_points_to()
1293    }
1294
1295    /// Location of the underlying resource
1296    pub closed spec fn id(self) -> Loc {
1297        self.submap.id()
1298    }
1299
1300    /// Key-Value pair underlying the points to relationship
1301    pub open spec fn view(self) -> (K, V) {
1302        (self.key(), self.value())
1303    }
1304
1305    /// Key of the points to
1306    pub closed spec fn key(self) -> K {
1307        self.submap.dom().choose()
1308    }
1309
1310    /// Pointed-to value
1311    pub closed spec fn value(self) -> V {
1312        self.submap[self.key()]
1313    }
1314
1315    /// Agreement between a [`GhostIPointsTo`] and a corresponding [`GhostIMapAuth`]
1316    ///
1317    /// Verus might not have full context of the [`GhostIMapAuth`] and a corresponding [`GhostIPointsTo`].
1318    /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
1319    /// can assert that the [`GhostIPointsTo`] is a key-value pair in the [`GhostIMapAuth`].
1320    /// ```
1321    /// proof fn test(tracked &auth: GhostIMapAuth<int, int>, tracked &pt: GhostIPointsTo<int, int>)
1322    ///     requires
1323    ///         auth.id() == sub.id(),
1324    ///         pt@ == (1int, 1int)
1325    ///     ensures
1326    ///         auth[1int] == 1int
1327    /// {
1328    ///     pt.agree(auth);
1329    ///     assert(auth[1int] == 1int);
1330    /// }
1331    /// ```
1332    pub proof fn agree(tracked self: &GhostIPointsTo<K, V>, tracked auth: &GhostIMapAuth<K, V>)
1333        requires
1334            self.id() == auth.id(),
1335        ensures
1336            auth@.contains_pair(self.key(), self.value()),
1337    {
1338        use_type_invariant(self);
1339        use_type_invariant(auth);
1340
1341        self.lemma_map_view();
1342        self.submap.agree(auth);
1343        assert(self.submap@ <= auth@);
1344        assert(self.submap@.dom().contains(self.key()));
1345        assert(auth@.dom().contains(self.key()));
1346        assert(self.submap@[self.key()] == self.value());
1347        assert(auth@[self.key()] == self.value());
1348    }
1349
1350    /// We can combine two [`GhostIPointsTo`]s into a [`GhostISubmap`]
1351    /// We also learn that they were disjoint.
1352    pub proof fn combine(tracked self, tracked other: GhostIPointsTo<K, V>) -> (tracked r:
1353        GhostISubmap<K, V>)
1354        requires
1355            self.id() == other.id(),
1356        ensures
1357            r.id() == self.id(),
1358            r@ == imap![self.key() => self.value(), other.key() => other.value()],
1359            self.key() != other.key(),
1360    {
1361        use_type_invariant(&self);
1362        use_type_invariant(&other);
1363
1364        let tracked mut submap = self.submap();
1365        submap.combine_points_to(other);
1366
1367        submap
1368    }
1369
1370    /// Shows that if a two [`GhostIPointsTo`]s are not owning the same key
1371    pub proof fn disjoint(tracked &mut self, tracked other: &GhostIPointsTo<K, V>)
1372        requires
1373            old(self).id() == other.id(),
1374        ensures
1375            final(self).id() == old(self).id(),
1376            final(self)@ == old(self)@,
1377            final(self).key() != other.key(),
1378    {
1379        use_type_invariant(&*self);
1380        use_type_invariant(other);
1381        self.submap.disjoint(&other.submap);
1382    }
1383
1384    /// Shows that if a [`GhostIPointsTo`] and a [`GhostISubmap`] are not owning the same key
1385    pub proof fn disjoint_submap(tracked &mut self, tracked other: &GhostISubmap<K, V>)
1386        requires
1387            old(self).id() == other.id(),
1388        ensures
1389            final(self).id() == old(self).id(),
1390            final(self)@ == old(self)@,
1391            !other.dom().contains(final(self).key()),
1392    {
1393        use_type_invariant(&*self);
1394        use_type_invariant(other);
1395        self.submap.disjoint(other);
1396    }
1397
1398    /// Shows that if a [`GhostIPointsTo`] and a [`GhostPersistentISubmap`] are not owning the same key
1399    pub proof fn disjoint_persistent_submap(
1400        tracked &mut self,
1401        tracked other: &GhostPersistentISubmap<K, V>,
1402    )
1403        requires
1404            old(self).id() == other.id(),
1405        ensures
1406            final(self).id() == old(self).id(),
1407            final(self)@ == old(self)@,
1408            !other.dom().contains(final(self).key()),
1409    {
1410        use_type_invariant(&*self);
1411        use_type_invariant(other);
1412        self.submap.disjoint_persistent(other);
1413    }
1414
1415    /// Shows that if a [`GhostIPointsTo`] and a [`GhostPersistentIPointsTo`] are not owning the same key
1416    pub proof fn disjoint_persistent(
1417        tracked &mut self,
1418        tracked other: &GhostPersistentIPointsTo<K, V>,
1419    )
1420        requires
1421            old(self).id() == other.id(),
1422        ensures
1423            final(self).id() == old(self).id(),
1424            final(self)@ == old(self)@,
1425            final(self).key() != other.key(),
1426    {
1427        use_type_invariant(&*self);
1428        use_type_invariant(other);
1429        self.submap.disjoint_persistent_points_to(other);
1430    }
1431
1432    /// Update pointed to value
1433    pub proof fn update(tracked &mut self, tracked auth: &mut GhostIMapAuth<K, V>, v: V)
1434        requires
1435            old(self).id() == old(auth).id(),
1436        ensures
1437            final(self).id() == old(self).id(),
1438            final(auth).id() == old(auth).id(),
1439            final(self).key() == old(self).key(),
1440            final(self)@ == (final(self).key(), v),
1441            final(auth)@ == old(auth)@.union_prefer_right(imap![final(self).key() => v]),
1442    {
1443        broadcast use lemma_submap_of_trans;
1444        broadcast use lemma_submap_of_op;
1445
1446        use_type_invariant(&*self);
1447        use_type_invariant(&*auth);
1448
1449        let ghost old_dom = self.submap.dom();
1450        self.lemma_map_view();
1451        let m = imap![self.key() => v];
1452        assert(self.submap@.union_prefer_right(m) == m);
1453        self.submap.update(auth, m);
1454    }
1455
1456    /// Convert the [`GhostIPointsTo`] a [`GhostISubmap`]
1457    pub proof fn submap(tracked self) -> (tracked r: GhostISubmap<K, V>)
1458        ensures
1459            r.id() == self.id(),
1460            r@ == imap![self.key() => self.value()],
1461    {
1462        self.lemma_map_view();
1463        self.submap
1464    }
1465
1466    proof fn lemma_map_view(tracked &self)
1467        ensures
1468            self.submap@ == imap![self.key() => self.value()],
1469    {
1470        use_type_invariant(self);
1471        let key = self.key();
1472        let target_dom = iset![key];
1473
1474        assert(self.submap@.dom().len() == 1);
1475        assert(target_dom.len() == 1);
1476
1477        assert(self.submap@.dom().finite());
1478        assert(target_dom.finite());
1479
1480        assert(self.submap@.dom().contains(key));
1481        assert(target_dom.contains(key));
1482
1483        assert(self.submap@.dom().remove(key).len() == 0);
1484        assert(target_dom.remove(key).len() == 0);
1485
1486        assert(self.submap@.dom() =~= target_dom);
1487        assert(self.submap@ == imap![self.key() => self.value()]);
1488    }
1489
1490    /// Can be used to learn what the key-value pair of [`GhostIPointsTo`] is
1491    pub proof fn lemma_view(self)
1492        ensures
1493            self@ == (self.key(), self.value()),
1494    {
1495    }
1496
1497    /// Convert a [`GhostIPointsTo`] into a [`GhostPersistentIPointsTo`]
1498    pub proof fn persist(tracked self) -> (tracked r: GhostPersistentIPointsTo<K, V>)
1499        ensures
1500            self@ == r@,
1501            self.id() == r.id(),
1502    {
1503        use_type_invariant(&self);
1504        self.submap.persist().points_to()
1505    }
1506}
1507
1508impl<K, V> GhostPersistentIPointsTo<K, V> {
1509    #[verifier::type_invariant]
1510    spec fn inv(self) -> bool {
1511        self.submap.is_points_to()
1512    }
1513
1514    /// Location of the underlying resource
1515    pub closed spec fn id(self) -> Loc {
1516        self.submap.id()
1517    }
1518
1519    /// Key-Value pair underlying the points to relationship
1520    pub open spec fn view(self) -> (K, V) {
1521        (self.key(), self.value())
1522    }
1523
1524    /// Key of the points to
1525    pub closed spec fn key(self) -> K {
1526        self.submap.dom().choose()
1527    }
1528
1529    /// Pointed-to value
1530    pub closed spec fn value(self) -> V {
1531        self.submap[self.key()]
1532    }
1533
1534    /// Duplicate the [`GhostPersistentIPointsTo`]
1535    pub proof fn duplicate(tracked &self) -> (tracked result: GhostPersistentIPointsTo<K, V>)
1536        ensures
1537            result.id() == self.id(),
1538            result@ == self@,
1539    {
1540        use_type_invariant(&*self);
1541        let tracked submap = self.submap.duplicate();
1542        GhostPersistentIPointsTo { submap }
1543    }
1544
1545    /// Agreement between a [`GhostPersistentIPointsTo`] and a corresponding [`GhostIMapAuth`]
1546    ///
1547    /// Verus might not have full context of the [`GhostIMapAuth`] and a corresponding [`GhostPersistentIPointsTo`].
1548    /// However, whenever we know that they refer to the same resource (i.e., have matching ids) we
1549    /// can assert that the [`GhostPersistentIPointsTo`] is a key-value pair in the [`GhostIMapAuth`].
1550    /// ```
1551    /// proof fn test(tracked &auth: GhostIMapAuth<int, int>, tracked &pt: GhostPersistentIPointsTo<int, int>)
1552    ///     requires
1553    ///         auth.id() == sub.id(),
1554    ///         pt@ == (1int, 1int)
1555    ///     ensures
1556    ///         auth[1int] == 1int
1557    /// {
1558    ///     pt.agree(auth);
1559    ///     assert(auth[1int] == 1int);
1560    /// }
1561    /// ```
1562    pub proof fn agree(
1563        tracked self: &GhostPersistentIPointsTo<K, V>,
1564        tracked auth: &GhostIMapAuth<K, V>,
1565    )
1566        requires
1567            self.id() == auth.id(),
1568        ensures
1569            auth@.contains_pair(self.key(), self.value()),
1570    {
1571        use_type_invariant(self);
1572        use_type_invariant(auth);
1573
1574        self.lemma_map_view();
1575        self.submap.agree(auth);
1576        assert(self.submap@ <= auth@);
1577        assert(self.submap@.contains_key(self.key()));
1578    }
1579
1580    /// We can combine two [`GhostPersistentIPointsTo`]s into a [`GhostPersistentISubmap`]
1581    pub proof fn combine(
1582        tracked self,
1583        tracked other: GhostPersistentIPointsTo<K, V>,
1584    ) -> (tracked submap: GhostPersistentISubmap<K, V>)
1585        requires
1586            self.id() == other.id(),
1587        ensures
1588            submap.id() == self.id(),
1589            submap@ == imap![self.key() => self.value(), other.key() => other.value()],
1590            self.key() != other.key() ==> submap@.len() == 2,
1591            self.key() == other.key() ==> submap@.len() == 1,
1592    {
1593        use_type_invariant(&self);
1594        use_type_invariant(&other);
1595
1596        let tracked mut submap = self.submap();
1597        submap.combine_points_to(other);
1598
1599        submap
1600    }
1601
1602    /// When we have a [`GhostPersistentIPointsTo`] and a [`GhostIPointsTo`], we can prove that they are in disjoint
1603    /// domains.
1604    pub proof fn disjoint(tracked &mut self, tracked other: &GhostIPointsTo<K, V>)
1605        requires
1606            old(self).id() == other.id(),
1607        ensures
1608            final(self).id() == old(self).id(),
1609            final(self)@ == old(self)@,
1610            final(self).key() != other.key(),
1611    {
1612        use_type_invariant(&*self);
1613        use_type_invariant(other);
1614        self.disjoint_submap(&other.submap);
1615    }
1616
1617    /// When we have a [`GhostPersistentIPointsTo`] and a [`GhostISubmap`], we can prove that they are in disjoint
1618    /// domains.
1619    pub proof fn disjoint_submap(tracked &mut self, tracked other: &GhostISubmap<K, V>)
1620        requires
1621            old(self).id() == other.id(),
1622        ensures
1623            final(self).id() == old(self).id(),
1624            final(self)@ == old(self)@,
1625            !other@.contains_key(final(self).key()),
1626    {
1627        use_type_invariant(&*self);
1628        use_type_invariant(other);
1629        self.submap.disjoint(&other);
1630    }
1631
1632    /// Shows that if a client has two [`GhostPersistentIPointsTo`]s they are either disjoint or
1633    /// agreeing in values in the intersection
1634    pub proof fn intersection_agrees(
1635        tracked &mut self,
1636        tracked other: &GhostPersistentIPointsTo<K, V>,
1637    )
1638        requires
1639            old(self).id() == other.id(),
1640        ensures
1641            final(self).id() == old(self).id(),
1642            final(self)@ == old(self)@,
1643            final(self).key() == other.key() ==> final(self).value() == other.value(),
1644    {
1645        use_type_invariant(&*self);
1646        use_type_invariant(other);
1647        self.submap.intersection_agrees_points_to(&other);
1648    }
1649
1650    /// Shows that if a [`GhostPersistentIPointsTo`] and a [`GhostISubmap`] are not owning the same key
1651    pub proof fn intersection_agrees_submap(
1652        tracked &mut self,
1653        tracked other: &GhostPersistentISubmap<K, V>,
1654    )
1655        requires
1656            old(self).id() == other.id(),
1657        ensures
1658            final(self).id() == old(self).id(),
1659            final(self)@ == old(self)@,
1660            other@.contains_key(final(self).key()) ==> other@[final(self).key()]
1661                == final(self).value(),
1662    {
1663        use_type_invariant(&*self);
1664        use_type_invariant(other);
1665        self.submap.intersection_agrees(other);
1666    }
1667
1668    /// Convert the [`GhostPersistentIPointsTo`] a [`GhostPersistentISubmap`]
1669    pub proof fn submap(tracked self) -> (tracked r: GhostPersistentISubmap<K, V>)
1670        ensures
1671            r.id() == self.id(),
1672            r@ == imap![self.key() => self.value()],
1673    {
1674        self.lemma_map_view();
1675        self.submap
1676    }
1677
1678    proof fn lemma_map_view(tracked &self)
1679        ensures
1680            self.submap@ == imap![self.key() => self.value()],
1681    {
1682        use_type_invariant(self);
1683        let key = self.key();
1684        let target_dom = iset![key];
1685
1686        assert(self.submap@.dom().len() == 1);
1687        assert(target_dom.len() == 1);
1688
1689        assert(self.submap@.dom().finite());
1690        assert(target_dom.finite());
1691
1692        assert(self.submap@.dom().contains(key));
1693        assert(target_dom.contains(key));
1694
1695        assert(self.submap@.dom().remove(key).len() == 0);
1696        assert(target_dom.remove(key).len() == 0);
1697
1698        assert(self.submap@.dom() =~= target_dom);
1699        assert(self.submap@ == imap![self.key() => self.value()]);
1700    }
1701
1702    /// Can be used to learn what the key-value pair of [`GhostPersistentIPointsTo`] is
1703    pub proof fn lemma_view(self)
1704        ensures
1705            self@ == (self.key(), self.value()),
1706    {
1707    }
1708}
1709
1710} // verus!
vstd/resource/impls/imap.rs

vstd/resource/impls/
imap.rs
