creusot_std/std/iter/
rev.rs

1use crate::{
2    prelude::*,
3    std::iter::{ExactSizeIteratorSpec, Rev},
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    #[logic(opaque)]
16    fn iter(self) -> I {
17        dead
18    }
19
20    #[trusted]
21    #[logic(opaque)]
22    #[ensures((*self).iter() == *result && (^self).iter() == ^result)]
23    fn iter_mut(&mut self) -> &mut I {
24        dead
25    }
26}
27
28impl<I> Invariant for Rev<I> {
29    #[logic(prophetic, open, inline)]
30    fn invariant(self) -> bool {
31        inv(self.iter())
32    }
33}
34
35impl<I: DoubleEndedIteratorSpec> IteratorSpec for Rev<I> {
36    #[logic(open, prophetic)]
37    fn completed(&mut self) -> bool {
38        self.iter_mut().completed_back()
39    }
40
41    #[logic(open, prophetic)]
42    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
43        self.iter().produces_back(visited, o.iter())
44    }
45
46    #[logic(law)]
47    #[ensures(self.produces(Seq::empty(), self))]
48    fn produces_refl(self) {}
49
50    #[logic(law)]
51    #[requires(a.produces(ab, b))]
52    #[requires(b.produces(bc, c))]
53    #[ensures(a.produces(ab.concat(bc), c))]
54    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
55}
56
57impl<I: DoubleEndedIteratorSpec> DoubleEndedIteratorSpec for Rev<I> {
58    #[logic(open, prophetic)]
59    fn completed_back(&mut self) -> bool {
60        self.iter_mut().completed()
61    }
62
63    #[logic(open, prophetic)]
64    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
65        self.iter().produces(visited, o.iter())
66    }
67
68    #[logic(law)]
69    #[ensures(self.produces_back(Seq::empty(), self))]
70    fn produces_back_refl(self) {}
71
72    #[logic(law)]
73    #[requires(a.produces_back(ab, b))]
74    #[requires(b.produces_back(bc, c))]
75    #[ensures(a.produces_back(ab.concat(bc), c))]
76    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
77
78    #[logic(law)]
79    #[requires(Self::size_hint.postcondition((self,), r))]
80    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
81        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
82    #[ensures(match r.1 {
83        Some(r) => {
84            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
85        }
86        None => true
87    })]
88    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
89}
90
91extern_spec! {
92    impl<I: DoubleEndedIterator> Iterator for Rev<I> {
93        #[ensures(I::size_hint.postcondition((&self.iter(),), result))]
94        fn size_hint(&self) -> (usize, Option<usize>);
95    }
96}
97
98impl<I: ExactSizeIteratorSpec + DoubleEndedIteratorSpec> ExactSizeIteratorSpec for Rev<I> {
99    #[logic(law)]
100    #[requires(Self::size_hint.postcondition((self,), r))]
101    #[ensures(r.1 == Some(r.0))]
102    fn size_hint_exact(&self, r: (usize, Option<usize>)) {
103        self.iter().size_hint_exact(r)
104    }
105}
creusot_std/std/iter/rev.rs

creusot_std/std/iter/
rev.rs
