feat: bv_decide diagnosis (leanprover#5365)

Fixes: leanprover#5326

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

@@ -41,9 +41,9 @@ 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 bvExpr _ => do
+  let unsatProver : UnsatProver := fun reflectionResult _ => do
     withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
-      let proof ← lratChecker cfg bvExpr
+      let proof ← lratChecker cfg reflectionResult.bvExpr
       return ⟨proof, ""⟩
   let _ ← closeWithBVReflection g unsatProver
   return ()

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

@@ -74,19 +74,111 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
+structure ReflectionResult where
+  bvExpr : BVLogicalExpr
+  proveFalse : Expr → M Expr
+  unusedHypotheses : Std.HashSet FVarId
+
 structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := BVLogicalExpr → Std.HashMap Nat Expr → MetaM UnsatProver.Result
+abbrev UnsatProver := ReflectionResult → Std.HashMap Nat Expr → MetaM UnsatProver.Result
+
+/--
+Contains values that will be used to diagnose spurious counter examples.
+-/
+structure DiagnosisInput where
+  unusedHypotheses : Std.HashSet FVarId
+  atomsAssignment : Std.HashMap Nat Expr
+
+/--
+The result of a spurious counter example diagnosis.
+-/
+structure Diagnosis where
+  uninterpretedSymbols : Std.HashSet Expr := {}
+  unusedRelevantHypotheses : Std.HashSet FVarId := {}
+
+abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnosis MetaM
+
+namespace DiagnosisM
+
+def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId)
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do
+  let (_, issues) ← ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {}
+  return issues
+
+def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
+  return (← read).unusedHypotheses
+
+def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
+  return (← read).atomsAssignment
+
+def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
+  modify fun s => { s with uninterpretedSymbols := s.uninterpretedSymbols.insert e }
 
-def lratBitblaster (cfg : TacticContext) (bv : BVLogicalExpr)
+def addUnusedRelevantHypothesis (fvar : FVarId) : DiagnosisM Unit :=
+  modify fun s => { s with unusedRelevantHypotheses := s.unusedRelevantHypotheses.insert fvar }
+
+def checkRelevantHypsUsed (fvar : FVarId) : DiagnosisM Unit := do
+  for hyp in ← unusedHyps do
+    if (← hyp.getType).containsFVar fvar then
+      addUnusedRelevantHypothesis hyp
+
+/--
+Diagnose spurious counter examples, currently this checks:
+- Whether uninterpreted symbols were used
+- Whether all hypotheses which contain any variable that was bitblasted were included
+-/
+def diagnose : DiagnosisM Unit := do
+  for (_, expr) in ← atomsAssignment do
+    match_expr expr with
+    | BitVec.ofBool x =>
+      match x with
+      | .fvar fvarId => checkRelevantHypsUsed fvarId
+      | _ => addUninterpretedSymbol expr
+    | _ =>
+      match expr with
+      | .fvar fvarId => checkRelevantHypsUsed fvarId
+      | _ => addUninterpretedSymbol expr
+
+end DiagnosisM
+
+def uninterpretedExplainer (d : Diagnosis) : Option MessageData := do
+  guard !d.uninterpretedSymbols.isEmpty
+  let symList := d.uninterpretedSymbols.toList
+  return m!"It abstracted the following unsupported expressions as opaque variables: {symList}"
+
+def unusedRelevantHypothesesExplainer (d : Diagnosis) : Option MessageData := do
+  guard !d.unusedRelevantHypotheses.isEmpty
+  let hypList := d.unusedRelevantHypotheses.toList.map mkFVar
+  return m!"The following potentially relevant hypotheses could not be used: {hypList}"
+
+def explainers : List (Diagnosis → Option MessageData) :=
+  [uninterpretedExplainer, unusedRelevantHypothesesExplainer]
+
+def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
+  let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
+  let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
+  let explanations := explainers.foldl (init := #[]) folder
+
+  if explanations.isEmpty then
+    return m!"The prover found a counterexample, consider the following assignment:\n"
+  else
+    let mut err := m!"The prover found a potentially spurious counterexample:\n"
+    err := err ++ explanations.foldl (init := m!"") (fun acc exp => acc ++ m!"- " ++ exp ++ m!"\n")
+    err := err ++ m!"Consider the following assignment:\n"
+    return err
+
+def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat Expr) :
     MetaM UnsatProver.Result := do
+  let bvExpr := reflectionResult.bvExpr
   let entry ←
     withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
       -- lazyPure to prevent compiler lifting
-      IO.lazyPure (fun _ => bv.bitblast)
+      IO.lazyPure (fun _ => bvExpr.bitblast)
   let aigSize := entry.aig.decls.size
   trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
 
@@ -108,18 +200,25 @@ def lratBitblaster (cfg : TacticContext) (bv : BVLogicalExpr)
 
   match res with
   | .ok cert =>
-    let proof ← cert.toReflectionProof cfg bv ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+    let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
     return ⟨proof, cert⟩
   | .error assignment =>
     let reconstructed := reconstructCounterExample map assignment aigSize atomsAssignment
