Fixed-width integer rules for numerical automation

Symbolic goals use the proved modular, checked, and saturating contracts. Concrete reduction unfolds the BitVec kernels only during the explicit closed-term phase.