From 38682c4d4a31d4c717ff98c05c0dc8809f8c5400 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 26 Feb 2026 17:40:42 +0100
Subject: [PATCH] fix: heartbeat limit in mvcgen due to withDefault rfl
 (#12696)

This PR fixes a test case reported by Alexander Bentkamp that runs into
a heartbeat limit due to daring use of `withDefault` `rfl` in `mvcgen`.
---
 src/Lean/Elab/Tactic/Do/Spec.lean         |  2 +-
 tests/lean/run/mvcgenRflReducibility.lean | 52 +++++++++++++++++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/mvcgenRflReducibility.lean

diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean
index 84a28ffff5..43083657b0 100644
--- a/src/Lean/Elab/Tactic/Do/Spec.lean
+++ b/src/Lean/Elab/Tactic/Do/Spec.lean
@@ -223,7 +223,7 @@ public def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag
   -- Often P or Q are schematic (i.e. an MVar app). Try to solve by rfl.
   -- We do `fullApproxDefEq` here so that `constApprox` is active; this is useful in
   -- `need_const_approx` of `doLogicTests.lean`.
-  let (HPRfl, QQ'Rfl) ← withDefault <| fullApproxDefEq <| do
+  let (HPRfl, QQ'Rfl) ← fullApproxDefEq <| do
     return (← isDefEqGuarded P goal.hyps, ← isDefEqGuarded Q Q')
 
   -- Discharge the validity proof for the spec if not rfl
diff --git a/tests/lean/run/mvcgenRflReducibility.lean b/tests/lean/run/mvcgenRflReducibility.lean
new file mode 100644
index 0000000000..10f4d6b4b5
--- /dev/null
+++ b/tests/lean/run/mvcgenRflReducibility.lean
@@ -0,0 +1,52 @@
+import Std.Tactic.Do
+
+/-!
+This test case from Hax asserts that `mspec` doesn't use default reducibility when trying
+`SPred.entails.rfl`. If it did, then the `MyShl.shl a 32` would be unfolded deeply and we'd run
+into timeouts.
+-/
+
+open Std.Do
+
+set_option mvcgen.warning false
+
+abbrev RustM := Except String
+
+class MyAdd (Self : Type) (Rhs : Type)
+  where
+  add : (Self -> Rhs -> RustM Self)
+
+instance : MyAdd UInt64 UInt64 := {
+  add x y := if BitVec.uaddOverflow x.toBitVec y.toBitVec then Except.error "" else pure (x + y)
+}
+
+class MyShl (Self : Type) (Rhs : Type)
+  where
+  shl : (Self -> Rhs -> RustM Self)
+
+instance : MyShl UInt64 Int32 := {
+  shl x y := pure (x <<< (UInt64.ofNat y.toInt.toNat))
+}
+
+-- Cannot close the proof with `sorry` due to heartbeat limit, so we'll just capture the error message.
+/--
+error: unsolved goals
+case vc1
+a : UInt64
+⊢ (wp⟦MyShl.shl a 32⟧
+      (fun a =>
+        wp⟦do
+            let a ← MyAdd.add 0 a
+            pure a⟧
+          (PostCond.noThrow fun r => ⌜True⌝),
+        ExceptConds.false)).down
+-/
+#guard_msgs in
+example (a : UInt64) :
+    ⦃⌜True⌝⦄
+      do
+        let a ← MyShl.shl a (32: Int32)
+        let a ← MyAdd.add (0 : UInt64) a
+        pure a
+    ⦃PostCond.noThrow fun r => ⌜True⌝⦄ := by
+  mvcgen -trivial -- (deterministic) timeout at `whnf`, maximum number of heartbeats (200000) has been reached