creusot_std/std/iter/
range.rs

1use crate::{prelude::*, std::iter::ExactSizeIteratorSpec};
2#[cfg(feature = "nightly")]
3use core::iter::Step;
4use core::ops::{Range, RangeInclusive};
5
6#[cfg(feature = "nightly")]
7impl<Idx: DeepModel<DeepModelTy = Int> + Step> IteratorSpec for Range<Idx> {
8    #[logic(open, prophetic)]
9    fn completed(&mut self) -> bool {
10        pearlite! {
11            resolve(self) && self.start.deep_model() >= self.end.deep_model()
12        }
13    }
14
15    #[logic(open)]
16    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
17        pearlite! {
18            self.end == o.end && self.start.deep_model() <= o.start.deep_model()
19            && (visited.len() > 0 ==> o.start.deep_model() <= o.end.deep_model())
20            && visited.len() == o.start.deep_model() - self.start.deep_model()
21            && forall<i> 0 <= i && i < visited.len() ==>
22                visited[i].deep_model() == self.start.deep_model() + i
23        }
24    }
25
26    #[logic(law)]
27    #[ensures(self.produces(Seq::empty(), self))]
28    fn produces_refl(self) {}
29
30    #[logic(law)]
31    #[requires(a.produces(ab, b))]
32    #[requires(b.produces(bc, c))]
33    #[ensures(a.produces(ab.concat(bc), c))]
34    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
35}
36
37extern_spec! {
38    impl<Idx: DeepModel<DeepModelTy = Int> + Step> Iterator for Range<Idx> {
39        #[ensures(self.start.deep_model() >= self.end.deep_model() ==>
40            result == (0usize, Some(0usize)))]
41        #[ensures({
42            let s = self.end.deep_model() - self.start.deep_model();
43            s >= 0 && s <= usize::MAX@ ==>
44            result.0@ == s && result.1 == Some(result.0)
45        })]
46        #[ensures(self.end.deep_model() - self.start.deep_model() > usize::MAX@ ==>
47            result == (usize::MAX, None))]
48        fn size_hint(&self) -> (usize, Option<usize>);
49    }
50}
51
52macro_rules! impl_exact_size_range {
53    ($($t:ty)*) => ($(
54        impl ExactSizeIteratorSpec for Range<$t> {
55            #[logic(law)]
56            #[requires(Self::size_hint.postcondition((self,), r))]
57            #[ensures(r.1 == Some(r.0))]
58            #[allow(unused_variables)]
59            fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
60        }
61    )*)
62}
63
64impl_exact_size_range! { i8 u8 i16 u16 isize usize }
65
66// Apparently, `ExactSizeIterator` is not implemented for `Range<i64>` and `Range<u64>` even
67// on 64-bit platforms.
68#[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))]
69impl_exact_size_range! { i32 u32 }
70
71#[cfg(feature = "nightly")]
72impl<Idx: DeepModel<DeepModelTy = Int> + Step> DoubleEndedIteratorSpec for Range<Idx> {
73    #[logic(open)]
74    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
75        pearlite! {
76            self.start == o.start && self.end.deep_model() >= o.end.deep_model()
77            && (visited.len() > 0 ==> o.end.deep_model() >= o.start.deep_model())
78            && visited.len() == self.end.deep_model() - o.end.deep_model()
79            && forall<i> 0 <= i && i < visited.len() ==>
80                visited[i].deep_model() == self.end.deep_model() - i - 1
81        }
82    }
83
84    #[logic(open, prophetic)]
85    fn completed_back(&mut self) -> bool {
86        self.completed()
87    }
88
89    #[logic(law)]
90    #[ensures(self.produces_back(Seq::empty(), self))]
91    fn produces_back_refl(self) {}
92
93    #[logic(law)]
94    #[requires(a.produces_back(ab, b))]
95    #[requires(b.produces_back(bc, c))]
96    #[ensures(a.produces_back(ab.concat(bc), c))]
97    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
98
99    #[logic(law)]
100    #[requires(Self::size_hint.postcondition((self,), r))]
101    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
102        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
103    #[ensures(match r.1 {
104        Some(r) => {
105            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
106        }
107        None => true
108    })]
109    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
110}
111
112#[logic(open)]
113#[ensures(r.is_empty_log() == (result == 0))]
114pub fn range_inclusive_len<Idx: DeepModel<DeepModelTy = Int>>(r: RangeInclusive<Idx>) -> Int {
115    if r.is_empty_log() { 0 } else { r.end_log().deep_model() - r.start_log().deep_model() + 1 }
116}
117
118#[cfg(feature = "nightly")]
119impl<Idx: DeepModel<DeepModelTy = Int> + Step> IteratorSpec for RangeInclusive<Idx> {
120    #[logic(open, prophetic)]
121    fn completed(&mut self) -> bool {
122        pearlite! {
123            self.is_empty_log() && (^self).is_empty_log()
124        }
125    }
126
127    #[logic(open)]
128    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
129        pearlite! {
130            visited.len() == range_inclusive_len(self) - range_inclusive_len(o) &&
131            (self.is_empty_log() ==> o.is_empty_log()) &&
132            (o.is_empty_log() || self.end_log() == o.end_log()) &&
133            forall<i> 0 <= i && i < visited.len() ==>
134                visited[i].deep_model() == self.start_log().deep_model() + i
135        }
136    }
137
138    #[logic(law)]
139    #[ensures(self.produces(Seq::empty(), self))]
140    fn produces_refl(self) {}
141
142    #[logic(law)]
143    #[requires(a.produces(ab, b))]
144    #[requires(b.produces(bc, c))]
145    #[ensures(a.produces(ab.concat(bc), c))]
146    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
147}
148
149extern_spec! {
150    impl<Idx: DeepModel<DeepModelTy = Int> + Step> Iterator for RangeInclusive<Idx> {
151        #[ensures({
152            let s = range_inclusive_len(*self);
153            s <= usize::MAX@ ==> result.0@ == s && result.1 == Some(result.0)
154        })]
155        #[ensures(range_inclusive_len(*self) > usize::MAX@ ==>
156            result == (usize::MAX, None))]
157        fn size_hint(&self) -> (usize, Option<usize>);
158    }
159}
160
161macro_rules! impl_exact_size_range_inclusive {
162    ($($t:ty)*) => ($(
163        impl ExactSizeIteratorSpec for RangeInclusive<$t> {
164            #[logic(law)]
165            #[requires(Self::size_hint.postcondition((self,), r))]
166            #[ensures(r.1 == Some(r.0))]
167            #[allow(unused_variables)]
168            fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
169        }
170    )*)
171}
172
173impl_exact_size_range_inclusive! { i8 u8 }
174
175#[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))]
176impl_exact_size_range_inclusive! { i16 u16 }
177
178#[cfg(feature = "nightly")]
179impl<Idx: DeepModel<DeepModelTy = Int> + Step> DoubleEndedIteratorSpec for RangeInclusive<Idx> {
180    #[logic(open)]
181    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
182        pearlite! {
183            visited.len() == range_inclusive_len(self) - range_inclusive_len(o) &&
184            (self.is_empty_log() ==> o.is_empty_log()) &&
185            (o.is_empty_log() || self.start_log() == o.start_log()) &&
186            forall<i> 0 <= i && i < visited.len() ==>
187                visited[i].deep_model() == self.end_log().deep_model() - i
188        }
189    }
190
191    #[logic(open, prophetic)]
192    fn completed_back(&mut self) -> bool {
193        self.completed()
194    }
195
196    #[logic(law)]
197    #[ensures(self.produces_back(Seq::empty(), self))]
198    fn produces_back_refl(self) {}
199
200    #[logic(law)]
201    #[requires(a.produces_back(ab, b))]
202    #[requires(b.produces_back(bc, c))]
203    #[ensures(a.produces_back(ab.concat(bc), c))]
204    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
205
206    #[logic(law)]
207    #[requires(Self::size_hint.postcondition((self,), r))]
208    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
209        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
210    #[ensures(match r.1 {
211        Some(r) => {
212            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
213        }
214        None => true
215    })]
216    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
217}
218
219/// Dummy impls that don't use the unstable trait Step
220#[cfg(not(feature = "nightly"))]
221macro_rules! impl_range {
222    ( $( $ty:tt ),+ ) => {
223        $(
224            impl IteratorSpec for Range<$ty> {}
225            impl IteratorSpec for RangeInclusive<$ty> {}
226            impl DoubleEndedIteratorSpec for Range<$ty> {}
227            impl DoubleEndedIteratorSpec for RangeInclusive<$ty> {}
228        )+
229    };
230}
231
232#[cfg(not(feature = "nightly"))]
233impl_range! { char, i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize }
creusot_std/std/iter/range.rs

creusot_std/std/iter/
range.rs
