feat: more BitVec operations for Sym.(D)Simp.evalGround

[hargoniX]

This PR adds additional BitVec operations to the set of operations supported by Simp.Simp.evalGround and Sym.DSimp.evalGround.

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for afc6cd8 against 33ae929 are in. There are significant results. @hargoniX

• 🟥 build//instructions: +8.0G (+0.07%)

Large changes (4✅)

• ✅ elab/cbv_aes//instructions: -8.2G (-23.11%)
• ✅ elab/cbv_aes//task-clock: -1s (-33.15%)
• ✅ elab/cbv_aes//wall-clock: -1s (-35.26%)
• ✅ elab/cbv_arm_ldst//instructions: -4.3G (-6.92%)

Medium changes (3✅)

• ✅ elab/cbv_aes//maxrss: -115MiB (-13.31%)
• ✅ elab/cbv_dedup//instructions: -127.1M (-4.03%)
• ✅ elab/cbv_merge_sort//instructions: -304.3M (-1.89%)

Small changes (2✅, 4🟥)

• 🟥 build/module/Init.Sym.Lemmas//instructions: +25.8M (+1.20%)
• 🟥 build/module/Lean.Meta.Sym.DSimp.EvalGround//instructions: +3.4G (+22.98%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Sym.LitValues//instructions: +80.5M (+5.53%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Sym.Simp.EvalGround//instructions: +4.0G (+19.08%) (reduced significance based on *//lines)
• ✅ elab/bv_decide_mod//maxrss: -139MiB (-6.90%)
• ✅ elab/cbv_arm_ldst//wall-clock: -396ms (-10.21%)

[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 33ae929879bfcec8c4bceadf3dbc91172b36365f --onto 25ba8c3d3bcb1dded7ff5a6f3b6044b0a7970198. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-20 10:10: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 33ae929879bfcec8c4bceadf3dbc91172b36365f --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-20 10:10:27)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 0e30821 against 33ae929 are in. There are significant results. @hargoniX

• 🟥 build//instructions: +10.2G (+0.09%)

Large changes (4✅)

• ✅ elab/cbv_aes//instructions: -8.2G (-23.18%)
• ✅ elab/cbv_aes//task-clock: -1s (-32.95%)
• ✅ elab/cbv_aes//wall-clock: -1s (-35.22%)
• ✅ elab/cbv_arm_ldst//instructions: -4.6G (-7.47%)

Medium changes (3✅)

• ✅ elab/cbv_aes//maxrss: -105MiB (-12.21%)
• ✅ elab/cbv_dedup//instructions: -127.8M (-4.05%)
• ✅ elab/cbv_merge_sort//instructions: -294.3M (-1.83%)

Small changes (1✅, 5🟥)

• 🟥 build/module/Init.Sym.Lemmas//instructions: +28.1M (+1.31%)
• 🟥 build/module/Lean.Meta.Sym.DSimp.EvalGround//instructions: +5.0G (+33.71%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Sym.LitValues//instructions: +79.4M (+5.45%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Sym.Simp.EvalGround//instructions: +4.5G (+21.47%) (reduced significance based on *//lines)
• ✅ elab/cbv_arm_ldst//wall-clock: -452ms (-11.64%)
• 🟥 size/all/.c//lines: +25.4k (+0.21%)