vstd/
map.rs

1#![allow(unused_imports)]
2
3use super::pervasive::*;
4use super::prelude::*;
5use super::set::*;
6
7use verus as verus_; // skip verusfmt due to unhandled return-value-pattern
8verus_! {
9
10broadcast use {
11    super::set::group_set_lemmas,
12    super::set_lib::group_set_lib_default,
13};
14
15/// `Map<K, V>` is an abstract map type for specifications.
16/// To use a "map" in compiled code, use an `exec` type like HashMap
17/// that has a `Map<K, V>` as its specification type.
18///
19/// An object `map: Map<K, V>` has a _domain_, a set of keys given by [`map.dom()`](Map::dom),
20/// and a mapping for keys in the domain to values, given by [`map[key]`](Map::index).
21/// Alternatively, a map can be thought of as a set of `(K, V)` pairs where each key
22/// appears in at most entry.
23///
24/// A Map must will always be finite.
25/// To work with infinite maps, see `IMap`.
26///
27/// Maps can be constructed in a few different ways:
28///  * [`Map::empty()`] constructs an empty map.
29///  * [`Map::new`] constructs a map given a `Set` that specifies its domain and the mapping
30///     from keys to values (a _map comprehension_).
31///  * The [`map!`] macro, to construct small maps of a fixed size.
32///  * By manipulating an existing map with [`Map::insert`] or [`Map::remove`].
33///
34/// To prove that two maps are equal, it is usually easiest to use the extensionality operator `=~=`.
35///
36/// `Map` always has a finite domain, so it can be used in recursive types. For instance,
37/// a type `T` can contain a `Map<T, T>`.
38#[verifier::ext_equal]
39#[verifier::external_body]
40#[verifier::accept_recursive_types(K)]
41#[verifier::accept_recursive_types(V)]
42pub tracked struct Map<K, V> {
43    // To prevent Verus's internal checks from rejecting recursive types
44    // using `Map`, we use an artificial definition of `Map` that hides its
45    // inclusion of a function from keys to values.
46    //
47    // To make sure that proofs in this file don't take advantage of
48    // this artificial structure (e.g., to prove that any two `Map`s are
49    // equal), we mark this definition as `external_body`.
50    dummy_key: core::marker::PhantomData<K>,
51    dummy_value: core::marker::PhantomData<V>,
52}
53
54impl<K, V> Map<K, V> {
55    /// The domain of the map as a set.
56    pub uninterp spec fn dom(self) -> Set<K>;
57
58    /// Gets the value that the given key `key` maps to.
59    /// For keys not in the domain, the result is meaningless and arbitrary.
60    pub uninterp spec fn index(self, key: K) -> V
61        recommends
62            self.dom().contains(key),
63    ;
64
65    /// Gives a `Map<K, V>` whose domain is given, mapping each key to
66    /// the value given by `fv`.
67    pub uninterp spec fn new(s: Set<K>, fv: spec_fn(K) -> V) -> Map<K, V>;
68
69    /// This axiom says that `Map<K, V>::new` produces a `Map` whose domain
70    /// is given, mapping each key `k` to the value given by `fv(k)`.
71    broadcast axiom fn axiom_new(s: Set<K>, fv: spec_fn(K) -> V)
72        ensures
73            #![trigger Self::new(s, fv)]
74            Self::new(s, fv).dom() == s,
75            forall|k| s.contains(k) ==> #[trigger] Self::new(s, fv)[k] == fv(k),
76    ;
77
78    /// An empty map.
79    pub closed spec fn empty() -> Map<K, V> {
80        Self::new(Set::<K>::empty(), |k| arbitrary())
81    }
82
83    /// `[]` operator, synonymous with `index`
84    #[verifier::inline]
85    pub open spec fn spec_index(self, key: K) -> V
86        recommends
87            self.dom().contains(key),
88    {
89        self.index(key)
90    }
91
92    /// Inserts the given (key, value) pair into the map.
93    ///
94    /// If the key is already present from the map, then its existing value is overwritten
95    /// by the new value.
96    pub closed spec fn insert(self, key: K, value: V) -> Map<K, V> {
97        Map::new(self.dom().insert(key), |k| if k == key { value } else { self[k] })
98    }
99
100    /// Removes the given key and its associated value from the map.
101    ///
102    /// If the key is already absent from the map, then the map is left unchanged.
103    pub closed spec fn remove(self, key: K) -> Map<K, V> {
104        Map::new(self.dom().remove(key), |k| self[k])
105    }
106
107    /// Returns the number of key-value pairs in the map
108    pub open spec fn len(self) -> nat {
109        self.dom().len()
110    }
111
112    /// Converts this `Map` into an equivalent `IMap`
113    pub open spec fn to_imap(self) -> IMap<K, V> {
114        IMap::new(|k| self.dom().contains(k), |k| self[k])
115    }
116
117    /// Indicates if this `Map` is equivalent to the given `IMap`.
118    pub open spec fn congruent(self, m2: IMap<K, V>) -> bool {
119        &&& self.dom().congruent(m2.dom())
120        &&& forall|k| #[trigger] self.dom().contains(k) ==> self[k] == m2[k]
121    }
122
123    /// Create an empty tracked map.
124    ///
125    /// This allows us to create a map, which we know is empty, that is _tracked_.
126    pub axiom fn tracked_empty() -> (tracked out_v: Self)
127        ensures
128            out_v == Map::<K, V>::empty(),
129    ;
130
131    /// Inserts the given `(key, tracked value)` pair into the map.
132    ///
133    /// If the key is already present from the map, then its existing value is overwritten
134    /// by the new value.
135    pub axiom fn tracked_insert(tracked &mut self, key: K, tracked value: V)
136        ensures
137            *final(self) == Map::insert(*old(self), key, value),
138    ;
139
140    /// Removes the given key and its associated _tracked_ value from the map.
141    ///
142    /// The key must exist in the map
143    pub axiom fn tracked_remove(tracked &mut self, key: K) -> (tracked v: V)
144        requires
145            old(self).dom().contains(key),
146        ensures
147            *final(self) == Map::remove(*old(self), key),
148            v == old(self)[key],
149    ;
150
151    /// Index into a tracked map, getting a tracked borrow of the value
152    pub axiom fn tracked_borrow(tracked &self, key: K) -> (tracked v: &V)
153        requires
154            self.dom().contains(key),
155        ensures
156            *v == self.index(key),
157    ;
158
159    /// Index into a tracked map, getting a tracked mutable borrow of the value
160    pub axiom fn tracked_borrow_mut(tracked &mut self, key: K) -> (tracked v: &mut V)
161        requires
162            self.dom().contains(key),
163        ensures
164            *v == old(self).index(key),
165            *final(self) == old(self).insert(key, *final(v))
166    ;
167
168    /// Split a mutable borrow of a map into two.
169    pub axiom fn tracked_borrow_mut_split(tracked &mut self, keys: Set<K>)
170        -> (tracked (m1, m2): (&mut Self, &mut Self))
171        requires
172            keys <= self.dom(),
173        ensures
174            *m1 == old(self).restrict(keys),
175            *m2 == old(self).remove_keys(keys),
176            *final(self) == final(m1).union_prefer_right(*final(m2)),
177    ;
178
179    /// Change the keys of a map, by reverse lookup in a different map.
180    ///
181    /// For each `(old_key, new_key)` pair in `key_map`, the new map will have `(new_key, old_map[old_key])`.
182    /// Note the new map may be smaller than the old map if the `key_map` omits mappings for some of the old keys.
183    pub axiom fn tracked_map_keys<J>(
184        tracked old_map: Map<K, V>,
185        key_map: Map<J, K>,
186    ) -> (tracked new_map: Map<J, V>)
187        requires
188            forall|j| #![auto] key_map.contains_key(j) ==> old_map.contains_key(key_map[j]),
189            forall|j1, j2|
190                #![auto]
191                j1 != j2 && key_map.contains_key(j1) && key_map.contains_key(j2) ==> key_map[j1]
192                    != key_map[j2],
193        ensures
194            new_map.dom() == key_map.dom(),
195            forall|j|
196                key_map.contains_key(j) ==> new_map.contains_key(j) && #[trigger] new_map[j]
197                    == old_map[key_map[j]],
198    ;
199
200    /// Extract a set of keys (and their corresponding values) out of the map.
201    ///
202    /// This allows us to split a map based on a subset of the domain.
203    pub axiom fn tracked_remove_keys(tracked &mut self, keys: Set<K>) -> (tracked out_map: Map<
204        K,
205        V,
206    >)
207        requires
208            keys.subset_of(old(self).dom()),
209        ensures
210            *final(self) == old(self).remove_keys(keys),
211            out_map == old(self).restrict(keys),
212    ;
213
214    /// Merge a map into a tracked map.
215    ///
216    /// The new (key, value) pairs take precendece.
217    pub axiom fn tracked_union_prefer_right(tracked &mut self, right: Self)
218        ensures
219            *final(self) == old(self).union_prefer_right(right),
220    ;
221}
222
223// Trusted axioms
224pub broadcast axiom fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K)
225    requires
226        m.dom().contains(key),
227    ensures
228        #[trigger](decreases_to!(m => m[key]));
229
230pub broadcast axiom fn axiom_map_decreases_to_entry<K, V>(m: Map<K, V>, key: K)
231    requires
232        m.dom().contains(key),
233    ensures
234        #[trigger](decreases_to!(m => (key, m[key])));
235
236/// Since `Map::new` is uninterpret, this broadcast lemma is needed to establish
237/// that it produces a map with the given set as its domain.
238pub broadcast proof fn lemma_map_new_domain<K, V>(s: Set<K>, fv: spec_fn(K) -> V)
239    ensures
240        #![trigger Map::new(s, fv)]
241        Map::new(s, fv).dom() == s,
242{
243    broadcast use Map::axiom_new;
244}
245
246/// Since `Map::new` is closed, this broadcast lemma is needed to establish
247/// that it produces a map that maps elements using the given function.
248pub broadcast proof fn lemma_map_new_index<K, V>(s: Set<K>, fv: spec_fn(K) -> V, k: K)
249    requires
250        s.contains(k),
251    ensures
252        #![trigger Map::new(s, fv)[k]]
253        Map::new(s, fv)[k] == fv(k)
254{
255    broadcast use Map::axiom_new;
256}
257
258/// The domain of the empty map is the empty set
259pub broadcast proof fn lemma_map_empty<K, V>()
260    ensures
261        #[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),
262{
263    broadcast use Map::axiom_new;
264}
265
266/// The domain of a map after inserting a key-value pair is equivalent to inserting the key into
267/// the original map's domain set.
268pub broadcast proof fn lemma_map_insert_domain<K, V>(m: Map<K, V>, key: K, value: V)
269    ensures
270        #[trigger] m.insert(key, value).dom() == m.dom().insert(key),
271{
272    broadcast use Map::axiom_new;
273}
274
275/// Inserting `value` at `key` in `m` results in a map that maps `key` to `value`
276pub broadcast proof fn lemma_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V)
277    ensures
278        #[trigger] m.insert(key, value)[key] == value,
279{
280    broadcast use Map::axiom_new;
281}
282
283/// Inserting `value` at `key2` does not change the value mapped to by any other keys in `m`.
284/// This has to be an axiom because normally constructing a new map sets values outside
285/// the domain to arbitrary values.
286pub broadcast axiom fn axiom_map_insert_different<K, V>(m: Map<K, V>, key1: K, key2: K, value: V)
287    requires
288        key1 != key2,
289    ensures
290        #[trigger] m.insert(key2, value)[key1] == m[key1],
291;
292
293/// The domain of a map after removing a key-value pair is equivalent to removing the key from
294/// the original map's domain set.
295pub broadcast proof fn lemma_map_remove_domain<K, V>(m: Map<K, V>, key: K)
296    ensures
297        #[trigger] m.remove(key).dom() == m.dom().remove(key),
298{
299    broadcast use Map::axiom_new;
300}
301
302/// Removing a key-value pair from a map does not change the value mapped to by
303/// any other keys in the map.
304/// This has to be an axiom because normally constructing a new map sets values outside
305/// the domain to arbitrary values.
306pub broadcast axiom fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
307    requires
308        key1 != key2,
309    ensures
310        #[trigger] m.remove(key2)[key1] == m[key1],
311;
312
313/// Two maps are equivalent if their domains are equivalent and every key in their domains map to the same value.
314pub broadcast axiom fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
315    ensures
316        #[trigger] (m1 =~= m2) <==> {
317            &&& m1.dom() =~= m2.dom()
318            &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k]
319        },
320;
321
322/// Two maps are deeply equivalent if their domains are equivalent and
323/// every key in their domains map to values that are deeply
324/// equivalent.
325pub broadcast proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
326    ensures
327        #[trigger] (m1 =~~= m2) <==> {
328            &&& m1.dom() =~~= m2.dom()
329            &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] =~~= m2[k]
330        },
331{
332    axiom_map_ext_equal(m1, m2);
333}
334
335pub broadcast group group_map_lemmas {
336    axiom_map_index_decreases,
337    axiom_map_decreases_to_entry,
338    lemma_map_new_domain,
339    lemma_map_new_index,
340    lemma_map_empty,
341    lemma_map_insert_domain,
342    lemma_map_insert_same,
343    axiom_map_insert_different,
344    lemma_map_remove_domain,
345    axiom_map_remove_different,
346    axiom_map_ext_equal,
347    axiom_map_ext_equal_deep,
348}
349
350// Macros
351#[doc(hidden)]
352#[macro_export]
353macro_rules! map_internal {
354    [$($key:expr => $value:expr),* $(,)?] => {
355        $crate::vstd::map::Map::empty()
356            $(.insert($key, $value))*
357    }
358}
359
360/// Create a map using syntax like `map![key1 => val1, key2 => val, ...]`.
361///
362/// This is equivalent to `Map::empty().insert(key1, val1).insert(key2, val2)...`.
363///
364/// Note that this does _not_ require all keys to be distinct. In the case that two
365/// or more keys are equal, the resulting map uses the value of the rightmost entry.
366#[macro_export]
367macro_rules! map {
368    [$($tail:tt)*] => {
369        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::map::map_internal!($($tail)*))
370    };
371}
372
373#[doc(hidden)]
374#[verifier::inline]
375pub open spec fn check_argument_is_map<K, V>(m: Map<K, V>) -> Map<K, V> {
376    m
377}
378
379#[doc(hidden)]
380pub use map_internal;
381pub use map;
382
383/// Prove two maps `map1` and `map2` are equal by proving that their values are equal at each key.
384///
385/// More precisely, `assert_maps_equal!` requires that for each key `k`:
386///  * `map1` contains `k` in its domain if and only if `map2` does (`map1.dom().contains(k) <==> map2.dom().contains(k)`)
387///  * If they contain `k` in their domains, then their values are equal (`map1.dom().contains(k) && map2.dom().contains(k) ==> map1[k] == map2[k]`)
388///
389/// The property that equality follows from these facts is often called _extensionality_.
390///
391/// `assert_maps_equal!` can handle many trivial-looking
392/// identities without any additional help:
393///
394/// ```rust
395/// proof fn insert_remove(m: Map<int, int>, k: int, v: int)
396///     requires !m.dom().contains(k)
397///     ensures m.insert(k, v).remove(k) == m
398/// {
399///     let m2 = m.insert(k, v).remove(k);
400///     assert_maps_equal!(m == m2);
401///     assert(m == m2);
402/// }
403/// ```
404///
405/// For more complex cases, a proof may be required for each key:
406///
407/// ```rust
408/// proof fn bitvector_maps() {
409///     let m1 = Map::<u64, u64>::new(
410///         |key: u64| key & 31 == key,
411///         |key: u64| key | 5);
412///
413///     let m2 = Map::<u64, u64>::new(
414///         |key: u64| key < 32,
415///         |key: u64| 5 | key);
416///
417///     assert_maps_equal!(m1 == m2, key => {
418///         // Show that the domains of m1 and m2 are the same by showing their predicates
419///         // are equivalent.
420///         assert_bit_vector((key & 31 == key) <==> (key < 32));
421///
422///         // Show that the values are the same by showing that these expressions
423///         // are equivalent.
424///         assert_bit_vector(key | 5 == 5 | key);
425///     });
426/// }
427/// ```
428#[macro_export]
429macro_rules! assert_maps_equal {
430    [$($tail:tt)*] => {
431        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::map::assert_maps_equal_internal!($($tail)*))
432    };
433}
434
435#[macro_export]
436#[doc(hidden)]
437macro_rules! assert_maps_equal_internal {
438    (::verus_builtin::spec_eq($m1:expr, $m2:expr)) => {
439        assert_maps_equal_internal!($m1, $m2)
440    };
441    (::verus_builtin::spec_eq($m1:expr, $m2:expr), $k:ident $( : $t:ty )? => $bblock:block) => {
442        assert_maps_equal_internal!($m1, $m2, $k $( : $t )? => $bblock)
443    };
444    ($m1:expr, $m2:expr $(,)?) => {
445        assert_maps_equal_internal!($m1, $m2, key => { })
446    };
447    ($m1:expr, $m2:expr, $k:ident $( : $t:ty )? => $bblock:block) => {
448        #[verifier::spec] let m1 = $crate::vstd::map::check_argument_is_map($m1);
449        #[verifier::spec] let m2 = $crate::vstd::map::check_argument_is_map($m2);
450        $crate::vstd::prelude::assert_by($crate::vstd::prelude::equal(m1, m2), {
451            $crate::vstd::prelude::assert_forall_by(|$k $( : $t )?| {
452                // TODO better error message here: show the individual conjunct that fails,
453                // and maybe give an error message in english as well
454                $crate::vstd::prelude::ensures([
455                    $crate::vstd::prelude::imply(#[verifier::trigger] m1.dom().contains($k), m2.dom().contains($k))
456                    && $crate::vstd::prelude::imply(m2.dom().contains($k), m1.dom().contains($k))
457                    && $crate::vstd::prelude::imply(m1.dom().contains($k) && m2.dom().contains($k),
458                        $crate::vstd::prelude::equal(m1.index($k), m2.index($k)))
459                ]);
460                { $bblock }
461            });
462            $crate::vstd::prelude::assert_($crate::vstd::prelude::ext_equal(m1, m2));
463        });
464    }
465}
466
467#[doc(hidden)]
468pub use assert_maps_equal_internal;
469pub use assert_maps_equal;
470
471} // verus!
472
473verus_! { // skip verusfmt, issue with 'final'
474
475impl<K, V> Map<K, V> {
476    pub proof fn tracked_map_keys_in_place(tracked &mut self, key_map: Map<K, K>)
477        requires
478            forall|j|
479                #![auto]
480                key_map.dom().contains(j) ==> old(self).dom().contains(key_map.index(j)),
481            forall|j1, j2|
482                #![auto]
483                j1 != j2 && key_map.dom().contains(j1) && key_map.dom().contains(j2)
484                    ==> key_map.index(j1) != key_map.index(j2),
485        ensures
486            forall|j| #[trigger] final(self).dom().contains(j) == key_map.dom().contains(j),
487            forall|j|
488                key_map.dom().contains(j) ==> final(self).dom().contains(j) && #[trigger] final(self).index(j)
489                    == old(self).index(key_map.index(j)),
490    {
491        let tracked mut tmp = Self::tracked_empty();
492        super::modes::tracked_swap(&mut tmp, self);
493        let tracked mut tmp = Self::tracked_map_keys(tmp, key_map);
494        super::modes::tracked_swap(&mut tmp, self);
495    }
496}
497
498} // verus!
vstd/map.rs

vstd/
map.rs
