From e5bbda1c3d9d405a25b41e609417f350e331dfe3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 11 Oct 2024 10:57:06 +0200 Subject: [PATCH] fix: context tracking in bv_decide counter example (#5675) Closes #5674. --- .../Tactic/BVDecide/Frontend/BVCheck.lean | 2 +- .../Tactic/BVDecide/Frontend/BVDecide.lean | 31 ++++++++++++------- .../Elab/Tactic/BVDecide/Frontend/LRAT.lean | 11 +++---- tests/lean/run/5674.lean | 14 +++++++++ 4 files changed, 40 insertions(+), 18 deletions(-) create mode 100644 tests/lean/run/5674.lean diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean index 9b1d70702501..f6846e08c1d3 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean +++ b/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, ""⟩ diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 1dac032f678d..1416e58716f7 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean index 7756af5c6060..f67585f48135 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean +++ b/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 α) diff --git a/tests/lean/run/5674.lean b/tests/lean/run/5674.lean new file mode 100644 index 000000000000..149b1e35e64c --- /dev/null +++ b/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