creusot_std/std/iter/
map_inv.rs

1use crate::{invariant::Invariant, prelude::*, std::iter::ExactSizeIteratorSpec};
2use core::iter::Iterator;
3
4pub struct MapInv<I: Iterator, F> {
5    pub iter: I,
6    pub func: F,
7    pub produced: Snapshot<Seq<I::Item>>,
8}
9
10impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> IteratorSpec
11    for MapInv<I, F>
12{
13    #[logic(open, prophetic)]
14    fn completed(&mut self) -> bool {
15        pearlite! {
16            *(^self).produced == Seq::empty() &&
17            self.iter.completed() && self.func == (^self).func
18        }
19    }
20
21    #[logic(law)]
22    #[ensures(self.produces(Seq::empty(), self))]
23    fn produces_refl(self) {}
24
25    #[logic(law)]
26    #[requires(a.produces(ab, b))]
27    #[requires(b.produces(bc, c))]
28    #[ensures(a.produces(ab.concat(bc), c))]
29    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
30
31    #[logic(open, prophetic, inline)]
32    fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool {
33        pearlite! {
34            self.func.hist_inv(succ.func)
35            && exists<fs: Seq<&mut F>> fs.len() == visited.len()
36            && exists<s: Seq<I::Item>> s.len() == visited.len() && self.iter.produces(s, succ.iter)
37            && succ.produced.inner() == self.produced.concat(s)
38            && (forall<i> 1 <= i && i < fs.len() ==>  ^fs[i - 1] == * fs[i])
39            && if visited.len() == 0 { self.func == succ.func }
40               else { *fs[0] == self.func &&  ^fs[visited.len() - 1] == succ.func }
41            && forall<i> 0 <= i && i < visited.len() ==>
42                 self.func.hist_inv(*fs[i])
43                 && (*fs[i]).postcondition_mut((s[i], Snapshot::new(self.produced.concat(s.subsequence(0, i)))), ^fs[i], visited[i])
44        }
45    }
46}
47
48impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> Invariant
49    for MapInv<I, F>
50{
51    #[logic(open, prophetic)]
52    fn invariant(self) -> bool {
53        pearlite! {
54            Self::reinitialize() &&
55            Self::preservation_inv(self.iter, self.func, *self.produced) &&
56            Self::next_precondition(self.iter, self.func, *self.produced)
57        }
58    }
59}
60
61impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> Iterator for MapInv<I, F> {
62    type Item = B;
63
64    #[ensures(match result {
65        None => self.completed(),
66        Some(v) => (*self).produces_one(v, ^self)
67    })]
68    fn next(&mut self) -> Option<Self::Item> {
69        let _old_self: Snapshot<Self> = snapshot! { *self };
70        match self.iter.next() {
71            Some(v) => {
72                proof_assert! { self.func.precondition((v, self.produced)) };
73                let produced = snapshot! { self.produced.push_back(v) };
74                let r = (self.func)(v, self.produced);
75                self.produced = produced;
76                #[allow(path_statements)]
77                let _ = snapshot! { Self::produces_one_invariant };
78                proof_assert! { _old_self.produces_one(r, *self) };
79                let _ = self; // Make sure self is not resolve until here.
80                Some(r)
81            }
82            None => {
83                self.produced = snapshot! { Seq::empty() };
84                None
85            }
86        }
87    }
88
89    #[ensures(I::size_hint.postcondition((&self.iter,), result))]
90    fn size_hint(&self) -> (usize, Option<usize>) {
91        self.iter.size_hint()
92    }
93}
94
95impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> MapInv<I, F> {
96    #[logic(open, prophetic, inline)]
97    pub fn next_precondition(iter: I, func: F, produced: Seq<I::Item>) -> bool {
98        pearlite! {
99            forall<e: I::Item, i: I>
100                inv(e) && iter.produces(Seq::singleton(e), i) ==>
101                func.precondition((e, Snapshot::new(produced)))
102        }
103    }
104
105    #[logic(prophetic)]
106    #[ensures(produced == Seq::empty() ==> result == Self::preservation(iter, func))]
107    pub fn preservation_inv(iter: I, func: F, produced: Seq<I::Item>) -> bool {
108        pearlite! {
109            forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
110                func.hist_inv(*f) ==>
111                inv(s) && inv(e1) && inv(e2) && inv(f) ==>
112                iter.produces(s.push_back(e1).push_back(e2), i) ==>
113                (*f).postcondition_mut((e1, Snapshot::new(produced.concat(s))), ^f, b) ==>
114                (^f).precondition((e2, Snapshot::new(produced.concat(s).push_back(e1))))
115        }
116    }
117
118    #[logic(open, prophetic, inline)]
119    pub fn preservation(iter: I, func: F) -> bool {
120        pearlite! {
121            forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
122                func.hist_inv(*f) ==>
123                inv(s) && inv(e1) && inv(e2) && inv(f) ==>
124                iter.produces(s.push_back(e1).push_back(e2), i) ==>
125                (*f).postcondition_mut((e1, Snapshot::new(s)), ^f, b) ==>
126                (^f).precondition((e2, Snapshot::new(s.push_back(e1))))
127        }
128    }
129
130    #[logic(open, prophetic, inline)]
131    pub fn reinitialize() -> bool {
132        pearlite! {
133            forall<iter: &mut I, func: F>
134                iter.completed() ==>
135                Self::next_precondition(^iter, func, Seq::empty()) &&
136                Self::preservation(^iter, func)
137        }
138    }
139
140    #[logic]
141    #[requires(inv(e) && inv(f))]
142    #[requires(self.invariant())]
143    #[requires(self.iter.produces(Seq::singleton(e), iter))]
144    #[requires(*f == self.func)]
145    #[requires((*f).postcondition_mut((e, self.produced), ^f, r) )]
146    #[ensures(Self::preservation_inv(iter, ^f, self.produced.push_back(e)))]
147    #[ensures(Self::next_precondition(iter, ^f, self.produced.push_back(e)))]
148    fn produces_one_invariant(self, e: I::Item, r: B, f: &mut F, iter: I) {
149        proof_assert! {
150            forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, i: I>
151                iter.produces(s.push_back(e1).push_back(e2), i) ==>
152                self.iter.produces(s.push_front(e).push_back(e1).push_back(e2), i)
153        }
154    }
155
156    #[logic(open, prophetic)]
157    #[ensures(result == self.produces(Seq::singleton(visited), succ))]
158    pub fn produces_one(self, visited: B, succ: Self) -> bool {
159        pearlite! {
160            exists<f: &mut F, e: I::Item>
161                *f == self.func && ^f == succ.func
162                && self.iter.produces(Seq::singleton(e), succ.iter)
163                && succ.produced.inner() == self.produced.push_back(e)
164                && (*f).postcondition_mut((e, self.produced), ^f, visited)
165        }
166    }
167}
168
169impl<I: ExactSizeIteratorSpec + IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B>
170    ExactSizeIterator for MapInv<I, F>
171{
172    #[ensures(Self::size_hint.postcondition((self,), (result, Some(result))))]
173    fn len(&self) -> usize {
174        self.iter.len()
175    }
176}
177
178impl<I: ExactSizeIteratorSpec + IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B>
179    ExactSizeIteratorSpec for MapInv<I, F>
180{
181    #[logic(law)]
182    #[requires(Self::size_hint.postcondition((self,), r))]
183    #[ensures(r.1 == Some(r.0))]
184    fn size_hint_exact(&self, r: (usize, Option<usize>)) {
185        self.iter.size_hint_exact(r)
186    }
187}
creusot_std/std/iter/map_inv.rs

creusot_std/std/iter/
map_inv.rs
