vstd/std_specs/
slice.rs

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

vstd/std_specs/
slice.rs
