creusot_contracts/std/iter/
fuse.rs

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

creusot_contracts/std/iter/
fuse.rs
