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::{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
263pub open spec fn spec_slice_starts_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool {
264    &&& needle@.len() <= slice@.len()
265    &&& forall|i: int| #![auto]
266        0 <= i < needle@.len() ==>
267            <T as super::cmp::PartialEqSpec<T>>::eq_spec(
268                &slice@[i],
269                &needle@[i],
270            )
271}
272
273#[verifier::when_used_as_spec(spec_slice_starts_with)]
274pub assume_specification<T: PartialEq>[ <[T]>::starts_with ](
275    slice: &[T],
276    needle: &[T],
277) -> (result: bool)
278    ensures
279        needle@.len() > slice@.len() ==> !result,
280        <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_starts_with(
281            slice,
282            needle,
283        )),
284;
285
286// ends_with
287pub open spec fn spec_slice_ends_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool {
288    &&& needle@.len() <= slice@.len()
289    &&& forall|i: int| #![auto]
290        0 <= i < needle@.len() ==>
291            <T as super::cmp::PartialEqSpec<T>>::eq_spec(
292                &slice@[slice@.len() - needle@.len() + i],
293                &needle@[i],
294            )
295}
296
297#[verifier::when_used_as_spec(spec_slice_ends_with)]
298pub assume_specification<T: PartialEq>[ <[T]>::ends_with ](
299    slice: &[T],
300    needle: &[T],
301) -> (result: bool)
302    ensures
303        needle@.len() > slice@.len() ==> !result,
304        <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_ends_with(
305            slice,
306            needle,
307        )),
308;
309
310impl<T, I: SliceIndex<[T]>> super::core::IndexSpecImpl<I> for [T] {
311    open spec fn index_req(&self, index: &I) -> bool {
312        index.in_bounds(self)
313    }
314}
315
316pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
317    &<I as SliceIndex<[T]>>::Output,
318>) where I: SliceIndex<[T]>
319    ensures
320        call_ensures(<I as SliceIndex<[T]>>::get, (i, slice), b),
321;
322
323pub assume_specification<T, I>[ <[T]>::get_mut::<I> ](slice: &mut [T], i: I) -> (b: Option<
324    &mut <I as SliceIndex<[T]>>::Output,
325>) where I: SliceIndex<[T]>
326    ensures
327        call_ensures(<I as SliceIndex<[T]>>::get_mut, (i, slice), b),
328;
329
330pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as Index<I>>::index ](
331    slice: &[T],
332    index: I,
333) -> (output: &<I as SliceIndex<[T]>>::Output)
334    ensures
335        call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),
336;
337
338pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as IndexMut<I>>::index_mut ](
339    slice: &mut [T],
340    index: I,
341) -> (output: &mut <I as SliceIndex<[T]>>::Output)
342    ensures
343        call_ensures(<I as SliceIndex<[T]>>::index_mut, (index, slice), output),
344;
345
346impl<T, I, const N: usize> super::core::IndexSpecImpl<I> for [T; N]
347where
348    [T]: Index<I>,
349{
350    open spec fn index_req(&self, index: &I) -> bool {
351        <[T] as IndexSpec<I>>::index_req(self, index)
352    }
353}
354
355pub assume_specification<T, I, const N: usize>[ <[T; N]>::index ](array: &[T; N], index: I) -> (output: &<[T; N] as Index<I>>::Output)
356    where
357        [T]: Index<I>,
358    ensures
359        call_ensures(<[T]>::index, (array, index), output),
360;
361
362pub 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)
363    where
364        [T]: IndexMut<I>,
365    ensures
366        exists|slice: &mut [T]| {
367            &&& #[trigger] slice@ == old(array)@
368            &&& final(slice)@ == final(array)@
369            &&& call_ensures(<[T]>::index_mut, (slice, index), output)
370        },
371;
372
373pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
374    requires
375        false,
376;
377
378// slice == slice
379pub assume_specification<T: PartialEq<U>, U>[ <[T] as PartialEq<[U]>>::eq ](
380    left: &[T],
381    right: &[U],
382) -> bool
383;
384
385impl<T, U> super::cmp::PartialEqSpecImpl<[U]> for [T] where T: PartialEq<U> + super::cmp::PartialEqSpec<U> {
386    open spec fn obeys_eq_spec() -> bool {
387        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
388    }
389
390    open spec fn eq_spec(&self, other: &[U]) -> bool {
391        &&& self@.len() == other@.len()
392        &&& forall|i: int|
393            #![auto]
394            0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
395    }
396}
397
398// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
399// so we specify that type here.
400#[verifier::external_type_specification]
401#[verifier::external_body]
402#[verifier::accept_recursive_types(T)]
403pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
404
405// To allow reasoning about the "contents" of the slice iterator, without using
406// a prophecy, we need a function that gives us the underlying sequence of the original slice.
407pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<T>;
408
409impl <'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> {
410    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
411        true
412    }
413
414    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
415    uninterp spec fn will_return_none(&self) -> bool;
416    uninterp spec fn decrease(&self) -> Option<nat>;
417
418    open spec fn peek(&self, index: int) -> Option<Self::Item> {
419        if 0 <= index < into_iter_elts(*self).len() {
420            Some(&into_iter_elts(*self)[index])
421        } else {
422            None
423        }
424    }
425}
426
427pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>)
428    ensures
429        IteratorSpec::remaining(&iter) == s@.as_ref(),
430        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
431        IteratorSpec::decrease(&iter) is Some,
432;
433
434pub assume_specification<'a, T> [<&'a [T] as core::iter::IntoIterator>::into_iter] (s: &'a [T]) ->
435    (iter: Iter<'a, T>)
436    ensures
437        IteratorSpec::remaining(&iter) == s@.as_ref(),
438        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
439        IteratorSpec::decrease(&iter) is Some,
440;
441
442/***********************************************************************************************
443 * Definitions for `slice::IterMut` (the iterator behind `<[T]>::iter_mut` and `Vec::iter_mut`)
444 ***********************************************************************************************/
445#[verifier::external_type_specification]
446#[verifier::external_body]
447#[verifier::accept_recursive_types(T)]
448pub struct ExIterMut<'a, T: 'a>(IterMut<'a, T>);
449
450// See exampes/iterators/slice_iter_mut.rs for a verified implementation of this interface.
451// Any changes here should first be verified over there.
452impl<'a, T: 'a> super::iter::IteratorSpecImpl for IterMut<'a, T> {
453    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
454        true
455    }
456
457    #[verifier::prophetic]
458    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
459
460    open spec fn will_return_none(&self) -> bool { true }
461
462    uninterp spec fn decrease(&self) -> Option<nat>;
463
464    open spec fn peek(&self, index: int) -> Option<Self::Item> { None }
465}
466
467// Also covers `vec.iter_mut(), which reaches this slice fn through `Vec`'s `DerefMut`
468pub assume_specification<'a, T>[ <[T]>::iter_mut ](slice: &'a mut [T]) -> (iter: IterMut<'a, T>)
469    ensures
470        IteratorSpec::remaining(&iter).len() == old(slice)@.len() == final(slice)@.len(),
471        // Each yielded reference initially points at the corresponding element...
472        forall|i: int| #![trigger IteratorSpec::remaining(&iter)[i]]
473            0 <= i < old(slice)@.len() ==> *(IteratorSpec::remaining(&iter)[i]) == old(slice)@[i],
474        // ...and its eventual value flows back to the corresponding element.
475        forall|i: int|
476            #![trigger IteratorSpec::remaining(&iter)[i]]
477            #![trigger final(slice)@[i]]
478            0 <= i < old(slice)@.len() ==> *final(IteratorSpec::remaining(&iter)[i]) == final(slice)@[i],
479        IteratorSpec::obeys_prophetic_iter_laws(&iter),
480        IteratorSpec::will_return_none(&iter),
481        IteratorSpec::decrease(&iter) is Some,
482;
483
484pub assume_specification<T> [ <[T]>::first ](slice: &[T]) -> (res: Option<&T>)
485    ensures
486        slice.len() == 0 ==> res.is_none(),
487        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0]
488    no_unwind
489;
490
491pub assume_specification<T> [ <[T]>::last ](slice: &[T]) -> (res: Option<&T>)
492    ensures
493        slice.len() == 0 ==> res.is_none(),
494        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last()
495    no_unwind
496;
497
498#[doc(hidden)]
499pub assume_specification<T> [ <[T]>::first_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
500    ensures
501        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
502        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)[0]
503            && final(slice)@ == old(slice)@.update(0, *final(res.unwrap()))
504    no_unwind
505;
506
507#[doc(hidden)]
508pub assume_specification<T> [ <[T]>::last_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
509    ensures
510        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
511        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)@.last()
512            && final(slice)@ == old(slice)@.update(old(slice).len() - 1, *final(res.unwrap()))
513    no_unwind
514;
515
516pub assume_specification<T> [ <[T]>::split_at ](slice: &[T], mid: usize) -> (ret: (&[T], &[T]))
517    requires
518        0 <= mid <= slice.len(),
519    ensures
520        ret.0@ == slice@[..mid],
521        ret.1@ == slice@[mid..],
522    no_unwind
523;
524
525#[doc(hidden)]
526pub assume_specification<T> [ <[T]>::split_at_mut ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T]))
527    requires
528        0 <= mid <= slice.len(),
529    ensures
530        ret.0@ == old(slice)@[..mid],
531        ret.1@ == old(slice)@[mid..],
532        final(slice)@ == final(ret.0)@ + final(ret.1)@,
533    no_unwind
534;
535
536// The non-panicking (`Option`-returning) form of `split_at`: `Some((a, b))` split at `mid`
537// when `mid <= len`, else `None`.
538pub assume_specification<T> [ <[T]>::split_at_checked ](slice: &[T], mid: usize) -> (ret: Option<(&[T], &[T])>)
539    ensures
540        mid <= slice.len() ==> (ret matches Some((a, b))
541            && a@ == slice@[..mid]
542            && b@ == slice@[mid..]),
543        mid > slice.len() ==> ret is None,
544    no_unwind
545;
546
547pub assume_specification<T> [ <[T]>::split_first ](slice: &[T]) -> (ret: Option<(&T, &[T])>)
548    ensures
549        slice.len() == 0 ==> ret.is_none(),
550        slice.len() > 0 ==> (ret matches Some((a, b)) && a == slice[0] && b@ == slice@[1..])
551    no_unwind
552;
553
554pub assume_specification<T> [ <[T]>::split_first_mut ](slice: &mut [T]) -> (ret: Option<(&mut T, &mut [T])>)
555    ensures
556        old(slice).len() == 0 ==> ret.is_none() && final(slice)@ == seq![],
557        old(slice).len() > 0 ==> (ret matches Some((a, b))
558            && *a == old(slice)[0]
559            && b@ == old(slice)@[1..]
560            && b@.len() == final(b)@.len()
561            && final(slice)@ == seq![*final(a)] + final(b)@
562        )
563    no_unwind
564;
565
566/// Copy the contents of `src` into `dst`, which must have the same length.
567pub assume_specification<T: Copy>[ <[T]>::copy_from_slice ](dst: &mut [T], src: &[T])
568    requires
569        old(dst)@.len() == src@.len(),
570    ensures
571        final(dst)@ == src@,
572;
573
574/// The sequence resulting from copying `old_slice[src_start..src_end]` to start
575/// at index `dest`, leaving all other positions unchanged. Reads are taken from
576/// `old_slice`, so overlapping source and destination ranges are handled like
577/// std's `<[T]>::copy_within` (which uses `ptr::copy`).
578pub open spec fn copy_within_result<T>(
579    old_slice: Seq<T>,
580    src_start: int,
581    src_end: int,
582    dest: int,
583) -> Seq<T> {
584    let count = src_end - src_start;
585    Seq::new(
586        old_slice.len(),
587        |i: int|
588            if dest <= i && i < dest + count {
589                old_slice[src_start + (i - dest)]
590            } else {
591                old_slice[i]
592            },
593    )
594}
595
596/// Copy the elements in range `src` within the slice to start at index `dest`.
597pub assume_specification<T: Copy, R: core::ops::RangeBounds<usize>>[ <[T]>::copy_within::<R> ](
598    slice: &mut [T],
599    src: R,
600    dest: usize,
601)
602    requires
603        slice_range_valid(&src, old(slice)@.len()),
604        (dest as int) + (slice_range_end(&src, old(slice)@.len()) - slice_range_start(&src))
605            <= old(slice)@.len(),
606    ensures
607        final(slice)@ == copy_within_result(
608            old(slice)@,
609            slice_range_start(&src),
610            slice_range_end(&src, old(slice)@.len()),
611            dest as int,
612        ),
613;
614
615} // verus!
vstd/std_specs/slice.rs

vstd/std_specs/
slice.rs
