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
89pub assume_specification<Idx>[ RangeInclusive::<Idx>::new ](start: Idx, end: Idx) -> (ret:
90    core::ops::RangeInclusive<Idx>)
91    ensures
92        ret@.start == start,
93        ret@.end == end,
94        ret@.exhausted == false,
95;
96
97impl<A: core::iter::Step> super::iter::IteratorSpecImpl for Range<A> {
98    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
99        true
100    }
101
102    open spec fn remaining(&self) -> Seq<Self::Item> {
103        Seq::new(
104            self.start.spec_steps_between_int(self.end) as nat,
105            |i: int| self.start.spec_forward_checked_int(i).unwrap(),
106        )
107    }
108
109    uninterp spec fn will_return_none(&self) -> bool;
110
111    #[verifier::prophetic]
112    open spec fn initial_value_relation(&self, init: &Self) -> bool {
113        // Standard invariant for the iterator itself:
114        //   If there are no steps between start and end, then remaining is empty;
115        //   otherwise it contains all of the steps in between start and end
116        &&& (self.start.spec_steps_between_int(self.end) <= 0 && IteratorSpec::remaining(self).len()
117            == 0) || (self.start.spec_steps_between_int(self.end) == IteratorSpec::remaining(
118            self,
119        ).len() as int)
120        &&& forall|i: int|
121            0 <= i < IteratorSpec::remaining(self).len() ==> #[trigger] IteratorSpec::remaining(
122                self,
123            )[i] == self.start.spec_forward_checked_int(
124                i,
125            ).unwrap()
126        // Connections to init
127        &&& self.start == init.start
128        &&& self.end == init.end
129        &&& (init.start.spec_steps_between_int(init.end) <= 0 && IteratorSpec::remaining(self).len()
130            == 0) || (init.start.spec_steps_between_int(self.end) == IteratorSpec::remaining(
131            self,
132        ).len() as int)
133        &&& forall|i: int|
134            0 <= i < IteratorSpec::remaining(self).len() ==> #[trigger] IteratorSpec::remaining(
135                self,
136            )[i] == init.start.spec_forward_checked_int(i).unwrap()
137    }
138
139    open spec fn decrease(&self) -> Option<nat> {
140        Some(self.start.spec_steps_between_int(self.end) as nat)
141    }
142
143    open spec fn peek(&self, index: int) -> Option<Self::Item> {
144        //Some(self.start.spec_forward_checked_int(index).unwrap())
145        if 0 <= index <= self.start.spec_steps_between_int(self.end) {
146            Some(self.start.spec_forward_checked_int(index).unwrap())
147        } else {
148            None
149        }
150    }
151}
152
153pub assume_specification<A: core::iter::Step>[ <Range<A> as Iterator>::next ](
154    range: &mut Range<A>,
155) -> (r: Option<A>)
156    ensures
157        (*final(range), r) == spec_range_next(*old(range)),
158;
159
160} // verus!
161macro_rules! step_specs {
162    ($t: ty, $axiom: ident) => {
163        verus! {
164        impl StepSpecImpl for $t {
165            open spec fn spec_is_lt(self, other: Self) -> bool {
166                self < other
167            }
168            open spec fn spec_steps_between(self, end: Self) -> Option<usize> {
169                let n = end - self;
170                if usize::MIN <= n <= usize::MAX {
171                    Some(n as usize)
172                } else {
173                    None
174                }
175            }
176            open spec fn spec_steps_between_int(self, end: Self) -> int {
177                end - self
178            }
179            open spec fn spec_forward_checked(self, count: usize) -> Option<Self> {
180                StepSpec::spec_forward_checked_int(self, count as int)
181            }
182            open spec fn spec_forward_checked_int(self, count: int) -> Option<Self> {
183                if self + count <= $t::MAX {
184                    Some((self + count) as $t)
185                } else {
186                    None
187                }
188            }
189            open spec fn spec_backward_checked(self, count: usize) -> Option<Self> {
190                StepSpec::spec_backward_checked_int(self, count as int)
191            }
192            open spec fn spec_backward_checked_int(self, count: int) -> Option<Self> {
193                if self - count >= $t::MIN {
194                    Some((self - count) as $t)
195                } else {
196                    None
197                }
198            }
199        }
200        // TODO: we might be able to make this generic over A: StepSpec
201        // once we settle on a way to connect std traits like Step with spec traits like StepSpec.
202        pub broadcast proof fn $axiom(range: Range<$t>)
203            ensures
204                StepSpec::spec_is_lt(range.start, range.end) ==>
205                    // TODO (not important): use new "matches ==>" syntax here
206                    (if let Some(n) = StepSpec::spec_forward_checked(range.start, 1) {
207                        spec_range_next(range) == (Range { start: n, ..range }, Some(range.start))
208                    } else {
209                        true
210                    }),
211                !StepSpec::spec_is_lt(range.start, range.end) ==>
212                    #[trigger] spec_range_next(range) == (range, None::<$t>),
213        {
214            admit();
215        }
216        } // verus!
217    };
218}
219
220step_specs!(u8, axiom_spec_range_next_u8);
221step_specs!(u16, axiom_spec_range_next_u16);
222step_specs!(u32, axiom_spec_range_next_u32);
223step_specs!(u64, axiom_spec_range_next_u64);
224step_specs!(u128, axiom_spec_range_next_u128);
225step_specs!(usize, axiom_spec_range_next_usize);
226step_specs!(i8, axiom_spec_range_next_i8);
227step_specs!(i16, axiom_spec_range_next_i16);
228step_specs!(i32, axiom_spec_range_next_i32);
229step_specs!(i64, axiom_spec_range_next_i64);
230step_specs!(i128, axiom_spec_range_next_i128);
231step_specs!(isize, axiom_spec_range_next_isize);
232
233verus! {
234
235pub broadcast group group_range_axioms {
236    axiom_spec_range_next_u8,
237    axiom_spec_range_next_u16,
238    axiom_spec_range_next_u32,
239    axiom_spec_range_next_u64,
240    axiom_spec_range_next_u128,
241    axiom_spec_range_next_usize,
242    axiom_spec_range_next_i8,
243    axiom_spec_range_next_i16,
244    axiom_spec_range_next_i32,
245    axiom_spec_range_next_i64,
246    axiom_spec_range_next_i128,
247    axiom_spec_range_next_isize,
248}
249
250} // verus!
vstd/std_specs/range.rs

vstd/std_specs/
range.rs
