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    fn set(&mut self, idx: usize, t: T);
45}
46
47impl<T> SliceAdditionalExecFns<T> for [T] {
48    #[verifier::external_body]
49    fn set(&mut self, idx: usize, t: T)
50        requires
51            0 <= idx < old(self)@.len(),
52        ensures
53            self@ == old(self)@.update(idx as int, t),
54    {
55        self[idx] = t;
56    }
57}
58
59#[verifier::external_body]
60#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::slice_index_get")]
61pub exec fn slice_index_get<T>(slice: &[T], i: usize) -> (out: &T)
62    requires
63        0 <= i < slice.view().len(),
64    ensures
65        *out == slice@.index(i as int),
66{
67    &slice[i]
68}
69
70////// Len (with autospec)
71#[cfg_attr(all(verus_keep_ghost), rustc_diagnostic_item = "verus::vstd::slice::spec_slice_len")]
72pub uninterp spec fn spec_slice_len<T>(slice: &[T]) -> usize;
73
74// This axiom is slightly better than defining spec_slice_len to just be `slice@.len() as usize`
75// (the axiom also shows that slice@.len() is in-bounds for usize)
76pub broadcast axiom fn axiom_spec_len<T>(slice: &[T])
77    ensures
78        #[trigger] spec_slice_len(slice) == slice@.len(),
79;
80
81#[verifier::allow_in_spec]
82pub assume_specification<T>[ <[T]>::len ](slice: &[T]) -> (len: usize)
83    returns
84        spec_slice_len(slice),
85;
86
87pub open spec fn spec_slice_is_empty<T>(slice: &[T]) -> bool {
88    slice@.len() == 0
89}
90
91#[verifier::when_used_as_spec(spec_slice_is_empty)]
92pub assume_specification<T>[ <[T]>::is_empty ](slice: &[T]) -> (b: bool)
93    ensures
94        b <==> slice@.len() == 0,
95;
96
97#[cfg(feature = "alloc")]
98#[verifier::external_body]
99pub exec fn slice_to_vec<T: Copy>(slice: &[T]) -> (out: alloc::vec::Vec<T>)
100    ensures
101        out@ == slice@,
102{
103    slice.to_vec()
104}
105
106#[verifier::external_body]
107pub exec fn slice_subrange<T, 'a>(slice: &'a [T], i: usize, j: usize) -> (out: &'a [T])
108    requires
109        0 <= i <= j <= slice@.len(),
110    ensures
111        out@ == slice@.subrange(i as int, j as int),
112{
113    &slice[i..j]
114}
115
116#[verifier::external_trait_specification]
117#[verifier::external_trait_extension(SliceIndexSpec via SliceIndexSpecImpl)]
118pub trait ExSliceIndex<T> where T: ?Sized {
119    type ExternalTraitSpecificationFor: SliceIndex<T>;
120
121    type Output: ?Sized;
122
123    spec fn index_req(&self, slice: &T) -> bool;
124
125    fn index(self, slice: &T) -> &Self::Output
126        requires
127            self.index_req(slice),
128    ;
129}
130
131pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
132    &<I as SliceIndex<[T]>>::Output,
133>) where I: SliceIndex<[T]>
134    returns
135        spec_slice_get(slice, i),
136;
137
138pub uninterp spec fn spec_slice_get<T: ?Sized, I: SliceIndex<T>>(val: &T, idx: I) -> Option<
139    &<I as SliceIndex<T>>::Output,
140>;
141
142pub broadcast axiom fn axiom_slice_get_usize<T>(v: &[T], i: usize)
143    ensures
144        i < v.len() ==> #[trigger] spec_slice_get(v, i) === Some(&v[i as int]),
145        i >= v.len() ==> spec_slice_get(v, i).is_none(),
146;
147
148pub broadcast axiom fn axiom_slice_ext_equal<T>(a1: &[T], a2: &[T])
149    ensures
150        #[trigger] (a1 =~= a2) <==> (a1.len() == a2.len() && forall|i: int|
151            0 <= i < a1.len() ==> a1[i] == a2[i]),
152;
153
154#[verifier::external_body]
155#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::spec_slice_update")]
156pub uninterp spec fn spec_slice_update<T>(slice: &[T], i: int, t: T) -> &[T];
157
158pub broadcast axiom fn axiom_spec_slice_update<T>(slice: &[T], i: int, t: T)
159    ensures
160        0 <= i < spec_slice_len(slice) ==> (#[trigger] spec_slice_update(slice, i, t)@)
161            == slice@.update(i, t),
162;
163
164#[verifier::external_body]
165#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::spec_slice_index")]
166pub uninterp spec fn spec_slice_index<T>(slice: &[T], i: int) -> T;
167
168pub broadcast axiom fn axiom_spec_slice_index<T>(slice: &[T], i: int)
169    ensures
170        0 <= i < spec_slice_len(slice) ==> (#[trigger] spec_slice_index(slice, i)) == slice@[i],
171;
172
173pub broadcast axiom fn axiom_slice_has_resolved<T>(slice: &[T], i: int)
174    ensures
175        0 <= i < spec_slice_len(slice) ==> #[trigger] has_resolved_unsized::<[T]>(slice)
176            ==> has_resolved(#[trigger] slice@[i]),
177;
178
179pub broadcast group group_slice_axioms {
180    axiom_spec_len,
181    axiom_slice_get_usize,
182    axiom_slice_ext_equal,
183    axiom_spec_slice_update,
184    axiom_spec_slice_index,
185    axiom_slice_has_resolved,
186}
187
188} // verus!
vstd/slice.rs

vstd/
slice.rs
