Symbolic float model (RealBasedSymbolicFloat) diverges from IEEE-754 → false counterexamples in %, divmod, round, pow

[pschanely]

Summary

CrossHair's real-number-backed float model (RealBasedSymbolicFloat) reasons about float as an exact rational. For a handful of operations this diverges from CPython's IEEE-754 semantics, so CrossHair reports false counterexamples — it "finds" a violation of a property that actually holds for every concrete input.

This surfaced from the stdlib support-map measurement (the differential soundness probe in crosshair/tools/measure_support.py): these ops render as black ("gives a wrong answer") cells, and on inspection the divergence is real.

Minimal reproduction

def f(x: float) -> float:
    # This post is a tautology: it asserts exactly what Python computes for this
    # input, so it can never fail. CrossHair reports it as false anyway.
    """
    pre: x == -2.6229075025237076e+16
    post: __return__ == 8.12552781506134e-43
    """
    return x % 2.5890419884777833e-42

$ crosshair check --per_condition_timeout=10 repro.py
repro.py:6: error: false when calling f(-2.6229075025237076e+16) (which returns 2.1327293150557237e-42)

Concretely (-2.6229075025237076e+16) % 2.5890419884777833e-42 == 8.12552781506134e-43 in CPython (verified), so the post holds for the only permitted input and the counterexample is spurious. CrossHair's symbolic evaluation yields 2.1327293150557237e-42 instead.

Where it comes from

RealBasedSymbolicFloat (crosshair/libimpl/builtinslib.py) models a float as a z3 Real and solves modulo/floordiv with an exact real/integer constraint:

# crosshair/libimpl/builtinslib.py, _float_divmod
# TODO : precise float divmod
...
remainder = z3.Real(...)
modproduct = z3.Int(...)
space.add(smt_b * modproduct + remainder == smt_a)   # exact euclidean division

That is exact real arithmetic; realization then rounds the exact rational model to the nearest double (find_model_value(self.var).__float__()). CPython instead computes a % b directly on IEEE-754 doubles. For large |a/b| (here the exact quotient is a ~58-digit integer) the exact-real result and the IEEE result differ. The # TODO : precise float divmod comment at that site already flags this path as approximate; the same real-vs-IEEE gap affects the other float ops below.

Scope (from the current support-map run)

False black cells traceable to this:

• float.__mod__, float.__divmod__, float.__round__, float.__pow__
• downstream float-heavy stdlib: colorsys.hls_to_rgb, colorsys.hsv_to_rgb, colorsys.rgb_to_yiq

(The other black cells in the same run — bytearray.*, str.maketrans, bool.* — look unrelated and are being triaged separately.)

Possible remedies

1. Concrete-execution check on counterexamples (general safety net). The hypothesis‑CrossHair plugin already re-runs a candidate counterexample concretely and discards it when the property actually holds; CrossHair proper has no equivalent. A concrete-verification pass before reporting would suppress this whole class of false positives (float and beyond) cheaply — at the cost of possibly dropping a genuine-but-flaky counterexample, so it would want to be careful about how it treats a counterexample that can't be concretely reproduced.
2. Make the float model IEEE-faithful. More work, but fixes the reasoning rather than filtering its output — e.g. bracket each real by the two nearest representable doubles (round-toward-zero / round-away) so any realized value round-trips to what CPython computes, or model these ops on z3's floating-point sort directly.

Filed off the back of the support-grid regeneration work (lineage of #454).