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.

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
 

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

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

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

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

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