vstd/std_specs/
slice.rs

1use super::super::prelude::*;
2use super::super::slice::SliceIndexSpec;
3use super::core::{IndexSetTrustedSpec, IndexSpec, TrustedSpecSealed};
4use super::iter::IteratorSpec;
5
6use core::ops::{Index, Range};
7use core::slice::{Iter, SliceIndex};
8
9use verus as verus_;
10
11verus_! {
12
13impl<T, const N: usize> TrustedSpecSealed for [T; N] {}
14
15impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N] {
16    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
17        0 <= index < N
18    }
19
20    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
21        new_container@ == self@.update(index as int, val)
22    }
23}
24
25impl<T> TrustedSpecSealed for [T] {}
26
27impl<T> IndexSetTrustedSpec<usize> for [T] {
28    open spec fn spec_index_set_requires(&self, index: usize) -> bool {
29        0 <= index < self@.len()
30    }
31
32    open spec fn spec_index_set_ensures(&self, new_container: &Self, index: usize, val: T) -> bool {
33        new_container@ == self@.update(index as int, val)
34    }
35}
36
37impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for usize {
38    open spec fn index_req(&self, slice: &[T]) -> bool {
39        *self < slice@.len()
40    }
41}
42
43pub assume_specification<T>[ <usize as SliceIndex<[T]>>::index ](i: usize, slice: &[T]) -> &T
44    returns
45        slice@[i as int],
46;
47
48impl<T> super::super::slice::SliceIndexSpecImpl<[T]> for Range<usize> {
49    open spec fn index_req(&self, slice: &[T]) -> bool {
50        &&& self.start <= self.end
51        &&& self.end <= slice@.len()
52    }
53}
54
55pub assume_specification<T>[ <Range<usize> as SliceIndex<[T]>>::index ](i: Range<usize>, slice: &[T]) -> (r: &[T])
56    ensures
57        r@ == slice@.subrange(i.start as int, i.end as int),
58;
59
60impl<T, I: SliceIndex<[T]>> super::core::IndexSpecImpl<I> for [T] {
61    open spec fn index_req(&self, index: &I) -> bool {
62        index.index_req(self)
63    }
64}
65
66impl<T, I, const N: usize> super::core::IndexSpecImpl<I> for [T; N]
67    where [T]: Index<I>
68{
69    open spec fn index_req(&self, index: &I) -> bool {
70        <[T] as IndexSpec<I>>::index_req(self, index)
71    }
72}
73
74pub assume_specification<T, I: SliceIndex<[T]>> [<[T] as Index<I>>::index] (
75    slice: &[T],
76    index: I,
77) -> (output: &<I as core::slice::SliceIndex<[T]>>::Output)
78    ensures
79        call_ensures(<I as SliceIndex<[T]>>::index, (index, slice), output),
80;
81
82pub assume_specification<T, I, const N: usize> [<[T; N] as Index<I>>::index] (
83    array: &[T; N],
84    index: I,
85) -> (output: &<[T; N] as core::ops::Index<I>>::Output)
86    where [T]: Index<I>,
87    ensures
88        call_ensures(<[T] as Index<I>>::index, (array, index), output),
89;
90
91pub assume_specification[ core::hint::unreachable_unchecked ]() -> !
92    requires
93        false,
94;
95
96// The `iter` method of a `<T>` returns an iterator of type `Iter<'_, T>`,
97// so we specify that type here.
98#[verifier::external_type_specification]
99#[verifier::external_body]
100#[verifier::accept_recursive_types(T)]
101pub struct ExIter<'a, T: 'a>(Iter<'a, T>);
102
103// To allow reasoning about the "contents" of the slice iterator, without using
104// a prophecy, we need a function that gives us the underlying sequence of the original slice.
105pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<T>;
106
107impl <'a, T: 'a> super::iter::IteratorSpecImpl for Iter<'a, T> {
108    open spec fn obeys_prophetic_iter_laws(&self) -> bool {
109        true
110    }
111
112    uninterp spec fn remaining(&self) -> Seq<Self::Item>;
113    uninterp spec fn will_return_none(&self) -> bool;
114
115    #[verifier::prophetic]
116    open spec fn initial_value_relation(&self, init: &Self) -> bool {
117        &&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self)
118        &&& into_iter_elts(*self) == IteratorSpec::remaining(self).unref()
119    }
120
121    uninterp spec fn decrease(&self) -> Option<nat>;
122
123    open spec fn peek(&self, index: int) -> Option<Self::Item> {
124        if 0 <= index < into_iter_elts(*self).len() {
125            Some(&into_iter_elts(*self)[index])
126        } else {
127            None
128        }
129    }
130}
131
132
133// To allow reasoning about the returned iterator when the executable
134// function `iter()` is invoked in a `for` loop header (e.g., in
135// `for x in it: s.iter() { ... }`), we need to specify the behavior of
136// the iterator in spec mode. To do that, we add
137// `#[verifier::when_used_as_spec(spec_slice_iter)` to the specification for
138// the executable `into_iter` method and define that spec function here.
139pub uninterp spec fn spec_slice_iter<'a, T>(s: &'a [T]) -> (iter: Iter<'a, T>);
140
141pub broadcast proof fn axiom_spec_slice_iter<'a, T>(s: &'a [T])
142    ensures
143        #[trigger] spec_slice_iter(s).remaining() == s@.as_ref(),
144{
145    admit();
146}
147
148#[verifier::when_used_as_spec(spec_slice_iter)]
149pub assume_specification<'a, T>[ <[T]>::iter ](s: &'a [T]) -> (iter: Iter<'a, T>)
150    ensures
151        iter == spec_slice_iter(s),
152        IteratorSpec::decrease(&iter) is Some,
153        IteratorSpec::initial_value_relation(&iter, &iter),
154;
155
156#[verifier::when_used_as_spec(spec_slice_iter)]
157pub assume_specification<'a, T> [<&'a [T] as core::iter::IntoIterator>::into_iter] (s: &'a [T]) ->
158    (iter: Iter<'a, T>)
159    ensures
160        iter == spec_slice_iter(s),
161        IteratorSpec::decrease(&iter) is Some,
162        IteratorSpec::initial_value_relation(&iter, &iter),
163;
164
165pub assume_specification<T> [ <[T]>::first ](slice: &[T]) -> (res: Option<&T>)
166    ensures
167        slice.len() == 0 ==> res.is_none(),
168        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice[0]
169;
170
171pub assume_specification<T> [ <[T]>::last ](slice: &[T]) -> (res: Option<&T>)
172    ensures
173        slice.len() == 0 ==> res.is_none(),
174        slice.len() != 0 ==> res.is_some() && res.unwrap() == slice@.last()
175;
176
177#[doc(hidden)]
178pub assume_specification<T> [ <[T]>::first_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
179    ensures
180        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
181        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)[0]
182            && final(slice)@ == old(slice)@.update(0, *final(res.unwrap()))
183;
184
185#[doc(hidden)]
186pub assume_specification<T> [ <[T]>::last_mut ](slice: &mut [T]) -> (res: Option<&mut T>)
187    ensures
188        old(slice).len() == 0 ==> res.is_none() && final(slice)@ == seq![],
189        old(slice).len() != 0 ==> res.is_some() && *res.unwrap() == old(slice)@.last()
190            && final(slice)@ == old(slice)@.update(old(slice).len() - 1, *final(res.unwrap()))
191;
192
193pub assume_specification<T> [ <[T]>::split_at ](slice: &[T], mid: usize) -> (ret: (&[T], &[T]))
194    requires
195        0 <= mid <= slice.len(),
196    ensures
197        ret.0@ == slice@.subrange(0, mid as int),
198        ret.1@ == slice@.subrange(mid as int, slice@.len() as int),
199;
200
201#[doc(hidden)]
202pub assume_specification<T> [ <[T]>::split_at_mut ](slice: &mut [T], mid: usize) -> (ret: (&mut [T], &mut [T]))
203    requires
204        0 <= mid <= slice.len(),
205    ensures
206        ret.0@ == old(slice)@.subrange(0, mid as int),
207        ret.1@ == old(slice)@.subrange(mid as int, old(slice)@.len() as int),
208        final(slice)@ == final(ret.0)@ + final(ret.1)@,
209;
210
211pub broadcast group group_slice_axioms {
212    axiom_spec_slice_iter,
213}
214
215} // verus!
vstd/std_specs/slice.rs

vstd/std_specs/
slice.rs
