1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{prelude::*, std::iter::DoubleEndedIteratorSpec};
4use core::iter::Chain;
5
6pub trait ChainExt<A, B> {
7 #[logic]
8 fn iter_a(self) -> Option<A>;
9
10 #[logic]
11 fn iter_b(self) -> Option<B>;
12}
13
14impl<A, B> ChainExt<A, B> for Chain<A, B> {
15 #[logic(opaque)]
16 fn iter_a(self) -> Option<A> {
17 dead
18 }
19
20 #[logic(opaque)]
21 fn iter_b(self) -> Option<B> {
22 dead
23 }
24}
25
26impl<A, B> Resolve for Chain<A, B> {
27 #[logic(open, prophetic, inline)]
28 fn resolve(self) -> bool {
29 resolve(self.iter_a()) && resolve(self.iter_b())
30 }
31
32 #[trusted]
33 #[logic(prophetic)]
34 #[requires(structural_resolve(self))]
35 #[ensures(self.resolve())]
36 fn resolve_coherence(self) {}
37}
38
39impl<A, B> Invariant for Chain<A, B> {
40 #[logic(open, prophetic)]
41 fn invariant(self) -> bool {
42 inv(self.iter_a()) && inv(self.iter_b())
43 }
44}
45
46impl<A: IteratorSpec, B: IteratorSpec<Item = A::Item>> IteratorSpec for Chain<A, B> {
47 #[logic(open, prophetic)]
48 fn completed(&mut self) -> bool {
49 pearlite! {
50 (match self.iter_a() {
51 None => true,
52 Some(sa) => exists<a: &mut A> sa == *a && a.completed() && resolve(^a)
53 }) &&
54 (^self).iter_a() == None &&
55 (match self.iter_b() {
56 None => true,
57 Some(sb) => exists<b: &mut B> sb == *b && b.completed() && (^self).iter_b() == Some(^b)
58 })
59 }
60 }
61
62 #[logic(open, prophetic, inline)]
63 fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
64 pearlite! {
65 exists<visited_a: Seq<A::Item>, visited_b: Seq<B::Item>>
66 visited == visited_a.concat(visited_b) &&
67 chain_produces_inner(self, visited_a, visited_b, o)
68 }
69 }
70
71 #[logic(law)]
72 #[ensures(self.produces(Seq::empty(), self))]
73 fn produces_refl(self) {}
74
75 #[logic(law, prophetic)]
76 #[requires(x.produces(xy, y))]
77 #[requires(y.produces(yz, z))]
78 #[ensures(x.produces(xy.concat(yz), z))]
79 fn produces_trans(x: Self, xy: Seq<Self::Item>, y: Self, yz: Seq<Self::Item>, z: Self) {
80 let _ = chain_produces_inner_trans::<A, B>;
81 }
82}
83
84extern_spec! {
85 impl<A: Iterator, B: Iterator<Item = A::Item>> Chain<A, B> {
86 #[ensures(exists<sa, sb>
87 match self.iter_a() {
88 Some(a) => A::size_hint.postcondition((&a,), sa),
89 None => sa == (0usize, Some(0usize)),
90 } &&
91 match self.iter_b() {
92 Some(b) => B::size_hint.postcondition((&b,), sb),
93 None => sb == (0usize, Some(0usize)),
94 } &&
95 result.0 == if sa.0@ + sb.0@ > usize::MAX@ { usize::MAX } else { sa.0 + sb.0 } &&
96 result.1 == match (sa.1, sb.1) {
97 (Some(x), Some(y)) => if x@ + y@ > usize::MAX@ { None } else { Some(x + y) },
98 _ => None,
99 }
100 )]
101 fn size_hint(&self) -> (usize, Option<usize>);
102 }
103}
104
105impl<A: DoubleEndedIteratorSpec, B: DoubleEndedIteratorSpec<Item = A::Item>> DoubleEndedIteratorSpec
106 for Chain<A, B>
107{
108 #[logic(open, prophetic)]
109 fn completed_back(&mut self) -> bool {
110 pearlite! {
111 (match self.iter_b() {
112 None => true,
113 Some(sb) => exists<b: &mut B> sb == *b && b.completed_back() && resolve(^b)
114 }) &&
115 (^self).iter_b() == None &&
116 (match self.iter_a() {
117 None => true,
118 Some(sa) => exists<a: &mut A> sa == *a && a.completed_back() && (^self).iter_a() == Some(^a)
119 })
120 }
121 }
122
123 #[logic(open, prophetic, inline)]
124 fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
125 pearlite! {
126 exists<visited_a: Seq<A::Item>, visited_b: Seq<B::Item>>
127 visited == visited_b.concat(visited_a) &&
128 chain_produces_inner_back(self, visited_a, visited_b, o)
129 }
130 }
131
132 #[logic(law)]
133 #[ensures(self.produces_back(Seq::empty(), self))]
134 fn produces_back_refl(self) {}
135
136 #[logic(law, prophetic)]
137 #[requires(x.produces_back(xy, y))]
138 #[requires(y.produces_back(yz, z))]
139 #[ensures(x.produces_back(xy.concat(yz), z))]
140 fn produces_back_trans(x: Self, xy: Seq<Self::Item>, y: Self, yz: Seq<Self::Item>, z: Self) {
141 let _ = chain_produces_inner_back_trans::<A, B>;
142 }
143
144 #[logic(law)]
145 #[requires(Self::size_hint.postcondition((self,), r))]
146 #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
147 self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
148 #[ensures(match r.1 {
149 Some(r) => {
150 forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
151 }
152 None => true
153 })]
154 fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
155}
156
157#[logic(open, prophetic)]
158pub fn chain_produces_inner<A: IteratorSpec, B: IteratorSpec<Item = A::Item>>(
159 x: Chain<A, B>,
160 visited_a: Seq<A::Item>,
161 visited_b: Seq<B::Item>,
162 y: Chain<A, B>,
163) -> bool {
164 pearlite! {
165 (match x.iter_a() {
166 None => y.iter_a() == None && visited_a == Seq::empty(),
167 Some(xa) => match y.iter_a() {
168 None => exists<ya: &mut A> xa.produces(visited_a, *ya) && ya.completed() && resolve(^ya),
169 Some(ya) => xa.produces(visited_a, ya)
170 }
171 })
172 &&
173 (match y.iter_a() {
174 Some(_) => x.iter_b() == y.iter_b() && visited_b == Seq::empty(),
175 None => match (x.iter_b(), y.iter_b()) {
176 (None, _) => y.iter_b() == None && visited_b == Seq::empty(),
177 (Some(sb), Some(yb)) => sb.produces(visited_b, yb),
178 (Some(_), None) => false
179 }
180 })
181 }
182}
183
184#[logic]
185#[requires(chain_produces_inner(x, visited_a_xy, visited_b_xy, y))]
186#[requires(chain_produces_inner(y, visited_a_yz, visited_b_yz, z))]
187#[ensures(#[trigger(chain_produces_inner(x, visited_a_xy, visited_b_xy, y), chain_produces_inner(y, visited_a_yz, visited_b_yz, z))]
188 chain_produces_inner(x, visited_a_xy.concat(visited_a_yz), visited_b_xy.concat(visited_b_yz), z))]
189fn chain_produces_inner_trans<A: IteratorSpec, B: IteratorSpec<Item = A::Item>>(
190 x: Chain<A, B>,
191 visited_a_xy: Seq<A::Item>,
192 visited_b_xy: Seq<B::Item>,
193 y: Chain<A, B>,
194 visited_a_yz: Seq<A::Item>,
195 visited_b_yz: Seq<B::Item>,
196 z: Chain<A, B>,
197) {
198 proof_assert!(
199 Seq::<A::Item>::empty().concat(Seq::<A::Item>::empty()) == Seq::<A::Item>::empty()
200 );
201}
202
203#[logic(open, prophetic)]
204pub fn chain_produces_inner_back<
205 A: DoubleEndedIteratorSpec,
206 B: DoubleEndedIteratorSpec<Item = A::Item>,
207>(
208 x: Chain<A, B>,
209 visited_a: Seq<A::Item>,
210 visited_b: Seq<B::Item>,
211 y: Chain<A, B>,
212) -> bool {
213 pearlite! {
214 (match x.iter_b() {
215 None => y.iter_b() == None && visited_b == Seq::empty(),
216 Some(xb) => match y.iter_b() {
217 None => exists<yb: &mut B> xb.produces_back(visited_b, *yb) && yb.completed_back() && resolve(^yb),
218 Some(yb) => xb.produces_back(visited_b, yb)
219 }
220 })
221 &&
222 (match y.iter_b() {
223 Some(_) => x.iter_a() == y.iter_a() && visited_a == Seq::empty(),
224 None => match (x.iter_a(), y.iter_a()) {
225 (None, _) => y.iter_a() == None && visited_a == Seq::empty(),
226 (Some(xa), Some(ya)) => xa.produces_back(visited_a, ya),
227 (Some(_), None) => false
228 }
229 })
230 }
231}
232
233#[logic]
234#[requires(chain_produces_inner_back(x, visited_a_xy, visited_b_xy, y))]
235#[requires(chain_produces_inner_back(y, visited_a_yz, visited_b_yz, z))]
236#[ensures(#[trigger(chain_produces_inner_back(x, visited_a_xy, visited_b_xy, y), chain_produces_inner_back(y, visited_a_yz, visited_b_yz, z))]
237 chain_produces_inner_back(x, visited_a_xy.concat(visited_a_yz), visited_b_xy.concat(visited_b_yz), z))]
238fn chain_produces_inner_back_trans<
239 A: DoubleEndedIteratorSpec,
240 B: DoubleEndedIteratorSpec<Item = A::Item>,
241>(
242 x: Chain<A, B>,
243 visited_a_xy: Seq<A::Item>,
244 visited_b_xy: Seq<B::Item>,
245 y: Chain<A, B>,
246 visited_a_yz: Seq<A::Item>,
247 visited_b_yz: Seq<B::Item>,
248 z: Chain<A, B>,
249) {
250 proof_assert!(
251 Seq::<A::Item>::empty().concat(Seq::<A::Item>::empty()) == Seq::<A::Item>::empty()
252 );
253}