feat: define rotateLeft/Right with modulo

[bollu]

This ensures that rotateLeft/Right behave correctly even when the rotation amount is larger than the bitwidth.

This shall be followed up with getLsb theorems for rotations for LeanSAT.

We choose to write aux definitions since it is cleaner to reason about the aux theorems with the assumption that rotation-amount < bit-width, followed by auxiliary lemmas that link the behavior of rotation to the canonical case when rotation-amount < bit-width.

Proof strategy we will execute based on these definitions: Link to proof of getLsb_rotateLeft

[bollu]

awaiting-review

[leanprover-community-mathlib4-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 b278f9dd3096a6f183812b6f9129fc79f8675f00 --onto f53b778c0d4a474383eab709d67db5e12357f39d. (2024-05-20 15:13:59)