File the silent duplicate-definition binding, and enrol the wall we do not have as an expected red

[gunbai-bot]

What this files

Two definitions of one name in one module are accepted by the source → .dag acceptance path with zero diagnostics, and the second one silently binds.

This is below floor, not a rung that slipped. DESIGN §4b places silent wrongness outside the ladder rather than on its bottom rung, and a name binding to two definitions with no refusal is exactly that.

Three legs of evidence

1 — Mechanism, on a controlled fixture, measured in both directions. A single module carrying fn which_one() -> Bool { false } then fn which_one() -> Bool { true } compiles clean and answers true; swap the two bodies and the same module compiles clean and answers false. Zero diagnostics at either ordering. The direction test is what makes this a binding fact rather than a coincidence — the answer tracks source order, so the last definition wins.

2 — A confirmed production victim. #9081 commit 29088e133 landed dag/gunbc/fabric_cell_converge.dag with two definitions each of fabric_cell_ids and fabric_cell_population_unobserved. Compile clean, witness rows green, and the copy that executed was the second — a §3 single-authority violation running in production, found by a reviewer reading the file and by nothing else. That reviewer's inference was that it "will fail to parse or typecheck"; the inference was wrong, and that is part of the finding: the defect defeats the expectation a reader brings to it.

3 — A live instance on main. dag/test/claim/scm_commit_closure_json_v2_witness_test.dag defines scm_image_refused at two positions with byte-identical bodies and eight call sites. Benign today only because the two bodies agree — luck, not structure.

Census caveat. The live-instance search was a line-anchored regex over module text at main. It is a lower bound, not a closed census: it cannot see definitions differing in spacing or joined by a formatter, and it says nothing about type/data.

The boundary measured, and what was not

Measured: source → .dag acceptance, through our own binary, single module, fn declarations.

Not measured: the Rust emission path, type/data declarations, cross-module collisions, and whether a test fn collides with a plain fn of the same name. Each is its own row when someone measures it; none is claimed here — §4b's rule is that a class's rung is the minimum across its in-scope paths, and citing an unmeasured path is inflation.

The fix is a wall, not a ratchet

Membership is decidable at ingestion, where the module's own declarations are already being folded: two declarations sharing one name in one module is a property of one module's source — no corpus walk, no name resolution, no type information. §5's decidability test is met, so a lens counting occurrences would be validation standing exactly where construction was available.

The probe, and why it is enrolled as an expected red

dag/test/claim/duplicate_definition_binding_probe.dag asserts the correct behaviour — the compiler refuses the two-definition module — so it is RED today and is enrolled in v2.workflow.floor_expected_red floor_expected_red_chunk_19. Written the other way round ("assert the second definition binds") it would go green today and become a defender of the defect, cited forever after as coverage of a wall that does not exist.

Its positive control (single_definition_module_is_clean, the same module with one definition) is not enrolled and passes. That pair is what establishes the census reached its subject and answered rather than failing to run — a CensusNotRunnable maps to -1, which reds both rows and greens neither.

Measured locally at head, one row at a time:

FAIL duplicate_definition_in_one_module_is_refused
PASS single_definition_module_is_clean

When the wall lands the red flips green of its own accord, comes off the roster, and converts to a permanent regression control per §4b meta-obligation (4) — it does not retire.

On my own verification claim, recorded rather than tidied

My previous comment said "Compile: 0 blocking diagnostics." That check was not skipped and did not predate the duplicating edit — it ran on exactly this tree, after every edit, and it passed. The full compile of head 29088e133 reported zero blocking errors and 880 advisories, and grepping that log for duplicate|redefin|already defined|shadow returns nothing. So the quotation was true and worthless as evidence: I cited the compiler's silence as support for a property the compiler does not check. That is the same mistake this PR's own annotations describe — a judgment total at the level examined and blind one level below — and I would rather record it that way than in the tidier version.

— sent from silent-bear-842

[gunbai-bot]

Correction pushed, and it removes the one thing review 55326 singled out for praise. The enrolment in floor_expected_red_chunk_19 is gone, because it asserted something that is not true.

What I got wrong. I justified leaving live_tree_disposition undeclared by pointing at dag/test/claim/qualified_pattern_head_witness_test.dag — same census builtin, no declaration, therefore (I said) it routes and passes. Both halves of that fail:

• Undeclared is ReadsLiveTree by the fail-closed default, not the absence of a live read. v1_compiler.cli_run parse_entry_live_tree_disposition returns live when no row is found, and run_required_floor routes reads_live_tree sites to DeclinedLiveTree — discovered, counted, never run. So my probe was declined, and so is the sibling.
• I never measured the sibling passing. I observed that it is absent from the expected-red roster and inferred execution from that. A population fit is not mechanism confirmation, and absence from a roster of known reds is equally consistent with never running at all.

So the enrolled row would have been inert: enrolling asserts that a row reaches its subject and answers, and a declined row answers nothing. That is a false assertion wearing the shape of coverage — the exact failure this PR exists to name, committed by the PR itself.

What is now in the diff. The module declares ReadsLiveTree honestly (the census resolves its synthetic source against build_module_path_index_from_witness_roots, which walks the live tree — the read is real). It is not enrolled anywhere. The module header and row 33 both state that it does not execute in the required floor today, and both carry an execution trigger kept distinct from the next-rung trigger:

• execution trigger — deletion of the DeclinedLiveTree arm, which v2.workflow.required_floor already carries as retained and staged for deletion at the root. When that lands, the row executes, reds, and belongs on the roster the same day.
• next-rung trigger — the ingestion wall itself. When that lands the row flips green and converts to a permanent regression control per §4b(4).

This makes the probe one more member of item 28's existing population (the guarantee-probe corpus, discovered and declined), not a new condition.

Unchanged and re-measured at the new head, one row at a time:

FAIL duplicate_definition_in_one_module_is_refused
PASS single_definition_module_is_clean

The declaration changed only the routing, not the answers — and the pair still rules out CensusNotRunnable, which maps to -1 and reds both.

— sent from silent-bear-842

[gunbai-bot]

One more thing on record, because it is worth more than the fix.

Review 55326 approved the enrolled version and specifically named the enrolment as a thing it liked. So an approving review endorsed a row that could not execute.

That is not a reviewer failure. It is structural, and it is the same distinction this PR's subject turns on: an approval means no blocking defect was found, never that the change does what it claims. A reviewer reads the diff. Whether a row lands in the executed population is a property of the floor's routing — reads_live_tree → DeclinedLiveTree, decided in run_required_floor — which is not in the diff at all and cannot be read from it. The diff said "enrolled"; the tree said "declined"; nothing in the review's field of view could put those two facts side by side.

The general form, which is what I would want the next person to take from this: absence from a roster of known reds is not evidence of execution. It is equally consistent with never running. Two different states, one silence — and I read the silence the way I wanted to read it.

Also recorded so it is not re-derived: the inverse repair was available and is worse. Relabelling this module SubstrateInputsOnly would have forced it into the executed population, and it would have been a lie to affected-set selection, which is the fact that declaration actually owns. dag/test/claim/compile_diagnostic_census_witness_test.dag census_live_tree_note already records one such mis-declaration found and corrected. Declaring what the module reads and stating that it therefore does not execute is the honest shape, even though it leaves the row quieter.

— sent from silent-bear-842