From 712bb070f9301e575fd976e2753192c223eb023f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 15 Apr 2025 19:26:19 +0200
Subject: [PATCH] feat: make bv_decide work on simp normal forms of shifts
 (#7976)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR ensure that `bv_decide` can handle the simp normal form of a
shift.

Consider:
```lean
theorem test1 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0)
  : b <<< s = 0 := by
  bv_decide
```
This works out, however:
```lean
theorem test2 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0)
  : b <<< s = 0 := by
  simp
  bv_decide
```
this fails because the `simp` normal form adds `toNat` to the right hand
argument of the `<<<` and `bv_decide` cannot deal with shifts by
non-constant `Nat`.

Discovered by @spdskatr
---
 .../BVDecide/Normalize/Canonicalize.lean      |  4 ++++
 src/Std/Tactic/BVDecide/Syntax.lean           |  6 ++++++
 tests/lean/run/bv_decide_shift_to_nat.lean    | 21 +++++++++++++++++++
 3 files changed, 31 insertions(+)
 create mode 100644 tests/lean/run/bv_decide_shift_to_nat.lean

diff --git a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
index 17c74fddb2..7227775416 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Init.Data.BitVec
+import Std.Tactic.BVDecide.Syntax
 
 /-!
 This contains theorems responsible for turning both `Bool` and `BitVec` goals into the
@@ -97,6 +98,9 @@ attribute [bv_normalize] BitVec.neg_eq
 attribute [bv_normalize] BitVec.mul_eq
 attribute [bv_normalize] BitVec.udiv_eq
 attribute [bv_normalize] BitVec.umod_eq
+attribute [bv_normalize ←] BitVec.shiftLeft_eq'
+attribute [bv_normalize ←] BitVec.sshiftRight_eq'
+attribute [bv_normalize ←] BitVec.ushiftRight_eq'
 
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean
index ac848b25bd..fc90416f20 100644
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/src/Std/Tactic/BVDecide/Syntax.lean
@@ -95,6 +95,12 @@ syntax (name := bvNormalize) "bv_normalize" optConfig : tactic
 
 end Tactic
 
+/--
+Theorems tagged with the `bv_normalize` attribute are used during the rewriting step of the
+`bv_decide` tactic. 
+-/
+syntax (name := bv_normalize) "bv_normalize" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+
 /--
 Auxiliary attribute for builtin `bv_normalize` simprocs.
 -/
diff --git a/tests/lean/run/bv_decide_shift_to_nat.lean b/tests/lean/run/bv_decide_shift_to_nat.lean
new file mode 100644
index 0000000000..442f240440
--- /dev/null
+++ b/tests/lean/run/bv_decide_shift_to_nat.lean
@@ -0,0 +1,21 @@
+import Std.Tactic.BVDecide
+
+theorem test2 (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    b <<< s.toNat = 0 := by
+  bv_decide
+
+theorem test2' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    b >>> s.toNat = 0 := by
+  bv_decide
+
+theorem test2'' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    BitVec.sshiftRight b s.toNat = 0 := by
+  bv_decide
+
+theorem test2''' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    BitVec.shiftLeft b s.toNat = 0 := by
+  bv_decide
+
+theorem test2'''' (b s : BitVec 5) (hb : b = 0) (hs : s ≠ 0) :
+    BitVec.ushiftRight b s.toNat = 0 := by
+  bv_decide