Upstream lemmas for bitwise arithmetic

[lucasmt]

This PR adds a file bitwise-lemmas.md with lemmas for rewriting bitwise arithmetic expressions (&Int, >>Int and <<Int) into arithmetic operations that the SMT solver can more easily reason about (modInt, /Int, *Int), as well as lemmas for bounding the results of bitwise expressions. Because of how the introduced lemmas interact with previous lemmas defined in kmir-lemmas.md, in particular the lemmas for simplifying round-trip conversions (which are defined in terms of bitwise expressions), we also include lemmas for simplifying such expressions even after being rewritten in terms of non-bitwise operators.

The PR also includes new integration tests that exercise the new lemmas, and regenerates .expected files that are affected (all of them by simplifying out redundant bitmasks).