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

creusot_std/std/
vec.rs
