creusot_contracts/std/iter/
enumerate.rs

1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{invariant::*, prelude::*, std::iter::Enumerate};
4
5pub trait EnumerateExt<I> {
6    #[logic]
7    fn iter(self) -> I;
8
9    #[logic]
10    fn n(self) -> usize;
11}
12
13impl<I> EnumerateExt<I> for Enumerate<I> {
14    #[logic(opaque)]
15    fn iter(self) -> I {
16        dead
17    }
18
19    #[logic(opaque)]
20    fn n(self) -> usize {
21        dead
22    }
23}
24
25impl<I> Resolve for Enumerate<I> {
26    #[logic(open, prophetic, inline)]
27    fn resolve(self) -> bool {
28        resolve(self.iter())
29    }
30
31    #[trusted]
32    #[logic(prophetic)]
33    #[requires(structural_resolve(self))]
34    #[ensures(self.resolve())]
35    fn resolve_coherence(self) {}
36}
37
38impl<I: IteratorSpec> Invariant for Enumerate<I> {
39    #[logic(prophetic)]
40    #[ensures(result ==> inv(self.iter()))]
41    fn invariant(self) -> bool {
42        pearlite! {
43            inv(self.iter())
44            && (forall<s: Seq<I::Item>, i: I>
45                #[trigger(self.iter().produces(s, i))]
46                self.iter().produces(s, i) ==>
47                self.n()@ + s.len() < std::usize::MAX@)
48            && (forall<i: &mut I> i.completed() ==> (*i).produces(Seq::empty(), ^i))
49        }
50    }
51}
52
53impl<I: IteratorSpec> IteratorSpec for Enumerate<I> {
54    #[logic(open, prophetic)]
55    fn completed(&mut self) -> bool {
56        pearlite! {
57            exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter()
58                && inner.completed()
59                && self.n()@ == (^self).n()@
60        }
61    }
62
63    #[logic(open, prophetic)]
64    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
65        pearlite! {
66            visited.len() == o.n()@ - self.n()@
67            && exists<s: Seq<I::Item>>
68                   self.iter().produces(s, o.iter())
69                && visited.len() == s.len()
70                && forall<i> 0 <= i && i < s.len() ==> visited[i].0@ == self.n()@ + i && visited[i].1 == s[i]
71        }
72    }
73
74    #[logic(law)]
75    #[ensures(self.produces(Seq::empty(), self))]
76    fn produces_refl(self) {}
77
78    #[logic(law)]
79    #[requires(a.produces(ab, b))]
80    #[requires(b.produces(bc, c))]
81    #[ensures(a.produces(ab.concat(bc), c))]
82    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
83}
creusot_contracts/std/iter/enumerate.rs

creusot_contracts/std/iter/
enumerate.rs
