Function vstd::std_specs::bits::axiom_u8_trailing_ones

pub broadcast proof fn axiom_u8_trailing_ones(i: u8)

Expand description

ensures

0 <= #[trigger] u8_trailing_ones(i) <= 8,

i == 0xffu8 <==> u8_trailing_ones(i) == 8,

0 <= u8_trailing_ones(i) < 8 ==> (i >> u8_trailing_ones(i) as u8) & 1u8 == 0u8,

(!i) << sub(8, u8_trailing_ones(i) as u8) == 0,

forall |j: u8| 0 <= j < u8_trailing_ones(i) ==> #[trigger] (i >> j) & 1u8 == 1u8,