creusot_std/std/iter/
map.rs

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

creusot_std/std/iter/
map.rs
