Function vstd::bits::lemma_u32_low_bits_mask_is_mod

source · 
pub broadcast proof fn lemma_u32_low_bits_mask_is_mod(x: u32, n: nat)
Expand description
requires
n < <u32>::BITS,
ensures
#[trigger] (x & (low_bits_mask(n) as u32)) == x % (pow2(n) as u32),

Proof that for natural n and x of type u32 , and with the low n-bit mask is equivalent to modulo 2^n.