Function vstd::bits::lemma_u8_low_bits_mask_is_mod

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

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