conformance: promote gf96 selfconsistent -> strict SW-bitexact (71/4/8)#1367
Merged
Conversation
Promote gf96 (GoldenFloat96: S1 E36 M59, BIAS=34359738367=2^35-1) from bitexact_selfconsistent to strict bitexact. INDEX totals 70/5/8 -> 71/4/8 (bitexact / selfconsistent / structural, sum=83). Status tag: [verified SW] (software chain, NOT on-silicon Tier-E; encoding != compute != FPGA). gf96 has M=59 > 52, so binary64 cannot hold the mantissa exactly: there is NO FP lowering and NO rounding. Every finite gf96 value is an exact dyadic rational. Proof = analytic zero-rounding separation-bound + two structurally independent EXACT decode paths (no RTL bit-model / iverilog needed): - Witness 1 (dyadic independent decoder): 15/15 bit-exact (abs_error=0). - Witness 2 (golden Fraction oracle, different internal representation): 15/15 exact vs pack. - Two-path cross-check: 201512/201512 agree (5-class + exponent boundaries + full-mantissa edges + deep-underflow/overflow + 200k random seed=96). Memory note: +-2^35 exponent => 2^(exp-BIAS) is never materialized as an integer (would OOM); both paths keep the huge power symbolic (peak RSS ~14 MB). Files: - conformance/vectors/gf96_conformance_v0.json: witnesses[] array + refined structural_reason; new sha256. - conformance/vectors/INDEX_all_formats.json: gf96 kind=bitexact + new sha; counts recount 71/4/8. - conformance/witness/gf96/: README.md, gf96_decode_ref.py, cross_check_representative.py, SEPARATION_BOUND.md (English/ASCII). - docs/NOW.md: gf96 promotion section; remaining selfconsistent 5 -> 4. wp18_conformance_gate verdict CLEAN. HW-decode / HW-compute remain [REQUIRES USER ACTION] (trinity-fpga #199). Additive only; SSOT untouched. Remaining selfconsistent: gf128, gf256, gf512, gf1024 (gf256 do NOT promote). Anchor: phi^2 + phi^-2 = 3. Closes #1366
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Promote
gf96(GoldenFloat96: S1 E36 M59, BIAS=34359738367=2^35-1) frombitexact_selfconsistentto strict SW-bitexact. INDEX totals70/5/8 -> 71/4/8 (bitexact / selfconsistent / structural, sum=83).
Status tag: [verified SW] — software chain, NOT an on-silicon Tier-E claim.
encoding != compute != FPGA.
Why the proof differs from gf48 (#1358)
gf48 (M=29) lowers exactly into binary64 (52-bit mantissa) with RNE only on the
FP64-subnormal edge, so #1358 used a fixed-width FP64 RTL bit-model + iverilog.
gf96 has M=59 > 52, so binary64 CANNOT hold the mantissa exactly — a binary64
lowering WOULD round. The pack therefore stores every value as an EXACT dyadic
literal (
value_encoding=dyadic) and the decode has NO rounding: every finitegf96 value is an exact dyadic rational. The iverilog-FP64 witness is not
applicable and no RTL bit-model is required (there is nothing to round). The proof
is an analytic zero-rounding separation-bound plus two structurally independent
EXACT decode paths.
Witnesses (all pass in-sandbox)
conformance/gf_wide_independent_witness.py):15/15 bit-exact (abs_error=0).conformance/witness/gf96/gf96_decode_ref.py,DIFFERENT internal representation):
15/15 exactvs pack.conformance/witness/gf96/cross_check_representative.py):201512/201512 agreeover 5-class + exponent boundaries + full-mantissa edgesconformance/witness/gf96/SEPARATION_BOUND.md):zero-rounding lemma => deterministic over the whole domain.
Memory note: the +-2^35 exponent means
2^(exp-BIAS)is NEVER materialized as aninteger (would OOM); both paths keep the huge power symbolic (peak RSS ~14 MB).
Files
conformance/vectors/gf96_conformance_v0.json—witnesses[]array + refinedstructural_reason; new sha256
43127e758d653d26640d38801d42d4daf36fdc70df66a63aadac6a8ce06159fa.conformance/vectors/INDEX_all_formats.json— gf96kind=bitexact+ new sha;counts recount 71/4/8.
conformance/witness/gf96/— README.md, gf96_decode_ref.py,cross_check_representative.py, SEPARATION_BOUND.md (English/ASCII).
docs/NOW.md— gf96 promotion section; remaining selfconsistent 5 -> 4.Gates
tools/wp18_conformance_gate.pyverdict = CLEAN (recomputes per-pack sha).docs/NOW.mdin diff (now-sync-gate);Last updated: 2026-07-05.Closes #1366.Scope / honesty
AX7203, trinity-fpga Ring 052: Lotus phase automation — brain seal refresh pipeline #199).
gf256 stays open (bitexact:false, open bias R&D) — do NOT promote.
Anchor: phi^2 + phi^-2 = 3.
Refs #1366