vstd/
slice.rs

1#![allow(unused_imports)]
2use super::prelude::*;
3use super::seq::*;
4use super::view::*;
5use core::slice::SliceIndex;
6
7#[cfg(verus_keep_ghost)]
8#[cfg(feature = "alloc")]
9pub use super::std_specs::vec::VecAdditionalSpecFns;
10
11verus! {
12
13impl<T> View for [T] {
14    type V = Seq<T>;
15
16    uninterp spec fn view(&self) -> Seq<T>;
17}
18
19impl<T: DeepView> DeepView for [T] {
20    type V = Seq<T::V>;
21
22    open spec fn deep_view(&self) -> Seq<T::V> {
23        let v = self.view();
24        Seq::new(v.len(), |i: int| v[i].deep_view())
25    }
26}
27
28pub trait SliceAdditionalSpecFns<T>: View<V = Seq<T>> {
29    spec fn spec_index(&self, i: int) -> T
30        recommends
31            0 <= i < self.view().len(),
32    ;
33}
34
35impl<T> SliceAdditionalSpecFns<T> for [T] {
36    #[verifier::inline]
37    open spec fn spec_index(&self, i: int) -> T {
38        self.view().index(i)
39    }
40}
41
42#[verifier::external]
43pub trait SliceAdditionalExecFns<T> {
44    #[cfg_attr(not(verus_verify_core), deprecated = "use `slice[i] = value` instead")]
45    fn set(&mut self, idx: usize, t: T);
46}
47
48impl<T> SliceAdditionalExecFns<T> for [T] {
49    #[verifier::external_body]
50    fn set(&mut self, idx: usize, t: T)
51        requires
52            0 <= idx < old(self)@.len(),
53        ensures
54            final(self)@ == old(self)@.update(idx as int, t),
55    {
56        self[idx] = t;
57    }
58}
59
60#[verifier::external_body]
61#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::slice_index_get")]
62pub exec fn slice_index_get<T>(slice: &[T], i: usize) -> (out: &T)
63    requires
64        0 <= i < slice.view().len(),
65    ensures
66        *out == slice@.index(i as int),
67{
68    &slice[i]
69}
70
71////// Len (with autospec)
72#[cfg_attr(all(verus_keep_ghost), rustc_diagnostic_item = "verus::vstd::slice::spec_slice_len")]
73pub uninterp spec fn spec_slice_len<T>(slice: &[T]) -> usize;
74
75// This axiom is slightly better than defining spec_slice_len to just be `slice@.len() as usize`
76// (the axiom also shows that slice@.len() is in-bounds for usize)
77pub broadcast axiom fn axiom_spec_len<T>(slice: &[T])
78    ensures
79        #[trigger] spec_slice_len(slice) == slice@.len(),
80;
81
82#[verifier::allow_in_spec]
83pub assume_specification<T>[ <[T]>::len ](slice: &[T]) -> (len: usize)
84    returns
85        spec_slice_len(slice),
86    opens_invariants none
87    no_unwind
88;
89
90pub open spec fn spec_slice_is_empty<T>(slice: &[T]) -> bool {
91    slice@.len() == 0
92}
93
94#[verifier::when_used_as_spec(spec_slice_is_empty)]
95pub assume_specification<T>[ <[T]>::is_empty ](slice: &[T]) -> (b: bool)
96    ensures
97        b <==> slice@.len() == 0,
98    opens_invariants none
99    no_unwind
100;
101
102#[cfg(feature = "alloc")]
103#[verifier::external_body]
104pub exec fn slice_to_vec<T: Copy>(slice: &[T]) -> (out: alloc::vec::Vec<T>)
105    ensures
106        out@ == slice@,
107{
108    // Not `slice.to_vec()`: since Rust 1.93, `to_vec` copies bitwise only for `TrivialClone`
109    // types and calls `Clone::clone` for a `Copy` type with a hand-written `Clone`.
110    slice.iter().copied().collect()
111}
112
113#[verifier::external_body]
114pub exec fn slice_subrange<T, 'a>(slice: &'a [T], i: usize, j: usize) -> (out: &'a [T])
115    requires
116        0 <= i <= j <= slice@.len(),
117    ensures
118        out@ == slice@[i..j],
119{
120    &slice[i..j]
121}
122
123#[verifier::external_trait_specification]
124#[verifier::external_trait_extension(SliceIndexSpec via SliceIndexSpecImpl)]
125pub trait ExSliceIndex<T> where T: ?Sized {
126    type ExternalTraitSpecificationFor: SliceIndex<T>;
127
128    type Output: ?Sized;
129
130    spec fn in_bounds(&self, slice: &T) -> bool;
131
132    spec fn index_postcondition(&self, slice: &T, r: &Self::Output) -> bool;
133
134    spec fn index_mut_postcondition(
135        &self,
136        old_slice: &T,
137        final_slice: &T,
138        immediate_output: &Self::Output,
139        final_output: &Self::Output,
140    ) -> bool;
141
142    fn index(self, slice: &T) -> (r: &Self::Output)
143        requires
144            self.in_bounds(slice),
145        ensures
146            self.index_postcondition(slice, r),
147    ;
148
149    fn index_mut(self, slice: &mut T) -> (r: &mut Self::Output)
150        requires
151            self.in_bounds(slice),
152        ensures
153            self.index_mut_postcondition(&*old(slice), &*final(slice), r, &*final(r)),
154    ;
155
156    fn get(self, slice: &T) -> (r: Option<&Self::Output>)
157        ensures
158            match r {
159                None => !self.in_bounds(slice),
160                Some(x) => self.in_bounds(slice) && self.index_postcondition(slice, x),
161            },
162    ;
163
164    fn get_mut(self, slice: &mut T) -> (r: Option<&mut Self::Output>)
165        ensures
166            match r {
167                None => !self.in_bounds(old(slice)) && &*final(slice) == &*old(slice),
168                Some(x) => {
169                    &&& self.in_bounds(old(slice))
170                    &&& self.index_mut_postcondition(&*old(slice), &*final(slice), x, &*final(x))
171                },
172            },
173    ;
174}
175
176pub broadcast axiom fn axiom_slice_ext_equal<T>(a1: &[T], a2: &[T])
177    ensures
178        #[trigger] (a1 =~= a2) <==> (a1.len() == a2.len() && forall|i: int|
179            0 <= i < a1.len() ==> a1[i] == a2[i]),
180;
181
182#[verifier::external_body]
183#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::spec_slice_update")]
184pub uninterp spec fn spec_slice_update<T>(slice: &[T], i: int, t: T) -> &[T];
185
186pub broadcast axiom fn axiom_spec_slice_update<T>(slice: &[T], i: int, t: T)
187    ensures
188        0 <= i < spec_slice_len(slice) ==> (#[trigger] spec_slice_update(slice, i, t)@)
189            == slice@.update(i, t),
190;
191
192#[verifier::external_body]
193#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::spec_slice_index")]
194pub uninterp spec fn spec_slice_index<T>(slice: &[T], i: int) -> T;
195
196pub broadcast axiom fn axiom_spec_slice_index<T>(slice: &[T], i: int)
197    ensures
198        0 <= i < spec_slice_len(slice) ==> (#[trigger] spec_slice_index(slice, i)) == slice@[i],
199;
200
201pub broadcast axiom fn axiom_slice_has_resolved<T>(slice: &[T], i: int)
202    ensures
203        0 <= i < spec_slice_len(slice) ==> #[trigger] has_resolved_unsized::<[T]>(slice)
204            ==> has_resolved(#[trigger] slice@[i]),
205;
206
207/// We axiomatize that a slice can decrease to its corresponding sequence.
208pub broadcast axiom fn axiom_slice_decreases_to_seq<T>(s: &[T])
209    ensures
210        #[trigger] (decreases_to!(s => s@)),
211;
212
213/// A slice can decrease to any of its elements, obtained by indexing.
214pub broadcast proof fn lemma_slice_index_decreases<T>(s: &[T], i: int)
215    requires
216        0 <= i < s@.len(),
217    ensures
218        #[trigger] (decreases_to!(s => s@[i])),
219{
220    axiom_slice_decreases_to_seq(s);
221    lemma_seq_index_decreases(s@, i);
222}
223
224pub axiom fn mut_ref_slice_len_eq<T>(tracked slice: &&mut [T])
225    ensures
226        old(*slice).len() == final(*slice).len(),
227;
228
229pub broadcast group group_slice_axioms {
230    axiom_spec_len,
231    axiom_slice_ext_equal,
232    axiom_spec_slice_update,
233    axiom_spec_slice_index,
234    axiom_slice_has_resolved,
235    axiom_slice_decreases_to_seq,
236    lemma_slice_index_decreases,
237}
238
239pub axiom fn tracked_borrow<T>(tracked s: &[T], i: int) -> (tracked t: &T)
240    requires
241        0 <= i < s.len(),
242    ensures
243        t == s[i],
244;
245
246pub axiom fn tracked_borrow_mut<T>(tracked s: &mut [T], i: int) -> (tracked t: &mut T)
247    requires
248        0 <= i < s.len(),
249    ensures
250        *t == old(s)[i],
251        final(s)@ == old(s)@.update(i, *final(t)),
252;
253
254} // verus!
vstd/slice.rs

vstd/
slice.rs
