Function vstd::arithmetic::power2::lemma2_to64

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

Proof establishing the concrete values for all powers of 2 from 0 to 32 and also 2^64