vstd/std_specs/
slice.rs

1use super::super::prelude::*;
2use super::super::slice::SliceIndexSpec;
3use super::core::{IndexSetTrustedSpec, IndexSpec, TrustedSpecSealed};
4
5use core::ops::{Index, Range};
6use core::slice::{Iter, SliceIndex};
7
8use verus as verus_;
9
10verus_! {
11
12impl<T, const N: usize> TrustedSpecSealed for [T; N] {}
13
14impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N] {
15    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
16        0 <= index < N
17    }
18
19    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
20        new_container@ === self@.update(index as int, val)
21    }
22}
23
24impl<T> TrustedSpecSealed for [T] {}
25
26impl<T> IndexSetTrustedSpec<usize> for [T] {
27    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
28        0 <= index < self@.len()
29    }
30
31    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
32        new_container@ == self@.update(index as int, val)
33    }
34}
35
36impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for usize {
37    open spec fn index_req(&self, slice: &[T]) -> bool {
38        *self < slice@.len()
39    }
40}
41
42pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index ](i: usize, slice: &[T]) -> &T
43    returns
44        slice@[i as int],
45;
46
47impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for Range<usize> {
48    open spec fn index_req(&self, slice: &[T]) -> bool {
49        &&& self.start <= self.end
50        &&& self.end <= slice@.len()
51    }
52}
53
54pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index ](i: Range<usize>, slice: &[T]) -> (r: &[T])
55    ensures
56        r@ == slice@.subrange(i.start as int, i.end as int),
57;
58
59impl<T, I: SliceIndex<[T]>> super::core::IndexSpecImpl<I> for [T] {
60    open spec fn index_req(&self, index: &I) -> bool {
61        index.index_req(self)
62    }
63}
64
65impl<T, I, const N: usize> super::core::IndexSpecImpl<I> for [T; N]
66    where [T]: Index<I>
67{
68    open spec fn index_req(&self, index: &I) -> bool {
69        <[T] as IndexSpec<I>>::index_req(self, index)
70    }
71}
72
73pub assume_specification<T, I: SliceIndex<[T]>> [<[T] as Index<I>>::index] (
74    slice: &[T],
75    index: I,
76) -> (output: &<I as core::slice::SliceIndex<[T]>>::Output)
77    ensures
78        call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),
79;
80
81pub assume_specification<T, I, const N: usize> [<[T; N] as Index<I>>::index] (
82    array: &[T; N],
83    index: I,
84) -> (output: &<[T; N] as core::ops::Index<I>>::Output)
85    where [T]: Index<I>,
86    ensures
87        call_ensures(<[T] as Index<I>>::index, (array, index), output),
88;
89
90pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
91    requires
92        false,
93;
94
95// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
96// so we specify that type here.
97#[verifier::external_type_specification]
98#[verifier::external_body]
99#[verifier::accept_recursive_types(T)]
100pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
101
102impl<T> View for Iter<'_, T> {
103    type V = (int, Seq<T>);
104
105    uninterp spec fn view(&self) -> (int, Seq<T>);
106}
107
108impl<T: DeepView> DeepView for Iter<'_, T> {
109    type V = (int, Seq<T::V>);
110
111    open spec fn deep_view(&self) -> Self::V {
112        let (i, v) = self@;
113        (i, Seq::new(v.len(), |i: int| v[i].deep_view()))
114    }
115}
116
117pub assume_specification<'a, T>[ Iter::<'a, T>::next ](elements: &mut Iter<'a, T>) -> (r: Option<
118    &'a T,
119>)
120    ensures
121        ({
122            let (old_index, old_seq) = old(elements)@;
123            match r {
124                None => {
125                    &&& elements@ == old(elements)@
126                    &&& old_index >= old_seq.len()
127                },
128                Some(element) => {
129                    let (new_index, new_seq) = elements@;
130                    &&& 0 <= old_index < old_seq.len()
131                    &&& new_seq == old_seq
132                    &&& new_index == old_index + 1
133                    &&& element == old_seq[old_index]
134                },
135            }
136        }),
137;
138
139pub struct IterGhostIterator<'a, T> {
140    pub pos: int,
141    pub elements: Seq<T>,
142    pub phantom: Option<&'a T>,
143}
144
145impl<'a, T> super::super::pervasive::ForLoopGhostIteratorNew for Iter<'a, T> {
146    type GhostIter = IterGhostIterator<'a, T>;
147
148    open spec fn ghost_iter(&self) -> IterGhostIterator<'a, T> {
149        IterGhostIterator { pos: self@.0, elements: self@.1, phantom: None }
150    }
151}
152
153impl<'a, T: 'a> super::super::pervasive::ForLoopGhostIterator for IterGhostIterator<'a, T> {
154    type ExecIter = Iter<'a, T>;
155
156    type Item = T;
157
158    type Decrease = int;
159
160    open spec fn exec_invariant(&self, exec_iter: &Iter<'a, T>) -> bool {
161        &&& self.pos == exec_iter@.0
162        &&& self.elements == exec_iter@.1
163    }
164
165    open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool {
166        init matches Some(init) ==> {
167            &&& init.pos == 0
168            &&& init.elements == self.elements
169            &&& 0 <= self.pos <= self.elements.len()
170        }
171    }
172
173    open spec fn ghost_ensures(&self) -> bool {
174        self.pos == self.elements.len()
175    }
176
177    open spec fn ghost_decrease(&self) -> Option<int> {
178        Some(self.elements.len() - self.pos)
179    }
180
181    open spec fn ghost_peek_next(&self) -> Option<T> {
182        if 0 <= self.pos < self.elements.len() {
183            Some(self.elements[self.pos])
184        } else {
185            None
186        }
187    }
188
189    open spec fn ghost_advance(&self, _exec_iter: &Iter<'a, T>) -> IterGhostIterator<'a, T> {
190        Self { pos: self.pos + 1, ..*self }
191    }
192}
193
194impl<'a, T> View for IterGhostIterator<'a, T> {
195    type V = Seq<T>;
196
197    open spec fn view(&self) -> Seq<T> {
198        self.elements.take(self.pos)
199    }
200}
201
202// To allow reasoning about the ghost iterator when the executable
203// function `iter()` is invoked in a `for` loop header (e.g., in
204// `for x in it: s.iter() { ... }`), we need to specify the behavior of
205// the iterator in spec mode. To do that, we add
206// `#[verifier::when_used_as_spec(spec_slice_iter)` to the specification for
207// the executable `into_iter` method and define that spec function here.
208pub uninterp spec fn spec_slice_iter<'a, T>(s: &'a [T]) -> (iter: Iter<'a, T>);
209
210pub broadcast proof fn axiom_spec_slice_iter<'a, T>(s: &'a [T])
211    ensures
212        (#[trigger] spec_slice_iter(s))@ == (0int, s@),
213{
214    admit();
215}
216
217#[verifier::when_used_as_spec(spec_slice_iter)]
218pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>)
219    ensures
220        ({
221            let (index, seq) = iter@;
222            &&& index == 0
223            &&& seq == s@
224        }),
225;
226
227pub assume_specification<T> [ <[T]>::first ](slice: &[T]) -> (res: Option<&T>)
228    ensures
229        slice.len() == 0 ==> res.is_none(),
230        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0]
231;
232
233pub assume_specification<T> [ <[T]>::last ](slice: &[T]) -> (res: Option<&T>)
234    ensures
235        slice.len() == 0 ==> res.is_none(),
236        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last()
237;
238
239#[doc(hidden)]
240#[verifier::ignore_outside_new_mut_ref_experiment]
241pub assume_specification<T> [ <[T]>::first_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
242    ensures
243        old(slice).len() == 0 ==> res.is_none() && final(slice)@ === seq![],
244        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)[0]
245            && final(slice)@ === old(slice)@.update(0, *final(res.unwrap()))
246;
247
248#[doc(hidden)]
249#[verifier::ignore_outside_new_mut_ref_experiment]
250pub assume_specification<T> [ <[T]>::last_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
251    ensures
252        old(slice).len() == 0 ==> res.is_none() && final(slice)@ === seq![],
253        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)@.last()
254            && final(slice)@ === old(slice)@.update(old(slice).len() - 1, *final(res.unwrap()))
255;
256
257pub assume_specification<T> [ <[T]>::split_at ](slice: &[T], mid: usize) -> (ret: (&[T], &[T]))
258    requires
259        0 <= mid <= slice.len(),
260    ensures
261        ret.0@ == slice@.subrange(0, mid as int),
262        ret.1@ == slice@.subrange(mid as int, slice@.len() as int),
263;
264
265#[doc(hidden)]
266#[verifier::ignore_outside_new_mut_ref_experiment]
267pub assume_specification<T> [ <[T]>::split_at_mut ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T]))
268    requires
269        0 <= mid <= slice.len(),
270    ensures
271        ret.0@ == old(slice)@.subrange(0, mid as int),
272        ret.1@ == old(slice)@.subrange(mid as int, old(slice)@.len() as int),
273        final(slice)@ == final(ret.0)@ + final(ret.1)@,
274;
275
276pub broadcast group group_slice_axioms {
277    axiom_spec_slice_iter,
278}
279
280} // verus!
vstd/std_specs/slice.rs

vstd/std_specs/
slice.rs
