lemma_u16_ilog2_to16

vstd_extra::external::ilog2

Function lemma_u16_ilog2_to16 

Source 
pub proof fn lemma_u16_ilog2_to16()
Expand description
ensures
(0x1 as u16).ilog2() == 0,
(0x2 as u16).ilog2() == 1,
(0x4 as u16).ilog2() == 2,
(0x8 as u16).ilog2() == 3,
(0x10 as u16).ilog2() == 4,
(0x20 as u16).ilog2() == 5,
(0x40 as u16).ilog2() == 6,
(0x80 as u16).ilog2() == 7,
(0x100 as u16).ilog2() == 8,
(0x200 as u16).ilog2() == 9,
(0x400 as u16).ilog2() == 10,
(0x800 as u16).ilog2() == 11,
(0x1000 as u16).ilog2() == 12,
(0x2000 as u16).ilog2() == 13,
(0x4000 as u16).ilog2() == 14,
(0x8000 as u16).ilog2() == 15,