stillwater-sc / universal / 27021302154

85%

master: 84%

Build Type

push

github

Committed by web-flow

Commit Message

fix(elreal): addRec_step emits the canonical 0-overlap form (#1057) (#1064)

add()'s streaming addRec_step could emit a VALUE-CORRECT but NON-canonical (0-overlap-
violating) expansion. Root cause (instrumented): the gs-empty / fs-empty re-injection
path (FCL.hs `addRec fs [] (e:es) bound = e:...`) emitted the workspace head `e`
unconditionally. But a prior twoSum merge can LOWER e's exponent toward an un-merged
operand block -- e.g. a1@146 + residual -> @142 while the canonical a2@91 is now only
51 < k below it -- and a carry can push the operand one bit higher still. Emitting e
then leaves an adjacent pair closer than k.

Fix: before emitting the workspace head, fold any remaining operand block whose exponent
is >= head.exponent() - k into the workspace via priestAdd (which renormalises). The
">=" accounts for the +1 carry a same-exponent merge can produce. Applied symmetrically
to the gs-empty and fs-empty paths.

This is the root of both #1057's exact-cancellation symptom (asin+acos) AND the #1061
streaming-infSum blocker (repeated add composition). It also subsumes the leading-pair
overlap class (#1044) in the streaming path.

Validation:
- minimal repro: add gives canonical (...,87,...) matching priestRenorm
- 1,000,000 randomized single-adds: 0 0-overlap violations (asserts ON), value exact
- left-fold composition n=3..20: 0 violations, value == eager sum()
- full elreal suite (34 tests) PASS on gcc AND clang; no regressions
- regression test added to el_arith_add_renormalization (minimal repro + 50k fuzz vs the
  exact-dyadic oracle), passes gcc + clang

Resolves #1057

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

Coverage Stats

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

20 existing lines in 3 files now uncovered.

47611 of 56325 relevant lines covered (84.53%)

6031922.74 hits per line