feat: bitblasting support for BitVec.carry

[alexkeizer]

This PR adds two normalization lemmas to the bv_normalize simpset, which will enable bv_decide to reason about BitVec.carry: these lemmas are BitVec.carry_eq_getLsbD_add_zeroExtend and BitVec.carry_width_eq_msb_add_zeroExtend. In principle, the former is strictly more general than the latter (which is applicable only in the case carry w x y _, where w is the width of x and y). However, I choose to include the latter still, because asking for the final carry bit is particularly common, and it has a simpler rhs, which presumably means a faster bitblasted circuit.

In the process of adding these lemmas, I also proved carry_gt, which (analogous to getLsbD_ge) says that asking for an out-of-range carry bit gives false. I didn't end up needing this lemma, but it seemed a useful addition to the API nonetheless, so I kept it around. The PR also adds a missing Commutative instance for Boolean xor (which is needed for the main result).

TODO (this PR is still WIP):

• write tests