Function vstd::arithmetic::power2::lemma2_to64_rest

pub proof fn lemma2_to64_rest()

Expand description

ensures

pow2(33) == 0x200000000,

pow2(34) == 0x400000000,

pow2(35) == 0x800000000,

pow2(36) == 0x1000000000,

pow2(37) == 0x2000000000,

pow2(38) == 0x4000000000,

pow2(39) == 0x8000000000,

pow2(40) == 0x10000000000,

pow2(41) == 0x20000000000,

pow2(42) == 0x40000000000,

pow2(43) == 0x80000000000,

pow2(44) == 0x100000000000,

pow2(45) == 0x200000000000,

pow2(46) == 0x400000000000,

pow2(47) == 0x800000000000,

pow2(48) == 0x1000000000000,

pow2(49) == 0x2000000000000,

pow2(50) == 0x4000000000000,

pow2(51) == 0x8000000000000,

pow2(52) == 0x10000000000000,

pow2(53) == 0x20000000000000,

pow2(54) == 0x40000000000000,

pow2(55) == 0x80000000000000,

pow2(56) == 0x100000000000000,

pow2(57) == 0x200000000000000,

pow2(58) == 0x400000000000000,

pow2(59) == 0x800000000000000,

pow2(60) == 0x1000000000000000,

pow2(61) == 0x2000000000000000,

pow2(62) == 0x4000000000000000,

pow2(63) == 0x8000000000000000,

pow2(64) == 0x10000000000000000,

Proof establishing the concrete values for all powers of 2 from 33 to 64. This lemma is separated from lemma2_to64() to avoid a stack overflow issue while executing ./tools/docs.sh.