creusot_std/std/iter/
fuse.rs

1use crate::{
2    prelude::*,
3    std::iter::{ExactSizeIteratorSpec, Fuse},
4};
5use core::iter::FusedIterator;
6
7impl<I: Iterator> View for Fuse<I> {
8    type ViewTy = Option<I>;
9
10    #[logic(opaque)]
11    fn view(self) -> Option<I> {
12        dead
13    }
14}
15
16impl<I: Iterator> Invariant for Fuse<I> {
17    #[logic(prophetic, open, inline)]
18    fn invariant(self) -> bool {
19        inv(self.view())
20    }
21}
22
23impl<I: IteratorSpec> IteratorSpec for Fuse<I> {
24    #[logic(open, prophetic)]
25    fn completed(&mut self) -> bool {
26        pearlite! {
27            (self@ == None || exists<it:&mut I> it.completed() && self@ == Some(*it)) &&
28            (^self)@ == None
29        }
30    }
31
32    #[logic(open, prophetic)]
33    fn produces(self, prod: Seq<Self::Item>, other: Self) -> bool {
34        pearlite! {
35            match self@ {
36                None => prod == Seq::empty() && other@ == self@,
37                Some(i) => match other@ {
38                    Some(i2) => i.produces(prod, i2),
39                    None => false,
40                },
41            }
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}
55
56pub trait FusedIteratorSpec: FusedIterator + IteratorSpec {
57    #[logic(law)]
58    #[requires(self.completed())]
59    #[requires((^self).produces(steps, next))]
60    #[ensures(steps == Seq::empty())]
61    fn is_fused(&mut self, steps: Seq<Self::Item>, next: Self);
62}
63
64impl<I: IteratorSpec> FusedIteratorSpec for Fuse<I> {
65    #[logic(law)]
66    #[requires(self.completed())]
67    #[requires((^self).produces(steps, next))]
68    #[ensures(steps == Seq::empty())]
69    fn is_fused(&mut self, steps: Seq<Self::Item>, next: Self) {}
70}
71
72extern_spec! {
73    impl<I: Iterator> Iterator for Fuse<I> {
74        #[ensures(match self@ {
75            Some(s) => I::size_hint.postcondition((&s,), result),
76            None => result == (0usize, Some(0usize))
77        })]
78        fn size_hint(&self) -> (usize, Option<usize>);
79    }
80}
81
82impl<I: ExactSizeIteratorSpec> ExactSizeIteratorSpec for Fuse<I> {
83    #[logic(law)]
84    #[requires(Self::size_hint.postcondition((self,), r))]
85    #[ensures(r.1 == Some(r.0))]
86    #[allow(unused_variables)]
87    fn size_hint_exact(&self, r: (usize, Option<usize>)) {
88        let _ = I::size_hint_exact;
89    }
90}
creusot_std/std/iter/fuse.rs

creusot_std/std/iter/
fuse.rs
