creusot_std/std/
array.rs

1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{invariant::*, logic::ops::IndexLogic, prelude::*, std::iter::ExactSizeIteratorSpec};
4use core::array::*;
5
6impl<T, const N: usize> Invariant for [T; N] {
7    #[logic(open, prophetic)]
8    fn invariant(self) -> bool {
9        pearlite! { inv(self@) && self@.len() == N@ }
10    }
11}
12
13impl<T, const N: usize> View for [T; N] {
14    type ViewTy = Seq<T>;
15
16    #[logic]
17    #[cfg_attr(target_pointer_width = "16", builtin("creusot.slice.Slice16.view"))]
18    #[cfg_attr(target_pointer_width = "32", builtin("creusot.slice.Slice32.view"))]
19    #[cfg_attr(target_pointer_width = "64", builtin("creusot.slice.Slice64.view"))]
20    fn view(self) -> Self::ViewTy {
21        dead
22    }
23}
24
25impl<T: DeepModel, const N: usize> DeepModel for [T; N] {
26    type DeepModelTy = Seq<T::DeepModelTy>;
27
28    #[trusted]
29    #[logic(opaque)]
30    #[ensures(self.view().len() == result.len())]
31    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == self[i].deep_model())]
32    fn deep_model(self) -> Self::DeepModelTy {
33        dead
34    }
35}
36
37impl<T, const N: usize> Resolve for [T; N] {
38    #[logic(open, prophetic, inline)]
39    #[creusot::trusted_trivial_if_param_trivial]
40    fn resolve(self) -> bool {
41        pearlite! { forall<i: Int> 0 <= i && i < N@ ==> resolve(self@[i]) }
42    }
43
44    #[trusted]
45    #[logic(prophetic)]
46    #[requires(structural_resolve(self))]
47    #[ensures(self.resolve())]
48    fn resolve_coherence(self) {}
49}
50
51impl<T, const N: usize> IndexLogic<Int> for [T; N] {
52    type Item = T;
53
54    #[logic(open, inline)]
55    fn index_logic(self, ix: Int) -> Self::Item {
56        pearlite! { self@[ix] }
57    }
58}
59
60impl<T, const N: usize> IndexLogic<usize> for [T; N] {
61    type Item = T;
62
63    #[logic(open, inline)]
64    fn index_logic(self, ix: usize) -> Self::Item {
65        pearlite! { self@[ix@] }
66    }
67}
68
69impl<T, const N: usize> View for IntoIter<T, N> {
70    type ViewTy = Seq<T>;
71
72    #[logic(opaque)]
73    fn view(self) -> Self::ViewTy {
74        dead
75    }
76}
77
78impl<T, const N: usize> IteratorSpec for IntoIter<T, N> {
79    #[logic(open, prophetic)]
80    fn produces(self, visited: Seq<T>, o: Self) -> bool {
81        pearlite! { self@ == visited.concat(o@) }
82    }
83
84    #[logic(open, prophetic)]
85    fn completed(&mut self) -> bool {
86        pearlite! { resolve(self) && self@ == Seq::empty() }
87    }
88
89    #[logic(law)]
90    #[ensures(self.produces(Seq::empty(), self))]
91    fn produces_refl(self) {
92        let _ = Seq::<T>::concat_empty;
93    }
94
95    #[logic(law)]
96    #[requires(a.produces(ab, b))]
97    #[requires(b.produces(bc, c))]
98    #[ensures(a.produces(ab.concat(bc), c))]
99    fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {
100        let _ = ab.reverse_concat(bc);
101        let _ = Seq::<T>::concat_assoc;
102    }
103}
104
105extern_spec! {
106    impl<T, const N: usize> Iterator for IntoIter<T, N> {
107        #[ensures(result.0@ == self@.len())]
108        #[ensures(result.1 == Some(result.0))]
109        fn size_hint(&self) -> (usize, Option<usize>);
110    }
111}
112
113impl<T, const N: usize> ExactSizeIteratorSpec for IntoIter<T, N> {
114    #[logic(law)]
115    #[requires(Self::size_hint.postcondition((self,), r))]
116    #[ensures(r.1 == Some(r.0))]
117    #[allow(unused_variables)]
118    fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
119}
120
121impl<T, const N: usize> DoubleEndedIteratorSpec for IntoIter<T, N> {
122    #[logic(open)]
123    fn produces_back(self, visited: Seq<T>, o: Self) -> bool {
124        pearlite! {
125            self@ == o@.concat(visited.reverse())
126        }
127    }
128
129    #[logic(open, prophetic)]
130    fn completed_back(&mut self) -> bool {
131        self.completed()
132    }
133
134    #[logic(law)]
135    #[ensures(self.produces_back(Seq::empty(), self))]
136    fn produces_back_refl(self) {
137        let _ = Seq::<T>::reverse_empty();
138        let _ = Seq::<T>::concat_empty;
139    }
140
141    #[logic(law)]
142    #[requires(a.produces_back(ab, b))]
143    #[requires(b.produces_back(bc, c))]
144    #[ensures(a.produces_back(ab.concat(bc), c))]
145    fn produces_back_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {
146        let _ = ab.reverse_concat(bc);
147        let _ = Seq::<T>::concat_assoc;
148    }
149
150    #[logic(law)]
151    #[requires(Self::size_hint.postcondition((self,), r))]
152    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
153        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
154    #[ensures(match r.1 {
155        Some(r) => {
156            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
157        }
158        None => true
159    })]
160    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
161}
162
163extern_spec! {
164    impl<T, const N: usize> IntoIterator for [T; N] {
165        #[check(ghost)]
166        #[ensures(self@ == result@)]
167        fn into_iter(self) -> core::array::IntoIter<T, N>;
168    }
169
170    impl<T: Clone, const N: usize> Clone for [T; N] {
171        #[ensures(forall<i> 0 <= i && i < self@.len() ==>
172            T::clone.postcondition((&self@[i],), result@[i]))]
173        fn clone(&self) -> [T; N];
174    }
175
176    impl<T, const N: usize> [T; N] {
177        #[check(ghost)]
178        #[ensures(result@ == self@)]
179        fn as_slice(&self) -> &[T] {
180            self
181        }
182
183        #[check(ghost)]
184        #[ensures(result@ == self@)]
185        #[ensures((^self)@.len() == (*self)@.len())]
186        #[ensures((^result)@ == (^self)@)]
187        fn as_mut_slice(&mut self) -> &mut [T] {
188            self
189        }
190    }
191}
creusot_std/std/array.rs

creusot_std/std/
array.rs
