Function vstd::std_specs::bits::axiom_u64_leading_ones
source · pub broadcast proof fn axiom_u64_leading_ones(i: u64)Expand description
ensures
0 <= #[trigger] u64_leading_ones(i) <= 64,i == 0xffff_ffff_ffff_ffffu64 <==> u64_leading_ones(i) == 64,0 <= u64_leading_ones(i) < 64
==> (i >> sub(63u64, u64_leading_ones(i) as u64)) & 1u64 == 0u64,(!i) >> sub(64, u64_leading_ones(i) as u64) == 0,forall |j: u64| 64 - u64_leading_ones(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 1u64,