fix: context tracking in bv_decide counter example (#5675)

Closes #5674.

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -41,7 +41,7 @@ def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := d
 
 @[inherit_doc Lean.Parser.Tactic.bvCheck]
 def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
-  let unsatProver : UnsatProver := fun reflectionResult _ => do
+  let unsatProver : UnsatProver := fun _ reflectionResult _ => do
     withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
       let proof ← lratChecker cfg reflectionResult.bvExpr
       return .ok ⟨proof, ""⟩

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -83,6 +83,10 @@ structure ReflectionResult where
 A counter example generated from the bitblaster.
 -/
 structure CounterExample where
+  /--
+  The goal in which to interpret this counter example.
+  -/
+  goal : MVarId
   /--
   The set of unused but potentially relevant hypotheses. Useful for diagnosing spurious counter
   examples.
@@ -97,7 +101,7 @@ structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := ReflectionResult → Std.HashMap Nat (Nat × Expr) →
+abbrev UnsatProver := MVarId → ReflectionResult → Std.HashMap Nat (Nat × Expr) →
     MetaM (Except CounterExample UnsatProver.Result)
 
 /--
@@ -112,8 +116,9 @@ abbrev DiagnosisM : Type → Type := ReaderT CounterExample <| StateRefT Diagnos
 namespace DiagnosisM
 
 def run (x : DiagnosisM Unit) (counterExample : CounterExample) : MetaM Diagnosis := do
-  let (_, issues) ← ReaderT.run x counterExample |>.run {}
-  return issues
+  counterExample.goal.withContext do
+    let (_, issues) ← ReaderT.run x counterExample |>.run {}
+    return issues
 
 def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
   return (← read).unusedHypotheses
@@ -177,7 +182,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
     err := err ++ m!"Consider the following assignment:\n"
     return err
 
-def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
+def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
     MetaM (Except CounterExample UnsatProver.Result) := do
   let bvExpr := reflectionResult.bvExpr
@@ -206,11 +211,13 @@ def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
 
   match res with
   | .ok cert =>
+    trace[Meta.Tactic.sat] "SAT solver found a proof."
     let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
     return .ok ⟨proof, cert⟩
   | .error assignment =>
+    trace[Meta.Tactic.sat] "SAT solver found a counter example."
     let equations := reconstructCounterExample map assignment aigSize atomsAssignment
-    return .error { unusedHypotheses := reflectionResult.unusedHypotheses, equations }
+    return .error { goal, unusedHypotheses := reflectionResult.unusedHypotheses, equations }
 
 
 def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
@@ -248,7 +255,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
 
     let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
-    match ← unsatProver reflectionResult atomsAssignment with
+    match ← unsatProver g reflectionResult atomsAssignment with
     | .ok ⟨bvExprUnsat, cert⟩ =>
       let proveFalse ← reflectionResult.proveFalse bvExprUnsat
       g.assign proveFalse
@@ -256,9 +263,9 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
     | .error counterExample => return .error counterExample
 
 def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM (Except CounterExample LratCert) := M.run do
-  let unsatProver : UnsatProver := fun reflectionResult atomsAssignment => do
+  let unsatProver : UnsatProver := fun g reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
-      lratBitblaster cfg reflectionResult atomsAssignment
+      lratBitblaster g cfg reflectionResult atomsAssignment
   closeWithBVReflection g unsatProver
 
 /--
@@ -289,9 +296,11 @@ def bvDecide (g : MVarId) (cfg : TacticContext) : MetaM Result := do
   match ← bvDecide' g cfg with
   | .ok result => return result
   | .error counterExample =>
-    let error ← explainCounterExampleQuality counterExample
-    let folder := fun error (var, value) => error ++ m!"{var} = {value.bv}\n"
-    throwError counterExample.equations.foldl (init := error) folder
+    counterExample.goal.withContext do
+      let error ← explainCounterExampleQuality counterExample
+      let folder := fun error (var, value) => error ++ m!"{var} = {value.bv}\n"
+      let errorMessage := counterExample.equations.foldl (init := error) folder
+      throwError (← addMessageContextFull errorMessage)
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
 def evalBvTrace : Tactic := fun

src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean

@@ -105,7 +105,7 @@ instance : ToExpr LRAT.IntAction where
       mkApp3 (mkConst ``LRAT.Action.del [.zero, .zero]) beta alpha (toExpr ids)
   toTypeExpr := mkConst ``LRAT.IntAction
 
-def LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : MetaM LratCert := do
+def LratCert.ofFile (lratPath : System.FilePath) (trimProofs : Bool) : CoreM LratCert := do
   let proofInput ← IO.FS.readBinFile lratPath
   let proof ←
     withTraceNode `sat (fun _ => return s!"Parsing LRAT file") do
@@ -139,8 +139,8 @@ Run an external SAT solver on the `CNF` to obtain an LRAT proof.
 This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwise.
 -/
 def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath)
-    (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool)
-    : MetaM (Except (Array (Bool × Nat)) LratCert) := do
+    (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) :
+    CoreM (Except (Array (Bool × Nat)) LratCert) := do
   IO.FS.withTempFile fun cnfHandle cnfPath => do
     withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do
       -- lazyPure to prevent compiler lifting
@@ -162,7 +162,7 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi
 /--
 Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
 -/
-def mkAuxDecl (name : Name) (value type : Expr) : MetaM Unit :=
+def mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
   addAndCompile <| .defnDecl {
     name := name,
     levelParams := [],
@@ -181,8 +181,7 @@ function together with a correctness theorem for it.
   `∀ (b : α) (c : LratCert), verifier b c = true → unsat b`
 -/
 def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContext) (reflected : α)
-    (verifier : Name) (unsat_of_verifier_eq_true : Name) :
-    MetaM Expr := do
+    (verifier : Name) (unsat_of_verifier_eq_true : Name) : MetaM Expr := do
   withTraceNode `sat (fun _ => return "Compiling expr term") do
     mkAuxDecl cfg.exprDef (toExpr reflected) (toTypeExpr α)
 

tests/lean/run/5674.lean

@@ -0,0 +1,14 @@
+import Std.Tactic.BVDecide
+
+/--
+error: The prover found a potentially spurious counterexample:
+- The following potentially relevant hypotheses could not be used: [h]
+Consider the following assignment:
+b = 0x0000000000000000#64
+-/
+#guard_msgs in
+example
+    (b : BitVec 64)
+    (h : b.toNat > 0) :
+    b > 0 := by
+  bv_decide