1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135

use crate::{std::ops::*, structural_resolve, *};
use ::std::iter::Map;

pub trait MapExt<I, F> {
    #[logic]
    fn iter(self) -> I;

    #[logic]
    fn func(self) -> F;
}

impl<I, F> MapExt<I, F> for Map<I, F> {
    #[trusted]
    #[logic]
    #[ensures(inv(self) ==> inv(result))]
    fn iter(self) -> I {
        dead
    }

    #[trusted]
    #[logic]
    #[ensures(inv(self) ==> inv(result))]
    fn func(self) -> F {
        dead
    }
}

impl<I, F> Resolve for Map<I, F> {
    #[open]
    #[predicate(prophetic)]
    fn resolve(self) -> bool {
        resolve(&self.iter()) && resolve(&self.func())
    }

    #[trusted]
    #[logic(prophetic)]
    #[open(self)]
    #[requires(structural_resolve(self))]
    #[ensures((*self).resolve())]
    fn resolve_coherence(&self) {}
}

impl<B, I, F> Iterator for Map<I, F>
where
    I: Iterator,
    Self: ::std::iter::Iterator<Item = B>,
    F: FnMut(I::Item) -> B,
{
    #[open]
    #[predicate(prophetic)]
    fn completed(&mut self) -> bool {
        pearlite! {
            (exists<inner : &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed())
            && (*self).func() == (^self).func()
        }
    }

    #[open]
    #[predicate(prophetic)]
    #[why3::attr = "inline:trivial"]
    fn produces(self, visited: Seq<Self::Item>, succ: Self) -> bool {
        pearlite! {
            self.func().unnest(succ.func())
            && exists<fs: Seq<&mut F>> fs.len() == visited.len()
            && exists<s : Seq<I::Item>>
                #![trigger self.iter().produces(s, succ.iter())]
                s.len() == visited.len() && self.iter().produces(s, succ.iter())
            && (forall<i : Int> 1 <= i && i < fs.len() ==>  ^fs[i - 1] == *fs[i])
            && if visited.len() == 0 { self.func() == succ.func() }
               else { *fs[0] == self.func() &&  ^fs[visited.len() - 1] == succ.func() }
            && forall<i : Int> 0 <= i && i < visited.len() ==>
                 self.func().unnest(*fs[i])
                 && (*fs[i]).precondition((s[i],))
                 && (*fs[i]).postcondition_mut((s[i],), ^fs[i], visited[i])
        }
    }

    #[law]
    #[open(self)]
    #[ensures(self.produces(Seq::EMPTY, self))]
    fn produces_refl(self) {}

    #[law]
    #[open(self)]
    #[requires(a.produces(ab, b))]
    #[requires(b.produces(bc, c))]
    #[ensures(a.produces(ab.concat(bc), c))]
    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
}

#[open]
#[predicate(prophetic)]
pub fn next_precondition<I, B, F>(iter: I, func: F) -> bool
where
    I: Iterator,
    F: FnMut(I::Item) -> B,
{
    pearlite! {
        forall<e: I::Item, i: I>
            #![trigger iter.produces(Seq::singleton(e), i)]
            iter.produces(Seq::singleton(e), i) ==>
            func.precondition((e,))
    }
}

#[open]
#[predicate(prophetic)]
pub fn preservation<I, B, F>(iter: I, func: F) -> bool
where
    I: Iterator,
    F: FnMut(I::Item) -> B,
{
    pearlite! {
        forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
            #![trigger iter.produces(s.push_back(e1).push_back(e2), i), (*f).postcondition_mut((e1,), ^f, b)]
            func.unnest(*f) ==>
            iter.produces(s.push_back(e1).push_back(e2), i) ==>
            (*f).precondition((e1,)) ==>
            (*f).postcondition_mut((e1,), ^f, b) ==>
            (^f).precondition((e2, ))
    }
}

#[open]
#[predicate(prophetic)]
pub fn reinitialize<I, B, F>() -> bool
where
    I: Iterator,
    F: FnMut(I::Item) -> B,
{
    pearlite! {
        forall<iter: &mut I, func: F>
            iter.completed() ==> next_precondition(^iter, func) && preservation(^iter, func)
    }
}