creusot_contracts/std/iter/
rev.rs

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

creusot_contracts/std/iter/
rev.rs
