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

creusot_std/std/
iter.rs
