Function vstd::std_specs::bits::axiom_u32_leading_ones

pub broadcast proof fn axiom_u32_leading_ones(i: u32)

Expand description

ensures

0 <= #[trigger] u32_leading_ones(i) <= 32,

i == 0xffff_ffffu32 <==> u32_leading_ones(i) == 32,

0 <= u32_leading_ones(i) < 32
    ==> (i >> sub(31u32, u32_leading_ones(i) as u32)) & 1u32 == 0u32,

(!i) >> sub(32, u32_leading_ones(i) as u32) == 0,

forall |j: u32| 32 - u32_leading_ones(i) <= j < 32 ==> #[trigger] (i >> j) & 1u32 == 1u32,