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>(tracked m: &mut Map<K, V>, key: K) -> (tracked v: &mut V)
290    requires
291        old(m).dom().contains(key),
292    ensures
293        *v === old(m).index(key),
294        final(m).dom() === old(m).dom(),
295        forall|k: K| k != key ==> #[trigger] final(m).index(k) === old(m).index(k),
296        final(m).index(key) === *final(v),
297;
298
299/// Same as [`tracked_borrow_mut`] for `PointsTo<R, T>` values, with the
300/// additional open-spec equalities that Verus cannot derive through
301/// `simple_pptr::PointsTo`'s opaque fields.
302pub axiom fn tracked_borrow_mut_points_to<K, R, T: crate::cast_ptr::Repr<R>>(
303    tracked m: &mut Map<K, crate::cast_ptr::PointsTo<R, T>>,
304    key: K,
305) -> (tracked v: &mut crate::cast_ptr::PointsTo<R, T>)
306    requires
307        old(m).dom().contains(key),
308    ensures
309        *v === old(m).index(key),
310        // Open-spec equalities that don't fall out of `*v === old_v` because
311        // the inner `simple_pptr::PointsTo<R>` is external_body.
312        v.pptr() === old(m).index(key).pptr(),
313        v.addr() === old(m).index(key).addr(),
314        v.is_init() == old(m).index(key).is_init(),
315        v.wf(&v.inner_perms) == old(m).index(key).wf(&old(m).index(key).inner_perms),
316        v.inner_perms === old(m).index(key).inner_perms,
317        final(m).dom() === old(m).dom(),
318        forall|k: K| k != key ==> #[trigger] final(m).index(k) === old(m).index(k),
319        final(m).index(key) === *final(v),
320        final(m).index(key).pptr() === final(v).pptr(),
321        final(m).index(key).is_init() == final(v).is_init(),
322        final(m).index(key).wf(&final(v).inner_perms) == final(v).wf(&final(v).inner_perms),
323;
324
325} // verus!
326verus! {
327
328/// Returns true if predicate `f(k,v)` holds for all `(k,v)` in `map`.
329pub open spec fn forall_map<K, V>(map: Map<K, V>, f: spec_fn(K, V) -> bool) -> bool {
330    forall|k| #[trigger] map.contains_key(k) ==> f(k, map[k])
331}
332
333/// Returns true if predicate `f(v)` holds for all values in `map`.
334pub open spec fn forall_map_values<K, V>(map: Map<K, V>, f: spec_fn(V) -> bool) -> bool {
335    forall|k| #[trigger] map.contains_key(k) ==> f(map[k])
336}
337
338pub broadcast group group_forall_map_lemmas {
339    lemma_forall_map_insert,
340    lemma_forall_map_values_insert,
341    lemma_forall_map_remove,
342    lemma_forall_map_values_remove,
343}
344
345/// For any key in the map, `f(k, map[k])` holds if `forall_map(map, f)` holds.
346pub proof fn lemma_forall_map_entry<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
347    requires
348        forall_map(m, f),
349        m.contains_key(k),
350    ensures
351        f(k, m[k]),
352{
353}
354
355/// For any key in the map, `f(map[k])` holds if `forall_map_values(map, f)` holds.
356pub proof fn lemma_forall_map_values_entry<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
357    requires
358        forall_map_values(m, f),
359        m.contains_key(k),
360    ensures
361        f(m[k]),
362{
363}
364
365/// `forall_map(m.insert(k, v), f)` holds if `f(k, v)` holds and
366/// `forall_map(m.remove(k),f)` (if `m` contains `k`) or `forall_map(m, f)` (if `m` does not contain `k`).
367pub broadcast proof fn lemma_forall_map_insert<K, V>(
368    m: Map<K, V>,
369    f: spec_fn(K, V) -> bool,
370    k: K,
371    v: V,
372)
373    ensures
374        #[trigger] forall_map(m.insert(k, v), f) ==> f(k, v) && if m.contains_key(k) {
375            forall_map(m.remove(k), f)
376        } else {
377            forall_map(m, f)
378        },
379{
380    assert(m.insert(k, v).contains_key(k));
381    if m.contains_key(k) {
382        assert(m.insert(k, v) == m.remove(k).insert(k, v));
383    } else {
384        assert(m.insert(k, v) == m.insert(k, v));
385    }
386    if forall_map(m.insert(k, v), f) {
387        if m.contains_key(k) {
388        } else {
389            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
390        }
391    }
392}
393
394/// `forall_map_values(m.insert(k, v), f)` holds if `f(v)` holds and
395/// `forall_map_values(m.remove(k),f)` (if `m` contains `k`) or `forall_map_values(m, f)` (if `m` does not contain `k`).
396pub broadcast proof fn lemma_forall_map_values_insert<K, V>(
397    m: Map<K, V>,
398    f: spec_fn(V) -> bool,
399    k: K,
400    v: V,
401)
402    ensures
403        #[trigger] forall_map_values(m.insert(k, v), f) ==> f(v) && if m.contains_key(k) {
404            forall_map_values(m.remove(k), f)
405        } else {
406            forall_map_values(m, f)
407        },
408{
409    assert(m.insert(k, v).contains_key(k));
410    if m.contains_key(k) {
411        assert(m.insert(k, v) == m.remove(k).insert(k, v));
412    } else {
413        assert(m.insert(k, v) == m.insert(k, v));
414    }
415    if forall_map_values(m.insert(k, v), f) {
416        if m.contains_key(k) {
417        } else {
418            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
419        }
420    }
421}
422
423/// `forall_map(m,f)` holds if `forall_map(m.remove(k), f)` holds and
424/// `f(k, m[k])` holds (if `m` contains `k`).
425pub broadcast proof fn lemma_forall_map_remove<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
426    ensures
427        forall_map(m, f) <==> #[trigger] forall_map(m.remove(k), f) && (m.contains_key(k) ==> f(
428            k,
429            m[k],
430        )),
431{
432    if m.contains_key(k) {
433        assert(m == m.remove(k).insert(k, m[k]));
434    } else {
435        assert(m == m.remove(k));
436    }
437}
438
439/// `forall_map_values(m,f)` holds if `forall_map_values(m.remove(k), f)` holds and
440/// `f(m[k])` holds (if `m` contains `k`).
441pub broadcast proof fn lemma_forall_map_values_remove<K, V>(
442    m: Map<K, V>,
443    f: spec_fn(V) -> bool,
444    k: K,
445)
446    ensures
447        forall_map_values(m, f) <==> #[trigger] forall_map_values(m.remove(k), f) && (
448        m.contains_key(k) ==> f(m[k])),
449{
450    if m.contains_key(k) {
451        assert(m == m.remove(k).insert(k, m[k]));
452    } else {
453        assert(m == m.remove(k));
454    }
455
456}
457
458/// Returns a new map that projects the first key of a pair `(K1, K2)`,
459/// keeping the values associated with the second key `K2`.
460pub open spec fn project_first_key<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1) -> Map<K2, V> {
461    Map::new(|k2: K2| m.contains_key((k1, k2)), |k2: K2| m[(k1, k2)])
462}
463
464/// Returns a new map that projects the second key of a pair `(K1, K2)`,
465/// keeping the values associated with the first key `K1`.
466pub open spec fn project_second_key<K1, K2, V>(m: Map<(K1, K2), V>, k2: K2) -> Map<K1, V> {
467    Map::new(|k1: K1| m.contains_key((k1, k2)), |k1: K1| m[(k1, k2)])
468}
469
470/// A lemma showing that `project_first_key`` is sound.
471/// There is no need to actually use this lemma in practice at most of the time because Verus can automatically prove it.
472pub proof fn lemma_project_first_key_sound<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
473    ensures
474        forall|k2: K2|
475            {
476                &&& #[trigger] project_first_key(m, k1).contains_key(k2) <==> m.contains_key(
477                    (k1, k2),
478                )
479                &&& project_first_key(m, k1).contains_key(k2) ==> project_first_key(m, k1)[k2]
480                    == m[(k1, k2)]
481            },
482{
483}
484
485/// If the value filter of the projected map is non-empty, then there exists a key `k2`
486/// such that the original map contains the pair `(k1, k2)` and `m[(k1, k2)]` satisfies the predicate `f`.
487pub proof fn lemma_project_first_key_value_filter_non_empty<K1, K2, V>(
488    m: Map<(K1, K2), V>,
489    k1: K1,
490    f: spec_fn(V) -> bool,
491)
492    requires
493        value_filter(project_first_key(m, k1), f).len() != 0,
494    ensures
495        exists|k2: K2| #[trigger]
496            project_first_key(m, k1).contains_key(k2) && f(project_first_key(m, k1)[k2]),
497{
498    lemma_value_filter_choose(project_first_key(m, k1), f);
499    let k2 = value_filter_choose(project_first_key(m, k1), f);
500    assert(project_first_key(m, k1).contains_key(k2) && f(m[(k1, k2)]));
501}
502
503pub proof fn lemma_project_first_key_value_filter_empty<K1, K2, V>(
504    m: Map<(K1, K2), V>,
505    k1: K1,
506    f: spec_fn(V) -> bool,
507)
508    requires
509        m.dom().finite(),
510        value_filter(project_first_key(m, k1), f).len() == 0,
511    ensures
512        forall|k2: K2| #[trigger]
513            project_first_key(m, k1).contains_key(k2) ==> !f(project_first_key(m, k1)[k2]),
514{
515    assert forall|k2: K2| #[trigger] project_first_key(m, k1).contains_key(k2) implies !f(
516        project_first_key(m, k1)[k2],
517    ) by {
518        if f(project_first_key(m, k1)[k2]) {
519            assert(value_filter(project_first_key(m, k1), f).dom().contains(k2));
520            lemma_project_first_key_finite(m, k1);
521            lemma_value_filter_finite(project_first_key(m, k1), f);
522            Set::lemma_len0_is_empty(value_filter(project_first_key(m, k1), f).dom());
523            assert(false);
524        }
525    }
526}
527
528/// If the original map is finite, then the projected map is also finite.
529pub proof fn lemma_project_first_key_finite<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
530    requires
531        m.dom().finite(),
532    ensures
533        project_first_key(m, k1).dom().finite(),
534    decreases m.dom().len(),
535{
536    if m.dom().len() == 0 {
537        assert(project_first_key(m, k1).dom() == Set::<K2>::empty());
538    } else {
539        let pair = m.dom().choose();
540        lemma_project_first_key_finite(m.remove(pair), k1);
541        if pair.0 != k1 {
542            assert(project_first_key(m, k1) == project_first_key(m.remove(pair), k1));
543        } else {
544            assert(project_first_key(m, k1).dom() == project_first_key(
545                m.remove(pair),
546                k1,
547            ).dom().insert(pair.1));
548        }
549    }
550}
551
552} // verus!
vstd_extra/map_extra.rs

vstd_extra/
map_extra.rs
