vstd/
array.rs

Help
1#![allow(unused_imports)]
2use super::prelude::*;
3use super::seq::*;
4use super::slice::SliceAdditionalSpecFns;
5use super::view::*;
6
7verus! {
8
9pub open spec fn array_view<T, const N: usize>(a: [T; N]) -> Seq<T> {
10    Seq::new(N as nat, |i: int| array_index(a, i))
11}
12
13impl<T, const N: usize> View for [T; N] {
14    type V = Seq<T>;
15
16    open spec fn view(&self) -> Seq<T> {
17        array_view(*self)
18    }
19}
20
21impl<T: DeepView, const N: usize> DeepView for [T; N] {
22    type V = Seq<T::V>;
23
24    open spec fn deep_view(&self) -> Seq<T::V> {
25        let v = self.view();
26        Seq::new(v.len(), |i: int| v[i].deep_view())
27    }
28}
29
30pub trait ArrayAdditionalSpecFns<T>: View<V = Seq<T>> {
31    spec fn spec_index(&self, i: int) -> T
32        recommends
33            0 <= i < self.view().len(),
34    ;
35}
36
37#[verifier::external]
38pub trait ArrayAdditionalExecFns<T> {
39    fn set(&mut self, idx: usize, t: T);
40}
41
42impl<T, const N: usize> ArrayAdditionalSpecFns<T> for [T; N] {
43    #[verifier::inline]
44    open spec fn spec_index(&self, i: int) -> T {
45        self.view().index(i)
46    }
47}
48
49// Automatically introduce a[0], ..., a[N - 1] into SMT context
50pub broadcast proof fn lemma_array_index<T, const N: usize>(a: [T; N], i: int)
51    requires
52        0 <= i < N,
53    ensures
54        #![trigger array_index(a, i)]
55        a[i] == array_view(a)[i],
56{
57}
58
59impl<T, const N: usize> ArrayAdditionalExecFns<T> for [T; N] {
60    #[verifier::external_body]
61    fn set(&mut self, idx: usize, t: T)
62        requires
63            0 <= idx < N,
64        ensures
65            self@ == old(self)@.update(idx as int, t),
66    {
67        self[idx] = t;
68    }
69}
70
71#[verifier::external_body]
72#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_index_get")]
73pub exec fn array_index_get<T, const N: usize>(ar: &[T; N], i: usize) -> (out: &T)
74    requires
75        0 <= i < N,
76    ensures
77        *out == ar@.index(i as int),
78{
79    &ar[i]
80}
81
82pub broadcast axiom fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
83    ensures
84        (#[trigger] ar@.len()) == N,
85;
86
87pub uninterp spec fn spec_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T]);
88
89pub broadcast axiom fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
90    ensures
91        (#[trigger] spec_array_as_slice(ar))@ == ar@,
92;
93
94// Referenced by Verus' internal encoding for array -> slice coercion
95#[doc(hidden)]
96#[verifier::external_body]
97#[verifier::when_used_as_spec(spec_array_as_slice)]
98#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_as_slice")]
99pub fn array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
100    ensures
101        ar@ == out@,
102{
103    ar
104}
105
106pub assume_specification<T, const N: usize>[ <[T; N]>::as_slice ](ar: &[T; N]) -> (out: &[T])
107    ensures
108        ar@ == out@,
109;
110
111pub uninterp spec fn spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T) -> (res: [T; N]);
112
113pub broadcast axiom fn axiom_spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T)
114    ensures
115        #![trigger spec_array_fill_for_copy_type::<T, N>(t)]
116        // intentionally triggering on `spec_array_fill_for_copy_type` only
117        forall|i: int|
118            0 <= i < N ==> spec_array_fill_for_copy_type::<T, N>(t).view()[i] == t,
119;
120
121// The 'array fill' [t; N] where t is a Copy type
122// (Does not necessarily apply when t is a non-Copy const)
123#[doc(hidden)]
124#[verifier::external_body]
125#[verifier::when_used_as_spec(spec_array_fill_for_copy_type)]
126#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_fill_for_copy_types")]
127pub fn array_fill_for_copy_types<T: Copy, const N: usize>(t: T) -> (res: [T; N])
128    ensures
129        res == spec_array_fill_for_copy_type::<T, N>(t),
130{
131    [t;N]
132}
133
134pub broadcast axiom fn axiom_array_ext_equal<T, const N: usize>(a1: [T; N], a2: [T; N])
135    ensures
136        #[trigger] (a1 =~= a2) <==> (forall|i: int| 0 <= i < N ==> a1[i] == a2[i]),
137;
138
139pub broadcast group group_array_axioms {
140    array_len_matches_n,
141    lemma_array_index,
142    axiom_spec_array_as_slice,
143    axiom_spec_array_fill_for_copy_type,
144    axiom_array_ext_equal,
145}
146
147} // verus!
vstd/array.rs

vstd/
array.rs
