vstd/std_specs/
slice.rs

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

vstd/std_specs/
slice.rs
