creusot_contracts/std/
iter.rs

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

creusot_contracts/std/
iter.rs
