feat: teach bv_normalize overshifting equals 0

[vlad902]

This PR adds lemmas that x >>> n = 0 and x <<< n = 0 when n exceeds x's bithwidth to the bv_normalize simpset.

[vlad902]

changelog-library

[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 5c0231f508cca395fe790cd85b426954ace4075b --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 14:10:34)

[hargoniX]

We want to implement this one a little differently, consider the two PRs:

• feat: BitVec.shiftLeft in terms of extractLsb' #6743
• feat: BitVec.ushiftRight in terms of extractLsb' #6745

these add theory for both overshifting and general constant shifting. The idea for bv_decide would be the following: write a simproc that acts on shifts by constants. It extracts the constants and applies the lemmas as appropriate to return either 0#w directly or an 0#w concatenated with an extract.

[vlad902]

Yea I suppose this is something I didn't quite understand, right now it seems like bv_normalize is able to apply these to e.g. x <<< 100 when x is a BitVec 16, but when the hypothesis 16 ≤ 100 was generated and whether one could rely on Lean to do this in all contexts/for all constants is not clear to me.