Skip to content

feat: Confluent simp-set for left shift by BitVec.twoPow #6782

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
bollu wants to merge 1 commit into from
Closed

feat: Confluent simp-set for left shift by BitVec.twoPow #6782

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 22 additions & 1 deletion src/Init/Data/BitVec/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3401,6 +3401,22 @@ theorem twoPow_and (x : BitVec w) (i : Nat) :
(twoPow w i) &&& x = if x.getLsbD i then twoPow w i else 0#w := by
rw [BitVec.and_comm, and_twoPow]

/-!
NOTE(confluence of multiplication by twoPow):
The three rewrite rules:
- mul_twoPow_eq_shiftLeft: x * twoPow w i = x << i
- twoPow_mul_eq_shiftLeft: twoPow w i * x = x << i
- twoPow_shiftLeft_eq_twoPow_add: `twoPow w i << j = twoPow w (i + j)`

ensure confluence in the case of `twoPow w i * twoPow w j`, which can get rewritten into:
- `twoPow w i * twoPow w j → twoPow w i << j → twoPow w (i + j)
- `twoPow w i * twoPow w j → twoPow w j << i → twoPow w (j + i)
- `twoPow w i * twoPow w j → twoPow w (i + j)

which produce the same right hand side, upto a commutation of `i + j`,
which is acceptable for constant folding.
-/

@[simp]
theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
x * (twoPow w i) = x <<< i := by
Expand All @@ -3414,6 +3430,7 @@ theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
apply Nat.pow_dvd_pow 2 (by omega)
simp [Nat.mul_mod, hpow]

@[simp]
theorem twoPow_mul_eq_shiftLeft (x : BitVec w) (i : Nat) :
(twoPow w i) * x = x <<< i := by
rw [BitVec.mul_comm, mul_twoPow_eq_shiftLeft]
Expand All @@ -3429,11 +3446,15 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]

/-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
apply BitVec.eq_of_toNat_eq
simp only [toNat_mul, toNat_twoPow]
rw [← Nat.mul_mod, Nat.pow_add]

@[simp]
theorem twoPow_shiftLeft_eq_twoPow_add {w i j : Nat} : twoPow w i <<< j = twoPow w (i + j) := by
rw [shiftLeft_eq_mul_twoPow, twoPow_mul_twoPow_eq]

/--
The unsigned division of `x` by `2^k` equals shifting `x` right by `k`,
when `k` is less than the bitwidth `w`.
Expand Down
9 changes: 9 additions & 0 deletions tests/lean/run/bitvec_simproc.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,3 +141,12 @@ example (h : False) : 1#2 = 2#2 := by
simp; guard_target =ₛ False; exact h
example : 1#2 ≠ 2#2 := by
simp
/-! Check that multiplication by twoPow and <<< rewrites to the <<< normal form. -/
example : twoPow 32 3 * twoPow 32 4 = twoPow 32 7 := by
simp
example (x : BitVec 32) : x * twoPow 32 4 = x <<< 4 := by
simp
example (x : BitVec 32) : twoPow 32 4 * x = x <<< 4 := by
simp
example (x : BitVec 32) : ((twoPow 32 4 * x) <<< 3) * twoPow 32 3 = x <<< 10 := by
simp
Loading