max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: bv_normalize rewrite shifts by BitVec const to shift by Nat const (#6851)

Browse source 
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`.
This commit is contained in:
Henrik Böving 2025-01-29 16:17:39 +01:00 • committed by GitHub
parent 2c00f8fe2f
commit 41fe7bc71a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Std/Tactic/BVDecide/Normalize/BitVec.lean
View file

@ -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

3
tests/lean/run/bv_decide_rewriter.lean
View file

@ -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