chore: fix acNf bug in bv_decide by switching over to grind

[bollu]

The bug seems to be because acNfUnnormalized creates a simp set that loops. I'll isolate an explanation of what's going on later.

For now, we choose instead to justify our rewrites using grind. We will improve this to use grind's internal CommRing solver, rather than all of the grind infrastructure.

We make this change as we wish to implement more of bitwuzla's associativity/commutatitivy normalization, which rely on canonicalizing non-linear combinations (such as $$x (y + x) + x y \mapsto 2xy + x^2$$ ), which requires a theory solver at least as powerful as ring to justify.

[bollu]

Investigated. The issue is that the use of simp in ac_nf to rewrite with congr theorems, and in trying to show that an equality holds by reflexivity, appears to spend time reducing a term with lage constants. Live lean lang link

import Std.Tactic.BVDecide

set_option trace.Meta.Tactic.simp true
set_option trace.Meta.Tactic.simp.all true
set_option trace.Meta.AC true
-- set_option diagnostics true

theorem simp_timeout (x y : BitVec 32) : (s * (~~~ (0#32) + s)) = (s * (~~~ (0#32) + s)) := by
  -- simp only [BitVec.not_zero, BitVec.reduceAllOnes]
  ac_nf

theorem grind_success (x y : BitVec 32) : (s * (~~~ (0#32) + s)) = (s * (~~~ (0#32) + s)) := by
  grind 

theorem grind_success_original_problem (x y : BitVec 32) :
    (s * (4294967295#32 + t) == s * (t + 4294967295#32)) = (s * (4294967295#32 + t) == s * (t + 4294967295#32)) := by
  grind -- grind justifies this rewrite without needing to unfold.

/-
(declare-fun s () (_ BitVec 32))
(declare-fun t () (_ BitVec 32))
-- SAT (exists s t, not P s t ) => USAT (forall s t, P s t)
(assert (not (= (bvmul s (bvadd (bvnot #b00000000000000000000000000000000) t)) (bvmul s (bvnot (bvneg t))))))
-/
theorem original_report (s t : BitVec 32) : (s * ((~~~(0#32) + t)) = (s * (~~~(-t)))) := by
  bv_normalize
  -- ac_nf
  bv_decide (config := { acNf := true })

[bollu]

Oh, that's a bit unfortunate, it seems that grind dies given symbolic bitvectors of large bitwidths example here:

import Std.Tactic.BVDecide
open Lean.Grind.CommRing


#synth Lean.Grind.CommRing (BitVec 256)

example (x y : BitVec 10) : x * y = y * x := by grind (config := {}) -- succeeds
/--
error: `grind` failed
case grind
x y : BitVec 256
h : ¬x * y = y * x
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
[grind] Issues
  [issue] maximum recursion depth has been reached
      use `set_option maxRecDepth <num>` to increase limit
      use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in example (x y : BitVec 256) : x * y = y * x := by grind (config := {}) -- fails

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5b18ea15457255a9db8a3c92fde7d55003f0cff9 --onto 3a3c816a27c0bd454711e2f9e4e20cbbde47ba85. You can force Mathlib CI using the force-mathlib-ci label. (2025-08-01 10:22:39)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5b18ea15457255a9db8a3c92fde7d55003f0cff9 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-08-01 10:22:41)

[bollu]

Private communication from @hargoniX was that integrating grind into BV is a nogo at the moment. We will revisit this in half a year :)