Homomorphism rules for Nat used by the grind tactic. These are target-domain rules: shifts are normalized to arithmetic, testBit decomposes bitwise operations, and the %-cleanup rules remove the redundant modular wrappers produced by the BitVec.toNat injection.