creusot_contracts/std/iter/
filter.rs

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

creusot_contracts/std/iter/
filter.rs
