refactor: USize/ISize handling in bv_decide

[hargoniX]

This PR refactors the way that bv_decide handles USize and ISize. This is necessary for SymM support in bv_decide because calling revert in SymM is illegal.

Instead of building a custom motive to replace USize/ISize constants with BitVec ones, it now uses a modified int_toBitVec simp set. For all fixed width IntX this still contains the original lemmas. For USize/ISize it contains lemmas that convert to BitVec 32 or BitVec 64, conditionally on which of the two assumptions is available. Through this USize/ISize already get converted to fixed-width BitVec in the int_toBitVec simp pass in bv_decide.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-06-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-30 14:32:21)

[leanprover-bot]

Reference manual CI status:

• 🟡 Reference manual branch lean-pr-testing-14227 build against this PR didn't complete normally. (2026-06-30 15:35:40) View Log
• ✅ Reference manual branch lean-pr-testing-14227 has successfully built against this PR. (2026-06-30 15:35:54) View Log

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for e9edb7b against 28b99ec are in. No significant results found. @hargoniX

• 🟥 build//instructions: +6.9G (+0.06%)

Small changes (2✅, 13🟥)

• 🟥 build/module/Init.Data.SInt.Bitwise//instructions: +408.2M (+3.70%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.SInt//instructions: +16.9M (+4.43%) (reduced significance based on *//lines)
• 🟥 build/module/Init.Data.UInt.Bitwise//instructions: +411.4M (+1.98%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.BVDecide.Counterexample//instructions: +395.3M (+10.49%) (reduced significance based on *//lines)
• ✅ build/module/Lean.Meta.Tactic.BVDecide.Normalize.IntToBitVec//instructions: -1.5G (-46.97%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Async//instructions: +10.5M (+1.65%)
• 🟥 build/module/Std.Http.Data.Body//instructions: +11.5M (+1.68%)
• 🟥 build/module/Std.Internal.UV.DNS//instructions: +14.3M (+3.42%)
• 🟥 build/module/Std.Internal.UV.TCP//instructions: +17.3M (+3.29%)
• 🟥 build/module/Std.Internal.UV//instructions: +15.3M (+3.86%)
• 🟥 build/module/Std//instructions: +10.3M (+1.34%)
• 🟥 elab/charactersIn//instructions: +35.6M (+0.10%)
• 🟥 size/Init/.olean.server//bytes: +33kiB (+0.29%)
• 🟥 size/Init/.olean//bytes: +246kiB (+0.26%)
• ✅ vcgen/AddSubCancelDeep/500/vcgen//wall-clock: -3ms (-3.49%)