bv_decide - kernel deterministic timeout + ofBool normalization

tobiasgrosser commented 1 week ago

Prerequisites

Please put an X between the brackets as you perform the following steps:

[x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

The following test case fails with 'kernel deterministic timeout) import Lean.Elab.Tactic.BVDecide

/-
(kernel) deterministic timeout
-/
theorem extracted_1 (x : BitVec 32) :
  BitVec.ofBool (x != 51#32) &&& BitVec.ofBool (x != 50#32) =
    BitVec.ofBool (4294967294#32 > x + 4294967244#32) := by
  -- simp [BitVec.ofBool_and_ofBool, BitVec.ofBool_eq_iff_eq]
  bv_decide

Steps to Reproduce

Copy test case into lean
Observe error

Expected behavior: bv_decide should solve this goal quickly. In case it fails, it should not be a kernel timeout

Actual behavior: A kernel timeout

Versions

Lean 4.15.0-nightly-2024-11-11 Target: arm64-apple-darwin23.6.0 macOS

Additional Information

This bug goes away if I simplify with the relevant ofBool_* theorems. Adding them to bv_normalize does not help, though.

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

hargoniX commented 1 week ago

The error is correct but the diagnosis around BitVec.ofBool is wrong. bv_decide reduces ofBool to ite and the bug also exists if the ofBool/ite gets hidden behind variables + equality statements. So this is not just something we can fix by adding more simp lemmas surrounding ofBool or ite. It's a more fundamental issue.

tobiasgrosser commented 1 week ago

The error is correct but the diagnosis around BitVec.ofBool is wrong. bv_decide reduces ofBool to ite and the bug also exists if the ofBool/ite gets hidden behind variables + equality statements. So this is not just something we can fix by adding more simp lemmas surrounding ofBool or ite. It's a more fundamental issue.

AFAIU there are two issues in this test case. One is the fundamental issue with 'deterministic timeout'. The second is that bv_normalize should normalize this better.

In particular, we currently get:

theorem extracted_1 (x : BitVec 32) :
  BitVec.ofBool (x != 51#32) &&& BitVec.ofBool (x != 50#32) =
    BitVec.ofBool (4294967294#32 > x + 4294967244#32) := by

  /-
  case h
  x : BitVec 32
  a✝ : (!((if (!x == 51#32) = true then 1#1 else 0#1) &&& if (!x == 50#32) = true then 1#1 else 0#1) ==
        if (x + 4294967244#32).ult 4294967294#32 = true then 1#1 else 0#1) =
    true
  ⊢ False
  -/
  bv_normalize

but should get

theorem extracted_1 (x : BitVec 32) :
  BitVec.ofBool (x != 51#32) &&& BitVec.ofBool (x != 50#32) =
    BitVec.ofBool (4294967294#32 > x + 4294967244#32) := by
  simp [BitVec.ofBool_and_ofBool, BitVec.ofBool_eq_iff_eq]
  /-
  case h
  x : BitVec 32
  a✝ : (!(!x == 51#32 && !x == 50#32) == (x + 4294967244#32).ult 4294967294#32) = true
  ⊢ False
  -/
  bv_normalize
  bv_decide

This improved bv_normalize would hide the 'deterministic timeout' bug but is generally desirable.

Or is there a reason we would want to bit-blast an if-statement if there is a way to eliminate it?

hargoniX commented 1 week ago

There is almost no difference between the bitblasted versions of these two, they get solved in basically the same time. The way to rewrite this would be with rewrite rules on the ite form so we actually handle not only BitVec.ofBool but all ite problems of this form. But even then you can trivially retrigger the itmeout by hiding the BitVec.ofBool behind variables so the actual issue at hand here is not solved by rewrites.

leanprover / lean4