creusot_contracts/std/iter/
map.rs

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

creusot_contracts/std/iter/
map.rs
