creusot_std/std/
vec.rs

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

creusot_std/std/
vec.rs
