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
7/// The length of inserting a key-value pair `(k,v)` into a map `m` depends on whether
8/// the key `k` already exists in the map. If it does, the length remains the same;
9/// if it doesn't, the length increases by 1.
10pub proof fn lemma_map_insert_len<K, V>(m: Map<K, V>, k: K, v: V)
11    ensures
12        #[trigger] m.insert(k, v).len() == m.len() + (if m.contains_key(k) {
13            0int
14        } else {
15            1
16        }),
17{
18    lemma_map_insert_domain(m, k, v)
19}
20
21/// The length of removing a key-value pair `(k,v)` from a map `m` depends on whether
22/// the key `k` exists in the map. If it does, the length decreases by 1; if it doesn't,
23/// the length remains the same.
24pub proof fn lemma_map_remove_len<K, V>(m: Map<K, V>, k: K)
25    ensures
26        m.len() == #[trigger] m.remove(k).len() + (if m.contains_key(k) {
27            1
28        } else {
29            0int
30        }),
31{
32    lemma_map_remove_domain(m, k)
33}
34
35/// Filters a map based on a predicate function applied to its values.
36pub open spec fn value_filter<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool) -> Map<K, V> {
37    m.restrict(m.dom().filter(|s| f(m[s])))
38}
39
40pub open spec fn value_filter_choose<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool) -> K {
41    choose|k: K| value_filter(m, f).contains_key(k)
42}
43
44pub broadcast group group_value_filter_lemmas {
45    lemma_value_filter_choose,
46    lemma_insert_value_filter_same_len,
47    lemma_insert_value_filter_different_len_contains,
48    lemma_insert_value_filter_different_len_not_contains,
49}
50
51/// If a key `k` exists in the map `m`, then whether the value-filtered map
52/// contains the key depends on whether the predicate function `f` is true for
53/// its value.
54pub proof fn lemma_value_filter_contains<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
55    requires
56        m.contains_key(k),
57    ensures
58        if f(m[k]) {
59            value_filter(m, f).contains_key(k)
60        } else {
61            !value_filter(m, f).contains_key(k)
62        },
63{
64}
65
66/// If the predicate function `f` is true for all values in the map `m`, then
67/// the value-filtered map is equal to the original map.
68pub proof fn lemma_value_filter_all_true<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool)
69    requires
70        forall|k: K| m.contains_key(k) ==> #[trigger] f(m[k]),
71    ensures
72        value_filter(m, f) == m,
73{
74}
75
76/// If the predicate function `f` is false for all values in the map `m`, then
77/// the value-filtered map is empty.
78pub proof fn lemma_value_filter_all_false<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool)
79    ensures
80        value_filter(m, f).is_empty() <==> forall|k: K| m.contains_key(k) ==> !#[trigger] f(m[k]),
81{
82    if value_filter(m, f).is_empty() {
83        assert forall|k: K| m.contains_key(k) implies !#[trigger] f(m[k]) by {
84            if f(m[k]) {
85                assert(value_filter(m, f).contains_key(k));
86            }
87        }
88    }
89}
90
91/// If the predicate function `f` is true for `m[k]`, then fist removing `k`
92/// from the map `m` and then applying the value filter is equivalent to
93/// applying the value filter first and then removing `k` from the result.
94pub proof fn lemma_remove_value_filter_true<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
95    requires
96        f(m[k]),
97    ensures
98        value_filter(m.remove(k), f) == value_filter(m, f).remove(k),
99{
100}
101
102/// If the predicate function `f` is false for `m[k]`, then first removing `k`
103/// from the map `m` and then applying the value filter is equivalent to
104/// directly applying the value filter to the original map `m`.
105pub proof fn lemma_remove_value_filter_false<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
106    requires
107        !f(m[k]),
108    ensures
109        value_filter(m.remove(k), f) == value_filter(m, f),
110{
111}
112
113/// If the predicate function `f` is true for the newly inserted value `v`,
114/// then inserting `(k,v)` into the map `m` and then applying the value filter
115/// is equivalent to applying the value filter to the original map `m` and
116/// then inserting `(k,v)` into the result.
117pub proof fn lemma_insert_value_filter_true<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K, v: V)
118    requires
119        f(v),
120    ensures
121        value_filter(m.insert(k, v), f) == value_filter(m, f).insert(k, v),
122{
123}
124
125/// If the predicate function `f` is false for the newly inserted value `v`,
126/// then inserting `(k,v)` into the map `m` and then applying the value filter
127/// is equivalent to applying the value filter to the original map `m` and
128/// then removing `k` from the result (if `k` exists in `m`) or leaving it unchanged
129/// (if it doesn't).
130pub proof fn lemma_insert_value_filter_false<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K, v: V)
131    requires
132        !f(v),
133    ensures
134        value_filter(m.insert(k, v), f) == if m.contains_key(k) {
135            value_filter(m, f).remove(k)
136        } else {
137            value_filter(m, f)
138        },
139{
140}
141
142/// The length of the value-filtered map after inserting `(k,v)` into `m`
143/// is equal to the length of the value-filtered map for the original map `m`
144/// if `k` exists in `m`, and `m[k]` and `v` both satisfy/un-satisfy the predicate
145/// function `f`.
146pub broadcast proof fn lemma_insert_value_filter_same_len<K, V>(
147    m: Map<K, V>,
148    f: spec_fn(V) -> bool,
149    k: K,
150    v: V,
151)
152    requires
153        m.contains_key(k) && f(m[k]) == f(v) || !m.contains_key(k) && !f(v),
154    ensures
155        #[trigger] value_filter(m.insert(k, v), f).len() == value_filter(m, f).len(),
156{
157    if f(v) {
158        lemma_insert_value_filter_true(m, f, k, v);
159        lemma_map_insert_len(value_filter(m, f), k, v);
160    } else {
161        lemma_insert_value_filter_false(m, f, k, v);
162        lemma_map_remove_len(value_filter(m, f), k);
163    }
164}
165
166/// The length of the value-filtered map after inserting `(k,v)` into `m`
167/// is equal to the length of the value-filtered map for the original map `m`
168/// plus one if `m[k]` does not satisfy `f` but `v` does, and minus one if
169/// `m[k]` satisfies `f` but `v` does not.
170pub broadcast proof fn lemma_insert_value_filter_different_len_contains<K, V>(
171    m: Map<K, V>,
172    f: spec_fn(V) -> bool,
173    k: K,
174    v: V,
175)
176    requires
177        m.contains_key(k),
178        f(m[k]) != f(v),
179    ensures
180        #[trigger] value_filter(m.insert(k, v), f).len() == value_filter(m, f).len() + if f(v) {
181            1
182        } else {
183            -1
184        },
185{
186    if f(v) {
187        lemma_insert_value_filter_true(m, f, k, v);
188        lemma_map_insert_len(m, k, v);
189    } else {
190        lemma_insert_value_filter_false(m, f, k, v);
191        lemma_map_remove_len(value_filter(m, f), k);
192    }
193}
194
195/// The length of the value-filtered map after inserting `(k,v)` into `m`
196/// is equal to the length of the value-filtered map for the original map `m`
197/// plus one if `k` does not exist in `m` and `v` satisfies the predicate function `f`.
198pub broadcast proof fn lemma_insert_value_filter_different_len_not_contains<K, V>(
199    m: Map<K, V>,
200    f: spec_fn(V) -> bool,
201    k: K,
202    v: V,
203)
204    requires
205        !m.contains_key(k),
206        f(v),
207    ensures
208        #[trigger] value_filter(m.insert(k, v), f).len() == value_filter(m, f).len() + 1,
209{
210    lemma_insert_value_filter_true(m, f, k, v);
211    lemma_map_insert_len(m, k, v);
212}
213
214pub proof fn lemma_value_filter_contains_key<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
215    requires
216        value_filter(m, f).contains_key(k),
217    ensures
218        m.contains_key(k),
219{
220}
221
222pub broadcast proof fn lemma_value_filter_choose<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool)
223    requires
224        value_filter(m, f).len() != 0,
225    ensures
226        value_filter(m, f).contains_key(#[trigger] value_filter_choose(m, f)),
227        f(m[value_filter_choose(m, f)]),
228{
229    lemma_set_choose_len(value_filter(m, f).dom());
230}
231
232} // verus!
233verus! {
234
235/// Returns true if predicate `f(k,v)` holds for all `(k,v)` in `map`.
236pub open spec fn forall_map<K, V>(map: Map<K, V>, f: spec_fn(K, V) -> bool) -> bool {
237    forall|k| #[trigger] map.contains_key(k) ==> f(k, map[k])
238}
239
240/// Returns true if predicate `f(v)` holds for all values in `map`.
241pub open spec fn forall_map_values<K, V>(map: Map<K, V>, f: spec_fn(V) -> bool) -> bool {
242    forall|k| #[trigger] map.contains_key(k) ==> f(map[k])
243}
244
245pub broadcast group group_forall_map_lemmas {
246    lemma_forall_map_insert,
247    lemma_forall_map_values_insert,
248    lemma_forall_map_remove,
249    lemma_forall_map_values_remove,
250}
251
252/// For any key in the map, `f(k, map[k])` holds if `forall_map(map, f)` holds.
253pub proof fn lemma_forall_map_entry<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
254    requires
255        forall_map(m, f),
256        m.contains_key(k),
257    ensures
258        f(k, m[k]),
259{
260}
261
262/// For any key in the map, `f(map[k])` holds if `forall_map_values(map, f)` holds.
263pub proof fn lemma_forall_map_values_entry<K, V>(m: Map<K, V>, f: spec_fn(V) -> bool, k: K)
264    requires
265        forall_map_values(m, f),
266        m.contains_key(k),
267    ensures
268        f(m[k]),
269{
270}
271
272/// `forall_map(m.insert(k, v), f)` holds if `f(k, v)` holds and
273/// `forall_map(m.remove(k),f)` (if `m` contains `k`) or `forall_map(m, f)` (if `m` does not contain `k`).
274pub broadcast proof fn lemma_forall_map_insert<K, V>(
275    m: Map<K, V>,
276    f: spec_fn(K, V) -> bool,
277    k: K,
278    v: V,
279)
280    ensures
281        #[trigger] forall_map(m.insert(k, v), f) ==> f(k, v) && if m.contains_key(k) {
282            forall_map(m.remove(k), f)
283        } else {
284            forall_map(m, f)
285        },
286{
287    assert(m.insert(k, v).contains_key(k));
288    if m.contains_key(k) {
289        assert(m.insert(k, v) == m.remove(k).insert(k, v));
290    }
291    if forall_map(m.insert(k, v), f) {
292        if !m.contains_key(k) {
293            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
294        }
295    }
296}
297
298/// `forall_map_values(m.insert(k, v), f)` holds if `f(v)` holds and
299/// `forall_map_values(m.remove(k),f)` (if `m` contains `k`) or `forall_map_values(m, f)` (if `m` does not contain `k`).
300pub broadcast proof fn lemma_forall_map_values_insert<K, V>(
301    m: Map<K, V>,
302    f: spec_fn(V) -> bool,
303    k: K,
304    v: V,
305)
306    ensures
307        #[trigger] forall_map_values(m.insert(k, v), f) ==> f(v) && if m.contains_key(k) {
308            forall_map_values(m.remove(k), f)
309        } else {
310            forall_map_values(m, f)
311        },
312{
313    assert(m.insert(k, v).contains_key(k));
314    if m.contains_key(k) {
315        assert(m.insert(k, v) == m.remove(k).insert(k, v));
316    }
317    if forall_map_values(m.insert(k, v), f) {
318        if !m.contains_key(k) {
319            assert(forall|k0| #[trigger] m.contains_key(k0) ==> m.insert(k, v).contains_key(k0));
320        }
321    }
322}
323
324/// `forall_map(m,f)` holds if `forall_map(m.remove(k), f)` holds and
325/// `f(k, m[k])` holds (if `m` contains `k`).
326pub broadcast proof fn lemma_forall_map_remove<K, V>(m: Map<K, V>, f: spec_fn(K, V) -> bool, k: K)
327    ensures
328        forall_map(m, f) <==> #[trigger] forall_map(m.remove(k), f) && (m.contains_key(k) ==> f(
329            k,
330            m[k],
331        )),
332{
333    if m.contains_key(k) {
334        assert(m == m.remove(k).insert(k, m[k]));
335    } else {
336        assert(m == m.remove(k));
337    }
338}
339
340/// `forall_map_values(m,f)` holds if `forall_map_values(m.remove(k), f)` holds and
341/// `f(m[k])` holds (if `m` contains `k`).
342pub broadcast proof fn lemma_forall_map_values_remove<K, V>(
343    m: Map<K, V>,
344    f: spec_fn(V) -> bool,
345    k: K,
346)
347    ensures
348        forall_map_values(m, f) <==> #[trigger] forall_map_values(m.remove(k), f) && (
349        m.contains_key(k) ==> f(m[k])),
350{
351    if m.contains_key(k) {
352        assert(m == m.remove(k).insert(k, m[k]));
353    } else {
354        assert(m == m.remove(k));
355    }
356}
357
358/// Returns a new map that projects the first key of a pair `(K1, K2)`,
359/// keeping the values associated with the second key `K2`.
360pub open spec fn project_first_key<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1) -> Map<K2, V> {
361    Map::new(m.dom().filter(|p: (K1, K2)| p.0 == k1).map(|p: (K1, K2)| p.1), |k2: K2| m[(k1, k2)])
362}
363
364/// Returns a new map that projects the second key of a pair `(K1, K2)`,
365/// keeping the values associated with the first key `K1`.
366pub open spec fn project_second_key<K1, K2, V>(m: Map<(K1, K2), V>, k2: K2) -> Map<K1, V> {
367    Map::new(m.dom().filter(|p: (K1, K2)| p.1 == k2).map(|p: (K1, K2)| p.0), |k1: K1| m[(k1, k2)])
368}
369
370/// A lemma showing that `project_first_key`` is sound.
371/// There is no need to actually use this lemma in practice at most of the time because Verus can automatically prove it.
372pub proof fn lemma_project_first_key_sound<K1, K2, V>(m: Map<(K1, K2), V>, k1: K1)
373    ensures
374        forall|k2: K2|
375            {
376                &&& #[trigger] project_first_key(m, k1).contains_key(k2) <==> m.contains_key(
377                    (k1, k2),
378                )
379                &&& project_first_key(m, k1).contains_key(k2) ==> project_first_key(m, k1)[k2]
380                    == m[(k1, k2)]
381            },
382{
383    assert forall|k2: K2|
384        {
385            &&& #[trigger] project_first_key(m, k1).contains_key(k2) <==> m.contains_key((k1, k2))
386            &&& project_first_key(m, k1).contains_key(k2) ==> project_first_key(m, k1)[k2] == m[(
387                k1,
388                k2,
389            )]
390        } by {
391        if m.contains_key((k1, k2)) {
392            assert(m.dom().filter(|p: (K1, K2)| p.0 == k1).contains((k1, k2)));
393        }
394        if project_first_key(m, k1).contains_key(k2) {
395            assert(m.contains_key((k1, k2)));
396        }
397    }
398}
399
400/// If the value filter of the projected map is non-empty, then there exists a key `k2`
401/// such that the original map contains the pair `(k1, k2)` and `m[(k1, k2)]` satisfies the predicate `f`.
402pub proof fn lemma_project_first_key_value_filter_non_empty<K1, K2, V>(
403    m: Map<(K1, K2), V>,
404    k1: K1,
405    f: spec_fn(V) -> bool,
406)
407    requires
408        value_filter(project_first_key(m, k1), f).len() != 0,
409    ensures
410        exists|k2: K2| #[trigger]
411            project_first_key(m, k1).contains_key(k2) && f(project_first_key(m, k1)[k2]),
412{
413    lemma_value_filter_choose(project_first_key(m, k1), f);
414    let k2 = value_filter_choose(project_first_key(m, k1), f);
415    assert(project_first_key(m, k1).contains_key(k2) && f(m[(k1, k2)]));
416}
417
418pub proof fn lemma_project_first_key_value_filter_empty<K1, K2, V>(
419    m: Map<(K1, K2), V>,
420    k1: K1,
421    f: spec_fn(V) -> bool,
422)
423    requires
424        value_filter(project_first_key(m, k1), f).len() == 0,
425    ensures
426        forall|k2: K2| #[trigger]
427            project_first_key(m, k1).contains_key(k2) ==> !f(project_first_key(m, k1)[k2]),
428{
429    assert forall|k2: K2| #[trigger] project_first_key(m, k1).contains_key(k2) implies !f(
430        project_first_key(m, k1)[k2],
431    ) by {
432        if f(project_first_key(m, k1)[k2]) {
433            assert(value_filter(project_first_key(m, k1), f).dom().contains(k2));
434            Set::lemma_len0_is_empty(value_filter(project_first_key(m, k1), f).dom());
435            assert(false);
436        }
437    }
438}
439
440} // verus!
vstd_extra/map_extra.rs

vstd_extra/
map_extra.rs
