lemma_u8_pow2_ilog2

vstd_extra::external::ilog2

Function lemma_u8_pow2_ilog2 

Source 
pub broadcast proof fn lemma_u8_pow2_ilog2(e: u32)
Expand description
requires
pow2(e as nat) <= u8::MAX,
ensures
#[trigger] (pow2(e as nat) as u8).ilog2() == e,