vstd/
compute.rs

1use super::prelude::*;
2use core::ops::Range;
3
4verus! {
5
6/// Simplify proofs-by-computation for ranges of values
7pub trait RangeAll where Self: Sized {
8    /// Checks whether `p` holds for all values in this range.
9    /// See the [Verus tutorial](https://verus-lang.github.io/verus/guide/assert_by_compute.html) for example usage.
10    spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool;
11}
12
13pub open spec fn range_all_spec_rec(r: Range<int>, p: spec_fn(int) -> bool) -> bool
14    decreases r.end - r.start,
15{
16    if r.start >= r.end {
17        true
18    } else {
19        p(r.start) && range_all_spec_rec(r.start + 1..r.end, p)
20    }
21}
22
23impl RangeAll for Range<int> {
24    open spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool {
25        range_all_spec_rec(self, p)
26    }
27}
28
29pub broadcast proof fn all_spec_ensures(r: Range<int>, p: spec_fn(int) -> bool)
30    ensures
31        #[trigger] r.all_spec(p) ==> (forall|i| r.start <= i < r.end ==> #[trigger] p(i)),
32    decreases r.end - r.start,
33{
34    if r.start >= r.end {
35    } else {
36        all_spec_ensures(r.start + 1..r.end, p);
37    }
38}
39
40} // verus!
vstd/compute.rs

vstd/
compute.rs
