creusot_std/std/iter/
filter_map.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use crate::{logic::Mapping, std::ops::*};
4use core::iter::FilterMap;
5
6pub trait FilterMapExt<I, F> {
7    #[logic]
8    fn iter(self) -> I;
9
10    #[logic]
11    fn func(self) -> F;
12}
13
14impl<I, F> FilterMapExt<I, F> for FilterMap<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<B, I: Iterator, F: FnMut(I::Item) -> Option<B>> Invariant for FilterMap<I, F> {
27    #[logic(prophetic, open, inline)]
28    fn invariant(self) -> bool {
29        inv(self.iter()) && inv(self.func()) && private_invariant(self)
30    }
31}
32
33#[logic(prophetic)]
34pub fn private_invariant<B, I: Iterator, F: FnMut(I::Item) -> Option<B>>(
35    f: FilterMap<I, F>,
36) -> bool {
37    // trivial precondition: simplification for sake of proof complexity
38    no_precondition(f.func()) &&
39    // immutable state: simplification for sake of proof complexity
40    immutable(f.func()) &&
41    // precision of postcondition
42    precise(f.func())
43}
44
45/// Asserts that `f` has no precondition: any closure state can be called with any input value
46/// In a future release this restriction may be lifted or weakened
47#[logic(open, prophetic)]
48pub fn no_precondition<A, B, F: FnMut(A) -> Option<B>>(f: F) -> bool {
49    pearlite! { forall<i: A> inv(i) ==> f.precondition((i,)) }
50}
51
52/// Asserts that the captures of `f` are used immutably
53/// In a future release this restriction may be lifted or weakened
54#[logic(open, prophetic)]
55pub fn immutable<A, B, F: FnMut(A) -> Option<B>>(f: F) -> bool {
56    pearlite! { forall<g: F> f.hist_inv(g) ==> f == g }
57}
58
59/// Asserts that the postcondition of `f` is *precise*: that there are never two possible values matching the postcondition
60#[logic(open, prophetic)]
61pub fn precise<A, B, F: FnMut(A) -> Option<B>>(f1: F) -> bool {
62    pearlite! { forall<f2: F, i> !((exists<b: B> f1.postcondition_mut((i,), f2, Some(b))) && f1.postcondition_mut((i,), f2, None)) }
63}
64
65impl<I: IteratorSpec, B, F: FnMut(I::Item) -> Option<B>> IteratorSpec for FilterMap<I, F> {
66    #[logic(open, prophetic)]
67    fn completed(&mut self) -> bool {
68        pearlite! {
69            (exists<s: Seq<_>, e: &mut I > self.iter().produces(s, *e) && e.completed() &&
70                forall<i> 0 <= i && i < s.len() ==> (*self).func().postcondition_mut((s[i],), (^self).func(), None))
71            && (*self).func() == (^self).func()
72        }
73    }
74
75    #[logic(open, prophetic)]
76    fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool {
77        pearlite! {
78            private_invariant(self) ==>
79            self.func().hist_inv(succ.func()) &&
80            // f here is a mapping from indices of `visited` to those of `s`, where `s` is the whole sequence produced by the underlying iterator
81            // Interestingly, Z3 guesses `f` quite readily but gives up *totally* on `s`. However, the addition of the final assertions on the correctness of the values
82            // blocks z3's guess for `f`.
83            exists<s: Seq<I::Item>, f: Mapping<Int, Int>> self.iter().produces(s, succ.iter()) &&
84                (forall<i> 0 <= i && i < visited.len() ==> 0 <= f.get(i) && f.get(i) < s.len()) &&
85                // `f` is a monotone mapping
86                (forall<i, j> 0 <= i && i < j && j < visited.len() ==> f.get(i) < f.get(j)) &&
87                // `f` points to elements produced in `s` (by the underlying `iter`) for which the predicate `self.func()` returned `Some`.
88                (forall<i> 0 <= i && i < visited.len() ==> self.func().postcondition_mut((s[f.get(i)],), self.func(), Some(visited[i]))) &&
89                // For other elements not in the image of `f`, the predicate `self.func()` returned `None`.
90                (forall<j> 0 <= j && j < s.len()
91                    ==> (!exists<i> 0 <= i && i < visited.len() && f.get(i) == j) == self.func().postcondition_mut((s[j],), self.func(), None))
92        }
93    }
94
95    #[logic(law)]
96    #[ensures(self.produces(Seq::empty(), self))]
97    fn produces_refl(self) {}
98
99    #[logic(law)]
100    #[requires(a.produces(ab, b))]
101    #[requires(b.produces(bc, c))]
102    #[ensures(a.produces(ab.concat(bc), c))]
103    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
104}
creusot_std/std/iter/filter_map.rs

creusot_std/std/iter/
filter_map.rs
