creusot_contracts/std/
vec.rs

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

creusot_contracts/std/
vec.rs
