vstd/
array.rs

1#![allow(unused_imports)]
2use super::prelude::*;
3use super::seq::*;
4use super::slice::SliceAdditionalSpecFns;
5#[cfg(verus_keep_ghost)]
6use super::std_specs::iter::IteratorSpec;
7use super::view::*;
8
9verus! {
10
11pub open spec fn array_view<T, const N: usize>(a: [T; N]) -> Seq<T> {
12    Seq::new(N as nat, |i: int| array_index(a, i))
13}
14
15impl<T, const N: usize> View for [T; N] {
16    type V = Seq<T>;
17
18    open spec fn view(&self) -> Seq<T> {
19        array_view(*self)
20    }
21}
22
23impl<T: DeepView, const N: usize> DeepView for [T; N] {
24    type V = Seq<T::V>;
25
26    open spec fn deep_view(&self) -> Seq<T::V> {
27        let v = self.view();
28        Seq::new(v.len(), |i: int| v[i].deep_view())
29    }
30}
31
32pub trait ArrayAdditionalSpecFns<T>: View<V = Seq<T>> {
33    spec fn spec_index(&self, i: int) -> T
34        recommends
35            0 <= i < self.view().len(),
36    ;
37}
38
39#[verifier::external]
40pub trait ArrayAdditionalExecFns<T> {
41    #[cfg_attr(not(verus_verify_core), deprecated = "use `array[i] = value` instead")]
42    fn set(&mut self, idx: usize, t: T);
43}
44
45impl<T, const N: usize> ArrayAdditionalSpecFns<T> for [T; N] {
46    #[verifier::inline]
47    open spec fn spec_index(&self, i: int) -> T {
48        self.view().index(i)
49    }
50}
51
52// Automatically introduce a[0], ..., a[N - 1] into SMT context
53pub broadcast proof fn lemma_array_index<T, const N: usize>(a: [T; N], i: int)
54    requires
55        0 <= i < N,
56    ensures
57        #![trigger array_index(a, i)]
58        a[i] == array_view(a)[i],
59{
60}
61
62impl<T, const N: usize> ArrayAdditionalExecFns<T> for [T; N] {
63    #[verifier::external_body]
64    fn set(&mut self, idx: usize, t: T)
65        requires
66            0 <= idx < N,
67        ensures
68            final(self)@ == old(self)@.update(idx as int, t),
69    {
70        self[idx] = t;
71    }
72}
73
74#[verifier::external_body]
75#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_index_get")]
76pub exec fn array_index_get<T, const N: usize>(ar: &[T; N], i: usize) -> (out: &T)
77    requires
78        0 <= i < N,
79    ensures
80        *out == ar@.index(i as int),
81{
82    &ar[i]
83}
84
85pub broadcast axiom fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
86    ensures
87        (#[trigger] ar@.len()) == N,
88;
89
90pub uninterp spec fn spec_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T]);
91
92pub broadcast axiom fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
93    ensures
94        (#[trigger] spec_array_as_slice(ar))@ == ar@,
95;
96
97pub assume_specification<
98    'a,
99    T,
100    const N: usize,
101>[ <&'a [T; N] as core::iter::IntoIterator>::into_iter ](s: &'a [T; N]) -> (iter: core::slice::Iter<
102    'a,
103    T,
104>)
105    ensures
106        IteratorSpec::remaining(&iter) == s@.as_ref(),
107        IteratorSpec::decrease(&iter) is Some,
108;
109
110// Referenced by Verus' internal encoding for array -> slice coercion
111#[doc(hidden)]
112#[verifier::external_body]
113#[verifier::when_used_as_spec(spec_array_as_slice)]
114#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_as_slice")]
115pub fn array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
116    ensures
117        out == spec_array_as_slice(ar),
118        ar@ == out@,
119{
120    ar
121}
122
123pub assume_specification<T, const N: usize>[ <[T; N]>::as_slice ](ar: &[T; N]) -> (out: &[T])
124    ensures
125        ar@ == out@,
126    opens_invariants none
127    no_unwind
128;
129
130pub uninterp spec fn spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T) -> (res: [T; N]);
131
132pub broadcast axiom fn axiom_spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T)
133    ensures
134        #![trigger spec_array_fill_for_copy_type::<T, N>(t)]
135        // intentionally triggering on `spec_array_fill_for_copy_type` only
136        forall|i: int|
137            0 <= i < N ==> spec_array_fill_for_copy_type::<T, N>(t).view()[i] == t,
138;
139
140// The 'array fill' [t; N] where t is a Copy type
141// (Does not necessarily apply when t is a non-Copy const)
142#[doc(hidden)]
143#[verifier::external_body]
144#[verifier::when_used_as_spec(spec_array_fill_for_copy_type)]
145#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_fill_for_copy_types")]
146pub fn array_fill_for_copy_types<T: Copy, const N: usize>(t: T) -> (res: [T; N])
147    ensures
148        res == spec_array_fill_for_copy_type::<T, N>(t),
149{
150    [t;N]
151}
152
153pub broadcast axiom fn axiom_array_ext_equal<T, const N: usize>(a1: [T; N], a2: [T; N])
154    ensures
155        #[trigger] (a1 =~= a2) <==> (forall|i: int| 0 <= i < N ==> a1[i] == a2[i]),
156;
157
158#[verifier::external_body]
159#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::spec_array_update")]
160pub uninterp spec fn spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T) -> [T; N];
161
162pub broadcast axiom fn axiom_spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T)
163    ensures
164        0 <= i < N ==> (#[trigger] spec_array_update(array, i, t)@) == array@.update(i, t),
165;
166
167pub broadcast axiom fn axiom_array_has_resolved<T, const N: usize>(array: [T; N], i: int)
168    ensures
169        0 <= i < N ==> #[trigger] has_resolved::<[T; N]>(array) ==> has_resolved(
170            #[trigger] array@[i],
171        ),
172;
173
174#[doc(hidden)]
175#[verifier::external_body]
176#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::ref_mut_array_unsizing_coercion")]
177pub fn ref_mut_array_unsizing_coercion<T, const N: usize>(r: &mut [T; N]) -> (out: &mut [T])
178    ensures
179        out.view() == old(r).view(),
180        final(out).view() == final(r).view(),
181    opens_invariants none
182    no_unwind
183{
184    r
185}
186
187/// We axiomatize that an array can decrease to its corresponding sequence.
188pub broadcast axiom fn axiom_array_decreases_to_seq<T, const N: usize>(a: &[T; N])
189    ensures
190        #[trigger] (decreases_to!(a => a@)),
191;
192
193/// An array can decrease to any of its elements, obtained by indexing.
194pub broadcast proof fn lemma_array_index_decreases<T, const N: usize>(a: &[T; N], i: int)
195    requires
196        0 <= i < a@.len(),
197    ensures
198        #[trigger] (decreases_to!(a => a@[i])),
199{
200    axiom_array_decreases_to_seq(a);
201    lemma_seq_index_decreases(a@, i);
202}
203
204pub broadcast group group_array_axioms {
205    array_len_matches_n,
206    lemma_array_index,
207    axiom_spec_array_as_slice,
208    axiom_spec_array_fill_for_copy_type,
209    axiom_array_ext_equal,
210    axiom_spec_array_update,
211    axiom_array_has_resolved,
212    axiom_array_decreases_to_seq,
213    lemma_array_index_decreases,
214}
215
216} // verus!
vstd/array.rs

vstd/
array.rs
