lemma_u32_log2_bounds

vstd_extra::external::ilog2

Function lemma_u32_log2_bounds 

Source 
pub proof fn lemma_u32_log2_bounds(x: u32)
Expand description
ensures
0 <= log(2, x as int) <= u32::BITS,
0 <= x.ilog2() <= u32::BITS,