Unsound: `crosshair check` confirms `a != Decimal("2")` (symbolic Decimal cannot reach most nonzero values)

[pschanely]

Summary

crosshair check unsoundly confirms contracts of the form a != Decimal("<nonzero>"). The symbolic Decimal proxy appears to explore only a limited value domain — it can reach Decimal("0") but not most nonzero values — so a postcondition asserting a Decimal argument is never some specific nonzero value is "Confirmed over all paths" even though a violating input exists.

Minimal repro

from decimal import Decimal

def f(a: Decimal):
    """
    post: a != Decimal("2")
    """
    return a

$ crosshair check --report_all repro.py
repro.py:5: info: Confirmed over all paths.
$ echo $?
0

But f(Decimal("2")) returns Decimal("2"), and Decimal("2") != Decimal("2") is False — the postcondition is violated, so the confirmation is unsound.

It's value-dependent (reaches 0, misses nonzero)

post:	result	correct?
a != Decimal("2")	Confirmed over all paths	❌ unsound (f(Decimal("2")) violates)
a != Decimal("0")	false when calling f(Decimal('0'))	✅ counterexample found
a < Decimal("0")	false when calling f(Decimal('0'))	✅
a + Decimal(1) != a	Not confirmed	✅ (UNKNOWN)

So the symbolic Decimal can produce Decimal("0") but not Decimal("2") — the reachable set is too narrow, and asserting a nonzero target is confirmed unreachable.

Suspected area

crosshair/libimpl/decimallib.py — the symbolic construction (_make_decimal / the sign·digits·exponent representation). Sign/exponent look exercised (0 is reachable) but the coefficient/digit-string domain seems to exclude ordinary values like 2. A direct probe shows symbolic_decimal == Decimal(2) returning a concrete False (no solver variable), consistent with the reachable set never including 2.

Environment

• CPython 3.13, C _decimal active (decimal.__libmpdec_version__ == "2.5.1").

Notes

Surfaced by the measured stdlib support-map tooling: because the holdout inverts each op against a concrete output target, every decimal.Decimal method inherits this single root cause and renders as a black ("wrong answer") cell — one bug shown as many cells.