creusot_std/std/
slice.rs

1#[cfg(creusot)]
2use crate::resolve::structural_resolve;
3use crate::{
4    ghost::perm::Perm, invariant::*, logic::ops::IndexLogic, prelude::*,
5    std::iter::ExactSizeIteratorSpec,
6};
7#[cfg(creusot)]
8use core::ops::{Index, IndexMut};
9use core::{
10    ops::{Bound, Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive},
11    slice::*,
12};
13#[cfg(all(creusot, feature = "std"))]
14use std::alloc::Allocator;
15
16impl<T> Invariant for [T] {
17    #[logic(open, prophetic)]
18    #[creusot::trusted_trivial_if_param_trivial]
19    fn invariant(self) -> bool {
20        pearlite! { inv(self@) }
21    }
22}
23
24impl<T> Resolve for [T] {
25    #[logic(open, prophetic, inline)]
26    #[creusot::trusted_trivial_if_param_trivial]
27    fn resolve(self) -> bool {
28        pearlite! { forall<i> 0 <= i && i < self@.len() ==> resolve(self[i]) }
29    }
30
31    #[trusted]
32    #[logic(prophetic)]
33    #[requires(structural_resolve(self))]
34    #[ensures(self.resolve())]
35    fn resolve_coherence(self) {}
36}
37
38impl<T> View for [T] {
39    type ViewTy = Seq<T>;
40
41    #[logic]
42    #[cfg_attr(target_pointer_width = "16", builtin("creusot.slice.Slice16$BW$.view"))]
43    #[cfg_attr(target_pointer_width = "32", builtin("creusot.slice.Slice32$BW$.view"))]
44    #[cfg_attr(target_pointer_width = "64", builtin("creusot.slice.Slice64$BW$.view"))]
45    fn view(self) -> Self::ViewTy {
46        dead
47    }
48}
49
50impl<T: DeepModel> DeepModel for [T] {
51    type DeepModelTy = Seq<T::DeepModelTy>;
52
53    #[trusted]
54    #[logic(opaque)]
55    #[ensures((&self)@.len() == result.len())]
56    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == (&self)[i].deep_model())]
57    fn deep_model(self) -> Self::DeepModelTy {
58        dead
59    }
60}
61
62impl<T> IndexLogic<Int> for [T] {
63    type Item = T;
64
65    #[logic(open, inline)]
66    fn index_logic(self, ix: Int) -> Self::Item {
67        pearlite! { self@[ix] }
68    }
69}
70
71impl<T> IndexLogic<usize> for [T] {
72    type Item = T;
73
74    #[logic(open, inline)]
75    fn index_logic(self, ix: usize) -> Self::Item {
76        pearlite! { self@[ix@] }
77    }
78}
79
80pub trait SliceExt<T> {
81    #[logic]
82    fn to_mut_seq(&mut self) -> Seq<&mut T>;
83
84    #[logic]
85    fn to_ref_seq(&self) -> Seq<&T>;
86
87    #[check(terminates)]
88    fn as_ptr_perm(&self) -> (*const T, Ghost<&Perm<*const [T]>>);
89
90    #[check(terminates)]
91    fn as_mut_ptr_perm<'a>(
92        &'a mut self,
93    ) -> (*mut T, Ghost<Guarded<&'a mut Perm<*const [T]>, *const [T]>>);
94}
95
96impl<T> SliceExt<T> for [T] {
97    #[trusted]
98    #[logic(opaque)]
99    #[ensures(result.len() == self@.len())]
100    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == &mut self[i])]
101    // TODO: replace with a map function applied on a sequence
102    fn to_mut_seq(&mut self) -> Seq<&mut T> {
103        dead
104    }
105
106    #[trusted]
107    #[logic(opaque)]
108    #[ensures(result.len() == self@.len())]
109    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == &self[i])]
110    fn to_ref_seq(&self) -> Seq<&T> {
111        dead
112    }
113
114    /// Convert `&[T]` to `*const T` and a shared ownership token.
115    #[check(terminates)]
116    #[ensures(result.0 == *result.1.ward() as *const T)]
117    #[ensures(self == result.1.val_unsized())]
118    #[erasure(Self::as_ptr)]
119    fn as_ptr_perm(&self) -> (*const T, Ghost<&Perm<*const [T]>>) {
120        let (ptr, own) = Perm::from_ref(self);
121        (ptr as *const T, own)
122    }
123
124    /// Convert `&mut [T]` to `*mut T` and a mutable ownership token.
125    #[check(terminates)]
126    #[ensures(result.1.guard().thin() == result.0 as *const T)]
127    #[ensures(*self == *result.1.inner.val_unsized())]
128    #[ensures(^self == *(^result.1.inner).val_unsized())]
129    #[erasure(Self::as_mut_ptr)]
130    fn as_mut_ptr_perm<'a>(
131        &'a mut self,
132    ) -> (*mut T, Ghost<Guarded<&'a mut Perm<*const [T]>, *const [T]>>) {
133        let (ptr, own) = Perm::from_mut(self);
134        (ptr as *mut T, own)
135    }
136}
137
138pub trait SliceIndexSpec<T: ?Sized>: SliceIndex<T>
139where
140    T: View,
141{
142    #[logic]
143    fn in_bounds(self, seq: T::ViewTy) -> bool;
144
145    #[logic]
146    fn has_value(self, seq: T::ViewTy, out: Self::Output) -> bool;
147
148    #[logic]
149    fn resolve_elswhere(self, old: T::ViewTy, fin: T::ViewTy) -> bool;
150}
151
152impl<T> SliceIndexSpec<[T]> for usize {
153    #[logic(open, inline)]
154    fn in_bounds(self, seq: Seq<T>) -> bool {
155        pearlite! { self@ < seq.len() }
156    }
157
158    #[logic(open, inline)]
159    fn has_value(self, seq: Seq<T>, out: T) -> bool {
160        pearlite! { seq[self@] == out }
161    }
162
163    #[logic(open, inline)]
164    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
165        pearlite! { forall<i> 0 <= i && i != self@ && i < old.len() ==> old[i] == fin[i] }
166    }
167}
168
169impl<T> SliceIndexSpec<[T]> for Range<usize> {
170    #[logic(open)]
171    fn in_bounds(self, seq: Seq<T>) -> bool {
172        pearlite! { self.start@ <= self.end@ && self.end@ <= seq.len() }
173    }
174
175    #[logic(open)]
176    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
177        pearlite! { seq.subsequence(self.start@, self.end@) == out@ }
178    }
179
180    #[logic(open)]
181    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
182        pearlite! {
183            forall<i> 0 <= i && (i < self.start@ || self.end@ <= i) && i < old.len()
184            ==> old[i] == fin[i]
185        }
186    }
187}
188
189impl<T> SliceIndexSpec<[T]> for RangeInclusive<usize> {
190    #[trusted]
191    #[logic(opaque)]
192    #[ensures(self.end_log()@ < seq.len() && self.start_log()@ <= self.end_log()@+1 ==> result)]
193    #[ensures(self.end_log()@ >= seq.len() ==> !result)]
194    fn in_bounds(self, seq: Seq<T>) -> bool {
195        dead
196    }
197
198    #[logic(open)]
199    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
200        pearlite! {
201            if self.is_empty_log() { out@ == Seq::empty() }
202            else { seq.subsequence(self.start_log()@, self.end_log()@ + 1) == out@ }
203        }
204    }
205
206    #[logic(open)]
207    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
208        pearlite! {
209            forall<i> 0 <= i
210                && (i < self.start_log()@ || self.end_log()@ < i || self.is_empty_log())
211                && i < old.len()
212                ==> old[i] == fin[i]
213        }
214    }
215}
216
217impl<T> SliceIndexSpec<[T]> for RangeTo<usize> {
218    #[logic(open)]
219    fn in_bounds(self, seq: Seq<T>) -> bool {
220        pearlite! { self.end@ <= seq.len() }
221    }
222
223    #[logic(open)]
224    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
225        pearlite! { seq.subsequence(0, self.end@) == out@ }
226    }
227
228    #[logic(open)]
229    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
230        pearlite! { forall<i> self.end@ <= i && i < old.len() ==> old[i] == fin[i] }
231    }
232}
233
234impl<T> SliceIndexSpec<[T]> for RangeFrom<usize> {
235    #[logic(open)]
236    fn in_bounds(self, seq: Seq<T>) -> bool {
237        pearlite! { self.start@ <= seq.len() }
238    }
239
240    #[logic(open)]
241    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
242        pearlite! { seq.subsequence(self.start@, seq.len()) == out@ }
243    }
244
245    #[logic(open)]
246    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
247        pearlite! {
248            forall<i> 0 <= i && i < self.start@ && i < old.len() ==> old[i] == fin[i]
249        }
250    }
251}
252
253impl<T> SliceIndexSpec<[T]> for RangeFull {
254    #[logic(open)]
255    fn in_bounds(self, _seq: Seq<T>) -> bool {
256        pearlite! { true }
257    }
258
259    #[logic(open)]
260    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
261        pearlite! { seq == out@ }
262    }
263
264    #[logic(open)]
265    fn resolve_elswhere(self, _old: Seq<T>, _fin: Seq<T>) -> bool {
266        pearlite! { true }
267    }
268}
269
270impl<T> SliceIndexSpec<[T]> for RangeToInclusive<usize> {
271    #[logic(open)]
272    fn in_bounds(self, seq: Seq<T>) -> bool {
273        pearlite! { self.end@ < seq.len() }
274    }
275
276    #[logic(open)]
277    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
278        pearlite! { seq.subsequence(0, self.end@ + 1) == out@ }
279    }
280
281    #[logic(open)]
282    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
283        pearlite! { forall<i> self.end@ < i && i < old.len() ==> old[i] == fin[i] }
284    }
285}
286
287#[logic(open, inline)]
288pub fn to_logic_range((lo, hi): (Bound<usize>, Bound<usize>), len: Int) -> Range<Int> {
289    pearlite! {
290        let lo = match lo {
291            Bound::Included(i) => i@,
292            Bound::Excluded(i) => i@ + 1,
293            Bound::Unbounded => 0
294        };
295        let hi = match hi {
296            Bound::Included(i) => i@ + 1,
297            Bound::Excluded(i) => i@,
298            Bound::Unbounded => len
299        };
300        lo..hi
301    }
302}
303
304impl<T> SliceIndexSpec<[T]> for (Bound<usize>, Bound<usize>) {
305    #[logic(open)]
306    fn in_bounds(self, seq: Seq<T>) -> bool {
307        let range = to_logic_range(self, seq.len());
308        pearlite! { range.start <= range.end && range.end <= seq.len() }
309    }
310
311    #[logic(open)]
312    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
313        let range = to_logic_range(self, seq.len());
314        pearlite! { seq.subsequence(range.start, range.end) == out@ }
315    }
316
317    #[logic(open)]
318    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
319        let range = to_logic_range(self, old.len());
320        pearlite! {
321            forall<i> 0 <= i && (i < range.start || range.end <= i) && i < old.len()
322            ==> old[i] == fin[i]
323        }
324    }
325}
326
327extern_spec! {
328    impl<T> [T] {
329        #[check(ghost)]
330        #[requires(self@.len() == src@.len())]
331        #[ensures((^self)@ == src@)]
332        fn copy_from_slice(&mut self, src: &[T]) where T: Copy;
333
334        #[check(ghost)]
335        #[ensures(self@.len() == result@)]
336        fn len(&self) -> usize;
337
338        #[check(ghost)]
339        #[ensures(result == (self@.len() == 0))]
340        fn is_empty(&self) -> bool;
341
342        #[check(ghost)]
343        #[requires(i@ < self@.len())]
344        #[requires(j@ < self@.len())]
345        #[ensures((^self)@.exchange(self@, i@, j@))]
346        fn swap(&mut self, i: usize, j: usize);
347
348        #[check(ghost)]
349        #[ensures(ix.in_bounds(self@) ==> exists<r> result == Some(r) && ix.has_value(self@, *r))]
350        #[ensures(ix.in_bounds(self@) || result == None)]
351        fn get<I: SliceIndexSpec<[T]>>(&self, ix: I) -> Option<&<I as SliceIndex<[T]>>::Output>;
352
353        #[check(ghost)]
354        #[ensures((^self)@.len() == self@.len())]
355        #[ensures(ix.in_bounds(self@) ==> exists<r>
356                    result == Some(r) &&
357                    ix.has_value(self@, *r) &&
358                    ix.has_value((^self)@, ^r) &&
359                    ix.resolve_elswhere(self@, (^self)@))]
360        #[ensures(ix.in_bounds(self@) || result == None)]
361        fn get_mut<I: SliceIndexSpec<[T]>>(&mut self, ix: I)
362            -> Option<&mut <I as SliceIndex<[T]>>::Output>;
363
364        #[check(ghost)]
365        #[requires(mid@ <= self@.len())]
366        #[ensures(result.0@ == self@[..mid@])]
367        #[ensures(result.1@ == self@[mid@..])]
368        fn split_at(&self, mid: usize) -> (&[T], &[T]);
369
370        #[check(ghost)]
371        #[ensures(match result {
372            Some((l, r)) => mid@ <= self@.len() && l@ == self@[..mid@] && r@ == self@[mid@..],
373            None => mid@ > self@.len()
374        })]
375        fn split_at_checked(&self, mid: usize) -> Option<(&[T], &[T])> {
376            if mid > self.len() {
377                None
378            } else {
379                Some(self.split_at(mid))
380            }
381        }
382
383        #[check(ghost)]
384        #[requires(mid@ <= self@.len())]
385        #[ensures((^self)@.len() == self@.len())]
386        #[ensures(result.0@ == self@[..mid@])]
387        #[ensures(result.1@ == self@[mid@..])]
388        #[ensures((^result.0)@ == (^self)@[..mid@])]
389        #[ensures((^result.1)@ == (^self)@[mid@..])]
390        fn split_at_mut(&mut self, mid: usize) -> (&mut [T], &mut [T]);
391
392        #[check(ghost)]
393        #[ensures((^self)@.len() == self@.len())]
394        #[ensures(match result {
395            Some((l, r)) => {
396                mid@ <= self@.len() &&
397                l@ == self@[..mid@] && r@ == self@[mid@..] &&
398                (^l)@ == (^self)@[..mid@] && (^r)@ == (^self)@[mid@..]
399            }
400            None => mid@ > self@.len() && *self == ^self
401        })]
402        fn split_at_mut_checked(&mut self, mid: usize) -> Option<(&mut [T], &mut [T])> {
403            if mid > self.len() {
404                None
405            } else {
406                Some(self.split_at_mut(mid))
407            }
408        }
409
410        #[check(ghost)]
411        #[ensures(match result {
412            Some((l, r)) => 1 <= self@.len() && l == &self[0] && r@ == self@[1..],
413            None => self@ == Seq::empty()
414        })]
415        fn split_first(&self) -> Option<(&T, &[T])> {
416            let (l, r) = self.split_at_checked(1)?;
417            Some((&l[0], r))
418        }
419
420        #[check(ghost)]
421        #[ensures((^self)@.len() == self@.len())]
422        #[ensures(match result {
423            Some((l, r)) => {
424                1 <= self@.len() &&
425                *l == self[0] && ^l == (^self)[0] && r@ == self@[1..] && (^r)@ == (^self)@[1..]
426            }
427            None => self@ == Seq::empty() && *self == ^self
428        })]
429        fn split_first_mut(&mut self) -> Option<(&mut T, &mut [T])> {
430            let (l, r) = self.split_at_mut_checked(1)?;
431            Some((&mut l[0], r))
432        }
433
434        #[check(ghost)]
435        #[ensures(match result {
436            Some((l, r)) => 1 <= self@.len() && l == &self[self@.len() - 1] && r@ == self@.init(),
437            None => self@ == Seq::empty()
438        })]
439        fn split_last(&self) -> Option<(&T, &[T])> {
440            if self.len() == 0 {
441                return None
442            }
443            let (l, r) = self.split_at(self.len() - 1);
444            Some((&r[0], l))
445        }
446
447        #[check(ghost)]
448        #[ensures((^self)@.len() == self@.len())]
449        #[ensures(match result {
450            Some((l, r)) => {
451                1 <= self@.len() &&
452                *l == self[self@.len() - 1] && ^l == (^self)[self@.len() - 1] &&
453                r@ == self@.init() && (^r)@ == (^self)@.init()
454            }
455            None => self@ == Seq::empty() && *self == ^self
456        })]
457        fn split_last_mut(&mut self) -> Option<(&mut T, &mut [T])> {
458            if self.len() == 0 {
459                return None
460            }
461            let (l, r) = self.split_at_mut(self.len() - 1);
462            Some((&mut r[0], l))
463        }
464
465
466        #[check(ghost)]
467        #[ensures((^*self)@.len() == (**self)@.len())]
468        #[ensures((^^self)@.len() == (*^self)@.len())]
469        #[ensures(match result {
470            Some(r) => {
471                (**self)@.len() > 0 &&
472                r == &mut (**self)[0] &&
473                (^self).to_mut_seq() == (*self).to_mut_seq().tail()
474            }
475            None => resolve(self) && (^*self)@ == Seq::empty() && (**self)@ == Seq::empty()
476        })]
477        fn split_off_first_mut<'a>(self: &mut &'a mut [T]) -> Option<&'a mut T>;
478
479        #[check(ghost)]
480        #[ensures((^*self)@.len() == (**self)@.len())]
481        #[ensures((^^self)@.len() == (*^self)@.len())]
482        #[ensures(match result {
483            Some(r) => {
484                (**self)@.len() > 0 &&
485                r == &mut (**self)[(**self)@.len()-1] &&
486                (^self).to_mut_seq() == (*self).to_mut_seq().init()
487            }
488            None => resolve(self) && (^*self)@ == Seq::empty() && (**self)@ == Seq::empty()
489        })]
490        fn split_off_last_mut<'a>(self: &mut &'a mut [T]) -> Option<&'a mut T>;
491
492        #[check(ghost)]
493        #[ensures(result@ == self)]
494        fn iter(&self) -> Iter<'_, T>;
495
496        #[check(ghost)]
497        #[ensures(result@ == self)]
498        fn iter_mut(&mut self) -> IterMut<'_, T>;
499
500        #[check(ghost)]
501        #[ensures((result == None) == (self@.len() == 0))]
502        #[ensures(forall<x> result == Some(x) ==> self[self@.len() - 1] == *x)]
503        fn last(&self) -> Option<&T>;
504
505        #[check(ghost)]
506        #[ensures((result == None) == (self@.len() == 0))]
507        #[ensures(forall<x> result == Some(x) ==> self[self@.len() - 1] == *x)]
508        #[ensures(forall<x> result == Some(x) ==> (^self)[self@.len() - 1] == ^x)]
509        #[ensures((*self)@.len() == (^self)@.len())]
510        #[ensures(forall<i> 0 <= i && i < (*self)@.len() - 1 ==> (*self)[i] == (^self)[i])]
511        fn last_mut(&mut self) -> Option<&mut T>;
512
513        #[check(ghost)]
514        #[ensures((result == None) == (self@.len() == 0))]
515        #[ensures(forall<x> result == Some(x) ==> self[0] == *x)]
516        fn first(&self) -> Option<&T>;
517
518        #[check(ghost)]
519        #[ensures((result == None) == (self@.len() == 0))]
520        #[ensures(forall<x> result == Some(x) ==> self[0] == *x)]
521        #[ensures(forall<x> result == Some(x) ==> (^self)[0] == ^x)]
522        #[ensures((*self)@.len() == (^self)@.len())]
523        #[ensures(forall<i> 1 <= i && i < (*self)@.len() ==> (*self)[i] == (^self)[i])]
524        fn first_mut(&mut self) -> Option<&mut T>;
525
526        #[requires(self.deep_model().sorted())]
527        #[ensures(forall<i:usize> result == Ok(i) ==>
528            i@ < self@.len() && (*self).deep_model()[i@] == x.deep_model())]
529        #[ensures(forall<i:usize> result == Err(i) ==> i@ <= self@.len() &&
530            forall<j> 0 <= j && j < self@.len() ==> self.deep_model()[j] != x.deep_model())]
531        #[ensures(forall<i:usize> result == Err(i) ==>
532            forall<j:usize> j < i ==> self.deep_model()[j@] < x.deep_model())]
533        #[ensures(forall<i:usize> result == Err(i) ==>
534            forall<j:usize> i <= j && j@ < self@.len() ==> x.deep_model() < self.deep_model()[j@])]
535        fn binary_search(&self, x: &T) -> Result<usize, usize>
536            where T: Ord + DeepModel,  T::DeepModelTy: OrdLogic,;
537
538        #[check(ghost)]
539        #[requires(ix.in_bounds(self@))]
540        #[ensures(ix.has_value(self@, *result))]
541        unsafe fn get_unchecked<I: SliceIndexSpec<[T]>>(&self, ix: I)
542            -> &<I as SliceIndex<[T]>>::Output;
543
544        #[check(ghost)]
545        #[requires(ix.in_bounds(self@))]
546        #[ensures(ix.has_value(self@, *result))]
547        #[ensures(ix.has_value((^self)@, ^result))]
548        #[ensures(ix.resolve_elswhere(self@, (^self)@))]
549        #[ensures((^self)@.len() == self@.len())]
550        unsafe fn get_unchecked_mut<I: SliceIndexSpec<[T]>>(&mut self, ix: I)
551            -> &mut <I as SliceIndex<[T]>>::Output;
552
553        // Calling this is safe but you should use `as_ptr_perm` instead to prove things.
554        #[check(ghost)]
555        fn as_ptr(&self) -> *const T;
556
557        // Calling this is safe but you should use `as_mut_ptr_perm` instead to prove things.
558        #[check(ghost)]
559        fn as_mut_ptr(&mut self) -> *mut T;
560    }
561
562    impl<T, I: SliceIndexSpec<[T]>> IndexMut<I> for [T] {
563        #[check(ghost)]
564        #[requires(ix.in_bounds(self@))]
565        #[ensures(ix.has_value(self@, *result))]
566        #[ensures(ix.has_value((&^self)@, ^result))]
567        #[ensures(ix.resolve_elswhere(self@, (&^self)@))]
568        #[ensures((&^self)@.len() == self@.len())]
569        fn index_mut(&mut self, ix: I) -> &mut <[T] as Index<I>>::Output;
570    }
571
572    impl<T, I: SliceIndexSpec<[T]>> Index<I> for [T] {
573        #[check(ghost)]
574        #[requires(ix.in_bounds(self@))]
575        #[ensures(ix.has_value(self@, *result))]
576        fn index(&self, ix: I) -> &<[T] as Index<I>>::Output;
577    }
578
579    impl<'a, T> IntoIterator for &'a [T] {
580        #[check(ghost)]
581        #[ensures(self == result@)]
582        fn into_iter(self) -> Iter<'a, T>;
583    }
584
585    impl<'a, T> IntoIterator for &'a mut [T] {
586        #[check(ghost)]
587        #[ensures(self == result@)]
588        fn into_iter(self) -> IterMut<'a, T>;
589    }
590
591    impl<'a, T> Default for &'a mut [T] {
592        #[check(ghost)]
593        #[ensures((*result)@ == Seq::empty())]
594        #[ensures((^result)@ == Seq::empty())]
595        fn default() -> &'a mut [T];
596    }
597
598    impl<'a, T> Default for &'a [T] {
599        #[check(ghost)]
600        #[ensures(result@ == Seq::empty())]
601        fn default() -> &'a [T];
602    }
603
604    mod core {
605        mod slice {
606            #[check(ghost)]
607            #[ensures(result@.len() == 1)]
608            #[ensures(result@[0] == *s)]
609            fn from_ref<T>(s: &T) -> &[T];
610
611            #[check(ghost)]
612            #[ensures(result@.len() == 1)]
613            #[ensures(result@[0] == *s)]
614            #[ensures((^result)@.len() == 1)]
615            #[ensures((^result)@[0] == ^s)]
616            fn from_mut<T>(s: &mut T) -> &mut [T];
617        }
618    }
619}
620
621#[cfg(feature = "std")]
622extern_spec! {
623    impl<T> [T] {
624        #[check(ghost)]
625        #[ensures(result@ == self@)]
626        fn into_vec<A: Allocator>(self: Box<Self, A>) -> Vec<T, A>;
627
628        // FIXME: inherit ghost/terminates from clone
629        #[ensures(result@.len() == self@.len())]
630        #[ensures(forall<i> 0 <= i && i < self@.len() ==> <T as Clone>::clone.postcondition((&self@[i],), result@[i]))]
631        fn to_vec(&self) -> Vec<T> where T: Clone;
632    }
633
634    impl<T: Clone, A: Allocator + Clone> Clone for Box<[T], A> {
635        #[ensures(forall<i> 0 <= i && i < self@.len() ==>
636            T::clone.postcondition((&self@[i],), result@[i]))]
637        fn clone(&self) -> Box<[T], A>;
638    }
639}
640
641impl<'a, T> View for Iter<'a, T> {
642    type ViewTy = &'a [T];
643
644    #[logic(opaque)]
645    fn view(self) -> Self::ViewTy {
646        dead
647    }
648}
649
650impl<'a, T> IteratorSpec for Iter<'a, T> {
651    #[logic(open, prophetic)]
652    fn completed(&mut self) -> bool {
653        pearlite! { resolve(self) && (*self@)@ == Seq::empty() }
654    }
655
656    #[logic(open)]
657    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
658        pearlite! {
659            self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
660        }
661    }
662
663    #[logic(law)]
664    #[ensures(self.produces(Seq::empty(), self))]
665    fn produces_refl(self) {
666        let _ = Seq::<Self::Item>::concat_empty;
667    }
668
669    #[logic(law)]
670    #[requires(a.produces(ab, b))]
671    #[requires(b.produces(bc, c))]
672    #[ensures(a.produces(ab.concat(bc), c))]
673    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
674        let _ = Seq::<Self::Item>::concat_assoc;
675    }
676}
677
678extern_spec! {
679    impl<'a, T> Iterator for Iter<'a, T> {
680        #[ensures(result.0@ == self@@.len())]
681        #[ensures(result.1 == Some(result.0))]
682        fn size_hint(&self) -> (usize, Option<usize>);
683    }
684}
685
686impl<'a, T> ExactSizeIteratorSpec for Iter<'a, T> {
687    #[logic(law)]
688    #[requires(Self::size_hint.postcondition((self,), r))]
689    #[ensures(r.1 == Some(r.0))]
690    #[allow(unused_variables)]
691    fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
692}
693
694impl<'a, T> DoubleEndedIteratorSpec for Iter<'a, T> {
695    #[logic(open)]
696    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
697        pearlite! {
698          self@.to_ref_seq() == o@.to_ref_seq().concat(visited.reverse())
699        }
700    }
701
702    #[logic(open, prophetic)]
703    fn completed_back(&mut self) -> bool {
704        self.completed()
705    }
706
707    #[logic(law)]
708    #[ensures(self.produces_back(Seq::empty(), self))]
709    fn produces_back_refl(self) {
710        let _ = Seq::<Self::Item>::reverse_empty();
711        let _ = Seq::<Self::Item>::concat_empty;
712    }
713
714    #[logic(law)]
715    #[requires(a.produces_back(ab, b))]
716    #[requires(b.produces_back(bc, c))]
717    #[ensures(a.produces_back(ab.concat(bc), c))]
718    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
719        let _ = ab.reverse_concat(bc);
720        let _ = Seq::<Self::Item>::concat_assoc;
721    }
722
723    #[logic(law)]
724    #[requires(Self::size_hint.postcondition((self,), r))]
725    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
726        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
727    #[ensures(match r.1 {
728        Some(r) => {
729            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
730        }
731        None => true
732    })]
733    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
734}
735
736impl<'a, T> View for IterMut<'a, T> {
737    type ViewTy = &'a mut [T];
738
739    #[trusted]
740    #[logic(opaque)]
741    #[ensures((^result)@.len() == (*result)@.len())]
742    fn view(self) -> Self::ViewTy {
743        dead
744    }
745}
746
747impl<'a, T> Resolve for IterMut<'a, T> {
748    #[logic(open, prophetic, inline)]
749    fn resolve(self) -> bool {
750        pearlite! { *self@ == ^self@ }
751    }
752
753    #[trusted]
754    #[logic(prophetic)]
755    #[requires(structural_resolve(self))]
756    #[ensures(self.resolve())]
757    fn resolve_coherence(self) {}
758}
759
760impl<'a, T> IteratorSpec for IterMut<'a, T> {
761    #[logic(open, prophetic)]
762    fn completed(&mut self) -> bool {
763        pearlite! { resolve(self) && (*self@)@ == Seq::empty() }
764    }
765
766    #[logic(open)]
767    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
768        pearlite! {
769            self@.to_mut_seq() == visited.concat(tl@.to_mut_seq())
770        }
771    }
772
773    #[logic(law)]
774    #[ensures(self.produces(Seq::empty(), self))]
775    fn produces_refl(self) {
776        let _ = Seq::<Self::Item>::concat_empty;
777    }
778
779    #[logic(law)]
780    #[requires(a.produces(ab, b))]
781    #[requires(b.produces(bc, c))]
782    #[ensures(a.produces(ab.concat(bc), c))]
783    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
784        let _ = Seq::<Self::Item>::concat_assoc;
785    }
786}
787
788extern_spec! {
789    impl<'a, T> Iterator for IterMut<'a, T> {
790        #[ensures(result.0@ == self@@.len())]
791        #[ensures(result.1 == Some(result.0))]
792        fn size_hint(&self) -> (usize, Option<usize>);
793    }
794}
795
796impl<'a, T> ExactSizeIteratorSpec for IterMut<'a, T> {
797    #[logic(law)]
798    #[requires(Self::size_hint.postcondition((self,), r))]
799    #[ensures(r.1 == Some(r.0))]
800    #[allow(unused_variables)]
801    fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
802}
803
804impl<'a, T> DoubleEndedIteratorSpec for IterMut<'a, T> {
805    #[logic(open)]
806    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
807        pearlite! {
808            self@.to_mut_seq() == o@.to_mut_seq().concat(visited.reverse())
809        }
810    }
811
812    #[logic(open, prophetic)]
813    fn completed_back(&mut self) -> bool {
814        self.completed()
815    }
816
817    #[logic(law)]
818    #[ensures(self.produces_back(Seq::empty(), self))]
819    fn produces_back_refl(self) {
820        let _ = Seq::<Self::Item>::reverse_empty();
821        let _ = Seq::<Self::Item>::concat_empty;
822    }
823
824    #[logic(law)]
825    #[requires(a.produces_back(ab, b))]
826    #[requires(b.produces_back(bc, c))]
827    #[ensures(a.produces_back(ab.concat(bc), c))]
828    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
829        let _ = ab.reverse_concat(bc);
830        let _ = Seq::<Self::Item>::concat_assoc;
831    }
832
833    #[logic(law)]
834    #[requires(Self::size_hint.postcondition((self,), r))]
835    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
836        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
837    #[ensures(match r.1 {
838        Some(r) => {
839            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
840        }
841        None => true
842    })]
843    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
844}
845
846extern_spec! {
847    impl<'a, T> Iterator for Iter<'a, T> {
848        #[check(ghost)]
849        #[ensures(match result {
850            None => self.completed(),
851            Some(v) => (*self).produces(Seq::singleton(v), ^self)
852        })]
853        fn next(&mut self) -> Option<&'a T>;
854    }
855
856    impl<'a, T> Iter<'a, T> {
857        #[check(ghost)]
858        #[ensures(result@ == self@@)]
859        fn as_slice(&self) -> &'a [T];
860    }
861
862    impl<'a, T> ExactSizeIterator for Iter<'a, T> {
863        #[check(ghost)]
864        #[ensures(result@ == self@@.len())]
865        fn len(&self) -> usize;
866    }
867
868    impl<'a, T> Iterator for IterMut<'a, T> {
869        #[check(ghost)]
870        #[ensures(match result {
871            None => self.completed(),
872            Some(v) => (*self).produces(Seq::singleton(v), ^self)
873        })]
874        fn next(&mut self) -> Option<&'a mut T>;
875    }
876
877    impl<'a, T> IterMut<'a, T> {
878        #[check(ghost)]
879        #[ensures(result@ == self@@)]
880        fn as_slice(&self) -> &'a [T];
881    }
882
883    impl<'a, T> ExactSizeIterator for IterMut<'a, T> {
884        #[check(ghost)]
885        #[ensures(result@ == self@@.len())]
886        fn len(&self) -> usize;
887    }
888}
creusot_std/std/slice.rs

creusot_std/std/
slice.rs
