a bit further

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean

@@ -31,9 +31,7 @@ def getConfig : PreProcessM BVDecideConfig := read
 
 @[inline]
 def checkRewritten (fvar : FVarId) : PreProcessM Bool := do
-  let val := (← get).rewriteCache.contains fvar
-  trace[Meta.Tactic.bv] m!"{mkFVar fvar} was already rewritten? {val}"
-  return val
+  return (← get).rewriteCache.contains fvar
 
 @[inline]
 def rewriteFinished (fvar : FVarId) : PreProcessM Unit := do

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Tactic.Simp
 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
@@ -21,6 +22,9 @@ open Lean.Meta
 def intToBitVecPass : Pass where
   name := `intToBitVec
   run' goal := do
+    -- TODO: change this to "if we detect usize look for hypothesis"
+    if ← detectUSize goal then
+      logWarning "bv_decide is currently unable to reason about USize"
     let intToBvThms ← intToBitVecExt.getTheorems
     let cfg ← PreProcessM.getConfig
     let simpCtx ← Simp.mkContext
@@ -32,6 +36,21 @@ def intToBitVecPass : Pass where
     let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := hyps)
     let some (_, newGoal) := result? | return none
     return newGoal
+where
+  detectUSize (goal : MVarId) : MetaM Bool := do
+    let checker e :=
+      match e with
+      | .const n _ => n == ``USize || n == ``System.Platform.numBits
+      | _ => false
+
+    let indicatesUSize (e : Expr) := Option.isSome <| e.find? checker
+
+    goal.withContext do
+      let lctx ← getLCtx
+      if lctx.any (fun decl => indicatesUSize decl.type) then
+        return true
+      else
+        return indicatesUSize (← goal.getType)
 
 end Frontend.Normalize
 end Lean.Elab.Tactic.BVDecide

tests/lean/run/bv_uint.lean

@@ -57,3 +57,27 @@ b.toBitVec = 0xffffffffffffffff#64
 #guard_msgs in
 example (a b : UInt64) : a + b = a := by
   bv_decide
+
+
+
+
+
+/-! USize -/
+example (a b : USize) : a + b = b + a := by
+  rcases System.Platform.numBits_eq with h | h
+  · simp only [int_toBitVec]
+    subst h
+    simp only [h, int_toBitVec]
+    bv_decide
+    sorry
+  · sorry
+  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 : USize) : a + b = a := by
+  bv_decide