From 41fe7bc71ac5335ff9abbb82cbfd262a1b3854e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 29 Jan 2025 16:17:39 +0100 Subject: [PATCH] feat: bv_normalize rewrite shifts by BitVec const to shift by Nat const (#6851) This PR makes `bv_normalize` rewrite shifts by `BitVec` constants to shifts by `Nat` constants. This is part of the greater effort in providing good support for constant shift simplification in `bv_normalize`. --- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 5 +++++ tests/lean/run/bv_decide_rewriter.lean | 3 +++ 2 files changed, 8 insertions(+) diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 864843c6b1..3b85d79ac9 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -257,6 +257,11 @@ theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a : attribute [bv_normalize] BitVec.mul_zero attribute [bv_normalize] BitVec.zero_mul + +attribute [bv_normalize] BitVec.shiftLeft_ofNat_eq +attribute [bv_normalize] BitVec.ushiftRight_ofNat_eq +attribute [bv_normalize] BitVec.sshiftRight'_ofNat_eq_sshiftRight + attribute [bv_normalize] BitVec.shiftLeft_zero attribute [bv_normalize] BitVec.zero_shiftLeft diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index 5a28d192b0..6b9977a607 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -52,6 +52,9 @@ example : BitVec.sshiftRight 0#16 n = 0#16 := by bv_normalize example {x : BitVec 16} : BitVec.sshiftRight x 0 = x := by bv_normalize example {x : BitVec 16} : 0#16 * x = 0 := by bv_normalize example {x : BitVec 16} : x * 0#16 = 0 := by bv_normalize +example {x : BitVec 16} : x >>> (12 : Nat) = x >>> 12#16 := by bv_normalize +example {x : BitVec 16} : x <<< (12 : Nat) = x <<< 12#16 := by bv_normalize +example {x : BitVec 16} : x.sshiftRight (12 : Nat) = x.sshiftRight' 12#16 := by bv_normalize example {x : BitVec 16} : x <<< 0#16 = x := by bv_normalize example {x : BitVec 16} : x <<< 0 = x := by bv_normalize example : 0#16 <<< (n : Nat) = 0 := by bv_normalize