refactor: reuse Grind.withProtectedMCtx in sym VCGen emitVC

This removes the reimplemented `resolveDelayedAssignments` and the manual
`withNewMCtxDepth` + `mkFreshExprSyntheticOpaqueMVar` pattern in `emitVC`,
replacing them with a call to `Grind.withProtectedMCtx`. On exception,
`withProtectedMCtx` admits the goal, so we save/restore the `MetavarContext`
to undo the admit and fall back to emitting an unsolved VC.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean

@@ -13,8 +13,8 @@ set_option mvcgen.warning false
 
 @[spec high]
 theorem Spec.MonadState_get {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond σ (.arg σ ps)} :
-    ⦃fun s => Q.fst s s⦄ get (m := StateT σ m) ⦃Q⦄ := by
-  mvcgen'
+    ⦃fun s => let x := s; Q.fst x x⦄ get (m := StateT σ m) ⦃Q⦄ := by
+  mvcgen
 
 @[spec high]
 theorem Spec.MonadStateOf_set {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond PUnit (.arg σ ps)} {s : σ} :

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -797,27 +797,14 @@ meta def solve (item : WorkItem) : VCGenM SolveResult := item.mvarId.withContext
 
   return .noStrategyForProgram e
 
-/--
-Resolve delayed metavariable assignments in `e`.
-Grind uses delayed mvar assignments internally for proof construction; these must be resolved
-before the proof can pass the kernel type checker.
-Reimplements the logic of `Lean.Meta.Grind.resolveDelayedMVarAssignments` (which is private).
--/
-private meta partial def resolveDelayedAssignments (e : Expr) : MetaM Expr := do
-  if !e.hasMVar then return e
-  for mvarId in (e.collectMVars {}).result do
-    if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-      if let some val ← getExprMVarAssignment? mvarIdPending then
-        let pendingDecl ← mvarIdPending.getDecl
-        let val ← resolveDelayedAssignments (← instantiateMVars val)
-        mvarId.assign (pendingDecl.lctx.mkLambda fvars val)
-  instantiateMVars e
-
 /--
 Called when decomposing the goal further did not succeed; in this case we emit a VC for the goal.
 In grind mode, tries to solve the VC using the accumulated `Grind.Goal` state (E-graph) via
-`Grind.processHypotheses` + `Grind.solve`. Uses `withNewMCtxDepth` to protect parent mvars
-from grind's `isDefEq` calls, and resolves delayed assignments before exiting.
+`Grind.withProtectedMCtx` + `Grind.processHypotheses` + `Grind.solve`.
+`withProtectedMCtx` handles `withNewMCtxDepth` isolation, delayed assignment resolution, and
+optional proof abstraction.
+If grind fails (or `withProtectedMCtx` admits on exception), we undo the assignment and fall back
+to emitting an unsolved VC.
 -/
 meta def emitVC (item : WorkItem) : VCGenM Unit := do
   let ty ← item.mvarId.getType
@@ -825,28 +812,21 @@ meta def emitVC (item : WorkItem) : VCGenM Unit := do
     item.mvarId.setKind .syntheticOpaque
     modify fun s => { s with invariants := s.invariants.push item.mvarId }
   else if let some grindGoal := item.grindGoal? then
-    let solved ← item.mvarId.withContext do
-      let type ← item.mvarId.getType
-      try
-        let val? ← withNewMCtxDepth do
-          let mvar' ← mkFreshExprSyntheticOpaqueMVar type
-          let grindGoal' := { grindGoal with mvarId := mvar'.mvarId! }
-          -- Internalize new hypotheses. This may discover contradictions and
-          -- assign mvar' directly via closeGoal.
-          let grindGoal' ← Grind.processHypotheses grindGoal'
-          unless ← mvar'.mvarId!.isAssigned do
-            discard <| Grind.solve grindGoal'
-          if ← mvar'.mvarId!.isAssigned then
-            let val ← instantiateMVars mvar'
-            let val ← resolveDelayedAssignments val
-            if val.hasMVar then pure none
-            else pure (some val)
-          else
-            pure none
-        match val? with
-        | some val => item.mvarId.assign val; pure true
-        | none => pure false
-      catch _ => pure false
+    let config ← Grind.getConfig
+    -- Save mctx so we can undo if withProtectedMCtx admits on exception
+    let savedMCtx ← getMCtx
+    let solved ← tryCatchRuntimeEx
+        (do
+          Grind.withProtectedMCtx config item.mvarId fun mvarId' => do
+            let grindGoal' := { grindGoal with mvarId := mvarId' }
+            let grindGoal' ← Grind.processHypotheses grindGoal'
+            unless ← mvarId'.isAssigned do
+              discard <| Grind.solve grindGoal'
+          pure true)
+        fun _ => do
+          -- withProtectedMCtx admits on exception; undo the admit
+          setMCtx savedMCtx
+          pure false
     unless solved do
       item.mvarId.setKind .syntheticOpaque
       modify fun s => { s with vcs := s.vcs.push item.mvarId }

tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean

@@ -7,7 +7,12 @@ open GetThrowSet
 set_option maxRecDepth 100000
 set_option maxHeartbeats 100000000
 
+-- example : Goal 10 := by
+--   simp only [Goal, loop, step]
+--   mvcgen
+
 -- Benchmark `mvcgen' with grind`: grind integrated into VCGen loop for incremental
 -- context internalization. This avoids O(n) re-internalization per VC.
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| sorry)
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with grind) `(tactic| fail)
+  -- [100]
   [100, 500, 1000]