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]).postcondition_mut((s[i], Snapshot::new(self.produced.concat(s.subsequence(0, i)))), ^fs[i], visited[i])
43 }
44 }
45}
46
47impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> Invariant
48 for MapInv<I, F>
49{
50 #[logic(open, prophetic)]
51 fn invariant(self) -> bool {
52 pearlite! {
53 Self::reinitialize() &&
54 Self::preservation_inv(self.iter, self.func, *self.produced) &&
55 Self::next_precondition(self.iter, self.func, *self.produced)
56 }
57 }
58}
59
60impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> core::iter::Iterator
61 for MapInv<I, F>
62{
63 type Item = B;
64
65 #[ensures(match result {
66 None => self.completed(),
67 Some(v) => (*self).produces_one(v, ^self)
68 })]
69 fn next(&mut self) -> Option<Self::Item> {
70 let old_self: Snapshot<Self> = snapshot! { *self };
71 match self.iter.next() {
72 Some(v) => {
73 proof_assert! { self.func.precondition((v, self.produced)) };
74 let produced = snapshot! { self.produced.push_back(v) };
75 let r = (self.func)(v, self.produced);
76 self.produced = produced;
77 #[allow(path_statements)]
78 let _ = snapshot! { Self::produces_one_invariant };
79 proof_assert! { old_self.produces_one(r, *self) };
80 let _ = self; Some(r)
82 }
83 None => {
84 self.produced = snapshot! { Seq::empty() };
85 None
86 }
87 }
88 }
89}
90
91impl<I: IteratorSpec, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> MapInv<I, F> {
92 #[logic(open, prophetic, inline)]
93 pub fn next_precondition(iter: I, func: F, produced: Seq<I::Item>) -> bool {
94 pearlite! {
95 forall<e: I::Item, i: I>
96 inv(e) && iter.produces(Seq::singleton(e), i) ==>
97 func.precondition((e, Snapshot::new(produced)))
98 }
99 }
100
101 #[logic(prophetic)]
102 #[ensures(produced == Seq::empty() ==> result == Self::preservation(iter, func))]
103 pub fn preservation_inv(iter: I, func: F, produced: Seq<I::Item>) -> bool {
104 pearlite! {
105 forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
106 func.hist_inv(*f) ==>
107 inv(s) && inv(e1) && inv(e2) && inv(f) ==>
108 iter.produces(s.push_back(e1).push_back(e2), i) ==>
109 (*f).postcondition_mut((e1, Snapshot::new(produced.concat(s))), ^f, b) ==>
110 (^f).precondition((e2, Snapshot::new(produced.concat(s).push_back(e1))))
111 }
112 }
113
114 #[logic(open, prophetic, inline)]
115 pub fn preservation(iter: I, func: F) -> bool {
116 pearlite! {
117 forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
118 func.hist_inv(*f) ==>
119 inv(s) && inv(e1) && inv(e2) && inv(f) ==>
120 iter.produces(s.push_back(e1).push_back(e2), i) ==>
121 (*f).postcondition_mut((e1, Snapshot::new(s)), ^f, b) ==>
122 (^f).precondition((e2, Snapshot::new(s.push_back(e1))))
123 }
124 }
125
126 #[logic(open, prophetic, inline)]
127 pub fn reinitialize() -> bool {
128 pearlite! {
129 forall<iter: &mut I, func: F>
130 iter.completed() ==>
131 Self::next_precondition(^iter, func, Seq::empty()) &&
132 Self::preservation(^iter, func)
133 }
134 }
135
136 #[logic]
137 #[requires(inv(e) && inv(f))]
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).postcondition_mut((e, self.produced), ^f, visited)
161 }
162 }
163}