creusot_std/std/iter/
skip.rs

1#[cfg(creusot)]
2use crate::{logic::such_that, resolve::structural_resolve};
3use crate::{prelude::*, std::iter::ExactSizeIteratorSpec};
4use core::iter::Skip;
5
6pub trait SkipExt<I> {
7    #[logic]
8    fn iter(self) -> I;
9
10    #[logic]
11    fn n(self) -> usize;
12}
13
14impl<I> SkipExt<I> for Skip<I> {
15    #[logic(opaque)]
16    fn iter(self) -> I {
17        dead
18    }
19
20    #[logic(opaque)]
21    fn n(self) -> usize {
22        dead
23    }
24}
25
26impl<I> Resolve for Skip<I> {
27    #[logic(open, prophetic, inline)]
28    fn resolve(self) -> bool {
29        resolve(self.iter())
30    }
31
32    #[trusted]
33    #[logic(prophetic)]
34    #[requires(structural_resolve(self))]
35    #[ensures(self.resolve())]
36    fn resolve_coherence(self) {}
37}
38
39impl<I: Iterator> Invariant for Skip<I> {
40    #[logic(prophetic, open, inline)]
41    fn invariant(self) -> bool {
42        inv(self.iter())
43    }
44}
45
46impl<I: IteratorSpec> IteratorSpec for Skip<I> {
47    #[logic(open, prophetic)]
48    fn completed(&mut self) -> bool {
49        pearlite! {
50            (^self).n()@ == 0 &&
51            exists<s: Seq<Self::Item>, i: &mut I>
52                   s.len() <= (*self).n()@
53                && self.iter().produces(s, *i)
54                && (forall<i> 0 <= i && i < s.len() ==> resolve(s[i]))
55                && i.completed()
56                && ^i == (^self).iter()
57        }
58    }
59
60    #[logic(open, prophetic)]
61    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
62        pearlite! {
63            visited == Seq::empty() && self == o ||
64            o.n()@ == 0 && visited.len() > 0 &&
65            exists<s: Seq<Self::Item>>
66                   s.len() == self.n()@
67                && self.iter().produces(s.concat(visited), o.iter())
68                && forall<i> 0 <= i && i < s.len() ==> resolve(s[i])
69        }
70    }
71
72    #[logic(law)]
73    #[ensures(self.produces(Seq::empty(), self))]
74    fn produces_refl(self) {}
75
76    #[logic(law)]
77    #[requires(a.produces(ab, b))]
78    #[requires(b.produces(bc, c))]
79    #[ensures(a.produces(ab.concat(bc), c))]
80    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
81        // associativity of concat
82        proof_assert!(forall<s1: Seq<Self::Item>, s2: Seq<Self::Item>, s3: Seq<Self::Item>> s1.concat(s2.concat(s3)) == s1.concat(s2).concat(s3));
83        // empty is neutral for concat
84        proof_assert!(forall<s: Seq<Self::Item>> Seq::empty().concat(s) == s);
85        if ab != Seq::empty() {
86            proof_assert!(
87                // instantiate the existential in `b.produces(bc, c)`
88                let s = such_that(|s: Seq<Self::Item>| {
89                    s.len() == 0 && b.iter().produces(s.concat(bc), c.iter())
90                });
91                s.concat(bc) == bc
92            );
93        }
94    }
95}
96
97extern_spec! {
98    impl<I: Iterator> Iterator for Skip<I> {
99        #[ensures(exists<r>
100            I::size_hint.postcondition((&self.iter(),), r) &&
101            (r.0@ <= self.n()@ ==> result.0 == 0usize) &&
102            (r.0@ >= self.n()@ ==> result.0 == r.0 - self.n()) &&
103            match r.1 {
104                Some(ub) =>
105                    (ub@ <= self.n()@ ==> result.1 == Some(0usize)) &&
106                    (ub@ >= self.n()@ ==> result.1 == Some(ub - self.n())),
107                None => result.1 == None
108            }
109        )]
110        fn size_hint(&self) -> (usize, Option<usize>);
111    }
112}
113
114impl<I: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Skip<I> {
115    #[logic(law)]
116    #[requires(Self::size_hint.postcondition((self,), r))]
117    #[ensures(r.1 == Some(r.0))]
118    #[allow(unused_variables)]
119    fn size_hint_exact(&self, r: (usize, Option<usize>)) {
120        let _ = I::size_hint_exact;
121    }
122}
creusot_std/std/iter/skip.rs

creusot_std/std/iter/
skip.rs
