vstd_extra/
range.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Finite-set models and proof lemmas for half-open ranges.
3use vstd::{prelude::*, set_lib::FiniteRange, std_specs::cmp::PartialOrdIs};
4
5use core::ops::Range;
6
7verus! {
8
9/// Specification helpers for half-open ranges.
10pub trait RangeExtraFns<T: FiniteRange> {
11    /// The finite set denoted by this range.
12    spec fn view_set(self) -> Set<T>;
13}
14
15impl<T: FiniteRange> RangeExtraFns<T> for Range<T> {
16    open spec fn view_set(self) -> Set<T> {
17        T::range_set(self.start, self.end)
18    }
19}
20
21/// The union of the sets denoted by a sequence of ranges.
22pub open spec fn seq_range_union<T: FiniteRange>(s: Seq<Range<T>>) -> Set<T> {
23    s.map_values(|r: Range<T>| r.view_set()).to_set().flatten()
24}
25
26/// Whether the finite-range model agrees with the ordering model.
27pub open spec fn finite_range_matches_ord<T: FiniteRange + Ord>() -> bool {
28    forall|x: T, lo: T, hi: T| T::in_range(x, lo, hi) <==> lo.is_le(&x) && x.is_lt(&hi)
29}
30
31/// An element belongs to the union of a sequence of ranges if and only if it
32/// belongs to at least one of those ranges.
33pub proof fn lemma_seq_range_union_contains<T: FiniteRange>(s: Seq<Range<T>>, x: T)
34    ensures
35        seq_range_union(s).contains(x) <==> s.any(|r: Range<T>| r.view_set().contains(x)),
36{
37    broadcast use {Seq::to_set_ensures, Set::lemma_flatten_contains};
38
39    let pred = |r: Range<T>| r.view_set().contains(x);
40    let range_sets = s.map_values(|r: Range<T>| r.view_set());
41
42    if seq_range_union(s).contains(x) {
43        range_sets.to_set().lemma_flatten_contains(x);
44        let range_set = choose|range_set: Set<T>|
45            #![trigger range_sets.to_set().contains(range_set)]
46            range_sets.to_set().contains(range_set) && range_set.contains(x);
47        let i = choose|i: int| 0 <= i < range_sets.len() && range_sets[i] == range_set;
48
49        assert(pred(s[i]));
50        assert(s.any(pred));
51    } else if s.any(pred) {
52        let i = choose|i: int| #![auto] 0 <= i < s.len() && pred(s[i]);
53
54        assert(range_sets.to_set().contains(range_sets[i]));
55        range_sets.to_set().lemma_flatten_contains(x);
56    }
57}
58
59} // verus!
vstd_extra/range.rs

vstd_extra/
range.rs
