1#![allow(unused_imports)]
2
3use super::pervasive::*;
4use super::prelude::*;
5use super::set::*;
6
7verus! {
8
9#[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 pub closed spec fn empty() -> Map<K, V> {
39 Map { mapping: |k| None }
40 }
41
42 pub open spec fn total(fv: spec_fn(K) -> V) -> Map<K, V> {
45 Set::full().mk_map(fv)
46 }
47
48 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 pub closed spec fn dom(self) -> Set<K> {
56 Set::new(|k| (self.mapping)(k) is Some)
57 }
58
59 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 #[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 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 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 pub open spec fn len(self) -> nat {
108 self.dom().len()
109 }
110
111 pub axiom fn tracked_empty() -> (tracked out_v: Self)
112 ensures
113 out_v == Map::<K, V>::empty(),
114 ;
115
116 pub axiom fn tracked_insert(tracked &mut self, key: K, tracked value: V)
117 ensures
118 *self == Map::insert(*old(self), key, value),
119 ;
120
121 pub axiom fn tracked_remove(tracked &mut self, key: K) -> (tracked v: V)
123 requires
124 old(self).dom().contains(key),
125 ensures
126 *self == Map::remove(*old(self), key),
127 v == old(self)[key],
128 ;
129
130 pub axiom fn tracked_borrow(tracked &self, key: K) -> (tracked v: &V)
131 requires
132 self.dom().contains(key),
133 ensures
134 *v === self.index(key),
135 ;
136
137 pub axiom fn tracked_map_keys<J>(
138 tracked old_map: Map<K, V>,
139 key_map: Map<J, K>,
140 ) -> (tracked new_map: Map<J, V>)
141 requires
142 forall|j|
143 #![auto]
144 key_map.dom().contains(j) ==> old_map.dom().contains(key_map.index(j)),
145 forall|j1, j2|
146 #![auto]
147 !equal(j1, j2) && key_map.dom().contains(j1) && key_map.dom().contains(j2)
148 ==> !equal(key_map.index(j1), key_map.index(j2)),
149 ensures
150 forall|j| #[trigger] new_map.dom().contains(j) <==> key_map.dom().contains(j),
151 forall|j|
152 key_map.dom().contains(j) ==> new_map.dom().contains(j) && #[trigger] new_map.index(
153 j,
154 ) == old_map.index(key_map.index(j)),
155 ;
156
157 pub axiom fn tracked_remove_keys(tracked &mut self, keys: Set<K>) -> (tracked out_map: Map<
158 K,
159 V,
160 >)
161 requires
162 keys.subset_of(old(self).dom()),
163 ensures
164 self == old(self).remove_keys(keys),
165 out_map == old(self).restrict(keys),
166 ;
167
168 pub axiom fn tracked_union_prefer_right(tracked &mut self, right: Self)
169 ensures
170 *self == old(self).union_prefer_right(right),
171 ;
172}
173
174pub broadcast axiom fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
184 requires
185 m.dom().finite(),
186 m.dom().contains(key),
187 ensures
188 #[trigger] (decreases_to!(m => m[key])),
189;
190
191pub broadcast axiom fn axiom_map_index_decreases_infinite<K, V>(m: Map<K, V>, key: K)
194 requires
195 m.dom().contains(key),
196 ensures
197 #[trigger] is_smaller_than_recursive_function_field(m[key], m),
198;
199
200pub broadcast proof fn axiom_map_empty<K, V>()
202 ensures
203 #[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),
204{
205 broadcast use super::set::group_set_axioms;
206
207 assert(Set::new(|k: K| (|k| None::<V>)(k) is Some) == Set::<K>::empty());
208}
209
210pub broadcast proof fn axiom_map_insert_domain<K, V>(m: Map<K, V>, key: K, value: V)
213 ensures
214 #[trigger] m.insert(key, value).dom() == m.dom().insert(key),
215{
216 broadcast use super::set::group_set_axioms;
217
218 assert(m.insert(key, value).dom() =~= m.dom().insert(key));
219}
220
221pub broadcast proof fn axiom_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V)
223 ensures
224 #[trigger] m.insert(key, value)[key] == value,
225{
226}
227
228pub broadcast proof fn axiom_map_insert_different<K, V>(m: Map<K, V>, key1: K, key2: K, value: V)
230 requires
231 key1 != key2,
232 ensures
233 #[trigger] m.insert(key2, value)[key1] == m[key1],
234{
235}
236
237pub broadcast proof fn axiom_map_remove_domain<K, V>(m: Map<K, V>, key: K)
240 ensures
241 #[trigger] m.remove(key).dom() == m.dom().remove(key),
242{
243 broadcast use super::set::group_set_axioms;
244
245 assert(m.remove(key).dom() =~= m.dom().remove(key));
246}
247
248pub broadcast proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
251 requires
252 key1 != key2,
253 ensures
254 #[trigger] m.remove(key2)[key1] == m[key1],
255{
256}
257
258pub broadcast proof fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
260 ensures
261 #[trigger] (m1 =~= m2) <==> {
262 &&& m1.dom() =~= m2.dom()
263 &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k]
264 },
265{
266 broadcast use super::set::group_set_axioms;
267
268 if m1 =~= m2 {
269 assert(m1.dom() =~= m2.dom());
270 assert(forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k]);
271 }
272 if ({
273 &&& m1.dom() =~= m2.dom()
274 &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] == m2[k]
275 }) {
276 if m1.mapping != m2.mapping {
277 assert(exists|k| #[trigger] (m1.mapping)(k) != (m2.mapping)(k));
278 let k = choose|k| #[trigger] (m1.mapping)(k) != (m2.mapping)(k);
279 if m1.dom().contains(k) {
280 assert(m1[k] == m2[k]);
281 }
282 assert(false);
283 }
284 assert(m1 =~= m2);
285 }
286}
287
288pub broadcast proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
289 ensures
290 #[trigger] (m1 =~~= m2) <==> {
291 &&& m1.dom() =~~= m2.dom()
292 &&& forall|k: K| #![auto] m1.dom().contains(k) ==> m1[k] =~~= m2[k]
293 },
294{
295 axiom_map_ext_equal(m1, m2);
296}
297
298pub broadcast group group_map_axioms {
299 axiom_map_index_decreases_finite,
300 axiom_map_index_decreases_infinite,
301 axiom_map_empty,
302 axiom_map_insert_domain,
303 axiom_map_insert_same,
304 axiom_map_insert_different,
305 axiom_map_remove_domain,
306 axiom_map_remove_different,
307 axiom_map_ext_equal,
308 axiom_map_ext_equal_deep,
309}
310
311#[doc(hidden)]
313#[macro_export]
314macro_rules! map_internal {
315 [$($key:expr => $value:expr),* $(,)?] => {
316 $crate::vstd::map::Map::empty()
317 $(.insert($key, $value))*
318 }
319}
320
321#[macro_export]
328macro_rules! map {
329 [$($tail:tt)*] => {
330 ::builtin_macros::verus_proof_macro_exprs!($crate::vstd::map::map_internal!($($tail)*))
331 };
332}
333
334#[doc(hidden)]
335#[verifier::inline]
336pub open spec fn check_argument_is_map<K, V>(m: Map<K, V>) -> Map<K, V> {
337 m
338}
339
340#[doc(hidden)]
341pub use map_internal;
342pub use map;
343
344#[macro_export]
390macro_rules! assert_maps_equal {
391 [$($tail:tt)*] => {
392 ::builtin_macros::verus_proof_macro_exprs!($crate::vstd::map::assert_maps_equal_internal!($($tail)*))
393 };
394}
395
396#[macro_export]
397#[doc(hidden)]
398macro_rules! assert_maps_equal_internal {
399 (::builtin::spec_eq($m1:expr, $m2:expr)) => {
400 assert_maps_equal_internal!($m1, $m2)
401 };
402 (::builtin::spec_eq($m1:expr, $m2:expr), $k:ident $( : $t:ty )? => $bblock:block) => {
403 assert_maps_equal_internal!($m1, $m2, $k $( : $t )? => $bblock)
404 };
405 ($m1:expr, $m2:expr $(,)?) => {
406 assert_maps_equal_internal!($m1, $m2, key => { })
407 };
408 ($m1:expr, $m2:expr, $k:ident $( : $t:ty )? => $bblock:block) => {
409 #[verifier::spec] let m1 = $crate::vstd::map::check_argument_is_map($m1);
410 #[verifier::spec] let m2 = $crate::vstd::map::check_argument_is_map($m2);
411 ::builtin::assert_by(::builtin::equal(m1, m2), {
412 ::builtin::assert_forall_by(|$k $( : $t )?| {
413 ::builtin::ensures([
416 ::builtin::imply(#[verifier::trigger] m1.dom().contains($k), m2.dom().contains($k))
417 && ::builtin::imply(m2.dom().contains($k), m1.dom().contains($k))
418 && ::builtin::imply(m1.dom().contains($k) && m2.dom().contains($k),
419 ::builtin::equal(m1.index($k), m2.index($k)))
420 ]);
421 { $bblock }
422 });
423 ::builtin::assert_(::builtin::ext_equal(m1, m2));
424 });
425 }
426}
427
428#[doc(hidden)]
429pub use assert_maps_equal_internal;
430pub use assert_maps_equal;
431
432impl<K, V> Map<K, V> {
433 pub proof fn tracked_map_keys_in_place(
434 #[verifier::proof]
435 &mut self,
436 key_map: Map<K, K>,
437 )
438 requires
439 forall|j|
440 #![auto]
441 key_map.dom().contains(j) ==> old(self).dom().contains(key_map.index(j)),
442 forall|j1, j2|
443 #![auto]
444 j1 != j2 && key_map.dom().contains(j1) && key_map.dom().contains(j2)
445 ==> key_map.index(j1) != key_map.index(j2),
446 ensures
447 forall|j| #[trigger] self.dom().contains(j) == key_map.dom().contains(j),
448 forall|j|
449 key_map.dom().contains(j) ==> self.dom().contains(j) && #[trigger] self.index(j)
450 == old(self).index(key_map.index(j)),
451 {
452 #[verifier::proof]
453 let mut tmp = Self::tracked_empty();
454 super::modes::tracked_swap(&mut tmp, self);
455 #[verifier::proof]
456 let mut tmp = Self::tracked_map_keys(tmp, key_map);
457 super::modes::tracked_swap(&mut tmp, self);
458 }
459}
460
461}