Function vstd::std_specs::bits::axiom_u32_trailing_ones
source · pub broadcast proof fn axiom_u32_trailing_ones(i: u32)Expand description
ensures
0 <= #[trigger] u32_trailing_ones(i) <= 32,i == 0xffff_ffffu32 <==> u32_trailing_ones(i) == 32,0 <= u32_trailing_ones(i) < 32 ==> (i >> u32_trailing_ones(i) as u32) & 1u32 == 0u32,(!i) << sub(32, u32_trailing_ones(i) as u32) == 0,forall |j: u32| 0 <= j < u32_trailing_ones(i) ==> #[trigger] (i >> j) & 1u32 == 1u32,