feat: refactor remainder to use unpacked floats

[abdoo8080]

Algorithm: upow2Mod vs SymFPU's divideStep

SymFPU computes the remainder via a divideStep loop: one bit of long division per iteration, running for up to O(2^e) steps. This is simple but exponential in the exponent width.

Our approach uses modular arithmetic: to compute rem(x, y) = x - y * n, we only need the quotient parity (n mod 2), guard, and sticky bits. These are recovered from (x.sig * 2^k) mod (2 * D) where D = y.sig and k = ex - ey. The key primitive is BitVec.upow2Mod, which computes 2^k mod m via repeated squaring in O(e) iterations of O(s)-bit operations.

	divideStep (SymFPU)	upow2Mod (ours)
Iterations	O(2^e)	O(e)
Per iteration	O(s)	O(s²) (modular squaring)
Total	O(2^e * s)	O(e * s²)
BV width	O(s)	O(s)
ITP proofs	Easier (long division is transparent)	Harder (modular arithmetic, CRT-style argument)
ATP/bitblasting	Larger formula (exponential unrolling)	Smaller formula (fewer steps, deeper per step)

For IEEE double precision (e=11, s=53): ~30K vs ~108K bit operations. The gap grows exponentially with e.

Structure

• BitVec.umulMod — modular multiplication (double-width)
• BitVec.umul2Mod — modular doubling (shift + conditional subtract)
• BitVec.upowMod — general modular exponentiation via repeated squaring
• BitVec.upow2Mod — specialized 2^exp mod m using umul2Mod for the multiply-by-2 step
• UnpackedFloat.mod — core remainder with rounding mode parameter (uses roundingDecision for integer quotient rounding, supports all SMT-LIB rounding modes)
• EUnpackedFloat.mod — special cases (NaN, ∞, zero)
• PackedFloat.mod — packed wrapper

🤖 Generated with Claude Code