From c7dec60428d4bf41b0f9f8d34b9a574a41f61ace Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 29 Jan 2025 16:41:38 +0100 Subject: [PATCH] feat: support `UIntX` and `USize` in `bv_decide` (#6711) This PR adds support for `UIntX` and `USize` in `bv_decide` by adding a preprocessor that turns them into `BitVec` of their corresponding size. --- .../Tactic/BVDecide/Frontend/BVDecide.lean | 29 ++- .../Tactic/BVDecide/Frontend/Normalize.lean | 5 + .../BVDecide/Frontend/Normalize/Basic.lean | 3 +- .../Frontend/Normalize/IntToBitVec.lean | 169 ++++++++++++++++++ src/Std/Tactic/BVDecide/Syntax.lean | 5 + tests/lean/run/bv_uint.lean | 78 ++++++++ 6 files changed, 278 insertions(+), 11 deletions(-) create mode 100644 src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean create mode 100644 tests/lean/run/bv_uint.lean diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index bf5bec71de..0eaf990a13 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -148,15 +148,26 @@ Diagnose spurious counter examples, currently this checks: -/ def diagnose : DiagnosisM Unit := do for (expr, _) in ← equations 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 + match findRelevantFVar expr with + | some fvarId => checkRelevantHypsUsed fvarId + | none => addUninterpretedSymbol expr +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 + end DiagnosisM diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean index 34e947a9ef..720cc22489 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean @@ -12,6 +12,7 @@ import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AndFlatten import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.EmbeddedConstraint import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AC import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Structures +import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.IntToBitVec /-! This module contains the implementation of `bv_normalize`, the preprocessing tactic for `bv_decide`. @@ -54,6 +55,10 @@ where let some g' ← structuresPass.run g | return none g := g' + if cfg.fixedInt then + let some g' ← intToBitVecPass.run g | return none + g := g' + trace[Meta.Tactic.bv] m!"Running fixpoint pipeline on:\n{g}" let pipeline ← passPipeline Pass.fixpointPipeline pipeline g diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean index 0e20a4870a..e0723babf1 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean @@ -31,8 +31,7 @@ def getConfig : PreProcessM BVDecideConfig := read @[inline] def checkRewritten (fvar : FVarId) : PreProcessM Bool := do - let val := (← get).rewriteCache.contains fvar - return val + return (← get).rewriteCache.contains fvar @[inline] def rewriteFinished (fvar : FVarId) : PreProcessM Unit := do diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean new file mode 100644 index 0000000000..dfc0f94b18 --- /dev/null +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean @@ -0,0 +1,169 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +prelude +import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic +import Lean.Elab.Tactic.BVDecide.Frontend.Attr +import Lean.Elab.Tactic.Simp + +/-! +This module contains the implementation of the pre processing pass for reducing `UIntX`/`IntX` to +`BitVec` and thus allow `bv_decide` to reason about them. + +It: +1. runs the `int_toBitVec` simp set +2. If `USize.toBitVec` is used anywhere looks for equations of the form + `System.Platform.numBits = constant` (or flipped) and uses them to convert the system back to + fixed width. +-/ + +namespace Lean.Elab.Tactic.BVDecide +namespace Frontend.Normalize + +open Lean.Meta + +/-- +Contains information for the `USize` elimination pass. +-/ +structure USizeState where + /-- + Contains terms of the form `USize.toBitVec e` that we will translate to constant width `BitVec`. + -/ + relevantTerms : Std.HashSet Expr := {} + /-- + Contains all hypotheses that contain terms from `relevantTerms` + -/ + relevantHyps : Std.HashSet FVarId := {} + +private abbrev M := StateRefT USizeState MetaM + +namespace M + +@[inline] +def addUSizeTerm (e : Expr) : M Unit := do + modify fun s => { s with relevantTerms := s.relevantTerms.insert e } + +@[inline] +def addUSizeHyp (f : FVarId) : M Unit := do + modify fun s => { s with relevantHyps := s.relevantHyps.insert f } + +end M + +def intToBitVecPass : Pass where + name := `intToBitVec + run' goal := do + let intToBvThms ← intToBitVecExt.getTheorems + let cfg ← PreProcessM.getConfig + let simpCtx ← Simp.mkContext + (config := { failIfUnchanged := false, zetaDelta := true, maxSteps := cfg.maxSteps }) + (simpTheorems := #[intToBvThms]) + (congrTheorems := (← getSimpCongrTheorems)) + + let hyps ← goal.getNondepPropHyps + let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps) + let some (_, goal) := result? | return none + handleUSize goal |>.run' {} +where + handleUSize (goal : MVarId) : M MVarId := do + if ← detectUSize goal then + replaceUSize goal + else + return goal + + detectUSize (goal : MVarId) : M Bool := do + goal.withContext do + for hyp in ← getPropHyps do + (← hyp.getType).forEachWhere + (stopWhenVisited := true) + (·.isAppOfArity ``USize.toBitVec 1) + fun e => do + M.addUSizeTerm e + M.addUSizeHyp hyp + + return !(← get).relevantTerms.isEmpty + + /-- + Turn `goal` into a goal containing `BitVec const` instead of `USize`. + -/ + replaceUSize (goal : MVarId) : M MVarId := do + if let some (numBits, numBitsEq) ← findNumBitsEq goal then + goal.withContext do + let relevantHyps := (← get).relevantHyps.toArray.map mkFVar + let relevantTerms := (← get).relevantTerms.toArray + let (app, abstractedHyps) ← liftMkBindingM <| MetavarContext.revert relevantHyps goal true + let newMVar := app.getAppFn.mvarId! + let targetType ← newMVar.getType + /- + newMVar has type : h1 → h2 → ... → False` + This code computes a motive of the form: + ``` + fun z _ => ∀ (x_1 : BitVec z) (x_2 : BitVec z) ..., h1 → h2 → ... → False + ``` + Where: + - all terms from `relevantTerms` in the implication are substituted by `x_1`, ... + - all occurences of `numBits` are substituted by `z` + + Additionally we compute a new metavariable with type: + ``` + ∀ (x_1 : BitVec const) (x_2 : BitVec const) ..., h1 → h2 → ... → False + ``` + with all occurences of `numBits` substituted by const. This meta variable is going to become + the next goal + -/ + let (motive, newGoalType) ← + withLocalDeclD `z (mkConst ``Nat) fun z => do + let otherArgType := mkApp3 (mkConst ``Eq [1]) (mkConst ``Nat) (toExpr numBits) z + withLocalDeclD `h otherArgType fun other => do + let argType := mkApp (mkConst ``BitVec) z + let argTypes := relevantTerms.map (fun _ => (`x, argType)) + let innerMotiveType ← + withLocalDeclsDND argTypes fun args => do + let mut subst : Std.HashMap Expr Expr := Std.HashMap.empty (args.size + 1) + subst := subst.insert (mkConst ``System.Platform.numBits) z + for term in relevantTerms, arg in args do + subst := subst.insert term arg + let motiveType := targetType.replace subst.get? + mkForallFVars args motiveType + let newGoalType := innerMotiveType.replaceFVar z (toExpr numBits) + let motive ← mkLambdaFVars #[z, other] innerMotiveType + return (motive, newGoalType) + let mut newGoal := (← mkFreshExprMVar newGoalType).mvarId! + let casesOn := mkApp6 (mkConst ``Eq.casesOn [0, 1]) + (mkConst ``Nat) + (toExpr numBits) + motive + (mkConst ``System.Platform.numBits) + numBitsEq + (mkMVar newGoal) + goal.assign <| mkAppN casesOn (relevantTerms ++ abstractedHyps) + -- remove all of the hold hypotheses about USize.toBitVec to prevent false counter examples + (newGoal, _) ← newGoal.tryClearMany' (abstractedHyps.map Expr.fvarId!) + -- intro both the new `BitVec const` as well as all hypotheses about them + (_, newGoal) ← newGoal.introN (relevantTerms.size + abstractedHyps.size) + return newGoal + else + logWarning m!"Detected USize in the goal but no hypothesis about System.Platform.numBits, consider case splitting on {mkConst ``System.Platform.numBits_eq}" + return goal + + /-- + Builds an expression of type: `const = System.Platform.numBits` from the hypotheses in the context + if possible. + -/ + findNumBitsEq (goal : MVarId) : MetaM (Option (Nat × Expr)) := do + goal.withContext do + for hyp in ← getPropHyps do + match_expr ← hyp.getType with + | Eq eqTyp lhs rhs => + if lhs.isConstOf ``System.Platform.numBits then + let some val ← getNatValue? rhs | return none + return some (val, mkApp4 (mkConst ``Eq.symm [1]) eqTyp lhs rhs (mkFVar hyp)) + else if rhs.isConstOf ``System.Platform.numBits then + let some val ← getNatValue? lhs | return none + return some (val, mkFVar hyp) + | _ => continue + return none + +end Frontend.Normalize +end Lean.Elab.Tactic.BVDecide diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean index 902faa21a7..8de03b3e4c 100644 --- a/src/Std/Tactic/BVDecide/Syntax.lean +++ b/src/Std/Tactic/BVDecide/Syntax.lean @@ -44,6 +44,11 @@ structure BVDecideConfig where -/ structures : Bool := true /-- + Enable preprocessing with the `int_toBitVec` simp set to reduce `UIntX`/`IntX` to `BitVec` and + thus make them accessible for `bv_decide`. + -/ + fixedInt : Bool := true + /-- Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the Lean process. -/ diff --git a/tests/lean/run/bv_uint.lean b/tests/lean/run/bv_uint.lean new file mode 100644 index 0000000000..dc7dab4211 --- /dev/null +++ b/tests/lean/run/bv_uint.lean @@ -0,0 +1,78 @@ +import Std.Tactic.BVDecide + +/-! UInt8 -/ +example (a b c : UInt8) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a.toBitVec = 0xff#8 +b.toBitVec = 0xff#8 +-/ +#guard_msgs in +example (a b : UInt8) : a + b > a := by + bv_decide + + + +/-! UInt16 -/ +example (a b c : UInt16) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a.toBitVec = 0xffff#16 +b.toBitVec = 0xffff#16 +-/ +#guard_msgs in +example (a b : UInt16) : a + b > a := by + bv_decide + + + +/-! UInt32 -/ +example (a b c : UInt32) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a.toBitVec = 0xffffffff#32 +b.toBitVec = 0xffffffff#32 +-/ +#guard_msgs in +example (a b : UInt32) : a + b > a := by + bv_decide + + + +/-! UInt64 -/ +example (a b c : UInt64) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a.toBitVec = 0xffffffffffffffff#64 +b.toBitVec = 0xffffffffffffffff#64 +-/ +#guard_msgs in +example (a b : UInt64) : a + b > a := by + bv_decide + + + +/-! USize -/ +example (a b c : USize) (h1 : a < b) (h2 : b < c) : a < c := by + cases System.Platform.numBits_eq <;> bv_decide + +/-- +warning: Detected USize in the goal but no hypothesis about System.Platform.numBits, consider case splitting on System.Platform.numBits_eq +--- +warning: declaration uses 'sorry' +-/ +#guard_msgs in +example (a b : USize) : a + b > a := by + bv_normalize + sorry + +example (h : 32 = System.Platform.numBits) (a b c : USize) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide