creusot_contracts/std/iter/
zip.rs

1use crate::{invariant::*, prelude::*};
2use std::iter::Zip;
3
4pub trait ZipExt<A: Iterator, B: Iterator> {
5    #[logic]
6    fn itera(self) -> A;
7
8    #[logic]
9    fn iterb(self) -> B;
10}
11
12impl<A: Iterator, B: Iterator> ZipExt<A, B> for Zip<A, B> {
13    #[logic(opaque)]
14    fn itera(self) -> A {
15        dead
16    }
17
18    #[logic(opaque)]
19    fn iterb(self) -> B {
20        dead
21    }
22}
23
24impl<A: Iterator, B: Iterator> Invariant for Zip<A, B> {
25    #[logic(prophetic, open, inline)]
26    fn invariant(self) -> bool {
27        inv(self.itera()) && inv(self.iterb())
28    }
29}
30
31impl<A: IteratorSpec, B: IteratorSpec> IteratorSpec for Zip<A, B> {
32    #[logic(open, prophetic)]
33    fn completed(&mut self) -> bool {
34        pearlite! {
35            exists<a: &mut A, b: &mut B>
36                   *a == (*self).itera() && *b == (*self).iterb()
37                && ^a == (^self).itera() && ^b == (^self).iterb()
38                && (a.completed() && resolve(b)
39                    || exists<x: A::Item> inv(x) && (*a).produces(Seq::singleton(x), ^a) &&
40                                          resolve(x) && (*b).completed())
41        }
42    }
43
44    #[logic(open, prophetic)]
45    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
46        pearlite! {
47            // Using an `unzip` definition doesn't work well because of issues related to datatypes and `match`
48            exists<p1: Seq<_>, p2: Seq<_>>
49                   p1.len() == p2.len() && p2.len() == visited.len()
50                && (forall<i> 0 <= i && i < visited.len() ==> visited[i] == (p1[i], p2[i]))
51                && self.itera().produces(p1, o.itera()) && self.iterb().produces(p2, o.iterb())
52        }
53    }
54
55    #[logic(law)]
56    #[ensures(self.produces(Seq::empty(), self))]
57    fn produces_refl(self) {}
58
59    #[logic(law)]
60    #[requires(a.produces(ab, b))]
61    #[requires(b.produces(bc, c))]
62    #[ensures(a.produces(ab.concat(bc), c))]
63    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
64}
creusot_contracts/std/iter/zip.rs

creusot_contracts/std/iter/
zip.rs
