creusot_contracts/std/
slice.rs

1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{
4    ghost::PtrOwn,
5    invariant::*,
6    logic::ops::IndexLogic,
7    std::ops::{
8        Index, IndexMut, Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive,
9    },
10    *,
11};
12#[cfg(feature = "nightly")]
13use ::std::alloc::Allocator;
14pub use ::std::slice::*;
15
16impl<T> Invariant for [T] {
17    #[logic(open, prophetic)]
18    #[creusot::trusted_ignore_structural_inv]
19    #[creusot::trusted_is_tyinv_trivial_if_param_trivial]
20    fn invariant(self) -> bool {
21        pearlite! { inv(self@) }
22    }
23}
24
25impl<T> View for [T] {
26    type ViewTy = Seq<T>;
27
28    #[logic]
29    #[cfg_attr(target_pointer_width = "16", builtin("creusot.slice.Slice16.view"))]
30    #[cfg_attr(target_pointer_width = "32", builtin("creusot.slice.Slice32.view"))]
31    #[cfg_attr(target_pointer_width = "64", builtin("creusot.slice.Slice64.view"))]
32    fn view(self) -> Self::ViewTy {
33        dead
34    }
35}
36
37impl<T: DeepModel> DeepModel for [T] {
38    type DeepModelTy = Seq<T::DeepModelTy>;
39
40    #[trusted]
41    #[logic(opaque)]
42    #[ensures((&self)@.len() == result.len())]
43    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == (&self)[i].deep_model())]
44    fn deep_model(self) -> Self::DeepModelTy {
45        dead
46    }
47}
48
49impl<T> IndexLogic<Int> for [T] {
50    type Item = T;
51
52    #[logic(open, inline)]
53    fn index_logic(self, ix: Int) -> Self::Item {
54        pearlite! { self@[ix] }
55    }
56}
57
58impl<T> IndexLogic<usize> for [T] {
59    type Item = T;
60
61    #[logic(open, inline)]
62    fn index_logic(self, ix: usize) -> Self::Item {
63        pearlite! { self@[ix@] }
64    }
65}
66
67pub trait SliceExt<T> {
68    #[logic]
69    fn to_mut_seq(&mut self) -> Seq<&mut T>;
70
71    #[logic]
72    fn to_ref_seq(&self) -> Seq<&T>;
73
74    #[check(ghost)]
75    fn as_ptr_own(&self) -> (*const T, Ghost<&PtrOwn<[T]>>);
76}
77
78impl<T> SliceExt<T> for [T] {
79    #[trusted]
80    #[logic(opaque)]
81    #[ensures(result.len() == self@.len())]
82    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == &mut self[i])]
83    // TODO: replace with a map function applied on a sequence
84    fn to_mut_seq(&mut self) -> Seq<&mut T> {
85        dead
86    }
87
88    #[trusted]
89    #[logic(opaque)]
90    #[ensures(result.len() == self@.len())]
91    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == &self[i])]
92    fn to_ref_seq(&self) -> Seq<&T> {
93        dead
94    }
95
96    /// Convert `&[T]` to `*const T` and a shared ownership token.
97    #[check(ghost)]
98    #[ensures(result.0 == result.1.ptr() as *const T)]
99    #[ensures(self@ == result.1.val()@)]
100    #[erasure(Self::as_ptr)]
101    fn as_ptr_own(&self) -> (*const T, Ghost<&PtrOwn<[T]>>) {
102        let (ptr, own) = PtrOwn::from_ref(self);
103        (ptr as *const T, own)
104    }
105}
106
107pub trait SliceIndex<T: ?Sized>: ::std::slice::SliceIndex<T>
108where
109    T: View,
110{
111    #[logic]
112    fn in_bounds(self, seq: T::ViewTy) -> bool;
113
114    #[logic]
115    fn has_value(self, seq: T::ViewTy, out: Self::Output) -> bool;
116
117    #[logic]
118    fn resolve_elswhere(self, old: T::ViewTy, fin: T::ViewTy) -> bool;
119}
120
121impl<T> SliceIndex<[T]> for usize {
122    #[logic(open, inline)]
123    fn in_bounds(self, seq: Seq<T>) -> bool {
124        pearlite! { self@ < seq.len() }
125    }
126
127    #[logic(open, inline)]
128    fn has_value(self, seq: Seq<T>, out: T) -> bool {
129        pearlite! { seq[self@] == out }
130    }
131
132    #[logic(open, inline)]
133    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
134        pearlite! { forall<i> 0 <= i && i != self@ && i < old.len() ==> old[i] == fin[i] }
135    }
136}
137
138impl<T> SliceIndex<[T]> for Range<usize> {
139    #[logic(open)]
140    fn in_bounds(self, seq: Seq<T>) -> bool {
141        pearlite! { self.start@ <= self.end@ && self.end@ <= seq.len() }
142    }
143
144    #[logic(open)]
145    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
146        pearlite! { seq.subsequence(self.start@, self.end@) == out@ }
147    }
148
149    #[logic(open)]
150    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
151        pearlite! {
152            forall<i> 0 <= i && (i < self.start@ || self.end@ <= i) && i < old.len()
153            ==> old[i] == fin[i]
154        }
155    }
156}
157
158impl<T> SliceIndex<[T]> for RangeInclusive<usize> {
159    #[trusted]
160    #[logic(opaque)]
161    #[ensures(self.end_log()@ < seq.len() && self.start_log()@ <= self.end_log()@+1 ==> result)]
162    #[ensures(self.end_log()@ >= seq.len() ==> !result)]
163    fn in_bounds(self, seq: Seq<T>) -> bool {
164        dead
165    }
166
167    #[logic(open)]
168    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
169        pearlite! {
170            if self.is_empty_log() { out@ == Seq::empty() }
171            else { seq.subsequence(self.start_log()@, self.end_log()@ + 1) == out@ }
172        }
173    }
174
175    #[logic(open)]
176    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
177        pearlite! {
178            forall<i> 0 <= i
179                && (i < self.start_log()@ || self.end_log()@ < i || self.is_empty_log())
180                && i < old.len()
181                ==> old[i] == fin[i]
182        }
183    }
184}
185
186impl<T> SliceIndex<[T]> for RangeTo<usize> {
187    #[logic(open)]
188    fn in_bounds(self, seq: Seq<T>) -> bool {
189        pearlite! { self.end@ <= seq.len() }
190    }
191
192    #[logic(open)]
193    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
194        pearlite! { seq.subsequence(0, self.end@) == out@ }
195    }
196
197    #[logic(open)]
198    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
199        pearlite! { forall<i> self.end@ <= i && i < old.len() ==> old[i] == fin[i] }
200    }
201}
202
203impl<T> SliceIndex<[T]> for RangeFrom<usize> {
204    #[logic(open)]
205    fn in_bounds(self, seq: Seq<T>) -> bool {
206        pearlite! { self.start@ <= seq.len() }
207    }
208
209    #[logic(open)]
210    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
211        pearlite! { seq.subsequence(self.start@, seq.len()) == out@ }
212    }
213
214    #[logic(open)]
215    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
216        pearlite! {
217            forall<i> 0 <= i && i < self.start@ && i < old.len() ==> old[i] == fin[i]
218        }
219    }
220}
221
222impl<T> SliceIndex<[T]> for RangeFull {
223    #[logic(open)]
224    fn in_bounds(self, _seq: Seq<T>) -> bool {
225        pearlite! { true }
226    }
227
228    #[logic(open)]
229    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
230        pearlite! { seq == out@ }
231    }
232
233    #[logic(open)]
234    fn resolve_elswhere(self, _old: Seq<T>, _fin: Seq<T>) -> bool {
235        pearlite! { true }
236    }
237}
238
239impl<T> SliceIndex<[T]> for RangeToInclusive<usize> {
240    #[logic(open)]
241    fn in_bounds(self, seq: Seq<T>) -> bool {
242        pearlite! { self.end@ < seq.len() }
243    }
244
245    #[logic(open)]
246    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
247        pearlite! { seq.subsequence(0, self.end@ + 1) == out@ }
248    }
249
250    #[logic(open)]
251    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
252        pearlite! { forall<i> self.end@ < i && i < old.len() ==> old[i] == fin[i] }
253    }
254}
255
256extern_spec! {
257    impl<T> [T] {
258        #[check(ghost)]
259        #[requires(self@.len() == src@.len())]
260        #[ensures((^self)@ == src@)]
261        fn copy_from_slice(&mut self, src: &[T]) where T: Copy;
262
263        #[check(ghost)]
264        #[ensures(self@.len() == result@)]
265        fn len(&self) -> usize;
266
267        #[check(ghost)]
268        #[requires(i@ < self@.len())]
269        #[requires(j@ < self@.len())]
270        #[ensures((^self)@.exchange(self@, i@, j@))]
271        fn swap(&mut self, i: usize, j: usize);
272
273        #[ensures(ix.in_bounds(self@) ==> exists<r> result == Some(r) && ix.has_value(self@, *r))]
274        #[ensures(ix.in_bounds(self@) || result == None)]
275        fn get<I: SliceIndex<[T]>>(&self, ix: I) -> Option<&<I as ::std::slice::SliceIndex<[T]>>::Output>;
276
277        #[ensures((^self)@.len() == self@.len())]
278        #[ensures(ix.in_bounds(self@) ==> exists<r> result == Some(r) && ix.has_value(self@, *r) && ix.has_value((^self)@, ^r) && ix.resolve_elswhere(self@, (^self)@))]
279        #[ensures(ix.in_bounds(self@) || result == None)]
280        fn get_mut<I: SliceIndex<[T]>>(&mut self, ix: I) -> Option<&mut <I as ::std::slice::SliceIndex<[T]>>::Output>;
281
282        #[check(ghost)]
283        #[requires(mid@ <= self@.len())]
284        #[ensures({
285            let (l,r) = result;  let sl = self@.len();
286            ((^self)@.len() == sl) &&
287            self@.subsequence(0, mid@) == l@ &&
288            self@.subsequence(mid@, sl) == r@ &&
289            (^self)@.subsequence(0, mid@) == (^l)@ &&
290            (^self)@.subsequence(mid@, sl) == (^r)@
291        })]
292        fn split_at_mut(&mut self, mid: usize) -> (&mut [T], &mut [T]);
293
294        #[check(ghost)]
295        #[ensures(match result {
296            Some((first, tail)) => {
297                *first == self[0] && ^first == (^self)[0] &&
298                (*self)@.len() > 0 && (^self)@.len() > 0 &&
299                (*tail)@ == (*self)@.tail() &&
300                (^tail)@ == (^self)@.tail()
301            }
302            None => self@.len() == 0 && ^self == *self && self@ == Seq::empty()
303        })]
304        fn split_first_mut(&mut self) -> Option<(&mut T, &mut [T])>;
305
306        #[check(ghost)]
307        #[ensures(match result {
308            Some(r) => {
309                *r == (**self)[0] && ^r == (^*self)[0] &&
310                (**self)@.len() > 0 && (^*self)@.len() > 0 &&
311                (*^self)@ == (**self)@.tail() && (^^self)@ == (^*self)@.tail()
312            }
313            None => (*^self)@ == Seq::empty() && (^*self)@ == Seq::empty() &&
314                    (**self)@ == Seq::empty() && (^^self)@ == Seq::empty()
315        })]
316        fn split_off_first_mut<'a>(self_: &mut &'a mut [T]) -> Option<&'a mut T>;
317
318        #[check(ghost)]
319        #[ensures(result@ == self)]
320        fn iter(&self) -> Iter<'_, T>;
321
322        #[check(ghost)]
323        #[ensures(result@ == self)]
324        fn iter_mut(&mut self) -> IterMut<'_, T>;
325
326        #[check(ghost)]
327        #[ensures(result == None ==> self@.len() == 0)]
328        #[ensures(forall<x> result == Some(x) ==> self[self@.len() - 1] == *x)]
329        fn last(&self) -> Option<&T>;
330
331        #[check(ghost)]
332        #[ensures(result == None ==> self@.len() == 0)]
333        #[ensures(forall<x> result == Some(x) ==> self[0] == *x)]
334        fn first(&self) -> Option<&T>;
335
336
337        #[requires(self.deep_model().sorted())]
338        #[ensures(forall<i:usize> result == Ok(i) ==> i@ < self@.len() && (*self).deep_model()[i@] == x.deep_model())]
339        #[ensures(forall<i:usize> result == Err(i) ==> i@ <= self@.len() &&
340            forall<j> 0 <= j && j < self@.len() ==> self.deep_model()[j] != x.deep_model())]
341        #[ensures(forall<i:usize> result == Err(i) ==>
342            forall<j:usize> j < i ==> self.deep_model()[j@] < x.deep_model())]
343        #[ensures(forall<i:usize> result == Err(i) ==>
344            forall<j:usize> i <= j && j@ < self@.len() ==> x.deep_model() < self.deep_model()[j@])]
345        fn binary_search(&self, x: &T) -> Result<usize, usize>
346            where T: Ord + DeepModel,  T::DeepModelTy: OrdLogic,;
347
348        #[check(terminates)] // can OOM (?)
349        #[ensures(result@ == self_@)]
350        fn into_vec<A: Allocator>(self_: Box<Self, A>) -> Vec<T, A>;
351
352        #[requires(ix.in_bounds(self@))]
353        #[ensures(ix.has_value(self@, *result))]
354        unsafe fn get_unchecked<I>(&self, ix: I) -> &<I as ::std::slice::SliceIndex<[T]>>::Output
355            where I: SliceIndex<[T]>;
356
357        #[requires(ix.in_bounds(self@))]
358        #[ensures(ix.has_value(self@, *result))]
359        #[ensures(ix.has_value((^self)@, ^result))]
360        #[ensures(ix.resolve_elswhere(self@, (^self)@))]
361        #[ensures((^self)@.len() == self@.len())]
362        unsafe fn get_unchecked_mut<I>(&mut self, ix: I) -> &mut <I as ::std::slice::SliceIndex<[T]>>::Output
363            where I: SliceIndex<[T]>;
364    }
365
366    impl<T, I> IndexMut<I> for [T]
367        where I: SliceIndex<[T]> {
368        #[check(ghost)]
369        #[requires(ix.in_bounds(self@))]
370        #[ensures(ix.has_value(self@, *result))]
371        #[ensures(ix.has_value((&^self)@, ^result))]
372        #[ensures(ix.resolve_elswhere(self@, (&^self)@))]
373        #[ensures((&^self)@.len() == self@.len())]
374        fn index_mut(&mut self, ix: I) -> &mut <[T] as Index<I>>::Output;
375    }
376
377    impl<T, I> Index<I> for [T]
378        where I: SliceIndex<[T]> {
379        #[check(ghost)]
380        #[requires(ix.in_bounds(self@))]
381        #[ensures(ix.has_value(self@, *result))]
382        fn index(&self, ix: I) -> &<[T] as Index<I>>::Output;
383    }
384
385    impl<'a, T> IntoIterator for &'a [T] {
386        #[check(ghost)]
387        #[ensures(self == result@)]
388        fn into_iter(self) -> Iter<'a, T>;
389    }
390
391    impl<'a, T> IntoIterator for &'a mut [T] {
392        #[check(ghost)]
393        #[ensures(self == result@)]
394        fn into_iter(self) -> IterMut<'a, T>;
395    }
396
397    impl<'a, T> Default for &'a mut [T] {
398        #[check(ghost)]
399        #[ensures((*result)@ == Seq::empty())]
400        #[ensures((^result)@ == Seq::empty())]
401        fn default() -> &'a mut [T];
402    }
403
404    impl<'a, T> Default for &'a [T] {
405        #[check(ghost)]
406        #[ensures(result@ == Seq::empty())]
407        fn default() -> &'a [T];
408    }
409
410    impl<T: Clone, A: Allocator + Clone> Clone for Box<[T], A> {
411        #[ensures(forall<i> 0 <= i && i < self@.len() ==>
412            T::clone.postcondition((&self@[i],), result@[i]))]
413        fn clone(&self) -> Box<[T], A>;
414    }
415
416    mod std {
417        mod slice {
418            #[check(ghost)]
419            #[ensures(result@.len() == 1)]
420            #[ensures(result@[0] == *s)]
421            fn from_ref<T>(s: &T) -> &[T];
422
423            #[check(ghost)]
424            #[ensures(result@.len() == 1)]
425            #[ensures(result@[0] == *s)]
426            #[ensures((^result)@.len() == 1)]
427            #[ensures((^result)@[0] == ^s)]
428            fn from_mut<T>(s: &mut T) -> &mut [T];
429        }
430    }
431}
432
433impl<'a, T> View for Iter<'a, T> {
434    type ViewTy = &'a [T];
435
436    #[logic(opaque)]
437    fn view(self) -> Self::ViewTy {
438        dead
439    }
440}
441
442impl<'a, T> Iterator for Iter<'a, T> {
443    #[logic(open, prophetic)]
444    fn completed(&mut self) -> bool {
445        pearlite! { self.resolve() && (*self@)@ == Seq::empty() }
446    }
447
448    #[logic(open)]
449    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
450        pearlite! {
451            self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
452        }
453    }
454
455    #[logic(open, law)]
456    #[ensures(self.produces(Seq::empty(), self))]
457    fn produces_refl(self) {}
458
459    #[logic(open, law)]
460    #[requires(a.produces(ab, b))]
461    #[requires(b.produces(bc, c))]
462    #[ensures(a.produces(ab.concat(bc), c))]
463    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
464}
465
466impl<'a, T> View for IterMut<'a, T> {
467    type ViewTy = &'a mut [T];
468
469    #[trusted]
470    #[logic(opaque)]
471    #[ensures((^result)@.len() == (*result)@.len())]
472    fn view(self) -> Self::ViewTy {
473        dead
474    }
475}
476
477impl<'a, T> Resolve for IterMut<'a, T> {
478    #[logic(open, prophetic, inline)]
479    fn resolve(self) -> bool {
480        pearlite! { *self@ == ^self@ }
481    }
482
483    #[trusted]
484    #[logic(prophetic)]
485    #[requires(structural_resolve(self))]
486    #[ensures(self.resolve())]
487    fn resolve_coherence(self) {}
488}
489
490impl<'a, T> Iterator for IterMut<'a, T> {
491    #[logic(open, prophetic)]
492    fn completed(&mut self) -> bool {
493        pearlite! { self.resolve() && (*self@)@ == Seq::empty() }
494    }
495
496    #[logic(open)]
497    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
498        pearlite! {
499            self@.to_mut_seq() == visited.concat(tl@.to_mut_seq())
500        }
501    }
502
503    #[logic(open, law)]
504    #[ensures(self.produces(Seq::empty(), self))]
505    fn produces_refl(self) {}
506
507    #[logic(open, law)]
508    #[requires(a.produces(ab, b))]
509    #[requires(b.produces(bc, c))]
510    #[ensures(a.produces(ab.concat(bc), c))]
511    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {}
512}
creusot_contracts/std/slice.rs

creusot_contracts/std/
slice.rs
