perf: use SymM for bv_decide rewriting

[hargoniX]

• refactoring step 1
• step
• first chunks of eval ground
• step
• attempt 1
• chore: update stage0
• no need to share it all

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for a4468ac against ee66ef2 are in. There are significant results. @hargoniX

• 🟥 build//instructions: +9.7G (+0.09%)
• 🟥 other exited with code 1

Large changes (1🟥)

• 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Simproc//instructions: +16.2G (+58.68%)

Medium changes (1🟥)

• 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Normalize.AndFlatten//instructions: +1.2G (+57.89%) (reduced significance based on absolute threshold)

Small changes (42✅, 12🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ee66ef27e0f8d4176071ed62266397eb34d9e119 --onto 727b4aad2bbb2562e0e2b42e29334738409d167c. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-24 18:55:25)

[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 ee66ef27e0f8d4176071ed62266397eb34d9e119 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-24 18:55:26)