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

creusot_std/std/
slice.rs
