stillwater-sc / universal / 30477756954

85%

master: 84%

push

github

feat(interval): Stage-2 EFT tightness for cfloat with subnormals (#1255) (#1256)

* feat(interval): Stage-2 EFT tightness for cfloat with subnormals (#1255)

cfloat with hasSubnormals=true is genuine IEEE-754 (RNE + gradual underflow), so
its TwoSum/TwoProduct are exact in the safe band exactly like native floats (the
only failures are the universal over/underflow boundary caveats). Enable the
Stage-2 tight enclosures for it, gated on the subnormal flag AND 2*digits <= 53.

interval_eft_exact<cfloat<nbits,es,bt,true,sup,sat>> is true iff 2*(nbits-es)<=53.
The gate guarantees the exact product of two significands fits in a double, so
prod_enclose verifies the rounding direction by exact double promotion instead of
the native frexp/ldexp path -- cfloat's own frexp/ldexp misbehave at narrow
configs (frexp(cfloat<8,2>) does not normalize; ldexp overflow returns garbage).

Three robustness fixes, each needed for soundness across cfloat configs:
- prod_enclose branches at the top on is_floating_point: native keeps the frexp
  normalized-domain path (#1252); cfloat uses double-verified direction.
- operator/= reciprocal EFT residual is gated on native floats too; cfloat uses
  the Stage-1 (unconditional outward) reciprocal, then the tight *= recovers most
  tightness.
- round_down/round_up clamp NaN to -/+inf. cfloat's nextafter(maxneg,-inf) returns
  NaN at the boundary; without the clamp an overflowing corner product yielded a
  NaN that std::min silently swallowed, producing a too-tight (unsound) lower
  bound. -/+inf is the correct directed value there (also improves Stage-1).

Verified: 0 containment breaks over 68M+ samples (+ - * / sqr sqrt) across
cfloat<8,2>+sub, <10,4>+sub, <16,5>+sub, <32,8>+sub, <16,5>+sub+inf -- wide
(bit-for-bit IEEE) and pathologically narrow alike. cfloat WITHOUT subnormals
stays Stage-1. Regression added to containment.cpp (EFT cfloat<16,5>+sub and the
narrow cfloat<8,2>+sub); VerifyContainmentFuzzT now scales its operand ra... (continued)

25 of 25 new or added lines in 1 file covered. (100.0%)

41605 of 48809 relevant lines covered (85.24%)

7173558.36 hits per line