improv_verified/
take.rs

1//! The index range of `TAKE` / `DROP` over a list.
2
3#[allow(unused_imports)]
4use vstd::prelude::*;
5
6verus! {
7
8/// The `[from, to)` range `TAKE` (`drop` false) or `DROP` (`drop` true)
9/// keeps of a list of `len` values, for a count of `m` (already capped at
10/// `len`) from the front, or from the end when `from_end`.
11pub open spec fn range_spec(len: nat, m: nat, from_end: bool, drop: bool) -> (nat, nat) {
12    if !from_end && !drop {
13        (0, m)
14    } else if from_end && !drop {
15        ((len - m) as nat, len)
16    } else if !from_end && drop {
17        (m, len)
18    } else {
19        (0, (len - m) as nat)
20    }
21}
22
23/// `range_spec`: in bounds (`from ≤ to ≤ len`), `m` values for `TAKE` and
24/// `len − m` for `DROP`.
25pub fn range(len: usize, m: usize, from_end: bool, drop: bool) -> (r: (usize, usize))
26    requires
27        m <= len,
28    ensures
29        r.0 <= r.1 <= len,
30        (r.0 as nat, r.1 as nat) == range_spec(len as nat, m as nat, from_end, drop),
31        r.1 - r.0 == if drop { len - m } else { m as int },
32{
33    match (from_end, drop) {
34        (false, false) => (0, m),
35        (true, false) => (len - m, len),
36        (false, true) => (m, len),
37        (true, true) => (0, len - m),
38    }
39}
40
41/// Index `i` is in the range `r`.
42pub open spec fn within(r: (nat, nat), i: nat) -> bool {
43    r.0 <= i < r.1
44}
45
46/// `TAKE` and `DROP` of the same count partition the list: every index is
47/// in exactly one of the two ranges.
48pub proof fn lemma_take_drop_partition(len: nat, m: nat, from_end: bool)
49    requires
50        m <= len,
51    ensures
52        forall|i: nat|
53            i < len ==> (#[trigger] within(range_spec(len, m, from_end, false), i) != within(
54                range_spec(len, m, from_end, true),
55                i,
56            )),
57{
58}
59
60} // verus!
61
62#[cfg(test)]
63#[cfg_attr(coverage_nightly, coverage(off))]
64mod tests {
65    use super::*;
66
67    #[test]
68    fn take_and_drop_partition() {
69        for len in 0..6 {
70            for m in 0..=len {
71                for end in [false, true] {
72                    let (a, b) = range(len, m, end, false);
73                    let (c, d) = range(len, m, end, true);
74                    assert_eq!(b - a, m);
75                    let mut all: Vec<usize> = (a..b).chain(c..d).collect();
76                    all.sort_unstable();
77                    assert_eq!(all, (0..len).collect::<Vec<_>>());
78                }
79            }
80        }
81    }
82}
improv_verified/take.rs

improv_verified/
take.rs
