Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727use super::super::prelude::*;
verus! {
// TODO mark the lemmas as not external_body when it's supported// along with broadcast_forall////////////////////////////////////////////////////// For u8/// Equivalent to `i.trailing_zeros()`./// See [`axiom_u8_trailing_zeros`] for useful properties.pub closed spec fn u8_trailing_zeros(i: u8) -> u32 decreases i,{ if i == 0 { 8 } else if (i & 1) != 0 { 0 } else { (1 + u8_trailing_zeros(i / 2)) as u32 }}
/// Equivalent to `i.leading_zeros()`./// See [`axiom_u8_leading_zeros`] for useful properties.pub closed spec fn u8_leading_zeros(i: u8) -> u32 decreases i,{ if i == 0 { 8 } else { (u8_leading_zeros(i / 2) - 1) as u32 }}
/// Equivalent to `i.trailing_ones()`./// See [`axiom_u8_trailing_ones`] for useful properties.pub open spec fn u8_trailing_ones(i: u8) -> u32 { u8_trailing_zeros(!i)}
/// Equivalent to `i.leading_ones()`./// See [`axiom_u8_leading_ones`] for useful properties.pub open spec fn u8_leading_ones(i: u8) -> u32 { u8_leading_zeros(!i)}
#[verifier::when_used_as_spec(u8_trailing_zeros)]pub assume_specification[ u8::trailing_zeros ](i: u8) -> (r: u32) ensures r == u8_trailing_zeros(i),;
#[verifier::when_used_as_spec(u8_trailing_ones)]pub assume_specification[ u8::trailing_ones ](i: u8) -> (r: u32) ensures r == u8_trailing_ones(i),;
#[verifier::when_used_as_spec(u8_leading_zeros)]pub assume_specification[ u8::leading_zeros ](i: u8) -> (r: u32) ensures r == u8_leading_zeros(i),;
#[verifier::when_used_as_spec(u8_leading_ones)]pub assume_specification[ u8::leading_ones ](i: u8) -> (r: u32) ensures r == u8_leading_ones(i),;
pub broadcast proof fn axiom_u8_trailing_zeros(i: u8) ensures 0 <= #[trigger] u8_trailing_zeros(i) <= 8, i == 0 <==> u8_trailing_zeros(i) == 8, // i^th bit is 1 0 <= u8_trailing_zeros(i) < 8 ==> (i >> u8_trailing_zeros(i) as u8) & 1u8 == 1u8, // trailing bits are 0 i << sub(8, u8_trailing_zeros(i) as u8) == 0, forall|j: u8| 0 <= j < u8_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u8 == 0u8, decreases i,{ assert(i >> 0 == i) by (bit_vector); assert(i << 0 == i) by (bit_vector); assert(i & 0 == 0) by (bit_vector); assert(i / 2 == (i >> 1u8)) by (bit_vector); assert((i & 1) == 0 ==> i != 1) by (bit_vector); let x = u8_trailing_zeros(i / 2) as u8; assert(x < 8 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector); assert(i << 8 == 0) by (bit_vector); assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector); assert((i & 1) == 0 ==> (i >> 1) << sub(8, x) == 0 ==> i << sub(8, add(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u8_trailing_zeros(i / 2); } assert forall|j: u8| 0 <= j < u8_trailing_zeros(i) implies #[trigger] (i >> j) & 1u8 == 0u8 by { let y = u8_trailing_zeros(i) as u8; assert(y <= 8 ==> i << sub(8, y) == 0 && 0 <= j < y ==> (i >> j) & 1u8 == 0u8) by (bit_vector); }}
pub broadcast proof fn axiom_u8_trailing_ones(i: u8) ensures 0 <= #[trigger] u8_trailing_ones(i) <= 8, i == 0xffu8 <==> u8_trailing_ones(i) == 8, // i^th bit is 0 0 <= u8_trailing_ones(i) < 8 ==> (i >> u8_trailing_ones(i) as u8) & 1u8 == 0u8, // trailing bits are 1 (!i) << sub(8, u8_trailing_ones(i) as u8) == 0, forall|j: u8| 0 <= j < u8_trailing_ones(i) ==> #[trigger] (i >> j) & 1u8 == 1u8,{ axiom_u8_trailing_zeros(!i); assert(!0xffu8 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffu8) by (bit_vector); let x = u8_trailing_ones(i) as u8; assert(((!i) >> x) & 1u8 == 1u8 ==> (i >> x) & 1u8 == 0u8) by (bit_vector); assert forall|j: u8| 0 <= j < u8_trailing_ones(i) implies #[trigger] (i >> j) & 1u8 == 1u8 by { let y = u8_trailing_ones(i) as u8; assert(y <= 8 ==> (!i) << sub(8, y) == 0 && 0 <= j < y ==> (i >> j) & 1u8 == 1u8) by (bit_vector); }}
pub broadcast proof fn axiom_u8_leading_zeros(i: u8) ensures 0 <= #[trigger] u8_leading_zeros(i) <= 8, i == 0 <==> u8_leading_zeros(i) == 8, // i^th bit from the left is 1 0 <= u8_leading_zeros(i) < 8 ==> (i >> sub(7u8, u8_leading_zeros(i) as u8)) & 1u8 != 0u8, // leading bits are 0 i >> sub(8, u8_leading_zeros(i) as u8) == 0, forall|j: u8| 8 - u8_leading_zeros(i) <= j < 8 ==> #[trigger] (i >> j) & 1u8 == 0u8, decreases i,{ assert(i / 2 == (i >> 1u8)) by (bit_vector); assert(((i >> 1) >> sub(7u8, 0)) & 1u8 == 0u8) by (bit_vector); let x = u8_leading_zeros(i / 2) as u8; assert(i >> 0 == i) by (bit_vector); assert(1u8 & 1u8 == 1u8) by (bit_vector); assert(0 < x < 8 ==> ((i >> 1) >> sub(7u8, x)) == (i >> sub(7u8, sub(x, 1)))) by (bit_vector); assert(0 < x <= 8 ==> (i >> 1) >> sub(8, x) == 0 ==> i >> sub(8, sub(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u8_leading_zeros(i / 2); } assert forall|j: u8| 8 - u8_leading_zeros(i) <= j < 8 implies #[trigger] (i >> j) & 1u8 == 0u8 by { let y = u8_leading_zeros(i) as u8; assert(y <= 8 ==> i >> sub(8, y) == 0 ==> sub(8, y) <= j < 8 ==> (i >> j) & 1u8 == 0u8) by (bit_vector); }}
pub broadcast proof fn axiom_u8_leading_ones(i: u8) ensures 0 <= #[trigger] u8_leading_ones(i) <= 8, i == 0xffu8 <==> u8_leading_ones(i) == 8, // i^th bit from the left is 0 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,{ axiom_u8_leading_zeros(!i); assert(!0xffu8 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffu8) by (bit_vector); let x = u8_leading_ones(i) as u8; assert(((!i) >> sub(7u8, x)) & 1u8 != 0u8 ==> (i >> sub(7u8, x)) & 1u8 == 0u8) by (bit_vector); assert forall|j: u8| 8 - u8_leading_ones(i) <= j < 8 implies #[trigger] (i >> j) & 1u8 == 1u8 by { let y = u8_leading_ones(i) as u8; assert(y <= 8 ==> (!i) >> sub(8, y) == 0 ==> sub(8, y) <= j < 8 ==> (i >> j) & 1u8 == 1u8) by (bit_vector); }}
////////////////////////////////////////////////////// For u16/// Equivalent to `i.trailing_zeros()`./// See [`axiom_u16_trailing_zeros`] for useful properties.pub closed spec fn u16_trailing_zeros(i: u16) -> u32 decreases i,{ if i == 0 { 16 } else if (i & 1) != 0 { 0 } else { (1 + u16_trailing_zeros(i / 2)) as u32 }}
/// Equivalent to `i.leading_zeros()`./// See [`axiom_u16_leading_zeros`] for useful properties.pub closed spec fn u16_leading_zeros(i: u16) -> u32 decreases i,{ if i == 0 { 16 } else { (u16_leading_zeros(i / 2) - 1) as u32 }}
/// Equivalent to `i.trailing_ones()`./// See [`axiom_u16_trailing_ones`] for useful properties.pub open spec fn u16_trailing_ones(i: u16) -> u32 { u16_trailing_zeros(!i)}
/// Equivalent to `i.leading_ones()`./// See [`axiom_u16_leading_ones`] for useful properties.pub open spec fn u16_leading_ones(i: u16) -> u32 { u16_leading_zeros(!i)}
#[verifier::when_used_as_spec(u16_trailing_zeros)]pub assume_specification[ u16::trailing_zeros ](i: u16) -> (r: u32) ensures r == u16_trailing_zeros(i),;
#[verifier::when_used_as_spec(u16_trailing_ones)]pub assume_specification[ u16::trailing_ones ](i: u16) -> (r: u32) ensures r == u16_trailing_ones(i),;
#[verifier::when_used_as_spec(u16_leading_zeros)]pub assume_specification[ u16::leading_zeros ](i: u16) -> (r: u32) ensures r == u16_leading_zeros(i),;
#[verifier::when_used_as_spec(u16_leading_ones)]pub assume_specification[ u16::leading_ones ](i: u16) -> (r: u32) ensures r == u16_leading_ones(i),;
pub broadcast proof fn axiom_u16_trailing_zeros(i: u16) ensures 0 <= #[trigger] u16_trailing_zeros(i) <= 16, i == 0 <==> u16_trailing_zeros(i) == 16, // i^th bit is 1 0 <= u16_trailing_zeros(i) < 16 ==> (i >> u16_trailing_zeros(i) as u16) & 1u16 == 1u16, // trailing bits are 0 i << sub(16, u16_trailing_zeros(i) as u16) == 0, forall|j: u16| 0 <= j < u16_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u16 == 0u16, decreases i,{ assert(i >> 0 == i) by (bit_vector); assert(i << 0 == i) by (bit_vector); assert(i & 0 == 0) by (bit_vector); assert(i / 2 == (i >> 1u16)) by (bit_vector); assert((i & 1) == 0 ==> i != 1) by (bit_vector); let x = u16_trailing_zeros(i / 2) as u16; assert(x < 16 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector); assert(i << 16 == 0) by (bit_vector); assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector); assert((i & 1) == 0 ==> (i >> 1) << sub(16, x) == 0 ==> i << sub(16, add(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u16_trailing_zeros(i / 2); } assert forall|j: u16| 0 <= j < u16_trailing_zeros(i) implies #[trigger] (i >> j) & 1u16 == 0u16 by { let y = u16_trailing_zeros(i) as u16; assert(y <= 16 ==> i << sub(16, y) == 0 && 0 <= j < y ==> (i >> j) & 1u16 == 0u16) by (bit_vector); }}
pub broadcast proof fn axiom_u16_trailing_ones(i: u16) ensures 0 <= #[trigger] u16_trailing_ones(i) <= 16, i == 0xffffu16 <==> u16_trailing_ones(i) == 16, // i^th bit is 0 0 <= u16_trailing_ones(i) < 16 ==> (i >> u16_trailing_ones(i) as u16) & 1u16 == 0u16, // trailing bits are 1 (!i) << sub(16, u16_trailing_ones(i) as u16) == 0, forall|j: u16| 0 <= j < u16_trailing_ones(i) ==> #[trigger] (i >> j) & 1u16 == 1u16,{ axiom_u16_trailing_zeros(!i); assert(!0xffffu16 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffffu16) by (bit_vector); let x = u16_trailing_ones(i) as u16; assert(((!i) >> x) & 1u16 == 1u16 ==> (i >> x) & 1u16 == 0u16) by (bit_vector); assert forall|j: u16| 0 <= j < u16_trailing_ones(i) implies #[trigger] (i >> j) & 1u16 == 1u16 by { let y = u16_trailing_ones(i) as u16; assert(y <= 16 ==> (!i) << sub(16, y) == 0 && 0 <= j < y ==> (i >> j) & 1u16 == 1u16) by (bit_vector); }}
pub broadcast proof fn axiom_u16_leading_zeros(i: u16) ensures 0 <= #[trigger] u16_leading_zeros(i) <= 16, i == 0 <==> u16_leading_zeros(i) == 16, // i^th bit from the left is 1 0 <= u16_leading_zeros(i) < 16 ==> (i >> sub(15u16, u16_leading_zeros(i) as u16)) & 1u16 != 0u16, // leading bits are 0 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, decreases i,{ assert(i / 2 == (i >> 1u16)) by (bit_vector); assert(((i >> 1) >> sub(15u16, 0)) & 1u16 == 0u16) by (bit_vector); let x = u16_leading_zeros(i / 2) as u16; assert(i >> 0 == i) by (bit_vector); assert(1u16 & 1u16 == 1u16) by (bit_vector); assert(0 < x < 16 ==> ((i >> 1) >> sub(15u16, x)) == (i >> sub(15u16, sub(x, 1)))) by (bit_vector); assert(0 < x <= 16 ==> (i >> 1) >> sub(16, x) == 0 ==> i >> sub(16, sub(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u16_leading_zeros(i / 2); } assert forall|j: u16| 16 - u16_leading_zeros(i) <= j < 16 implies #[trigger] (i >> j) & 1u16 == 0u16 by { let y = u16_leading_zeros(i) as u16; assert(y <= 16 ==> i >> sub(16, y) == 0 ==> sub(16, y) <= j < 16 ==> (i >> j) & 1u16 == 0u16) by (bit_vector); }}
pub broadcast proof fn axiom_u16_leading_ones(i: u16) ensures 0 <= #[trigger] u16_leading_ones(i) <= 16, i == 0xffffu16 <==> u16_leading_ones(i) == 16, // i^th bit from the left is 0 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,{ axiom_u16_leading_zeros(!i); assert(!0xffffu16 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffffu16) by (bit_vector); let x = u16_leading_ones(i) as u16; assert(((!i) >> sub(15u16, x)) & 1u16 != 0u16 ==> (i >> sub(15u16, x)) & 1u16 == 0u16) by (bit_vector); assert forall|j: u16| 16 - u16_leading_ones(i) <= j < 16 implies #[trigger] (i >> j) & 1u16 == 1u16 by { let y = u16_leading_ones(i) as u16; assert(y <= 16 ==> (!i) >> sub(16, y) == 0 ==> sub(16, y) <= j < 16 ==> (i >> j) & 1u16 == 1u16) by (bit_vector); }}
////////////////////////////////////////////////////// For u32/// Equivalent to `i.trailing_zeros()`./// See [`axiom_u32_trailing_zeros`] for useful properties.pub closed spec fn u32_trailing_zeros(i: u32) -> u32 decreases i,{ if i == 0 { 32 } else if (i & 1) != 0 { 0 } else { (1 + u32_trailing_zeros(i / 2)) as u32 }}
/// Equivalent to `i.leading_zeros()`./// See [`axiom_u32_leading_zeros`] for useful properties.pub closed spec fn u32_leading_zeros(i: u32) -> u32 decreases i,{ if i == 0 { 32 } else { (u32_leading_zeros(i / 2) - 1) as u32 }}
/// Equivalent to `i.trailing_ones()`./// See [`axiom_u32_trailing_ones`] for useful properties.pub open spec fn u32_trailing_ones(i: u32) -> u32 { u32_trailing_zeros(!i)}
/// Equivalent to `i.leading_ones()`./// See [`axiom_u32_leading_ones`] for useful properties.pub open spec fn u32_leading_ones(i: u32) -> u32 { u32_leading_zeros(!i)}
#[verifier::when_used_as_spec(u32_trailing_zeros)]pub assume_specification[ u32::trailing_zeros ](i: u32) -> (r: u32) ensures r == u32_trailing_zeros(i),;
#[verifier::when_used_as_spec(u32_trailing_ones)]pub assume_specification[ u32::trailing_ones ](i: u32) -> (r: u32) ensures r == u32_trailing_ones(i),;
#[verifier::when_used_as_spec(u32_leading_zeros)]pub assume_specification[ u32::leading_zeros ](i: u32) -> (r: u32) ensures r == u32_leading_zeros(i),;
#[verifier::when_used_as_spec(u32_leading_ones)]pub assume_specification[ u32::leading_ones ](i: u32) -> (r: u32) ensures r == u32_leading_ones(i),;
pub broadcast proof fn axiom_u32_trailing_zeros(i: u32) ensures 0 <= #[trigger] u32_trailing_zeros(i) <= 32, i == 0 <==> u32_trailing_zeros(i) == 32, // i^th bit is 1 0 <= u32_trailing_zeros(i) < 32 ==> (i >> u32_trailing_zeros(i) as u32) & 1u32 == 1u32, // trailing bits are 0 i << sub(32, u32_trailing_zeros(i) as u32) == 0, forall|j: u32| 0 <= j < u32_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u32 == 0u32, decreases i,{ assert(i >> 0 == i) by (bit_vector); assert(i << 0 == i) by (bit_vector); assert(i & 0 == 0) by (bit_vector); assert(i / 2 == (i >> 1u32)) by (bit_vector); assert((i & 1) == 0 ==> i != 1) by (bit_vector); let x = u32_trailing_zeros(i / 2) as u32; assert(x < 32 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector); assert(i << 32 == 0) by (bit_vector); assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector); assert((i & 1) == 0 ==> (i >> 1) << sub(32, x) == 0 ==> i << sub(32, add(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u32_trailing_zeros(i / 2); } assert forall|j: u32| 0 <= j < u32_trailing_zeros(i) implies #[trigger] (i >> j) & 1u32 == 0u32 by { let y = u32_trailing_zeros(i) as u32; assert(y <= 32 ==> i << sub(32, y) == 0 && 0 <= j < y ==> (i >> j) & 1u32 == 0u32) by (bit_vector); }}
pub broadcast proof fn axiom_u32_trailing_ones(i: u32) ensures 0 <= #[trigger] u32_trailing_ones(i) <= 32, i == 0xffff_ffffu32 <==> u32_trailing_ones(i) == 32, // i^th bit is 0 0 <= u32_trailing_ones(i) < 32 ==> (i >> u32_trailing_ones(i) as u32) & 1u32 == 0u32, // trailing bits are 1 (!i) << sub(32, u32_trailing_ones(i) as u32) == 0, forall|j: u32| 0 <= j < u32_trailing_ones(i) ==> #[trigger] (i >> j) & 1u32 == 1u32,{ axiom_u32_trailing_zeros(!i); assert(!0xffff_ffffu32 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffff_ffffu32) by (bit_vector); let x = u32_trailing_ones(i) as u32; assert(((!i) >> x) & 1u32 == 1u32 ==> (i >> x) & 1u32 == 0u32) by (bit_vector); assert forall|j: u32| 0 <= j < u32_trailing_ones(i) implies #[trigger] (i >> j) & 1u32 == 1u32 by { let y = u32_trailing_ones(i) as u32; assert(y <= 32 ==> (!i) << sub(32, y) == 0 && 0 <= j < y ==> (i >> j) & 1u32 == 1u32) by (bit_vector); }}
pub broadcast proof fn axiom_u32_leading_zeros(i: u32) ensures 0 <= #[trigger] u32_leading_zeros(i) <= 32, i == 0 <==> u32_leading_zeros(i) == 32, // i^th bit from the left is 1 0 <= u32_leading_zeros(i) < 32 ==> (i >> sub(31u32, u32_leading_zeros(i) as u32)) & 1u32 != 0u32, // leading bits are 0 i >> sub(32, u32_leading_zeros(i) as u32) == 0, forall|j: u32| 32 - u32_leading_zeros(i) <= j < 32 ==> #[trigger] (i >> j) & 1u32 == 0u32, decreases i,{ assert(i / 2 == (i >> 1u32)) by (bit_vector); assert(((i >> 1) >> sub(31u32, 0)) & 1u32 == 0u32) by (bit_vector); let x = u32_leading_zeros(i / 2) as u32; assert(i >> 0 == i) by (bit_vector); assert(1u32 & 1u32 == 1u32) by (bit_vector); assert(0 < x < 32 ==> ((i >> 1) >> sub(31u32, x)) == (i >> sub(31u32, sub(x, 1)))) by (bit_vector); assert(0 < x <= 32 ==> (i >> 1) >> sub(32, x) == 0 ==> i >> sub(32, sub(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u32_leading_zeros(i / 2); } assert forall|j: u32| 32 - u32_leading_zeros(i) <= j < 32 implies #[trigger] (i >> j) & 1u32 == 0u32 by { let y = u32_leading_zeros(i) as u32; assert(y <= 32 ==> i >> sub(32, y) == 0 ==> sub(32, y) <= j < 32 ==> (i >> j) & 1u32 == 0u32) by (bit_vector); }}
pub broadcast proof fn axiom_u32_leading_ones(i: u32) ensures 0 <= #[trigger] u32_leading_ones(i) <= 32, i == 0xffff_ffffu32 <==> u32_leading_ones(i) == 32, // i^th bit from the left is 0 0 <= u32_leading_ones(i) < 32 ==> (i >> sub(31u32, u32_leading_ones(i) as u32)) & 1u32 == 0u32, (!i) >> sub(32, u32_leading_ones(i) as u32) == 0, forall|j: u32| 32 - u32_leading_ones(i) <= j < 32 ==> #[trigger] (i >> j) & 1u32 == 1u32,{ axiom_u32_leading_zeros(!i); assert(!0xffff_ffffu32 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffff_ffffu32) by (bit_vector); let x = u32_leading_ones(i) as u32; assert(((!i) >> sub(31u32, x)) & 1u32 != 0u32 ==> (i >> sub(31u32, x)) & 1u32 == 0u32) by (bit_vector); assert forall|j: u32| 32 - u32_leading_ones(i) <= j < 32 implies #[trigger] (i >> j) & 1u32 == 1u32 by { let y = u32_leading_ones(i) as u32; assert(y <= 32 ==> (!i) >> sub(32, y) == 0 ==> sub(32, y) <= j < 32 ==> (i >> j) & 1u32 == 1u32) by (bit_vector); }}
////////////////////////////////////////////////////// For u64/// Equivalent to `i.trailing_zeros()`./// See [`axiom_u64_trailing_zeros`] for useful properties.pub closed spec fn u64_trailing_zeros(i: u64) -> u32 decreases i,{ if i == 0 { 64 } else if (i & 1) != 0 { 0 } else { (1 + u64_trailing_zeros(i / 2)) as u32 }}
/// Equivalent to `i.leading_zeros()`./// See [`axiom_u64_leading_zeros`] for useful properties.#[verifier::opaque]pub open spec fn u64_leading_zeros(i: u64) -> int decreases i,{ if i == 0 { 64 } else { u64_leading_zeros(i / 2) - 1 }}
/// Equivalent to `i.trailing_ones()`./// See [`axiom_u64_trailing_ones`] for useful properties.pub open spec fn u64_trailing_ones(i: u64) -> u32 { u64_trailing_zeros(!i) as u32}
/// Equivalent to `i.leading_ones()`./// See [`axiom_u64_leading_ones`] for useful properties.pub open spec fn u64_leading_ones(i: u64) -> u32 { u64_leading_zeros(!i) as u32}
#[verifier::when_used_as_spec(u64_trailing_zeros)]pub assume_specification[ u64::trailing_zeros ](i: u64) -> (r: u32) ensures r == u64_trailing_zeros(i),;
#[verifier::when_used_as_spec(u64_trailing_ones)]pub assume_specification[ u64::trailing_ones ](i: u64) -> (r: u32) ensures r == u64_trailing_ones(i),;
//#[verifier::when_used_as_spec(u64_leading_zeros)]pub assume_specification[ u64::leading_zeros ](i: u64) -> (r: u32) ensures r as int == u64_leading_zeros(i),;
#[verifier::when_used_as_spec(u64_leading_ones)]pub assume_specification[ u64::leading_ones ](i: u64) -> (r: u32) ensures r == u64_leading_ones(i),;
pub broadcast proof fn axiom_u64_trailing_zeros(i: u64) ensures 0 <= #[trigger] u64_trailing_zeros(i) <= 64, i == 0 <==> u64_trailing_zeros(i) == 64, // i^th bit is 1 0 <= u64_trailing_zeros(i) < 64 ==> (i >> u64_trailing_zeros(i) as u64) & 1u64 == 1u64, // trailing bits are 0 i << sub(64, u64_trailing_zeros(i) as u64) == 0, forall|j: u64| 0 <= j < u64_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u64 == 0u64, decreases i,{ assert(i >> 0 == i) by (bit_vector); assert(i << 0 == i) by (bit_vector); assert(i & 0 == 0) by (bit_vector); assert(i / 2 == (i >> 1u64)) by (bit_vector); assert((i & 1) == 0 ==> i != 1) by (bit_vector); let x = u64_trailing_zeros(i / 2) as u64; assert(x < 64 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector); assert(i << 64 == 0) by (bit_vector); assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector); assert((i & 1) == 0 ==> (i >> 1) << sub(64, x) == 0 ==> i << sub(64, add(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u64_trailing_zeros(i / 2); } assert forall|j: u64| 0 <= j < u64_trailing_zeros(i) implies #[trigger] (i >> j) & 1u64 == 0u64 by { let y = u64_trailing_zeros(i) as u64; assert(y <= 64 ==> i << sub(64, y) == 0 && 0 <= j < y ==> (i >> j) & 1u64 == 0u64) by (bit_vector); }}
pub broadcast proof fn axiom_u64_trailing_ones(i: u64) ensures 0 <= #[trigger] u64_trailing_ones(i) <= 64, i == 0xffff_ffff_ffff_ffffu64 <==> u64_trailing_ones(i) == 64, // i^th bit is 0 0 <= u64_trailing_ones(i) < 64 ==> (i >> u64_trailing_ones(i) as u64) & 1u64 == 0u64, // trailing bits are 1 (!i) << sub(64, u64_trailing_ones(i) as u64) == 0, forall|j: u64| 0 <= j < u64_trailing_ones(i) ==> #[trigger] (i >> j) & 1u64 == 1u64,{ axiom_u64_trailing_zeros(!i); assert(!0xffff_ffff_ffff_ffffu64 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffff_ffff_ffff_ffffu64) by (bit_vector); let x = u64_trailing_ones(i) as u64; assert(((!i) >> x) & 1u64 == 1u64 ==> (i >> x) & 1u64 == 0u64) by (bit_vector); assert forall|j: u64| 0 <= j < u64_trailing_ones(i) implies #[trigger] (i >> j) & 1u64 == 1u64 by { let y = u64_trailing_ones(i) as u64; assert(y <= 64 ==> (!i) << sub(64, y) == 0 && 0 <= j < y ==> (i >> j) & 1u64 == 1u64) by (bit_vector); }}
pub broadcast proof fn axiom_u64_leading_zeros(i: u64) ensures 0 <= #[trigger] u64_leading_zeros(i) <= 64, i == 0 <==> u64_leading_zeros(i) == 64, // i^th bit from the left is 1 0 <= u64_leading_zeros(i) < 64 ==> (i >> sub(63u64, u64_leading_zeros(i) as u64)) & 1u64 != 0u64, // leading bits are 0 i >> sub(64, u64_leading_zeros(i) as u64) == 0, forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 0u64, decreases i,{ reveal(u64_leading_zeros); assert(i / 2 == (i >> 1u64)) by (bit_vector); assert(((i >> 1) >> sub(63u64, 0)) & 1u64 == 0u64) by (bit_vector); let x = u64_leading_zeros(i / 2) as u64; assert(i >> 0 == i) by (bit_vector); assert(1u64 & 1u64 == 1u64) by (bit_vector); assert(0 < x < 64 ==> ((i >> 1) >> sub(63u64, x)) == (i >> sub(63u64, sub(x, 1)))) by (bit_vector); assert(0 < x <= 64 ==> (i >> 1) >> sub(64, x) == 0 ==> i >> sub(64, sub(x, 1)) == 0) by (bit_vector); if i != 0 { axiom_u64_leading_zeros(i / 2); } assert forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 implies #[trigger] (i >> j) & 1u64 == 0u64 by { let y = u64_leading_zeros(i) as u64; assert(y <= 64 ==> i >> sub(64, y) == 0 ==> sub(64, y) <= j < 64 ==> (i >> j) & 1u64 == 0u64) by (bit_vector); }}
pub broadcast proof fn axiom_u64_leading_ones(i: u64) ensures 0 <= #[trigger] u64_leading_ones(i) <= 64, i == 0xffff_ffff_ffff_ffffu64 <==> u64_leading_ones(i) == 64, // i^th bit from the left is 0 0 <= u64_leading_ones(i) < 64 ==> (i >> sub(63u64, u64_leading_ones(i) as u64)) & 1u64 == 0u64, (!i) >> sub(64, u64_leading_ones(i) as u64) == 0, forall|j: u64| 64 - u64_leading_ones(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 1u64,{ axiom_u64_leading_zeros(!i); assert(!0xffff_ffff_ffff_ffffu64 == 0) by (bit_vector); assert(!i == 0 ==> i == 0xffff_ffff_ffff_ffffu64) by (bit_vector); let x = u64_leading_ones(i) as u64; assert(((!i) >> sub(63u64, x)) & 1u64 != 0u64 ==> (i >> sub(63u64, x)) & 1u64 == 0u64) by (bit_vector); assert forall|j: u64| 64 - u64_leading_ones(i) <= j < 64 implies #[trigger] (i >> j) & 1u64 == 1u64 by { let y = u64_leading_ones(i) as u64; assert(y <= 64 ==> (!i) >> sub(64, y) == 0 ==> sub(64, y) <= j < 64 ==> (i >> j) & 1u64 == 1u64) by (bit_vector); }}
pub broadcast group group_bits_axioms { axiom_u8_trailing_zeros, axiom_u8_trailing_ones, axiom_u8_leading_zeros, axiom_u8_leading_ones, axiom_u16_trailing_zeros, axiom_u16_trailing_ones, axiom_u16_leading_zeros, axiom_u16_leading_ones, axiom_u32_trailing_zeros, axiom_u32_trailing_ones, axiom_u32_leading_zeros, axiom_u32_leading_ones, axiom_u64_trailing_zeros, axiom_u64_trailing_ones, axiom_u64_leading_zeros, axiom_u64_leading_ones,}
} // verus!