lemma_log2_to64

vstd_extra::external::ilog2

Function lemma_log2_to64 

Source 
pub proof fn lemma_log2_to64()
Expand description
ensures
log(2, 0x1) == 0,
log(2, 0x2) == 1,
log(2, 0x4) == 2,
log(2, 0x8) == 3,
log(2, 0x10) == 4,
log(2, 0x20) == 5,
log(2, 0x40) == 6,
log(2, 0x80) == 7,
log(2, 0x100) == 8,
log(2, 0x200) == 9,
log(2, 0x400) == 10,
log(2, 0x800) == 11,
log(2, 0x1000) == 12,
log(2, 0x2000) == 13,
log(2, 0x4000) == 14,
log(2, 0x8000) == 15,
log(2, 0x10000) == 16,
log(2, 0x20000) == 17,
log(2, 0x40000) == 18,
log(2, 0x80000) == 19,
log(2, 0x100000) == 20,
log(2, 0x200000) == 21,
log(2, 0x400000) == 22,
log(2, 0x800000) == 23,
log(2, 0x1000000) == 24,
log(2, 0x2000000) == 25,
log(2, 0x4000000) == 26,
log(2, 0x8000000) == 27,
log(2, 0x10000000) == 28,
log(2, 0x20000000) == 29,
log(2, 0x40000000) == 30,
log(2, 0x80000000) == 31,
log(2, 0x100000000) == 32,
log(2, 0x200000000) == 33,
log(2, 0x400000000) == 34,
log(2, 0x800000000) == 35,
log(2, 0x1000000000) == 36,
log(2, 0x2000000000) == 37,
log(2, 0x4000000000) == 38,
log(2, 0x8000000000) == 39,
log(2, 0x10000000000) == 40,
log(2, 0x20000000000) == 41,
log(2, 0x40000000000) == 42,
log(2, 0x80000000000) == 43,
log(2, 0x100000000000) == 44,
log(2, 0x200000000000) == 45,
log(2, 0x400000000000) == 46,
log(2, 0x800000000000) == 47,
log(2, 0x1000000000000) == 48,
log(2, 0x2000000000000) == 49,
log(2, 0x4000000000000) == 50,
log(2, 0x8000000000000) == 51,
log(2, 0x10000000000000) == 52,
log(2, 0x20000000000000) == 53,
log(2, 0x40000000000000) == 54,
log(2, 0x80000000000000) == 55,
log(2, 0x100000000000000) == 56,
log(2, 0x200000000000000) == 57,
log(2, 0x400000000000000) == 58,
log(2, 0x800000000000000) == 59,
log(2, 0x1000000000000000) == 60,
log(2, 0x2000000000000000) == 61,
log(2, 0x4000000000000000) == 62,
log(2, 0x8000000000000000) == 63,
log(2, 0x10000000000000000) == 64,