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.view"))]
43    #[cfg_attr(target_pointer_width = "32", builtin("creusot.slice.Slice32.view"))]
44    #[cfg_attr(target_pointer_width = "64", builtin("creusot.slice.Slice64.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(&mut self) -> (*mut T, Ghost<&mut Perm<*const [T]>>);
92}
93
94impl<T> SliceExt<T> for [T] {
95    #[trusted]
96    #[logic(opaque)]
97    #[ensures(result.len() == self@.len())]
98    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == &mut self[i])]
99    // TODO: replace with a map function applied on a sequence
100    fn to_mut_seq(&mut self) -> Seq<&mut T> {
101        dead
102    }
103
104    #[trusted]
105    #[logic(opaque)]
106    #[ensures(result.len() == self@.len())]
107    #[ensures(forall<i> 0 <= i && i < result.len() ==> result[i] == &self[i])]
108    fn to_ref_seq(&self) -> Seq<&T> {
109        dead
110    }
111
112    /// Convert `&[T]` to `*const T` and a shared ownership token.
113    #[check(terminates)]
114    #[ensures(result.0 == *result.1.ward() as *const T)]
115    #[ensures(self == result.1.val())]
116    #[erasure(Self::as_ptr)]
117    fn as_ptr_perm(&self) -> (*const T, Ghost<&Perm<*const [T]>>) {
118        let (ptr, own) = Perm::from_ref(self);
119        (ptr as *const T, own)
120    }
121
122    /// Convert `&mut [T]` to `*mut T` and a mutable ownership token.
123    #[check(terminates)]
124    #[ensures(result.0 as *const T == *result.1.ward() as *const T)]
125    #[ensures(&*self == result.1.val())]
126    #[ensures(&^self == (^result.1).val())]
127    #[erasure(Self::as_mut_ptr)]
128    fn as_mut_ptr_perm(&mut self) -> (*mut T, Ghost<&mut Perm<*const [T]>>) {
129        let (ptr, own) = Perm::from_mut(self);
130        (ptr as *mut T, own)
131    }
132}
133
134pub trait SliceIndexSpec<T: ?Sized>: SliceIndex<T>
135where
136    T: View,
137{
138    #[logic]
139    fn in_bounds(self, seq: T::ViewTy) -> bool;
140
141    #[logic]
142    fn has_value(self, seq: T::ViewTy, out: Self::Output) -> bool;
143
144    #[logic]
145    fn resolve_elswhere(self, old: T::ViewTy, fin: T::ViewTy) -> bool;
146}
147
148impl<T> SliceIndexSpec<[T]> for usize {
149    #[logic(open, inline)]
150    fn in_bounds(self, seq: Seq<T>) -> bool {
151        pearlite! { self@ < seq.len() }
152    }
153
154    #[logic(open, inline)]
155    fn has_value(self, seq: Seq<T>, out: T) -> bool {
156        pearlite! { seq[self@] == out }
157    }
158
159    #[logic(open, inline)]
160    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
161        pearlite! { forall<i> 0 <= i && i != self@ && i < old.len() ==> old[i] == fin[i] }
162    }
163}
164
165impl<T> SliceIndexSpec<[T]> for Range<usize> {
166    #[logic(open)]
167    fn in_bounds(self, seq: Seq<T>) -> bool {
168        pearlite! { self.start@ <= self.end@ && self.end@ <= seq.len() }
169    }
170
171    #[logic(open)]
172    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
173        pearlite! { seq.subsequence(self.start@, self.end@) == out@ }
174    }
175
176    #[logic(open)]
177    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
178        pearlite! {
179            forall<i> 0 <= i && (i < self.start@ || self.end@ <= i) && i < old.len()
180            ==> old[i] == fin[i]
181        }
182    }
183}
184
185impl<T> SliceIndexSpec<[T]> for RangeInclusive<usize> {
186    #[trusted]
187    #[logic(opaque)]
188    #[ensures(self.end_log()@ < seq.len() && self.start_log()@ <= self.end_log()@+1 ==> result)]
189    #[ensures(self.end_log()@ >= seq.len() ==> !result)]
190    fn in_bounds(self, seq: Seq<T>) -> bool {
191        dead
192    }
193
194    #[logic(open)]
195    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
196        pearlite! {
197            if self.is_empty_log() { out@ == Seq::empty() }
198            else { seq.subsequence(self.start_log()@, self.end_log()@ + 1) == out@ }
199        }
200    }
201
202    #[logic(open)]
203    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
204        pearlite! {
205            forall<i> 0 <= i
206                && (i < self.start_log()@ || self.end_log()@ < i || self.is_empty_log())
207                && i < old.len()
208                ==> old[i] == fin[i]
209        }
210    }
211}
212
213impl<T> SliceIndexSpec<[T]> for RangeTo<usize> {
214    #[logic(open)]
215    fn in_bounds(self, seq: Seq<T>) -> bool {
216        pearlite! { self.end@ <= seq.len() }
217    }
218
219    #[logic(open)]
220    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
221        pearlite! { seq.subsequence(0, self.end@) == out@ }
222    }
223
224    #[logic(open)]
225    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
226        pearlite! { forall<i> self.end@ <= i && i < old.len() ==> old[i] == fin[i] }
227    }
228}
229
230impl<T> SliceIndexSpec<[T]> for RangeFrom<usize> {
231    #[logic(open)]
232    fn in_bounds(self, seq: Seq<T>) -> bool {
233        pearlite! { self.start@ <= seq.len() }
234    }
235
236    #[logic(open)]
237    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
238        pearlite! { seq.subsequence(self.start@, seq.len()) == out@ }
239    }
240
241    #[logic(open)]
242    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
243        pearlite! {
244            forall<i> 0 <= i && i < self.start@ && i < old.len() ==> old[i] == fin[i]
245        }
246    }
247}
248
249impl<T> SliceIndexSpec<[T]> for RangeFull {
250    #[logic(open)]
251    fn in_bounds(self, _seq: Seq<T>) -> bool {
252        pearlite! { true }
253    }
254
255    #[logic(open)]
256    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
257        pearlite! { seq == out@ }
258    }
259
260    #[logic(open)]
261    fn resolve_elswhere(self, _old: Seq<T>, _fin: Seq<T>) -> bool {
262        pearlite! { true }
263    }
264}
265
266impl<T> SliceIndexSpec<[T]> for RangeToInclusive<usize> {
267    #[logic(open)]
268    fn in_bounds(self, seq: Seq<T>) -> bool {
269        pearlite! { self.end@ < seq.len() }
270    }
271
272    #[logic(open)]
273    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
274        pearlite! { seq.subsequence(0, self.end@ + 1) == out@ }
275    }
276
277    #[logic(open)]
278    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
279        pearlite! { forall<i> self.end@ < i && i < old.len() ==> old[i] == fin[i] }
280    }
281}
282
283#[logic(open, inline)]
284pub fn to_logic_range((lo, hi): (Bound<usize>, Bound<usize>), len: Int) -> Range<Int> {
285    pearlite! {
286        let lo = match lo {
287            Bound::Included(i) => i@,
288            Bound::Excluded(i) => i@ + 1,
289            Bound::Unbounded => 0
290        };
291        let hi = match hi {
292            Bound::Included(i) => i@ + 1,
293            Bound::Excluded(i) => i@,
294            Bound::Unbounded => len
295        };
296        lo..hi
297    }
298}
299
300impl<T> SliceIndexSpec<[T]> for (Bound<usize>, Bound<usize>) {
301    #[logic(open)]
302    fn in_bounds(self, seq: Seq<T>) -> bool {
303        let range = to_logic_range(self, seq.len());
304        pearlite! { range.start <= range.end && range.end <= seq.len() }
305    }
306
307    #[logic(open)]
308    fn has_value(self, seq: Seq<T>, out: [T]) -> bool {
309        let range = to_logic_range(self, seq.len());
310        pearlite! { seq.subsequence(range.start, range.end) == out@ }
311    }
312
313    #[logic(open)]
314    fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool {
315        let range = to_logic_range(self, old.len());
316        pearlite! {
317            forall<i> 0 <= i && (i < range.start || range.end <= i) && i < old.len()
318            ==> old[i] == fin[i]
319        }
320    }
321}
322
323extern_spec! {
324    impl<T> [T] {
325        #[check(ghost)]
326        #[requires(self@.len() == src@.len())]
327        #[ensures((^self)@ == src@)]
328        fn copy_from_slice(&mut self, src: &[T]) where T: Copy;
329
330        #[check(ghost)]
331        #[ensures(self@.len() == result@)]
332        fn len(&self) -> usize;
333
334        #[check(ghost)]
335        #[requires(i@ < self@.len())]
336        #[requires(j@ < self@.len())]
337        #[ensures((^self)@.exchange(self@, i@, j@))]
338        fn swap(&mut self, i: usize, j: usize);
339
340        #[ensures(ix.in_bounds(self@) ==> exists<r> result == Some(r) && ix.has_value(self@, *r))]
341        #[ensures(ix.in_bounds(self@) || result == None)]
342        fn get<I: SliceIndexSpec<[T]>>(&self, ix: I) -> Option<&<I as SliceIndex<[T]>>::Output>;
343
344        #[ensures((^self)@.len() == self@.len())]
345        #[ensures(ix.in_bounds(self@) ==> exists<r>
346                    result == Some(r) &&
347                    ix.has_value(self@, *r) &&
348                    ix.has_value((^self)@, ^r) &&
349                    ix.resolve_elswhere(self@, (^self)@))]
350        #[ensures(ix.in_bounds(self@) || result == None)]
351        fn get_mut<I: SliceIndexSpec<[T]>>(&mut self, ix: I)
352            -> Option<&mut <I as SliceIndex<[T]>>::Output>;
353
354        #[check(ghost)]
355        #[requires(mid@ <= self@.len())]
356        #[ensures({
357            let (l,r) = result;  let sl = self@.len();
358            ((^self)@.len() == sl) &&
359            self@.subsequence(0, mid@) == l@ &&
360            self@.subsequence(mid@, sl) == r@ &&
361            (^self)@.subsequence(0, mid@) == (^l)@ &&
362            (^self)@.subsequence(mid@, sl) == (^r)@
363        })]
364        fn split_at_mut(&mut self, mid: usize) -> (&mut [T], &mut [T]);
365
366        #[check(ghost)]
367        #[ensures(match result {
368            Some((first, tail)) => {
369                *first == self[0] && ^first == (^self)[0] &&
370                (*self)@.len() > 0 && (^self)@.len() > 0 &&
371                (*tail)@ == (*self)@.tail() &&
372                (^tail)@ == (^self)@.tail()
373            }
374            None => self@.len() == 0 && ^self == *self && self@ == Seq::empty()
375        })]
376        fn split_first_mut(&mut self) -> Option<(&mut T, &mut [T])>;
377
378        #[check(ghost)]
379        #[ensures((^*self)@.len() == (**self)@.len())]
380        #[ensures((^^self)@.len() == (*^self)@.len())]
381        #[ensures(match result {
382            Some(r) => {
383                (**self)@.len() > 0 &&
384                r == &mut (**self)[0] &&
385                (^self).to_mut_seq() == (*self).to_mut_seq().tail()
386            }
387            None => resolve(self) && (^*self)@ == Seq::empty() && (**self)@ == Seq::empty()
388        })]
389        fn split_off_first_mut<'a>(self: &mut &'a mut [T]) -> Option<&'a mut T>;
390
391        #[check(ghost)]
392        #[ensures((^*self)@.len() == (**self)@.len())]
393        #[ensures((^^self)@.len() == (*^self)@.len())]
394        #[ensures(match result {
395            Some(r) => {
396                (**self)@.len() > 0 &&
397                r == &mut (**self)[(**self)@.len()-1] &&
398                (^self).to_mut_seq() == (*self).to_mut_seq().subsequence(0, (*self).to_mut_seq().len()-1)
399            }
400            None => resolve(self) && (^*self)@ == Seq::empty() && (**self)@ == Seq::empty()
401        })]
402        fn split_off_last_mut<'a>(self: &mut &'a mut [T]) -> Option<&'a mut T>;
403
404        #[check(ghost)]
405        #[ensures(result@ == self)]
406        fn iter(&self) -> Iter<'_, T>;
407
408        #[check(ghost)]
409        #[ensures(result@ == self)]
410        fn iter_mut(&mut self) -> IterMut<'_, T>;
411
412        #[check(ghost)]
413        #[ensures(result == None ==> self@.len() == 0)]
414        #[ensures(forall<x> result == Some(x) ==> self[self@.len() - 1] == *x)]
415        fn last(&self) -> Option<&T>;
416
417        #[check(ghost)]
418        #[ensures(result == None ==> self@.len() == 0)]
419        #[ensures(forall<x> result == Some(x) ==> self[0] == *x)]
420        fn first(&self) -> Option<&T>;
421
422
423        #[requires(self.deep_model().sorted())]
424        #[ensures(forall<i:usize> result == Ok(i) ==>
425            i@ < self@.len() && (*self).deep_model()[i@] == x.deep_model())]
426        #[ensures(forall<i:usize> result == Err(i) ==> i@ <= self@.len() &&
427            forall<j> 0 <= j && j < self@.len() ==> self.deep_model()[j] != x.deep_model())]
428        #[ensures(forall<i:usize> result == Err(i) ==>
429            forall<j:usize> j < i ==> self.deep_model()[j@] < x.deep_model())]
430        #[ensures(forall<i:usize> result == Err(i) ==>
431            forall<j:usize> i <= j && j@ < self@.len() ==> x.deep_model() < self.deep_model()[j@])]
432        fn binary_search(&self, x: &T) -> Result<usize, usize>
433            where T: Ord + DeepModel,  T::DeepModelTy: OrdLogic,;
434
435        #[requires(ix.in_bounds(self@))]
436        #[ensures(ix.has_value(self@, *result))]
437        unsafe fn get_unchecked<I: SliceIndexSpec<[T]>>(&self, ix: I)
438            -> &<I as SliceIndex<[T]>>::Output;
439
440        #[requires(ix.in_bounds(self@))]
441        #[ensures(ix.has_value(self@, *result))]
442        #[ensures(ix.has_value((^self)@, ^result))]
443        #[ensures(ix.resolve_elswhere(self@, (^self)@))]
444        #[ensures((^self)@.len() == self@.len())]
445        unsafe fn get_unchecked_mut<I: SliceIndexSpec<[T]>>(&mut self, ix: I)
446            -> &mut <I as SliceIndex<[T]>>::Output;
447
448        // Calling this is safe but you should use `as_ptr_perm` instead to prove things.
449        #[check(ghost)]
450        fn as_ptr(&self) -> *const T;
451
452        // Calling this is safe but you should use `as_mut_ptr_perm` instead to prove things.
453        #[check(ghost)]
454        fn as_mut_ptr(&mut self) -> *mut T;
455    }
456
457    impl<T, I: SliceIndexSpec<[T]>> IndexMut<I> for [T] {
458        #[check(ghost)]
459        #[requires(ix.in_bounds(self@))]
460        #[ensures(ix.has_value(self@, *result))]
461        #[ensures(ix.has_value((&^self)@, ^result))]
462        #[ensures(ix.resolve_elswhere(self@, (&^self)@))]
463        #[ensures((&^self)@.len() == self@.len())]
464        fn index_mut(&mut self, ix: I) -> &mut <[T] as Index<I>>::Output;
465    }
466
467    impl<T, I: SliceIndexSpec<[T]>> Index<I> for [T] {
468        #[check(ghost)]
469        #[requires(ix.in_bounds(self@))]
470        #[ensures(ix.has_value(self@, *result))]
471        fn index(&self, ix: I) -> &<[T] as Index<I>>::Output;
472    }
473
474    impl<'a, T> IntoIterator for &'a [T] {
475        #[check(ghost)]
476        #[ensures(self == result@)]
477        fn into_iter(self) -> Iter<'a, T>;
478    }
479
480    impl<'a, T> IntoIterator for &'a mut [T] {
481        #[check(ghost)]
482        #[ensures(self == result@)]
483        fn into_iter(self) -> IterMut<'a, T>;
484    }
485
486    impl<'a, T> Default for &'a mut [T] {
487        #[check(ghost)]
488        #[ensures((*result)@ == Seq::empty())]
489        #[ensures((^result)@ == Seq::empty())]
490        fn default() -> &'a mut [T];
491    }
492
493    impl<'a, T> Default for &'a [T] {
494        #[check(ghost)]
495        #[ensures(result@ == Seq::empty())]
496        fn default() -> &'a [T];
497    }
498
499    mod core {
500        mod slice {
501            #[check(ghost)]
502            #[ensures(result@.len() == 1)]
503            #[ensures(result@[0] == *s)]
504            fn from_ref<T>(s: &T) -> &[T];
505
506            #[check(ghost)]
507            #[ensures(result@.len() == 1)]
508            #[ensures(result@[0] == *s)]
509            #[ensures((^result)@.len() == 1)]
510            #[ensures((^result)@[0] == ^s)]
511            fn from_mut<T>(s: &mut T) -> &mut [T];
512        }
513    }
514}
515
516#[cfg(feature = "std")]
517extern_spec! {
518    impl<T> [T] {
519        #[check(ghost)]
520        #[ensures(result@ == self_@)]
521        fn into_vec<A: Allocator>(self_: Box<Self, A>) -> Vec<T, A>;
522
523        // FIXME: inherit ghost/terminates from clone
524        #[ensures(result@.len() == self@.len())]
525        #[ensures(forall<i> 0 <= i && i < self@.len() ==> <T as Clone>::clone.postcondition((&self@[i],), result@[i]))]
526        fn to_vec(&self) -> Vec<T> where T: Clone;
527    }
528
529    impl<T: Clone, A: Allocator + Clone> Clone for Box<[T], A> {
530        #[ensures(forall<i> 0 <= i && i < self@.len() ==>
531            T::clone.postcondition((&self@[i],), result@[i]))]
532        fn clone(&self) -> Box<[T], A>;
533    }
534}
535
536impl<'a, T> View for Iter<'a, T> {
537    type ViewTy = &'a [T];
538
539    #[logic(opaque)]
540    fn view(self) -> Self::ViewTy {
541        dead
542    }
543}
544
545impl<'a, T> IteratorSpec for Iter<'a, T> {
546    #[logic(open, prophetic)]
547    fn completed(&mut self) -> bool {
548        pearlite! { resolve(self) && (*self@)@ == Seq::empty() }
549    }
550
551    #[logic(open)]
552    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
553        pearlite! {
554            self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
555        }
556    }
557
558    #[logic(law)]
559    #[ensures(self.produces(Seq::empty(), self))]
560    fn produces_refl(self) {
561        let _ = Seq::<Self::Item>::concat_empty;
562    }
563
564    #[logic(law)]
565    #[requires(a.produces(ab, b))]
566    #[requires(b.produces(bc, c))]
567    #[ensures(a.produces(ab.concat(bc), c))]
568    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
569        let _ = Seq::<Self::Item>::concat_assoc;
570    }
571}
572
573extern_spec! {
574    impl<'a, T> Iterator for Iter<'a, T> {
575        #[ensures(result.0@ == self@@.len())]
576        #[ensures(result.1 == Some(result.0))]
577        fn size_hint(&self) -> (usize, Option<usize>);
578    }
579}
580
581impl<'a, T> ExactSizeIteratorSpec for Iter<'a, T> {
582    #[logic(law)]
583    #[requires(Self::size_hint.postcondition((self,), r))]
584    #[ensures(r.1 == Some(r.0))]
585    #[allow(unused_variables)]
586    fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
587}
588
589impl<'a, T> DoubleEndedIteratorSpec for Iter<'a, T> {
590    #[logic(open)]
591    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
592        pearlite! {
593          self@.to_ref_seq() == o@.to_ref_seq().concat(visited.reverse())
594        }
595    }
596
597    #[logic(open, prophetic)]
598    fn completed_back(&mut self) -> bool {
599        self.completed()
600    }
601
602    #[logic(law)]
603    #[ensures(self.produces_back(Seq::empty(), self))]
604    fn produces_back_refl(self) {
605        let _ = Seq::<Self::Item>::reverse_empty();
606        let _ = Seq::<Self::Item>::concat_empty;
607    }
608
609    #[logic(law)]
610    #[requires(a.produces_back(ab, b))]
611    #[requires(b.produces_back(bc, c))]
612    #[ensures(a.produces_back(ab.concat(bc), c))]
613    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
614        let _ = ab.reverse_concat(bc);
615        let _ = Seq::<Self::Item>::concat_assoc;
616    }
617
618    #[logic(law)]
619    #[requires(Self::size_hint.postcondition((self,), r))]
620    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
621        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
622    #[ensures(match r.1 {
623        Some(r) => {
624            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
625        }
626        None => true
627    })]
628    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
629}
630
631impl<'a, T> View for IterMut<'a, T> {
632    type ViewTy = &'a mut [T];
633
634    #[trusted]
635    #[logic(opaque)]
636    #[ensures((^result)@.len() == (*result)@.len())]
637    fn view(self) -> Self::ViewTy {
638        dead
639    }
640}
641
642impl<'a, T> Resolve for IterMut<'a, T> {
643    #[logic(open, prophetic, inline)]
644    fn resolve(self) -> bool {
645        pearlite! { *self@ == ^self@ }
646    }
647
648    #[trusted]
649    #[logic(prophetic)]
650    #[requires(structural_resolve(self))]
651    #[ensures(self.resolve())]
652    fn resolve_coherence(self) {}
653}
654
655impl<'a, T> IteratorSpec for IterMut<'a, T> {
656    #[logic(open, prophetic)]
657    fn completed(&mut self) -> bool {
658        pearlite! { resolve(self) && (*self@)@ == Seq::empty() }
659    }
660
661    #[logic(open)]
662    fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool {
663        pearlite! {
664            self@.to_mut_seq() == visited.concat(tl@.to_mut_seq())
665        }
666    }
667
668    #[logic(law)]
669    #[ensures(self.produces(Seq::empty(), self))]
670    fn produces_refl(self) {
671        let _ = Seq::<Self::Item>::concat_empty;
672    }
673
674    #[logic(law)]
675    #[requires(a.produces(ab, b))]
676    #[requires(b.produces(bc, c))]
677    #[ensures(a.produces(ab.concat(bc), c))]
678    fn produces_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
679        let _ = Seq::<Self::Item>::concat_assoc;
680    }
681}
682
683extern_spec! {
684    impl<'a, T> Iterator for IterMut<'a, T> {
685        #[ensures(result.0@ == self@@.len())]
686        #[ensures(result.1 == Some(result.0))]
687        fn size_hint(&self) -> (usize, Option<usize>);
688    }
689}
690
691impl<'a, T> ExactSizeIteratorSpec for IterMut<'a, T> {
692    #[logic(law)]
693    #[requires(Self::size_hint.postcondition((self,), r))]
694    #[ensures(r.1 == Some(r.0))]
695    #[allow(unused_variables)]
696    fn size_hint_exact(&self, r: (usize, Option<usize>)) {}
697}
698
699impl<'a, T> DoubleEndedIteratorSpec for IterMut<'a, T> {
700    #[logic(open)]
701    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool {
702        pearlite! {
703            self@.to_mut_seq() == o@.to_mut_seq().concat(visited.reverse())
704        }
705    }
706
707    #[logic(open, prophetic)]
708    fn completed_back(&mut self) -> bool {
709        self.completed()
710    }
711
712    #[logic(law)]
713    #[ensures(self.produces_back(Seq::empty(), self))]
714    fn produces_back_refl(self) {
715        let _ = Seq::<Self::Item>::reverse_empty();
716        let _ = Seq::<Self::Item>::concat_empty;
717    }
718
719    #[logic(law)]
720    #[requires(a.produces_back(ab, b))]
721    #[requires(b.produces_back(bc, c))]
722    #[ensures(a.produces_back(ab.concat(bc), c))]
723    fn produces_back_trans(a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self) {
724        let _ = ab.reverse_concat(bc);
725        let _ = Seq::<Self::Item>::concat_assoc;
726    }
727
728    #[logic(law)]
729    #[requires(Self::size_hint.postcondition((self,), r))]
730    #[ensures(forall<s: Seq<Self::Item>, i: &mut Self>
731        self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len())]
732    #[ensures(match r.1 {
733        Some(r) => {
734            forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
735        }
736        None => true
737    })]
738    fn size_hint_back_spec(&self, r: (usize, Option<usize>)) {}
739}
740
741extern_spec! {
742    impl<'a, T> Iter<'a, T> {
743        #[ensures(result@ == self@@)]
744        fn as_slice(&self) -> &'a [T];
745    }
746
747    impl<'a, T> ExactSizeIterator for Iter<'a, T> {
748        #[ensures(result@ == self@@.len())]
749        fn len(&self) -> usize;
750    }
751
752    impl<'a, T> IterMut<'a, T> {
753        #[ensures(result@ == self@@)]
754        fn as_slice(&self) -> &'a [T];
755    }
756
757    impl<'a, T> ExactSizeIterator for IterMut<'a, T> {
758        #[ensures(result@ == self@@.len())]
759        fn len(&self) -> usize;
760    }
761}
creusot_std/std/slice.rs

creusot_std/std/
slice.rs
