creusot_contracts/std/iter/
range.rs

1use crate::prelude::*;
2#[cfg(feature = "nightly")]
3use std::iter::Step;
4use std::ops::{Range, RangeInclusive};
5
6#[cfg(feature = "nightly")]
7impl<Idx: DeepModel<DeepModelTy = Int> + Step> IteratorSpec for Range<Idx> {
8    #[logic(open, prophetic)]
9    fn completed(&mut self) -> bool {
10        pearlite! {
11            resolve(self) && self.start.deep_model() >= self.end.deep_model()
12        }
13    }
14
15    #[logic(open)]
16    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
17        pearlite! {
18            self.end == o.end && self.start.deep_model() <= o.start.deep_model()
19            && (visited.len() > 0 ==> o.start.deep_model() <= o.end.deep_model())
20            && visited.len() == o.start.deep_model() - self.start.deep_model()
21            && forall<i> 0 <= i && i < visited.len() ==>
22                visited[i].deep_model() == self.start.deep_model() + i
23        }
24    }
25
26    #[logic(law)]
27    #[ensures(self.produces(Seq::empty(), self))]
28    fn produces_refl(self) {}
29
30    #[logic(law)]
31    #[requires(a.produces(ab, b))]
32    #[requires(b.produces(bc, c))]
33    #[ensures(a.produces(ab.concat(bc), c))]
34    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
35}
36
37#[cfg(feature = "nightly")]
38impl<Idx: DeepModel<DeepModelTy = Int> + Step> DoubleEndedIteratorSpec for Range<Idx> {
39    #[logic(open)]
40    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
41        pearlite! {
42            self.start == o.start && self.end.deep_model() >= o.end.deep_model()
43            && (visited.len() > 0 ==> o.end.deep_model() >= o.start.deep_model())
44            && visited.len() == o.end.deep_model() - self.end.deep_model()
45            && forall<i> 0 <= i && i < visited.len() ==>
46                visited[i].deep_model() == self.end.deep_model() - i
47        }
48    }
49
50    #[logic(law)]
51    #[ensures(self.produces_back(Seq::empty(), self))]
52    fn produces_back_refl(self) {}
53
54    #[logic(law)]
55    #[requires(a.produces_back(ab, b))]
56    #[requires(b.produces_back(bc, c))]
57    #[ensures(a.produces_back(ab.concat(bc), c))]
58    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
59}
60
61#[logic(open)]
62#[ensures(r.is_empty_log() == (result == 0))]
63pub fn range_inclusive_len<Idx: DeepModel<DeepModelTy = Int>>(r: RangeInclusive<Idx>) -> Int {
64    pearlite! {
65        if r.is_empty_log() { 0 }
66        else { r.end_log().deep_model() - r.start_log().deep_model() + 1 }
67    }
68}
69
70#[cfg(feature = "nightly")]
71impl<Idx: DeepModel<DeepModelTy = Int> + Step> IteratorSpec for RangeInclusive<Idx> {
72    #[logic(open, prophetic)]
73    fn completed(&mut self) -> bool {
74        pearlite! {
75            self.is_empty_log() && (^self).is_empty_log()
76        }
77    }
78
79    #[logic(open)]
80    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool {
81        pearlite! {
82            visited.len() == range_inclusive_len(self) - range_inclusive_len(o) &&
83            (self.is_empty_log() ==> o.is_empty_log()) &&
84            (o.is_empty_log() || self.end_log() == o.end_log()) &&
85            forall<i> 0 <= i && i < visited.len() ==>
86                visited[i].deep_model() == self.start_log().deep_model() + i
87        }
88    }
89
90    #[logic(open, law)]
91    #[ensures(self.produces(Seq::empty(), self))]
92    fn produces_refl(self) {}
93
94    #[logic(open, law)]
95    #[requires(a.produces(ab, b))]
96    #[requires(b.produces(bc, c))]
97    #[ensures(a.produces(ab.concat(bc), c))]
98    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
99}
100
101#[cfg(feature = "nightly")]
102impl<Idx: DeepModel<DeepModelTy = Int> + Step> DoubleEndedIteratorSpec for RangeInclusive<Idx> {
103    #[logic(open)]
104    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
105        pearlite! {
106            visited.len() == range_inclusive_len(self) - range_inclusive_len(o) &&
107            (self.is_empty_log() ==> o.is_empty_log()) &&
108            (o.is_empty_log() || self.start_log() == o.start_log()) &&
109            forall<i> 0 <= i && i < visited.len() ==>
110                visited[i].deep_model() == self.end_log().deep_model() - i
111        }
112    }
113
114    #[logic(open, law)]
115    #[ensures(self.produces_back(Seq::empty(), self))]
116    fn produces_back_refl(self) {}
117
118    #[logic(open, law)]
119    #[requires(a.produces_back(ab, b))]
120    #[requires(b.produces_back(bc, c))]
121    #[ensures(a.produces_back(ab.concat(bc), c))]
122    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
123}
124
125/// Dummy impls that don't use the unstable trait Step
126#[cfg(not(feature = "nightly"))]
127macro_rules! impl_range {
128    ( $( $ty:tt ),+ ) => {
129        $(
130            impl IteratorSpec for Range<$ty> {}
131            impl IteratorSpec for RangeInclusive<$ty> {}
132            impl DoubleEndedIteratorSpec for Range<$ty> {}
133            impl DoubleEndedIteratorSpec for RangeInclusive<$ty> {}
134        )+
135    };
136}
137
138#[cfg(not(feature = "nightly"))]
139impl_range! { char, i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize }
creusot_contracts/std/iter/range.rs

creusot_contracts/std/iter/
range.rs
