vstd_extra/
map_extra.rs

1//! Extra properties of [`vstd::map::Map`](https://verus-lang.github.io/verus/verusdoc/vstd/map/struct.Map.html).
2use vstd::prelude::*;
3use vstd::{map::*, set::*};
4
5verus! {
6
7broadcast use {group_map_axioms, group_set_axioms};
8
9pub broadcast proof fn lemma_map_remove_keys_finite<K, V>(m: Map<K, V>, keys: Set<K>)
10    requires
11        m.dom().finite(),
12        keys.finite(),
13    ensures
14        (#[trigger] m.remove_keys(keys)).dom().finite(),
15{
16    assert(m.remove_keys(keys).dom() =~= m.dom().difference(keys));
17}
18
19pub broadcast group group_map_remove_keys_lemmas {
20    lemma_map_remove_keys_finite,
21}
22
23/// The length of inserting a key-value pair `(k,v)` into a map `m` depends on whether
24/// the key `k` already exists in the map. If it does, the length remains the same;
25/// if it doesn't, the length increases by 1.
26pub proof fn lemma_map_insert_len<K, V>(m: Map<K, V>, k: K, v: V)
27    requires
28        m.dom().finite(),
29    ensures
30        #[trigger] m.insert(k, v).len() == m.len() + (if m.contains_key(k) {
31            0int
32        } else {
33            1
34        }),
35{
36    axiom_map_insert_domain(m, k, v)
37}
38
39/// The length of removing a key-value pair `(k,v)` from a map `m` depends on whether
40/// the key `k` exists in the map. If it does, the length decreases by 1; if it doesn't,
41/// the length remains the same.
42pub proof fn lemma_map_remove_len<K, V>(m: Map<K, V>, k: K)
43    requires
44        m.dom().finite(),
45    ensures
46        m.len() == #[trigger] m.remove(k).len() + (if m.contains_key(k) {
47            1
48        } else {
49            0int
50        }),
51{
52    axiom_map_remove_domain(m, k)
53}
54
55/// Filters a map based on a predicate function applied to its values.
56pub open spec fn value_filter<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool) -> Map<K, V> {
57    m.restrict(m.dom().filter(|s| f(m[s])))
58}
59
60pub open spec fn value_filter_choose<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool) -> K {
61    choose|k: K| value_filter(m, f).contains_key(k)
62}
63
64pub broadcast group group_value_filter_lemmas {
65    lemma_value_filter_finite,
66    lemma_value_filter_choose,
67    lemma_insert_value_filter_same_len,
68    lemma_insert_value_filter_different_len_contains,
69    lemma_insert_value_filter_different_len_not_contains,
70}
71
72/// The result of value-filtering a finite map is also finite.
73pub broadcast proof fn lemma_value_filter_finite<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool)
74    requires
75        m.dom().finite(),
76    ensures
77        #[trigger] value_filter(m, f).dom().finite(),
78{
79    assert(value_filter(m, f).dom() == m.dom().filter(|s| f(m[s])));
80    m.dom().lemma_len_filter(|s| f(m[s]));
81}
82
83/// If a key `k` exists in the map `m`, then whether the value-filtered map
84/// contains the key depends on whether the predicate function `f` is true for
85/// its value.
86pub proof fn lemma_value_filter_contains<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
87    requires
88        m.contains_key(k),
89    ensures
90        if f(m[k]) {
91            value_filter(m, f).contains_key(k)
92        } else {
93            !value_filter(m, f).contains_key(k)
94        },
95{
96}
97
98/// If the predicate function `f` is true for all values in the map `m`, then
99/// the value-filtered map is equal to the original map.
100pub proof fn lemma_value_filter_all_true<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool)
101    requires
102        forall|k: K| m.contains_key(k) ==> #[trigger] f(m[k]),
103    ensures
104        value_filter(m, f) =~= m,
105{
106}
107
108/// If the predicate function `f` is false for all values in the map `m`, then
109/// the value-filtered map is empty.
110pub proof fn lemma_value_filter_all_false<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool)
111    ensures
112        value_filter(m, f).is_empty() <==> forall|k: K| m.contains_key(k) ==> !#[trigger] f(m[k]),
113{
114    if value_filter(m, f).is_empty() {
115        assert forall|k: K| m.contains_key(k) implies !#[trigger] f(m[k]) by {
116            if f(m[k]) {
117                assert(value_filter(m, f).contains_key(k));
118            }
119        }
120    }
121}
122
123/// If the predicate function `f` is true for `m[k]`, then fist removing `k`
124/// from the map `m` and then applying the value filter is equivalent to
125/// applying the value filter first and then removing `k` from the result.
126pub proof fn lemma_remove_value_filter_true<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
127    requires
128        f(m[k]),
129    ensures
130        value_filter(m.remove(k), f) =~= value_filter(m, f).remove(k),
131{
132}
133
134/// If the predicate function `f` is false for `m[k]`, then first removing `k`
135/// from the map `m` and then applying the value filter is equivalent to
136/// directly applying the value filter to the original map `m`.
137pub proof fn lemma_remove_value_filter_false<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
138    requires
139        !f(m[k]),
140    ensures
141        value_filter(m.remove(k), f) =~= value_filter(m, f),
142{
143}
144
145/// If the predicate function `f` is true for the newly inserted value `v`,
146/// then inserting `(k,v)` into the map `m` and then applying the value filter
147/// is equivalent to applying the value filter to the original map `m` and
148/// then inserting `(k,v)` into the result.
149pub proof fn lemma_insert_value_filter_true<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K, v: V)
150    requires
151        f(v),
152    ensures
153        value_filter(m.insert(k, v), f) =~= value_filter(m, f).insert(k, v),
154{
155}
156
157/// If the predicate function `f` is false for the newly inserted value `v`,
158/// then inserting `(k,v)` into the map `m` and then applying the value filter
159/// is equivalent to applying the value filter to the original map `m` and
160/// then removing `k` from the result (if `k` exists in `m`) or leaving it unchanged
161/// (if it doesn't).
162pub proof fn lemma_insert_value_filter_false<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K, v: V)
163    requires
164        !f(v),
165    ensures
166        value_filter(m.insert(k, v), f) =~= if m.contains_key(k) {
167            value_filter(m, f).remove(k)
168        } else {
169            value_filter(m, f)
170        },
171        value_filter(m.insert(k, v), f) =~= if m.contains_key(k) {
172            value_filter(m, f).remove(k)
173        } else {
174            value_filter(m, f)
175        },
176{
177}
178
179/// The length of the value-filtered map after inserting `(k,v)` into `m`
180/// is equal to the length of the value-filtered map for the original map `m`
181/// if `k` exists in `m`, and `m[k]` and `v` both satisfy/un-satisfy the predicate
182/// function `f`.
183pub broadcast proof fn lemma_insert_value_filter_same_len<K, V>(
184    m: Map<K, V>,
185    f: spec_fn(V) -> bool,
186    k: K,
187    v: V,
188)
189    requires
190        m.dom().finite(),
191        m.contains_key(k) && f(m[k]) == f(v) || !m.contains_key(k) && !f(v),
192    ensures
193        #[trigger] value_filter(m.insert(k, v), f).len() == value_filter(m, f).len(),
194{
195    lemma_value_filter_finite(m, f);
196    if f(v) {
197        lemma_insert_value_filter_true(m, f, k, v);
198        lemma_map_insert_len(value_filter(m, f), k, v);
199    } else {
200        lemma_insert_value_filter_false(m, f, k, v);
201        lemma_map_remove_len(value_filter(m, f), k);
202    }
203}
204
205/// The length of the value-filtered map after inserting `(k,v)` into `m`
206/// is equal to the length of the value-filtered map for the original map `m`
207/// plus one if `m[k]` does not satisfy `f` but `v` does, and minus one if
208/// `m[k]` satisfies `f` but `v` does not.
209pub broadcast proof fn lemma_insert_value_filter_different_len_contains<K, V>(
210    m: Map<K, V>,
211    f: spec_fn(V) -> bool,
212    k: K,
213    v: V,
214)
215    requires
216        m.dom().finite(),
217        m.contains_key(k),
218        f(m[k]) != f(v),
219    ensures
220        #[trigger] value_filter(m.insert(k, v), f).len() == value_filter(m, f).len() + if f(v) {
221            1
222        } else {
223            -1
224        },
225{
226    lemma_value_filter_finite(m, f);
227    if f(v) {
228        lemma_insert_value_filter_true(m, f, k, v);
229        lemma_map_insert_len(m, k, v);
230    } else {
231        lemma_insert_value_filter_false(m, f, k, v);
232        assert(value_filter(m.insert(k, v), f).len() == value_filter(m, f).remove(k).len());
233        lemma_map_remove_len(value_filter(m, f), k);
234    }
235}
236
237/// The length of the value-filtered map after inserting `(k,v)` into `m`
238/// is equal to the length of the value-filtered map for the original map `m`
239/// plus one if `k` does not exist in `m` and `v` satisfies the predicate function `f`.
240pub broadcast proof fn lemma_insert_value_filter_different_len_not_contains<K, V>(
241    m: Map<K, V>,
242    f: spec_fn(V) -> bool,
243    k: K,
244    v: V,
245)
246    requires
247        m.dom().finite(),
248        !m.contains_key(k),
249        f(v),
250    ensures
251        #[trigger] value_filter(m.insert(k, v), f).len() == value_filter(m, f).len() + 1,
252{
253    lemma_value_filter_finite(m, f);
254    lemma_insert_value_filter_true(m, f, k, v);
255    lemma_map_insert_len(m, k, v);
256}
257
258pub proof fn lemma_value_filter_contains_key<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
259    requires
260        value_filter(m, f).contains_key(k),
261    ensures
262        m.contains_key(k),
263{
264}
265
266pub broadcast proof fn lemma_value_filter_choose<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool)
267    requires
268        value_filter(m, f).len() != 0,
269    ensures
270        value_filter(m, f).contains_key(#[trigger] value_filter_choose(m, f)),
271        f(m[value_filter_choose(m, f)]),
272{
273    if value_filter(m, f).dom().finite() {
274        axiom_set_choose_len(value_filter(m, f).dom());
275    } else {
276        axiom_set_choose_infinite(value_filter(m, f).dom());
277    }
278}
279
280/// Borrows an entry from a tracked `Map` mutably.
281///
282/// Returns `&mut v` where `v = old(m)[key]`. While the returned borrow is
283/// live, `m` is exclusively held; at its end, `m[key]` equals whatever `v`
284/// ended up being, and all other entries are unchanged.
285///
286/// This is the mutable counterpart to `Map::tracked_borrow` and mirrors
287/// `PointsTo::borrow_mut_inner_perms` in structure.
288// TODO: upstream to vstd.
289pub axiom fn tracked_borrow_mut<K, V>(
290    tracked m: &mut Map<K, V>,
291    key: K,
292) -> (tracked v: &mut V)
293    requires
294        old(m).dom().contains(key),
295    ensures
296        *v === old(m).index(key),
297        final(m).dom() === old(m).dom(),
298        forall|k: K| k != key ==> #[trigger] final(m).index(k) === old(m).index(k),
299        final(m).index(key) === *final(v);
300
301/// Same as [`tracked_borrow_mut`] for `PointsTo<R, T>` values, with the
302/// additional open-spec equalities that Verus cannot derive through
303/// `simple_pptr::PointsTo`'s opaque fields.
304pub axiom fn tracked_borrow_mut_points_to<K, R, T: crate::cast_ptr::Repr<R>>(
305    tracked m: &mut Map<K, crate::cast_ptr::PointsTo<R, T>>,
306    key: K,
307) -> (tracked v: &mut crate::cast_ptr::PointsTo<R, T>)
308    requires
309        old(m).dom().contains(key),
310    ensures
311        *v === old(m).index(key),
312        // Open-spec equalities that don't fall out of `*v === old_v` because
313        // the inner `simple_pptr::PointsTo<R>` is external_body.
314        v.pptr() === old(m).index(key).pptr(),
315        v.addr() === old(m).index(key).addr(),
316        v.is_init() == old(m).index(key).is_init(),
317        v.wf(&v.inner_perms) == old(m).index(key).wf(&old(m).index(key).inner_perms),
318        v.inner_perms === old(m).index(key).inner_perms,
319        final(m).dom() === old(m).dom(),
320        forall|k: K| k != key ==> #[trigger] final(m).index(k) === old(m).index(k),
321        final(m).index(key) === *final(v),
322        final(m).index(key).pptr() === final(v).pptr(),
323        final(m).index(key).is_init() == final(v).is_init(),
324        final(m).index(key).wf(&final(v).inner_perms)
325            == final(v).wf(&final(v).inner_perms);
326
327} // verus!
328verus! {
329
330/// Returns true if predicate `f(k,v)` holds for all `(k,v)` in `map`.
331pub open spec fn forall_map<K, V>(map: Map<K, V>, f: spec_fn(K, V) -> bool) -> bool {
332    forall|k| #[trigger] map.contains_key(k) ==> f(k, map[k])
333}
334
335/// Returns true if predicate `f(v)` holds for all values in `map`.
336pub open spec fn forall_map_values<K, V>(map: Map<K, V>, f: spec_fn(V) -> bool) -> bool {
337    forall|k| #[trigger] map.contains_key(k) ==> f(map[k])
338}
339
340pub broadcast group group_forall_map_lemmas {
341    lemma_forall_map_insert,
342    lemma_forall_map_values_insert,
343    lemma_forall_map_remove,
344    lemma_forall_map_values_remove,
345}
346
347/// For any key in the map, `f(k, map[k])` holds if `forall_map(map, f)` holds.
348pub proof fn lemma_forall_map_entry<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
349    requires
350        forall_map(m, f),
351        m.contains_key(k),
352    ensures
353        f(k, m[k]),
354{
355}
356
357/// For any key in the map, `f(map[k])` holds if `forall_map_values(map, f)` holds.
358pub proof fn lemma_forall_map_values_entry<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
359    requires
360        forall_map_values(m, f),
361        m.contains_key(k),
362    ensures
363        f(m[k]),
364{
365}
366
367/// `forall_map(m.insert(k, v), f)` holds if `f(k, v)` holds and
368/// `forall_map(m.remove(k),f)` (if `m` contains `k`) or `forall_map(m, f)` (if `m` does not contain `k`).
369pub broadcast proof fn lemma_forall_map_insert<K, V>(
370    m: Map<K, V>,
371    f: spec_fn(K, V) -> bool,
372    k: K,
373    v: V,
374)
375    ensures
376        #[trigger] forall_map(m.insert(k, v), f) ==> f(k, v) && if m.contains_key(k) {
377            forall_map(m.remove(k), f)
378        } else {
379            forall_map(m, f)
380        },
381{
382    assert(m.insert(k, v).contains_key(k));
383    if m.contains_key(k) {
384        assert(m.insert(k, v) == m.remove(k).insert(k, v));
385    } else {
386        assert(m.insert(k, v) == m.insert(k, v));
387    }
388    if forall_map(m.insert(k, v), f) {
389        if m.contains_key(k) {
390        } else {
391            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
392        }
393    }
394}
395
396/// `forall_map_values(m.insert(k, v), f)` holds if `f(v)` holds and
397/// `forall_map_values(m.remove(k),f)` (if `m` contains `k`) or `forall_map_values(m, f)` (if `m` does not contain `k`).
398pub broadcast proof fn lemma_forall_map_values_insert<K, V>(
399    m: Map<K, V>,
400    f: spec_fn(V) -> bool,
401    k: K,
402    v: V,
403)
404    ensures
405        #[trigger] forall_map_values(m.insert(k, v), f) ==> f(v) && if m.contains_key(k) {
406            forall_map_values(m.remove(k), f)
407        } else {
408            forall_map_values(m, f)
409        },
410{
411    assert(m.insert(k, v).contains_key(k));
412    if m.contains_key(k) {
413        assert(m.insert(k, v) == m.remove(k).insert(k, v));
414    } else {
415        assert(m.insert(k, v) == m.insert(k, v));
416    }
417    if forall_map_values(m.insert(k, v), f) {
418        if m.contains_key(k) {
419        } else {
420            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
421        }
422    }
423}
424
425/// `forall_map(m,f)` holds if `forall_map(m.remove(k), f)` holds and
426/// `f(k, m[k])` holds (if `m` contains `k`).
427pub broadcast proof fn lemma_forall_map_remove<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
428    ensures
429        forall_map(m, f) <==> #[trigger] forall_map(m.remove(k), f) && (m.contains_key(k) ==> f(
430            k,
431            m[k],
432        )),
433{
434    if m.contains_key(k) {
435        assert(m == m.remove(k).insert(k, m[k]));
436    } else {
437        assert(m == m.remove(k));
438    }
439}
440
441/// `forall_map_values(m,f)` holds if `forall_map_values(m.remove(k), f)` holds and
442/// `f(m[k])` holds (if `m` contains `k`).
443pub broadcast proof fn lemma_forall_map_values_remove<K, V>(
444    m: Map<K, V>,
445    f: spec_fn(V) -> bool,
446    k: K,
447)
448    ensures
449        forall_map_values(m, f) <==> #[trigger] forall_map_values(m.remove(k), f) && (
450        m.contains_key(k) ==> f(m[k])),
451{
452    if m.contains_key(k) {
453        assert(m == m.remove(k).insert(k, m[k]));
454    } else {
455        assert(m == m.remove(k));
456    }
457
458}
459
460/// Returns a new map that projects the first key of a pair `(K1, K2)`,
461/// keeping the values associated with the second key `K2`.
462pub open spec fn project_first_key<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1) -> Map<K2, V> {
463    Map::new(|k2: K2| m.contains_key((k1, k2)), |k2: K2| m[(k1, k2)])
464}
465
466/// Returns a new map that projects the second key of a pair `(K1, K2)`,
467/// keeping the values associated with the first key `K1`.
468pub open spec fn project_second_key<K1, K2, V>(m: Map<(K1, K2), V>, k2: K2) -> Map<K1, V> {
469    Map::new(|k1: K1| m.contains_key((k1, k2)), |k1: K1| m[(k1, k2)])
470}
471
472/// A lemma showing that `project_first_key`` is sound.
473/// There is no need to actually use this lemma in practice at most of the time because Verus can automatically prove it.
474pub proof fn lemma_project_first_key_sound<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
475    ensures
476        forall|k2: K2|
477            {
478                &&& #[trigger] project_first_key(m, k1).contains_key(k2) <==> m.contains_key(
479                    (k1, k2),
480                )
481                &&& project_first_key(m, k1).contains_key(k2) ==> project_first_key(m, k1)[k2]
482                    == m[(k1, k2)]
483            },
484{
485}
486
487/// If the value filter of the projected map is non-empty, then there exists a key `k2`
488/// such that the original map contains the pair `(k1, k2)` and `m[(k1, k2)]` satisfies the predicate `f`.
489pub proof fn lemma_project_first_key_value_filter_non_empty<K1, K2, V>(
490    m: Map<(K1, K2), V>,
491    k1: K1,
492    f: spec_fn(V) -> bool,
493)
494    requires
495        value_filter(project_first_key(m, k1), f).len() != 0,
496    ensures
497        exists|k2: K2| #[trigger]
498            project_first_key(m, k1).contains_key(k2) && f(project_first_key(m, k1)[k2]),
499{
500    lemma_value_filter_choose(project_first_key(m, k1), f);
501    let k2 = value_filter_choose(project_first_key(m, k1), f);
502    assert(project_first_key(m, k1).contains_key(k2) && f(m[(k1, k2)]));
503}
504
505pub proof fn lemma_project_first_key_value_filter_empty<K1, K2, V>(
506    m: Map<(K1, K2), V>,
507    k1: K1,
508    f: spec_fn(V) -> bool,
509)
510    requires
511        m.dom().finite(),
512        value_filter(project_first_key(m, k1), f).len() == 0,
513    ensures
514        forall|k2: K2| #[trigger]
515            project_first_key(m, k1).contains_key(k2) ==> !f(project_first_key(m, k1)[k2]),
516{
517    assert forall|k2: K2| #[trigger] project_first_key(m, k1).contains_key(k2) implies !f(
518        project_first_key(m, k1)[k2],
519    ) by {
520        if f(project_first_key(m, k1)[k2]) {
521            assert(value_filter(project_first_key(m, k1), f).dom().contains(k2));
522            lemma_project_first_key_finite(m, k1);
523            lemma_value_filter_finite(project_first_key(m, k1), f);
524            Set::lemma_len0_is_empty(value_filter(project_first_key(m, k1), f).dom());
525            assert(false);
526        }
527    }
528}
529
530/// If the original map is finite, then the projected map is also finite.
531pub proof fn lemma_project_first_key_finite<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
532    requires
533        m.dom().finite(),
534    ensures
535        project_first_key(m, k1).dom().finite(),
536    decreases m.dom().len(),
537{
538    if m.dom().len() == 0 {
539        assert(project_first_key(m, k1).dom() == Set::<K2>::empty());
540    } else {
541        let pair = m.dom().choose();
542        lemma_project_first_key_finite(m.remove(pair), k1);
543        if pair.0 != k1 {
544            assert(project_first_key(m, k1) == project_first_key(m.remove(pair), k1));
545        } else {
546            assert(project_first_key(m, k1).dom() == project_first_key(
547                m.remove(pair),
548                k1,
549            ).dom().insert(pair.1));
550        }
551    }
552}
553
554} // verus!
vstd_extra/map_extra.rs

vstd_extra/
map_extra.rs
