1#![allow(unused_imports)]
2use super::prelude::*;
3use super::seq::*;
4use super::view::*;
5
6#[cfg(verus_keep_ghost)]
7#[cfg(feature = "alloc")]
8pub use super::std_specs::vec::VecAdditionalSpecFns;
9
10verus! {
11
12impl<T> View for [T] {
13 type V = Seq<T>;
14
15 uninterp spec fn view(&self) -> Seq<T>;
16}
17
18impl<T: DeepView> DeepView for [T] {
19 type V = Seq<T::V>;
20
21 open spec fn deep_view(&self) -> Seq<T::V> {
22 let v = self.view();
23 Seq::new(v.len(), |i: int| v[i].deep_view())
24 }
25}
26
27pub trait SliceAdditionalSpecFns<T>: View<V = Seq<T>> {
28 spec fn spec_index(&self, i: int) -> T
29 recommends
30 0 <= i < self.view().len(),
31 ;
32}
33
34impl<T> SliceAdditionalSpecFns<T> for [T] {
35 #[verifier::inline]
36 open spec fn spec_index(&self, i: int) -> T {
37 self.view().index(i)
38 }
39}
40
41#[verifier::external]
42pub trait SliceAdditionalExecFns<T> {
43 fn set(&mut self, idx: usize, t: T);
44}
45
46impl<T> SliceAdditionalExecFns<T> for [T] {
47 #[verifier::external_body]
48 fn set(&mut self, idx: usize, t: T)
49 requires
50 0 <= idx < old(self)@.len(),
51 ensures
52 self@ == old(self)@.update(idx as int, t),
53 {
54 self[idx] = t;
55 }
56}
57
58#[verifier::external_body]
59#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::slice_index_get")]
60pub exec fn slice_index_get<T>(slice: &[T], i: usize) -> (out: &T)
61 requires
62 0 <= i < slice.view().len(),
63 ensures
64 *out == slice@.index(i as int),
65{
66 &slice[i]
67}
68
69pub uninterp spec fn spec_slice_len<T>(slice: &[T]) -> usize;
71
72pub broadcast axiom fn axiom_spec_len<T>(slice: &[T])
75 ensures
76 #[trigger] spec_slice_len(slice) == slice@.len(),
77;
78
79#[verifier::when_used_as_spec(spec_slice_len)]
80pub assume_specification<T>[ <[T]>::len ](slice: &[T]) -> (len: usize)
81 ensures
82 len == spec_slice_len(slice),
83;
84
85#[cfg(feature = "alloc")]
86#[verifier::external_body]
87pub exec fn slice_to_vec<T: Copy>(slice: &[T]) -> (out: alloc::vec::Vec<T>)
88 ensures
89 out@ == slice@,
90{
91 slice.to_vec()
92}
93
94#[verifier::external_body]
95pub exec fn slice_subrange<T, 'a>(slice: &'a [T], i: usize, j: usize) -> (out: &'a [T])
96 requires
97 0 <= i <= j <= slice@.len(),
98 ensures
99 out@ == slice@.subrange(i as int, j as int),
100{
101 &slice[i..j]
102}
103
104#[verifier::external_trait_specification]
105pub trait ExSliceIndex<T> where T: ?Sized {
106 type ExternalTraitSpecificationFor: core::slice::SliceIndex<T>;
107
108 type Output: ?Sized;
109}
110
111pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
112 &<I as core::slice::SliceIndex<[T]>>::Output,
113>) where I: core::slice::SliceIndex<[T]>
114 returns
115 spec_slice_get(slice, i),
116;
117
118pub uninterp spec fn spec_slice_get<T: ?Sized, I: core::slice::SliceIndex<T>>(
119 val: &T,
120 idx: I,
121) -> Option<&<I as core::slice::SliceIndex<T>>::Output>;
122
123pub broadcast axiom fn axiom_slice_get_usize<T>(v: &[T], i: usize)
124 ensures
125 i < v.len() ==> #[trigger] spec_slice_get(v, i) === Some(&v[i as int]),
126 i >= v.len() ==> spec_slice_get(v, i).is_none(),
127;
128
129pub broadcast axiom fn axiom_slice_ext_equal<T>(a1: &[T], a2: &[T])
130 ensures
131 #[trigger] (a1 =~= a2) <==> (a1.len() == a2.len() && forall|i: int|
132 0 <= i < a1.len() ==> a1[i] == a2[i]),
133;
134
135pub broadcast group group_slice_axioms {
136 axiom_spec_len,
137 axiom_slice_get_usize,
138 axiom_slice_ext_equal,
139}
140
141}