creusot_std/std/iter/
once.rs

1use crate::{
2    prelude::*,
3    std::iter::{ExactSizeIteratorSpec, Once},
4};
5
6impl<T> View for Once<T> {
7    type ViewTy = Option<T>;
8
9    #[logic(opaque)]
10    fn view(self) -> Option<T> {
11        dead
12    }
13}
14
15impl<T> IteratorSpec for Once<T> {
16    #[logic(open, prophetic)]
17    fn completed(&mut self) -> bool {
18        pearlite! { (*self)@ == None && resolve(self) }
19    }
20
21    #[logic(open, prophetic)]
22    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
23        pearlite! {
24            visited == Seq::empty() && self == o ||
25            exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None
26        }
27    }
28
29    #[logic(law)]
30    #[ensures(self.produces(Seq::empty(), self))]
31    fn produces_refl(self) {}
32
33    #[logic(law)]
34    #[requires(a.produces(ab, b))]
35    #[requires(b.produces(bc, c))]
36    #[ensures(a.produces(ab.concat(bc), c))]
37    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
38}
39
40extern_spec! {
41    impl<T> Iterator for Once<T> {
42        #[check(ghost)]
43        #[ensures(match result {
44            None => self.completed(),
45            Some(v) => (*self).produces(Seq::singleton(v), ^self)
46        })]
47        fn next(&mut self) -> Option<T>;
48
49        #[check(ghost)]
50        #[ensures(result.0 == match self@ { Some(_) => 1usize, None => 0usize })]
51        #[ensures(result.1 == Some(result.0))]
52        fn size_hint(&self) -> (usize, Option<usize>);
53    }
54}
55
56impl<T> ExactSizeIteratorSpec for Once<T> {
57    #[logic(law)]
58    #[requires(Self::size_hint.postcondition((self,), r))]
59    #[ensures(r.1 == Some(r.0))]
60    #[allow(unused_variables)]
61    fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
62}
creusot_std/std/iter/once.rs

creusot_std/std/iter/
once.rs
