creusot_contracts/std/iter/
once.rs

1use crate::{prelude::*, std::iter::Once};
2
3impl<T> View for Once<T> {
4    type ViewTy = Option<T>;
5
6    #[logic(opaque)]
7    fn view(self) -> Option<T> {
8        dead
9    }
10}
11
12impl<T> IteratorSpec for Once<T> {
13    #[logic(open, prophetic)]
14    fn completed(&mut self) -> bool {
15        pearlite! { (*self)@ == None && resolve(self) }
16    }
17
18    #[logic(open, prophetic)]
19    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
20        pearlite! {
21            visited == Seq::empty() && self == o ||
22            exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
23        }
24    }
25
26    #[logic(law)]
27    #[ensures(self.produces(Seq::empty(), self))]
28    fn produces_refl(self) {}
29
30    #[logic(law)]
31    #[requires(a.produces(ab, b))]
32    #[requires(b.produces(bc, c))]
33    #[ensures(a.produces(ab.concat(bc), c))]
34    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
35}
36
37extern_spec! {
38    mod std {
39        mod iter {
40            impl<T> Iterator for Once<T> {
41                #[check(ghost)]
42                #[ensures(match result {
43                    None => self.completed(),
44                    Some(v) => (*self).produces(Seq::singleton(v), ^self)
45                })]
46                fn next(&mut self) -> Option<T>;
47            }
48        }
49    }
50}
creusot_contracts/std/iter/once.rs

creusot_contracts/std/iter/
once.rs
