Homomorphism rules for BitVec used by the grind tactic. The unsigned fragment is injected into Nat via BitVec.toNat, and the signed fragment into Int via BitVec.toInt.

Homomorphism predicates: range facts for the injection functions, instantiated by grind for the terms it internalizes. The 2 * toInt bounds are restated with an explicit parameter, as required by the [grind hom_pred] trigger inference.