stillwater-sc / universal / 26374781759

84%

master: 84%

Build Type

push

github

Committed by web-flow

Commit Message

feat(ereal): add Priest normal-form structural oracle (#954 D1) (#983)

First deliverable of the first-principles verification machinery (#954): a
no-external-oracle structural check that an ereal expansion is in Priest normal
form, derived directly from the limb vector.

include/sw/universal/verification/ereal_test_support.hpp:
- check_priest_normal(limbs) / check_priest_normal(ereal<N>) returning a
  structured PriestNormalResult { violation, index } so a fuzzer failure points
  at the exact broken invariant; plus an is_priest_normal() predicate.
- Checks: decreasing magnitude, non-overlapping (|z_{k+1}| <= ulp(z_k)/2), no
  interior zero components (canonical zero is the single {0.0} limb).
- Deliberately NO length<=maxlimbs check: investigation under #981 showed
  maxlimbs is the algorithmic ceiling on inputs, not a cap on result length (a
  non-overlapping product can need >maxlimbs components for a wide-range value).

elastic/ereal/arithmetic/priest_normal_form.cpp:
- unit-tests the oracle on crafted limb vectors (normal, non-decreasing,
  overlap, interior-zero) -- exercising the rejection logic that ereal's own
  ops would never produce.
- structural fuzzer asserting every +, -, *, / result over random
  multi-component expansions is Priest-normal (LEVEL_1..4 = x1k..x1M).

This passes only because #981 fixed expansion_product's missing renormalize;
before that, * and / produced ~93% overlapping results. Verified on gcc-13 and
clang-18 through x100k.

Relates to #944
Relates to #954

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

Coverage Stats

15 of 22 new or added lines in 1 file covered. (68.18%)

4 existing lines in 1 file now uncovered.

47343 of 56373 relevant lines covered (83.98%)

8603515.91 hits per line