Benchmarks: fix stackoverflow regression

Benchmarks/Dss/Clipper/Common.lean

@@ -479,6 +479,21 @@ theorem uInt256OfByteArray_word_toBytesBE (w : UInt256) :
   · rw [byteArray_toList_eq]
   · simpa using word_toBytesBE_toByteArray_size w
 
+-- LIBRARY CANDIDATE: decode a `PUSH32` from local opcode/payload facts without reducing the
+-- surrounding generated bytecode by definitional equality.
+theorem decode_push32_of_get?_extract' {code : ByteArray} {pc w : UInt256}
+    (hget : code.get? pc.toNat = some 0x7f)
+    (hpayload : code.extract' (pc.toNat + 1) (pc.toNat + 33)
+        = ({ data := (EVM.Word.toBytesBE w).toArray } : ByteArray)) :
+    decode code pc = some (.Push .PUSH32, some (w, 32)) := by
+  unfold decode
+  rw [hget]
+  have hparse : parseInstr 0x7f = some (.Push .PUSH32) := by native_decide
+  simp [hparse, argOnNBytesOfInstr]
+  rw [show pc.toNat + 1 + 32 = pc.toNat + 33 by omega]
+  rw [hpayload]
+  rw [uInt256OfByteArray_word_toBytesBE]
+
 theorem clipperPatchesStartAt (v : ClipperImmutables) :
     PatchesStartAt 1463 (patches v) := by
   unfold PatchesStartAt patches patchesFrom offsets immValues

Benchmarks/Dss/Clipper/Ilk.lean

@@ -264,15 +264,16 @@ theorem clipperIlkPush32Decode (v : ClipperImmutables) {code : ByteArray}
     (hlen : bs.length = 32) :
     decode code (⟨6799⟩ : UInt256) =
       some (.Push .PUSH32, some (EVM.Word.ofNat (fromBytesBigEndian bs), 32)) := by
-  unfold decode
-  rw [patchRuntime_get?_disjoint hpatch
-    (by apply clipperIlkPatchesWindowDisjoint32 v; native_decide)]
-  change some (Operation.Push Operation.POp.PUSH32,
-      some (uInt256OfByteArray (code.extract' 6800 6832), 32)) =
-    some (Operation.Push Operation.POp.PUSH32,
-      some (EVM.Word.ofNat (fromBytesBigEndian bs), 32))
-  rw [clipperIlkPatchPayload v hpatch hilk hlen]
-  rw [uInt256OfByteArray_word_toBytesBE]
+  exact decode_push32_of_get?_extract'
+    (pc := (⟨6799⟩ : UInt256)) (w := EVM.Word.ofNat (fromBytesBigEndian bs))
+    (by
+      rw [patchRuntime_get?_disjoint hpatch
+        (by apply clipperIlkPatchesWindowDisjoint32 v; native_decide)]
+      native_decide)
+    (by
+      rw [show (⟨6799⟩ : UInt256).toNat + 1 = 6800 by native_decide]
+      rw [show (⟨6799⟩ : UInt256).toNat + 33 = 6832 by native_decide]
+      exact clipperIlkPatchPayload v hpatch hilk hlen)
 
 set_option maxHeartbeats 1000000 in
 theorem clipperIlkConstGetterWf (v : ClipperImmutables) {code : ByteArray}

Benchmarks/Dss/Clipper/Vat.lean

@@ -348,14 +348,16 @@ theorem clipperVatPush32Decode (v : ClipperImmutables) {code : ByteArray}
     (hpatch : patchRuntime clipperBytecode (patches v) = some code) :
     decode code (⟨3144⟩ : UInt256) =
       some (.Push .PUSH32, some (EVM.Word.ofNat (↑v.vat : Nat), 32)) := by
-  unfold decode
-  rw [patchRuntime_get?_disjoint hpatch
-    (by apply clipperVatPatchesWindowDisjoint32 v; native_decide)]
-  change some (Operation.Push Operation.POp.PUSH32,
-      some (uInt256OfByteArray (code.extract' 3145 3177), 32)) =
-    some (Operation.Push Operation.POp.PUSH32, some (EVM.Word.ofNat (↑v.vat : Nat), 32))
-  rw [clipperVatPatchPayload v hpatch]
-  rw [uInt256OfByteArray_word_toBytesBE]
+  exact decode_push32_of_get?_extract'
+    (pc := (⟨3144⟩ : UInt256)) (w := EVM.Word.ofNat (↑v.vat : Nat))
+    (by
+      rw [patchRuntime_get?_disjoint hpatch
+        (by apply clipperVatPatchesWindowDisjoint32 v; native_decide)]
+      native_decide)
+    (by
+      rw [show (⟨3144⟩ : UInt256).toNat + 1 = 3145 by native_decide]
+      rw [show (⟨3144⟩ : UInt256).toNat + 33 = 3177 by native_decide]
+      exact clipperVatPatchPayload v hpatch)
 
 set_option maxHeartbeats 1000000 in
 theorem clipperVatConstGetterWf (v : ClipperImmutables) {code : ByteArray}