pub proof fn lemma_usize_ilog2_to32()Expand description
ensures
(0x1 as usize).ilog2() == 0,(0x2 as usize).ilog2() == 1,(0x4 as usize).ilog2() == 2,(0x8 as usize).ilog2() == 3,(0x10 as usize).ilog2() == 4,(0x20 as usize).ilog2() == 5,(0x40 as usize).ilog2() == 6,(0x80 as usize).ilog2() == 7,(0x100 as usize).ilog2() == 8,(0x200 as usize).ilog2() == 9,(0x400 as usize).ilog2() == 10,(0x800 as usize).ilog2() == 11,(0x1000 as usize).ilog2() == 12,(0x2000 as usize).ilog2() == 13,(0x4000 as usize).ilog2() == 14,(0x8000 as usize).ilog2() == 15,(0x10000 as usize).ilog2() == 16,(0x20000 as usize).ilog2() == 17,(0x40000 as usize).ilog2() == 18,(0x80000 as usize).ilog2() == 19,(0x100000 as usize).ilog2() == 20,(0x200000 as usize).ilog2() == 21,(0x400000 as usize).ilog2() == 22,(0x800000 as usize).ilog2() == 23,(0x1000000 as usize).ilog2() == 24,(0x2000000 as usize).ilog2() == 25,(0x4000000 as usize).ilog2() == 26,(0x8000000 as usize).ilog2() == 27,(0x10000000 as usize).ilog2() == 28,(0x20000000 as usize).ilog2() == 29,(0x40000000 as usize).ilog2() == 30,(0x80000000 as usize).ilog2() == 31,