creusot_std/std/iter/
map.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::resolve::structural_resolve;
4use core::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]) && (*fs[i]).postcondition_mut((s[i],), ^fs[i], visited[i])
74        }
75    }
76
77    #[logic(law)]
78    #[ensures(self.produces(Seq::empty(), self))]
79    fn produces_refl(self) {}
80
81    #[logic(law)]
82    #[requires(a.produces(ab, b))]
83    #[requires(b.produces(bc, c))]
84    #[ensures(a.produces(ab.concat(bc), c))]
85    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
86}
87
88#[logic(open, prophetic, inline)]
89pub fn next_precondition<I: IteratorSpec, B, F: FnMut(I::Item) -> B>(iter: I, func: F) -> bool {
90    pearlite! {
91        forall<e: I::Item, i: I>
92            #[trigger(iter.produces(Seq::singleton(e), i))]
93            inv(e) && iter.produces(Seq::singleton(e), i) ==>
94            func.precondition((e,))
95    }
96}
97
98#[logic(open, prophetic, inline)]
99pub fn preservation<I: IteratorSpec, B, F: FnMut(I::Item) -> B>(iter: I, func: F) -> bool {
100    pearlite! {
101        forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
102            #[trigger(iter.produces(s.push_back(e1).push_back(e2), i), (*f).postcondition_mut((e1,), ^f, b))]
103            func.hist_inv(*f) ==>
104            inv(s) && inv(e1) && inv(e2) && inv(f) ==>
105            iter.produces(s.push_back(e1).push_back(e2), i) ==>
106            (*f).postcondition_mut((e1,), ^f, b) ==>
107            (^f).precondition((e2, ))
108    }
109}
110
111#[logic(open, prophetic, inline)]
112pub fn reinitialize<I: IteratorSpec, B, F: FnMut(I::Item) -> B>() -> bool {
113    pearlite! {
114        forall<iter: &mut I, func: F>
115            iter.completed() ==> next_precondition(^iter, func) && preservation(^iter, func)
116    }
117}
creusot_std/std/iter/map.rs

creusot_std/std/iter/
map.rs
