Function vstd::std_specs::bits::axiom_u64_leading_zeros

pub broadcast proof fn axiom_u64_leading_zeros(i: u64)

Expand description

ensures

0 <= #[trigger] u64_leading_zeros(i) <= 64,

i == 0 <==> u64_leading_zeros(i) == 64,

0 <= u64_leading_zeros(i) < 64
    ==> (i >> sub(63u64, u64_leading_zeros(i) as u64)) & 1u64 != 0u64,

i >> sub(64, u64_leading_zeros(i) as u64) == 0,

forall |j: u64| {
    64 - u64_leading_zeros(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 0u64
},