gft interpreter: pin renormalisation carry at all four sites (Refs #2161) - #2648
Merged
Conversation
) `enc`, `_magmul`, `_magadd` and `_magsub` all end in if mant >= 512: mant = 0; <exponent> += 1 and all four survived the `>=` -> `>` boundary mutant, for one shared reason: the mutant leaves mant == 512, and `(off << 9) | 512` is IDENTICAL to `((off + 1) << 9)` whenever `off` is EVEN, because 512 == 1 << 9 is the low bit of the exponent field. The stuck mantissa renormalises the value by accident across half the exponent space. Two further reasons a sweep misses this, both measured: * mant == 512 is reached only by rounding UP from 511, so a sweep of exactly-representable inputs never enters the branch; * in `_magmul` the carry path cannot reach it in principle -- the largest product 1023 * 1023 == 1046529 gives q == 1022, mant == 510. Four assertions, each checked both ways: holds clean, fails when its own site is mutated, catches no other site's mutant. Boundary column for this file, measured after the change: killed 8/31 -> 12/31.
Contributor
PR DashboardGenerated at: 2026-08-24 02:12:10 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
…#2161) The gate asks for docs/now/<date>-<slug>.md, which is where 184 entries live. Root NOW.md has not changed on master since 2026-08-09; editing it satisfied nothing and was the wrong file.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-24 02:15:31 UTC
Summary
Seal Status
|
… (Refs #2161) Section 116. The mechanism (512 == 1 << 9 is the low bit of the exponent field, so a stuck mantissa renormalises for free on even exponents), the three probe failures that hid it, and the two controls that localised the fault to the input space rather than the harness.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-24 02:16:34 UTC
Summary
Seal Status
|
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.
enc,_magmul,_magaddand_magsuball end in the same line:All four survived
>=->>, and one mechanism explains all four: the mutant leavesmant == 512, and(off << 9) | 512is identical to((off + 1) << 9)wheneveroffis even —512 == 1 << 9is the low bit of the exponent field, so the stuck mantissa renormalises the value by accident. Half the exponent space hides the defect.Three probes read "no difference", all three about the probe
1.0 + k/4096off = 40— even, so the mutant is invisible(512+k)·2^(e−9)mant == 512is reached only by rounding up from 511 — the branch is never entered__pycache__The third is the sharpest: all four sites reported the same difference count at the same position, in a function three of them do not touch. An impossible result is the cheap signal — a plausible one would have shipped.
A positive control on the harness (planting a known-live mutant, expecting differences) is what proved the harness worked while its answers were still wrong.
One site is structurally different
In
_magmulthe carry path cannot reachmant == 512in principle: the largest product is1023 * 1023 == 1046529, givingq == 1022,mant == 510. Only the no-carry path distinguishes that site. My hand-derivation saidq == 1021; the computation said1022. Computed, not derived.Assertions
Each was checked both ways — holds clean, fails when its own site is mutated — and none catches any other site's mutant, so all four are load-bearing rather than three plus a duplicate.
Boundary column for this file, measured after the change: killed 8/31 → 12/31.
Refs #2161