feat: present bv_decide counter examples for UIntX and enums better (#7033)

This PR improves presentation of counter examples for UIntX and enum
inductives in bv_decide.

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

@@ -114,6 +114,7 @@ The result of a spurious counter example diagnosis.
 structure Diagnosis where
   uninterpretedSymbols : Std.HashSet Expr := {}
   unusedRelevantHypotheses : Std.HashSet FVarId := {}
+  derivedEquations : Array (Expr × Expr) := #[]
 
 abbrev DiagnosisM : Type → Type := ReaderT CounterExample <| StateRefT Diagnosis MetaM
 
@@ -124,18 +125,26 @@ def run (x : DiagnosisM Unit) (counterExample : CounterExample) : MetaM Diagnosi
     let (_, issues) ← ReaderT.run x counterExample |>.run {}
     return issues
 
+@[inline]
 def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
   return (← read).unusedHypotheses
 
+@[inline]
 def equations : DiagnosisM (Array (Expr × BVExpr.PackedBitVec)) := do
   return (← read).equations
 
+@[inline]
 def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
   modify fun s => { s with uninterpretedSymbols := s.uninterpretedSymbols.insert e }
 
+@[inline]
 def addUnusedRelevantHypothesis (fvar : FVarId) : DiagnosisM Unit :=
   modify fun s => { s with unusedRelevantHypotheses := s.unusedRelevantHypotheses.insert fvar }
 
+@[inline]
+def addDerivedEquation (var : Expr) (value : Expr) : DiagnosisM Unit :=
+  modify fun s => { s with derivedEquations := s.derivedEquations.push (var, value) }
+
 def checkRelevantHypsUsed (fvar : FVarId) : DiagnosisM Unit := do
   for hyp in ← unusedHyps do
     if (← hyp.getType).containsFVar fvar then
@@ -147,26 +156,51 @@ Diagnose spurious counter examples, currently this checks:
 - Whether all hypotheses which contain any variable that was bitblasted were included
 -/
 def diagnose : DiagnosisM Unit := do
-  for (expr, _) in ← equations do
-    match findRelevantFVar expr with
-    | some fvarId => checkRelevantHypsUsed fvarId
-    | none => addUninterpretedSymbol expr
+  for (var, value) in ← equations do
+    let (var, value) ← transformEquation var value
+    addDerivedEquation var value
+    match var with
+    | .fvar fvarId => checkRelevantHypsUsed fvarId
+    | _ => addUninterpretedSymbol var
 where
-  findRelevantFVar (expr : Expr) : Option FVarId :=
-    match fvarId? expr with
-    | some fvarId => some fvarId
-    | none =>
-      match_expr expr with
-      | BitVec.ofBool x => fvarId? x
-      | UInt8.toBitVec x => fvarId? x
-      | UInt16.toBitVec x => fvarId? x
-      | UInt32.toBitVec x => fvarId? x
-      | UInt64.toBitVec x => fvarId? x
-      | _ => none
-  fvarId? (expr : Expr) : Option FVarId :=
-    match expr with
-    | .fvar fvarId => some fvarId
-    | _ => none
+  transformEquation (var : Expr) (value : BVExpr.PackedBitVec) : DiagnosisM (Expr × Expr) := do
+    if var.isFVar then
+      return (var, toExpr value.bv)
+    else
+      match_expr var with
+      | BitVec.ofBool x =>
+        return (x, toExpr <| value.bv == 1)
+      | UInt8.toBitVec x =>
+        if h : value.w = 8 then
+          return (x, toExpr <| UInt8.mk (h ▸ value.bv))
+        else
+          throwError m!"Value for UInt8 was not 8 bit but {value.w} bit"
+      | UInt16.toBitVec x =>
+        if h : value.w = 16 then
+          return (x, toExpr <| UInt16.mk (h ▸ value.bv))
+        else
+          throwError m!"Value for UInt16 was not 16 bit but {value.w} bit"
+      | UInt32.toBitVec x =>
+        if h : value.w = 32 then
+          return (x, toExpr <| UInt32.mk (h ▸ value.bv))
+        else
+          throwError m!"Value for UInt32 was not 32 bit but {value.w} bit"
+      | UInt64.toBitVec x =>
+        if h : value.w = 64 then
+          return (x, toExpr <| UInt64.mk (h ▸ value.bv))
+        else
+          throwError m!"Value for UInt64 was not 64 bit but {value.w} bit"
+      | _ =>
+        match var with
+        | .app (.const (.str p s) []) arg =>
+          if s == Normalize.enumToBitVecSuffix then
+            let .inductInfo inductiveInfo ← getConstInfo p | unreachable!
+            let ctors := inductiveInfo.ctors
+            let enumVal := mkConst ctors[value.bv.toNat]!
+            return (arg, enumVal)
+          else
+            return (var, toExpr value.bv)
+        | _ => return (var, toExpr value.bv)
 
 
 end DiagnosisM
@@ -189,13 +223,19 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
   let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
   let explanations := explainers.foldl (init := #[]) folder
 
+  let mut err := m!""
+
   if explanations.isEmpty then
-    return m!"The prover found a counterexample, consider the following assignment:\n"
+    err := err ++ 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 ++ 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
+
+
+  let folder := fun error (var, value) => error ++ m!"{var} = {value}\n"
+  err := diagnosis.derivedEquations.foldl (init := err) folder
+  return err
 
 def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
@@ -314,9 +354,7 @@ def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
   | .error counterExample =>
     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)
+      throwError (← addMessageContextFull error)
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
 def evalBvDecide : Tactic := fun

tests/lean/run/5674.lean

@@ -4,7 +4,7 @@ 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
+b = 0#64
 -/
 #guard_msgs in
 example

tests/lean/run/bv_counterexample.lean

@@ -4,7 +4,7 @@ open BitVec
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 0xffffffffffffffff#64
+x = 18446744073709551615#64
 -/
 #guard_msgs in
 example (x : BitVec 64) : x < x + 1 := by
@@ -12,7 +12,7 @@ example (x : BitVec 64) : x < x + 1 := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 0x00000000000001ff#64
+x = 511#64
 -/
 #guard_msgs in
 example (x : BitVec 64) (h : x < 512) : x ^^^ x ≠ 0 := by
@@ -44,7 +44,7 @@ def optimized (x : BitVec 32) : BitVec 32 :=
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 0xffffffff#32
+x = 4294967295#32
 -/
 #guard_msgs in
 example (x : BitVec 32) : pop_spec' x = optimized x := by
@@ -54,7 +54,7 @@ example (x : BitVec 32) : pop_spec' x = optimized x := by
 -- limit the search domain
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 0x0007ffff#32
+x = 524287#32
 -/
 #guard_msgs in
 example (x : BitVec 32) (h1 : x < 0xfffff) : pop_spec' x = optimized x := by
@@ -63,9 +63,9 @@ example (x : BitVec 32) (h1 : x < 0xfffff) : pop_spec' x = optimized x := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 0x00000000#32
-y = 0x80000000#32
-ofBool a = 0x1#1
+x = 0#32
+y = 2147483648#32
+a = true
 -/
 #guard_msgs in
 example (x y : BitVec 32) (a : Bool) (h : x < y) : (x = y) ↔ a := by
@@ -76,8 +76,8 @@ example (x y : BitVec 32) (a : Bool) (h : x < y) : (x = y) ↔ a := by
 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
+x = 4294967295#32
+y = 2147483647#32
 -/
 #guard_msgs in
 example (x y : BitVec 32) (h : x.toNat = y.toNat) : x = y := by
@@ -89,8 +89,8 @@ 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
+x = 4294967295#32
+zeros 32 = 4294967295#32
 -/
 #guard_msgs in
 example (x : BitVec 32) (h : x = zeros 32) : x = 0 := by
@@ -101,9 +101,9 @@ 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
+x = 4294967295#32
+zeros 32 = 4294967295#32
+y = 4294967295#32
 -/
 #guard_msgs in
 example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 := by
@@ -111,7 +111,7 @@ example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 :
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 0x3#2
+x = 3#2
 -/
 #guard_msgs in
 example (x : BitVec 2) : (bif x.ult 1#2 then 1#2 else 2#2) == 3#2 := by

tests/lean/run/bv_enums.lean

@@ -60,6 +60,15 @@ structure Pair where
 example (a : Pair) (h : a.x > 0) : a.s = .s2 := by
   bv_decide
 
+/--
+error: The prover found a counterexample, consider the following assignment:
+x = 0#16
+s = State.s1
+-/
+#guard_msgs in
+example (x : BitVec 16) (s : State) (h1 : s = .s1 ↔ x = 0) (h : s = .s1) : x > 0 := by
+  bv_decide
+
 end Ex2
 
 namespace Ex3

tests/lean/run/bv_uint.lean

@@ -6,8 +6,8 @@ example (a b c : UInt8) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a.toBitVec = 0xff#8
-b.toBitVec = 0xff#8
+a = 255
+b = 255
 -/
 #guard_msgs in
 example (a b : UInt8) : a + b > a := by
@@ -21,8 +21,8 @@ example (a b c : UInt16) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a.toBitVec = 0xffff#16
-b.toBitVec = 0xffff#16
+a = 65535
+b = 65535
 -/
 #guard_msgs in
 example (a b : UInt16) : a + b > a := by
@@ -36,8 +36,8 @@ example (a b c : UInt32) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a.toBitVec = 0xffffffff#32
-b.toBitVec = 0xffffffff#32
+a = 4294967295
+b = 4294967295
 -/
 #guard_msgs in
 example (a b : UInt32) : a + b > a := by
@@ -51,8 +51,8 @@ example (a b c : UInt64) (h1 : a < b) (h2 : b < c) : a < c := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-a.toBitVec = 0xffffffffffffffff#64
-b.toBitVec = 0xffffffffffffffff#64
+a = 18446744073709551615
+b = 18446744073709551615
 -/
 #guard_msgs in
 example (a b : UInt64) : a + b > a := by

tests/lean/run/bv_unused.lean

@@ -4,7 +4,7 @@ open BitVec
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-y = 0xffffffffffffffff#64
+y = 18446744073709551615#64
 -/
 #guard_msgs in
 example {y : BitVec 64} : zeroExtend 32 y = 0 := by