creusot_std/std/iter/
filter.rs

1#[cfg(creusot)]
2use crate::logic::Mapping;
3use crate::prelude::*;
4use core::iter::Filter;
5
6pub trait FilterExt<I, F> {
7    #[logic]
8    fn iter(self) -> I;
9
10    #[logic]
11    fn func(self) -> F;
12}
13
14impl<I, F> FilterExt<I, F> for Filter<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: Iterator, F: FnMut(&I::Item) -> bool> Invariant for Filter<I, F> {
27    #[logic(prophetic, open, inline)]
28    #[ensures(result ==> inv(self.iter()) && inv(self.func()))]
29    fn invariant(self) -> bool {
30        inv(self.iter()) && inv(self.func()) && private_invariant(self)
31    }
32}
33
34#[logic(prophetic)]
35pub fn private_invariant<I: Iterator, F: FnMut(&I::Item) -> bool>(f: Filter<I, F>) -> bool {
36    no_precondition(f.func()) && immutable(f.func()) && precise(f.func())
37}
38
39/// Asserts that `f` has no precondition: any closure state can be called with any input value
40/// In a future release this restriction may be lifted or weakened
41#[logic(open, prophetic)]
42pub fn no_precondition<A, F: FnMut(A) -> bool>(_: F) -> bool {
43    pearlite! { forall<f: F, i: A> inv(f) && inv(i) ==> f.precondition((i,)) }
44}
45
46/// Asserts that the captures of `f` are used immutably
47/// In a future release this restriction may be lifted or weakened
48#[logic(open, prophetic)]
49pub fn immutable<A, F: FnMut(A) -> bool>(_: F) -> bool {
50    pearlite! { forall<f: F, g: F> f.hist_inv(g) ==> f == g }
51}
52
53/// Asserts that the postcondition of `f` is *precise*: that there are never two possible values
54/// matching the postcondition
55// precision of postcondition. This is not *necessary*, but simplifies the proof that we have
56// returned *all* elements which evaluate to true. If we remove this we could prove an alternate
57// statement of produces that says we returned `true` for elements in `visited`, and `false` for
58// ones which we didn't remove. *if* the postcondition happened to be precise, these two statements
59// would be equivalent .
60#[logic(open, prophetic)]
61pub fn precise<A, F: FnMut(A) -> bool>(_: F) -> bool {
62    pearlite! { forall<f1: F, f2: F, i> !(f1.postcondition_mut((i,), f2, true) && f1.postcondition_mut((i,), f2, false)) }
63}
64
65impl<I: IteratorSpec, F: FnMut(&I::Item) -> bool> IteratorSpec for Filter<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(), false))
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<Self::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                (forall<i> 0 <= i && i < visited.len() ==> visited[i] == s[f.get(i)]) &&
88                (forall<i> 0 <= i &&  i < s.len() ==>
89                    (exists<j> 0 <= j && j < visited.len() && f.get(j) == i) == self.func().postcondition_mut((&s[i],), self.func(), true))
90        }
91    }
92
93    #[logic(law)]
94    #[ensures(self.produces(Seq::empty(), self))]
95    fn produces_refl(self) {}
96
97    #[logic(law)]
98    #[requires(a.produces(ab, b))]
99    #[requires(b.produces(bc, c))]
100    #[ensures(a.produces(ab.concat(bc), c))]
101    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
102}
creusot_std/std/iter/filter.rs

creusot_std/std/iter/
filter.rs
