feat: add IntX and ISize support for bv_decide (#7269)

This PR implements support for `IntX` and `ISize` in `bv_decide`.

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 =>

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
 
   /--

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:

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

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

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

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'
 -/