vstd/std_specs/
range.rs

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

vstd/std_specs/
range.rs
