creusot_std/std/
iter.rs

1use crate::prelude::*;
2use core::iter::*;
3
4mod cloned;
5mod copied;
6mod empty;
7mod enumerate;
8mod filter;
9mod filter_map;
10mod fuse;
11mod map;
12mod map_inv;
13mod once;
14mod range;
15mod repeat;
16mod rev;
17mod skip;
18mod take;
19mod zip;
20
21pub use cloned::ClonedExt;
22pub use copied::CopiedExt;
23pub use enumerate::EnumerateExt;
24pub use filter::FilterExt;
25pub use filter_map::FilterMapExt;
26pub use fuse::FusedIterator;
27pub use map::MapExt;
28pub use map_inv::MapInv;
29pub use rev::RevExt;
30pub use skip::SkipExt;
31pub use take::TakeExt;
32pub use zip::ZipExt;
33
34pub trait IteratorSpec: Iterator {
35    #[logic(prophetic)]
36    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool;
37
38    #[logic(prophetic)]
39    fn completed(&mut self) -> bool;
40
41    #[logic(law)]
42    #[ensures(self.produces(Seq::empty(), self))]
43    fn produces_refl(self);
44
45    #[logic(law)]
46    #[requires(a.produces(ab, b))]
47    #[requires(b.produces(bc, c))]
48    #[ensures(a.produces(ab.concat(bc), c))]
49    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self);
50
51    #[check(ghost)]
52    #[requires(forall<e, i2>
53                    self.produces(Seq::singleton(e), i2) ==>
54                    func.precondition((e, Snapshot::new(Seq::empty()))))]
55    #[requires(MapInv::<Self, F>::reinitialize())]
56    #[requires(MapInv::<Self, F>::preservation(self, func))]
57    #[ensures(result == MapInv { iter: self, func, produced: Snapshot::new(Seq::empty())})]
58    fn map_inv<B, F>(self, func: F) -> MapInv<Self, F>
59    where
60        Self: Sized,
61        F: FnMut(Self::Item, Snapshot<Seq<Self::Item>>) -> B,
62    {
63        MapInv { iter: self, func, produced: snapshot! {Seq::empty()} }
64    }
65}
66
67pub trait FromIteratorSpec<A>: FromIterator<A> {
68    #[logic]
69    fn from_iter_post(prod: Seq<A>, res: Self) -> bool;
70}
71
72impl FromIteratorSpec<()> for () {
73    #[logic(open)]
74    fn from_iter_post(_: Seq<()>, _res: Self) -> bool {
75        true
76    }
77}
78
79pub trait DoubleEndedIteratorSpec: DoubleEndedIterator + IteratorSpec {
80    #[logic(prophetic)]
81    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool;
82
83    #[logic(law)]
84    #[ensures(self.produces_back(Seq::empty(), self))]
85    fn produces_back_refl(self);
86
87    #[logic(law)]
88    #[requires(a.produces_back(ab, b))]
89    #[requires(b.produces_back(bc, c))]
90    #[ensures(a.produces_back(ab.concat(bc), c))]
91    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self);
92}
93
94extern_spec! {
95    mod core {
96        mod iter {
97            trait Iterator
98                where Self: IteratorSpec {
99
100                #[ensures(match result {
101                    None => self.completed(),
102                    Some(v) => (*self).produces(Seq::singleton(v), ^self)
103                })]
104                fn next(&mut self) -> Option<Self::Item>;
105
106                #[check(ghost)]
107                #[ensures(result.iter() == self && result.n() == n)]
108                fn skip(self, n: usize) -> Skip<Self>
109                    where Self: Sized;
110
111                #[check(ghost)]
112                #[ensures(result.iter() == self && result.n() == n)]
113                fn take(self, n: usize) -> Take<Self>
114                    where Self: Sized;
115
116                #[check(ghost)]
117                #[ensures(result.iter() == self)]
118                fn cloned<'a, T>(self) -> Cloned<Self>
119                    where T: 'a + Clone,
120                        Self: Sized + Iterator<Item = &'a T>;
121
122                #[check(ghost)]
123                #[ensures(result.iter() == self)]
124                fn copied<'a, T>(self) -> Copied<Self>
125                    where T: 'a + Copy,
126                        Self: Sized + Iterator<Item = &'a T>;
127
128                #[check(ghost)]
129                #[requires(forall<e, i2>
130                                self.produces(Seq::singleton(e), i2) ==>
131                                f.precondition((e,)))]
132                #[requires(map::reinitialize::<Self, B, F>())]
133                #[requires(map::preservation::<Self, B, F>(self, f))]
134                #[ensures(result.iter() == self && result.func() == f)]
135                fn map<B, F>(self, f: F) -> Map<Self, F>
136                    where Self: Sized, F: FnMut(Self::Item) -> B;
137
138                #[check(ghost)]
139                #[requires(filter::immutable(f))]
140                #[requires(filter::no_precondition(f))]
141                #[requires(filter::precise(f))]
142                #[ensures(result.iter() == self && result.func() == f)]
143                fn filter<P>(self, f: P) -> Filter<Self, P>
144                    where Self: Sized, P: for<'a> FnMut(&Self::Item) -> bool;
145
146                #[check(ghost)]
147                #[requires(filter_map::immutable(f))]
148                #[requires(filter_map::no_precondition(f))]
149                #[requires(filter_map::precise(f))]
150                #[ensures(result.iter() == self && result.func() == f)]
151                fn filter_map<B, F>(self, f: F) -> FilterMap<Self, F>
152                    where Self: Sized, F: for<'a> FnMut(Self::Item) -> Option<B>;
153
154                #[check(ghost)]
155                // These two requirements are here only to prove the absence of overflows
156                #[requires(forall<i: &mut Self> (*i).completed() ==> (*i).produces(Seq::empty(), ^i))]
157                #[requires(forall<s: Seq<Self::Item>, i: Self> self.produces(s, i) ==> s.len() < core::usize::MAX@)]
158                #[ensures(result.iter() == self && result.n()@ == 0)]
159                fn enumerate(self) -> Enumerate<Self>
160                    where Self: Sized;
161
162                #[check(ghost)]
163                #[ensures(result@ == Some(self))]
164                fn fuse(self) -> Fuse<Self>
165                    where Self: Sized;
166
167                #[check(ghost)]
168                #[requires(U::into_iter.precondition((other,)))]
169                #[ensures(result.itera() == self)]
170                #[ensures(U::into_iter.postcondition((other,), result.iterb()))]
171                fn zip<U: IntoIterator>(self, other: U) -> Zip<Self, U::IntoIter>
172                    where Self: Sized, U::IntoIter: Iterator;
173
174                #[ensures(exists<done: &mut Self, prod>
175                    resolve(^done) && done.completed() && self.produces(prod, *done) && B::from_iter_post(prod, result))]
176                fn collect<B>(self) -> B
177                    where Self: Sized, B: FromIteratorSpec<Self::Item>;
178
179                #[check(ghost)]
180                #[ensures(result.iter() == self)]
181                fn rev(self) -> Rev<Self>
182                    where Self: Sized + DoubleEndedIteratorSpec;
183            }
184
185            trait FromIterator<A>
186                where Self: FromIteratorSpec<A> {
187
188                #[requires(T::into_iter.precondition((iter,)))]
189                #[ensures(exists<into_iter: T::IntoIter, done: &mut T::IntoIter, prod: Seq<A>>
190                            T::into_iter.postcondition((iter,), into_iter) &&
191                            into_iter.produces(prod, *done) && done.completed() && resolve(^done) &&
192                            Self::from_iter_post(prod, result))]
193                fn from_iter<T>(iter: T) -> Self
194                    where Self: Sized, T: IntoIterator<Item = A>, T::IntoIter: IteratorSpec;
195            }
196
197            #[check(ghost)]
198            fn empty<T>() -> Empty<T>;
199
200            #[check(ghost)]
201            #[ensures(result@ == Some(value))]
202            fn once<T>(value: T) -> Once<T>;
203
204            #[check(ghost)]
205            #[ensures(result@ == elt)]
206            fn repeat<T: Clone>(elt: T) -> Repeat<T>;
207
208            trait DoubleEndedIterator
209                where Self: DoubleEndedIteratorSpec {
210                #[ensures(match result {
211                    None => self.completed(),
212                    Some(v) => (*self).produces_back(Seq::singleton(v), ^self)
213                })]
214                fn next_back(&mut self) -> Option<Self::Item>;
215            }
216        }
217    }
218
219    impl<I: Iterator> IntoIterator for I {
220        #[check(ghost)]
221        #[ensures(result == self)]
222        fn into_iter(self) -> I;
223    }
224}
225
226impl<I: IteratorSpec + ?Sized> IteratorSpec for &mut I {
227    #[logic(open, prophetic)]
228    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
229        pearlite! { (*self).produces(visited, *o) && ^self == ^o }
230    }
231
232    #[logic(open, prophetic)]
233    fn completed(&mut self) -> bool {
234        pearlite! { (*self).completed() && ^*self == ^^self }
235    }
236
237    #[logic(open, law)]
238    #[ensures(self.produces(Seq::empty(), self))]
239    fn produces_refl(self) {}
240
241    #[logic(open, law)]
242    #[requires(a.produces(ab, b))]
243    #[requires(b.produces(bc, c))]
244    #[ensures(a.produces(ab.concat(bc), c))]
245    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
246}
creusot_std/std/iter.rs

creusot_std/std/
iter.rs
