vstd_extra/
seq_extra.rs

1//! Extra properties of [`vstd::seq::Seq`](https://verus-lang.github.io/verus/verusdoc/vstd/seq/struct.Seq.html).
2use vstd::prelude::*;
3use vstd::seq::*;
4use vstd::seq_lib::*;
5
6verus! {
7
8/// Splits a tracked sequence at position `n`, leaving `[0, n)` in `s`
9/// and returning `[n, len)`.
10pub proof fn seq_tracked_split_at<T>(tracked s: &mut Seq<T>, n: int) -> (tracked result: Seq<T>)
11    requires
12        0 <= n <= old(s).len(),
13    ensures
14        *final(s) == old(s)[..n],
15        result == old(s)[n..],
16    decreases old(s).len() - n,
17{
18    if n == s.len() {
19        Seq::tracked_empty()
20    } else {
21        let ghost orig = *s;
22        let tracked last = s.tracked_pop();
23        let tracked mut result = seq_tracked_split_at(s, n);
24        result.tracked_push(last);
25        result
26    }
27}
28
29pub broadcast proof fn lemma_seq_add_head_back<T>(s: Seq<T>)
30    requires
31        s.len() > 0,
32    ensures
33        s == #[trigger] seq![s[0]].add(s.drop_first()),
34{
35}
36
37pub broadcast proof fn lemma_seq_push_head<T>(s: Seq<T>, hd: T)
38    ensures
39        #[trigger] seq![hd].add(s) == s.reverse().push(hd).reverse(),
40{
41}
42
43pub broadcast proof fn lemma_seq_drop_pushed_head<T>(s: Seq<T>, hd: T)
44    ensures
45        #[trigger] seq![hd].add(s).drop_first() == s,
46{
47}
48
49pub broadcast proof fn lemma_seq_push_head_take_head<T>(s: Seq<T>, hd: T)
50    ensures
51        #[trigger] seq![hd].add(s)[0] == hd,
52{
53}
54
55} // verus!
56verus! {
57
58/// The result of pushing element `needle` into the sequence `s` contains `needle`.
59pub proof fn lemma_push_contains_same<T>(s: Seq<T>, needle: T)
60    ensures
61        #[trigger] s.push(needle).contains(needle),
62{
63    assert(s.push(needle).last() == needle);
64}
65
66/// If element `needle` is different from `new_elem`, then whether the sequence `s` contains `needle`
67/// after pushing `new_elem` depends on whether `s` contains `needle` before the push.
68pub proof fn lemma_push_contains_different<T>(s: Seq<T>, new_elem: T, needle: T)
69    requires
70        new_elem != needle,
71    ensures
72        #[trigger] s.push(new_elem).contains(needle) == s.contains(needle),
73{
74    if s.contains(needle) {
75        let i = choose|i: int| 0 <= i < s.len() && s[i] == needle;
76        lemma_seq_push_index_different(s, needle, i);
77        assert(0 <= i < s.push(new_elem).len() && s.push(new_elem)[i] == needle);
78    }
79}
80
81/// If the last element of the sequence `s` is different from `needle`, then whether the sequence
82/// `s` contains `needle` after dropping the last element depends on whether `s` contains `needle`
83/// before the drop.
84pub proof fn lemma_drop_last_contains_different<T>(s: Seq<T>, needle: T)
85    requires
86        s.len() > 0,
87        s.last() != needle,
88    ensures
89        #[trigger] s.drop_last().contains(needle) == s.contains(needle),
90{
91    if s.contains(needle) {
92        let i = choose|i: int| 0 <= i < s.len() && s[i] == needle;
93        assert(0 <= i < s.drop_last().len() && s.drop_last()[i] == needle);
94    }
95}
96
97} // verus!
98verus! {
99
100/// Returns true if predicate `f(i,seq[i])` holds for all indices `i`.
101pub open spec fn forall_seq<T>(seq: Seq<T>, f: spec_fn(int, T) -> bool) -> bool {
102    forall|i| #![trigger seq[i]] 0 <= i < seq.len() ==> f(i, seq[i])
103}
104
105pub broadcast group group_forall_seq_lemmas {
106    lemma_forall_seq_push,
107    lemma_seq_all_push,
108    lemma_forall_seq_drop_last,
109    lemma_seq_all_drop_last,
110    lemma_seq_all_add,
111    lemma_seq_all_index,
112}
113
114/// Index `i` of the sequence `s` satisfies `f(i,s[i])` if `forall_seq(s,f)` holds.
115pub proof fn lemma_forall_seq_index<T>(s: Seq<T>, f: spec_fn(int, T) -> bool, i: int)
116    requires
117        forall_seq(s, f),
118        0 <= i < s.len(),
119    ensures
120        f(i, s[i]),
121{
122}
123
124/// Index `i` of the sequence `s` satisfies `f(s[i])` if `s.all(f)` holds.
125/// This proof is required due to the change of trigger by replacing the original `forall_seq_values` with `Seq::all`.
126pub broadcast proof fn lemma_seq_all_index<T>(s: Seq<T>, f: spec_fn(T) -> bool, i: int)
127    requires
128        0 <= i < s.len(),
129        #[trigger] s.all(f),
130    ensures
131        f(#[trigger] (s[i])),
132{
133}
134
135/// `forall_seq(s.push(v),f)` is equivalent to `forall_seq(s,f)` and `f(s.len(),v)`.
136pub broadcast proof fn lemma_forall_seq_push<T>(s: Seq<T>, f: spec_fn(int, T) -> bool, v: T)
137    ensures
138        forall_seq(s, f) && f(s.len() as int, v) <==> #[trigger] forall_seq(s.push(v), f),
139{
140    if forall_seq(s.push(v), f) {
141        assert forall|i| 0 <= i < s.len() implies f(i, s[i]) by {
142            assert(s[i] == s.push(v)[i]);
143        }
144        assert(s.push(v)[s.len() as int] == v);
145    }
146}
147
148/// s.push(v).all(f)` is equivalent to `s.all(f)` and `f(v)`.
149pub broadcast proof fn lemma_seq_all_push<T>(s: Seq<T>, f: spec_fn(T) -> bool, v: T)
150    ensures
151        #[trigger] s.push(v).all(f) <==> s.all(f) && f(v),
152{
153    if s.push(v).all(f) {
154        assert forall|i| 0 <= i < s.len() implies f(s[i]) by {
155            assert(s[i] == s.push(v)[i]);
156        }
157        assert(s.push(v)[s.len() as int] == v);
158    }
159}
160
161/// `forall_seq(s,f)` is equivalent to `forall_seq(s.drop_last(),f)` and `f(s.len() as int - 1, s.last())`.
162pub broadcast proof fn lemma_forall_seq_drop_last<T>(s: Seq<T>, f: spec_fn(int, T) -> bool)
163    requires
164        s.len() > 0,
165    ensures
166        forall_seq(s, f) <==> #[trigger] forall_seq(s.drop_last(), f) && f(
167            s.len() as int - 1,
168            s.last(),
169        ),
170{
171    assert(s == s.drop_last().push(s.last()));
172}
173
174/// `s.all(f)` is equivalent to `s.drop_last().all(f)` and `f(s.last())`.
175pub broadcast proof fn lemma_seq_all_drop_last<T>(s: Seq<T>, f: spec_fn(T) -> bool)
176    requires
177        s.len() > 0,
178    ensures
179        s.all(f) <==> #[trigger] s.drop_last().all(f) && f(s.last()),
180{
181    assert(s == s.drop_last().push(s.last()));
182}
183
184pub broadcast proof fn lemma_seq_all_add<T>(s1: Seq<T>, s2: Seq<T>, f: spec_fn(T) -> bool)
185    ensures
186        s1.all(f) && s2.all(f) <==> #[trigger] (s1 + s2).all(f),
187    decreases s2.len(),
188{
189    if s2.len() == 0 {
190        assert(s1 + s2 == s1);
191    } else {
192        lemma_seq_all_add(s1, s2.drop_last(), f);
193        if s1.all(f) && s2.all(f) {
194            assert((s1 + s2).all(f));
195        }
196        if (s1 + s2).all(f) {
197            assert((s1 + s2).drop_last() == s1 + s2.drop_last());
198            assert(s2 == s2.drop_last().push(s2.last()));
199            assert((s1 + s2).last() == s2.last());
200        }
201    }
202}
203
204/// If `source1` and `source2` are prefixes of `child`, then either `source1` is equal to `source2` or
205/// one of them is a prefix of the other.
206pub proof fn lemma_prefix_of_common_sequence(source1: Seq<nat>, source2: Seq<nat>, child: Seq<nat>)
207    requires
208        source1.is_prefix_of(child),
209        source2.is_prefix_of(child),
210    ensures
211        source1 == source2 || source1.len() < source2.len() && source1.is_prefix_of(source2)
212            || source2.len() < source1.len() && source2.is_prefix_of(source1),
213{
214}
215
216pub broadcast proof fn lemma_seq_to_set_map_contains<T, U>(s: Seq<T>, f: spec_fn(T) -> U, i: int)
217    requires
218        0 <= i < s.len(),
219    ensures
220        #![trigger s.map_values(f), s[i]]
221        (s.map_values(f)).to_set().contains(f(s[i])),
222{
223    assert(s.contains(s[i]));
224    assert(f(s[i]) == s.map_values(f)[i]);
225}
226
227pub broadcast group group_seq_extra_lemmas {
228    lemma_seq_add_head_back,
229    lemma_seq_push_head,
230    lemma_seq_drop_pushed_head,
231    lemma_seq_push_head_take_head,
232    lemma_seq_to_set_map_contains,
233}
234
235/// The index of the first `false` bit in `s`, or `s.len()` if every bit is `true`.
236pub open spec fn is_first_zero(s: Seq<bool>, i: int) -> bool {
237    &&& 0 <= i <= s.len()
238    &&& (forall|j: int| #![trigger s[j]] 0 <= j < i ==> s[j])
239    &&& (i < s.len() ==> !s[i])
240}
241
242/// Index of the first `false` bit, or `s.len()` if every bit is `true`. Defined
243/// recursively so it is deterministic and the SMT solver can unfold it.
244pub open spec fn first_zero_index(s: Seq<bool>) -> int
245    decreases s.len(),
246{
247    if s.len() == 0 {
248        0
249    } else if !s[0] {
250        0
251    } else {
252        1 + first_zero_index(s[1..])
253    }
254}
255
256/// `is_first_zero` is uniquely satisfied.
257pub proof fn lemma_is_first_zero_unique(s: Seq<bool>, i: int, j: int)
258    requires
259        is_first_zero(s, i),
260        is_first_zero(s, j),
261    ensures
262        #![auto]
263        i == j,
264{
265}
266
267/// `first_zero_index(s)` itself satisfies `is_first_zero` (induction on `s.len()`).
268pub proof fn lemma_first_zero_index_is_first_zero(s: Seq<bool>)
269    ensures
270        is_first_zero(s, first_zero_index(s)),
271    decreases s.len(),
272{
273    if s.len() == 0 {
274    } else if !s[0] {
275    } else {
276        let sub = s[1..];
277        lemma_first_zero_index_is_first_zero(sub);
278        let i2 = first_zero_index(sub);
279        assert(is_first_zero(s, 1 + i2)) by {
280            assert forall|j: int| 0 <= j < 1 + i2 implies s[j] by {
281                if j == 0 {
282                } else {
283                    assert(s[j] == sub[j - 1]);
284                }
285            }
286            if 1 + i2 < s.len() {
287            }
288        }
289    }
290}
291
292/// If the prefix `[0, k)` of `s` is all `true`, then the first zero of `s` is
293/// `k` plus the first zero of the remainder (induction on `s.len()`).
294pub proof fn lemma_first_zero_index_after_true_prefix(s: Seq<bool>, k: int)
295    requires
296        0 <= k <= s.len(),
297        forall|j: int| #![trigger s[j]] 0 <= j < k ==> s[j],
298    ensures
299        first_zero_index(s) == k + first_zero_index(s[k..]),
300    decreases s.len(),
301{
302    if k == 0 {
303        assert(s[k..] =~= s) by {}
304    } else if s.len() == 0 {
305    } else {
306        let sub = s[1..];
307        lemma_first_zero_index_after_true_prefix(sub, k - 1);
308        assert(sub[k - 1..] =~= s[k..]) by {}
309    }
310}
311
312/// Setting the bit at `k - 1` (the current first zero) to `true`, when the prefix
313/// `[0, k - 1)` is all `true`, advances the first zero to
314/// `k + first_zero_index(s[k..])`.
315pub proof fn lemma_first_zero_index_advance_after_set(s: Seq<bool>, k: int)
316    requires
317        0 < k <= s.len(),
318        is_first_zero(s, k - 1),
319    ensures
320        first_zero_index(s.update(k - 1, true)) == k + first_zero_index(s[k..]),
321{
322    let t = s.update(k - 1, true);
323    lemma_first_zero_index_after_true_prefix(t, k);
324    assert(t[k..] =~= s[k..]) by {}
325}
326
327/// Clearing a `true` bit at `i` moves the first zero to `min(first_zero_index(s), i)`.
328pub proof fn lemma_first_zero_index_clear(s: Seq<bool>, i: int)
329    requires
330        0 <= i < s.len(),
331        s[i],
332    ensures
333        first_zero_index(s.update(i, false)) == if first_zero_index(s) <= i {
334            first_zero_index(s)
335        } else {
336            i
337        },
338    decreases s.len(),
339{
340    let fz = first_zero_index(s);
341    lemma_first_zero_index_is_first_zero(s);
342    let t = s.update(i, false);
343    lemma_first_zero_index_is_first_zero(t);
344    if fz <= i {
345        assert(is_first_zero(t, fz)) by {
346            if fz < s.len() {
347                assert(!t[fz]) by {
348                    if fz == i {
349                        assert(t[fz] == false);
350                    } else {
351                        assert(t[fz] == s[fz]);
352                        assert(!s[fz]);
353                    }
354                }
355            }
356            assert(forall|j: int| 0 <= j < fz ==> t[j]) by {
357                assert(forall|j: int| 0 <= j < fz ==> s[j]);
358            }
359        }
360        lemma_is_first_zero_unique(t, first_zero_index(t), fz);
361    } else {
362        assert(is_first_zero(t, i)) by {
363            assert(!t[i]);
364            assert(forall|j: int| 0 <= j < i ==> t[j]) by {
365                assert(forall|j: int| 0 <= j < i ==> s[j]);
366            }
367        }
368        lemma_is_first_zero_unique(t, first_zero_index(t), i);
369    }
370}
371
372/// Clearing all bits in `[start, end)` moves the first zero to
373/// `min(first_zero_index(s), start)`.
374pub proof fn lemma_first_zero_index_clear_range(s: Seq<bool>, t: Seq<bool>, start: int, end: int)
375    requires
376        s.len() == t.len(),
377        0 <= start < end <= s.len(),
378        forall|j: int| #![trigger t[j]] 0 <= j < start ==> t[j] == s[j],
379        forall|j: int| #![trigger t[j]] start <= j < end ==> !t[j],
380        forall|j: int| #![trigger t[j]] end <= j < s.len() ==> t[j] == s[j],
381    ensures
382        first_zero_index(t) == if first_zero_index(s) <= start {
383            first_zero_index(s)
384        } else {
385            start
386        },
387{
388    let fz = first_zero_index(s);
389    lemma_first_zero_index_is_first_zero(s);
390    lemma_first_zero_index_is_first_zero(t);
391    if fz <= start {
392        assert(is_first_zero(t, fz)) by {
393            if fz < s.len() {
394                assert(!t[fz]) by {
395                    if fz < start {
396                        assert(t[fz] == s[fz]);
397                        assert(!s[fz]);
398                    }
399                }
400            }
401            assert(forall|j: int| 0 <= j < fz ==> t[j]) by {
402                assert(forall|j: int| 0 <= j < fz ==> s[j]);
403                assert(forall|j: int| 0 <= j < fz ==> t[j] == s[j]);
404            }
405        }
406        lemma_is_first_zero_unique(t, first_zero_index(t), fz);
407    } else {
408        assert(is_first_zero(t, start)) by {
409            assert(!t[start]);
410            assert(forall|j: int| 0 <= j < start ==> t[j]) by {
411                assert(forall|j: int| 0 <= j < start ==> s[j]);
412            }
413        }
414        lemma_is_first_zero_unique(t, first_zero_index(t), start);
415    }
416}
417
418/// Setting a `false` bit at `i` that is strictly past the first zero leaves the
419/// first zero unchanged.
420pub proof fn lemma_first_zero_index_set_after_first_zero(s: Seq<bool>, i: int)
421    requires
422        0 <= i < s.len(),
423        first_zero_index(s) < i,
424        !s[i],
425    ensures
426        first_zero_index(s.update(i, true)) == first_zero_index(s),
427{
428    let fz = first_zero_index(s);
429    lemma_first_zero_index_is_first_zero(s);
430    let t = s.update(i, true);
431    lemma_first_zero_index_is_first_zero(t);
432    assert(is_first_zero(t, fz)) by {
433        if fz < s.len() {
434            assert(!t[fz]) by {
435                assert(fz < i);
436                assert(t[fz] == s[fz]);
437                assert(!s[fz]);
438            }
439        }
440        assert forall|j: int| 0 <= j < fz implies t[j] by {
441            assert(t[j] == s[j]);
442            assert(s[j]);
443        }
444    }
445    lemma_is_first_zero_unique(t, first_zero_index(t), fz);
446}
447
448} // verus!
vstd_extra/seq_extra.rs

vstd_extra/
seq_extra.rs
