vstd/
map_lib.rs

1#[macro_use]
2use super::map::{Map, assert_maps_equal, assert_maps_equal_internal};
3#[allow(unused_imports)]
4use super::pervasive::*;
5#[allow(unused_imports)]
6use super::prelude::*;
7use super::set::*;
8#[cfg(verus_keep_ghost)]
9use super::set_lib::*;
10
11verus! {
12
13broadcast use {super::map::group_map_axioms, super::set::group_set_axioms};
14
15impl<K, V> Map<K, V> {
16    /// Is `true` if called by a "full" map, i.e., a map containing every element of type `A`.
17    #[verifier::inline]
18    pub open spec fn is_full(self) -> bool {
19        self.dom().is_full()
20    }
21
22    /// Is `true` if called by an "empty" map, i.e., a map containing no elements and has length 0
23    #[verifier::inline]
24    pub open spec fn is_empty(self) -> (b: bool) {
25        self.dom().is_empty()
26    }
27
28    /// Returns true if the key `k` is in the domain of `self`.
29    #[verifier::inline]
30    pub open spec fn contains_key(self, k: K) -> bool {
31        self.dom().contains(k)
32    }
33
34    /// Returns true if the value `v` is in the range of `self`.
35    pub open spec fn contains_value(self, v: V) -> bool {
36        exists|i: K| #[trigger] self.dom().contains(i) && self[i] == v
37    }
38
39    /// Returns `Some(v)` if the key `k` is in the domain of `self` and maps to `v`,
40    /// and `None` if the key `k` is not in the domain of `self`.
41    pub open spec fn index_opt(self, k: K) -> Option<V> {
42        if self.contains_key(k) {
43            Some(self[k])
44        } else {
45            None
46        }
47    }
48
49    ///
50    /// Returns the set of values in the map.
51    ///
52    /// ## Example
53    ///
54    /// ```rust
55    /// let m: Map<int, int> = map![1 => 10, 2 => 11];
56    /// assert(m.values() == set![10int, 11int]) by {
57    ///     assert(m.contains_key(1));
58    ///     assert(m.contains_key(2));
59    ///     assert(m.values() =~= set![10int, 11int]);
60    /// }
61    /// ```
62    pub open spec fn values(self) -> Set<V> {
63        Set::<V>::new(|v: V| self.contains_value(v))
64    }
65
66    ///
67    /// Returns the set of key-value pairs representing the map
68    ///
69    /// ## Example
70    ///
71    /// ```rust
72    /// let m: Map<int, int> = map![1 => 10, 2 => 11];
73    /// assert(m.kv_pairs() == set![(1int, 10int), (2int, 11int)] by {
74    ///     assert(m.contains_pair(1int, 10int));
75    ///     assert(m.contains_pair(2int, 11int));
76    ///     assert(m.kv_pairs() =~= set![(1int, 10int), (2int, 11int)]);
77    /// }
78    /// ```
79    pub open spec fn kv_pairs(self) -> Set<(K, V)> {
80        Set::<(K, V)>::new(|kv: (K, V)| self.dom().contains(kv.0) && self[kv.0] == kv.1)
81    }
82
83    /// Returns true if the key `k` is in the domain of `self`, and it maps to the value `v`.
84    pub open spec fn contains_pair(self, k: K, v: V) -> bool {
85        self.dom().contains(k) && self[k] == v
86    }
87
88    /// Returns true if `m1` is _contained in_ `m2`, i.e., the domain of `m1` is a subset
89    /// of the domain of `m2`, and they agree on all values in `m1`.
90    ///
91    /// ## Example
92    ///
93    /// ```rust
94    /// assert(
95    ///    map![1 => 10, 2 => 11].le(map![1 => 10, 2 => 11, 3 => 12])
96    /// );
97    /// ```
98    pub open spec fn submap_of(self, m2: Self) -> bool {
99        forall|k: K| #[trigger]
100            self.dom().contains(k) ==> #[trigger] m2.dom().contains(k) && self[k] == m2[k]
101    }
102
103    #[verifier::inline]
104    pub open spec fn spec_le(self, m2: Self) -> bool {
105        self.submap_of(m2)
106    }
107
108    /// Gives the union of two maps, defined as:
109    ///  * The domain is the union of the two input maps.
110    ///  * For a given key in _both_ input maps, it maps to the same value that it maps to in the _right_ map (`m2`).
111    ///  * For any other key in either input map (but not both), it maps to the same value
112    ///    as it does in that map.
113    ///
114    /// ## Example
115    ///
116    /// ```rust
117    /// assert(
118    ///    map![1 => 10, 2 => 11].union_prefer_right(map![1 => 20, 3 => 13])
119    ///    =~= map![1 => 20, 2 => 11, 3 => 13]);
120    /// ```
121    pub open spec fn union_prefer_right(self, m2: Self) -> Self {
122        Self::new(
123            |k: K| self.dom().contains(k) || m2.dom().contains(k),
124            |k: K|
125                if m2.dom().contains(k) {
126                    m2[k]
127                } else {
128                    self[k]
129                },
130        )
131    }
132
133    /// Removes the given keys and their associated values from the map.
134    ///
135    /// Ignores any key in `keys` which is not in the domain of `self`.
136    ///
137    /// ## Example
138    ///
139    /// ```rust
140    /// assert(
141    ///    map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
142    ///    =~= map![1 => 10]);
143    /// ```
144    pub open spec fn remove_keys(self, keys: Set<K>) -> Self {
145        Self::new(|k: K| self.dom().contains(k) && !keys.contains(k), |k: K| self[k])
146    }
147
148    /// Complement to `remove_keys`. Restricts the map to (key, value) pairs
149    /// for keys that are _in_ the given set; that is, it removes any keys
150    /// _not_ in the set.
151    ///
152    /// ## Example
153    ///
154    /// ```rust
155    /// assert(
156    ///    map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
157    ///    =~= map![2 => 11, 3 => 12]);
158    /// ```
159    pub open spec fn restrict(self, keys: Set<K>) -> Self {
160        Self::new(|k: K| self.dom().contains(k) && keys.contains(k), |k: K| self[k])
161    }
162
163    /// Returns `true` if and only if the given key maps to the same value or does not exist in self and m2.
164    pub open spec fn is_equal_on_key(self, m2: Self, key: K) -> bool {
165        ||| (!self.dom().contains(key) && !m2.dom().contains(key))
166        ||| (self.dom().contains(key) && m2.dom().contains(key) && self[key] == m2[key])
167    }
168
169    /// Returns `true` if the two given maps agree on all keys that their domains share
170    pub open spec fn agrees(self, m2: Self) -> bool {
171        forall|k| #![auto] self.dom().contains(k) && m2.dom().contains(k) ==> self[k] == m2[k]
172    }
173
174    /// Map a function `f` over all (k, v) pairs in `self`.
175    pub open spec fn map_entries<W>(self, f: spec_fn(K, V) -> W) -> Map<K, W> {
176        Map::new(|k: K| self.contains_key(k), |k: K| f(k, self[k]))
177    }
178
179    /// Map a function `f` over the values in `self`.
180    pub open spec fn map_values<W>(self, f: spec_fn(V) -> W) -> Map<K, W> {
181        Map::new(|k: K| self.contains_key(k), |k: K| f(self[k]))
182    }
183
184    /// Returns `true` if and only if a map is injective
185    pub open spec fn is_injective(self) -> bool {
186        forall|x: K, y: K|
187            x != y && self.dom().contains(x) && self.dom().contains(y) ==> #[trigger] self[x]
188                != #[trigger] self[y]
189    }
190
191    /// Swaps map keys and values. Values are not required to be unique; no
192    /// promises on which key is chosen on the intersection.
193    pub open spec fn invert(self) -> Map<V, K> {
194        Map::<V, K>::new(
195            |v: V| self.contains_value(v),
196            |v: V| choose|k: K| self.contains_pair(k, v),
197        )
198    }
199
200    // Proven lemmas
201    /// Removing a key from a map that previously contained that key decreases
202    /// the map's length by one
203    pub proof fn lemma_remove_key_len(self, key: K)
204        requires
205            self.dom().contains(key),
206            self.dom().finite(),
207        ensures
208            self.dom().len() == 1 + self.remove(key).dom().len(),
209    {
210    }
211
212    /// The domain of a map after removing a key is equivalent to removing the key from
213    /// the domain of the original map.
214    pub proof fn lemma_remove_equivalency(self, key: K)
215        ensures
216            self.remove(key).dom() == self.dom().remove(key),
217    {
218    }
219
220    /// Removing a set of n keys from a map that previously contained all n keys
221    /// results in a domain of size n less than the original domain.
222    pub proof fn lemma_remove_keys_len(self, keys: Set<K>)
223        requires
224            forall|k: K| #[trigger] keys.contains(k) ==> self.contains_key(k),
225            keys.finite(),
226            self.dom().finite(),
227        ensures
228            self.remove_keys(keys).dom().len() == self.dom().len() - keys.len(),
229        decreases keys.len(),
230    {
231        broadcast use group_set_properties;
232
233        if keys.len() > 0 {
234            let key = keys.choose();
235            let val = self[key];
236            self.remove(key).lemma_remove_keys_len(keys.remove(key));
237            assert(self.remove(key).remove_keys(keys.remove(key)) =~= self.remove_keys(keys));
238        } else {
239            assert(self.remove_keys(keys) =~= self);
240        }
241    }
242
243    /// The function `invert` results in an injective map
244    pub proof fn lemma_invert_is_injective(self)
245        ensures
246            self.invert().is_injective(),
247    {
248        assert forall|x: V, y: V|
249            x != y && self.invert().dom().contains(x) && self.invert().dom().contains(
250                y,
251            ) implies #[trigger] self.invert()[x] != #[trigger] self.invert()[y] by {
252            let i = choose|i: K| #[trigger] self.dom().contains(i) && self[i] == x;
253            assert(self.contains_pair(i, x));
254            let j = choose|j: K| self.contains_pair(j, x) && self.invert()[x] == j;
255            let k = choose|k: K| #[trigger] self.dom().contains(k) && self[k] == y;
256            assert(self.contains_pair(k, y));
257            let l = choose|l: K| self.contains_pair(l, y) && self.invert()[y] == l && l != j;
258        }
259    }
260
261    /// Keeps only those key-value pairs whose key satisfies `p`.
262    ///
263    /// ## Example
264    /// ```rust
265    /// proof fn example() {
266    ///     let m = map![1 => 10, 2 => 20];
267    ///     let even = |k: int| k % 2 == 0;
268    ///     assert(m.filter_keys(even) =~= map![2 => 20]);
269    /// }
270    /// ```
271    pub open spec fn filter_keys(self, p: spec_fn(K) -> bool) -> Self {
272        self.restrict(self.dom().filter(p))
273    }
274
275    /// Returns the value associated with key `k` in the map if it exists,
276    /// otherwise returns None.
277    ///
278    /// ## Example
279    /// ```rust
280    /// proof fn get_test() {
281    ///     let m: Map<int, bool> = map![
282    ///         1 => true,
283    ///         2 => false
284    ///     ];
285    ///
286    ///     assert(m.get(1) == Some(true));
287    ///     assert(m.get(3) == None);
288    /// }
289    /// ```
290    pub open spec fn get(self, k: K) -> Option<V> {
291        if self.dom().contains(k) {
292            Some(self[k])
293        } else {
294            None
295        }
296    }
297
298    /// A map contains a value satisfying predicate `p` iff some key maps to a value satisfying `p`.
299    ///
300    /// ## Example
301    /// ```rust
302    /// proof fn get_dom_value_any_test() {
303    ///     let m = map![1 => 10, 2 => 20, 3 => 30];
304    ///     let p = |v: int| v > 25;
305    ///     assert(m[3] == 30);
306    ///     assert(m.dom().any(|k| p(m[k])));
307    /// }
308    /// ```
309    pub proof fn get_dom_value_any(self, p: spec_fn(V) -> bool)
310        ensures
311            self.dom().any(|k: K| p(self[k])) <==> self.values().any(p),
312    {
313        broadcast use group_map_properties;
314
315        if self.dom().any(|k: K| p(self[k])) {
316            let k = choose|k: K| self.dom().contains(k) && #[trigger] p(self[k]);
317            assert(self.values().contains(self[k]));
318            assert(self.values().any(p));
319        }
320    }
321
322    /// Two maps are equal if and only if they are submaps of each other.
323    ///
324    /// ## Example
325    /// ```rust
326    /// proof fn submap_eq_test() {
327    ///     let m1 = map![1 => 10, 2 => 20];
328    ///     let m2 = map![1 => 10, 2 => 20];
329    ///     let m3 = map![1 => 10, 2 => 30];
330    ///
331    ///     assert(m1.submap_of(m2) && m2.submap_of(m1));
332    ///     assert(m1 == m2);
333    /// }
334    /// ```
335    pub proof fn lemma_submap_eq_iff(self, m: Self)
336        ensures
337            (self == m) <==> (self.submap_of(m) && m.submap_of(self)),
338    {
339        broadcast use group_map_properties;
340
341        if self.submap_of(m) && m.submap_of(self) {
342            assert(self.dom() == m.dom());
343            assert(self == m);
344        }
345    }
346
347    /// When removing a set of keys from a map after inserting (k,v),
348    /// the result depends on whether k is in the set:
349    /// if k is in the set, the insertion is discarded;
350    /// if not, the insertion happens after removal.
351    ///
352    /// ## Example
353    /// ```rust
354    /// proof fn map_remove_keys_insert_test() {
355    ///     let m = map![1 => 10, 2 => 20, 3 => 30];
356    ///     let to_remove = set![2, 4];
357    ///
358    ///     // 5 not in m: insert happens after remove
359    ///     assert(m.insert(5, 15).remove_keys(to_remove) == m.remove_keys(to_remove).insert(5, 15));
360    ///
361    ///     // 2 in m: insert is eliminated by remove
362    ///     assert(m.insert(2, 25).remove_keys(to_remove) == m.remove_keys(to_remove));
363    /// }
364    /// ```
365    pub broadcast proof fn lemma_map_remove_keys_insert(self, r: Set<K>, k: K, v: V)
366        ensures
367            #[trigger] self.insert(k, v).remove_keys(r) == if r.contains(k) {
368                self.remove_keys(r)
369            } else {
370                self.remove_keys(r).insert(k, v)
371            },
372    {
373        broadcast use group_map_properties;
374
375        let lhs = self.insert(k, v).remove_keys(r);
376        let rhs = if r.contains(k) {
377            self.remove_keys(r)
378        } else {
379            self.remove_keys(r).insert(k, v)
380        };
381        assert(lhs == rhs);
382    }
383
384    /// Filtering keys after inserting `(k, v)` leaves the result unchanged when `p(k)` is false,
385    /// and otherwise adds `(k, v)` to the already-filtered map.
386    ///
387    /// ## Example
388    /// ```rust
389    /// proof fn example() {
390    ///     let m = map![1 => 10];
391    ///     let even = |k: int| k % 2 == 0;
392    ///
393    ///     assert(m.insert(3, 30).filter_keys(even) =~= m.filter_keys(even));
394    ///     assert(m.insert(2, 20).filter_keys(even)
395    ///            =~= m.filter_keys(even).insert(2, 20));
396    /// }
397    /// ```
398    pub broadcast proof fn lemma_filter_keys_insert(self, p: spec_fn(K) -> bool, k: K, v: V)
399        ensures
400            #[trigger] self.insert(k, v).filter_keys(p) == (if p(k) {
401                self.filter_keys(p).insert(k, v)
402            } else {
403                self.filter_keys(p)
404            }),
405    {
406        broadcast use group_map_properties;
407
408        let lhs = self.insert(k, v).filter_keys(p);
409        let rhs = if p(k) {
410            self.filter_keys(p).insert(k, v)
411        } else {
412            self.filter_keys(p)
413        };
414        assert(lhs == rhs);
415    }
416}
417
418impl<K, V> Map<Seq<K>, V> {
419    /// Returns a sub-map of all entries whose key begins with `prefix`,
420    /// re-indexed so that the stored keys have that prefix removed.
421    ///
422    /// ## Example
423    /// ```rust
424    /// proof fn example() {
425    ///     let m = map![seq![1, 2] => 10, seq![1, 2, 3] => 20, seq![2] => 30];
426    ///     let sub = m.prefixed_entries(seq![1, 2]);
427    ///
428    ///     assert(sub.contains_key(seq![]));          // original key [1,2]
429    ///     assert(sub[seq![]] == 10);
430    ///
431    ///     assert(sub.contains_key(seq![3]));         // original key [1,2,3]
432    ///     assert(sub[seq![3]] == 20);
433    ///
434    ///     assert(!sub.contains_key(seq![2]));        // original key [2] was not prefixed
435    /// }
436    /// ```
437    pub open spec fn prefixed_entries(self, prefix: Seq<K>) -> Self {
438        Map::new(|k: Seq<K>| self.contains_key(prefix + k), |k: Seq<K>| self[prefix + k])
439    }
440
441    /// For every key `k` kept by `prefixed_entries(prefix)`,
442    /// the associated value is the one stored at `prefix + k` in the original map.
443    ///
444    /// ## Example
445    /// ```rust
446    /// proof fn example() {
447    ///     let m = map![seq![1, 2] => 10, seq![1, 2, 3] => 20];
448    ///     let p = seq![1, 2];
449    ///
450    ///     // key inside the sub-map
451    ///     assert(m.prefixed_entries(p)[seq![]] == m[p + seq![]]);      // 10
452    ///     assert(m.prefixed_entries(p)[seq![3]] == m[p + seq![3]]);    // 20
453    /// }
454    /// ```
455    pub broadcast proof fn lemma_prefixed_entries_get(self, prefix: Seq<K>, k: Seq<K>)
456        requires
457            self.prefixed_entries(prefix).contains_key(k),
458        ensures
459            self.prefixed_entries(prefix)[k] == #[trigger] self[prefix + k],
460    {
461        broadcast use group_map_properties;
462
463    }
464
465    /// A key `k` is in `prefixed_entries(prefix)` exactly when the original map
466    /// contains the key `prefix + k`.
467    ///
468    /// ## Example
469    /// ```rust
470    /// proof fn example() {
471    ///     let m = map![seq![1, 2] => 10, seq![1, 2, 3] => 20];
472    ///     let p = seq![1, 2];
473    ///
474    ///     assert(m.prefixed_entries(p).contains_key(seq![])
475    ///            <==> m.contains_key(p + seq![]));
476    ///
477    ///     assert(m.prefixed_entries(p).contains_key(seq![3])
478    ///            <==> m.contains_key(p + seq![3]));
479    ///
480    ///     assert(!m.prefixed_entries(p).contains_key(seq![2]));
481    /// }
482    /// ```
483    pub broadcast proof fn lemma_prefixed_entries_contains(self, prefix: Seq<K>, k: Seq<K>)
484        ensures
485            #[trigger] self.prefixed_entries(prefix).contains_key(k) <==> self.contains_key(
486                prefix + k,
487            ),
488    {
489        broadcast use group_map_properties;
490
491        let lhs = self.prefixed_entries(prefix);
492        let rhs = self;
493    }
494
495    /// Inserting `(prefix + k, v)` before taking `prefixed_entries(prefix)`
496    /// has the same effect as inserting `(k, v)` into the prefixed map.
497    ///
498    /// ## Example
499    /// ```rust
500    /// proof fn example() {
501    ///     let m = map![seq![1, 2] => 10];
502    ///     let p = seq![1, 2];
503    ///
504    ///     let left  = m.insert(p + seq![3], 20).prefixed_entries(p);
505    ///     let right = m.prefixed_entries(p).insert(seq![3], 20);
506    ///
507    ///     assert(left == right);
508    /// }
509    /// ```
510    pub broadcast proof fn lemma_prefixed_entries_insert(self, prefix: Seq<K>, k: Seq<K>, v: V)
511        ensures
512            #[trigger] self.insert(prefix + k, v).prefixed_entries(prefix) == self.prefixed_entries(
513                prefix,
514            ).insert(k, v),
515    {
516        broadcast use group_map_properties;
517        broadcast use super::seq::group_seq_axioms;
518
519        #[allow(deprecated)]
520        super::seq_lib::lemma_seq_properties::<K>();  // new broadcast group not working here
521        broadcast use Map::lemma_prefixed_entries_contains, Map::lemma_prefixed_entries_get;
522
523        let lhs = self.insert(prefix + k, v).prefixed_entries(prefix);
524        let rhs = self.prefixed_entries(prefix).insert(k, v);
525        assert(lhs =~= rhs) by {
526            assert(forall|key| key != k ==> prefix.is_prefix_of(#[trigger] (prefix + key)));
527        }
528    }
529
530    /// Taking the entries that share `prefix` commutes with `union_prefer_right`:
531    /// union the two maps first and then strip the prefix, or strip the prefix from
532    /// each map and then union them—the resulting maps are identical.
533    ///
534    /// ## Example
535    /// ```rust
536    /// proof fn example() {
537    ///     let a = map![seq![1, 2] => 10, seq![2, 3] => 20];
538    ///     let b = map![seq![1, 2] => 99, seq![2, 4] => 40];
539    ///     let p = seq![2];
540    ///
541    ///     assert(
542    ///         a.union_prefer_right(b).prefixed_entries(p)
543    ///         == a.prefixed_entries(p).union_prefer_right(b.prefixed_entries(p))
544    ///     );
545    /// }
546    /// ```
547    pub broadcast proof fn lemma_prefixed_entries_union(self, m: Self, prefix: Seq<K>)
548        ensures
549            #[trigger] self.union_prefer_right(m).prefixed_entries(prefix) == self.prefixed_entries(
550                prefix,
551            ).union_prefer_right(m.prefixed_entries(prefix)),
552    {
553        broadcast use group_map_properties;
554        broadcast use
555            Map::lemma_prefixed_entries_contains,
556            Map::lemma_prefixed_entries_get,
557            Map::lemma_prefixed_entries_insert,
558        ;
559
560        let lhs = self.union_prefer_right(m).prefixed_entries(prefix);
561        let rhs = self.prefixed_entries(prefix).union_prefer_right(m.prefixed_entries(prefix));
562        assert(lhs == rhs);
563    }
564}
565
566impl Map<int, int> {
567    /// Returns `true` if a map is monotonic -- that is, if the mapping between ordered sets
568    /// preserves the regular `<=` ordering on integers.
569    pub open spec fn is_monotonic(self) -> bool {
570        forall|x: int, y: int|
571            self.dom().contains(x) && self.dom().contains(y) && x <= y ==> #[trigger] self[x]
572                <= #[trigger] self[y]
573    }
574
575    /// Returns `true` if and only if a map is monotonic, only considering keys greater than
576    /// or equal to start
577    pub open spec fn is_monotonic_from(self, start: int) -> bool {
578        forall|x: int, y: int|
579            self.dom().contains(x) && self.dom().contains(y) && start <= x <= y
580                ==> #[trigger] self[x] <= #[trigger] self[y]
581    }
582}
583
584// Proven lemmas
585pub broadcast proof fn lemma_union_insert_left<K, V>(m1: Map<K, V>, m2: Map<K, V>, k: K, v: V)
586    requires
587        !m2.contains_key(k),
588    ensures
589        #[trigger] m1.insert(k, v).union_prefer_right(m2) == m1.union_prefer_right(m2).insert(k, v),
590{
591    assert(m1.insert(k, v).union_prefer_right(m2) =~= m1.union_prefer_right(m2).insert(k, v));
592}
593
594pub broadcast proof fn lemma_union_insert_right<K, V>(m1: Map<K, V>, m2: Map<K, V>, k: K, v: V)
595    ensures
596        #[trigger] m1.union_prefer_right(m2.insert(k, v)) == m1.union_prefer_right(m2).insert(k, v),
597{
598    assert(m1.union_prefer_right(m2.insert(k, v)) =~= m1.union_prefer_right(m2).insert(k, v));
599}
600
601pub broadcast proof fn lemma_union_remove_left<K, V>(m1: Map<K, V>, m2: Map<K, V>, k: K)
602    requires
603        m1.contains_key(k),
604        !m2.contains_key(k),
605    ensures
606        #[trigger] m1.union_prefer_right(m2).remove(k) == m1.remove(k).union_prefer_right(m2),
607{
608    assert(m1.remove(k).union_prefer_right(m2) =~= m1.union_prefer_right(m2).remove(k));
609}
610
611pub broadcast proof fn lemma_union_remove_right<K, V>(m1: Map<K, V>, m2: Map<K, V>, k: K)
612    requires
613        !m1.contains_key(k),
614        m2.contains_key(k),
615    ensures
616        #[trigger] m1.union_prefer_right(m2).remove(k) == m1.union_prefer_right(m2.remove(k)),
617{
618    assert(m1.union_prefer_right(m2.remove(k)) =~= m1.union_prefer_right(m2).remove(k));
619}
620
621pub broadcast proof fn lemma_union_dom<K, V>(m1: Map<K, V>, m2: Map<K, V>)
622    ensures
623        #[trigger] m1.union_prefer_right(m2).dom() == m1.dom().union(m2.dom()),
624{
625    assert(m1.dom().union(m2.dom()) =~= m1.union_prefer_right(m2).dom());
626}
627
628/// The size of the union of two disjoint maps is equal to the sum of the sizes of the individual maps
629pub broadcast proof fn lemma_disjoint_union_size<K, V>(m1: Map<K, V>, m2: Map<K, V>)
630    requires
631        m1.dom().disjoint(m2.dom()),
632        m1.dom().finite(),
633        m2.dom().finite(),
634    ensures
635        #[trigger] m1.union_prefer_right(m2).dom().len() == m1.dom().len() + m2.dom().len(),
636{
637    let u = m1.union_prefer_right(m2);
638    assert(u.dom() =~= m1.dom() + m2.dom());  //proves u.dom() is finite
639    assert(u.remove_keys(m1.dom()).dom() =~= m2.dom());
640    assert(u.remove_keys(m1.dom()).dom().len() == u.dom().len() - m1.dom().len()) by {
641        u.lemma_remove_keys_len(m1.dom());
642    }
643}
644
645pub broadcast group group_map_union {
646    lemma_union_dom,
647    lemma_union_remove_left,
648    lemma_union_remove_right,
649    lemma_union_insert_left,
650    lemma_union_insert_right,
651    lemma_disjoint_union_size,
652}
653
654/// submap_of (<=) is transitive.
655pub broadcast proof fn lemma_submap_of_trans<K, V>(m1: Map<K, V>, m2: Map<K, V>, m3: Map<K, V>)
656    requires
657        #[trigger] m1.submap_of(m2),
658        #[trigger] m2.submap_of(m3),
659    ensures
660        m1.submap_of(m3),
661{
662    assert forall|k| m1.dom().contains(k) implies #[trigger] m3.dom().contains(k) && m1[k]
663        == m3[k] by {
664        assert(m2.dom().contains(k));
665    }
666}
667
668// This verified lemma used to be an axiom in the Dafny prelude
669/// The domain of a map constructed with `Map::new(fk, fv)` is equivalent to the set constructed with `Set::new(fk)`.
670pub broadcast proof fn lemma_map_new_domain<K, V>(fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V)
671    ensures
672        #[trigger] Map::<K, V>::new(fk, fv).dom() == Set::<K>::new(|k: K| fk(k)),
673{
674    assert(Set::new(fk) =~= Set::<K>::new(|k: K| fk(k)));
675}
676
677// This verified lemma used to be an axiom in the Dafny prelude
678/// The set of values of a map constructed with `Map::new(fk, fv)` is equivalent to
679/// the set constructed with `Set::new(|v: V| (exists |k: K| fk(k) && fv(k) == v)`. In other words,
680/// the set of all values fv(k) where fk(k) is true.
681pub broadcast proof fn lemma_map_new_values<K, V>(fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V)
682    ensures
683        #[trigger] Map::<K, V>::new(fk, fv).values() == Set::<V>::new(
684            |v: V| (exists|k: K| #[trigger] fk(k) && #[trigger] fv(k) == v),
685        ),
686{
687    let keys = Set::<K>::new(fk);
688    let values = Map::<K, V>::new(fk, fv).values();
689    let map = Map::<K, V>::new(fk, fv);
690    assert(map.dom() =~= keys);
691    assert(forall|k: K| #[trigger] fk(k) ==> keys.contains(k));
692    assert(values =~= Set::<V>::new(
693        |v: V| (exists|k: K| #[trigger] fk(k) && #[trigger] fv(k) == v),
694    ));
695}
696
697/// Properties of maps from the Dafny prelude (which were axioms in Dafny, but proven here in Verus)
698#[deprecated = "Use `broadcast use group_map_properties` instead"]
699pub proof fn lemma_map_properties<K, V>()
700    ensures
701        forall|fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V| #[trigger]
702            Map::<K, V>::new(fk, fv).dom() == Set::<K>::new(|k: K| fk(k)),  //from lemma_map_new_domain
703        forall|fk: spec_fn(K) -> bool, fv: spec_fn(K) -> V| #[trigger]
704            Map::<K, V>::new(fk, fv).values() == Set::<V>::new(
705                |v: V| exists|k: K| #[trigger] fk(k) && #[trigger] fv(k) == v,
706            ),  //from lemma_map_new_values
707{
708    broadcast use group_map_properties;
709
710}
711
712pub broadcast group group_map_properties {
713    lemma_map_new_domain,
714    lemma_map_new_values,
715}
716
717pub broadcast group group_map_extra {
718    Map::lemma_map_remove_keys_insert,
719    Map::lemma_filter_keys_insert,
720    Map::lemma_prefixed_entries_get,
721    Map::lemma_prefixed_entries_contains,
722    Map::lemma_prefixed_entries_insert,
723    Map::lemma_prefixed_entries_union,
724}
725
726pub proof fn lemma_values_finite<K, V>(m: Map<K, V>)
727    requires
728        m.dom().finite(),
729    ensures
730        m.values().finite(),
731    decreases m.len(),
732{
733    if m.len() > 0 {
734        let k = m.dom().choose();
735        let v = m[k];
736        let m1 = m.remove(k);
737        assert(m.contains_key(k));
738        assert(m.contains_value(v));
739        let mv = m.values();
740        let m1v = m1.values();
741        assert_sets_equal!(mv == m1v.insert(v), v0 => {
742            if m.contains_value(v0) {
743                if v0 != v {
744                    let k0 = choose|k0| #![auto] m.contains_key(k0) && m[k0] == v0;
745                    assert(k0 != k);
746                    assert(m1.contains_key(k0));
747                    assert(mv.contains(v0) ==> m1v.insert(v).contains(v0));
748                    assert(mv.contains(v0) <== m1v.insert(v).contains(v0));
749                }
750            }
751        });
752        assert(m1.len() < m.len());
753        lemma_values_finite(m1);
754        axiom_set_insert_finite(m1.values(), v);
755    } else {
756        assert(m.values() =~= Set::<V>::empty());
757    }
758}
759
760} // verus!