Module vstd::bits

Properties of bitwise operators.

Functions

• lemma_low_bits_mask_div2
• lemma_low_bits_mask_is_odd
• lemma_low_bits_mask_unfold
• lemma_low_bits_mask_values
• lemma_u8_low_bits_mask_is_mod
• lemma_u8_pow2_no_overflow
• lemma_u8_shl_is_mul
• lemma_u8_shr_is_div
• lemma_u16_low_bits_mask_is_mod
• lemma_u16_pow2_no_overflow
• lemma_u16_shl_is_mul
• lemma_u16_shr_is_div
• lemma_u32_low_bits_mask_is_mod
• lemma_u32_pow2_no_overflow
• lemma_u32_shl_is_mul
• lemma_u32_shr_is_div
• lemma_u64_low_bits_mask_is_mod
• lemma_u64_pow2_no_overflow
• lemma_u64_shl_is_mul
• lemma_u64_shr_is_div
• low_bits_mask