vstd: Add missing cases of lemma2_to64

verus-lang · Aug 24, 2024 · ab522ec · ab522ec
1 parent 0d7b766
commit ab522ec
Showing 1 changed file with 77 additions and 0 deletions.
diff --git a/source/vstd/arithmetic/power2.rs b/source/vstd/arithmetic/power2.rs
@@ -172,4 +172,81 @@ pub proof fn lemma2_to64()
     ) by(compute_only);
 }
 
+/// 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.
+pub proof fn lemma2_to64_rest()
+    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,
+{
+    reveal(pow2);
+    reveal(pow);
+    #[verusfmt::skip]
+    assert(
+        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
+    ) by(compute_only);
+}
+
 } // verus!