creusot_contracts/std/iter/
skip.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::resolve::structural_resolve;
4use std::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}
creusot_contracts/std/iter/skip.rs

creusot_contracts/std/iter/
skip.rs
