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
97// To allow reasoning about the returned iterator when the executable
98// function `iter()` is invoked in a `for` loop header (e.g., in
99// `for x in it: a.iter() { ... }`), we need to specify the behavior of
100// the iterator in spec mode. To do that, we add
101// `#[verifier::when_used_as_spec(spec_array_iter)` to the specification for
102// the executable `into_iter` method and define that spec function here.
103pub uninterp spec fn spec_array_iter<T, const N: usize>(s: &[T; N]) -> (iter: core::slice::Iter<
104    '_,
105    T,
106>);
107
108pub broadcast proof fn axiom_spec_array_iter<T, const N: usize>(s: &[T; N])
109    ensures
110        #[trigger] spec_array_iter(s).remaining() == s@.as_ref(),
111{
112    admit();
113}
114
115#[verifier::when_used_as_spec(spec_array_iter)]
116pub assume_specification<
117    'a,
118    T,
119    const N: usize,
120>[ <&'a [T; N] as core::iter::IntoIterator>::into_iter ](s: &'a [T; N]) -> (iter: core::slice::Iter<
121    'a,
122    T,
123>)
124    ensures
125        iter == spec_array_iter(s),
126        IteratorSpec::decrease(&iter) is Some,
127        IteratorSpec::initial_value_relation(&iter, &iter),
128;
129
130// Referenced by Verus' internal encoding for array -> slice coercion
131#[doc(hidden)]
132#[verifier::external_body]
133#[verifier::when_used_as_spec(spec_array_as_slice)]
134#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_as_slice")]
135pub fn array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
136    ensures
137        out == spec_array_as_slice(ar),
138        ar@ == out@,
139{
140    ar
141}
142
143pub assume_specification<T, const N: usize>[ <[T; N]>::as_slice ](ar: &[T; N]) -> (out: &[T])
144    ensures
145        ar@ == out@,
146;
147
148pub uninterp spec fn spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T) -> (res: [T; N]);
149
150pub broadcast axiom fn axiom_spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T)
151    ensures
152        #![trigger spec_array_fill_for_copy_type::<T, N>(t)]
153        // intentionally triggering on `spec_array_fill_for_copy_type` only
154        forall|i: int|
155            0 <= i < N ==> spec_array_fill_for_copy_type::<T, N>(t).view()[i] == t,
156;
157
158// The 'array fill' [t; N] where t is a Copy type
159// (Does not necessarily apply when t is a non-Copy const)
160#[doc(hidden)]
161#[verifier::external_body]
162#[verifier::when_used_as_spec(spec_array_fill_for_copy_type)]
163#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_fill_for_copy_types")]
164pub fn array_fill_for_copy_types<T: Copy, const N: usize>(t: T) -> (res: [T; N])
165    ensures
166        res == spec_array_fill_for_copy_type::<T, N>(t),
167{
168    [t;N]
169}
170
171pub broadcast axiom fn axiom_array_ext_equal<T, const N: usize>(a1: [T; N], a2: [T; N])
172    ensures
173        #[trigger] (a1 =~= a2) <==> (forall|i: int| 0 <= i < N ==> a1[i] == a2[i]),
174;
175
176#[verifier::external_body]
177#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::spec_array_update")]
178pub uninterp spec fn spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T) -> [T; N];
179
180pub broadcast axiom fn axiom_spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T)
181    ensures
182        0 <= i < N ==> (#[trigger] spec_array_update(array, i, t)@) == array@.update(i, t),
183;
184
185pub broadcast axiom fn axiom_array_has_resolved<T, const N: usize>(array: [T; N], i: int)
186    ensures
187        0 <= i < N ==> #[trigger] has_resolved::<[T; N]>(array) ==> has_resolved(
188            #[trigger] array@[i],
189        ),
190;
191
192#[doc(hidden)]
193#[verifier::external_body]
194#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::ref_mut_array_unsizing_coercion")]
195pub fn ref_mut_array_unsizing_coercion<T, const N: usize>(r: &mut [T; N]) -> (out: &mut [T])
196    ensures
197        out.view() == old(r).view(),
198        final(out).view() == final(r).view(),
199    opens_invariants none
200    no_unwind
201{
202    r
203}
204
205pub broadcast group group_array_axioms {
206    array_len_matches_n,
207    lemma_array_index,
208    axiom_spec_array_as_slice,
209    axiom_spec_array_fill_for_copy_type,
210    axiom_array_ext_equal,
211    axiom_spec_array_iter,
212    axiom_spec_array_update,
213    axiom_array_has_resolved,
214}
215
216} // verus!
vstd/array.rs

vstd/
array.rs
