stillwater-sc / universal / 26399740586

84%

master: 84%

Build Type

push

github

Committed by web-flow

Commit Message

feat(internal): EFT primitive exactness proof (#988, #987 Layer 1) (#994)

* docs(ereal): verification failure-mode assessment + dyadic oracle (WIP, epic #987)

Captures the ereal/Priest verification gap (structural + self-referential
oracles never check exact value), the 3-layer remediation plan, and the
discovery that both candidate exact-arithmetic backends are broken
(einteger multiply #991, erational conversion #986). Includes the dyadic
exact-rational oracle header; blocked on a sound integer backend.

Relates to #987. WIP -- not for merge until #991 and #986 are fixed.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* feat(expansion): prove EFT primitive exactness against exact oracle (#988, #987 Layer 1)

Layer 1 of the ereal/Priest conformance epic #987. Verify the three error-free
transformations the expansion algorithms rest on satisfy their defining exact
identities, against an independent exact dyadic-rational oracle (dyadic_exact.hpp,
einteger-backed -- no shared code with the transforms):

  two_sum / fast_two_sum:  s + e == a + b  exactly (s == fl(a+b))
  two_prod:                x + y == a * b  exactly (x == fl(a*b))

internal/expansion/primitives/eft_exactness.cpp: oracle self-check, structured
edges (equal magnitude, opposite signs, subnormal tails, ties, signed zero,
large exponent gaps), and randomized fuzz across the exponent range, L1..L4.
two_sum holds for any finite sum; two_prod within the normal-product band (its
error term is unrepresentable on subnormal underflow). fast_two_sum is fed
|a|>=|b| (its precondition, guaranteed at the priest_renormalize call site) and
the test confirms that precondition is load-bearing. VerifyTwoProd doubles as a
platform check that std::fma is correctly rounded.

Includes the verification failure-mode assessment doc and the dyadic oracle.
gcc-13 + clang-18 PASS.

Relates to #987.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(internal): addr... (continued)

Coverage Stats

117 of 127 new or added lines in 2 files covered. (92.13%)

2 existing lines in 1 file now uncovered.

47569 of 56582 relevant lines covered (84.07%)

8724937.21 hits per line