From c61ced3f15fad68fbeaf0158c2bc9fe0af5d2e4d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 4 Nov 2024 11:14:51 +0100 Subject: [PATCH] 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. --- .../Tactic/BVDecide/Frontend/BVDecide.lean | 15 +++++--- .../BVDecide/Frontend/BVDecide/Reflect.lean | 38 ++++++++++++++----- .../Frontend/BVDecide/ReifiedBVExpr.lean | 12 +++--- .../Frontend/BVDecide/ReifiedBVPred.lean | 2 +- .../BVDecide/Frontend/BVDecide/Reify.lean | 6 +-- tests/lean/run/bv_counterexample.lean | 8 ++++ 6 files changed, 57 insertions(+), 24 deletions(-) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 01ce8224aa..d5098d0428 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/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⟩ => diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean index bf4e4680bc..25187d8e57 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean index aeb0526e97..a7e5d1fb55 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean +++ b/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 /-- diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean index 76dae112c4..31cabd742f 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean index 002ed92408..6aaeaf917d 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean +++ b/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 /-- diff --git a/tests/lean/run/bv_counterexample.lean b/tests/lean/run/bv_counterexample.lean index b4a66b8a97..e622ef3350 100644 --- a/tests/lean/run/bv_counterexample.lean +++ b/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