vstd/
slice.rs

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

vstd/
slice.rs
