Function vstd::bits::lemma_u16_low_bits_mask_is_mod

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

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