1use crate::prelude::*;
2use core::iter::*;
3
4mod chain;
5mod cloned;
6mod copied;
7mod empty;
8mod enumerate;
9mod filter;
10mod filter_map;
11mod fuse;
12mod map;
13mod map_inv;
14mod once;
15mod range;
16mod repeat;
17mod rev;
18mod skip;
19mod take;
20mod zip;
21
22pub use chain::ChainExt;
23pub use cloned::ClonedExt;
24pub use copied::CopiedExt;
25pub use enumerate::EnumerateExt;
26pub use filter::FilterExt;
27pub use filter_map::FilterMapExt;
28pub use fuse::FusedIteratorSpec;
29pub use map::MapExt;
30pub use map_inv::MapInv;
31pub use rev::RevExt;
32pub use skip::SkipExt;
33pub use take::TakeExt;
34pub use zip::ZipExt;
35
36pub trait IteratorSpec: Iterator {
37 #[logic(prophetic)]
38 fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool;
39
40 #[logic(prophetic)]
41 fn completed(&mut self) -> bool;
42
43 #[logic(law, prophetic)]
44 #[ensures(self.produces(Seq::empty(), self))]
45 fn produces_refl(self);
46
47 #[logic(law, prophetic)]
48 #[requires(a.produces(ab, b))]
49 #[requires(b.produces(bc, c))]
50 #[ensures(a.produces(ab.concat(bc), c))]
51 fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self);
52
53 #[check(ghost)]
54 #[requires(forall<e, i2> self.produces(Seq::singleton(e), i2) && inv(e) ==>
55 func.precondition((e, Snapshot::new(Seq::empty()))))]
56 #[requires(MapInv::<Self, F>::reinitialize())]
57 #[requires(MapInv::<Self, F>::preservation(self, func))]
58 #[ensures(result == MapInv { iter: self, func, produced: Snapshot::new(Seq::empty())})]
59 fn map_inv<B, F>(self, func: F) -> MapInv<Self, F>
60 where
61 Self: Sized,
62 F: FnMut(Self::Item, Snapshot<Seq<Self::Item>>) -> B,
63 {
64 MapInv { iter: self, func, produced: snapshot! {Seq::empty()} }
65 }
66}
67
68pub trait ExactSizeIteratorSpec: ExactSizeIterator + IteratorSpec {
69 #[logic(law)]
70 #[requires(Self::size_hint.postcondition((self,), r))]
71 #[ensures(r.1 == Some(r.0))]
72 #[allow(unused_variables)]
73 fn size_hint_exact(&self, r: (usize, Option<usize>));
74}
75
76extern_spec! {
77 impl FromIterator<()> for () {
78 #[requires(T::into_iter.precondition((iter,)))]
79 #[ensures(exists<into_iter: T::IntoIter, prod: Seq<()>, done: &mut T::IntoIter>
80 T::into_iter.postcondition((iter,), into_iter) &&
81 into_iter.produces(prod, *done) && done.completed() && resolve(^done))]
82 fn from_iter<T: IntoIterator<Item = (), IntoIter: IteratorSpec>>(iter: T);
83 }
84}
85
86pub trait DoubleEndedIteratorSpec: DoubleEndedIterator + IteratorSpec {
87 #[logic(prophetic)]
88 fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool;
89
90 #[logic(prophetic)]
91 fn completed_back(&mut self) -> bool;
92
93 #[logic(law, prophetic)]
94 #[ensures(self.produces_back(Seq::empty(), self))]
95 fn produces_back_refl(self);
96
97 #[logic(law, prophetic)]
98 #[requires(a.produces_back(ab, b))]
99 #[requires(b.produces_back(bc, c))]
100 #[ensures(a.produces_back(ab.concat(bc), c))]
101 fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self);
102
103 #[logic(law)]
104 #[requires(Self::size_hint.postcondition((self,), r))]
105 #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
106 self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
107 #[ensures(match r.1 {
108 Some(r) => {
109 forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
110 }
111 None => true
112 })]
113 fn size_hint_back_spec(&self, r: (usize, Option<usize>));
114}
115
116extern_spec! {
117 mod core {
118 mod iter {
119 trait Iterator: IteratorSpec {
120 #[ensures(match result {
121 None => self.completed(),
122 Some(v) => (*self).produces(Seq::singleton(v), ^self)
123 })]
124 fn next(&mut self) -> Option<Self::Item>;
125
126 #[check(ghost)]
127 #[ensures(result.iter() == self && result.n() == n)]
128 fn skip(self, n: usize) -> Skip<Self>
129 where Self: Sized;
130
131 #[check(ghost)]
132 #[ensures(result.iter() == self && result.n() == n)]
133 fn take(self, n: usize) -> Take<Self>
134 where Self: Sized;
135
136 #[check(ghost)]
137 #[requires(U::into_iter.precondition((other,)))]
138 #[ensures(result.iter_a() == Some(self))]
139 #[ensures(match result.iter_b() {
140 Some(b) => U::into_iter.postcondition((other,), b),
141 None => false
142 })]
143 fn chain<U: IntoIterator<Item = Self::Item>>(self, other: U) -> Chain<Self, U::IntoIter>
144 where Self: Sized;
145
146 #[check(ghost)]
147 #[ensures(result.iter() == self)]
148 fn cloned<'a, T: 'a + Clone>(self) -> Cloned<Self>
149 where Self: Sized + Iterator<Item = &'a T>;
150
151 #[check(ghost)]
152 #[ensures(result.iter() == self)]
153 fn copied<'a, T: 'a + Copy>(self) -> Copied<Self>
154 where Self: Sized + Iterator<Item = &'a T>;
155
156 #[check(ghost)]
157 #[requires(forall<e, i2> self.produces(Seq::singleton(e), i2) && inv(e) ==>
158 f.precondition((e,)))]
159 #[requires(map::reinitialize::<Self, B, F>())]
160 #[requires(map::preservation::<Self, B, F>(self, f))]
161 #[ensures(result.iter() == self && result.func() == f)]
162 fn map<B, F: FnMut(Self::Item) -> B>(self, f: F) -> Map<Self, F>
163 where Self: Sized;
164
165 #[check(ghost)]
166 #[requires(filter::immutable(f))]
167 #[requires(filter::no_precondition(f))]
168 #[requires(filter::precise(f))]
169 #[ensures(result.iter() == self && result.func() == f)]
170 fn filter<P: for<'a> FnMut(&Self::Item) -> bool>(self, f: P) -> Filter<Self, P>
171 where Self: Sized;
172
173 #[check(ghost)]
174 #[requires(filter_map::immutable(f))]
175 #[requires(filter_map::no_precondition(f))]
176 #[requires(filter_map::precise(f))]
177 #[ensures(result.iter() == self && result.func() == f)]
178 fn filter_map<B, F: for<'a> FnMut(Self::Item) -> Option<B>>(self, f: F) -> FilterMap<Self, F>
179 where Self: Sized;
180
181 #[check(ghost)]
182 #[requires(forall<i: &mut Self> i.completed() ==> (*i).produces(Seq::empty(), ^i))]
184 #[requires(forall<s: Seq<Self::Item>, i: Self> self.produces(s, i) ==> s.len() < core::usize::MAX@)]
185 #[ensures(result.iter() == self && result.n()@ == 0)]
186 fn enumerate(self) -> Enumerate<Self>
187 where Self: Sized;
188
189 #[check(ghost)]
190 #[ensures(result@ == Some(self))]
191 fn fuse(self) -> Fuse<Self>
192 where Self: Sized;
193
194 #[check(ghost)]
195 #[requires(U::into_iter.precondition((other,)))]
196 #[ensures(result.iter_a() == self)]
197 #[ensures(U::into_iter.postcondition((other,), result.iter_b()))]
198 fn zip<U: IntoIterator>(self, other: U) -> Zip<Self, U::IntoIter>
199 where Self: Sized;
200
201 #[requires(B::from_iter.precondition((self,)))]
202 #[ensures(B::from_iter.postcondition((self,), result))]
203 fn collect<B: FromIterator<Self::Item>>(self) -> B
204 where Self: Sized
205 {
206 FromIterator::from_iter(self)
207 }
208
209 #[check(ghost)]
210 #[ensures(result.iter() == self)]
211 fn rev(self) -> Rev<Self>
212 where Self: Sized + DoubleEndedIteratorSpec;
213
214 #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
215 self.produces(s, *i) && i.completed() ==> result.0@ <= s.len())]
216 #[ensures(match result.1 {
217 Some(r) => {
218 forall<s: Seq<Self::Item>, i: Self> self.produces(s, i) ==> s.len() <= r@
219 }
220 None => true
221 })]
222 fn size_hint(&self) -> (usize, Option<usize>) {
223 (0, None)
224 }
225 }
226
227 trait FromIterator<A>: Sized {
228 #[requires(T::into_iter.precondition((iter,)))]
229 fn from_iter<T>(iter: T) -> Self
230 where T: IntoIterator<Item = A>;
231 }
232
233 trait ExactSizeIterator: ExactSizeIteratorSpec {
234 #[ensures(Self::size_hint.postcondition((self,), (result, Some(result))))]
235 fn len(&self) -> usize {
236 snapshot!(Self::size_hint_exact);
237 let (lower, upper) = self.size_hint();
238 assert_eq!(upper, Some(lower));
239 lower
240 }
241
242 #[ensures(exists<l> Self::size_hint.postcondition((self,), (l, Some(l))) && result == (l == 0usize))]
243 fn is_empty(&self) -> bool {
244 self.len() == 0
245 }
246 }
247
248 #[check(ghost)]
249 fn empty<T>() -> Empty<T>;
250
251 #[check(ghost)]
252 #[ensures(result@ == Some(value))]
253 fn once<T>(value: T) -> Once<T>;
254
255 #[check(ghost)]
256 #[ensures(result@ == elt)]
257 fn repeat<T: Clone>(elt: T) -> Repeat<T>;
258
259 trait DoubleEndedIterator: DoubleEndedIteratorSpec {
260 #[ensures(match result {
261 None => self.completed_back(),
262 Some(v) => (*self).produces_back(Seq::singleton(v), ^self)
263 })]
264 fn next_back(&mut self) -> Option<Self::Item>;
265 }
266 }
267 }
268
269 impl<I: Iterator> IntoIterator for I {
270 #[check(ghost)]
271 #[ensures(result == self)]
272 fn into_iter(self) -> I;
273 }
274}
275
276impl<I: IteratorSpec + ?Sized> IteratorSpec for &mut I {
277 #[logic(open, prophetic)]
278 fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
279 pearlite! { (*self).produces(visited, *o) && ^self == ^o }
280 }
281
282 #[logic(open, prophetic)]
283 fn completed(&mut self) -> bool {
284 pearlite! { (*self).completed() && ^*self == ^^self }
285 }
286
287 #[logic(law)]
288 #[ensures(self.produces(Seq::empty(), self))]
289 fn produces_refl(self) {}
290
291 #[logic(law)]
292 #[requires(a.produces(ab, b))]
293 #[requires(b.produces(bc, c))]
294 #[ensures(a.produces(ab.concat(bc), c))]
295 fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
296}
297
298extern_spec! {
299 impl<I: Iterator + ?Sized> Iterator for &mut I {
300 #[ensures(I::size_hint.postcondition((&*self,), result))]
301 fn size_hint(&self) -> (usize, Option<usize>);
302 }
303}
304
305impl<I: ExactSizeIteratorSpec + ?Sized> ExactSizeIteratorSpec for &mut I {
306 #[logic(law)]
307 #[requires(Self::size_hint.postcondition((self,), r))]
308 #[ensures(r.1 == Some(r.0))]
309 fn size_hint_exact(&self, r: (usize, Option<usize>)) {
310 (**self).size_hint_exact(r)
311 }
312}