Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041use super::prelude::*;use core::ops::Range;
verus! {
/// Simplify proofs-by-computation for ranges of valuespub trait RangeAll where Self: Sized { /// Checks whether `p` holds for all values in this range. /// See the [Verus tutorial](https://verus-lang.github.io/verus/guide/assert_by_compute.html) for example usage. spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool;}
pub open spec fn range_all_spec_rec(r: Range<int>, p: spec_fn(int) -> bool) -> bool decreases r.end - r.start,{ if r.start >= r.end { true } else { p(r.start) && range_all_spec_rec(r.start + 1..r.end, p) }}
impl RangeAll for Range<int> { open spec fn all_spec(self, p: spec_fn(int) -> bool) -> bool { range_all_spec_rec(self, p) }}
pub broadcast proof fn all_spec_ensures(r: Range<int>, p: spec_fn(int) -> bool) ensures #[trigger] r.all_spec(p) ==> (forall|i| r.start <= i < r.end ==> #[trigger] p(i)), decreases r.end - r.start,{ if r.start >= r.end { } else { all_spec_ensures(r.start + 1..r.end, p); }}
} // verus!