-    let mut error := m!"The prover found a potential counterexample, consider the following assignment:\n"
+    let mut error ← explainCounterExampleQuality reflectionResult.unusedHypotheses atomsAssignment
     for (var, value) in reconstructed do
       error := error ++ m!"{var} = {value.bv}\n"
     throwError error
 
-def reflectBV (g : MVarId) : M (BVLogicalExpr × (Expr → M Expr)) := g.withContext do
-  let hyps ← getLocalHyps
-  let sats ← hyps.filterMapM SatAtBVLogical.of
+
+def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
+  let hyps ← getPropHyps
+  let mut sats := #[]
+  let mut unusedHypotheses := {}
+  for hyp in hyps do
+    if let some reflected ← SatAtBVLogical.of (mkFVar hyp) then
+      sats := sats.push reflected
+    else
+      unusedHypotheses := unusedHypotheses.insert hyp
   if sats.size = 0 then
     let mut error := "None of the hypotheses are in the supported BitVec fragment.\n"
     error := error ++ "There are two potential fixes for this:\n"
@@ -128,27 +227,32 @@ def reflectBV (g : MVarId) : M (BVLogicalExpr × (Expr → M Expr)) := g.withCon
     error := error ++ "   Consider expressing it in terms of different operations that are better supported."
     throwError error
   let sat := sats.foldl (init := SatAtBVLogical.trivial) SatAtBVLogical.and
-  return (sat.bvExpr, sat.proveFalse)
+  return {
+    bvExpr := sat.bvExpr,
+    proveFalse := sat.proveFalse,
+    unusedHypotheses := unusedHypotheses
+  }
+
 
 def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
     MetaM LratCert := M.run do
   g.withContext do
-    let (bvLogicalExpr, f) ←
+    let reflectionResult ←
       withTraceNode `bv (fun _ => return "Reflecting goal into BVLogicalExpr") do
         reflectBV g
-    trace[Meta.Tactic.bv] "Reflected bv logical expression: {bvLogicalExpr}"
+    trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
     let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
-    let ⟨bvExprUnsat, cert⟩ ← unsatProver bvLogicalExpr atomsAssignment
-    let proveFalse ← f bvExprUnsat
+    let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment
+    let proveFalse ← reflectionResult.proveFalse bvExprUnsat
     g.assign proveFalse
     return cert
 
 def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM LratCert := M.run do
-  let unsatProver : UnsatProver := fun bvExpr atomsAssignment => do
+  let unsatProver : UnsatProver := fun reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
-      lratBitblaster cfg bvExpr atomsAssignment
+      lratBitblaster cfg reflectionResult atomsAssignment
   closeWithBVReflection g unsatProver
 
 structure Result where

tests/lean/run/bv_counterexample.lean

@@ -3,15 +3,15 @@ import Std.Tactic.BVDecide
 open BitVec
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0xffffffffffffffff#64
 -/
 #guard_msgs in
 example (x : BitVec 64) : x < x + 1 := by
   bv_decide
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0x00000000000001ff#64
 -/
 #guard_msgs in
@@ -43,7 +43,7 @@ def optimized (x : BitVec 32) : BitVec 32 :=
     x &&& 0x0000004F
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0xffffffff#32
 -/
 #guard_msgs in
@@ -53,7 +53,7 @@ example (x : BitVec 32) : pop_spec' x = optimized x := by
 
 -- limit the search domain
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0x0007ffff#32
 -/
 #guard_msgs in
@@ -62,11 +62,49 @@ example (x : BitVec 32) (h1 : x < 0xfffff) : pop_spec' x = optimized x := by
   bv_decide
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0x00000000#32
 y = 0x80000000#32
 ofBool a = 0x1#1
 -/
 #guard_msgs in
 example (x y : BitVec 32) (a : Bool) (h : x < y) : (x = y) ↔ a := by
   bv_decide
+
+-- False counter examples but correctly detected as such.
+/--
+error: The prover found a potentially spurious counterexample:
+- The following potentially relevant hypotheses could not be used: [h]
+Consider the following assignment:
+x = 0xffffffff#32
+y = 0x7fffffff#32
+-/
+#guard_msgs in
+example (x y : BitVec 32) (h : x.toNat = y.toNat) : x = y := by
+  bv_decide
+
+def zeros (w : Nat) : BitVec w := 0#w
+
+/--
+error: The prover found a potentially spurious counterexample:
+- It abstracted the following unsupported expressions as opaque variables: [zeros 32]
+Consider the following assignment:
+x = 0xffffffff#32
+zeros 32 = 0xffffffff#32
+-/
+#guard_msgs in
+example (x : BitVec 32) (h : x = zeros 32) : x = 0 := by
+  bv_decide
+
+/--
+error: The prover found a potentially spurious counterexample:
+- It abstracted the following unsupported expressions as opaque variables: [zeros 32]
+- The following potentially relevant hypotheses could not be used: [h1]
+Consider the following assignment:
+x = 0xffffffff#32
+zeros 32 = 0xffffffff#32
+y = 0xffffffff#32
+-/
+#guard_msgs in
+example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 := by
+  bv_decide

tests/lean/run/bv_unused.lean

@@ -3,7 +3,7 @@ import Std.Tactic.BVDecide
 open BitVec
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 y = 0xffffffffffffffff#64
 -/
 #guard_msgs in