From d719fb3a1db0707b169a25ab450d70c3ec087c32 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Mon, 24 Aug 2026 17:33:28 +0700 Subject: [PATCH] gft self-check: fourteen more plants raise the assert column 2/34 -> 16/34 (Refs #2161) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The column was the number of planted faults, not a verdict on 32 assertions (§123). The model was tested by predicting before measuring: 2 plants -> 2/34, +7 -> 9/34, +7 more -> 16/34. Three for three. Cost was never the obstacle and nobody had checked. Each new plant fires in the arithmetic block at the top of `__main__`, before any training: 0.06s apiece. The control went 11.8s -> 12.5s for eight times the coverage. The old assumption that more plants meant more whole-program runs was generalised from a sample of two, both of which are full runs. Within a family the fault has to be surgical -- adjacent assertions test adjacent cases, so the obvious fault breaks them all and only the first is seen. `elif t == hf and (s & 1)` -> `... and False` kills the ODD tie only, leaving the even one true so it passes and the odd one speaks. One resisted and is left alone: disabling `_magsub`'s `if rem > half` also breaks the renormalisation-carry case, which is checked earlier, so the plant fires that instead. Separating them would mean encoding the exact remainders, and then the control is a second copy of the subject. Also: `spawned()` now asserts the plant edited the SUBJECT. All subject code sits above the control and every assertion under test below it, so the first changed byte must precede `def self_check(`. T124 caught a plant that edited the control's own source; T211 one that edited the assertion checking the result. Both went green. Neither was caught by reading; both would have been caught by this line. --- .claude/skills/ci-gates/SKILL.md | 82 +++++++++++++ ...g-a-ceiling-you-have-finally-understood.md | 10 ++ tools/gft_backprop_microcode.py | 111 ++++++++++++++++++ 3 files changed, 203 insertions(+) create mode 100644 docs/now/2026-08-24-raising-a-ceiling-you-have-finally-understood.md diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index ccc0e5c8c2..8ba89497e3 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -4963,3 +4963,85 @@ output distinguished the two readings. **When a score is stuck at a small integer, count the things that can produce a kill before you look at the things being killed.** + +## 124. Raising a ceiling you have finally understood + +§123 established that `--assert`'s 2 of 34 was the *number of planted faults*, +not a verdict on 32 assertions. This tick tested that model the only way a model +can be tested: **predict the number before measuring it.** + +| plants | predicted | measured | +|---|---|---| +| 2 | 2 | 2/34 | +| +7 | 9 | **9/34** | +| +7 more | 16 | **16/34** | + +Three for three. A model that survives being used to predict is worth more than +one that survives being argued for. + +### Cost was never the obstacle, and nobody had checked + +Each new plant fires in the arithmetic block at the top of `__main__`, long +before any training runs: **0.06s apiece**. The whole control went 11.8s → 12.5s +for **eight times** the coverage. + +Three iterations deferred this column partly on an unexamined assumption that +more plants meant more whole-program runs. The two existing plants *are* +full runs, so the assumption generalised from a sample of two. **A cost you have +not measured is a reason you have not checked.** + +### Within a family, the fault has to be surgical + +Adjacent assertions test adjacent cases of the same code, so the obvious fault +breaks them all and only the first is ever seen. To surface the second member, +the fault must falsify it while leaving the first **true**: + +```python +elif t == hf and (s & 1): mant += 1 # clean +elif t == hf and (s & 1) and False: ... # kills the ODD tie only +``` + +The even tie still correctly declines to round up, passes, and lets the odd one +speak. Seven of eight designed this way hit their target exactly. + +### The eighth is the lesson arriving inside the lesson + +Disabling `_magsub`'s `if rem > half` to surface *"strictly above half"* also +breaks the renormalisation-carry case — which is checked **earlier**. The plant +fires that one instead. + +It is left alone on purpose. A plant narrow enough to separate them would have +to encode the exact remainders, and then **the control becomes a second copy of +the thing it checks**, which fails for its own reasons and agrees with the +subject about all of them. + +### The guard that mechanises two earlier lessons + +T124 caught a plant whose needle's first occurrence was the control's own +source. T211 caught one whose needle's only occurrence was the **assertion** +checking the result. Both went green; both had names that were lies. + +Every piece of subject code in that file sits **above** the control, and every +assertion under test sits **below** it. So one comparison decides it: + +```python +cut = first byte where the plant's output differs from the input +assert cut < src.index("def self_check(") +``` + +Positive control: a plant that edits an assertion's text is now refused with +*"the plant edited the control or an assertion (byte 28218), not the subject +(which ends at 20179)"*. **Neither of the two earlier cases was caught by +reading; both would have been caught by this line.** + +### A smaller one worth keeping + +Listing the file's assertions with a throwaway `line.strip().startswith("assert ")` +scored **prose inside the control's docstring** as an assertion — the exact bug +fixed in `assert_sites` one tick earlier. The tool had learned; my one-off script +had not. + +**A fix that lives only in the tool does not protect the scratch commands you +reach for while using it**, and those are where a wrong list quietly becomes a +wrong plan. The tell was the classification coming out nonsensical — zero +training assertions in a file that is mostly training assertions. diff --git a/docs/now/2026-08-24-raising-a-ceiling-you-have-finally-understood.md b/docs/now/2026-08-24-raising-a-ceiling-you-have-finally-understood.md new file mode 100644 index 0000000000..293295a374 --- /dev/null +++ b/docs/now/2026-08-24-raising-a-ceiling-you-have-finally-understood.md @@ -0,0 +1,10 @@ +# NOW -- Raising a ceiling you have finally understood (2026-08-24) + +## Raising a ceiling you have finally understood (Refs #2161) + +- Refs #2161. The assert column was 2 of 34 because the control planted two faults, not because 32 assertions were weak. This tick tested that model the only way a model can be tested -- by predicting the number before measuring it. 2 plants predicted 2, measured 2/34. Plus seven predicted 9, measured 9/34. Plus seven more predicted 16, measured 16/34. Three for three +- Cost was never the obstacle and nobody had checked. Each new plant fires in the arithmetic block at the top of __main__, long before any training: 0.06 s apiece. The whole control went 11.8 s to 12.5 s for EIGHT TIMES the coverage. Three iterations deferred this partly on an unexamined assumption that more plants meant more whole-program runs -- generalised from a sample of two, both of which happen to be full runs. A cost you have not measured is a reason you have not checked +- Within a family the fault has to be SURGICAL: adjacent assertions test adjacent cases of the same code, so the obvious fault breaks them all and only the first is seen. `elif t == hf and (s & 1): mant += 1` becomes `... and False`, which kills the ODD tie only -- the even tie still correctly declines to round up, passes, and lets the odd one speak. Seven of eight hit their target exactly +- The eighth is the lesson arriving inside the lesson. Disabling _magsub `if rem > half` to surface "strictly above half" also breaks the renormalisation-carry case, which is checked EARLIER, so the plant fires that one instead. Left alone on purpose: a plant narrow enough to separate them would encode the exact remainders, and then the control becomes a second copy of the thing it checks +- New guard mechanises two earlier lessons. T124 caught a plant whose needle first occurrence was the control own source; T211 caught one whose needle ONLY occurrence was the assertion checking the result. Both went green with names that were lies. All subject code sits above the control and every assertion under test below it, so one comparison decides it: the first byte the plant changed must come before `def self_check(`. Positive control: a plant editing an assertion text is now refused by byte offset. Neither earlier case was caught by reading; both would have been caught by this line +- Smaller one worth keeping: listing the file assertions with a throwaway startswith("assert ") scored PROSE inside the control docstring as an assertion -- the exact bug fixed in assert_sites one tick earlier. The tool had learned; my one-off script had not. A fix that lives only in the tool does not protect the scratch commands you reach for while using it. The tell was the classification coming out nonsensical: zero training assertions in a file that is mostly training assertions diff --git a/tools/gft_backprop_microcode.py b/tools/gft_backprop_microcode.py index 775a70c505..653ad521e8 100644 --- a/tools/gft_backprop_microcode.py +++ b/tools/gft_backprop_microcode.py @@ -408,6 +408,30 @@ def spawned(label, edit, want_rc, expect, absent): before = src src = edit(src) assert src != before, f"{label}: the plant changed nothing" + # T212: and it must have changed the SUBJECT. Twice now a plant + # has passed while editing something else -- once this control's + # own source (T124), once the assertion that checks the result + # (T211, where the literal it targeted existed nowhere but + # inside that assertion). Both times the case went green and + # both times its name was a lie. + # + # Every piece of subject code in this file -- enc, the _mag* + # arithmetic, gen, emit_verilog -- sits ABOVE this function, and + # every assertion under test sits BELOW it in `__main__`. So one + # comparison decides it: the first byte the plant changed must + # come before this function starts. + # + # This is the check that would have caught both, and neither was + # caught by reading. + cut = next((i for i, (a, b) in enumerate(zip(before, src)) if a != b), + min(len(before), len(src))) + guard = before.index("def self_ch" + "eck(") + assert cut < guard, ( + f"{label}: the plant edited the control or an assertion " + f"(byte {cut}), not the subject (which ends at {guard}). " + f"A plant that edits the check proves only that corrupting " + f"a check makes it fail." + ) me = os.path.join(tools, os.path.basename(__file__)) open(me, "w", encoding="utf-8").write(src) r = subprocess.run([sys.executable, me], capture_output=True, text=True) @@ -479,6 +503,93 @@ def spawned(label, edit, want_rc, expect, absent): 1, ["AssertionError"], ["emit_verilog: clk_div=16"]) + # T212: RAISING THE CEILING. The assert operator scored 2 of 34 for three + # iterations, read each time as a verdict on 32 weak assertions. It was + # nothing of the kind: this control planted exactly TWO faults, and Python + # stops at the first failing assert, so each plant can surface exactly one + # assertion. Two plants, two kills -- the number was arithmetic on the + # length of this list. + # + # So the list grows. One plant per ASSERTION, not per family: a plant that + # falsifies a whole family still surfaces only its first member. Measured: + # plant a sign flip in smul and the program dies at the XOR assertion, and + # the held-out assertion it ALSO falsifies stays invisible until the first + # one is neutered. + # + # These cost nothing. Each fires in the arithmetic block at the top of + # `__main__`, long before any training runs: 0.06s apiece against 11.8s for + # the three whole-program cases below. + spawned("enc: the smallest normal binade is not zero", + lambda s: s.replace(" if off < 0: return 0", + " if off <= 0: return 0", 1), + 1, ["smallest normal binade must not encode as zero"], []) + spawned("enc: the sign bit survives", + lambda s: s.replace(" s = 1 if x < 0 else 0;", " s = 0;", 1), + 1, ["sign survives the smallest binade"], []) + spawned("enc: below the smallest binade is zero", + lambda s: s.replace(" if off < 0: return 0", + " if off < -1: return 0", 1), + 1, ["below the smallest binade IS zero"], []) + spawned("add: round-half-to-EVEN, not half-to-odd", + lambda s: s.replace(" elif t == hf and (s & 1): mant += 1", + " elif t == hf and not (s & 1): mant += 1", 1), + 1, ["tie with even s must NOT round up"], []) + spawned("mul: round-half-to-EVEN, not half-to-odd", + lambda s: s.replace(" elif r == half and (q & 1): mant += 1", + " elif r == half and not (q & 1): mant += 1", 1), + 1, ["mul: tie, even q, no carry"], []) + spawned("enc: renormalisation carries into the exponent", + lambda s: s.replace(" if m >= 512: m = 0; off += 1", + " if m > 512: m = 0; off += 1", 1), + 1, ["mantissa rounding to 512 must carry"], []) + spawned("sub: round-half-to-EVEN, not half-to-odd", + lambda s: s.replace(" elif q & 1: mant += 1", + " elif not (q & 1): mant += 1", 1), + 1, ["sub: tie, odd q"], []) + + # Seven more, and these had to be SURGICAL. Within one family the + # assertions test adjacent cases of the same code, so the obvious fault + # breaks all of them and only the first is ever seen. To surface the second + # member, the fault must falsify it while leaving the first true: + # + # `elif t == hf and (s & 1)` -> `... and False` kills the ODD tie only; + # the even tie still correctly declines to round up, so it passes and the + # odd one speaks. + # + # One resisted and is left alone deliberately. Disabling `_magsub`'s + # `if rem > half` to surface "strictly above half" also breaks the + # renormalisation-carry case, which is checked EARLIER -- so the plant fires + # that one instead. That is the shadowing this whole list is about, arriving + # in the list itself; a plant narrow enough to separate them would have to + # encode the exact remainders, which makes the control a second copy of the + # thing it checks. + spawned("sub: the sticky guard is not decoration", + lambda s: s.replace("if (ls - (la << d)) > 0: sticky = 1", + "if (ls - (la << d)) >= 0: sticky = 1", 1), + 1, ["a tie was reached with bits discarded"], []) + spawned("add: the ODD tie rounds up (the even one is a different case)", + lambda s: s.replace(" elif t == hf and (s & 1): mant += 1", + " elif t == hf and (s & 1) and False: mant += 1", 1), + 1, ["tie with odd s must round up"], []) + spawned("add: strictly above half is not a tie", + lambda s: s.replace(" if t > hf: mant += 1", " if False: mant += 1", 1), + 1, ["strictly above half must round up"], []) + spawned("mul: the ODD tie rounds to even", + lambda s: s.replace(" elif r == half and (q & 1): mant += 1", + " elif r == half and (q & 1) and False: mant += 1", 1), + 1, ["mul: tie, odd q, no carry"], []) + spawned("mul: the carry path has its own half", + lambda s: s.replace("if carry: q = prod >> 10; r = prod & 1023; half = 512", + "if carry: q = prod >> 10; r = prod & 1023; half = 511", 1), + 1, ["mul: tie, even q, carry"], []) + spawned("mul: renormalisation carries into the exponent", + lambda s: s.replace(" if mant >= 512: mant = 0; oo = min(oo + 1, 80)", + " if mant > 512: mant = 0; oo = min(oo + 1, 80)", 1), + 1, ["mul: mant == 512 must carry"], []) + spawned("sub: the EVEN tie does not round up", + lambda s: s.replace(" if rem > half: mant += 1", " if rem >= half: mant += 1", 1), + 1, ["sub: tie, even q -- must NOT round up"], []) + print(f" self-check: the training verdict and an emitter verdict both go red, " f"and a clean tree stays green = {ok}") return 0 if ok else 1