Two whitebox cases per branch, from different fields: closing E20's second cause - #37
Merged
Conversation
`_takeCase` kept the FIRST block per label and refused the rest. The generators
loop `for F in FIELDS` with FIELDS ascending, so that made every branch's one case
come from the SMALLEST field reaching it -- the most degenerate arithmetic
available. That is the second cause of ERRATA E20: `ADD33`'s case has `t8 = 0`, so
the corpus could not distinguish a change to that term, and a correct -2M -2A
saving was reverted because deliberately breaking the line also measured green.
Measured on the genus-3 nch2 family, perturbing every executed assignment by one
and asking whether the returned divisor moves:
one case at GF(3), as shipped 20.0% of assignments invisible
one case at GF(5) 9.7%
TWO cases both at GF(3) 11.8% <-- worse than one at GF(5)
two cases, GF(3) and GF(5) 7.1%
So one case per (label, field) is a CONSTRAINT rather than a preference: two draws
at one field share that field's coincidence probabilities and the second is blind
to most of what the first is. Spreading across fields is what buys detectability.
The quota is per CHARACTERISTIC CLASS, which is what gives arb four cases without a
per-family table -- nch2 admits only odd fields and ch2 only even ones, so each
takes two, while arb admits both and takes two of each. That matters for arb
specifically: as shipped its genus-3 corpus was 45 cases in characteristic 2
against 3 in odd characteristic, so 45 of its 48 branches had never been
whiteboxed in odd characteristic at all, in the one family that must work in every
characteristic.
Selection is two-pass. `_takeCase` banks one block per (label, field) and
`applyQuota` then keeps the LARGEST fields per class, because applying the quota
greedily would keep the two smallest -- a milder version of the same bias. On ch2
genus 3, whose log holds GF(2), GF(4) and GF(8), greedy gives GF(2)+GF(4) where
the quota gives GF(4)+GF(8).
Nothing is capped silently. `parseLog` prints the fields kept, the case count as
well as the branch count, and names every branch left below quota -- which is what
tells you to extend the ladder. A silent one-case branch is precisely what let a
correct saving be reverted. Also fixed: the closing message reported `len(cases)`,
saying "48 cases" for a tester holding 94.
`whitebox.py` answers "is every branch reached?" and has answered yes for a long time -- 1,925 of 1,929 labels. That is COMPLETENESS, and it is not ADEQUACY. A branch reached by one case whose arithmetic happens to zero a term cannot distinguish a change to that term, so the branch is covered and the change is still invisible. ERRATA E20 is that gap costing something real, and it is why this exists: a correct -2M -2A saving at `ADD29`/`ADD33` was applied, measured green under real Magma across 2,119 comparisons, and reverted -- because deliberately breaking the same line ALSO measured green. Nothing in the repository could express the difference between "the tests pass" and "the tests would notice", so the honest move was to revert a change that was probably right. This closes that gap. Every assignment the corpus executes is perturbed by one and the operation's returned divisor compared. If the divisor does not move, that assignment is invisible: nothing would catch a change to the expression producing it. Two decisions in the metric, both of which a naive version gets wrong. ONLY THE Deg* BODIES ARE SCORED. Counting every layer gives 48.2% invisible where the formula bodies are at 18.7%, because the split dispatchers unpack `ccs` into some sixty named constants of which any branch reads a handful, and perturbing a constant a branch never reads is dead unpacking rather than a blind spot. The other layers are reported separately rather than dropped. SCORED BY BRANCH, NOT BY CASE. An assignment is invisible only if EVERY case covering that branch misses it. Summing per case instead means adding a redundant case can LOWER the score, which is wrong for a metric whose entire point is that more cases cannot hurt -- it also understated the two-case corpus at 85.9% where the union is 93.3%. Cases covering one branch run the same assignments in the same order, so the union is a plain intersection of their blind sets. The `selftest` section holds the instrument to both its claims: that it is faithful, since it copies `maginterp.run` rather than wrapping it and must reproduce the real interpreter exactly when nothing is perturbed; and that it is sensitive, since an all-zero or all-invisible answer would mean the perturbation never lands or the comparison never fires. Deliberately a RELATIVE instrument. 100% is not reachable and is not the target: `f7` is assigned and never read and is not deletable, a branch guarded on `d = 0` must have `d = 0` to be reached, and the adjugate entries are dead on the degenerate paths that do not consume them. Use it to show one corpus strictly better than another.
Corpus 1,886 -> 2,146 cases. Branch coverage is UNCHANGED at 1,925 of 1,929 with
the same four exemptions, because coverage is label-keyed and a label gaining a
second case does not move the denominator -- `coverage_baseline.json` needed no
edit, which was predicted and then checked rather than assumed.
family cases fields detectability
arb g3 48 -> 190 GF(2,3,4,5) 81.8% -> 95.8%
nch2 g3 48 -> 96 GF(3,5) 80.0% -> 93.3%
ch2 g3 48 -> 96 GF(4,8) 81.4% -> 88.3%
ch2 g2 22 -> 44 GF(4,8) 87.9% -> 94.4%
arb gains most because it gains a characteristic. It was 45 cases in
characteristic 2 against 3 in odd characteristic and is now 94 against 96, so its
branches are exercised in both regimes rather than almost entirely in one.
THE ACCEPTANCE TEST, which is the point of the whole exercise: E20's own mutation,
dropping `t8` from `ADD33`'s `C0`, was applied to the live formula file. The
committed 48-case corpus reported 48/48 matched and MISSED it, reproducing the
original failure exactly. The new 96-case corpus CAUGHT it, 94 of 96. The file was
then restored and the corpus verified green, and no .mag formula file is touched by
this commit.
nch2 needed 12 curves per field where the budget of record was 3: at 3 curves,
`DBL02` and `DBL06` reached only GF(3) and the shortfall report named them. That
was rarity rather than a field ceiling -- `DBL02` appears once in 27,030 blocks --
so more trials fixed it without needing GF(9), which measured no better than GF(5)
anyway while taking twenty minutes against seconds.
Two arb branches, `ADD06` and `ADD26`, hold three cases rather than four. Named by
the shortfall report rather than accepted quietly.
Out of scope here and stated rather than implied: arb and nch2 at genus 2 keep one
case per branch, because their generators are the older generation -- `while true`,
`Random(FIELDS)` over a set rather than an ascending loop, and no WB_TRIALS or
WB_FIELDS -- so they cannot be re-driven without modernising them first. The four
split families need real generation runs, their committed logs being partial:
rebuilding nch2_splitG3 from its log reaches 86 of 405 branches.
Gates: whitebox all 2,146 replayed and matched, coverage unchanged; driver --strict
13,746/13,746; opcount byte-identical across all fifteen families; dominance clean
on 39 files; selftest 19 passed 0 failed 0 skipped; Magma 30 testers 0 failures 0
skips, its own logs confirming 190/96/96/44 cases executed rather than an unchanged
file.
ERRATA E20's second cause is fixed and the entry says how: the cause was a selection rule, not bad luck. `ADD33`'s `t8 = 0` was the predictable consequence of taking GF(2) when GF(8) sat in the same log, and every one of the 1,886 cases had at least one invisible assignment, so it was systemic rather than a handful of branches. N32 records it at publication depth. The transferable result is that a suite can reach every branch of a program and still not see a change to it, and that the distinction is measurable rather than rhetorical -- perturb each computed value and ask whether the output moves. Three findings there were not obvious in advance: two cases at the SAME field are worse than one case at a bigger field, because same-field failures are correlated; field size saturates at one step up while its cost does not, GF(9) gaining nothing over GF(5) for twenty minutes of Magma; and the quota belongs to the characteristic class rather than the family, which is what exposed arb's genus-3 corpus being 45 characteristic-2 cases against 3 odd ones. A CORRECTION TO MY OWN RECORD, and it is the honest-limits item in N32. PR7+8's outcome summary said the `ADD29`/`ADD33` saving was reverted and stopped there, so this work's plan claimed it would be recovered. It had already been recovered, in PR7+8 itself, once the exhaustive GF(4) probe gave it an oracle -- `0fa1def` says so explicitly and the code carries the collapse at both leaves. So THIS WORK RECOVERS NO OPERATIONS and its case is detectability alone. Two lessons: a summary that records a refusal must record its resolution, and here the errata entry was the reliable record where my summary was not. Counts re-derived rather than moved, since that figure has gone stale three times in this series: 2,146 cases across 15 testers, measured. The description moved with it -- "one per computation path" is no longer true, and README, verification/README and the CI comment all said it. Note the recount itself needed care: keying cases by BASENAME collapses `arb_splitG2_whiteBox_tester.mag`, which exists under both posReduced and negReduced, and silently loses 231 cases -- the same duplicate- basename hazard PR12 fixed 19 call sites for.
Groundwork for extending the two-cases-per-branch corpus past the four ramified
families. Changes no tester and no formula; every figure in the repository is
unaffected.
THE SIX GENUS-2 GENERATORS WERE THE OLDER GENERATION. `while true do`, a field
drawn by `Random(FIELDS)` from a hardcoded set, the output path hardcoded into
`SetOutputFile`, and no environment budget at all. Three consequences, each
measured rather than assumed:
- they cannot be driven by whitebox_auto_NEG.py, which sets a budget and waits
for the run to finish: a `while true` loop never finishes;
- `Random(FIELDS)` makes field coverage itself random, so a field in the set can
contribute nothing to a run;
- and the ladder cannot be widened, which is what actually blocks the quota.
`arb_ramifiedG2`'s {3,4,5,7} holds exactly ONE even-characteristic field, so
every one of its 22 branches comes up a case short of the four that
two-per-characteristic-class asks for.
All six now read WB_FIELDS, WB_TRIALS, WB_SEED and WB_LOG, and sweep every field in
the ladder rather than sampling it. The arithmetic, the pair construction and the
emitted block format are untouched, so a regenerated tester differs from its
predecessor only in which cases were kept. Verified by running all six under real
Magma: each loads, honours the ladder, and emits parseable blocks.
Worth recording why the cheaper route was abandoned. These generators redirect
their own output with `SetOutputFile`, so running one and capturing stdout gives
nothing -- 100 seconds of `arb_ramifiedG2` produced an 8-line stdout and a 14MB log
at the hardcoded path. That is usable, and it is how the ch2 genus-2 tester in the
previous commit was built; but the path cannot be chosen, the loop cannot be
bounded, and the ladder cannot be widened, so it is a way to read an old run rather
than to commission a new one.
THE TOOL COULD NOT TARGET posReduced AT ALL. `FileInfo` hardcoded `negReduced/`, so
three of the fifteen testers were unmaintainable by the tool that maintains the
other twelve. They are not interchangeable: a case records the result the formulas
produced, and the two bases normalise v against different polynomials at infinity,
so a negReduced case replayed against posReduced formulas compares a different
divisor -- `whitebox.py` already keys on the basis for exactly that reason. `--basis`
now selects it, and WB_BASIS is forwarded through MAGMA_ENV, without which it would
silently not reach the generator.
Still outstanding for posReduced, and stated rather than implied: the three split
generators are deeply negReduced-specific beyond their load paths --
`RandomDivisor_SPLIT_NEG`, `Add_SPLIT_NEG`, `Double_SPLIT_NEG`, and `nV` rebuilt
from `Vn`. All 22 `_SPLIT_POS` counterparts exist in
`genFiles/reduced_basis_arithmetic.mag`, so this is a mechanical copy-and-swap into
three POS generators rather than new mathematics, but it is not done here.
It fired before the budget block that defines WB_LOG, so it landed at a path WB_LOG cannot influence and left an untracked file behind on every run -- three of them, since whitebox/logs/*_splitG2_log.txt is not gitignored the way the ramified ones are. It only ever wrote a 'Loaded ...' banner; the real log is opened by SetOutputFile a few lines below. Re-verified under Magma after removal.
All six ramified families now hold two cases per branch per characteristic class.
Corpus 2,146 -> 2,233; coverage unchanged at 1,925 of 1,929.
family cases ladder detectable
arb g2 22 -> 88 3,5,4,8 86.1% -> 96.5%
nch2 g2 22 -> 44 3,5 93.2% -> 94.1%
ch2 g2 44 -> 43 4,8 94.4% -> 95.7%
ramified total ~81% -> 93.0%
arb genus 2 gains most for the same reason arb genus 3 did -- it reaches full quota
in both characteristic classes, 88 cases against 22, where before it had three
characteristic-2 cases in the whole corpus.
ch2 genus 2 is regenerated rather than left as it was, and now has ONE case fewer
while being more detectable. The previous version was built from an existing 43MB
log because its generator could not be driven; this one comes from a recorded
budget, so it can be reproduced.
APPLYQUOTA NOW TAKES THE LADDER IN ORDER, WHICH REVERSES THE EARLIER LARGEST-FIRST
RULE. "A bigger field has fewer coincidences" is true on average and useless as a
selection rule -- the variance between individual cases swamps it. Measured on nch2
genus 2, same generator, same 400 curves per field, only the ladder differing:
ladder kept invisible of 236
{3,5,7} 3,5,7 13
{3,5} 3,5 14
{3,7} 3,7 19
{3,5,7,9,11} 9,11 24 <-- largest-first picked these
one case, shipped 3,5,7 16
Largest-first turned a corpus that should have improved on the shipped one into a
REGRESSION: 16 invisible becoming 24. Taking the ladder in order makes the ladder
the knob -- visible in the generator, chosen per family, checked by measurement --
instead of burying the choice in a heuristic invisible from outside. A family whose
best pair is its two largest fields lists those two.
And the ladder is chosen by MEASURING candidates, not by reasoning about field
size, because a ladder change also shifts every later curve: the generator draws
from one RNG stream, so adding GF(3) to a ladder changes which GF(5) curves appear.
Four to five candidates were built per family and the most detectable kept, with
the committed corpus as the bar -- a regenerated corpus that scores worse than the
one it replaces is not an improvement, whatever rule produced it. Candidates that
regressed are recorded above rather than discarded quietly.
Gates: whitebox all 2,233 replayed and matched, coverage unchanged; selftest 19/0/0;
driver --strict 13,746/13,746; Magma 30 testers 0 failures 0 skips. No formula file
touched. Case counts re-derived in README, verification/README and checks.yml.
…aid "which?" TWO DEFECTS, both found by trying to extend the corpus past the ramified families. THE EMITTER READ THE WEIGHT AT A FIXED INDEX. The two genuses talk to different reference libraries and those libraries disagree on a divisor's shape: genus 2 loads reduced_basis_arithmetic.mag, whose divisor is <u, v, w, n> carrying the cofactor w = (f - v(v+h))/u explicitly, and genus 3 loads poly_balanced_arithmetic.mag, whose divisor is <u, v, n> -- AdaptedBasis there returns <D[1], vhat, D[3]>, three slots. Index 2 is the weight at genus 3 and the COFACTOR at genus 2, so a generated genus-2 case read `N2 := x + FF.1^2`, a polynomial where an integer weight belongs, and every case was unparseable: 295 extract errors, 0 replayed. This is the exact inverse of the defect PR12 fixed. That change moved the emitter from the 4-tuple form to the 3-tuple one for genus 3 and thereby broke genus 2, which went unnoticed for the plainest reason -- no genus-2 split tester has been regenerated since, so the deployed three predate the break. The emitter has been unable to produce a correct one that whole time. `d[-1]` is right under both conventions. Two more things were genus-3-shaped and are now genus-aware: the divisor tuple itself, where genus 2 reconstructs w inline exactly as its deployed testers do (w is redundant rather than extra, being derivable from u, v, f and h); and the reference operation, where genus 2 must assert against Add_SPLIT_NEG or Add_SPLIT_POS according to basis while genus 3 has one library function. polyV likewise took its top coefficients from Vn unconditionally, so a posReduced tester would have rebuilt v against the negative basis and compared a different divisor. Verified: a regenerated arb genus-2 split tester now replays 295 of 295, matched, 0 mismatches, and its emitted case is line-for-line the shape of the deployed one. DETECT.PY LABELLED ROWS BY BASENAME. `arb_splitG2_whiteBox_tester.mag` exists under both posReduced/ and negReduced/ -- different algorithms with different costs -- so a run over both printed two identically named rows and there was no way to tell which basis either belonged to. I hit this while trying to read my own output. PR12 fixed the same hazard at 19 call sites; this is a twentieth, in a tool written after it.
…ot better
Corpus 2,233 -> 2,607. All three negReduced families improve, measured with the
same instrument on both sides:
family cases ladder detectable
arb g2 neg 77 -> 304 3,5,4,8 77.2% -> 78.5%
nch2 g2 neg 77 -> 152 5,7,9 84.6% -> 85.4%
ch2 g2 neg 77 -> 149 4,8,16 82.0% -> 82.9%
Small gains next to the ramified families' ten-plus points, and the reason is
recorded rather than glossed: the assignment count rose from 1,559 to 2,462 where
per-branch scoring should hold it fixed, which means detect.py is splitting one
branch into several groups when its cases traverse different LABEL SETS -- a
differing UTL or dispatcher label is enough -- so their blind sets are never
intersected and the union benefit is suppressed. The comparison above is still
like-for-like, both sides measured the same way, but the true gain is larger than
it shows. Fixing the grouping is separate work.
A BASELINE EXEMPTION DIED OF PROGRESS. `ch2_splitG2_UTL`'s UTL0 was exempt because
"the rarest leaf is 0.88% of curves and a corpus of ~130 sampled curves misses it
about a third of the time" -- and a corpus drawing 800 curves across four fields
hits it. The gate refused to pass on the now-stale exemption, which is exactly the
PR3 rule working: an exempt label that IS reached must be re-recorded rather than
silently kept. Repository coverage 1,925 -> 1,926 of 1,929.
posReduced IS NOT IN THIS COMMIT, and Magma is why. I generated all six, and the
Python gates passed all six -- whitebox replayed 295 of 295 matched for arb pos --
while the Magma suite failed all three posReduced testers on assertions. The cause
is the one I had already written down and then walked past: `--basis pos` routes
the paths, the label counting and the emitter, but the split genus-2 GENERATORS are
negReduced to their bones (`RandomDivisor_SPLIT_NEG`, `Add_SPLIT_NEG`, negReduced
loads), so they produced negReduced cases that the emitter then labelled as
posReduced. Reverted; posReduced needs the three POS generators, which is real work
and not plumbing.
Worth stating plainly because it is the second time in this series: the Python
gates and Magma are not redundant. whitebox replays through the interpreter and
agreed with itself about a divisor that Magma's own arithmetic rejects.
Gates: whitebox all 2,607 replayed and matched, coverage 1,926/1,929; selftest
19/0/0; driver --strict 13,746/13,746; Magma 30 testers 0 failures 0 skips. No
formula file touched.
An assignment was keyed by its index in the execution trace, and the per-branch
union intersected blind sets by that index. That is correct only while every case
reaching a branch executes the identical prefix, and they do not: `Precompute` has
eight exits taking different numbers of assignments, so a case whose curve routes
through a different leaf shifts every later index and nothing lines up. The
grouping key had the same problem one level up, since it included UTL labels --
Precompute's own exits, a property of the CURVE rather than of the operation under
test -- so two cases exercising the same formula branch were filed apart.
The symptom was visible in the numbers and I nearly shipped past it: the genus-2
split families reported 2,462 assignments where one case per branch reported 1,559,
when per-branch scoring should hold that figure FIXED. Every extra "branch" was one
branch counted twice because its cases disagreed about a prefix length, so their
blind sets were never intersected and the second case bought nothing measurable.
Those families looked like they had gained one point where the ramified families
gained ten, and the explanation was the instrument rather than the corpus.
An assignment is now (function, variable, nth occurrence), which is stable under
anything happening before it, and a triple counts invisible only if EVERY case
reaching it is blind to it.
Measured on the same two corpora, before and after the fix:
arb genus-2 split negReduced cases assigns invisible detect
committed, one per branch 77 1559 355 77.2%
two per branch, keyed by index 304 2462 530 78.5%
two per branch, keyed by name 304 1559 277 82.2%
So the corpus was 5 points better than it measured, not 1. The denominator now
holds fixed at 1,559 across both, which is the property that says the instrument is
comparing like with like.
Figures quoted in the two preceding commits for the genus-2 split families
understate their gains for this reason. The ramified figures are unaffected: their
families have no Precompute layer, so no prefix could shift.
…ainable
Two things, both needed before the corpus rule could be called uniform.
ARB NOW CARRIES ITS OWN CASES PLUS ITS SPECIALISATIONS'. `--inherit-from` merges
another family's kept cases into arb's tester, which is sound for a reason worth
stating: arb is valid on every curve nch2 and ch2 are, so their cases are
legitimate arb inputs, and the testers RECOMPUTE the expected result rather than
storing it -- the ramified ones against Magma's Jacobian, the split ones against the
reference library -- so an inherited case re-derives its own answer and a mismatch
would be a real disagreement.
They ADD rather than replace, and that was measured rather than assumed. nch2 only
ever presents h = 0 and ch2 only h monic of degree g, so the union of the two
exercises neither non-monic h nor deg h < g -- and ERRATA E11 is a defect of exactly
that class, `arb_ramifiedG2_DBL`'s DBL4 reading h2^2*upp0 where the derivation gives
h2, invisible on h in {0,1} and wrong on 166 of 3,600 off-domain doublings. Replacing
arb's own cases would have retired the only cases that can see it.
What inheritance actually buys, honestly: arb genus 3 goes 95.8% to 96.2% and arb
genus 2 does not move at all. The gain is not detectability, it is a curve shape --
arb genus 3's own corpus contained NO h = 0 case (deg2 46, deg2 non-monic 87, deg3
57) and now holds 96, and arb must handle h = 0 because an nch2 curve is a valid arb
input. arb genus 2 now spans deg h = 0, 1 and 2, monic and non-monic, plus h = 0.
POSREDUCED IS REGENERABLE FOR THE FIRST TIME. Three new generators,
{arb,nch2,ch2}_splitG2_POS_WB_gen.mag, derived from their negReduced twins by four
substitutions: the formulas loaded, the three _SPLIT_NEG library calls, the basis
polynomial handed to them, and the basis v's top coefficients come from. Generated
by script rather than by hand so the two versions cannot drift and the diff is
reviewable as exactly those four things.
Three files rather than a flag because Magma CANNOT `load` inside a conditional --
tested, not assumed: `User error: bad syntax`. Branching on GetEnv works and
function-valued variables work, so the operations and the basis could have been
selected at run time; the loads could not, and the loads are what bring in the
formulas under test. Magma now passes all three posReduced testers where it failed
all three before.
Also fixed: FileInfo.LOG was not basis-aware, so a posReduced run wrote over the
negReduced run's log. Worse than untidy, because --inherit-from READS those logs: a
negReduced arb could be handed posReduced cases and would compare a different
divisor. Caught by seeing a POS log where a NEG one belonged; both were regenerated.
family cases detectable
arb ram g3 190 -> 382 95.8% -> 96.2%
arb ram g2 88 -> 175 96.5% -> 96.5%
arb split g2 304 -> 606 both bases
nch2 split g2 77 -> 153 both bases
ch2 split g2 77 -> 149 both bases
Corpus 2,607 -> 3,866. Coverage 1,926 -> 1,927 of 1,929: another baseline exemption
died of progress, posReduced nch2's UTL0, the same Precompute leaf a wider corpus
now reaches. Genus-3 split is the only group still at one case per branch.
Gates: whitebox all 3,866 replayed and matched; selftest 19/0/0; driver --strict
13,746/13,746; Magma 30 testers 0 failures 0 skips, its own logs confirming the new
counts for all twelve regenerated families; both path gates; ruff. No formula file
touched.
E21 -- the case emitter could not produce a genus-2 split tester, and had not been able to since PR12. The weight was read from a fixed index, and the two genuses load different reference libraries with different divisor shapes: <u, v, w, n> at genus 2 against <u, v, n> at genus 3, so that index is the weight at one and the COFACTOR at the other. PR12 fixed this defect's mirror image for genus 3 and created this one. Latent because the three deployed testers predate the break and nothing ever asked the emitter for another. The transferable lesson is in the entry: a tool can lose a capability silently for as long as nothing exercises it, and the deployed artefacts being correct says nothing about whether the thing that produced them still works. E22 -- the tool could not target posReduced at all, so three of fifteen testers were unmaintainable by the tool that maintains the other twelve. A --basis flag looks sufficient and is not: it routes the output side and leaves the generator negReduced in four places. Built that way every Python gate passed all three posReduced testers and Magma failed all three on assertions, which is the sharpest instance in this series of the two oracles not being redundant. The single-file alternative is impossible rather than inelegant -- Magma cannot `load` inside a conditional -- and that is recorded with the error it produces so nobody retries it. E20 and N32 now describe twelve of the fifteen families rather than four, carry the arb-inheritance rule and why the inherited cases are additive rather than replacing, and record that coverage ROSE to 1,927 of 1,929 because two baseline exemptions died of progress. N32 also gains a section on the four defects the extension turned up, three of them in tooling and one in the instrument I wrote for this PR -- detect.py was understating the split families by five points by keying assignments on trace position, which breaks as soon as two cases reach a branch through different Precompute exits. The tell was in its own output: the denominator rose with the case count where per-branch scoring should hold it fixed.
Re-measured all twelve regenerated families with the fixed instrument. The genus-2
split numbers in the two earlier commits understate their gains, because those were
taken before detect.py stopped keying assignments on trace position:
family reported actual
arb g2 split neg 78.5% 83.0%
ch2 g2 split neg 82.9% 84.1%
nch2 g2 split neg 85.4% 85.0%
arb g2 split pos -- 69.4% (was 65.0%)
ch2 g2 split pos -- 70.3% (was 67.2%)
nch2 g2 split pos -- 76.1% (was 75.1%)
The before-figures are comparable under either keying, and that is worth saying
rather than assuming: a one-case-per-branch corpus has nothing to intersect, so the
grouping flaw could not bite it. Only the multi-case measurements were wrong, and
they were wrong in the direction that understated the work.
Every one of the twelve families improves. Recorded per family rather than as a
repository total, because the total is 82.5% and is dominated by the three families
NOT yet done -- genus-3 split is 54,431 of the 67,931 scored assignments, 80% of the
whole -- so the headline barely moves until those land while every family that has
been touched moves ten to fourteen points. Quoting the total as this work's result
would understate it by a wide margin.
…stion The scoreboard gained a row and lost two exempt branches. More importantly it gained a paragraph distinguishing the two questions, because they are easy to conflate and this project conflated them for a long time: coverage asks whether every branch is REACHED, and has said yes for ages; detectability asks whether a change to the arithmetic would be NOTICED. A branch can be covered by a case that cannot see a change to the very term the change touches, which is ERRATA E20 -- a correct optimisation reverted because breaking the same line left both oracles green. Figures corrected: branch coverage 1,925 -> 1,927 of 1,929 (two exemptions died of progress), selftest 17 -> 19 sections, and the corpus row was already updated. The new detectability row carries its own caveat inline: 82.5% is dominated by the three genus-3 split families still holding one case per branch, while the twelve regenerated ones sit between 69% and 96.5%. Also states that 100% is neither reachable nor the target, since a guard variable a branch requires to be zero is structurally invisible.
detect.py gets a row explaining what it measures and, as importantly, the two design decisions that make the number meaningful: scored per BRANCH so more cases can never lower a score, and an assignment identified by (function, variable, occurrence) rather than by trace position, which breaks as soon as two cases reach a branch through different Precompute exits. Also that it is a relative instrument -- 100% is unreachable, a guard variable a branch requires to be zero being invisible by construction. Corrected: selftest is nineteen sections not seventeen, the current-state table said 16 of 16 with blocks skipping, and the family count was 14 where discover_families finds 15.
The three genus-3 split families cannot be rebuilt from scratch without LOSING coverage, and the reason is specific rather than a matter of budget. Their deployed testers hold 405 / 404 / 405 cases covering every branch, so 405 labels are reachable; a fresh search at 300 curves over three fields reaches 403, and the three it misses -- ADD011, ADD082, DBL22 -- are each covered by exactly ONE case in the deployed corpus. Even the original long run found them once apiece. Nor can the deployed cases be re-selected: their provenance logs are partial, and rebuilding nch2_splitG3 from its committed log reaches 86 of 405. The tester text is the only surviving record of those cases. So `--merge-tester` appends an existing tester's case blocks verbatim, which is regeneration rather than copying: a tester written by this emitter is a header plus one self-contained block per case -- each setting its own field, curve and divisors, calling the formulas and asserting against the reference -- so the blocks ARE what the emitter would write for them. The result is still produced by one command and still reproducible. THE CONSEQUENCE WORTH HAVING is that a partial generation run is now useful. Any second case found is additive, coverage cannot fall below the deployed corpus, and a run no longer has to reach 405 to be worth keeping. That turns an open-ended job into a bounded one. Measured on nch2 genus-3 split: 405 deployed plus 798 newly selected gives 1,203 cases, all replaying matched, covering 413 labels against the deployed 412. Coverage ROSE, and a second baseline exemption died of progress -- nch2_splitG3_UTL's UTL4, a Precompute leaf the wider corpus now reaches.
…ires 405 deployed cases plus 798 newly selected, giving 1,203 that all replay matched and cover 413 labels against the deployed 412. Coverage ROSE rather than held, which is the property that says merging was the right shape: the deployed cases carry three branches a fresh search reaches only once apiece, and the new ones carry the second case per branch that a search can find. `nch2_splitG3_UTL`'s UTL4 exemption retires with it -- a Precompute leaf whose eight exits fire on as little as 0.88% of curves, which a corpus drawing across three fields now reaches. That leaves exactly ONE exempt branch in the repository, `ch2_splitG3_ADD`'s ADD227, and that one carries a proof rather than a budget excuse. Repository coverage 1,925 of 1,929 at the start of this work, 1,928 now. Corpus 3,866 -> 4,664 cases. Figures re-derived rather than moved, per the standing rule. Gates: whitebox all 4,664 replayed and matched; selftest 19/0/0; driver --strict 13,746/13,746; Magma 30 testers 0 failures 0 skips. No formula file touched. ch2 and arb genus-3 split are still generating; they merge the same way and will land separately.
The narrative said twelve of fifteen families, 3,866 cases and 1,927 of 1,929 branches; nch2 genus-3 split has landed since, so it is thirteen, 4,664 and 1,928 -- and three baseline exemptions have now died of progress rather than two, leaving one in the whole repository. Added its measured row: 405 -> 1,203 cases, 84.7% -> 88.2%. Two claims were reworded rather than renumbered, because they were true when written and are misleading now: "branch coverage is unchanged at 1,925 of 1,929" appeared in both the E20 verification paragraph and N32's acceptance-test paragraph, where the point was that nothing was TRADED for the improvement. That point stands, but coverage did not stay put -- it rose -- so saying "unchanged" now reads as though the later gains had not happened. Figures re-derived by running the tools rather than edited in place, which is the standing rule here and the reason this file has gone stale three times before.
arb and ch2 genus-3 split, merged the same way nch2 was -- a fresh search for the
second case per branch, plus the deployed cases verbatim so nothing is lost. arb
1,979 cases across 413 labels, ch2 1,209 across 412; both replay fully matched.
That completes the corpus rule across every family in the repository:
corpus 1,886 -> 7,043 cases
branch coverage 1,925 -> 1,928 of 1,929
exempt branches 4 -> 1
The one remaining exemption is ch2_splitG3_ADD's ADD227, which carries a proof that
it is unreachable in characteristic 2 rather than a search-budget excuse. Three
exemptions retired during this work, each a Precompute leaf firing on as little as
0.88% of curves that a corpus drawing across several fields now reaches.
MAGMA COSTS 45 SECONDS MORE, which is the number worth checking given the suite was
deliberately cut from ~45 minutes to four earlier in this series. The split genus-3
testers roughly quadrupled and the suite went 4m03s to 4m48s -- the whitebox testers
were never the expensive part, the random ones were.
Gates: Magma 30 testers 0 failures 0 skips; whitebox all 7,043 replayed and matched;
selftest 19/0/0; driver --strict 13,746/13,746; dominance clean on 39 files; ruff and
both path gates. No formula file is touched anywhere in this PR.
Detectability figures for these two are still measuring -- 20,767 and 17,270
assignments, one replay each -- and land in the docs when they finish.
family cases detectable
arb ram g2 22 -> 88 86.1% -> 96.5%
nch2 ram g2 22 -> 44 93.2% -> 94.1%
ch2 ram g2 22 -> 43 87.9% -> 95.7%
arb ram g3 48 -> 382 81.8% -> 96.2%
nch2 ram g3 48 -> 96 80.0% -> 93.3%
ch2 ram g3 48 -> 96 81.4% -> 88.3%
arb split g2 neg 77 -> 606 77.2% -> 83.0%
nch2 split g2 neg 77 -> 153 84.6% -> 85.0%
ch2 split g2 neg 77 -> 149 82.0% -> 84.1%
arb split g2 pos 77 -> 606 65.0% -> 69.4%
nch2 split g2 pos 77 -> 153 75.1% -> 76.1%
ch2 split g2 pos 77 -> 149 67.2% -> 70.3%
arb split g3 405 -> 1,979 80.6% -> 84.3%
nch2 split g3 405 -> 1,203 84.7% -> 88.2%
ch2 split g3 404 -> 1,209 81.9% -> 85.8%
REPOSITORY 1,886 -> 7,043 81.3% -> 85.4%
12,728 invisible assignments of 67,931 down to 9,884. The denominator is IDENTICAL
before and after, and that is the check rather than a coincidence: it is per-branch,
and the branches did not change. A denominator that moved would have meant the
instrument was comparing different things, which is exactly the bug it had earlier in
this branch.
The repository figure moves less than the per-family ones because genus-3 split is
54,431 of those 67,931 assignments -- 80% of the whole -- and those three gain three
to four points where the smaller families gain ten to fourteen. Recorded as a fact
about where the code is rather than explained away: they were already the
best-covered families, and they are three to four points better now.
The before-figures are comparable under either version of the instrument, which is
worth stating rather than assuming: a one-case-per-branch corpus has nothing to
intersect, so the position-keying flaw could not bite it. Only the multi-case
measurements were ever wrong, and they were wrong in the direction that understated
the work.
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.
Closes the second cause of
ERRATA.mdE20: the frozen whitebox corpus was complete — everybranch reached — without being adequate. A branch covered by one case whose arithmetic happens to
zero a term cannot distinguish a change to that term.
That is not hypothetical. It is why a correct
−2M −2Asaving atADD29/ADD33was applied, measuredgreen under real Magma across 2,119 comparisons, and reverted — because breaking the same line
deliberately also measured green.
The finding a reviewer should see first
Every Python gate passed three testers that Magma rejected on assertions.
While extending the corpus to the
posReducedbasis,whitebox.pyreplayed 295 of 295 cases matchedfor
arb_splitG2posReduced, and the Magma suite failed all three posReduced testers. The cause isrecorded as E22: a
--basisflag routes the output side — paths, label counting, the emitter — andleaves the generator negReduced in four places, so it produced negReduced cases that were then
labelled posReduced.
This repository has argued for years that its Python framework and Magma are complementary rather than
redundant, because Magma is licensed and cannot run in CI. This is the sharpest evidence yet: the
framework agreed with itself about a divisor that Magma's own arithmetic rejects.
Three more defects, all latent, all in tooling
E21 — the case emitter could not produce a genus-2 split tester, and had not been able to since
PR12. The weight was read at a fixed index, and the two genuses load different reference libraries
with different divisor shapes:
<u, v, w, n>at genus 2 against<u, v, n>at genus 3. So that indexis the weight at one and the cofactor at the other, and a generated case read
N2 := x + FF.1^2—a polynomial where an integer weight belongs. PR12 fixed this defect's mirror image for genus 3 and
created this one. Nothing shipped wrong; the deployed testers predate the break. What was lost was the
ability to regenerate them, which is what PR12 existed to restore.
A tool can lose a capability silently for as long as nothing exercises it, and "the deployed artefacts
are correct" says nothing about whether the thing that produces them still works.
E22 — the tool could not target
posReducedat all, so three of fifteen testers were unmaintainableby the tool maintaining the other twelve. Fixed with three generated POS generators. Three files rather
than a flag because Magma cannot
loadinside a conditional — tested, not assumed:User error: bad syntax.And a flaw in the new instrument itself.
detect.pykeyed each assignment by its position in theexecution trace;
Precomputehas eight exits taking different numbers of assignments, so two casesreaching one branch by different curve routes had every later index shifted and their blind sets were
never intersected. The tell was in its own output and nearly went past me: the denominator rose with
the case count, where per-branch scoring must hold it fixed. It was understating the split families by
five points.
What the corpus rule now is
Two cases per branch per characteristic class, from different fields.
arbadditionally carriesits specialisations' cases.
Each clause is measured, not chosen:
at GF(5) at 9.7% — because same-field failures are correlated. A cross-field pair reaches 7.1%.
costing twenty minutes against seconds. An earlier "prefer the largest field" rule was reverted:
it picked {9,11} from {3,5,7,9,11} and turned an improvement into a regression, 16 invisible becoming
24.
per-family table, and it exposed that
arb's genus-3 corpus was 45 characteristic-2 cases against 3odd ones.
arb's inherited cases add rather than replace, because nch2 only presentsh = 0and ch2 onlyhmonic of degreeg, so between them they never exercise the non-monic or low-degreehthatE11 is a defect of. Replacing would have retired the only cases that can see it.
Results
The denominator is identical before and after, 67,931 either way — and that is the check rather than
a coincidence. It is per-branch, and the branches did not change. A denominator that moved would have
meant the instrument was comparing different things, which is exactly the bug it had midway through
this branch.
Coverage rose, 1,925 → 1,928 of 1,929. Three baseline exemptions died of progress — each a
Precomputeleaf firing on as little as 0.88% of curves, which a corpus drawing across several fieldsnow reaches. One exemption remains in the whole repository,
ch2_splitG3_ADD'sADD227, and itcarries a proof of unreachability in characteristic 2 rather than a search-budget excuse.
The acceptance test
E20's own mutation — drop
t8fromADD33'sC0— applied to the live formula file:The file was restored and the corpus verified green.
verification/detect.pylands as a committedgate, with a
selftestsection holding it to both its claims: faithful, since it copiesmaginterp.runrather than wrapping it and must reproduce the real interpreter exactly when nothing isperturbed; and sensitive, since an all-zero or all-invisible answer would mean the perturbation never
lands or the comparison never fires.
Genus-3 split is merged, not regenerated
Those three families cannot be rebuilt from scratch without losing coverage. A fresh search reaches 403
of 405 branches, and the three it misses are each covered by exactly one case in the deployed
corpus — even the original long run found them once apiece. Their provenance logs cannot be
re-selected from either: rebuilding
nch2_splitG3from its committed log reaches 86 of 405.So
--merge-testerappends an existing tester's case blocks verbatim, which is regeneration ratherthan copying — a tester written by this emitter is a header plus one self-contained block per case, so
the blocks are what the emitter would write for them. The useful consequence is that a partial run
now pays: any second case found is additive and coverage cannot fall.
Honest limits
ADD29/ADD33refusal and notits resolution, so this work's plan claimed it would recover the saving. It had already been
recovered inside PR7+8 once the exhaustive probe gave it an oracle. The errata entry was the reliable
record where my summary was not. The case here is detectability alone.
f7is assigned and never read andis deliberately not deletable; a branch guarded on
d = 0must haved = 0to be reached; theadjugate entries are dead on the degenerate paths that never consume them. Measured, those are
exactly the names that survive every field.
67,931 scored assignments and those three gain three to four points where smaller families gain ten
to fourteen. They were already the best-covered families.
Verification
Magma 30 testers, 0 failures, 0 skips — and 4m03s → 4m48s on a 3.7× corpus, which is the figure
worth checking given this suite was deliberately cut from ~45 minutes earlier in the series; the
whitebox testers were never the expensive part.
whiteboxall 7,043 replayed and matched ·selftest19/0/0 ·driver --strict13,746/13,746 ·dominanceclean on 39 files ·opcountbyte-identical across all fifteen families · both path gates · ruff.
No formula file is touched anywhere in this PR.