vstd_extra/external/
range.rs

1use core::ops::{Range, RangeInclusive};
2use vstd::prelude::*;
3
4verus! {
5
6/// Length of a `Range<usize>`. Malformed ranges (`start > end`) are length 0,
7/// matching `ExactSizeIterator::len` for `Range<A: Step>` where `Step::steps_between`
8/// returns `None` on `end < start`, collapsed to 0.
9pub open spec fn range_usize_len_spec(r: &Range<usize>) -> usize {
10    if r.start < r.end {
11        (r.end - r.start) as usize
12    } else {
13        0usize
14    }
15}
16
17/// Exec-mode `len` for a `Range<usize>`: use in place of `r.len()` which is an
18/// `ExactSizeIterator` provided method and can't be specced with
19/// `assume_specification`.
20#[verifier::when_used_as_spec(range_usize_len_spec)]
21pub fn range_usize_len(r: &Range<usize>) -> (ret: usize)
22    ensures
23        ret == range_usize_len_spec(r),
24{
25    if r.start < r.end {
26        r.end - r.start
27    } else {
28        0
29    }
30}
31
32/// Whether a `Range<usize>` is empty. Malformed ranges (`start > end`) are empty.
33pub open spec fn range_usize_is_empty_spec(r: &Range<usize>) -> bool {
34    !(r.start < r.end)
35}
36
37/// Exec-mode `is_empty` for a `Range<usize>`: use in place of `r.is_empty()`
38/// which needs `Idx: PartialOrd<Idx>` bound that doesn't round-trip cleanly
39/// through `assume_specification`.
40#[verifier::when_used_as_spec(range_usize_is_empty_spec)]
41pub fn range_usize_is_empty(r: &Range<usize>) -> (ret: bool)
42    ensures
43        ret == range_usize_is_empty_spec(r),
44{
45    !(r.start < r.end)
46}
47
48pub assume_specification<Idx>[ RangeInclusive::start ](r: &RangeInclusive<Idx>) -> (ret: &Idx)
49    ensures
50        *ret == r@.start,
51;
52
53pub assume_specification<Idx>[ RangeInclusive::end ](r: &RangeInclusive<Idx>) -> (ret: &Idx)
54    ensures
55        *ret == r@.end,
56;
57
58} // verus!
vstd_extra/external/range.rs

vstd_extra/external/
range.rs
