vstd/std_specs/
range.rs

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

vstd/std_specs/
range.rs
