creusot_std/std/
vec.rs

1#[cfg(creusot)]
2use crate::{invariant::inv, resolve::structural_resolve, std::slice::SliceIndexSpec};
3use crate::{logic::ops::IndexLogic, prelude::*};
4use alloc::vec::*;
5#[cfg(feature = "nightly")]
6use core::alloc::Allocator;
7#[cfg(creusot)]
8use core::ops::{Deref, DerefMut, Index, IndexMut};
9
10#[cfg(feature = "nightly")]
11impl<T, A: Allocator> View for Vec<T, A> {
12    type ViewTy = Seq<T>;
13
14    #[trusted]
15    #[logic(opaque)]
16    #[ensures(result.len() <= usize::MAX@)]
17    fn view(self) -> Seq<T> {
18        dead
19    }
20}
21
22#[cfg(feature = "nightly")]
23impl<T: DeepModel, A: Allocator> DeepModel for Vec<T, A> {
24    type DeepModelTy = Seq<T::DeepModelTy>;
25
26    #[trusted]
27    #[logic(opaque)]
28    #[ensures(self.view().len() == result.len())]
29    #[ensures(forall<i> 0 <= i && i < self.view().len()
30              ==> result[i] == self[i].deep_model())]
31    fn deep_model(self) -> Self::DeepModelTy {
32        dead
33    }
34}
35
36#[cfg(feature = "nightly")]
37impl<T, A: Allocator> IndexLogic<Int> for Vec<T, A> {
38    type Item = T;
39
40    #[logic(open, inline)]
41    fn index_logic(self, ix: Int) -> Self::Item {
42        pearlite! { self@[ix] }
43    }
44}
45
46#[cfg(feature = "nightly")]
47impl<T, A: Allocator> IndexLogic<usize> for Vec<T, A> {
48    type Item = T;
49
50    #[logic(open, inline)]
51    fn index_logic(self, ix: usize) -> Self::Item {
52        pearlite! { self@[ix@] }
53    }
54}
55
56/// Dummy impls that don't use the unstable trait Allocator
57#[cfg(not(feature = "nightly"))]
58impl<T> IndexLogic<Int> for Vec<T> {
59    type Item = T;
60}
61
62#[cfg(not(feature = "nightly"))]
63impl<T> IndexLogic<usize> for Vec<T> {
64    type Item = T;
65}
66
67#[cfg(feature = "nightly")]
68impl<T, A: Allocator> Resolve for Vec<T, A> {
69    #[logic(open, prophetic, inline)]
70    #[creusot::trusted_trivial_if_param_trivial]
71    fn resolve(self) -> bool {
72        pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self[i]) }
73    }
74
75    #[trusted]
76    #[logic(prophetic)]
77    #[requires(structural_resolve(self))]
78    #[ensures(self.resolve())]
79    fn resolve_coherence(self) {}
80}
81
82#[cfg(feature = "nightly")]
83impl<T, A: Allocator> Invariant for Vec<T, A> {
84    #[logic(open, prophetic)]
85    #[creusot::trusted_trivial_if_param_trivial]
86    fn invariant(self) -> bool {
87        pearlite! { inv(self@) }
88    }
89}
90
91extern_spec! {
92    mod alloc {
93        mod vec {
94            impl<T> Vec<T> {
95                #[check(ghost)]
96                #[ensures(result@.len() == 0)]
97                fn new() -> Vec<T>;
98
99                #[check(terminates)] // can OOM
100                #[ensures(result@.len() == 0)]
101                fn with_capacity(capacity: usize) -> Vec<T>;
102            }
103            impl<T, A: Allocator> Vec<T, A> {
104                #[check(ghost)]
105                #[ensures(result@ == self@.len())]
106                fn len(&self) -> usize;
107
108                #[check(terminates)] // can OOM
109                #[ensures((^self)@ == self@.push_back(v))]
110                fn push(&mut self, v: T);
111
112                #[check(ghost)]
113                #[ensures(match result {
114                    Some(t) =>
115                        (^self)@ == self@.subsequence(0, self@.len() - 1) &&
116                        self@ == (^self)@.push_back(t),
117                    None => *self == ^self && self@.len() == 0
118                })]
119                fn pop(&mut self) -> Option<T>;
120
121                #[check(ghost)]
122                #[requires(ix@ < self@.len())]
123                #[ensures(result == self[ix@])]
124                #[ensures((^self)@ == self@.subsequence(0, ix@).concat(self@.subsequence(ix@ + 1, self@.len())))]
125                #[ensures((^self)@.len() == self@.len() - 1)]
126                fn remove(&mut self, ix: usize) -> T;
127
128                #[check(terminates)] // can OOM
129                #[ensures((^self)@.len() == self@.len() + 1)]
130                #[ensures(forall<i> 0 <= i && i < index@ ==> (^self)[i] == self[i])]
131                #[ensures((^self)[index@] == element)]
132                #[ensures(forall<i> index@ < i && i < (^self)@.len() ==> (^self)[i] == self[i - 1])]
133                fn insert(&mut self, index: usize, element: T);
134
135                #[check(ghost)]
136                #[ensures(result@ >= self@.len())]
137                fn capacity(&self) -> usize;
138
139                #[check(terminates)] // can OOM
140                #[ensures((^self)@ == self@)]
141                fn reserve(&mut self, additional: usize);
142
143                #[check(terminates)] // can OOM
144                #[ensures((^self)@ == self@)]
145                fn reserve_exact(&mut self, additional: usize);
146
147                #[check(ghost)]
148                #[ensures((^self)@ == self@)]
149                fn shrink_to_fit(&mut self);
150
151                #[check(ghost)]
152                #[ensures((^self)@ == self@)]
153                fn shrink_to(&mut self, min_capacity: usize);
154
155                #[check(ghost)]
156                #[ensures((^self)@.len() == 0)]
157                fn clear(&mut self);
158            }
159
160            impl<T, A: Allocator> Extend<T> for Vec<T, A> {
161                #[requires(I::into_iter.precondition((iter,)))]
162                #[ensures(exists<start_: I::IntoIter, done: &mut I::IntoIter, prod: Seq<T>>
163                    inv(start_) && inv(done) && inv(prod) &&
164                    I::into_iter.postcondition((iter,), start_) &&
165                    done.completed() && start_.produces(prod, *done) && (^self)@ == self@.concat(prod)
166                )]
167                fn extend<I: IntoIterator<Item = T, IntoIter: IteratorSpec>>(&mut self, iter: I);
168            }
169
170            impl<T, I: SliceIndexSpec<[T]>, A: Allocator> IndexMut<I> for Vec<T, A> {
171                #[check(ghost)]
172                #[requires(ix.in_bounds(self@))]
173                #[ensures(ix.has_value(self@, *result))]
174                #[ensures(ix.has_value((^self)@, ^result))]
175                #[ensures(ix.resolve_elswhere(self@, (^self)@))]
176                #[ensures((^self)@.len() == self@.len())]
177                fn index_mut(&mut self, ix: I) -> &mut <Vec<T, A> as Index<I>>::Output;
178            }
179
180            impl<T, I: SliceIndexSpec<[T]>, A: Allocator> Index<I> for Vec<T, A> {
181                #[check(ghost)]
182                #[requires(ix.in_bounds(self@))]
183                #[ensures(ix.has_value(self@, *result))]
184                fn index(&self, ix: I) -> & <Vec<T, A> as Index<I>>::Output;
185            }
186
187            impl<T, A: Allocator> Deref for Vec<T, A> {
188                #[check(ghost)]
189                #[ensures(result@ == self@)]
190                fn deref(&self) -> &[T];
191            }
192
193            impl<T, A: Allocator> DerefMut for Vec<T, A> {
194                #[check(ghost)]
195                #[ensures(result@ == self@)]
196                #[ensures((^result)@ == (^self)@)]
197                fn deref_mut(&mut self) -> &mut [T];
198            }
199
200            #[ensures(result@.len() == n@)]
201            #[ensures(forall<i> 0 <= i && i < n@ ==> result[i] == elem)]
202            fn from_elem<T: Clone>(elem: T, n: usize) -> Vec<T>;
203        }
204    }
205
206    impl<T, A: Allocator> IntoIterator for Vec<T, A> {
207        #[check(ghost)]
208        #[ensures(self@ == result@)]
209        fn into_iter(self) -> IntoIter<T, A>;
210    }
211
212    impl<'a, T, A: Allocator> IntoIterator for &'a Vec<T, A> {
213        #[check(ghost)]
214        #[ensures(self@ == result@@)]
215        fn into_iter(self) -> core::slice::Iter<'a, T>;
216    }
217
218    impl<'a, T, A: Allocator> IntoIterator for &'a mut Vec<T, A> {
219        #[check(ghost)]
220        #[ensures(self@ == result@@)]
221        fn into_iter(self) -> core::slice::IterMut<'a, T>;
222    }
223
224    impl<T> Default for Vec<T> {
225        #[check(ghost)]
226        #[ensures(result@ == Seq::empty())]
227        fn default() -> Vec<T>;
228    }
229
230    impl<T: Clone, A: Allocator + Clone> Clone for Vec<T, A> {
231        #[check(terminates)]
232        #[ensures(self@.len() == result@.len())]
233        #[ensures(forall<i> 0 <= i && i < self@.len() ==>
234            T::clone.postcondition((&self@[i],), result@[i]))]
235        fn clone(&self) -> Vec<T, A>;
236    }
237}
238
239#[cfg(feature = "nightly")]
240impl<T, A: Allocator> View for IntoIter<T, A> {
241    type ViewTy = Seq<T>;
242
243    #[logic(opaque)]
244    fn view(self) -> Self::ViewTy {
245        dead
246    }
247}
248
249#[cfg(feature = "nightly")]
250impl<T, A: Allocator> Resolve for IntoIter<T, A> {
251    #[logic(open, prophetic, inline)]
252    fn resolve(self) -> bool {
253        pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self@[i]) }
254    }
255
256    #[trusted]
257    #[logic(prophetic)]
258    #[requires(structural_resolve(self))]
259    #[ensures(self.resolve())]
260    fn resolve_coherence(self) {}
261}
262
263#[cfg(feature = "nightly")]
264impl<T, A: Allocator> IteratorSpec for IntoIter<T, A> {
265    #[logic(open, prophetic)]
266    fn completed(&mut self) -> bool {
267        pearlite! { resolve(self) && self@ == Seq::empty() }
268    }
269
270    #[logic(open)]
271    fn produces(self, visited: Seq<T>, rhs: Self) -> bool {
272        pearlite! {
273            self@ == visited.concat(rhs@)
274        }
275    }
276
277    #[logic(open, law)]
278    #[ensures(self.produces(Seq::empty(), self))]
279    fn produces_refl(self) {}
280
281    #[logic(open, law)]
282    #[requires(a.produces(ab, b))]
283    #[requires(b.produces(bc, c))]
284    #[ensures(a.produces(ab.concat(bc), c))]
285    fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {}
286}
287
288impl<T> FromIteratorSpec<T> for Vec<T> {
289    #[logic(open)]
290    fn from_iter_post(prod: Seq<T>, res: Self) -> bool {
291        pearlite! { prod == res@ }
292    }
293}
294
295/// Dummy impls that don't use the unstable trait Allocator
296#[cfg(not(feature = "nightly"))]
297mod impls {
298    use crate::prelude::*;
299    use alloc::vec::*;
300
301    impl<T> View for Vec<T> {
302        type ViewTy = Seq<T>;
303    }
304
305    impl<T: DeepModel> DeepModel for Vec<T> {
306        type DeepModelTy = Seq<T::DeepModelTy>;
307    }
308    impl<T> Resolve for Vec<T> {}
309    impl<T> Invariant for Vec<T> {}
310    impl<T> View for IntoIter<T> {
311        type ViewTy = Seq<T>;
312    }
313    impl<T> Resolve for IntoIter<T> {}
314    impl<T> IteratorSpec for IntoIter<T> {}
315}
316
317/// Creusot-friendly replacement of `vec!`
318///
319/// The std vec macro uses special magic to construct the array argument
320/// to `Box::new` directly on the heap. Because the generated MIR is hard
321/// to translate, we provide a custom `vec!` macro which does not do this.
322#[macro_export]
323macro_rules! vec {
324    () => (
325        ::std::vec::Vec::new()
326    );
327    ($elem:expr; $n:expr) => (
328        ::std::vec::from_elem($elem, $n)
329    );
330    ($($x:expr),*) => (
331        <[_]>::into_vec(::std::boxed::Box::new([$($x),*]))
332    );
333    ($($x:expr,)*) => (vec![$($x),*])
334}
335pub use vec;
creusot_std/std/vec.rs

creusot_std/std/
vec.rs
