Function vstd::std_specs::bits::axiom_u16_leading_ones

pub broadcast proof fn axiom_u16_leading_ones(i: u16)

Expand description

ensures

0 <= #[trigger] u16_leading_ones(i) <= 16,

i == 0xffffu16 <==> u16_leading_ones(i) == 16,

0 <= u16_leading_ones(i) < 16
    ==> (i >> sub(15u16, u16_leading_ones(i) as u16)) & 1u16 == 0u16,

(!i) >> sub(16, u16_leading_ones(i) as u16) == 0,

forall |j: u16| 16 - u16_leading_ones(i) <= j < 16 ==> #[trigger] (i >> j) & 1u16 == 1u16,