Functions§
- _verus_
external_ ⚠fn_ specification_ 0_ u8_ 32__ 58__ 58__ 32_ ilog2 - _verus_
external_ ⚠fn_ specification_ 1_ u16_ 32__ 58__ 58__ 32_ ilog2 - _verus_
external_ ⚠fn_ specification_ 2_ u32_ 32__ 58__ 58__ 32_ ilog2 - _verus_
external_ ⚠fn_ specification_ 3_ usize_ 32__ 58__ 58__ 32_ ilog2 - _verus_
external_ ⚠fn_ specification_ 4_ u64_ 32__ 58__ 58__ 32_ ilog2 - lemma2_
to64_ hi32 - lemma_
log2_ to64 - lemma_
pow2_ increases - lemma_
pow2_ is_ pow2 - lemma_
pow2_ is_ pow2_ to64 - lemma_
pow2_ log2 - lemma_
u8_ ilog2_ ordered - lemma_
u8_ ilog2_ to8 - lemma_
u8_ is_ pow2_ is_ ilog2_ pow2 - lemma_
u8_ log2_ bounds - lemma_
u8_ pow2_ ilog2 - lemma_
u8_ pow2_ ilog2_ x - lemma_
u16_ ilog2_ ordered - lemma_
u16_ ilog2_ to16 - lemma_
u16_ is_ pow2_ is_ ilog2_ pow2 - lemma_
u16_ log2_ bounds - lemma_
u16_ pow2_ ilog2 - lemma_
u16_ pow2_ ilog2_ x - lemma_
u32_ ilog2_ ordered - lemma_
u32_ ilog2_ to32 - lemma_
u32_ is_ pow2_ is_ ilog2_ pow2 - lemma_
u32_ log2_ bounds - lemma_
u32_ pow2_ ilog2 - lemma_
u32_ pow2_ ilog2_ x - lemma_
u64_ ilog2_ ordered - lemma_
u64_ ilog2_ to64 - lemma_
u64_ is_ pow2_ is_ ilog2_ pow2 - lemma_
u64_ log2_ bounds - lemma_
u64_ pow2_ ilog2 - lemma_
u64_ pow2_ ilog2_ x - lemma_
usize_ ilog2_ ordered - lemma_
usize_ ilog2_ to32 - lemma_
usize_ is_ pow2_ is_ ilog2_ pow2 - lemma_
usize_ log2_ bounds - lemma_
usize_ pow2_ ilog2 - lemma_
usize_ pow2_ ilog2_ x - lemma_
usize_ pow2_ shl_ is_ pow2 - lemma_
usize_ shl_ is_ mul - u8_
ilog2_ spec - u16_
ilog2_ spec - u32_
ilog2_ spec - u64_
ilog2_ spec - usize_
ilog2_ spec