vstd/std_specs/
slice.rs

1use super::super::prelude::*;
2use super::super::slice::SliceIndexSpec;
3use super::core::IndexSpec;
4use super::iter::IteratorSpec;
5use super::range::{
6    ExRange, RangeBoundsSpec, slice_range_end, slice_range_start, slice_range_valid,
7};
8
9use core::ops::{
10    Index, IndexMut, Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive,
11};
12use core::slice::{Chunks, Iter, IterMut, SliceIndex};
13
14use verus as verus_skip_verusfmt;
15verus_skip_verusfmt! {
16
17impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for usize {
18    open spec fn in_bounds(&self, slice: &[T]) -> bool {
19        *self < slice@.len()
20    }
21
22    open spec fn index_postcondition(&self, slice: &[T], r: &T) -> bool {
23        r == slice@[self as int]
24    }
25
26    open spec fn index_mut_postcondition(
27        &self,
28        old_slice: &[T],
29        final_slice: &[T],
30        immediate_output: &T,
31        final_output: &T,
32    ) -> bool {
33        &&& *immediate_output == old_slice@[*self as int]
34        &&& final_slice@ == old_slice@.update(*self as int, *final_output)
35    }
36}
37
38pub assume_specification<T>[ <usize as SliceIndex<[T]>>::get ](i: usize, slice: &[T]) -> Option<&T>;
39
40pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index ](i: usize, slice: &[T]) -> &T
41;
42
43pub assume_specification<T>[ <usize as SliceIndex<[T]>>::get_mut ](i: usize, slice: &mut [T]) -> Option<&mut T>;
44
45pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index_mut ](i: usize, slice: &mut [T]) -> (output: &mut T)
46;
47
48pub open spec fn generic_slice_in_bounds<R: RangeBoundsSpec<usize>, T>(
49    range: &R,
50    s: Seq<T>
51) -> bool {
52    slice_range_valid(range, s.len())
53}
54
55pub open spec fn generic_slice_index_postcondition<R: RangeBoundsSpec<usize>, T>(
56    range: &R,
57    slice: Seq<T>,
58    r: Seq<T>,
59) -> bool {
60    r == slice[slice_range_start(range)..slice_range_end(range, slice.len())]
61}
62
63pub open spec fn generic_slice_index_mut_postcondition<R: RangeBoundsSpec<usize>, T>(
64    range: &R,
65    old_slice: Seq<T>,
66    final_slice: Seq<T>,
67    immediate_output: Seq<T>,
68    final_output: Seq<T>,
69) -> bool {
70    &&& immediate_output == old_slice[slice_range_start(range)..slice_range_end(range, old_slice.len())]
71    &&& final_slice.len() == old_slice.len()
72    &&& final_slice[..slice_range_start(range)] == old_slice[..slice_range_start(range)]
73    &&& final_slice[slice_range_start(range)..slice_range_end(range, old_slice.len())] == final_output
74    &&& final_slice[slice_range_end(range, old_slice.len())..old_slice.len()] ==
75        old_slice[slice_range_end(range, old_slice.len())..old_slice.len()]
76    // The following conjunct can be derived from the above four, but
77    // it's useful to include anyway.
78    &&& final_slice == old_slice[..slice_range_start(range)] + final_output + old_slice[
79           slice_range_end(range, old_slice.len())..old_slice.len()]
80}
81
82impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for Range<usize> {
83    open spec fn in_bounds(&self, slice: &[T]) -> bool {
84        generic_slice_in_bounds(self, slice@)
85    }
86
87    open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool {
88        generic_slice_index_postcondition(self, slice@, r@)
89    }
90
91    open spec fn index_mut_postcondition(
92        &self,
93        old_slice: &[T],
94        final_slice: &[T],
95        immediate_output: &[T],
96        final_output: &[T]
97    ) -> bool {
98        generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@)
99    }
100}
101
102pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::get ](i: Range<usize>, slice: &[T]) -> Option<&[T]>;
103
104pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index ](i: Range<usize>, slice: &[T]) -> (r: &[T])
105;
106
107pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::get_mut ](i: Range<usize>, slice: &mut [T]) -> Option<&mut [T]>;
108
109pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index_mut ](i: Range<usize>, slice: &mut [T]) -> (r: &mut [T])
110;
111
112impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeTo<usize> {
113    open spec fn in_bounds(&self, slice: &[T]) -> bool {
114        generic_slice_in_bounds(self, slice@)
115    }
116
117    open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool {
118        generic_slice_index_postcondition(self, slice@, r@)
119    }
120
121    open spec fn index_mut_postcondition(
122        &self,
123        old_slice: &[T],
124        final_slice: &[T],
125        immediate_output: &[T],
126        final_output: &[T]
127    ) -> bool {
128        generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@)
129    }
130}
131
132pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::get ](i: RangeTo<usize>, slice: &[T]) -> Option<&[T]>;
133
134pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::index ](i: RangeTo<usize>, slice: &[T]) -> (r: &[T])
135;
136
137pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::get_mut ](i: RangeTo<usize>, slice: &mut [T]) -> Option<&mut [T]>;
138
139pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::index_mut ](i: RangeTo<usize>, slice: &mut [T]) -> (r: &mut [T])
140;
141
142impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeFrom<usize> {
143    open spec fn in_bounds(&self, slice: &[T]) -> bool {
144        generic_slice_in_bounds(self, slice@)
145    }
146
147    open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool {
148        generic_slice_index_postcondition(self, slice@, r@)
149    }
150
151    open spec fn index_mut_postcondition(
152        &self,
153        old_slice: &[T],
154        final_slice: &[T],
155        immediate_output: &[T],
156        final_output: &[T]
157    ) -> bool {
158        generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@)
159    }
160}
161
162pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::get ](i: RangeFrom<usize>, slice: &[T]) -> Option<&[T]>;
163
164pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::index ](i: RangeFrom<usize>, slice: &[T]) -> (r: &[T])
165;
166
167pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::get_mut ](i: RangeFrom<usize>, slice: &mut [T]) -> Option<&mut [T]>;
168
169pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::index_mut ](i: RangeFrom<usize>, slice: &mut [T]) -> (r: &mut [T])
170;
171
172impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeToInclusive<usize> {
173    open spec fn in_bounds(&self, slice: &[T]) -> bool {
174        generic_slice_in_bounds(self, slice@)
175    }
176
177    open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool {
178        generic_slice_index_postcondition(self, slice@, r@)
179    }
180
181    open spec fn index_mut_postcondition(
182        &self,
183        old_slice: &[T],
184        final_slice: &[T],
185        immediate_output: &[T],
186        final_output: &[T]
187    ) -> bool {
188        generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@)
189    }
190}
191
192pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::get ](i: RangeToInclusive<usize>, slice: &[T]) -> Option<&[T]>;
193
194pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::index ](i: RangeToInclusive<usize>, slice: &[T]) -> (r: &[T])
195;
196
197pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::get_mut ](i: RangeToInclusive<usize>, slice: &mut [T]) -> Option<&mut [T]>;
198
199pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::index_mut ](i: RangeToInclusive<usize>, slice: &mut [T]) -> (r: &mut [T])
200;
201
202impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeFull {
203    open spec fn in_bounds(&self, slice: &[T]) -> bool {
204        generic_slice_in_bounds(self, slice@)
205    }
206
207    open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool {
208        generic_slice_index_postcondition(self, slice@, r@)
209    }
210
211    open spec fn index_mut_postcondition(
212        &self,
213        old_slice: &[T],
214        final_slice: &[T],
215        immediate_output: &[T],
216        final_output: &[T]
217    ) -> bool {
218        generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@)
219    }
220}
221
222pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::get ](i: RangeFull, slice: &[T]) -> Option<&[T]>;
223
224pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::index ](i: RangeFull, slice: &[T]) -> (r: &[T])
225;
226
227pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::get_mut ](i: RangeFull, slice: &mut [T]) -> Option<&mut [T]>;
228
229pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::index_mut ](i: RangeFull, slice: &mut [T]) -> (r: &mut [T])
230;
231
232impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeInclusive<usize> {
233    open spec fn in_bounds(&self, slice: &[T]) -> bool {
234        generic_slice_in_bounds(self, slice@)
235    }
236
237    open spec fn index_postcondition(&self, slice: &[T], r: &[T]) -> bool {
238        generic_slice_index_postcondition(self, slice@, r@)
239    }
240
241    open spec fn index_mut_postcondition(
242        &self,
243        old_slice: &[T],
244        final_slice: &[T],
245        immediate_output: &[T],
246        final_output: &[T]
247    ) -> bool {
248        generic_slice_index_mut_postcondition(self, old_slice@, final_slice@, immediate_output@, final_output@)
249    }
250}
251
252pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::get ](i: RangeInclusive<usize>, slice: &[T]) -> Option<&[T]>;
253
254pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::index ](i: RangeInclusive<usize>, slice: &[T]) -> (r: &[T])
255;
256
257pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::get_mut ](i: RangeInclusive<usize>, slice: &mut [T]) -> Option<&mut [T]>;
258
259pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::index_mut ](i: RangeInclusive<usize>, slice: &mut [T]) -> (r: &mut [T])
260;
261
262// starts_with
263// Rust compares `needle == &slice[..needle.len()]`
264pub open spec fn spec_slice_starts_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool {
265    &&& needle@.len() <= slice@.len()
266    &&& forall|i: int| #![auto]
267        0 <= i < needle@.len() ==>
268            <T as super::cmp::PartialEqSpec<T>>::eq_spec(
269                &needle@[i],
270                &slice@[i],
271            )
272}
273
274#[verifier::when_used_as_spec(spec_slice_starts_with)]
275pub assume_specification<T: PartialEq>[ <[T]>::starts_with ](
276    slice: &[T],
277    needle: &[T],
278) -> (result: bool)
279    ensures
280        needle@.len() > slice@.len() ==> !result,
281        <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_starts_with(
282            slice,
283            needle,
284        )),
285;
286
287// ends_with
288// Rust compares `needle == &slice[slice.len() - needle.len()..]`.
289pub open spec fn spec_slice_ends_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool {
290    &&& needle@.len() <= slice@.len()
291    &&& forall|i: int| #![auto]
292        0 <= i < needle@.len() ==>
293            <T as super::cmp::PartialEqSpec<T>>::eq_spec(
294                &needle@[i],
295                &slice@[slice@.len() - needle@.len() + i],
296            )
297}
298
299#[verifier::when_used_as_spec(spec_slice_ends_with)]
300pub assume_specification<T: PartialEq>[ <[T]>::ends_with ](
301    slice: &[T],
302    needle: &[T],
303) -> (result: bool)
304    ensures
305        needle@.len() > slice@.len() ==> !result,
306        <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_ends_with(
307            slice,
308            needle,
309        )),
310;
311
312impl<T, I: SliceIndex<[T]>> super::core::IndexSpecImpl<I> for [T] {
313    open spec fn index_req(&self, index: &I) -> bool {
314        index.in_bounds(self)
315    }
316}
317
318pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
319    &<I as SliceIndex<[T]>>::Output,
320>) where I: SliceIndex<[T]>
321    ensures
322        call_ensures(<I as SliceIndex<[T]>>::get, (i, slice), b),
323;
324
325pub assume_specification<T, I>[ <[T]>::get_mut::<I> ](slice: &mut [T], i: I) -> (b: Option<
326    &mut <I as SliceIndex<[T]>>::Output,
327>) where I: SliceIndex<[T]>
328    ensures
329        call_ensures(<I as SliceIndex<[T]>>::get_mut, (i, slice), b),
330;
331
332pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as Index<I>>::index ](
333    slice: &[T],
334    index: I,
335) -> (output: &<I as SliceIndex<[T]>>::Output)
336    ensures
337        call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),
338;
339
340pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as IndexMut<I>>::index_mut ](
341    slice: &mut [T],
342    index: I,
343) -> (output: &mut <I as SliceIndex<[T]>>::Output)
344    ensures
345        call_ensures(<I as SliceIndex<[T]>>::index_mut, (index, slice), output),
346;
347
348impl<T, I, const N: usize> super::core::IndexSpecImpl<I> for [T; N]
349where
350    [T]: Index<I>,
351{
352    open spec fn index_req(&self, index: &I) -> bool {
353        <[T] as IndexSpec<I>>::index_req(self, index)
354    }
355}
356
357pub assume_specification<T, I, const N: usize>[ <[T; N]>::index ](array: &[T; N], index: I) -> (output: &<[T; N] as Index<I>>::Output)
358    where
359        [T]: Index<I>,
360    ensures
361        call_ensures(<[T]>::index, (array, index), output),
362;
363
364pub assume_specification<T, I, const N: usize>[ <[T; N]>::index_mut ](array: &mut [T; N], index: I) -> (output: &mut <[T; N] as Index<I>>::Output)
365    where
366        [T]: IndexMut<I>,
367    ensures
368        exists|slice: &mut [T]| {
369            &&& #[trigger] slice@ == old(array)@
370            &&& final(slice)@ == final(array)@
371            &&& call_ensures(<[T]>::index_mut, (slice, index), output)
372        },
373;
374
375pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
376    requires
377        false,
378;
379
380// slice == slice
381pub assume_specification<T: PartialEq<U>, U>[ <[T] as PartialEq<[U]>>::eq ](
382    left: &[T],
383    right: &[U],
384) -> bool
385;
386
387impl<T, U> super::cmp::PartialEqSpecImpl<[U]> for [T] where T: PartialEq<U> + super::cmp::PartialEqSpec<U> {
388    open spec fn obeys_eq_spec() -> bool {
389        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
390    }
391
392    open spec fn eq_spec(&self, other: &[U]) -> bool {
393        &&& self@.len() == other@.len()
394        &&& forall|i: int|
395            #![auto]
396            0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
397    }
398}
399
400// contains
401pub open spec fn spec_slice_contains<T: PartialEq<T>>(slice: &[T], value: &T) -> bool {
402    exists |i: int| #![auto] 0 <= i < slice@.len()
403        && <T as super::cmp::PartialEqSpec<T>>::eq_spec(&slice[i], value)
404}
405
406#[verifier::when_used_as_spec(spec_slice_contains)]
407pub assume_specification<T>[ <[T]>::contains ] (slice: &[T], value: &T) -> (result: bool)
408    where
409        T: PartialEq<T>,
410        ensures
411            <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> result == spec_slice_contains(slice, value),
412;
413
414// reverse
415pub assume_specification<T>[ <[T]>::reverse ](slice: &mut [T])
416    ensures
417        final(slice)@ == old(slice)@.reverse(),
418;
419
420// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
421// so we specify that type here.
422#[verifier::external_type_specification]
423#[verifier::external_body]
424#[verifier::accept_recursive_types(T)]
425pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
426
427// To allow reasoning about the "contents" of the slice iterator, without using
428// a prophecy, we need a function that gives us the underlying sequence of the original slice.
429pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<T>;
430
431impl <'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> {
432    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
433        true
434    }
435
436    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
437    uninterp spec fn will_return_none(&self) -> bool;
438    uninterp spec fn decrease(&self) -> Option<nat>;
439
440    open spec fn peek(&self, index: int) -> Option<Self::Item> {
441        if 0 <= index < into_iter_elts(*self).len() {
442            Some(&into_iter_elts(*self)[index])
443        } else {
444            None
445        }
446    }
447}
448
449pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>)
450    ensures
451        IteratorSpec::remaining(&iter) == s@.as_ref(),
452        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
453        IteratorSpec::decrease(&iter) is Some,
454;
455
456pub assume_specification<'a, T> [<&'a [T] as core::iter::IntoIterator>::into_iter] (s: &'a [T]) ->
457    (iter: Iter<'a, T>)
458    ensures
459        IteratorSpec::remaining(&iter) == s@.as_ref(),
460        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
461        IteratorSpec::decrease(&iter) is Some,
462;
463
464/***********************************************************************************************
465 * Definitions for `slice::IterMut` (the iterator behind `<[T]>::iter_mut` and `Vec::iter_mut`)
466 ***********************************************************************************************/
467#[verifier::external_type_specification]
468#[verifier::external_body]
469#[verifier::accept_recursive_types(T)]
470pub struct ExIterMut<'a, T: 'a>(IterMut<'a, T>);
471
472// See exampes/iterators/slice_iter_mut.rs for a verified implementation of this interface.
473// Any changes here should first be verified over there.
474impl<'a, T: 'a> super::iter::IteratorSpecImpl for IterMut<'a, T> {
475    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
476        true
477    }
478
479    #[verifier::prophetic]
480    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
481
482    open spec fn will_return_none(&self) -> bool { true }
483
484    uninterp spec fn decrease(&self) -> Option<nat>;
485
486    open spec fn peek(&self, index: int) -> Option<Self::Item> { None }
487}
488
489// Also covers `vec.iter_mut(), which reaches this slice fn through `Vec`'s `DerefMut`
490pub assume_specification<'a, T>[ <[T]>::iter_mut ](slice: &'a mut [T]) -> (iter: IterMut<'a, T>)
491    ensures
492        IteratorSpec::remaining(&iter).len() == old(slice)@.len() == final(slice)@.len(),
493        // Each yielded reference initially points at the corresponding element...
494        forall|i: int| #![trigger IteratorSpec::remaining(&iter)[i]]
495            0 <= i < old(slice)@.len() ==> *(IteratorSpec::remaining(&iter)[i]) == old(slice)@[i],
496        // ...and its eventual value flows back to the corresponding element.
497        forall|i: int|
498            #![trigger IteratorSpec::remaining(&iter)[i]]
499            #![trigger final(slice)@[i]]
500            0 <= i < old(slice)@.len() ==> *final(IteratorSpec::remaining(&iter)[i]) == final(slice)@[i],
501        IteratorSpec::obeys_prophetic_iter_laws(&iter),
502        IteratorSpec::will_return_none(&iter),
503        IteratorSpec::decrease(&iter) is Some,
504;
505
506pub assume_specification<T> [ <[T]>::first ](slice: &[T]) -> (res: Option<&T>)
507    ensures
508        slice.len() == 0 ==> res.is_none(),
509        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0]
510    no_unwind
511;
512
513pub assume_specification<T> [ <[T]>::last ](slice: &[T]) -> (res: Option<&T>)
514    ensures
515        slice.len() == 0 ==> res.is_none(),
516        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last()
517    no_unwind
518;
519
520#[doc(hidden)]
521pub assume_specification<T> [ <[T]>::first_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
522    ensures
523        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
524        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)[0]
525            && final(slice)@ == old(slice)@.update(0, *final(res.unwrap()))
526    no_unwind
527;
528
529#[doc(hidden)]
530pub assume_specification<T> [ <[T]>::last_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
531    ensures
532        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
533        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)@.last()
534            && final(slice)@ == old(slice)@.update(old(slice).len() - 1, *final(res.unwrap()))
535    no_unwind
536;
537
538pub assume_specification<T> [ <[T]>::split_at ](slice: &[T], mid: usize) -> (ret: (&[T], &[T]))
539    requires
540        0 <= mid <= slice.len(),
541    ensures
542        ret.0@ == slice@[..mid],
543        ret.1@ == slice@[mid..],
544    no_unwind
545;
546
547#[doc(hidden)]
548pub assume_specification<T> [ <[T]>::split_at_mut ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T]))
549    requires
550        0 <= mid <= slice.len(),
551    ensures
552        ret.0@ == old(slice)@[..mid],
553        ret.1@ == old(slice)@[mid..],
554        final(slice)@ == final(ret.0)@ + final(ret.1)@,
555    no_unwind
556;
557
558// The non-panicking (`Option`-returning) form of `split_at`: `Some((a, b))` split at `mid`
559// when `mid <= len`, else `None`.
560pub assume_specification<T> [ <[T]>::split_at_checked ](slice: &[T], mid: usize) -> (ret: Option<(&[T], &[T])>)
561    ensures
562        mid <= slice.len() ==> (ret matches Some((a, b))
563            && a@ == slice@[..mid]
564            && b@ == slice@[mid..]),
565        mid > slice.len() ==> ret is None,
566    no_unwind
567;
568
569pub assume_specification<T> [ <[T]>::split_first ](slice: &[T]) -> (ret: Option<(&T, &[T])>)
570    ensures
571        slice.len() == 0 ==> ret.is_none(),
572        slice.len() > 0 ==> (ret matches Some((a, b)) && a == slice[0] && b@ == slice@[1..])
573    no_unwind
574;
575
576pub assume_specification<T> [ <[T]>::split_first_mut ](slice: &mut [T]) -> (ret: Option<(&mut T, &mut [T])>)
577    ensures
578        old(slice).len() == 0 ==> ret.is_none() && final(slice)@ == seq![],
579        old(slice).len() > 0 ==> (ret matches Some((a, b))
580            && *a == old(slice)[0]
581            && b@ == old(slice)@[1..]
582            && b@.len() == final(b)@.len()
583            && final(slice)@ == seq![*final(a)] + final(b)@
584        )
585    no_unwind
586;
587
588/// Copy the contents of `src` into `dst`, which must have the same length.
589pub assume_specification<T: Copy>[ <[T]>::copy_from_slice ](dst: &mut [T], src: &[T])
590    requires
591        old(dst)@.len() == src@.len(),
592    ensures
593        final(dst)@ == src@,
594;
595
596/// The sequence resulting from copying `old_slice[src_start..src_end]` to start
597/// at index `dest`, leaving all other positions unchanged. Reads are taken from
598/// `old_slice`, so overlapping source and destination ranges are handled like
599/// std's `<[T]>::copy_within` (which uses `ptr::copy`).
600pub open spec fn copy_within_result<T>(
601    old_slice: Seq<T>,
602    src_start: int,
603    src_end: int,
604    dest: int,
605) -> Seq<T> {
606    let count = src_end - src_start;
607    Seq::new(
608        old_slice.len(),
609        |i: int|
610            if dest <= i && i < dest + count {
611                old_slice[src_start + (i - dest)]
612            } else {
613                old_slice[i]
614            },
615    )
616}
617
618/// Copy the elements in range `src` within the slice to start at index `dest`.
619pub assume_specification<T: Copy, R: core::ops::RangeBounds<usize>>[ <[T]>::copy_within::<R> ](
620    slice: &mut [T],
621    src: R,
622    dest: usize,
623)
624    requires
625        slice_range_valid(&src, old(slice)@.len()),
626        (dest as int) + (slice_range_end(&src, old(slice)@.len()) - slice_range_start(&src))
627            <= old(slice)@.len(),
628    ensures
629        final(slice)@ == copy_within_result(
630            old(slice)@,
631            slice_range_start(&src),
632            slice_range_end(&src, old(slice)@.len()),
633            dest as int,
634        ),
635;
636
637// The `chunks` method of a `[T]` returns an iterator of type `Chunks<'_, T>`,
638// so we specify that type here.
639#[verifier::external_type_specification]
640#[verifier::external_body]
641#[verifier::accept_recursive_types(T)]
642pub struct ExChunks<'a, T: 'a>(Chunks<'a, T>);
643
644// To allow reasoning about the "chunks" of the slice iterator, without using
645// a prophecy, we need a function that gives us the the sequence of chunk slices
646// remaining in the iterator.
647pub uninterp spec fn after_chunks_elts<'a, T: 'a>(i: Chunks<'a, T>) -> Seq<&'a [T]>;
648
649impl<'a, T: 'a> super::iter::IteratorSpecImpl for Chunks<'a, T> {
650    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
651        true
652    }
653
654    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
655
656    uninterp spec fn will_return_none(&self) -> bool;
657
658    uninterp spec fn decrease(&self) -> Option<nat>;
659
660    open spec fn peek(&self, index: int) -> Option<Self::Item> {
661        if 0 <= index < after_chunks_elts(*self).len() {
662            Some(after_chunks_elts(*self)[index])
663        } else {
664            None
665        }
666    }
667}
668
669pub assume_specification<'a, T>[ <[T]>::chunks ](s: &'a [T], chunk_size: usize) -> (iter: Chunks<
670    'a,
671    T,
672>)
673    requires
674        chunk_size > 0,
675    ensures
676        IteratorSpec::remaining(&iter) == after_chunks_elts(iter),
677        IteratorSpec::remaining(&iter).len() == (s@.len() + chunk_size as int - 1) / (
678        chunk_size as int),
679        forall|i: int|
680            #![trigger IteratorSpec::remaining(&iter)[i]]
681            0 <= i < IteratorSpec::remaining(&iter).len() ==> {
682                let start = i * chunk_size as int;
683                let end = if start + chunk_size as int <= s@.len() {
684                    start + chunk_size as int
685                } else {
686                    s@.len() as int
687                };
688
689                IteratorSpec::remaining(&iter)[i]@ == s@.subrange(start, end)
690            },
691        IteratorSpec::decrease(&iter) is Some,
692;
693
694} // verus!
vstd/std_specs/slice.rs

vstd/std_specs/
slice.rs
