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::{Index, IndexMut, Range};
8use core::slice::{Iter, SliceIndex};
9
10use verus as verus_;
11
12verus_! {
13
14impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for usize {
15    open spec fn index_req(&self, slice: &[T]) -> bool {
16        *self < slice@.len()
17    }
18}
19
20pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index ](i: usize, slice: &[T]) -> &T
21    returns
22        slice@[i as int],
23;
24
25pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index_mut ](i: usize, slice: &mut [T]) -> (output: &mut T)
26    ensures
27        *output == old(slice)@[i as int],
28        final(slice)@ == old(slice)@.update(i as int, *final(output))
29;
30
31impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for Range<usize> {
32    open spec fn index_req(&self, slice: &[T]) -> bool {
33        &&& self.start <= self.end
34        &&& self.end <= slice@.len()
35    }
36}
37
38pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index ](i: Range<usize>, slice: &[T]) -> (r: &[T])
39    ensures
40        r@ == slice@.subrange(i.start as int, i.end as int),
41;
42
43pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index_mut ](i: Range<usize>, slice: &mut [T]) -> (r: &mut [T])
44    ensures
45        r@ == old(slice)@.subrange(i.start as int, i.end as int),
46        final(r)@ == final(slice)@.subrange(i.start as int, i.end as int),
47        forall|j: int| !(i.start <= j < i.end) ==> final(slice)@[j] == old(slice)@[j],
48;
49
50impl<T, I: SliceIndex<[T]>> super::core::IndexSpecImpl<I> for [T] {
51    open spec fn index_req(&self, index: &I) -> bool {
52        index.index_req(self)
53    }
54}
55
56pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as Index<I>>::index ](
57    slice: &[T],
58    index: I,
59) -> (output: &<I as SliceIndex<[T]>>::Output)
60    ensures
61        call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),
62;
63
64pub assume_specification<T, I: SliceIndex<[T]>>[ <[T] as IndexMut<I>>::index_mut ](
65    slice: &mut [T],
66    index: I,
67) -> (output: &mut <I as SliceIndex<[T]>>::Output)
68    ensures
69        call_ensures(<I as SliceIndex<[T]>>::index_mut, (index, slice), output),
70;
71
72impl<T, I, const N: usize> super::core::IndexSpecImpl<I> for [T; N]
73where
74    [T]: Index<I>,
75{
76    open spec fn index_req(&self, index: &I) -> bool {
77        <[T] as IndexSpec<I>>::index_req(self, index)
78    }
79}
80
81pub assume_specification<T, I, const N: usize>[ <[T; N]>::index ](array: &[T; N], index: I) -> (output: &<[T; N] as Index<I>>::Output)
82    where
83        [T]: Index<I>,
84    ensures
85        call_ensures(<[T]>::index, (array, index), output),
86;
87
88pub 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)
89    where
90        [T]: IndexMut<I>,
91    ensures
92        exists|slice: &mut [T]| {
93            &&& #[trigger] slice@ == old(array)@
94            &&& final(slice)@ == final(array)@
95            &&& call_ensures(<[T]>::index_mut, (slice, index), output)
96        },
97;
98
99pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
100    requires
101        false,
102;
103
104// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
105// so we specify that type here.
106#[verifier::external_type_specification]
107#[verifier::external_body]
108#[verifier::accept_recursive_types(T)]
109pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
110
111// To allow reasoning about the "contents" of the slice iterator, without using
112// a prophecy, we need a function that gives us the underlying sequence of the original slice.
113pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<T>;
114
115impl <'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> {
116    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
117        true
118    }
119
120    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
121    uninterp spec fn will_return_none(&self) -> bool;
122    uninterp spec fn decrease(&self) -> Option<nat>;
123
124    open spec fn peek(&self, index: int) -> Option<Self::Item> {
125        if 0 <= index < into_iter_elts(*self).len() {
126            Some(&into_iter_elts(*self)[index])
127        } else {
128            None
129        }
130    }
131}
132
133pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>)
134    ensures
135        IteratorSpec::remaining(&iter) == s@.as_ref(),
136        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
137        IteratorSpec::decrease(&iter) is Some,
138;
139
140pub assume_specification<'a, T> [<&'a [T] as core::iter::IntoIterator>::into_iter] (s: &'a [T]) ->
141    (iter: Iter<'a, T>)
142    ensures
143        IteratorSpec::remaining(&iter) == s@.as_ref(),
144        into_iter_elts(iter) == IteratorSpec::remaining(&iter).unref(),
145        IteratorSpec::decrease(&iter) is Some,
146;
147
148pub assume_specification<T> [ <[T]>::first ](slice: &[T]) -> (res: Option<&T>)
149    ensures
150        slice.len() == 0 ==> res.is_none(),
151        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0]
152;
153
154pub assume_specification<T> [ <[T]>::last ](slice: &[T]) -> (res: Option<&T>)
155    ensures
156        slice.len() == 0 ==> res.is_none(),
157        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last()
158;
159
160#[doc(hidden)]
161pub assume_specification<T> [ <[T]>::first_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
162    ensures
163        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
164        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)[0]
165            && final(slice)@ == old(slice)@.update(0, *final(res.unwrap()))
166;
167
168#[doc(hidden)]
169pub assume_specification<T> [ <[T]>::last_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
170    ensures
171        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
172        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)@.last()
173            && final(slice)@ == old(slice)@.update(old(slice).len() - 1, *final(res.unwrap()))
174;
175
176pub assume_specification<T> [ <[T]>::split_at ](slice: &[T], mid: usize) -> (ret: (&[T], &[T]))
177    requires
178        0 <= mid <= slice.len(),
179    ensures
180        ret.0@ == slice@.subrange(0, mid as int),
181        ret.1@ == slice@.subrange(mid as int, slice@.len() as int),
182;
183
184#[doc(hidden)]
185pub assume_specification<T> [ <[T]>::split_at_mut ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T]))
186    requires
187        0 <= mid <= slice.len(),
188    ensures
189        ret.0@ == old(slice)@.subrange(0, mid as int),
190        ret.1@ == old(slice)@.subrange(mid as int, old(slice)@.len() as int),
191        final(slice)@ == final(ret.0)@ + final(ret.1)@,
192;
193
194// The non-panicking (`Option`-returning) form of `split_at`: `Some((a, b))` split at `mid`
195// when `mid <= len`, else `None`.
196pub assume_specification<T> [ <[T]>::split_at_checked ](slice: &[T], mid: usize) -> (ret: Option<(&[T], &[T])>)
197    ensures
198        mid <= slice.len() ==> (ret matches Some((a, b))
199            && a@ == slice@.subrange(0, mid as int)
200            && b@ == slice@.subrange(mid as int, slice@.len() as int)),
201        mid > slice.len() ==> ret is None,
202;
203
204/// Copy the contents of `src` into `dst`, which must have the same length.
205pub assume_specification<T: Copy>[ <[T]>::copy_from_slice ](dst: &mut [T], src: &[T])
206    requires
207        old(dst)@.len() == src@.len(),
208    ensures
209        final(dst)@ == src@,
210;
211
212/// The sequence resulting from copying `old_slice[src_start..src_end]` to start
213/// at index `dest`, leaving all other positions unchanged. Reads are taken from
214/// `old_slice`, so overlapping source and destination ranges are handled like
215/// std's `<[T]>::copy_within` (which uses `ptr::copy`).
216pub open spec fn copy_within_result<T>(
217    old_slice: Seq<T>,
218    src_start: int,
219    src_end: int,
220    dest: int,
221) -> Seq<T> {
222    let count = src_end - src_start;
223    Seq::new(
224        old_slice.len(),
225        |i: int|
226            if dest <= i && i < dest + count {
227                old_slice[src_start + (i - dest)]
228            } else {
229                old_slice[i]
230            },
231    )
232}
233
234/// Copy the elements in range `src` within the slice to start at index `dest`.
235pub assume_specification<T: Copy, R: core::ops::RangeBounds<usize>>[ <[T]>::copy_within::<R> ](
236    slice: &mut [T],
237    src: R,
238    dest: usize,
239)
240    requires
241        slice_range_valid(&src, old(slice)@.len()),
242        (dest as int) + (slice_range_end(&src, old(slice)@.len()) - slice_range_start(&src))
243            <= old(slice)@.len(),
244    ensures
245        final(slice)@ == copy_within_result(
246            old(slice)@,
247            slice_range_start(&src),
248            slice_range_end(&src, old(slice)@.len()),
249            dest as int,
250        ),
251;
252
253} // verus!
vstd/std_specs/slice.rs

vstd/std_specs/
slice.rs
