Function axiom_mem_contents_unwrap_init_correctness

pub proof fn axiom_mem_contents_unwrap_init_correctness<V, const N: usize>(
    arr: [MemContents<V>; N],
    res: MemContents<[V; N]>,
)

Expand description

requires

res == mem_contents_unwrap(arr),

is_mem_contents_all_init(arr),

ensures

res.is_init(),

forall |index: int| {
    0 <= index < N ==> #[trigger] res.value()[index] == arr[index].value()
},

axiom_mem_contents_unwrap_init_correctness