lemma_usize_shl_is_mul

vstd::bits

Function lemma_usize_shl_is_mul 

Source 
pub broadcast proof fn lemma_usize_shl_is_mul(x: usize, shift: usize)
Expand description
requires
0 <= shift < <usize>::BITS,
x * pow2(shift as nat) <= <usize>::MAX,
ensures
#[trigger] (x << shift) == x * pow2(shift as nat),

Proof that for x and n of type usize , shifting x left by n is equivalent to multiplication of x by 2^n (provided no overflow).