vstd
In vstd::
bits
Functions
lemma_low_bits_mask_div2
lemma_low_bits_mask_is_odd
lemma_low_bits_mask_unfold
lemma_low_bits_mask_values
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
lemma_u8_low_bits_mask_is_mod
lemma_u8_pow2_no_overflow
lemma_u8_shl_is_mul
lemma_u8_shr_is_div
low_bits_mask
?
Settings
Function
vstd
::
bits
::
low_bits_mask
Copy item path
source
·
[
−
]
pub
open spec
fn low_bits_mask(n:
nat
) ->
nat
Expand description
{ (pow2(n) -
1
)
as
nat }
Mask with low n bits set.