creusot_std/std/
iter.rs

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
120                where Self: IteratorSpec {
121
122                #[ensures(match result {
123                    None => self.completed(),
124                    Some(v) => (*self).produces(Seq::singleton(v), ^self)
125                })]
126                fn next(&mut self) -> Option<Self::Item>;
127
128                #[check(ghost)]
129                #[ensures(result.iter() == self && result.n() == n)]
130                fn skip(self, n: usize) -> Skip<Self>
131                    where Self: Sized;
132
133                #[check(ghost)]
134                #[ensures(result.iter() == self && result.n() == n)]
135                fn take(self, n: usize) -> Take<Self>
136                    where Self: Sized;
137
138                #[check(ghost)]
139                #[requires(U::into_iter.precondition((other,)))]
140                #[ensures(result.iter_a() == Some(self))]
141                #[ensures(match result.iter_b() {
142                    Some(b) => U::into_iter.postcondition((other,), b),
143                    None => false
144                })]
145                fn chain<U>(self, other: U) -> Chain<Self, U::IntoIter>
146                    where Self: Sized, U: IntoIterator<Item = Self::Item>;
147
148                #[check(ghost)]
149                #[ensures(result.iter() == self)]
150                fn cloned<'a, T>(self) -> Cloned<Self>
151                    where T: 'a + Clone,
152                        Self: Sized + Iterator<Item = &'a T>;
153
154                #[check(ghost)]
155                #[ensures(result.iter() == self)]
156                fn copied<'a, T>(self) -> Copied<Self>
157                    where T: 'a + Copy,
158                        Self: Sized + Iterator<Item = &'a T>;
159
160                #[check(ghost)]
161                #[requires(forall<e, i2> self.produces(Seq::singleton(e), i2) && inv(e) ==>
162                                f.precondition((e,)))]
163                #[requires(map::reinitialize::<Self, B, F>())]
164                #[requires(map::preservation::<Self, B, F>(self, f))]
165                #[ensures(result.iter() == self && result.func() == f)]
166                fn map<B, F>(self, f: F) -> Map<Self, F>
167                    where Self: Sized, F: FnMut(Self::Item) -> B;
168
169                #[check(ghost)]
170                #[requires(filter::immutable(f))]
171                #[requires(filter::no_precondition(f))]
172                #[requires(filter::precise(f))]
173                #[ensures(result.iter() == self && result.func() == f)]
174                fn filter<P>(self, f: P) -> Filter<Self, P>
175                    where Self: Sized, P: for<'a> FnMut(&Self::Item) -> bool;
176
177                #[check(ghost)]
178                #[requires(filter_map::immutable(f))]
179                #[requires(filter_map::no_precondition(f))]
180                #[requires(filter_map::precise(f))]
181                #[ensures(result.iter() == self && result.func() == f)]
182                fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F>
183                    where Self: Sized, F: for<'a> FnMut(Self::Item) -> Option<B>;
184
185                #[check(ghost)]
186                // These two requirements are here only to prove the absence of overflows
187                #[requires(forall<i: &mut Self> i.completed() ==> (*i).produces(Seq::empty(), ^i))]
188                #[requires(forall<s: Seq<Self::Item>, i: Self> self.produces(s, i) ==> s.len() < core::usize::MAX@)]
189                #[ensures(result.iter() == self && result.n()@ == 0)]
190                fn enumerate(self) -> Enumerate<Self>
191                    where Self: Sized;
192
193                #[check(ghost)]
194                #[ensures(result@ == Some(self))]
195                fn fuse(self) -> Fuse<Self>
196                    where Self: Sized;
197
198                #[check(ghost)]
199                #[requires(U::into_iter.precondition((other,)))]
200                #[ensures(result.iter_a() == self)]
201                #[ensures(U::into_iter.postcondition((other,), result.iter_b()))]
202                fn zip<U: IntoIterator>(self, other: U) -> Zip<Self, U::IntoIter>
203                    where Self: Sized, U::IntoIter: Iterator;
204
205                #[requires(B::from_iter.precondition((self,)))]
206                #[ensures(B::from_iter.postcondition((self,), result))]
207                // FIXME: Self_
208                fn collect<B: FromIterator<Self_::Item>>(self) -> B
209                    where Self: Sized
210                {
211                    FromIterator::from_iter(self)
212                }
213
214                #[check(ghost)]
215                #[ensures(result.iter() == self)]
216                fn rev(self) -> Rev<Self>
217                    where Self: Sized + DoubleEndedIteratorSpec;
218
219                #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
220                    self.produces(s, *i) && i.completed() ==> result.0@ <= s.len())]
221                #[ensures(match result.1 {
222                    Some(r) => {
223                        forall<s: Seq<Self::Item>, i: Self> self.produces(s, i) ==> s.len() <= r@
224                    }
225                    None => true
226                })]
227                fn size_hint(&self) -> (usize, Option<usize>) {
228                    (0, None)
229                }
230            }
231
232            trait FromIterator<A>: Sized {
233                #[requires(T::into_iter.precondition((iter,)))]
234                fn from_iter<T>(iter: T) -> Self
235                    where T: IntoIterator<Item = A>;
236            }
237
238            trait ExactSizeIterator where Self: ExactSizeIteratorSpec {
239                #[ensures(Self::size_hint.postcondition((self,), (result, Some(result))))]
240                fn len(&self) -> usize {
241                    // FIXME: Self_
242                    snapshot!(Self_::size_hint_exact);
243                    let (lower, upper) = self.size_hint();
244                    assert_eq!(upper, Some(lower));
245                    lower
246                }
247
248                #[ensures(exists<l> Self::size_hint.postcondition((self,), (l, Some(l))) && result == (l == 0usize))]
249                fn is_empty(&self) -> bool {
250                    self.len() == 0
251                }
252            }
253
254            #[check(ghost)]
255            fn empty<T>() -> Empty<T>;
256
257            #[check(ghost)]
258            #[ensures(result@ == Some(value))]
259            fn once<T>(value: T) -> Once<T>;
260
261            #[check(ghost)]
262            #[ensures(result@ == elt)]
263            fn repeat<T: Clone>(elt: T) -> Repeat<T>;
264
265            trait DoubleEndedIterator
266                where Self: DoubleEndedIteratorSpec {
267                #[ensures(match result {
268                    None => self.completed_back(),
269                    Some(v) => (*self).produces_back(Seq::singleton(v), ^self)
270                })]
271                fn next_back(&mut self) -> Option<Self::Item>;
272            }
273        }
274    }
275
276    impl<I: Iterator> IntoIterator for I {
277        #[check(ghost)]
278        #[ensures(result == self)]
279        fn into_iter(self) -> I;
280    }
281}
282
283impl<I: IteratorSpec + ?Sized> IteratorSpec for &mut I {
284    #[logic(open, prophetic)]
285    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
286        pearlite! { (*self).produces(visited, *o) && ^self == ^o }
287    }
288
289    #[logic(open, prophetic)]
290    fn completed(&mut self) -> bool {
291        pearlite! { (*self).completed() && ^*self == ^^self }
292    }
293
294    #[logic(law)]
295    #[ensures(self.produces(Seq::empty(), self))]
296    fn produces_refl(self) {}
297
298    #[logic(law)]
299    #[requires(a.produces(ab, b))]
300    #[requires(b.produces(bc, c))]
301    #[ensures(a.produces(ab.concat(bc), c))]
302    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
303}
304
305extern_spec! {
306    impl<I: Iterator + ?Sized> Iterator for &mut I {
307        #[ensures(I::size_hint.postcondition((&*self,), result))]
308        fn size_hint(&self) -> (usize, Option<usize>);
309    }
310}
311
312impl<I: ExactSizeIteratorSpec + ?Sized> ExactSizeIteratorSpec for &mut I {
313    #[logic(law)]
314    #[requires(Self::size_hint.postcondition((self,), r))]
315    #[ensures(r.1 == Some(r.0))]
316    fn size_hint_exact(&self, r: (usize, Option<usize>)) {
317        (**self).size_hint_exact(r)
318    }
319}
creusot_std/std/iter.rs

creusot_std/std/
iter.rs
