pub proof fn usize_size_pow2()Expand description
ensures
is_pow2(size_of::<usize>() as int),The size of a usize will always be a power of 2, since Verus assumes 32 or 64-bit architecture.
pub proof fn usize_size_pow2()is_pow2(size_of::<usize>() as int),The size of a usize will always be a power of 2, since Verus assumes 32 or 64-bit architecture.