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::{slice_range_end, slice_range_start, slice_range_valid};
6
7use core::ops::{
8    Index, IndexMut, Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive,
9};
10use core::slice::{Iter, SliceIndex};
11
12use verus as verus_;
13
14verus_! {
15
16impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for usize {
17    open spec fn in_bounds(&self, slice: &[T]) -> bool {
18        *self < slice@.len()
19    }
20}
21
22pub assume_specification<T>[ <usize as SliceIndex<[T]>>::get ](i: usize, slice: &[T]) -> Option<&T>;
23
24pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index ](i: usize, slice: &[T]) -> &T
25    returns
26        slice@[i as int],
27;
28
29pub assume_specification<T>[ <usize as SliceIndex<[T]>>::get_mut ](i: usize, slice: &mut [T]) -> Option<&mut T>;
30
31pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index_mut ](i: usize, slice: &mut [T]) -> (output: &mut T)
32    ensures
33        *output == old(slice)@[i as int],
34        final(slice)@ == old(slice)@.update(i as int, *final(output))
35;
36
37impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for Range<usize> {
38    open spec fn in_bounds(&self, slice: &[T]) -> bool {
39        &&& self.start <= self.end
40        &&& self.end <= slice@.len()
41    }
42}
43
44pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::get ](i: Range<usize>, slice: &[T]) -> Option<&[T]>;
45
46pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index ](i: Range<usize>, slice: &[T]) -> (r: &[T])
47    ensures
48        r@ == slice@.subrange(i.start as int, i.end as int),
49;
50
51pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::get_mut ](i: Range<usize>, slice: &mut [T]) -> Option<&mut [T]>;
52
53pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index_mut ](i: Range<usize>, slice: &mut [T]) -> (r: &mut [T])
54    ensures
55        r@ == old(slice)@.subrange(i.start as int, i.end as int),
56        final(r)@ == final(slice)@.subrange(i.start as int, i.end as int),
57        final(slice)@ == old(slice)@.subrange(0, i.start as int) + final(r)@ + old(slice)@.subrange(
58            i.end as int,
59            old(slice)@.len() as int,
60        ),
61;
62
63impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeTo<usize> {
64    open spec fn in_bounds(&self, slice: &[T]) -> bool {
65        self.end <= slice@.len()
66    }
67}
68
69pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::get ](i: RangeTo<usize>, slice: &[T]) -> Option<&[T]>;
70
71pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::index ](i: RangeTo<usize>, slice: &[T]) -> (r: &[T])
72    ensures
73        r@ == slice@.subrange(0, i.end as int),
74;
75
76pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::get_mut ](i: RangeTo<usize>, slice: &mut [T]) -> Option<&mut [T]>;
77
78pub assume_specification<T>[ <RangeTo<usize> as SliceIndex<[T]>>::index_mut ](i: RangeTo<usize>, slice: &mut [T]) -> (r: &mut [T])
79    ensures
80        r@ == old(slice)@.subrange(0, i.end as int),
81        final(r)@ == final(slice)@.subrange(0, i.end as int),
82        final(slice)@ == final(r)@ + old(slice)@.subrange(i.end as int, old(slice)@.len() as int),
83;
84
85impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeFrom<usize> {
86    open spec fn in_bounds(&self, slice: &[T]) -> bool {
87        self.start <= slice@.len()
88    }
89}
90
91pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::get ](i: RangeFrom<usize>, slice: &[T]) -> Option<&[T]>;
92
93pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::index ](i: RangeFrom<usize>, slice: &[T]) -> (r: &[T])
94    ensures
95        r@ == slice@.subrange(i.start as int, slice@.len() as int),
96;
97
98pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::get_mut ](i: RangeFrom<usize>, slice: &mut [T]) -> Option<&mut [T]>;
99
100pub assume_specification<T>[ <RangeFrom<usize> as SliceIndex<[T]>>::index_mut ](i: RangeFrom<usize>, slice: &mut [T]) -> (r: &mut [T])
101    ensures
102        r@ == old(slice)@.subrange(i.start as int, old(slice)@.len() as int),
103        final(r)@ == final(slice)@.subrange(i.start as int, old(slice)@.len() as int),
104        final(slice)@ == old(slice)@.subrange(0, i.start as int) + final(r)@,
105;
106
107// starts_with
108pub open spec fn spec_slice_starts_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool {
109    &&& needle@.len() <= slice@.len()
110    &&& forall|i: int| #![auto]
111        0 <= i < needle@.len() ==>
112            <T as super::cmp::PartialEqSpec<T>>::eq_spec(
113                &slice@[i],
114                &needle@[i],
115            )
116}
117
118#[verifier::when_used_as_spec(spec_slice_starts_with)]
119pub assume_specification<T: PartialEq>[ <[T]>::starts_with ](
120    slice: &[T],
121    needle: &[T],
122) -> (result: bool)
123    ensures
124        needle@.len() > slice@.len() ==> !result,
125        <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_starts_with(
126            slice,
127            needle,
128        )),
129;
130
131// ends_with
132pub open spec fn spec_slice_ends_with<T: PartialEq>(slice: &[T], needle: &[T]) -> bool {
133    &&& needle@.len() <= slice@.len()
134    &&& forall|i: int| #![auto]
135        0 <= i < needle@.len() ==>
136            <T as super::cmp::PartialEqSpec<T>>::eq_spec(
137                &slice@[slice@.len() - needle@.len() + i],
138                &needle@[i],
139            )
140}
141
142#[verifier::when_used_as_spec(spec_slice_ends_with)]
143pub assume_specification<T: PartialEq>[ <[T]>::ends_with ](
144    slice: &[T],
145    needle: &[T],
146) -> (result: bool)
147    ensures
148        needle@.len() > slice@.len() ==> !result,
149        <T as super::cmp::PartialEqSpec<T>>::obeys_eq_spec() ==> (result == spec_slice_ends_with(
150            slice,
151            needle,
152        )),
153;
154
155impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeToInclusive<usize> {
156    open spec fn in_bounds(&self, slice: &[T]) -> bool {
157        self.end < slice@.len()
158    }
159}
160
161pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::get ](i: RangeToInclusive<usize>, slice: &[T]) -> Option<&[T]>;
162
163pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::index ](i: RangeToInclusive<usize>, slice: &[T]) -> (r: &[T])
164    ensures
165        r@ == slice@.subrange(0, i.end as int + 1),
166;
167
168pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::get_mut ](i: RangeToInclusive<usize>, slice: &mut [T]) -> Option<&mut [T]>;
169
170pub assume_specification<T>[ <RangeToInclusive<usize> as SliceIndex<[T]>>::index_mut ](i: RangeToInclusive<usize>, slice: &mut [T]) -> (r: &mut [T])
171    ensures
172        r@ == old(slice)@.subrange(0, i.end as int + 1),
173        final(r)@ == final(slice)@.subrange(0, i.end as int + 1),
174        final(slice)@ == final(r)@ + old(slice)@.subrange(i.end as int + 1, old(slice)@.len() as int),
175;
176
177impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeFull {
178    open spec fn in_bounds(&self, slice: &[T]) -> bool {
179        true
180    }
181}
182
183pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::get ](i: RangeFull, slice: &[T]) -> Option<&[T]>;
184
185pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::index ](i: RangeFull, slice: &[T]) -> (r: &[T])
186    ensures
187        r@ == slice@,
188;
189
190pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::get_mut ](i: RangeFull, slice: &mut [T]) -> Option<&mut [T]>;
191
192pub assume_specification<T>[ <RangeFull as SliceIndex<[T]>>::index_mut ](i: RangeFull, slice: &mut [T]) -> (r: &mut [T])
193    ensures
194        r@ == old(slice)@,
195        final(slice)@ == final(r)@,
196;
197
198impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for RangeInclusive<usize> {
199    open spec fn in_bounds(&self, slice: &[T]) -> bool {
200        slice_range_valid(self, slice@.len())
201    }
202}
203
204pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::get ](i: RangeInclusive<usize>, slice: &[T]) -> Option<&[T]>;
205
206pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::index ](i: RangeInclusive<usize>, slice: &[T]) -> (r: &[T])
207    ensures
208        r@ == slice@.subrange(slice_range_start(&i), slice_range_end(&i, slice@.len() as nat)),
209;
210
211pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::get_mut ](i: RangeInclusive<usize>, slice: &mut [T]) -> Option<&mut [T]>;
212
213pub assume_specification<T>[ <RangeInclusive<usize> as SliceIndex<[T]>>::index_mut ](i: RangeInclusive<usize>, slice: &mut [T]) -> (r: &mut [T])
214    ensures
215        r@ == old(slice)@.subrange(
216            slice_range_start(&i),
217            slice_range_end(&i, old(slice)@.len() as nat),
218        ),
219        final(r)@ == final(slice)@.subrange(
220            slice_range_start(&i),
221            slice_range_end(&i, old(slice)@.len() as nat),
222        ),
223        final(slice)@ == old(slice)@.subrange(0, slice_range_start(&i)) + final(r)@
224            + old(slice)@.subrange(
225                slice_range_end(&i, old(slice)@.len() as nat),
226                old(slice)@.len() as int,
227            ),
228;
229
230impl<T, I: SliceIndex<[T]>> super::core::IndexSpecImpl<I> for [T] {
231    open spec fn index_req(&self, index: &I) -> bool {
232        index.in_bounds(self)
233    }
234}
235
236pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
237    &<I as SliceIndex<[T]>>::Output,
238>) where I: SliceIndex<[T]>
239    ensures
240        call_ensures(<I as SliceIndex<[T]>>::get, (i, slice), b),
241;
242
243pub assume_specification<T, I>[ <[T]>::get_mut::<I> ](slice: &mut [T], i: I) -> (b: Option<
244    &mut <I as SliceIndex<[T]>>::Output,
245>) where I: SliceIndex<[T]>
246    ensures
247        call_ensures(<I as SliceIndex<[T]>>::get_mut, (i, slice), b),
248;
249
250pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as Index<I>>::index ](
251    slice: &[T],
252    index: I,
253) -> (output: &<I as SliceIndex<[T]>>::Output)
254    ensures
255        call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),
256;
257
258pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as IndexMut<I>>::index_mut ](
259    slice: &mut [T],
260    index: I,
261) -> (output: &mut <I as SliceIndex<[T]>>::Output)
262    ensures
263        call_ensures(<I as SliceIndex<[T]>>::index_mut, (index, slice), output),
264;
265
266impl<T, I, const N: usize> super::core::IndexSpecImpl<I> for [T; N]
267where
268    [T]: Index<I>,
269{
270    open spec fn index_req(&self, index: &I) -> bool {
271        <[T] as IndexSpec<I>>::index_req(self, index)
272    }
273}
274
275pub assume_specification<T, I, const N: usize>[ <[T; N]>::index ](array: &[T; N], index: I) -> (output: &<[T; N] as Index<I>>::Output)
276    where
277        [T]: Index<I>,
278    ensures
279        call_ensures(<[T]>::index, (array, index), output),
280;
281
282pub 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)
283    where
284        [T]: IndexMut<I>,
285    ensures
286        exists|slice: &mut [T]| {
287            &&& #[trigger] slice@ == old(array)@
288            &&& final(slice)@ == final(array)@
289            &&& call_ensures(<[T]>::index_mut, (slice, index), output)
290        },
291;
292
293pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
294    requires
295        false,
296;
297
298// slice == slice
299pub assume_specification<T: PartialEq<U>, U>[ <[T] as PartialEq<[U]>>::eq ](
300    left: &[T],
301    right: &[U],
302) -> bool
303;
304
305impl<T, U> super::cmp::PartialEqSpecImpl<[U]> for [T] where T: PartialEq<U> + super::cmp::PartialEqSpec<U> {
306    open spec fn obeys_eq_spec() -> bool {
307        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
308    }
309
310    open spec fn eq_spec(&self, other: &[U]) -> bool {
311        &&& self@.len() == other@.len()
312        &&& forall|i: int|
313            #![auto]
314            0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
315    }
316}
317
318// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
319// so we specify that type here.
320#[verifier::external_type_specification]
321#[verifier::external_body]
322#[verifier::accept_recursive_types(T)]
323pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
324
325// To allow reasoning about the "contents" of the slice iterator, without using
326// a prophecy, we need a function that gives us the underlying sequence of the original slice.
327pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<T>;
328
329impl <'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> {
330    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
331        true
332    }
333
334    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
335    uninterp spec fn will_return_none(&self) -> bool;
336    uninterp spec fn decrease(&self) -> Option<nat>;
337
338    open spec fn peek(&self, index: int) -> Option<Self::Item> {
339        if 0 <= index < into_iter_elts(*self).len() {
340            Some(&into_iter_elts(*self)[index])
341        } else {
342            None
343        }
344    }
345}
346
347pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>)
348    ensures
349        IteratorSpec::remaining(&iter) == s@.as_ref(),
350        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
351        IteratorSpec::decrease(&iter) is Some,
352;
353
354pub assume_specification<'a, T> [<&'a [T] as core::iter::IntoIterator>::into_iter] (s: &'a [T]) ->
355    (iter: Iter<'a, T>)
356    ensures
357        IteratorSpec::remaining(&iter) == s@.as_ref(),
358        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
359        IteratorSpec::decrease(&iter) is Some,
360;
361
362pub assume_specification<T> [ <[T]>::first ](slice: &[T]) -> (res: Option<&T>)
363    ensures
364        slice.len() == 0 ==> res.is_none(),
365        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0]
366;
367
368pub assume_specification<T> [ <[T]>::last ](slice: &[T]) -> (res: Option<&T>)
369    ensures
370        slice.len() == 0 ==> res.is_none(),
371        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last()
372;
373
374#[doc(hidden)]
375pub assume_specification<T> [ <[T]>::first_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
376    ensures
377        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
378        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)[0]
379            && final(slice)@ == old(slice)@.update(0, *final(res.unwrap()))
380;
381
382#[doc(hidden)]
383pub assume_specification<T> [ <[T]>::last_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
384    ensures
385        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
386        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)@.last()
387            && final(slice)@ == old(slice)@.update(old(slice).len() - 1, *final(res.unwrap()))
388;
389
390pub assume_specification<T> [ <[T]>::split_at ](slice: &[T], mid: usize) -> (ret: (&[T], &[T]))
391    requires
392        0 <= mid <= slice.len(),
393    ensures
394        ret.0@ == slice@.subrange(0, mid as int),
395        ret.1@ == slice@.subrange(mid as int, slice@.len() as int),
396;
397
398#[doc(hidden)]
399pub assume_specification<T> [ <[T]>::split_at_mut ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T]))
400    requires
401        0 <= mid <= slice.len(),
402    ensures
403        ret.0@ == old(slice)@.subrange(0, mid as int),
404        ret.1@ == old(slice)@.subrange(mid as int, old(slice)@.len() as int),
405        final(slice)@ == final(ret.0)@ + final(ret.1)@,
406;
407
408// The non-panicking (`Option`-returning) form of `split_at`: `Some((a, b))` split at `mid`
409// when `mid <= len`, else `None`.
410pub assume_specification<T> [ <[T]>::split_at_checked ](slice: &[T], mid: usize) -> (ret: Option<(&[T], &[T])>)
411    ensures
412        mid <= slice.len() ==> (ret matches Some((a, b))
413            && a@ == slice@.subrange(0, mid as int)
414            && b@ == slice@.subrange(mid as int, slice@.len() as int)),
415        mid > slice.len() ==> ret is None,
416;
417
418/// Copy the contents of `src` into `dst`, which must have the same length.
419pub assume_specification<T: Copy>[ <[T]>::copy_from_slice ](dst: &mut [T], src: &[T])
420    requires
421        old(dst)@.len() == src@.len(),
422    ensures
423        final(dst)@ == src@,
424;
425
426/// The sequence resulting from copying `old_slice[src_start..src_end]` to start
427/// at index `dest`, leaving all other positions unchanged. Reads are taken from
428/// `old_slice`, so overlapping source and destination ranges are handled like
429/// std's `<[T]>::copy_within` (which uses `ptr::copy`).
430pub open spec fn copy_within_result<T>(
431    old_slice: Seq<T>,
432    src_start: int,
433    src_end: int,
434    dest: int,
435) -> Seq<T> {
436    let count = src_end - src_start;
437    Seq::new(
438        old_slice.len(),
439        |i: int|
440            if dest <= i && i < dest + count {
441                old_slice[src_start + (i - dest)]
442            } else {
443                old_slice[i]
444            },
445    )
446}
447
448/// Copy the elements in range `src` within the slice to start at index `dest`.
449pub assume_specification<T: Copy, R: core::ops::RangeBounds<usize>>[ <[T]>::copy_within::<R> ](
450    slice: &mut [T],
451    src: R,
452    dest: usize,
453)
454    requires
455        slice_range_valid(&src, old(slice)@.len()),
456        (dest as int) + (slice_range_end(&src, old(slice)@.len()) - slice_range_start(&src))
457            <= old(slice)@.len(),
458    ensures
459        final(slice)@ == copy_within_result(
460            old(slice)@,
461            slice_range_start(&src),
462            slice_range_end(&src, old(slice)@.len()),
463            dest as int,
464        ),
465;
466
467} // verus!
vstd/std_specs/slice.rs

vstd/std_specs/
slice.rs
