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} // verus!
281verus! {
282
283/// Returns true if predicate `f(k,v)` holds for all `(k,v)` in `map`.
284pub open spec fn forall_map<K, V>(map: Map<K, V>, f: spec_fn(K, V) -> bool) -> bool {
285    forall|k| #[trigger] map.contains_key(k) ==> f(k, map[k])
286}
287
288/// Returns true if predicate `f(v)` holds for all values in `map`.
289pub open spec fn forall_map_values<K, V>(map: Map<K, V>, f: spec_fn(V) -> bool) -> bool {
290    forall|k| #[trigger] map.contains_key(k) ==> f(map[k])
291}
292
293pub broadcast group group_forall_map_lemmas {
294    lemma_forall_map_insert,
295    lemma_forall_map_values_insert,
296    lemma_forall_map_remove,
297    lemma_forall_map_values_remove,
298}
299
300/// For any key in the map, `f(k, map[k])` holds if `forall_map(map, f)` holds.
301pub proof fn lemma_forall_map_entry<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
302    requires
303        forall_map(m, f),
304        m.contains_key(k),
305    ensures
306        f(k, m[k]),
307{
308}
309
310/// For any key in the map, `f(map[k])` holds if `forall_map_values(map, f)` holds.
311pub proof fn lemma_forall_map_values_entry<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
312    requires
313        forall_map_values(m, f),
314        m.contains_key(k),
315    ensures
316        f(m[k]),
317{
318}
319
320/// `forall_map(m.insert(k, v), f)` holds if `f(k, v)` holds and
321/// `forall_map(m.remove(k),f)` (if `m` contains `k`) or `forall_map(m, f)` (if `m` does not contain `k`).
322pub broadcast proof fn lemma_forall_map_insert<K, V>(
323    m: Map<K, V>,
324    f: spec_fn(K, V) -> bool,
325    k: K,
326    v: V,
327)
328    ensures
329        #[trigger] forall_map(m.insert(k, v), f) ==> f(k, v) && if m.contains_key(k) {
330            forall_map(m.remove(k), f)
331        } else {
332            forall_map(m, f)
333        },
334{
335    assert(m.insert(k, v).contains_key(k));
336    if m.contains_key(k) {
337        assert(m.insert(k, v) == m.remove(k).insert(k, v));
338    } else {
339        assert(m.insert(k, v) == m.insert(k, v));
340    }
341    if forall_map(m.insert(k, v), f) {
342        if m.contains_key(k) {
343        } else {
344            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
345        }
346    }
347}
348
349/// `forall_map_values(m.insert(k, v), f)` holds if `f(v)` holds and
350/// `forall_map_values(m.remove(k),f)` (if `m` contains `k`) or `forall_map_values(m, f)` (if `m` does not contain `k`).
351pub broadcast proof fn lemma_forall_map_values_insert<K, V>(
352    m: Map<K, V>,
353    f: spec_fn(V) -> bool,
354    k: K,
355    v: V,
356)
357    ensures
358        #[trigger] forall_map_values(m.insert(k, v), f) ==> f(v) && if m.contains_key(k) {
359            forall_map_values(m.remove(k), f)
360        } else {
361            forall_map_values(m, f)
362        },
363{
364    assert(m.insert(k, v).contains_key(k));
365    if m.contains_key(k) {
366        assert(m.insert(k, v) == m.remove(k).insert(k, v));
367    } else {
368        assert(m.insert(k, v) == m.insert(k, v));
369    }
370    if forall_map_values(m.insert(k, v), f) {
371        if m.contains_key(k) {
372        } else {
373            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
374        }
375    }
376}
377
378/// `forall_map(m,f)` holds if `forall_map(m.remove(k), f)` holds and
379/// `f(k, m[k])` holds (if `m` contains `k`).
380pub broadcast proof fn lemma_forall_map_remove<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
381    ensures
382        forall_map(m, f) <==> #[trigger] forall_map(m.remove(k), f) && (m.contains_key(k) ==> f(
383            k,
384            m[k],
385        )),
386{
387    if m.contains_key(k) {
388        assert(m == m.remove(k).insert(k, m[k]));
389    } else {
390        assert(m == m.remove(k));
391    }
392}
393
394/// `forall_map_values(m,f)` holds if `forall_map_values(m.remove(k), f)` holds and
395/// `f(m[k])` holds (if `m` contains `k`).
396pub broadcast proof fn lemma_forall_map_values_remove<K, V>(
397    m: Map<K, V>,
398    f: spec_fn(V) -> bool,
399    k: K,
400)
401    ensures
402        forall_map_values(m, f) <==> #[trigger] forall_map_values(m.remove(k), f) && (
403        m.contains_key(k) ==> f(m[k])),
404{
405    if m.contains_key(k) {
406        assert(m == m.remove(k).insert(k, m[k]));
407    } else {
408        assert(m == m.remove(k));
409    }
410
411}
412
413/// Returns a new map that projects the first key of a pair `(K1, K2)`,
414/// keeping the values associated with the second key `K2`.
415pub open spec fn project_first_key<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1) -> Map<K2, V> {
416    Map::new(|k2: K2| m.contains_key((k1, k2)), |k2: K2| m[(k1, k2)])
417}
418
419/// Returns a new map that projects the second key of a pair `(K1, K2)`,
420/// keeping the values associated with the first key `K1`.
421pub open spec fn project_second_key<K1, K2, V>(m: Map<(K1, K2), V>, k2: K2) -> Map<K1, V> {
422    Map::new(|k1: K1| m.contains_key((k1, k2)), |k1: K1| m[(k1, k2)])
423}
424
425/// A lemma showing that `project_first_key`` is sound.
426/// There is no need to actually use this lemma in practice at most of the time because Verus can automatically prove it.
427pub proof fn lemma_project_first_key_sound<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
428    ensures
429        forall|k2: K2|
430            {
431                &&& #[trigger] project_first_key(m, k1).contains_key(k2) <==> m.contains_key(
432                    (k1, k2),
433                )
434                &&& project_first_key(m, k1).contains_key(k2) ==> project_first_key(m, k1)[k2]
435                    == m[(k1, k2)]
436            },
437{
438}
439
440/// If the value filter of the projected map is non-empty, then there exists a key `k2`
441/// such that the original map contains the pair `(k1, k2)` and `m[(k1, k2)]` satisfies the predicate `f`.
442pub proof fn lemma_project_first_key_value_filter_non_empty<K1, K2, V>(
443    m: Map<(K1, K2), V>,
444    k1: K1,
445    f: spec_fn(V) -> bool,
446)
447    requires
448        value_filter(project_first_key(m, k1), f).len() != 0,
449    ensures
450        exists|k2: K2| #[trigger]
451            project_first_key(m, k1).contains_key(k2) && f(project_first_key(m, k1)[k2]),
452{
453    lemma_value_filter_choose(project_first_key(m, k1), f);
454    let k2 = value_filter_choose(project_first_key(m, k1), f);
455    assert(project_first_key(m, k1).contains_key(k2) && f(m[(k1, k2)]));
456}
457
458pub proof fn lemma_project_first_key_value_filter_empty<K1, K2, V>(
459    m: Map<(K1, K2), V>,
460    k1: K1,
461    f: spec_fn(V) -> bool,
462)
463    requires
464        m.dom().finite(),
465        value_filter(project_first_key(m, k1), f).len() == 0,
466    ensures
467        forall|k2: K2| #[trigger]
468            project_first_key(m, k1).contains_key(k2) ==> !f(project_first_key(m, k1)[k2]),
469{
470    assert forall|k2: K2| #[trigger] project_first_key(m, k1).contains_key(k2) implies !f(
471        project_first_key(m, k1)[k2],
472    ) by {
473        if f(project_first_key(m, k1)[k2]) {
474            assert(value_filter(project_first_key(m, k1), f).dom().contains(k2));
475            lemma_project_first_key_finite(m, k1);
476            lemma_value_filter_finite(project_first_key(m, k1), f);
477            Set::lemma_len0_is_empty(value_filter(project_first_key(m, k1), f).dom());
478            assert(false);
479        }
480    }
481}
482
483/// If the original map is finite, then the projected map is also finite.
484pub proof fn lemma_project_first_key_finite<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
485    requires
486        m.dom().finite(),
487    ensures
488        project_first_key(m, k1).dom().finite(),
489    decreases m.dom().len(),
490{
491    if m.dom().len() == 0 {
492        assert(project_first_key(m, k1).dom() == Set::<K2>::empty());
493    } else {
494        let pair = m.dom().choose();
495        lemma_project_first_key_finite(m.remove(pair), k1);
496        if pair.0 != k1 {
497            assert(project_first_key(m, k1) == project_first_key(m.remove(pair), k1));
498        } else {
499            assert(project_first_key(m, k1).dom() == project_first_key(
500                m.remove(pair),
501                k1,
502            ).dom().insert(pair.1));
503        }
504    }
505}
506
507} // verus!
vstd_extra/map_extra.rs

vstd_extra/
map_extra.rs
