vstd_extra/resource/
range.rs

1//! Linear ownership of a contiguous finite range.
2use vstd::{
3    prelude::*,
4    resource::{Loc, set::GhostSubset},
5    set_lib::FiniteRange,
6};
7
8use crate::range::RangeExtraFns;
9use core::ops::Range;
10
11verus! {
12
13/// A [`GhostSubset`] whose elements are exactly one half-open range.
14#[verifier::reject_recursive_types(T)]
15pub tracked struct GhostSubRange<T: FiniteRange> {
16    subset: GhostSubset<T>,
17    ghost range: Range<T>,
18}
19
20impl<T: FiniteRange> GhostSubRange<T> {
21    #[verifier::type_invariant]
22    closed spec fn inv(self) -> bool {
23        self.subset@ == self.range.view_set()
24    }
25
26    /// Wraps subset ownership known to represent exactly `range`.
27    pub proof fn tracked_new(tracked subset: GhostSubset<T>, range: Range<T>) -> (tracked result:
28        Self)
29        requires
30            subset@ =~= range.view_set(),
31        ensures
32            result.id() == subset.id(),
33            result.range() == range,
34            result@ == range.view_set(),
35    {
36        Self { subset, range }
37    }
38
39    /// The underlying ghost-resource location.
40    pub closed spec fn id(self) -> Loc {
41        self.subset.id()
42    }
43
44    /// The continuous half-open range represented by this resource.
45    pub closed spec fn range(self) -> Range<T> {
46        self.range
47    }
48
49    /// The set of elements owned by this resource.
50    pub open spec fn view(self) -> Set<T> {
51        self.range().view_set()
52    }
53
54    /// Borrows this range resource as an ordinary [`GhostSubset`].
55    pub proof fn tracked_borrow(tracked &self) -> (tracked result: &GhostSubset<T>)
56        ensures
57            result.id() == self.id(),
58            result@ == self@,
59    {
60        use_type_invariant(self);
61        &self.subset
62    }
63
64    /// Consumes this range wrapper and returns its underlying [`GhostSubset`].
65    pub proof fn tracked_into_subset(tracked self) -> (tracked result: GhostSubset<T>)
66        ensures
67            result.id() == self.id(),
68            result@ == self@,
69    {
70        use_type_invariant(&self);
71        self.subset
72    }
73}
74
75} // verus!
vstd_extra/resource/range.rs

vstd_extra/resource/
range.rs
