gates: three scanner defects, and the assert column measures the control (Refs #2161)

[gHashTag]

A five-way fan-out audit raised 19 findings; 11 survived adversarial refutation, 8 were killed. This lands the ones that are mine to fix.

The headline is not a fix — it is what a number turned out to mean

--assert scores 2 of 34, the worst of the five operators, deferred three iterations as "the column to fix".

It is not a column about assertions. It is arithmetic on the number of planted faults.

self_check() spawns three whole-program runs: one clean, two with a fault planted. A neutered assertion changes nothing on the clean run, so it can only be noticed on a run where that assertion would have fired — and only if it fires first, because Python stops there.

Measured, one variable at a time:

• plant 1 falsifies both line 632 and line 660;
• the program dies at 632, so neutering 660 alone is invisible;
• neuter 632 and the same plant now dies at 660.

One kill per plant. The kill set is exactly {632, 668} — precisely the two lines missing from the survivor list. All 34 sites do execute on a clean run, so no survivor is unreachable; they are invisible, not dead. Iterating on the operator cannot move the number — only adding a spawned() case per assertion can.

My published explanation was wrong for at least 26 of the 32. The earlier NOW entry accounts for the six held-out-threshold assertions and offers a boundary rationale for the whole column. A partial explanation presented as a complete one is the most expensive kind of wrong: it closes the question, and three iterations then deferred the column as understood rather than unexplained.

The control's second plant did not test what it says

The case is "a renamed port is caught by the emitter check". input [31:0] x0i spelled out occurs exactly once in the file — at the assertion checking for it — because the emitter builds ports as f"input [31:0] x{k}i".

So the plant's str.replace rewrote the assertion's own expected string; the emitted Verilog was untouched, and the assertion failed for a reason unrelated to the emitter.

T124 fixed the case where a needle's first occurrence was the control's own source. This is the next one along: the needle's only occurrence is the subject's check rather than the subject. It now targets the emitter's format string, whose first occurrence is above the control. Verified: the plant edits line 336, the assertion at 668 is untouched, and the control still passes.

Three scanner defects, each with a test that fails without its fix

defect	measured
the three line-oriented site finders had no string state, so a flush-left line inside a control docstring cleared in_control	two files differing by four spaces of indentation on one docstring line: 3 assert sites vs 0, every extra site inside the control
the same blindness scored word-wrapped prose beginning assert as an assertion	assert anything. in a module docstring became a site
assert_sites advanced one byte on a backslash instead of two	assert s == "a\",b", "msg" → mutant assert True,b", "msg", which does not parse → python exits 1 → site scored KILLED

The third is the dangerous one: a false green in the exact column this command exists to make trustworthy. boundary_sites, byte-oriented, had i += 2 all along.

Neutering a control makes it pass, so a site inside one is recorded as a survivor nobody can ever kill — which is what leaves_function's own doc comment warns is the worst outcome: breaking the instrument instead of the thing being measured.

Three of my own numbers were stale

where	said	truth
skill, k/31 boundary denominators	31 sites	62 — the scanner stopped at def self_check(). Killed count unchanged at 14; errata added
tri pointers docstring	"193 mentions and 16 unresolved"	the tool printed 191 and 12 within a day
--boundary help text	"the worst kill rate of the five (26 of 77 across the tree)"	denominator doubled by this same fix

The frozen counts are removed, not updated. A number in help text has no way to learn it went stale, and the pointers docstring had reached the point where running the file refuted its own documentation — the failure the tool exists to find, one level up.

Filed rather than fixed

• PRL draft outline claims zero admitted lemmas; proofs/ contains 32, and the cited audit trail never existed #2685 — docs/reports/PRL_DRAFT_OUTLINE.md (a live manuscript outline) claims "Zero admitted lemmas (audited W211 — see docs/COQ_STATUS.md)". proofs/ contains 32 Admitted., and that audit trail has no commit in the whole history. Changing a physics paper's factual claims is the author's call.
• Gate Topology audits 15 of 45 workflows and misses two live violators; coq-proofs.yml has never been green in 50 runs #2686 — Gate Topology has run 433 times, never red, and audits 15 of 45 workflows; the two that today carry the exact filter it forbids are in neither its covered nor its excluded list. And coq-proofs.yml is 0 successes in 50 runs, still wired to push and pull_request.

Also: external/README.md and external/OWNERS.md pointed at a canon path that moved. tri pointers dead count 12 → 10.

§123 and errata in §§ earlier. 206 tests pass.

Refs #2161

[github-actions]

PR Dashboard

Generated at: 2026-08-24 08:49:38 UTC

• gates: three scanner defects, and the assert column measures the control (Refs #2161) #2687 gates: three scanner defects, and the assert column measures the control (Refs #2161) | Created: 2026-08-24 | Updated: 2026-08-24 | 18 failing / 25 total
• Unbreak FPGA CI and correct two unbacked hardware claims #2081 Unbreak FPGA CI and correct two unbacked hardware claims | Created: 2026-08-11 | Updated: 2026-08-20 | 5 failing / 27 total

Summary

Status	Count
Total Open PRs	2
PRs with Failing Checks	1
PRs with All Checks Green	1
READY	0
FAILING	1
PENDING	0

Seal Status

• ⚠️ STALE -- sha256(compiler.rs)=e6333575ec10 != manifest seal=87e5cbd3ad94.
  The committed NMSE numbers were certified against an older compiler.rs.
  Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

[github-actions]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.