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

vstd/std_specs/
slice.rs
