From 000e0cab7c4b3c32b0656f9802f493488b1c0c4a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 20 Jan 2025 20:50:31 +0100
Subject: [PATCH] a bit further

---
 .../BVDecide/Frontend/Normalize/Basic.lean    |  4 +---
 .../Frontend/Normalize/IntToBitVec.lean       | 19 +++++++++++++++
 tests/lean/run/bv_uint.lean                   | 24 +++++++++++++++++++
 3 files changed, 44 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean
index 377d770d2364..7fa261cea938 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean
index 65ffb839c0c4..65333eb7b1d6 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean
+++ b/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
diff --git a/tests/lean/run/bv_uint.lean b/tests/lean/run/bv_uint.lean
index 86b389536c1e..4a0f13bb8a6c 100644
--- a/tests/lean/run/bv_uint.lean
+++ b/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