vstd/
map.rs

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

vstd/
map.rs
