axiom_mem_contents_wrap_correctness

vstd_extra::array_ptr

Function axiom_mem_contents_wrap_correctness 

Source 
pub proof fn axiom_mem_contents_wrap_correctness<V, const N: usize>(
    data: MemContents<[V; N]>,
    res: [MemContents<V>; N],
)
Expand description
requires
res == mem_contents_wrap(data),
ensures
data.is_uninit() ==> is_mem_contents_all_uninit(res),
data.is_init()
    ==> is_mem_contents_all_init(res)
        && forall |index: int| {
            0 <= index < N ==> #[trigger] res[index].value() == data.value()[index]
        },