creusot_contracts/std/iter/
filter.rs

1use crate::{logic::Mapping, prelude::*};
2use std::iter::Filter;
3
4pub trait FilterExt<I, F> {
5    #[logic]
6    fn iter(self) -> I;
7
8    #[logic]
9    fn func(self) -> F;
10}
11
12impl<I, F> FilterExt<I, F> for Filter<I, F> {
13    #[logic(opaque)]
14    fn iter(self) -> I {
15        dead
16    }
17
18    #[logic(opaque)]
19    fn func(self) -> F {
20        dead
21    }
22}
23
24impl<I: Iterator, F: FnMut(&I::Item) -> bool> Invariant for Filter<I, F> {
25    #[logic(prophetic, open, inline)]
26    #[ensures(result ==> inv(self.iter()) && inv(self.func()))]
27    fn invariant(self) -> bool {
28        inv(self.iter()) && inv(self.func()) && private_invariant(self)
29    }
30}
31
32#[logic(prophetic)]
33pub fn private_invariant<I: Iterator, F: FnMut(&I::Item) -> bool>(f: Filter<I, F>) -> bool {
34    no_precondition(f.func()) && immutable(f.func()) && precise(f.func())
35}
36
37/// Asserts that `f` has no precondition: any closure state can be called with any input value
38/// In a future release this restriction may be lifted or weakened
39#[logic(open, prophetic)]
40pub fn no_precondition<A, F: FnMut(A) -> bool>(_: F) -> bool {
41    pearlite! { forall<f: F, i: A> f.precondition((i,)) }
42}
43
44/// Asserts that the captures of `f` are used immutably
45/// In a future release this restriction may be lifted or weakened
46#[logic(open, prophetic)]
47pub fn immutable<A, F: FnMut(A) -> bool>(_: F) -> bool {
48    pearlite! { forall<f: F, g: F> f.hist_inv(g) ==> f == g }
49}
50
51/// Asserts that the postcondition of `f` is *precise*: that there are never two possible values
52/// matching the postcondition
53// precision of postcondition. This is not *necessary*, but simplifies the proof that we have
54// returned *all* elements which evaluate to true. If we remove this we could prove an alternate
55// statement of produces that says we returned `true` for elements in `visited`, and `false` for
56// ones which we didn't remove. *if* the postcondition happened to be precise, these two statements
57// would be equivalent .
58#[logic(open, prophetic)]
59pub fn precise<A, F: FnMut(A) -> bool>(_: F) -> bool {
60    pearlite! { forall<f1: F, f2: F, i> !(f1.postcondition_mut((i,), f2, true) && f1.postcondition_mut((i,), f2, false)) }
61}
62
63impl<I: IteratorSpec, F: FnMut(&I::Item) -> bool> IteratorSpec for Filter<I, F> {
64    #[logic(open, prophetic)]
65    fn completed(&mut self) -> bool {
66        pearlite! {
67            (exists<s: Seq<_>, e: &mut I > self.iter().produces(s, *e) && e.completed() &&
68                forall<i> 0 <= i && i < s.len() ==> (*self).func().postcondition_mut((&s[i],), (^self).func(), false))
69            && (*self).func() == (^self).func()
70        }
71    }
72
73    #[logic(open, prophetic)]
74    fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool {
75        pearlite! {
76            private_invariant(self) ==>
77            self.func().hist_inv(succ.func()) &&
78            // f here is a mapping from indices of `visited` to those of `s`, where `s` is the whole sequence produced by the underlying iterator
79            // 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
80            // blocks z3's guess for `f`.
81            exists<s: Seq<Self::Item>, f: Mapping<Int, Int>> self.iter().produces(s, succ.iter()) &&
82                (forall<i> 0 <= i && i < visited.len() ==> 0 <= f.get(i) && f.get(i) < s.len()) &&
83                // `f` is a monotone mapping
84                (forall<i, j> 0 <= i && i < j && j < visited.len() ==> f.get(i) < f.get(j)) &&
85                (forall<i> 0 <= i && i < visited.len() ==> visited[i] == s[f.get(i)]) &&
86                (forall<i> 0 <= i &&  i < s.len() ==>
87                    (exists<j> 0 <= j && j < visited.len() && f.get(j) == i) == self.func().postcondition_mut((&s[i],), self.func(), true))
88        }
89    }
90
91    #[logic(law)]
92    #[ensures(self.produces(Seq::empty(), self))]
93    fn produces_refl(self) {}
94
95    #[logic(law)]
96    #[requires(a.produces(ab, b))]
97    #[requires(b.produces(bc, c))]
98    #[ensures(a.produces(ab.concat(bc), c))]
99    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
100}
creusot_contracts/std/iter/filter.rs

creusot_contracts/std/iter/
filter.rs
