Function u64_ilog2_spec Copy item path

pub open spec fn u64_ilog2_spec(x: u64) -> u32

{ log(2, x as int) as u32 }