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;
127
128pub uninterp spec fn spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T) -> (res: [T; N]);
129
130pub broadcast axiom fn axiom_spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T)
131    ensures
132        #![trigger spec_array_fill_for_copy_type::<T, N>(t)]
133        // intentionally triggering on `spec_array_fill_for_copy_type` only
134        forall|i: int|
135            0 <= i < N ==> spec_array_fill_for_copy_type::<T, N>(t).view()[i] == t,
136;
137
138// The 'array fill' [t; N] where t is a Copy type
139// (Does not necessarily apply when t is a non-Copy const)
140#[doc(hidden)]
141#[verifier::external_body]
142#[verifier::when_used_as_spec(spec_array_fill_for_copy_type)]
143#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_fill_for_copy_types")]
144pub fn array_fill_for_copy_types<T: Copy, const N: usize>(t: T) -> (res: [T; N])
145    ensures
146        res == spec_array_fill_for_copy_type::<T, N>(t),
147{
148    [t;N]
149}
150
151pub broadcast axiom fn axiom_array_ext_equal<T, const N: usize>(a1: [T; N], a2: [T; N])
152    ensures
153        #[trigger] (a1 =~= a2) <==> (forall|i: int| 0 <= i < N ==> a1[i] == a2[i]),
154;
155
156#[verifier::external_body]
157#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::spec_array_update")]
158pub uninterp spec fn spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T) -> [T; N];
159
160pub broadcast axiom fn axiom_spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T)
161    ensures
162        0 <= i < N ==> (#[trigger] spec_array_update(array, i, t)@) == array@.update(i, t),
163;
164
165pub broadcast axiom fn axiom_array_has_resolved<T, const N: usize>(array: [T; N], i: int)
166    ensures
167        0 <= i < N ==> #[trigger] has_resolved::<[T; N]>(array) ==> has_resolved(
168            #[trigger] array@[i],
169        ),
170;
171
172#[doc(hidden)]
173#[verifier::external_body]
174#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::ref_mut_array_unsizing_coercion")]
175pub fn ref_mut_array_unsizing_coercion<T, const N: usize>(r: &mut [T; N]) -> (out: &mut [T])
176    ensures
177        out.view() == old(r).view(),
178        final(out).view() == final(r).view(),
179    opens_invariants none
180    no_unwind
181{
182    r
183}
184
185pub broadcast group group_array_axioms {
186    array_len_matches_n,
187    lemma_array_index,
188    axiom_spec_array_as_slice,
189    axiom_spec_array_fill_for_copy_type,
190    axiom_array_ext_equal,
191    axiom_spec_array_update,
192    axiom_array_has_resolved,
193}
194
195} // verus!
vstd/array.rs

vstd/
array.rs
