creusot_contracts/std/iter/
fuse.rs

1use crate::{std::iter::Fuse, *};
2
3impl<I: Iterator> View for Fuse<I> {
4    type ViewTy = Option<I>;
5
6    #[trusted]
7    #[logic(opaque)]
8    #[ensures(inv(self) ==> inv(result))]
9    #[ensures(forall<other: Fuse<I>> result == other@ ==> self == other)]
10    fn view(self) -> Option<I> {
11        dead
12    }
13}
14
15impl<I: Iterator> Iterator for Fuse<I> {
16    #[logic(open, prophetic)]
17    fn completed(&mut self) -> bool {
18        pearlite! {
19            (self@ == None || exists<it:&mut I> it.completed() && self@ == Some(*it)) &&
20            (^self)@ == None
21        }
22    }
23
24    #[logic(open, prophetic)]
25    fn produces(self, prod: Seq<Self::Item>, other: Self) -> bool {
26        pearlite! {
27            match self@ {
28                None => prod == Seq::empty() && other@ == self@,
29                Some(i) => match other@ {
30                    Some(i2) => i.produces(prod, i2),
31                    None => false,
32                },
33            }
34        }
35    }
36
37    #[logic(open, law)]
38    #[ensures(self.produces(Seq::empty(), self))]
39    fn produces_refl(self) {}
40
41    #[logic(open, law)]
42    #[requires(a.produces(ab, b))]
43    #[requires(b.produces(bc, c))]
44    #[ensures(a.produces(ab.concat(bc), c))]
45    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
46}
47
48pub trait FusedIterator: ::std::iter::FusedIterator + Iterator {
49    #[logic(law)]
50    #[requires(self.completed())]
51    #[requires((^self).produces(steps, next))]
52    #[ensures(steps == Seq::empty() && ^self == next)]
53    fn is_fused(&mut self, steps: Seq<Self::Item>, next: Self);
54}
55
56impl<I: Iterator> FusedIterator for Fuse<I> {
57    #[logic(open, law)]
58    #[requires(self.completed())]
59    #[requires((^self).produces(steps, next))]
60    #[ensures(steps == Seq::empty() && ^self == next)]
61    fn is_fused(&mut self, steps: Seq<Self::Item>, next: Self) {}
62}
creusot_contracts/std/iter/fuse.rs

creusot_contracts/std/iter/
fuse.rs
