Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217#![allow(unused_imports)]use super::prelude::*;use super::seq::*;use super::slice::SliceAdditionalSpecFns;#[cfg(verus_keep_ghost)]use super::std_specs::iter::IteratorSpec;use super::view::*;
verus! {
pub open spec fn array_view<T, const N: usize>(a: [T; N]) -> Seq<T> { Seq::new(N as nat, |i: int| array_index(a, i))}
impl<T, const N: usize> View for [T; N] { type V = Seq<T>;
open spec fn view(&self) -> Seq<T> { array_view(*self) }}
impl<T: DeepView, const N: usize> DeepView for [T; N] { type V = Seq<T::V>;
open spec fn deep_view(&self) -> Seq<T::V> { let v = self.view(); Seq::new(v.len(), |i: int| v[i].deep_view()) }}
pub trait ArrayAdditionalSpecFns<T>: View<V = Seq<T>> { spec fn spec_index(&self, i: int) -> T recommends 0 <= i < self.view().len(), ;}
#[verifier::external]pub trait ArrayAdditionalExecFns<T> { #[cfg_attr(not(verus_verify_core), deprecated = "use `array[i] = value` instead")] fn set(&mut self, idx: usize, t: T);}
impl<T, const N: usize> ArrayAdditionalSpecFns<T> for [T; N] { #[verifier::inline] open spec fn spec_index(&self, i: int) -> T { self.view().index(i) }}
// Automatically introduce a[0], ..., a[N - 1] into SMT contextpub broadcast proof fn lemma_array_index<T, const N: usize>(a: [T; N], i: int) requires 0 <= i < N, ensures #![trigger array_index(a, i)] a[i] == array_view(a)[i],{}
impl<T, const N: usize> ArrayAdditionalExecFns<T> for [T; N] { #[verifier::external_body] fn set(&mut self, idx: usize, t: T) requires 0 <= idx < N, ensures final(self)@ == old(self)@.update(idx as int, t), { self[idx] = t; }}
#[verifier::external_body]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_index_get")]pub exec fn array_index_get<T, const N: usize>(ar: &[T; N], i: usize) -> (out: &T) requires 0 <= i < N, ensures *out == ar@.index(i as int),{ &ar[i]}
pub broadcast axiom fn array_len_matches_n<T, const N: usize>(ar: &[T; N]) ensures (#[trigger] ar@.len()) == N,;
pub uninterp spec fn spec_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T]);
pub broadcast axiom fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N]) ensures (#[trigger] spec_array_as_slice(ar))@ == ar@,;
pub assume_specification< 'a, T, const N: usize,>[ <&'a [T; N] as core::iter::IntoIterator>::into_iter ](s: &'a [T; N]) -> (iter: core::slice::Iter< 'a, T,>) ensures IteratorSpec::remaining(&iter) == s@.as_ref(), IteratorSpec::decrease(&iter) is Some,;
// Referenced by Verus' internal encoding for array -> slice coercion#[doc(hidden)]#[verifier::external_body]#[verifier::when_used_as_spec(spec_array_as_slice)]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_as_slice")]pub fn array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T]) ensures out == spec_array_as_slice(ar), ar@ == out@,{ ar}
pub assume_specification<T, const N: usize>[ <[T; N]>::as_slice ](ar: &[T; N]) -> (out: &[T]) ensures ar@ == out@, opens_invariants none no_unwind;
pub uninterp spec fn spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T) -> (res: [T; N]);
pub broadcast axiom fn axiom_spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T) ensures #![trigger spec_array_fill_for_copy_type::<T, N>(t)] // intentionally triggering on `spec_array_fill_for_copy_type` only forall|i: int| 0 <= i < N ==> spec_array_fill_for_copy_type::<T, N>(t).view()[i] == t,;
// The 'array fill' [t; N] where t is a Copy type// (Does not necessarily apply when t is a non-Copy const)#[doc(hidden)]#[verifier::external_body]#[verifier::when_used_as_spec(spec_array_fill_for_copy_type)]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_fill_for_copy_types")]pub fn array_fill_for_copy_types<T: Copy, const N: usize>(t: T) -> (res: [T; N]) ensures res == spec_array_fill_for_copy_type::<T, N>(t),{ [t;N]}
pub broadcast axiom fn axiom_array_ext_equal<T, const N: usize>(a1: [T; N], a2: [T; N]) ensures #[trigger] (a1 =~= a2) <==> (forall|i: int| 0 <= i < N ==> a1[i] == a2[i]),;
#[verifier::external_body]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::spec_array_update")]pub uninterp spec fn spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T) -> [T; N];
pub broadcast axiom fn axiom_spec_array_update<T, const N: usize>(array: [T; N], i: int, t: T) ensures 0 <= i < N ==> (#[trigger] spec_array_update(array, i, t)@) == array@.update(i, t),;
pub broadcast axiom fn axiom_array_has_resolved<T, const N: usize>(array: [T; N], i: int) ensures 0 <= i < N ==> #[trigger] has_resolved::<[T; N]>(array) ==> has_resolved( #[trigger] array@[i], ),;
#[doc(hidden)]#[verifier::external_body]#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::ref_mut_array_unsizing_coercion")]pub fn ref_mut_array_unsizing_coercion<T, const N: usize>(r: &mut [T; N]) -> (out: &mut [T]) ensures out.view() == old(r).view(), final(out).view() == final(r).view(), opens_invariants none no_unwind{ r}
/// We axiomatize that an array can decrease to its corresponding sequence.pub broadcast axiom fn axiom_array_decreases_to_seq<T, const N: usize>(a: &[T; N]) ensures #[trigger] (decreases_to!(a => a@)),;
/// An array can decrease to any of its elements, obtained by indexing.pub broadcast proof fn lemma_array_index_decreases<T, const N: usize>(a: &[T; N], i: int) requires 0 <= i < a@.len(), ensures #[trigger] (decreases_to!(a => a@[i])),{ axiom_array_decreases_to_seq(a); lemma_seq_index_decreases(a@, i);}
pub broadcast group group_array_axioms { array_len_matches_n, lemma_array_index, axiom_spec_array_as_slice, axiom_spec_array_fill_for_copy_type, axiom_array_ext_equal, axiom_spec_array_update, axiom_array_has_resolved, axiom_array_decreases_to_seq, lemma_array_index_decreases,}
} // verus!