lemma_u64_log2_bounds

vstd_extra::external::ilog2

Function lemma_u64_log2_bounds 

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