creusot_contracts/std/
slice.rs

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

creusot_contracts/std/
slice.rs
