creusot_contracts/std/iter/
rev.rs

1use crate::{
2    std::iter::{DoubleEndedIterator, Iterator, Rev},
3    *,
4};
5
6pub trait RevExt<I> {
7    #[logic]
8    fn iter(self) -> I;
9
10    #[logic]
11    fn iter_mut(&mut self) -> &mut I;
12}
13
14impl<I> RevExt<I> for Rev<I> {
15    #[trusted]
16    #[logic(opaque)]
17    #[ensures(inv(self) ==> inv(result))]
18    fn iter(self) -> I {
19        dead
20    }
21
22    #[trusted]
23    #[logic(opaque)]
24    #[ensures((*self).iter() == *result && (^self).iter() == ^result)]
25    fn iter_mut(&mut self) -> &mut I {
26        dead
27    }
28}
29
30impl<I: DoubleEndedIterator> Iterator for Rev<I> {
31    #[logic(open, prophetic)]
32    fn completed(&mut self) -> bool {
33        pearlite! { self.iter_mut().completed() }
34    }
35
36    #[logic(open, prophetic)]
37    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
38        pearlite! {
39            self.iter().produces_back(visited, o.iter())
40        }
41    }
42
43    #[logic(law)]
44    #[ensures(self.produces(Seq::empty(), self))]
45    fn produces_refl(self) {}
46
47    #[logic(law)]
48    #[requires(a.produces(ab, b))]
49    #[requires(b.produces(bc, c))]
50    #[ensures(a.produces(ab.concat(bc), c))]
51    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
52}
creusot_contracts/std/iter/rev.rs

creusot_contracts/std/iter/
rev.rs
