feat(symbolic): prove bounded mul-div monotonicity

[figtracer]

Summary

Teach native symbolic testing to prove bounded unsigned multiplication/division monotonicity without bit-blasting the nonlinear terms.

The Spark PSM3 verification harness from A Spark Is Born already runs unchanged under forge test --symbolic, but current master returns:

[FAIL: incomplete symbolic execution (Timeout): hard arithmetic heuristic witness used; no replayed counterexample found]

for prove_getSUsdsValue_roundDown_rate_monotonic, whose core shape is:

amount * rate1 / 1e9 / 1e18 <= amount * rate2 / 1e9 / 1e18

with amount <= uint128.max, rate1 <= rate2, and rate2 <= uint128.max.

With this branch, the unchanged proof reports:

[PASS] prove_getSUsdsValue_roundDown_rate_monotonic(...) (... hard-arith: 0 ...)

This is a focused first slice, not the full hevm arithmetic-abstraction catalogue. Spark's ceilDiv round-up properties and exact cancellation/telescoping identities remain incomplete.

This is also separate from #15591: that PR improves stateful invariant exploration and replay storage; its current head still returns the same incomplete result for this stateless nonlinear proof.

• propagate unsigned path bounds through order constraints, including a <= b <= uint128.max
• recognize weak product order when both products are proven not to overflow
• preserve that order through one or more UDIV operations with matching divisors
• prune contradictory failure paths and remove soundly implied success constraints before heuristic hard-arithmetic search
• keep wrapping/unbounded products on the existing exact/fallback path

[mattsse]

lgtm