7c62881a95
This PR adds short-circuit support to bv_decide to accelerate multiplications with shared coefficients. In particular, `a * x = b * x` can be extended to `a = b v (a * x = b * x)`. The latter is faster if `a = b` is true, as `a = b` may be evaluated without considering the multiplication circuit. On the other hand, we require the multiplication circuit, as `a * x = b * x -> a = b` is not always true due to two's complement wrapping. We support multiplications through acNF, which takes into account shared terms across equality canonicalizing `a * (b * c1) = a * (b * c2)` to `(a * b) * c1 = (a * b) * c2`. As a result, the non-shared terms are lifted to the top such that canonical rewrites for binary multiplication with shared terms on the left/right are sufficient. We add an option `bv_decide +shortCircuit` which controls this feature (currently disabled by default). --------- Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com> Co-authored-by: Henrik Böving <hargonix@gmail.com>
132 lines
4.3 KiB
Text
132 lines
4.3 KiB
Text
import Lean
|
|
/-!
|
|
# Tests for normalization up to associativity and commutativity
|
|
This file tests the `bv_ac_nf` normalization pass of `bv_decide`
|
|
-/
|
|
|
|
open Lean
|
|
|
|
/-! First, test the normalization up-to associativity and commutativity in isolation -/
|
|
namespace Unit
|
|
|
|
open Lean Elab Tactic in
|
|
/-- A tactic version of the `bv_ac_nf` normalization pass for `bv_decide`,
|
|
for testing purposes -/
|
|
elab "bv_ac_nf" : tactic =>
|
|
withMainContext do
|
|
liftMetaTactic1 fun goal => BVDecide.Frontend.Normalize.bvAcNfTarget goal
|
|
|
|
/- NOTE: the expression in this test is used as an example in the `bv_ac_nf` tactic
|
|
documentation. Any changes to the behaviour of this test should be reflected in
|
|
that docstring also. -/
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem mul_mul_beq_mul_mul (x₁ x₂ y₁ y₂ z : BitVec 4) :
|
|
(x₁ * (y₁ * z)) == (x₂ * (y₂ * z)) := by
|
|
bv_ac_nf
|
|
guard_target =ₛ (z * (x₁ * y₁) == z * (x₂ * y₂)) = true
|
|
sorry
|
|
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem ex_1 (x y z k₁ k₂ l₁ l₂ m₁ m₂ v : BitVec w) :
|
|
m₁ * x * (y * l₁ * k₁) * z == v * (k₂ * l₂ * x * y) * z * m₂ := by
|
|
bv_ac_nf
|
|
guard_target =ₛ (x * y * z * (m₁ * l₁ * k₁) == x * y * z * (v * k₂ * l₂ * m₂)) = true
|
|
sorry
|
|
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem ex_2 (x y : BitVec w) (h₁ : y = x) :
|
|
x * x * x * x == y * x * x * y := by
|
|
bv_ac_nf
|
|
guard_target =ₛ (x * x * (x * x) == x * x * (y * y)) = true
|
|
sorry
|
|
|
|
-- This theorem is short-circuited and scales to standard bitwidths.
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem mul_beq_mul_eq_right (x y z : BitVec 64) (h : x = y) :
|
|
x * z == y * z := by
|
|
bv_ac_nf
|
|
guard_target =ₛ (z * x == z * y) = true
|
|
sorry
|
|
|
|
-- This theorem is short-circuited and scales to standard bitwidths.
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem mul_beq_mul_eq_left (x y z : BitVec 64) (h : x = y) :
|
|
z * x == z * y := by
|
|
bv_ac_nf
|
|
guard_target =ₛ (z * x == z * y) = true
|
|
sorry
|
|
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem short_circuit_triple_mul (x x_1 x_2 : BitVec 32) (h : ¬x_2 &&& 4096#32 == 0#32) :
|
|
(x_1 ||| 4096#32) * x * (x_1 ||| 4096#32) = (x_1 ||| x_2 &&& 4096#32) * x * (x_1 ||| 4096#32) := by
|
|
bv_ac_nf
|
|
guard_target =ₛ (x_1 ||| 4096#32) * x * (x_1 ||| 4096#32) = (x_1 ||| 4096#32) * x * (x_1 ||| x_2 &&& 4096#32)
|
|
sorry
|
|
|
|
theorem add_mul_mixed (x y z : BitVec 64) :
|
|
z * (y + x) = (y + x) * z := by
|
|
bv_ac_nf
|
|
rfl
|
|
|
|
/-! ### Scaling Test -/
|
|
|
|
/-- `repeat_mul $n with $t` expands to `$t + $t + ... + $t`, with `n` repetitions
|
|
of `t` -/
|
|
local macro "repeat_mul" n:num "with" x:term : term =>
|
|
let rec go : Nat → MacroM Term
|
|
| 0 => `($x)
|
|
| n+1 => do
|
|
let r ← go n
|
|
`($r * $x)
|
|
go n.getNat
|
|
|
|
/-
|
|
This test showcases that the runtime of `bv_ac_nf` is not a bottleneck:
|
|
* Testing with 100 as the repetition amount runs in about 200ms with `skipKernelTC` set,
|
|
or ~3.3 seconds without (c.q. 2.3s for `ac_rfl`), and
|
|
* Putting in 125 for the repetition amount wil give a `maximum recursion depth has been reached`
|
|
error thrown by simp anyway, so the runtime is not a limiting factor to begin with.
|
|
-/
|
|
set_option debug.skipKernelTC true in
|
|
example (x y : BitVec 64) :
|
|
(repeat_mul 100 with x * y) = (repeat_mul 100 with x) * (repeat_mul 100 with y) := by
|
|
bv_ac_nf; rfl
|
|
|
|
end Unit
|
|
|
|
/-! Now, we test the pass as part of the full `bv_normalize` procedure -/
|
|
namespace Normalize
|
|
|
|
/-- Locally override `bv_normalize` with a config that enables the acNf pass -/
|
|
local macro "bv_normalize" : tactic =>
|
|
`(tactic| bv_normalize (config := {acNf := true, shortCircuit := true}))
|
|
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem mul_mul_eq_mul_mul (x₁ x₂ y₁ y₂ z : BitVec 4) (h₁ : x₁ = x₂) (h₂ : y₁ = y₂) :
|
|
x₁ * (y₁ * z) = x₂ * (y₂ * z) := by
|
|
bv_normalize
|
|
rename_i tgt
|
|
guard_hyp tgt :ₛ (!!(!x₁ * y₁ == x₂ * y₂ && !z * (x₁ * y₁) == z * (x₂ * y₂))) = true
|
|
sorry
|
|
|
|
/-- warning: declaration uses 'sorry' -/
|
|
#guard_msgs in
|
|
theorem mul_eq_mul_eq_right (x y z : BitVec 64) (h : x = y) :
|
|
x * z = y * z := by
|
|
bv_normalize
|
|
rename_i tgt
|
|
guard_hyp tgt :ₛ (!!(!x == y && !z * x == z * y)) = true
|
|
sorry
|
|
|
|
theorem add_mul_mixed (x y z : BitVec 64) :
|
|
z * (y + x) = (y + x) * z := by
|
|
bv_normalize
|
|
|
|
end Normalize
|