creusot_contracts/std/iter/
map_inv.rs

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

creusot_contracts/std/iter/
map_inv.rs
