From 060b2fe46fe728934744ee52271b92ab74cbd5b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 27 Mar 2025 18:40:12 +0100 Subject: [PATCH] perf: more sharing and caching in bv_decide's reflection (#7698) This PR adds more sharing and caching procedures to bv_decide's reflection step. In particular we cache the reflection proof better, enforce better term sharing in the reflected term, which in turn speeds up bitblasting as bitblaster cache lookups can be checked with pointer equality. This PR was motivated by SMTLIB problem `QF_BV/Sage2/bench_7415.smt2` --- .../Tactic/BVDecide/Frontend/BVCheck.lean | 6 +- .../Tactic/BVDecide/Frontend/BVDecide.lean | 70 ++++++++- .../BVDecide/Frontend/BVDecide/Reflect.lean | 63 ++++++++- .../Frontend/BVDecide/ReifiedBVExpr.lean | 4 +- .../Frontend/BVDecide/ReifiedBVLogical.lean | 17 +-- .../Frontend/BVDecide/ReifiedBVPred.lean | 23 +-- .../Frontend/BVDecide/ReifiedLemmas.lean | 15 +- .../BVDecide/Frontend/BVDecide/Reify.lean | 133 +++++++++--------- .../Elab/Tactic/BVDecide/Frontend/LRAT.lean | 56 -------- 9 files changed, 226 insertions(+), 161 deletions(-) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean index ba7b1eebc6..9841e17d05 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean @@ -35,15 +35,15 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta /-- Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`. -/ -def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do +def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs - cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true + cert.toReflectionProof ctx reflectionResult @[inherit_doc Lean.Parser.Tactic.bvCheck] def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do let unsatProver : UnsatProver := fun _ reflectionResult _ => do withTraceNode `Meta.Tactic.sat (fun _ => return "Preparing LRAT reflection term") do - let proof ← lratChecker ctx reflectionResult.bvExpr + let proof ← lratChecker ctx reflectionResult return .ok ⟨proof, ""⟩ let _ ← closeWithBVReflection g unsatProver return () diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index adda1025dc..393c2114eb 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -79,9 +79,22 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar return finalMap structure ReflectionResult where + /-- + The reflected expression. + -/ bvExpr : BVLogicalExpr + /-- + Function to prove `False` given a satisfiability proof of `bvExpr` + -/ proveFalse : Expr → M Expr + /-- + Set of unused hypotheses for diagnostic purposes. + -/ unusedHypotheses : Std.HashSet FVarId + /-- + A cache for `toExpr bvExpr`. + -/ + expr : Expr /-- A counter example generated from the bitblaster. @@ -257,6 +270,54 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa err := diagnosis.derivedEquations.foldl (init := err) folder return err +/-- +Turn an `LratCert` into a proof that some `reflectedExpr` is UNSAT. +-/ +def LratCert.toReflectionProof (cert : LratCert) (cfg : TacticContext) + (reflectionResult : ReflectionResult) : MetaM Expr := do + withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling expr term") do + mkAuxDecl cfg.exprDef reflectionResult.expr (mkConst ``BVLogicalExpr) + + withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling proof certificate term") do + mkAuxDecl cfg.certDef (toExpr cert) (mkConst ``String) + + let reflectedExpr := mkConst cfg.exprDef + let certExpr := mkConst cfg.certDef + + withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do + let auxValue := mkApp2 (mkConst ``verifyBVExpr) reflectedExpr certExpr + mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool) + + let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true) + let auxProof := + mkApp3 + (mkConst ``Lean.ofReduceBool) + (mkConst cfg.reflectionDef) + (toExpr true) + (← mkEqRefl (toExpr true)) + try + let auxLemma ← + -- disable async TC so we can catch its exceptions + withOptions (Elab.async.set · false) do + withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do + mkAuxLemma [] auxType auxProof + return mkApp3 (mkConst ``unsat_of_verifyBVExpr_eq_true) reflectedExpr certExpr (mkConst auxLemma) + catch e => + throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}" +where + /-- + Add an auxiliary declaration. Only used to create constants that appear in our reflection proof. + -/ + mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit := + addAndCompile <| .defnDecl { + name := name, + levelParams := [], + type := type, + value := value, + hints := .abbrev, + safety := .safe + } + def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) : MetaM (Except CounterExample UnsatProver.Result) := do @@ -287,14 +348,13 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref match res with | .ok cert => trace[Meta.Tactic.sat] "SAT solver found a proof." - let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true + let proof ← cert.toReflectionProof ctx reflectionResult 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 { goal, unusedHypotheses := reflectionResult.unusedHypotheses, equations } - def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do let hyps ← getPropHyps let mut sats := #[] @@ -314,12 +374,12 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do else let sat := sats[1:].foldl (init := sats[0]) SatAtBVLogical.and return { - bvExpr := sat.bvExpr, + bvExpr := ShareCommon.shareCommon sat.bvExpr, proveFalse := sat.proveFalse, - unusedHypotheses := unusedHypotheses + unusedHypotheses := unusedHypotheses, + expr := sat.expr } - def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) : MetaM (Except CounterExample LratCert) := M.run do g.withContext do diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean index 328f9f595b..f221c90f9c 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean @@ -142,6 +142,11 @@ structure State where contained in `atoms`. -/ atomsAssignmentCache : Option Expr := none + /-- + Cached calls to `evalsAtAtoms` of various reflection structures. Whenever `atoms` is modified + this cache is invalidated as `evalsAtAtoms` relies on `atoms`. + -/ + evalsAtCache : Std.HashMap Expr (Option Expr) := {} /-- The reflection monad, used to track `BitVec` variables that we see as we traverse the context. @@ -158,14 +163,26 @@ structure ReifiedBVExpr where -/ bvExpr : BVExpr width /-- - A proof that `bvExpr.eval atomsAssignment = originalBVExpr`, none if it holds by `rfl`. + The expression that was reflected, used for caching of `evalsAtAtoms`. -/ - evalsAtAtoms : M (Option Expr) + originalExpr : Expr + /-- + A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`. + -/ + evalsAtAtoms' : M (Option Expr) /-- A cache for `toExpr bvExpr`. -/ expr : Expr +def ReifiedBVExpr.evalsAtAtoms (reified : ReifiedBVExpr) : M (Option Expr) := do + match (← get).evalsAtCache[reified.originalExpr]? with + | some hit => return hit + | none => + let proof? ← reified.evalsAtAtoms' + modify fun s => { s with evalsAtCache := s.evalsAtCache.insert reified.originalExpr proof? } + return proof? + /-- A reified version of an `Expr` representing a `BVPred`. -/ @@ -175,14 +192,26 @@ structure ReifiedBVPred where -/ bvPred : BVPred /-- - A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`, none if it holds by `rfl`. + The expression that was reflected, usef for caching of `evalsAtAtoms`. -/ - evalsAtAtoms : M (Option Expr) + originalExpr : Expr + /-- + A proof that `bvPred.eval atomsAssignment = originalExpr`, none if it holds by `rfl`. + -/ + evalsAtAtoms' : M (Option Expr) /-- A cache for `toExpr bvPred` -/ expr : Expr +def ReifiedBVPred.evalsAtAtoms (reified : ReifiedBVPred) : M (Option Expr) := do + match (← get).evalsAtCache[reified.originalExpr]? with + | some hit => return hit + | none => + let proof? ← reified.evalsAtAtoms' + modify fun s => { s with evalsAtCache := s.evalsAtCache.insert reified.originalExpr proof? } + return proof? + /-- A reified version of an `Expr` representing a `BVLogicalExpr`. -/ @@ -192,14 +221,26 @@ structure ReifiedBVLogical where -/ bvExpr : BVLogicalExpr /-- - A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`, none if it holds by `rfl`. + The expression that was reflected, usef for caching of `evalsAtAtoms`. -/ - evalsAtAtoms : M (Option Expr) + originalExpr : Expr + /-- + A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`. + -/ + evalsAtAtoms' : M (Option Expr) /-- A cache for `toExpr bvExpr` -/ expr : Expr +def ReifiedBVLogical.evalsAtAtoms (reified : ReifiedBVLogical) : M (Option Expr) := do + match (← get).evalsAtCache[reified.originalExpr]? with + | some hit => return hit + | none => + let proof? ← reified.evalsAtAtoms' + modify fun s => { s with evalsAtCache := s.evalsAtCache.insert reified.originalExpr proof? } + return proof? + /-- A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true. -/ @@ -266,7 +307,15 @@ def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do trace[Meta.Tactic.bv] "New atom of width {width}, synthetic? {synthetic}: {e}" let ident ← modifyGetThe State fun s => let newAtom := { width, synthetic, atomNumber := s.atoms.size} - (s.atoms.size, { s with atoms := s.atoms.insert e newAtom, atomsAssignmentCache := none }) + let newAtomNumber := s.atoms.size + let s := { + s with + atoms := s.atoms.insert e newAtom, + -- must clear the caches as they depend on `atoms`. + atomsAssignmentCache := none + evalsAtCache := {} + } + (newAtomNumber, s) return ident @[specialize] diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean index ff3853ec33..68adfc54f6 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean @@ -39,7 +39,7 @@ def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident) -- This is safe because this proof always holds definitionally. let proof := pure none - return ⟨width, .var ident, proof, expr⟩ + return ⟨width, .var ident, expr, proof, expr⟩ /-- Parse `expr` as a `Nat` or `BitVec` constant depending on `ty`. @@ -71,7 +71,7 @@ def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val) -- This is safe because this proof always holds definitionally. let proof := pure none - return ⟨w, bvExpr, proof, expr⟩ + return ⟨w, bvExpr, toExpr val, proof, expr⟩ end ReifiedBVExpr diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean index 2700b9718d..e9b422dc73 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean @@ -33,8 +33,9 @@ Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom. def ofPred (bvPred : ReifiedBVPred) : M ReifiedBVLogical := do let boolExpr := .literal bvPred.bvPred let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr + -- important: This must be the same proof as the bvPred one in order for the cache to be correct let proof := bvPred.evalsAtAtoms - return ⟨boolExpr, proof, expr⟩ + return ⟨boolExpr, bvPred.originalExpr, proof, expr⟩ /-- Construct an uninterrpeted `Bool` atom from `t`. @@ -51,14 +52,14 @@ def mkBoolConst (val : Bool) : M ReifiedBVLogical := do let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val) -- This is safe because this proof always holds definitionally. let proof := pure none - return ⟨boolExpr, proof, expr⟩ + return ⟨boolExpr, toExpr val, proof, expr⟩ /-- Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`. This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs` and `rhs`. -/ -def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) : +def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) (origExpr : Expr) : M ReifiedBVLogical := do let congrThm := congrThmOfGate gate let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr @@ -84,7 +85,7 @@ def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) : lhsExpr rhsExpr lhsEvalExpr rhsEvalExpr lhsProof rhsProof - return ⟨boolExpr, proof, expr⟩ + return ⟨boolExpr, origExpr, proof, expr⟩ where congrThmOfGate (gate : Gate) : Name := match gate with @@ -97,7 +98,7 @@ where Construct the reified version of `Bool.not subExpr`. This function assumes that `subExpr` is the expression corresponding to `sub`. -/ -def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do +def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) (origExpr : Expr) : M ReifiedBVLogical := do let boolExpr := .not sub.bvExpr let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr let proof := do @@ -105,14 +106,14 @@ def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do let some subProof ← sub.evalsAtAtoms | return none let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof - return ⟨boolExpr, proof, expr⟩ + return ⟨boolExpr, origExpr, proof, expr⟩ /-- Construct the reified version of `if discrExpr then lhsExpr else rhsExpr`. This function assumes that `discrExpr`, lhsExpr` and `rhsExpr` are the corresponding expressions to `discr`, `lhs` and `rhs`. -/ -def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) : +def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) (origExpr : Expr) : M ReifiedBVLogical := do let boolExpr := .ite discr.bvExpr lhs.bvExpr rhs.bvExpr let expr := @@ -140,7 +141,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) discrExpr lhsExpr rhsExpr discrEvalExpr lhsEvalExpr rhsEvalExpr discrProof lhsProof rhsProof - return ⟨boolExpr, proof, expr⟩ + return ⟨boolExpr, origExpr, proof, expr⟩ end ReifiedBVLogical diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean index d700b43be1..c6c46f1f0d 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean @@ -19,9 +19,9 @@ open Lean.Meta namespace ReifiedBVPred /-- -Construct an uninterpreted `Bool` atom from `t`. +Construct an uninterpreted `Bool` atom from `origExpr`. -/ -def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do +def boolAtom (origExpr : Expr) : M (Option ReifiedBVPred) := do /- Idea: we have t : Bool here, let's construct: BitVec.ofBool t : BitVec 1 @@ -29,9 +29,9 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do BitVec.getLsb (BitVec.ofBool t) 0 : Bool We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred. -/ - let ty ← inferType t + let ty ← inferType origExpr let_expr Bool := ty | return none - let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 false + let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) origExpr) 1 false let bvExpr : BVPred := .getLsbD atom.bvExpr 0 let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0) let proof := do @@ -41,18 +41,18 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do let atomProof := (← atom.evalsAtAtoms).getD (ReifiedBVExpr.mkBVRefl atom.width atomEval) return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr) - t + origExpr atomEval atomProof - return some ⟨bvExpr, proof, expr⟩ + return some ⟨bvExpr, origExpr, proof, expr⟩ /-- Construct the reified version of applying the predicate in `pred` to `lhs` and `rhs`. This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs` and `rhs`. -/ -def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred) : - M (Option ReifiedBVPred) := do +def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred) + (origExpr : Expr) : M (Option ReifiedBVPred) := do if h : lhs.width = rhs.width then let congrThm := congrThmofBinPred pred let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr) @@ -79,7 +79,7 @@ def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPr lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof - return some ⟨bvExpr, proof, expr⟩ + return some ⟨bvExpr, origExpr, proof, expr⟩ else return none where @@ -92,7 +92,8 @@ where Construct the reified version of `BitVec.getLsbD subExpr idx`. This function assumes that `subExpr` is the expression corresponding to `sub`. -/ -def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPred := do +def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) (origExpr : Expr) : + M ReifiedBVPred := do let bvExpr : BVPred := .getLsbD sub.bvExpr idx let idxExpr := toExpr idx let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr @@ -107,7 +108,7 @@ def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPr subExpr subEval subProof - return ⟨bvExpr, proof, expr⟩ + return ⟨bvExpr, origExpr, proof, expr⟩ end ReifiedBVPred diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean index 554d3c2203..9739acae73 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean @@ -37,15 +37,16 @@ where let resValExpr := lhs let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true - let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr - let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr + let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr notDiscrExpr let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr] - let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none + let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq eqBVExpr + | return none let eqBV ← ReifiedBVLogical.ofPred eqBVPred - let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or + let orExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr + let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or orExpr let proof := do let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr @@ -70,10 +71,12 @@ where let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_false let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr] - let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none + let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq eqBVExpr + | return none let eqBV ← ReifiedBVLogical.ofPred eqBVPred - let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or + let orExpr := mkApp2 (mkConst ``Bool.or) discrExpr eqBVExpr + let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or orExpr let proof := do let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean index d5132acd05..4de8aa46ed 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean @@ -24,29 +24,29 @@ Reify an `Expr` that's a constant-width `BitVec`. Unless this function is called on something that is not a constant-width `BitVec` it is always going to return `some`. -/ -partial def ReifiedBVExpr.of (x : Expr) : LemmaM (Option ReifiedBVExpr) := do - goOrAtom x +partial def ReifiedBVExpr.of (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do + goOrAtom origExpr where /-- Reify `x`, returns `none` if the reification procedure failed. -/ - go (x : Expr) : LemmaM (Option ReifiedBVExpr) := do - match_expr x with - | BitVec.ofNat _ _ => goBvLit x + go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do + match_expr origExpr with + | BitVec.ofNat _ _ => goBvLit origExpr | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr + binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr origExpr | HXor.hXor _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr + binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr origExpr | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr + binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr origExpr | HMul.hMul _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr + binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr origExpr | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr + binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr origExpr | HMod.hMod _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr + binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr origExpr | Complement.complement _ _ innerExpr => - unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr + unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr origExpr | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr => let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr if distance?.isSome then throwError "internal error: constant shift should have been eliminated." @@ -57,6 +57,7 @@ where .shiftLeft ``BVExpr.shiftLeft ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr + origExpr | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr => let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr if distance?.isSome then throwError "internal error: constant shift should have been eliminated." @@ -67,6 +68,7 @@ where .shiftRight ``BVExpr.shiftRight ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr + origExpr | BitVec.sshiftRight _ innerExpr distanceExpr => let some distance ← getNatValue? distanceExpr | return none shiftConstLikeReflection @@ -75,6 +77,7 @@ where .arithShiftRightConst ``BVUnOp.arithShiftRightConst ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr + origExpr | BitVec.sshiftRight' _ _ innerExpr distanceExpr => shiftReflection distanceExpr @@ -82,6 +85,7 @@ where .arithShiftRight ``BVExpr.arithShiftRight ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr + origExpr | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr => let some lhs ← goOrAtom lhsExpr | return none let some rhs ← goOrAtom rhsExpr | return none @@ -109,7 +113,7 @@ where lhsExpr lhsEval rhsExpr rhsEval lhsProof rhsProof - return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩ + return some ⟨lhs.width + rhs.width, bvExpr, origExpr, proof, expr⟩ | BitVec.replicate _ nExpr innerExpr => let some inner ← goOrAtom innerExpr | return none let some n ← getNatValue? nExpr | return none @@ -132,7 +136,7 @@ where innerExpr innerEval innerProof - return some ⟨inner.width * n, bvExpr, proof, expr⟩ + return some ⟨inner.width * n, bvExpr, origExpr, proof, expr⟩ | BitVec.extractLsb' _ startExpr lenExpr innerExpr => let some start ← getNatValue? startExpr | return none let some len ← getNatValue? lenExpr | return none @@ -154,7 +158,7 @@ where innerExpr innerEval innerProof - return some ⟨len, bvExpr, proof, expr⟩ + return some ⟨len, bvExpr, origExpr, proof, expr⟩ | BitVec.rotateLeft _ innerExpr distanceExpr => rotateReflection distanceExpr @@ -162,6 +166,7 @@ where .rotateLeft ``BVUnOp.rotateLeft ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr + origExpr | BitVec.rotateRight _ innerExpr distanceExpr => rotateReflection distanceExpr @@ -169,29 +174,30 @@ where .rotateRight ``BVUnOp.rotateRight ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr + origExpr | cond _ discrExpr lhsExpr rhsExpr => - let some atom ← ReifiedBVExpr.bitVecAtom x true | return none + let some atom ← ReifiedBVExpr.bitVecAtom origExpr 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 - addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr + addCondLemmas discr atom lhs rhs discrExpr origExpr lhsExpr rhsExpr return some atom | _ => return none /-- - Reify `x` or abstract it as an atom. + Reify `origExpr` or abstract it as an atom. Unless this function is called on something that is not a fixed-width `BitVec` it is always going to return `some`. -/ - goOrAtom (x : Expr) : LemmaM (Option ReifiedBVExpr) := do - LemmaM.withBVExprCache x fun x => do - let res ← go x + goOrAtom (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do + LemmaM.withBVExprCache origExpr fun origExpr => do + let res ← go origExpr match res with | some exp => return some exp - | none => ReifiedBVExpr.bitVecAtom x false + | none => ReifiedBVExpr.bitVecAtom origExpr false shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp) - (shiftOpName : Name) (congrThm : Name) : + (shiftOpName : Name) (congrThm : Name) (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do let some inner ← goOrAtom innerExpr | return none let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr @@ -206,17 +212,17 @@ where (mkConst congrThm) (toExpr distance) let proof := unaryCongrProof inner innerExpr congrProof - return some ⟨inner.width, bvExpr, proof, expr⟩ + return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩ rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp) - (rotateOpName : Name) (congrThm : Name) : + (rotateOpName : Name) (congrThm : Name) (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do let some distance ← getNatValue? distanceExpr | return none - shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm + shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm origExpr shiftReflection (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name) - (congrThm : Name) : + (congrThm : Name) (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do let some inner ← goOrAtom innerExpr | return none let some distance ← goOrAtom distanceExpr | return none @@ -234,9 +240,9 @@ where (toExpr inner.width) (toExpr distance.width) let proof := binaryCongrProof inner distance innerExpr distanceExpr congrProof - return some ⟨inner.width, bvExpr, proof, expr⟩ + return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩ - binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) : + binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do let some lhs ← goOrAtom lhsExpr | return none let some rhs ← goOrAtom rhsExpr | return none @@ -245,7 +251,7 @@ where let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr let congrThm := mkApp (mkConst congrThm) (toExpr lhs.width) let proof := binaryCongrProof lhs rhs lhsExpr rhsExpr congrThm - return some ⟨lhs.width, bvExpr, proof, expr⟩ + return some ⟨lhs.width, bvExpr, origExpr, proof, expr⟩ else return none @@ -262,13 +268,13 @@ where rhsEval rhsProof? | return none return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof - unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) : + unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do let some inner ← goOrAtom innerExpr | return none let bvExpr := .un op inner.bvExpr let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr let proof := unaryCongrProof inner innerExpr (mkConst congrThm) - return some ⟨inner.width, bvExpr, proof, expr⟩ + return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩ unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M (Option Expr) := do let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr @@ -283,82 +289,83 @@ where Reify an `Expr` that is a predicate about `BitVec`. Unless this function is called on something that is not a `Bool` it is always going to return `some`. -/ -partial def ReifiedBVPred.of (t : Expr) : LemmaM (Option ReifiedBVPred) := do - LemmaM.withBVPredCache t fun t => do - match ← go t with +partial def ReifiedBVPred.of (origExpr : Expr) : LemmaM (Option ReifiedBVPred) := do + LemmaM.withBVPredCache origExpr fun origExpr => do + match ← go origExpr with | some pred => return some pred - | none => ReifiedBVPred.boolAtom t + | none => ReifiedBVPred.boolAtom origExpr where /-- - Reify `t`, returns `none` if the reification procedure failed. + Reify `origExpr`, returns `none` if the reification procedure failed. -/ - go (t : Expr) : LemmaM (Option ReifiedBVPred) := do - match_expr t with + go (origExpr : Expr) : LemmaM (Option ReifiedBVPred) := do + match_expr origExpr with | BEq.beq α _ lhsExpr rhsExpr => let_expr BitVec _ := α | return none - binaryReflection lhsExpr rhsExpr .eq + binaryReflection lhsExpr rhsExpr .eq origExpr | BitVec.ult _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .ult + binaryReflection lhsExpr rhsExpr .ult origExpr | BitVec.getLsbD _ subExpr idxExpr => let some sub ← ReifiedBVExpr.of subExpr | return none let some idx ← getNatValue? idxExpr | return none - return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx) + return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx origExpr) | _ => return none - binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) : LemmaM (Option ReifiedBVPred) := do + binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (origExpr : Expr) : + LemmaM (Option ReifiedBVPred) := do let some lhs ← ReifiedBVExpr.of lhsExpr | return none let some rhs ← ReifiedBVExpr.of rhsExpr | return none - ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred + ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred origExpr /-- Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms. Unless this function is called on something that is not a `Bool` it is always going to return `some`. -/ -partial def ReifiedBVLogical.of (t : Expr) : LemmaM (Option ReifiedBVLogical) := do - goOrAtom t +partial def ReifiedBVLogical.of (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do + goOrAtom origExpr where /-- Reify `t`, returns `none` if the reification procedure failed. -/ - go (t : Expr) : LemmaM (Option ReifiedBVLogical) := do - match_expr t with + go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do + match_expr origExpr with | Bool.true => ReifiedBVLogical.mkBoolConst true | Bool.false => ReifiedBVLogical.mkBoolConst false | Bool.not subExpr => let some sub ← goOrAtom subExpr | return none - return some (← ReifiedBVLogical.mkNot sub subExpr) - | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and - | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor + return some (← ReifiedBVLogical.mkNot sub subExpr origExpr) + | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and origExpr + | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor origExpr | BEq.beq α _ lhsExpr rhsExpr => match_expr α with - | Bool => gateReflection lhsExpr rhsExpr .beq - | BitVec _ => goPred t + | Bool => gateReflection lhsExpr rhsExpr .beq origExpr + | BitVec _ => goPred origExpr | _ => return none | cond _ discrExpr lhsExpr rhsExpr => let some discr ← goOrAtom discrExpr | return none let some lhs ← goOrAtom lhsExpr | return none let some rhs ← goOrAtom rhsExpr | return none - return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr) - | _ => goPred t + return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr origExpr) + | _ => goPred origExpr /-- Reify `t` or abstract it as an atom. Unless this function is called on something that is not a `Bool` it is always going to return `some`. -/ - goOrAtom (t : Expr) : LemmaM (Option ReifiedBVLogical) := do - LemmaM.withBVLogicalCache t fun t => do - match ← go t with + goOrAtom (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do + LemmaM.withBVLogicalCache origExpr fun origExpr => do + match ← go origExpr with | some boolExpr => return some boolExpr - | none => ReifiedBVLogical.boolAtom t + | none => ReifiedBVLogical.boolAtom origExpr - gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) : + gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do let some lhs ← goOrAtom lhsExpr | return none let some rhs ← goOrAtom rhsExpr | return none - ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate + ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate origExpr - goPred (t : Expr) : LemmaM (Option ReifiedBVLogical) := do - let some pred ← ReifiedBVPred.of t | return none + goPred (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do + let some pred ← ReifiedBVPred.of origExpr | return none ReifiedBVLogical.ofPred pred end diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean index f1f28229b1..2b7267a577 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean @@ -148,61 +148,5 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi return .ok lratProof -/-- -Add an auxiliary declaration. Only used to create constants that appear in our reflection proof. --/ -def mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit := - addAndCompile <| .defnDecl { - name := name, - levelParams := [], - type := type, - value := value, - hints := .abbrev, - safety := .safe - } - -/-- -Turn an `LratCert` into a proof that some `reflected` expression is UNSAT by providing a `verifier` -function together with a correctness theorem for it. - -- `verifier` is expected to have type `α → LratCert → Bool` -- `unsat_of_verifier_eq_true` is expected to have type - `∀ (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 - withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling expr term") do - mkAuxDecl cfg.exprDef (toExpr reflected) (toTypeExpr α) - - let certType := toTypeExpr LratCert - - withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling proof certificate term") do - mkAuxDecl cfg.certDef (toExpr cert) certType - - let reflectedExpr := mkConst cfg.exprDef - let certExpr := mkConst cfg.certDef - - withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do - let auxValue := mkApp2 (mkConst verifier) reflectedExpr certExpr - mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool) - - let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true) - let auxProof := - mkApp3 - (mkConst ``Lean.ofReduceBool) - (mkConst cfg.reflectionDef) - (toExpr true) - (← mkEqRefl (toExpr true)) - try - let auxLemma ← - -- disable async TC so we can catch its exceptions - withOptions (Elab.async.set · false) do - withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do - mkAuxLemma [] auxType auxProof - return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma) - catch e => - throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}" - - end Frontend end Lean.Elab.Tactic.BVDecide