From 2b752ec245bea616f04b06c4e8761bbf813b84ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 28 Feb 2025 11:33:11 +0100 Subject: [PATCH] feat: add IntX and ISize support for bv_decide (#7269) This PR implements support for `IntX` and `ISize` in `bv_decide`. --- .../Tactic/BVDecide/Frontend/BVDecide.lean | 20 +++++ .../Frontend/Normalize/IntToBitVec.lean | 41 +++++----- .../Frontend/Normalize/Structures.lean | 2 +- .../Frontend/Normalize/TypeAnalysis.lean | 6 ++ tests/lean/run/bv_sint.lean | 78 +++++++++++++++++++ tests/lean/run/bv_structures.lean | 24 ++++++ tests/lean/run/bv_uint.lean | 2 +- 7 files changed, 152 insertions(+), 21 deletions(-) create mode 100644 tests/lean/run/bv_sint.lean diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index a5ad663832..adda1025dc 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -190,6 +190,26 @@ where return (x, toExpr <| UInt64.ofBitVec (h ▸ value.bv)) else throwError m!"Value for UInt64 was not 64 bit but {value.w} bit" + | Int8.toBitVec x => + if h : value.w = 8 then + return (x, toExpr <| Int8.ofBitVec (h ▸ value.bv)) + else + throwError m!"Value for Int8 was not 8 bit but {value.w} bit" + | Int16.toBitVec x => + if h : value.w = 16 then + return (x, toExpr <| Int16.ofBitVec (h ▸ value.bv)) + else + throwError m!"Value for Int16 was not 16 bit but {value.w} bit" + | Int32.toBitVec x => + if h : value.w = 32 then + return (x, toExpr <| Int32.ofBitVec (h ▸ value.bv)) + else + throwError m!"Value for Int32 was not 32 bit but {value.w} bit" + | Int64.toBitVec x => + if h : value.w = 64 then + return (x, toExpr <| Int64.ofBitVec (h ▸ value.bv)) + else + throwError m!"Value for Int64 was not 64 bit but {value.w} bit" | _ => match var with | .app (.const (.str p s) []) arg => diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean index dfc0f94b18..b482f87dd6 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ prelude +import Init.Data.SInt.Basic import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic import Lean.Elab.Tactic.BVDecide.Frontend.Attr import Lean.Elab.Tactic.Simp @@ -14,7 +15,7 @@ This module contains the implementation of the pre processing pass for reducing It: 1. runs the `int_toBitVec` simp set -2. If `USize.toBitVec` is used anywhere looks for equations of the form +2. If `USize.toBitVec`/`ISize.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. -/ @@ -25,11 +26,12 @@ namespace Frontend.Normalize open Lean.Meta /-- -Contains information for the `USize` elimination pass. +Contains information for the `USize`/`ISize` elimination pass. -/ -structure USizeState where +structure SizeState where /-- - Contains terms of the form `USize.toBitVec e` that we will translate to constant width `BitVec`. + Contains terms of the form `USize.toBitVec e` and `ISize.toBitVec e` that we will translate to + constant width `BitVec`. -/ relevantTerms : Std.HashSet Expr := {} /-- @@ -37,16 +39,16 @@ structure USizeState where -/ relevantHyps : Std.HashSet FVarId := {} -private abbrev M := StateRefT USizeState MetaM +private abbrev M := StateRefT SizeState MetaM namespace M @[inline] -def addUSizeTerm (e : Expr) : M Unit := do +def addSizeTerm (e : Expr) : M Unit := do modify fun s => { s with relevantTerms := s.relevantTerms.insert e } @[inline] -def addUSizeHyp (f : FVarId) : M Unit := do +def addSizeHyp (f : FVarId) : M Unit := do modify fun s => { s with relevantHyps := s.relevantHyps.insert f } end M @@ -64,30 +66,30 @@ def intToBitVecPass : Pass where let hyps ← goal.getNondepPropHyps let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps) let some (_, goal) := result? | return none - handleUSize goal |>.run' {} + handleSize goal |>.run' {} where - handleUSize (goal : MVarId) : M MVarId := do - if ← detectUSize goal then - replaceUSize goal + handleSize (goal : MVarId) : M MVarId := do + if ← detectSize goal then + replaceSize goal else return goal - detectUSize (goal : MVarId) : M Bool := do + detectSize (goal : MVarId) : M Bool := do goal.withContext do for hyp in ← getPropHyps do (← hyp.getType).forEachWhere (stopWhenVisited := true) - (·.isAppOfArity ``USize.toBitVec 1) + (fun e => e.isAppOfArity ``USize.toBitVec 1 || e.isAppOfArity ``ISize.toBitVec 1) fun e => do - M.addUSizeTerm e - M.addUSizeHyp hyp + M.addSizeTerm e + M.addSizeHyp hyp return !(← get).relevantTerms.isEmpty /-- - Turn `goal` into a goal containing `BitVec const` instead of `USize`. + Turn `goal` into a goal containing `BitVec const` instead of `USize`/`ISize`. -/ - replaceUSize (goal : MVarId) : M MVarId := do + replaceSize (goal : MVarId) : M MVarId := do if let some (numBits, numBitsEq) ← findNumBitsEq goal then goal.withContext do let relevantHyps := (← get).relevantHyps.toArray.map mkFVar @@ -138,13 +140,14 @@ where numBitsEq (mkMVar newGoal) goal.assign <| mkAppN casesOn (relevantTerms ++ abstractedHyps) - -- remove all of the hold hypotheses about USize.toBitVec to prevent false counter examples + -- remove all of the hold hypotheses about USize.toBitVec/ISize.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}" + logWarning m!"Detected USize/ISize in the goal but no hypothesis about System.Platform.numBits, consider case splitting on {mkConst ``System.Platform.numBits_eq}" return goal /-- diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean index da5dc7e496..770ef4e32e 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean @@ -15,7 +15,7 @@ structures containing information about supported types into individual parts re The implementation runs cases recursively on all "interesting" types where a type is interesting if it is a non recursive structure and at least one of the following conditions hold: -- it contains something of type `BitVec`/`UIntX`/`Bool` +- it contains something of type `BitVec`/`UIntX`/`IntX`/`Bool` - it is parametrized by an interesting type - it contains another interesting type Afterwards we also: diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean index 53f1afcfbb..ab25db8904 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ prelude +import Init.Data.SInt.Basic import Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic /-! @@ -64,6 +65,11 @@ where | UInt32 => return true | UInt64 => return true | USize => return true + | Int8 => return true + | Int16 => return true + | Int32 => return true + | Int64 => return true + | ISize => return true | Bool => return true | _ => let some const := expr.getAppFn.constName? | return false diff --git a/tests/lean/run/bv_sint.lean b/tests/lean/run/bv_sint.lean new file mode 100644 index 0000000000..9968c29ec6 --- /dev/null +++ b/tests/lean/run/bv_sint.lean @@ -0,0 +1,78 @@ +import Std.Tactic.BVDecide + +/-! Int8 -/ +example (a b c : Int8) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a = -1 +b = -1 +-/ +#guard_msgs in +example (a b : Int8) : a + b > a := by + bv_decide + + + +/-! Int16 -/ +example (a b c : Int16) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a = -1 +b = -1 +-/ +#guard_msgs in +example (a b : Int16) : a + b > a := by + bv_decide + + + +/-! Int32 -/ +example (a b c : Int32) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a = -1 +b = -1 +-/ +#guard_msgs in +example (a b : Int32) : a + b > a := by + bv_decide + + + +/-! Int64 -/ +example (a b c : Int64) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide + +/-- +error: The prover found a counterexample, consider the following assignment: +a = -1 +b = -1 +-/ +#guard_msgs in +example (a b : Int64) : a + b > a := by + bv_decide + + + +/-! ISize -/ +example (a b c : ISize) (h1 : a < b) (h2 : b < c) : a < c := by + cases System.Platform.numBits_eq <;> bv_decide + +/-- +warning: Detected USize/ISize 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 : ISize) : a + b > a := by + bv_normalize + sorry + +example (h : 32 = System.Platform.numBits) (a b c : ISize) (h1 : a < b) (h2 : b < c) : a < c := by + bv_decide diff --git a/tests/lean/run/bv_structures.lean b/tests/lean/run/bv_structures.lean index 50dff26aa0..9e0a4408c4 100644 --- a/tests/lean/run/bv_structures.lean +++ b/tests/lean/run/bv_structures.lean @@ -143,3 +143,27 @@ example (a b c : Pair) (h1 : a ≠ b) (h2 : b = c) : a ≠ c := by bv_decide end Ex10 + +namespace Ex11 + +structure Pair where + x : UInt16 + y : UInt16 + h : x + y = 0 + +example (a : Pair) (b : UInt16) : a.x + a.y + b ≤ b := by + bv_decide + +end Ex11 + +namespace Ex12 + +structure Pair where + x : Int16 + y : Int16 + h : x + y = 0 + +example (a : Pair) (b : Int16) : a.x + a.y + b ≤ b := by + bv_decide + +end Ex12 diff --git a/tests/lean/run/bv_uint.lean b/tests/lean/run/bv_uint.lean index c1f6765956..445c60efc0 100644 --- a/tests/lean/run/bv_uint.lean +++ b/tests/lean/run/bv_uint.lean @@ -65,7 +65,7 @@ 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: Detected USize/ISize in the goal but no hypothesis about System.Platform.numBits, consider case splitting on System.Platform.numBits_eq --- warning: declaration uses 'sorry' -/