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            #[ensures(result@.len() == n@)]
95            #[ensures(forall<i> 0 <= i && i < n@ ==> result[i] == elem)]
96            fn from_elem<T: Clone>(elem: T, n: usize) -> Vec<T>;
97        }
98    }
99
100    impl<T> Vec<T> {
101        #[check(ghost)]
102        #[ensures(result@.len() == 0)]
103        fn new() -> Vec<T>;
104
105        #[check(terminates)] // can OOM
106        #[ensures(result@.len() == 0)]
107        fn with_capacity(capacity: usize) -> Vec<T>;
108    }
109
110    impl<T, A: Allocator> Vec<T, A> {
111        #[check(ghost)]
112        #[ensures(result@ == self@.len())]
113        fn len(&self) -> usize;
114
115        #[check(terminates)] // can OOM
116        #[ensures((^self)@ == self@.push_back(v))]
117        fn push(&mut self, v: T);
118
119        #[check(ghost)]
120        #[ensures(match result {
121            Some(t) =>
122                (^self)@ == self@.subsequence(0, self@.len() - 1) &&
123                self@ == (^self)@.push_back(t),
124            None => *self == ^self && self@.len() == 0
125        })]
126        fn pop(&mut self) -> Option<T>;
127
128        #[check(ghost)]
129        #[requires(ix@ < self@.len())]
130        #[ensures(result == self[ix@])]
131        #[ensures((^self)@ == self@.subsequence(0, ix@).concat(self@.subsequence(ix@ + 1, self@.len())))]
132        #[ensures((^self)@.len() == self@.len() - 1)]
133        fn remove(&mut self, ix: usize) -> T;
134
135        #[check(terminates)] // can OOM
136        #[ensures((^self)@.len() == self@.len() + 1)]
137        #[ensures(forall<i> 0 <= i && i < index@ ==> (^self)[i] == self[i])]
138        #[ensures((^self)[index@] == element)]
139        #[ensures(forall<i> index@ < i && i < (^self)@.len() ==> (^self)[i] == self[i - 1])]
140        fn insert(&mut self, index: usize, element: T);
141
142        #[check(ghost)]
143        #[ensures(result@ >= self@.len())]
144        fn capacity(&self) -> usize;
145
146        #[check(terminates)] // can OOM
147        #[ensures((^self)@ == self@)]
148        fn reserve(&mut self, additional: usize);
149
150        #[check(terminates)] // can OOM
151        #[ensures((^self)@ == self@)]
152        fn reserve_exact(&mut self, additional: usize);
153
154        #[check(ghost)]
155        #[ensures((^self)@ == self@)]
156        fn shrink_to_fit(&mut self);
157
158        #[check(ghost)]
159        #[ensures((^self)@ == self@)]
160        fn shrink_to(&mut self, min_capacity: usize);
161
162        #[check(ghost)]
163        #[ensures((^self)@.len() == 0)]
164        fn clear(&mut self);
165    }
166
167    impl<T, A: Allocator> Extend<T> for Vec<T, A> {
168        #[requires(I::into_iter.precondition((iter,)))]
169        #[ensures(exists<start_: I::IntoIter, done: &mut I::IntoIter, prod: Seq<T>>
170            inv(start_) && inv(done) && inv(prod) &&
171            I::into_iter.postcondition((iter,), start_) &&
172            done.completed() && start_.produces(prod, *done) && (^self)@ == self@.concat(prod)
173        )]
174        fn extend<I: IntoIterator<Item = T, IntoIter: IteratorSpec>>(&mut self, iter: I);
175    }
176
177    impl<T, I: SliceIndexSpec<[T]>, A: Allocator> IndexMut<I> for Vec<T, A> {
178        #[check(ghost)]
179        #[requires(ix.in_bounds(self@))]
180        #[ensures(ix.has_value(self@, *result))]
181        #[ensures(ix.has_value((^self)@, ^result))]
182        #[ensures(ix.resolve_elswhere(self@, (^self)@))]
183        #[ensures((^self)@.len() == self@.len())]
184        fn index_mut(&mut self, ix: I) -> &mut <Vec<T, A> as Index<I>>::Output;
185    }
186
187    impl<T, I: SliceIndexSpec<[T]>, A: Allocator> Index<I> for Vec<T, A> {
188        #[check(ghost)]
189        #[requires(ix.in_bounds(self@))]
190        #[ensures(ix.has_value(self@, *result))]
191        fn index(&self, ix: I) -> & <Vec<T, A> as Index<I>>::Output;
192    }
193
194    impl<T, A: Allocator> Deref for Vec<T, A> {
195        #[check(ghost)]
196        #[ensures(result@ == self@)]
197        fn deref(&self) -> &[T];
198    }
199
200    impl<T, A: Allocator> DerefMut for Vec<T, A> {
201        #[check(ghost)]
202        #[ensures(result@ == self@)]
203        #[ensures((^result)@ == (^self)@)]
204        fn deref_mut(&mut self) -> &mut [T];
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) -> core::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) -> core::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 alloc::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_std/std/vec.rs

creusot_std/std/
vec.rs
