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        proof_assert! {
87            let ac = ab.concat(bc);
88            let (fsab, sab) = produces_instantiate_existential(a, ab, b);
89            let (fsbc, sbc) = produces_instantiate_existential(b, bc, c);
90            let fs = fsab.concat(fsbc);
91            let s = sab.concat(sbc);
92
93            (forall<i> 1 <= i && i < fs.len() ==>  ^fs[i - 1] == *fs[i])
94            && if ac.len() == 0 { a.func() == c.func() }
95               else { *fs[0] == a.func() &&  ^fs[ac.len() - 1] == c.func() }
96            && forall<i> 0 <= i && i < ac.len() ==>
97                 a.func().hist_inv(*fs[i])
98                 && (*fs[i]).postcondition_mut((s[i],), ^fs[i], ac[i])
99        }
100    }
101}
102
103/// Get the witnesses for the existentials in `produces`
104#[logic(prophetic)]
105#[requires(this.produces(visited, succ))]
106#[ensures(result.0.len() == visited.len() && result.1.len() == visited.len()
107    && this.iter().produces(result.1, succ.iter())
108    && (forall<i> 1 <= i && i < result.0.len() ==>  ^result.0[i - 1] == *result.0[i])
109    && if visited.len() == 0 { this.func() == succ.func() }
110       else { *result.0[0] == this.func() &&  ^result.0[visited.len() - 1] == succ.func() }
111    && forall<i> 0 <= i && i < visited.len() ==>
112         this.func().hist_inv(*result.0[i])
113         && (*result.0[i]).postcondition_mut((result.1[i],), ^result.0[i], visited[i])
114)]
115fn produces_instantiate_existential<'a, I, B, F>(
116    this: Map<I, F>,
117    visited: Seq<B>,
118    succ: Map<I, F>,
119) -> (Seq<&'a mut F>, Seq<I::Item>)
120where
121    I: IteratorSpec,
122    F: FnMut(I::Item) -> B,
123{
124    creusot_std::logic::such_that(|(fs, s): (Seq<&mut F>, Seq<I::Item>)| {
125        pearlite! {
126            fs.len() == visited.len() && s.len() == visited.len()
127            && this.iter().produces(s, succ.iter())
128            && (forall<i> 1 <= i && i < fs.len() ==>  ^fs[i - 1] == *fs[i])
129            && if visited.len() == 0 { this.func() == succ.func() }
130               else { *fs[0] == this.func() &&  ^fs[visited.len() - 1] == succ.func() }
131            && forall<i> 0 <= i && i < visited.len() ==>
132                 this.func().hist_inv(*fs[i])
133                 && (*fs[i]).postcondition_mut((s[i],), ^fs[i], visited[i])
134
135        }
136    })
137}
138
139#[logic(open, prophetic, inline)]
140pub fn next_precondition<I: IteratorSpec, B, F: FnMut(I::Item) -> B>(iter: I, func: F) -> bool {
141    pearlite! {
142        forall<e: I::Item, i: I>
143            #[trigger(iter.produces(Seq::singleton(e), i))]
144            inv(e) && iter.produces(Seq::singleton(e), i) ==>
145            func.precondition((e,))
146    }
147}
148
149#[logic(open, prophetic, inline)]
150pub fn preservation<I: IteratorSpec, B, F: FnMut(I::Item) -> B>(iter: I, func: F) -> bool {
151    pearlite! {
152        forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
153            #[trigger(iter.produces(s.push_back(e1).push_back(e2), i), (*f).postcondition_mut((e1,), ^f, b))]
154            func.hist_inv(*f) ==>
155            inv(s) && inv(e1) && inv(e2) && inv(f) ==>
156            iter.produces(s.push_back(e1).push_back(e2), i) ==>
157            (*f).postcondition_mut((e1,), ^f, b) ==>
158            (^f).precondition((e2, ))
159    }
160}
161
162#[logic(open, prophetic, inline)]
163pub fn reinitialize<I: IteratorSpec, B, F: FnMut(I::Item) -> B>() -> bool {
164    pearlite! {
165        forall<iter: &mut I, func: F>
166            iter.completed() ==> next_precondition(^iter, func) && preservation(^iter, func)
167    }
168}
creusot_std/std/iter/map.rs

creusot_std/std/iter/
map.rs
