Function vstd::std_specs::bits::axiom_u16_leading_zeros

source · 
pub broadcast proof fn axiom_u16_leading_zeros(i: u16)
Expand description
ensures
0 <= #[trigger] u16_leading_zeros(i) <= 16,
i == 0 <==> u16_leading_zeros(i) == 16,
0 <= u16_leading_zeros(i) < 16
    ==> (i >> sub(15u16, u16_leading_zeros(i) as u16)) & 1u16 != 0u16,
i >> sub(16, u16_leading_zeros(i) as u16) == 0,
forall |j: u16| {
    16 - u16_leading_zeros(i) <= j < 16 ==> #[trigger] (i >> j) & 1u16 == 0u16
},