creusot_std/std/iter/
zip.rs

1use crate::{invariant::*, prelude::*, std::iter::ExactSizeIteratorSpec};
2use core::iter::Zip;
3
4pub trait ZipExt<A: Iterator, B: Iterator> {
5    #[logic]
6    fn iter_a(self) -> A;
7
8    #[logic]
9    fn iter_b(self) -> B;
10}
11
12impl<A: Iterator, B: Iterator> ZipExt<A, B> for Zip<A, B> {
13    #[logic(opaque)]
14    fn iter_a(self) -> A {
15        dead
16    }
17
18    #[logic(opaque)]
19    fn iter_b(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.iter_a()) && inv(self.iter_b())
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).iter_a() && *b == (*self).iter_b()
37                && ^a == (^self).iter_a() && ^b == (^self).iter_b()
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.iter_a().produces(p1, o.iter_a()) && self.iter_b().produces(p2, o.iter_b())
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}
65
66extern_spec! {
67    impl<A: Iterator, B: Iterator> Iterator for Zip<A, B> {
68        #[ensures(exists<ra, rb>
69            A::size_hint.postcondition((&self.iter_a(),), ra) &&
70            B::size_hint.postcondition((&self.iter_b(),), rb) &&
71            (ra.0@ <= rb.0@ ==> result.0 == ra.0) &&
72            (ra.0@ >= rb.0@ ==> result.0 == rb.0) &&
73            match (ra.1, rb.1) {
74                (Some(ua), Some(ub)) =>
75                    (ua@ <= ub@ ==> result.1 == Some(ua)) &&
76                    (ua@ >= ub@ ==> result.1 == Some(ub)),
77                (Some(ua), None) => result.1 == Some(ua),
78                (None, Some(ub)) => result.1 == Some(ub),
79                (None, None) => result.1 == None
80            }
81        )]
82        fn size_hint(&self) -> (usize, Option<usize>);
83    }
84}
85
86impl<A: ExactSizeIteratorSpec, B: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Zip<A, B> {
87    #[logic(law)]
88    #[requires(Self::size_hint.postcondition((self,), r))]
89    #[ensures(r.1 == Some(r.0))]
90    #[allow(unused_variables)]
91    fn size_hint_exact(&self, r: (usize, Option<usize>)) {
92        let _ = A::size_hint_exact;
93        let _ = B::size_hint_exact;
94    }
95}
creusot_std/std/iter/zip.rs

creusot_std/std/iter/
zip.rs
