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

creusot_std/std/
vec.rs
