stillwater-sc / universal / 26403525480
84%
master: 84%

LAST BUILD BRANCH: fix/issue-ci-ereal-regression-runtime
DEFAULT BRANCH: master
Ran
Jobs 1
Files 660
Run time 2min
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst
coverage: 84.059% (-0.01%) from 84.071%
26403525480

push

github

web-flow 
feat(ereal): independent exact-value oracle -- keystone (#989, #987 Layer 2) (#995)

* feat(ereal): independent exact-value oracle -- keystone (#989, #987 Layer 2)

Layer 2 of epic #987, the keystone the whole effort was for: prove ereal does
not just produce well-shaped (Priest-normal) and self-consistent results, but
the EXACT mathematical value -- checked against a reference that shares no code
with the expansion algorithms.

elastic/ereal/arithmetic/exact_value_oracle.cpp: the exact value of an expansion
is the sum of its non-overlapping limbs as exact dyadic rationals
(dyadic_exact.hpp, einteger-backed). ereal's +, -, * are error-free, so for
random multi-component operands:

    exact_value(a op b) == exact_value(a) op exact_value(b)   (bit-exact)

This catches normalized-but-wrong values, which neither the structural oracle
(#954, shape) nor the precision-lifting oracle (ereal<N> vs ereal<19>,
self-consistency) can. Configs ereal<2/4/8/16>, fuzz L1..L4, gcc-13 + clang-18
PASS with 0 failures.

Operands are centered in the exponent band (-511, 511) so every partial product
stays a normal double: an expansion spanning > ~1022 binary exponents cannot
have an exact double-limb product regardless of algorithm (low bits fall below
DBL_TRUE_MIN). Within the representable band the product identity holds exactly.
Division is not exact (a quotient need not be dyadic), so it is checked with a
relative-error bound rather than equality.

Relates to #987 (Layer 2 of 3).

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

* docs(ereal): clarify close_rel tolerance comment (CodeRabbit PR #995)

Describe the actual predicate: close if |x-y| <= absTol OR |x-y| <= relTol*max(|y|,absTol).

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

---------

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

47564 of 56584 relevant lines covered (84.06%)

8724879.88 hits per line

Coverage Regressions

Lines Coverage ∆ File
5
50.45
 -4.5% include/sw/universal/verification/posit_test_suite_randoms.hpp
3
81.03
 -0.45% include/sw/universal/number/posit1/specialized/posit_16_1.hpp
2
89.78
 0.0% include/sw/universal/number/posito/posito_impl.hpp
Jobs
ID Job ID Ran Files Coverage
1 26403525480.1 660
84.06
 GitHub Action Run
Source Files on build 26403525480