creusot_std/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;
6#[cfg(creusot)]
7use std::ops::{Deref, DerefMut, Index, IndexMut};
8use std::vec::*;
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 std {
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        #[check(ghost)]
167        #[ensures(result@ == self@)]
168        fn into_boxed_slice(self) -> Box<[T], A>;
169    }
170
171    impl<T, A: Allocator> Extend<T> for Vec<T, A> {
172        #[requires(I::into_iter.precondition((iter,)))]
173        #[ensures(exists<start_: I::IntoIter, done: &mut I::IntoIter, prod: Seq<T>>
174            inv(start_) && inv(done) && inv(prod) &&
175            I::into_iter.postcondition((iter,), start_) &&
176            done.completed() && start_.produces(prod, *done) && (^self)@ == self@.concat(prod)
177        )]
178        fn extend<I: IntoIterator<Item = T, IntoIter: IteratorSpec>>(&mut self, iter: I);
179    }
180
181    impl<T, I: SliceIndexSpec<[T]>, A: Allocator> IndexMut<I> for Vec<T, A> {
182        #[check(ghost)]
183        #[requires(ix.in_bounds(self@))]
184        #[ensures(ix.has_value(self@, *result))]
185        #[ensures(ix.has_value((^self)@, ^result))]
186        #[ensures(ix.resolve_elswhere(self@, (^self)@))]
187        #[ensures((^self)@.len() == self@.len())]
188        fn index_mut(&mut self, ix: I) -> &mut <Vec<T, A> as Index<I>>::Output;
189    }
190
191    impl<T, I: SliceIndexSpec<[T]>, A: Allocator> Index<I> for Vec<T, A> {
192        #[check(ghost)]
193        #[requires(ix.in_bounds(self@))]
194        #[ensures(ix.has_value(self@, *result))]
195        fn index(&self, ix: I) -> & <Vec<T, A> as Index<I>>::Output;
196    }
197
198    impl<T, A: Allocator> Deref for Vec<T, A> {
199        #[check(ghost)]
200        #[ensures(result@ == self@)]
201        fn deref(&self) -> &[T];
202    }
203
204    impl<T, A: Allocator> DerefMut for Vec<T, A> {
205        #[check(ghost)]
206        #[ensures(result@ == self@)]
207        #[ensures((^self)@.len() == (*self)@.len())]
208        #[ensures((^result)@ == (^self)@)]
209        fn deref_mut(&mut self) -> &mut [T];
210    }
211
212    impl<T, A: Allocator> IntoIterator for Vec<T, A> {
213        #[check(ghost)]
214        #[ensures(self@ == result@)]
215        fn into_iter(self) -> IntoIter<T, A>;
216    }
217
218    impl<'a, T, A: Allocator> IntoIterator for &'a Vec<T, A> {
219        #[check(ghost)]
220        #[ensures(self@ == result@@)]
221        fn into_iter(self) -> core::slice::Iter<'a, T>;
222    }
223
224    impl<'a, T, A: Allocator> IntoIterator for &'a mut Vec<T, A> {
225        #[check(ghost)]
226        #[ensures(self@ == result@@)]
227        #[ensures((^self)@ == (^result@)@)]
228        fn into_iter(self) -> core::slice::IterMut<'a, T>;
229    }
230
231    impl<T> Default for Vec<T> {
232        #[check(ghost)]
233        #[ensures(result@ == Seq::empty())]
234        fn default() -> Vec<T>;
235    }
236
237    impl<T: Clone, A: Allocator + Clone> Clone for Vec<T, A> {
238        #[check(terminates)]
239        #[ensures(self@.len() == result@.len())]
240        #[ensures(forall<i> 0 <= i && i < self@.len() ==>
241            T::clone.postcondition((&self@[i],), result@[i]))]
242        fn clone(&self) -> Vec<T, A>;
243    }
244}
245
246#[cfg(feature = "nightly")]
247impl<T, A: Allocator> View for IntoIter<T, A> {
248    type ViewTy = Seq<T>;
249
250    #[logic(opaque)]
251    fn view(self) -> Self::ViewTy {
252        dead
253    }
254}
255
256#[cfg(feature = "nightly")]
257impl<T, A: Allocator> Resolve for IntoIter<T, A> {
258    #[logic(open, prophetic, inline)]
259    fn resolve(self) -> bool {
260        pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self@[i]) }
261    }
262
263    #[trusted]
264    #[logic(prophetic)]
265    #[requires(structural_resolve(self))]
266    #[ensures(self.resolve())]
267    fn resolve_coherence(self) {}
268}
269
270#[cfg(feature = "nightly")]
271impl<T, A: Allocator> IteratorSpec for IntoIter<T, A> {
272    #[logic(open, prophetic)]
273    fn completed(&mut self) -> bool {
274        pearlite! { resolve(self) && self@ == Seq::empty() }
275    }
276
277    #[logic(open)]
278    fn produces(self, visited: Seq<T>, rhs: Self) -> bool {
279        pearlite! {
280            self@ == visited.concat(rhs@)
281        }
282    }
283
284    #[logic(law)]
285    #[ensures(self.produces(Seq::empty(), self))]
286    fn produces_refl(self) {
287        let _ = Seq::<T>::concat_empty;
288    }
289
290    #[logic(law)]
291    #[requires(a.produces(ab, b))]
292    #[requires(b.produces(bc, c))]
293    #[ensures(a.produces(ab.concat(bc), c))]
294    fn produces_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {
295        let _ = Seq::<T>::concat_assoc;
296    }
297}
298
299#[cfg(feature = "nightly")]
300impl<T, A: Allocator> DoubleEndedIteratorSpec for IntoIter<T, A> {
301    #[logic(open)]
302    fn produces_back(self, visited: Seq<T>, rhs: Self) -> bool {
303        pearlite! {
304            self@ == rhs@.concat(visited.reverse())
305        }
306    }
307
308    #[logic(law)]
309    #[ensures(self.produces_back(Seq::empty(), self))]
310    fn produces_back_refl(self) {
311        let _ = Seq::<T>::reverse_empty();
312        let _ = Seq::<T>::concat_empty;
313    }
314
315    #[logic(law)]
316    #[requires(a.produces_back(ab, b))]
317    #[requires(b.produces_back(bc, c))]
318    #[ensures(a.produces_back(ab.concat(bc), c))]
319    fn produces_back_trans(a: Self, ab: Seq<T>, b: Self, bc: Seq<T>, c: Self) {
320        let _ = ab.reverse_concat(bc);
321        let _ = Seq::<T>::concat_assoc;
322    }
323}
324
325impl<T> FromIteratorSpec<T> for Vec<T> {
326    #[logic(open)]
327    fn from_iter_post(prod: Seq<T>, res: Self) -> bool {
328        pearlite! { prod == res@ }
329    }
330}
331
332/// Dummy impls that don't use the unstable trait Allocator
333#[cfg(not(feature = "nightly"))]
334mod impls {
335    use crate::prelude::*;
336    use std::vec::*;
337
338    impl<T> View for Vec<T> {
339        type ViewTy = Seq<T>;
340    }
341
342    impl<T: DeepModel> DeepModel for Vec<T> {
343        type DeepModelTy = Seq<T::DeepModelTy>;
344    }
345    impl<T> Resolve for Vec<T> {}
346    impl<T> Invariant for Vec<T> {}
347    impl<T> View for IntoIter<T> {
348        type ViewTy = Seq<T>;
349    }
350    impl<T> Resolve for IntoIter<T> {}
351    impl<T> IteratorSpec for IntoIter<T> {}
352}
353
354/// Creusot-friendly replacement of `vec!`
355///
356/// The std vec macro uses special magic to construct the array argument
357/// to `Box::new` directly on the heap. Because the generated MIR is hard
358/// to translate, we provide a custom `vec!` macro which does not do this.
359#[macro_export]
360macro_rules! vec {
361    () => (
362        ::std::vec::Vec::new()
363    );
364    ($elem:expr; $n:expr) => (
365        ::std::vec::from_elem($elem, $n)
366    );
367    ($($x:expr),*) => (
368        <[_]>::into_vec(::std::boxed::Box::new([$($x),*]))
369    );
370    ($($x:expr,)*) => (vec![$($x),*])
371}
372pub use vec;
creusot_std/std/vec.rs

creusot_std/std/
vec.rs
