vstd/std_specs/
range.rs

1use super::super::prelude::*;
2use super::super::view::View;
3use super::cmp::{PartialOrdIs, PartialOrdSpec};
4use core::ops::{Range, RangeInclusive};
5
6verus! {
7
8#[verifier::external_type_specification]
9#[verifier::reject_recursive_types_in_ground_variants(Idx)]
10pub struct ExRange<Idx>(Range<Idx>);
11
12#[verifier::external_type_specification]
13#[verifier::external_body]
14#[verifier::reject_recursive_types_in_ground_variants(Idx)]
15pub struct ExRangeInclusive<Idx>(RangeInclusive<Idx>);
16
17pub struct RangeInclusiveView<Idx> {
18    pub start: Idx,
19    pub end: Idx,
20    pub exhausted: bool,
21}
22
23pub trait ContainsSpec<Idx, U> where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx> {
24    spec fn obeys_contains() -> bool;
25
26    spec fn contains_spec(&self, i: &U) -> bool;
27}
28
29impl<Idx, U> ContainsSpec<Idx, U> for RangeInclusive<Idx> where
30    Idx: PartialOrd<U>,
31    U: ?Sized + PartialOrd<Idx>,
32 {
33    open spec fn obeys_contains() -> bool {
34        (U::obeys_partial_cmp_spec() && <Idx as PartialOrdSpec<U>>::obeys_partial_cmp_spec())
35    }
36
37    open spec fn contains_spec(&self, i: &U) -> bool {
38        self@.start.is_le(&i) && if self@.exhausted {
39            i.is_lt(&self@.end)
40        } else {
41            i.is_le(&self@.end)
42        }
43    }
44}
45
46impl<Idx, U> ContainsSpec<Idx, U> for Range<Idx> where
47    Idx: PartialOrd<U>,
48    U: ?Sized + PartialOrd<Idx>,
49 {
50    open spec fn obeys_contains() -> bool {
51        (U::obeys_partial_cmp_spec() && <Idx as PartialOrdSpec<U>>::obeys_partial_cmp_spec())
52    }
53
54    open spec fn contains_spec(&self, i: &U) -> bool {
55        self.start.is_le(&i) && i.is_lt(&self.end)
56    }
57}
58
59impl<Idx> View for RangeInclusive<Idx> {
60    type V = RangeInclusiveView<Idx>;
61
62    uninterp spec fn view(&self) -> Self::V;
63}
64
65pub trait StepSpec where Self: Sized {
66    // REVIEW: it would be nice to be able to use SpecOrd::spec_lt (not yet supported)
67    spec fn spec_is_lt(self, other: Self) -> bool;
68
69    spec fn spec_steps_between(self, end: Self) -> Option<usize>;
70
71    spec fn spec_steps_between_int(self, end: Self) -> int;
72
73    spec fn spec_forward_checked(self, count: usize) -> Option<Self>;
74
75    spec fn spec_forward_checked_int(self, count: int) -> Option<Self>;
76
77    spec fn spec_backward_checked(self, count: usize) -> Option<Self>;
78
79    spec fn spec_backward_checked_int(self, count: int) -> Option<Self>;
80}
81
82pub uninterp spec fn spec_range_next<A>(a: Range<A>) -> (Range<A>, Option<A>);
83
84pub assume_specification<A: core::iter::Step>[ Range::<A>::next ](range: &mut Range<A>) -> (r:
85    Option<A>)
86    ensures
87        (*range, r) == spec_range_next(*old(range)),
88;
89
90/// Range::contains method is valid and safe to use only when cmp operations are implemented to satisfy
91/// obeys_partial_cmp_spec. Specifically, the comparison must be deterministic, and `lt` (less than)
92/// and `le` (less than or equal to) must define total orders.
93/// If using Range::contains with types that do not satisfy obeys_partial_cmp_spec, no spec is provided.
94pub assume_specification<Idx: PartialOrd<Idx>, U>[ Range::<Idx>::contains ](
95    r: &Range<Idx>,
96    i: &U,
97) -> (ret: bool) where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>
98    ensures
99        <Range::<Idx> as ContainsSpec<Idx, U>>::obeys_contains() ==> ret == r.contains_spec(i),
100;
101
102pub assume_specification<Idx: PartialOrd<Idx>, U>[ RangeInclusive::<Idx>::contains ](
103    r: &RangeInclusive<Idx>,
104    i: &U,
105) -> (ret: bool) where Idx: PartialOrd<U>, U: ?Sized + PartialOrd<Idx>
106    ensures
107        <RangeInclusive::<Idx> as ContainsSpec<Idx, U>>::obeys_contains() ==> ret
108            == r.contains_spec(i),
109;
110
111pub assume_specification<Idx>[ RangeInclusive::<Idx>::new ](start: Idx, end: Idx) -> (ret:
112    core::ops::RangeInclusive<Idx>)
113    ensures
114        ret@.start == start,
115        ret@.end == end,
116        ret@.exhausted == false,
117;
118
119pub struct RangeGhostIterator<A> {
120    pub start: A,
121    pub cur: A,
122    pub end: A,
123}
124
125impl<A: StepSpec> super::super::pervasive::ForLoopGhostIteratorNew for Range<A> {
126    type GhostIter = RangeGhostIterator<A>;
127
128    open spec fn ghost_iter(&self) -> RangeGhostIterator<A> {
129        RangeGhostIterator { start: self.start, cur: self.start, end: self.end }
130    }
131}
132
133impl<
134    A: StepSpec + core::iter::Step,
135> super::super::pervasive::ForLoopGhostIterator for RangeGhostIterator<A> {
136    type ExecIter = Range<A>;
137
138    type Item = A;
139
140    type Decrease = int;
141
142    open spec fn exec_invariant(&self, exec_iter: &Range<A>) -> bool {
143        &&& self.cur == exec_iter.start
144        &&& self.end == exec_iter.end
145    }
146
147    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
148        &&& self.start.spec_is_lt(self.cur) || self.start == self.cur
149        &&& self.cur.spec_is_lt(self.end) || self.cur
150            == self.end
151        // TODO (not important): use new "matches ==>" syntax here
152        &&& if let Some(init) = init {
153            &&& init.start == init.cur
154            &&& init.start == self.start
155            &&& init.end == self.end
156        } else {
157            true
158        }
159    }
160
161    open spec fn ghost_ensures(&self) -> bool {
162        !self.cur.spec_is_lt(self.end)
163    }
164
165    open spec fn ghost_decrease(&self) -> Option<int> {
166        Some(self.cur.spec_steps_between_int(self.end))
167    }
168
169    open spec fn ghost_peek_next(&self) -> Option<A> {
170        Some(self.cur)
171    }
172
173    open spec fn ghost_advance(&self, _exec_iter: &Range<A>) -> RangeGhostIterator<A> {
174        RangeGhostIterator { cur: self.cur.spec_forward_checked(1).unwrap(), ..*self }
175    }
176}
177
178impl<A: StepSpec + core::iter::Step> View for RangeGhostIterator<A> {
179    type V = Seq<A>;
180
181    // generate seq![start, start + 1, start + 2, ..., cur - 1]
182    open spec fn view(&self) -> Seq<A> {
183        Seq::new(
184            self.start.spec_steps_between_int(self.cur) as nat,
185            |i: int| self.start.spec_forward_checked_int(i).unwrap(),
186        )
187    }
188}
189
190} // verus!
191macro_rules! step_specs {
192    ($t: ty, $axiom: ident) => {
193        verus! {
194        impl StepSpec for $t {
195            open spec fn spec_is_lt(self, other: Self) -> bool {
196                self < other
197            }
198            open spec fn spec_steps_between(self, end: Self) -> Option<usize> {
199                let n = end - self;
200                if usize::MIN <= n <= usize::MAX {
201                    Some(n as usize)
202                } else {
203                    None
204                }
205            }
206            open spec fn spec_steps_between_int(self, end: Self) -> int {
207                end - self
208            }
209            open spec fn spec_forward_checked(self, count: usize) -> Option<Self> {
210                self.spec_forward_checked_int(count as int)
211            }
212            open spec fn spec_forward_checked_int(self, count: int) -> Option<Self> {
213                if self + count <= $t::MAX {
214                    Some((self + count) as $t)
215                } else {
216                    None
217                }
218            }
219            open spec fn spec_backward_checked(self, count: usize) -> Option<Self> {
220                self.spec_backward_checked_int(count as int)
221            }
222            open spec fn spec_backward_checked_int(self, count: int) -> Option<Self> {
223                if self - count >= $t::MIN {
224                    Some((self - count) as $t)
225                } else {
226                    None
227                }
228            }
229        }
230        // TODO: we might be able to make this generic over A: StepSpec
231        // once we settle on a way to connect std traits like Step with spec traits like StepSpec.
232        pub broadcast proof fn $axiom(range: Range<$t>)
233            ensures
234                range.start.spec_is_lt(range.end) ==>
235                    // TODO (not important): use new "matches ==>" syntax here
236                    (if let Some(n) = range.start.spec_forward_checked(1) {
237                        spec_range_next(range) == (Range { start: n, ..range }, Some(range.start))
238                    } else {
239                        true
240                    }),
241                !range.start.spec_is_lt(range.end) ==>
242                    #[trigger] spec_range_next(range) == (range, None::<$t>),
243        {
244            admit();
245        }
246        } // verus!
247    };
248}
249
250step_specs!(u8, axiom_spec_range_next_u8);
251step_specs!(u16, axiom_spec_range_next_u16);
252step_specs!(u32, axiom_spec_range_next_u32);
253step_specs!(u64, axiom_spec_range_next_u64);
254step_specs!(u128, axiom_spec_range_next_u128);
255step_specs!(usize, axiom_spec_range_next_usize);
256step_specs!(i8, axiom_spec_range_next_i8);
257step_specs!(i16, axiom_spec_range_next_i16);
258step_specs!(i32, axiom_spec_range_next_i32);
259step_specs!(i64, axiom_spec_range_next_i64);
260step_specs!(i128, axiom_spec_range_next_i128);
261step_specs!(isize, axiom_spec_range_next_isize);
262
263verus! {
264
265pub broadcast group group_range_axioms {
266    axiom_spec_range_next_u8,
267    axiom_spec_range_next_u16,
268    axiom_spec_range_next_u32,
269    axiom_spec_range_next_u64,
270    axiom_spec_range_next_u128,
271    axiom_spec_range_next_usize,
272    axiom_spec_range_next_i8,
273    axiom_spec_range_next_i16,
274    axiom_spec_range_next_i32,
275    axiom_spec_range_next_i64,
276    axiom_spec_range_next_i128,
277    axiom_spec_range_next_isize,
278}
279
280} // verus!
vstd/std_specs/range.rs

vstd/std_specs/
range.rs
