Skip to main content

lemma_unsigned_int_max_is_pow2_minus_1

vstd::bits

Function lemma_unsigned_int_max_is_pow2_minus_1 

Source 
pub proof fn lemma_unsigned_int_max_is_pow2_minus_1()
Expand description
ensures
(u8::MAX as nat) == pow2(u8::BITS as nat) - 1,
(u16::MAX as nat) == pow2(u16::BITS as nat) - 1,
(u32::MAX as nat) == pow2(u32::BITS as nat) - 1,
(u64::MAX as nat) == pow2(u64::BITS as nat) - 1,
(u128::MAX as nat) == pow2(u128::BITS as nat) - 1,

Proof that the max value of each unsigned integer type is 2^BITS - 1.