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 #[verifier::inline]
18 pub open spec fn is_full(self) -> bool {
19 self.dom().is_full()
20 }
21
22 #[verifier::inline]
24 pub open spec fn is_empty(self) -> (b: bool) {
25 self.dom().is_empty()
26 }
27
28 #[verifier::inline]
30 pub open spec fn contains_key(self, k: K) -> bool {
31 self.dom().contains(k)
32 }
33
34 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 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 pub open spec fn values(self) -> Set<V> {
63 Set::<V>::new(|v: V| self.contains_value(v))
64 }
65
66 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 pub open spec fn contains_pair(self, k: K, v: V) -> bool {
85 self.dom().contains(k) && self[k] == v
86 }
87
88 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 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 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 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 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 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 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 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 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 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 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 pub proof fn lemma_remove_equivalency(self, key: K)
215 ensures
216 self.remove(key).dom() == self.dom().remove(key),
217 {
218 }
219
220 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 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 pub open spec fn filter_keys(self, p: spec_fn(K) -> bool) -> Self {
272 self.restrict(self.dom().filter(p))
273 }
274
275 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 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 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 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 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 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 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 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 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>(); 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 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 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 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
584pub 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
628pub 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()); 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
654pub 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
668pub 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
677pub 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#[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)), 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 ), {
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}