feat: introduce synthetic atoms in bv_decide (#5942)

This introduces a notion of synthetic atoms into `bv_decide`'s
reflection framework. An atom can be declared synthetic if its behavior
is fully specified by additional lemmas that are added in the process of
creating it. This is for example useful in the code that handles `if` as
the entire `if` block is abstracted as an atom and then two lemmas to
describe either branch are added. Previously this had the effect of
creating error messages about potentially unsound counterexamples, now
the synthetic atoms get filtered from the counter example generation.

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

@@ -35,9 +35,13 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
 expression - pair values.
 -/
 def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
-    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
     Array (Expr × BVExpr.PackedBitVec) := Id.run do
   let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
+  let filter bvBit _ :=
+    let (_, _, synthetic) := atomsAssignment.get! bvBit.var
+    !synthetic
+  let var2Cnf := var2Cnf.filter filter
   for (bitVar, cnfVar) in var2Cnf.toArray do
     /-
     The setup of the variables in CNF is as follows:
@@ -70,7 +74,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
       if bitValue then
         value := value ||| (1 <<< currentBit)
       currentBit := currentBit + 1
-    let atomExpr := atomsAssignment.get! bitVecVar |>.snd
+    let (_, atomExpr, _) := atomsAssignment.get! bitVecVar
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
@@ -101,7 +105,7 @@ structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := MVarId → ReflectionResult → Std.HashMap Nat (Nat × Expr) →
+abbrev UnsatProver := MVarId → ReflectionResult → Std.HashMap Nat (Nat × Expr × Bool) →
     MetaM (Except CounterExample UnsatProver.Result)
 
 /--
@@ -183,7 +187,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
     return err
 
 def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
     MetaM (Except CounterExample UnsatProver.Result) := do
   let bvExpr := reflectionResult.bvExpr
   let entry ←
@@ -253,7 +257,8 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
         reflectBV g
     trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
-    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
+    let flipper := (fun (expr, {width, atomNumber, synthetic}) => (atomNumber, (width, expr, synthetic)))
+    let atomsPairs := (← getThe State).atoms.toList.map flipper
     let atomsAssignment := Std.HashMap.ofList atomsPairs
     match ← unsatProver g reflectionResult atomsAssignment with
     | .ok ⟨bvExprUnsat, cert⟩ =>

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

@@ -107,6 +107,25 @@ where
 
 open Lean.Meta
 
+/--
+A `BitVec` atom.
+-/
+structure Atom where
+  /--
+  The width of the `BitVec` that is being abstracted.
+  -/
+  width : Nat
+  /--
+  A unique numeric identifier for the atom.
+  -/
+  atomNumber : Nat
+  /--
+  Whether the atom is synthetic. The effect of this is that values for this atom are not considered
+  for the counter example deriviation. This is for example useful when we introduce an atom over
+  an expression, together with additional lemmas that fully describe the behavior of the atom.
+  -/
+  synthetic : Bool
+
 /--
 The state of the reflection monad
 -/
@@ -115,7 +134,7 @@ structure State where
   The atoms encountered so far. Saved as a map from `BitVec` expressions to a (width, atomNumber)
   pair.
   -/
-  atoms : Std.HashMap Expr (Nat × Nat) := {}
+  atoms : Std.HashMap Expr Atom := {}
   /--
   A cache for `atomsAssignment`.
   -/
@@ -208,8 +227,8 @@ def run (m : M α) : MetaM α :=
 Retrieve the atoms as pairs of their width and expression.
 -/
 def atoms : M (List (Nat × Expr)) := do
-  let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.2 < ·.2.2)
-  return sortedAtoms.map (fun (expr, width, _) => (width, expr)) |>.toList
+  let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.atomNumber < ·.2.atomNumber)
+  return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr)) |>.toList
 
 /--
 Retrieve a `BitVec.Assignment` representing the atoms we found so far.
@@ -220,16 +239,17 @@ def atomsAssignment : M Expr := do
 /--
 Look up an expression in the atoms, recording it if it has not previously appeared.
 -/
-def lookup (e : Expr) (width : Nat) : M Nat := do
+def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
   match (← getThe State).atoms[e]? with
-  | some (width', ident) =>
-    if width != width' then
+  | some atom =>
+    if width != atom.width then
       panic! "The same atom occurs with different widths, this is a bug"
-    return ident
+    return atom.atomNumber
   | none =>
-    trace[Meta.Tactic.bv] "New atom of width {width}: {e}"
+    trace[Meta.Tactic.bv] "New atom of width {width}, synthetic? {synthetic}: {e}"
     let ident ← modifyGetThe State fun s =>
-      (s.atoms.size, { s with atoms := s.atoms.insert e (width, s.atoms.size) })
+      let newAtom := { width, synthetic, atomNumber := s.atoms.size}
+      (s.atoms.size, { s with atoms := s.atoms.insert e newAtom })
     updateAtomsAssignment
     return ident
 where

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

@@ -32,10 +32,10 @@ def mkBVRefl (w : Nat) (expr : Expr) : Expr :=
    expr
 
 /--
-Register `e` as an atom of width `width`.
+Register `e` as an atom of `width` that might potentially be `synthetic`.
 -/
-def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
-  let ident ← M.lookup e width
+def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
+  let ident ← M.lookup e width synthetic
   let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
   let proof := do
     let evalExpr ← mkEvalExpr width expr
@@ -55,13 +55,13 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
   | _ => return none
 
 /--
-Construct an uninterpreted `BitVec` atom from `x`.
+Construct an uninterpreted `BitVec` atom from `x`, potentially `synthetic`.
 -/
-def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
+def bitVecAtom (x : Expr) (synthetic : Bool) : M (Option ReifiedBVExpr) := do
   let t ← instantiateMVars (← whnfR (← inferType x))
   let_expr BitVec widthExpr := t | return none
   let some width ← getNatValue? widthExpr | return none
-  let atom ← mkAtom x width
+  let atom ← mkAtom x width synthetic
   return some atom
 
 /--

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

@@ -31,7 +31,7 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
   -/
   let ty ← inferType t
   let_expr Bool := ty | return none
-  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
+  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 false
   let bvExpr : BVPred := .getLsbD atom.bvExpr 0
   let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
   let proof := do

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

@@ -209,7 +209,7 @@ where
       let_expr Eq α discrExpr val := discrExpr | return none
       let_expr Bool := α | return none
       let_expr Bool.true := val | return none
-      let some atom ← ReifiedBVExpr.bitVecAtom x | return none
+      let some atom ← ReifiedBVExpr.bitVecAtom x true | return none
       let some discr ← ReifiedBVLogical.of discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
@@ -226,7 +226,7 @@ where
     let res ← go x
     match res with
     | some exp => return some exp
-    | none => ReifiedBVExpr.bitVecAtom x
+    | none => ReifiedBVExpr.bitVecAtom x false
 
   shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
@@ -316,7 +316,7 @@ where
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x
+    let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x false
     ReifiedBVExpr.mkBVConst bvVal
 
 /--

tests/lean/run/bv_counterexample.lean

@@ -108,3 +108,11 @@ 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
+
+/--
+error: The prover found a counterexample, consider the following assignment:
+x = 0x3#2
+-/
+#guard_msgs in
+example (x : BitVec 2) : (bif x.ult 0#2 then 1#2 else 2#2) == 3#2 := by
+  bv_decide