vstd/std_specs/
range.rs

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

vstd/std_specs/
range.rs
