creusot_contracts/std/iter/
map.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::resolve::structural_resolve;
4use std::iter::Map;
5
6pub trait MapExt<I, F> {
7    #[logic]
8    fn iter(self) -> I;
9
10    #[logic]
11    fn func(self) -> F;
12}
13
14impl<I, F> MapExt<I, F> for Map<I, F> {
15    #[logic(opaque)]
16    fn iter(self) -> I {
17        dead
18    }
19
20    #[logic(opaque)]
21    fn func(self) -> F {
22        dead
23    }
24}
25
26impl<I, F> Resolve for Map<I, F> {
27    #[logic(open, prophetic, inline)]
28    fn resolve(self) -> bool {
29        resolve(self.iter()) && resolve(self.func())
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: IteratorSpec, B, F: FnMut(I::Item) -> B> Invariant for Map<I, F> {
40    #[logic(prophetic)]
41    #[ensures(result ==> inv(self.iter()) && inv(self.func()))]
42    fn invariant(self) -> bool {
43        pearlite! {
44            inv(self.iter()) && inv(self.func()) &&
45            reinitialize::<I, B, F>() &&
46            preservation(self.iter(), self.func()) &&
47            next_precondition(self.iter(), self.func())
48        }
49    }
50}
51
52impl<I: IteratorSpec, B, F: FnMut(I::Item) -> B> IteratorSpec for Map<I, F> {
53    #[logic(open, prophetic)]
54    fn completed(&mut self) -> bool {
55        pearlite! {
56            (exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed())
57            && (*self).func() == (^self).func()
58        }
59    }
60
61    #[logic(open, prophetic, inline)]
62    fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool {
63        pearlite! {
64            self.func().hist_inv(succ.func())
65            && exists<fs: Seq<&mut F>> fs.len() == visited.len()
66            && exists<s: Seq<I::Item>>
67                #[trigger(self.iter().produces(s, succ.iter()))]
68                s.len() == visited.len() && self.iter().produces(s, succ.iter())
69            && (forall<i> 1 <= i && i < fs.len() ==>  ^fs[i - 1] == *fs[i])
70            && if visited.len() == 0 { self.func() == succ.func() }
71               else { *fs[0] == self.func() &&  ^fs[visited.len() - 1] == succ.func() }
72            && forall<i> 0 <= i && i < visited.len() ==>
73                 self.func().hist_inv(*fs[i])
74                 && (*fs[i]).precondition((s[i],))
75                 && (*fs[i]).postcondition_mut((s[i],), ^fs[i], visited[i])
76        }
77    }
78
79    #[logic(law)]
80    #[ensures(self.produces(Seq::empty(), self))]
81    fn produces_refl(self) {}
82
83    #[logic(law)]
84    #[requires(a.produces(ab, b))]
85    #[requires(b.produces(bc, c))]
86    #[ensures(a.produces(ab.concat(bc), c))]
87    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
88}
89
90#[logic(open, prophetic)]
91pub fn next_precondition<I: IteratorSpec, B, F: FnMut(I::Item) -> B>(iter: I, func: F) -> bool {
92    pearlite! {
93        forall<e: I::Item, i: I>
94            #[trigger(iter.produces(Seq::singleton(e), i))]
95            iter.produces(Seq::singleton(e), i) ==>
96            func.precondition((e,))
97    }
98}
99
100#[logic(open, prophetic)]
101pub fn preservation<I: IteratorSpec, B, F: FnMut(I::Item) -> B>(iter: I, func: F) -> bool {
102    pearlite! {
103        forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
104            #[trigger(iter.produces(s.push_back(e1).push_back(e2), i), (*f).postcondition_mut((e1,), ^f, b))]
105            func.hist_inv(*f) ==>
106            iter.produces(s.push_back(e1).push_back(e2), i) ==>
107            (*f).precondition((e1,)) ==>
108            (*f).postcondition_mut((e1,), ^f, b) ==>
109            (^f).precondition((e2, ))
110    }
111}
112
113#[logic(open, prophetic)]
114pub fn reinitialize<I: IteratorSpec, B, F: FnMut(I::Item) -> B>() -> bool {
115    pearlite! {
116        forall<iter: &mut I, func: F>
117            iter.completed() ==> next_precondition(^iter, func) && preservation(^iter, func)
118    }
119}
creusot_contracts/std/iter/map.rs

creusot_contracts/std/iter/
map.rs
