creusot_contracts/std/
vec.rs

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

creusot_contracts/std/
vec.rs
