Function vstd::std_specs::bits::axiom_u8_leading_ones
source · pub broadcast proof fn axiom_u8_leading_ones(i: u8)Expand description
ensures
0 <= #[trigger] u8_leading_ones(i) <= 8,i == 0xffu8 <==> u8_leading_ones(i) == 8,0 <= u8_leading_ones(i) < 8 ==> (i >> sub(7u8, u8_leading_ones(i) as u8)) & 1u8 == 0u8,(!i) >> sub(8, u8_leading_ones(i) as u8) == 0,forall |j: u8| 8 - u8_leading_ones(i) <= j < 8 ==> #[trigger] (i >> j) & 1u8 == 1u8,