Function vstd::bits::lemma_u64_low_bits_mask_is_mod

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

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