Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
89 changes: 89 additions & 0 deletions dag/test/claim/duplicate_definition_binding_probe.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
module test.claim.duplicate_definition_binding_probe

import gunbc.compile_diagnostic_census {
CompileDiagnosticCensus,
CensusObserved,
CensusNotRunnable,
census_blocking_rows,
census_total_count
}
import std.types { String, Bool, Int }
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

// WHAT THIS PROBE MEASURES, and why its RED is the point rather than a defect in the probe.
// A module that defines one name TWICE is accepted by the source -> .dag acceptance path with
// ZERO diagnostics, and the SECOND definition silently wins. Measured on a controlled fixture
// in both directions: with `fn which_one() -> Bool { false }` first and `{ true }` second the
// program answers true; with the order swapped it answers false. Nothing is reported at either
// ordering. That is not a rung that slipped -- it is BELOW FLOOR (DESIGN section 4b): a name
// binding to two definitions with no refusal is silent wrongness, which is outside the ladder,
// not a weak rung on it.
//
// THIS ROW DOES NOT EXECUTE IN THE REQUIRED FLOOR TODAY, AND THAT IS DECLARED HERE RATHER THAN
// LEFT TO BE DISCOVERED. `compile_dag_diagnostic_census` resolves the synthetic source against
// `build_module_path_index_from_witness_roots`, which walks the live tree, so the read is real and
// the declaration below is `ReadsLiveTree`. `v1_compiler.cli_run` `run_required_floor` routes every
// such site to `DeclinedLiveTree` -- discovered, counted, never run -- so this row is not enrolled
// in `v2.workflow.floor_expected_red`: enrolling asserts that a row REACHES ITS SUBJECT AND
// ANSWERS, and a declined row answers nothing. An enrolment here would have been a false assertion
// wearing the shape of coverage, which is the exact failure this row exists to name.
// EXECUTION TRIGGER: the deletion of the `DeclinedLiveTree` arm, which
// `v2.workflow.required_floor` already carries as retained and staged for deletion at the root.
// When that lands this row executes, reds, and belongs on the expected-red roster the same day.
// An earlier revision of this module WAS enrolled, justified by a sibling census probe that
// declares no disposition and was inferred to route and pass. That inference was wrong twice over:
// undeclared is `ReadsLiveTree` by the fail-closed default (`cli_run`
// `parse_entry_live_tree_disposition`), so the sibling is declined too, and its passing was never
// measured -- a population fit standing where mechanism confirmation was required.
//
// THE ASSERTION HERE IS THE CORRECT BEHAVIOUR, NOT THE OBSERVED ONE. Written the other way --
// "assert the second definition binds" -- the row would go GREEN today and become a DEFENDER OF
// THE DEFECT, cited forever after as coverage of a wall that does not exist. So the row asserts
// that the compiler REFUSES a module carrying two definitions of one name, is enrolled as an
// expected red with the wrong answer recorded above as the observed state, and flips to green of
// its own accord when the wall lands. Per DESIGN section 4b meta-obligation (4) it does not
// retire at that point: it converts to a permanent regression control.
//
// 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, needing no corpus walk, no resolution and no type
// information. DESIGN section 5's decidability test is met, so a lens counting occurrences would
// be validation standing where construction was available.
//
// THE BOUNDARY THIS ROW MEASURES, stated so no receipt reads coverage it does not have
// (DESIGN section 4b: a class's rung is the MINIMUM across its in-scope paths): source -> .dag
// acceptance, through our own binary, single module, function declarations. NOT measured here:
// 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 by this one.

fn census_of(source: String) -> CompileDiagnosticCensus {
compile_dag_diagnostic_census(source)
}

// -1 on CensusNotRunnable, so could-not-measure REDS both rows below and greens neither
// (DESIGN section 5: bottom-as-answer must never be readable as bottom-as-ignorance).
fn blocking_count(source: String) -> Int {
match census_of(source: source) {
CensusObserved { rows: rows } => census_total_count(rows: census_blocking_rows(rows: rows))
CensusNotRunnable { cause: _ } => 0 - 1
}
}

// The discriminating RED: two definitions of one name, differing in body so that which one
// binds is observable rather than benign.
data duplicate_definition_source: String = "module probe_duplicate_definition\nimport std.types { Bool }\nfn which_one() -> Bool { false }\nfn which_one() -> Bool { true }\n"

test fn duplicate_definition_in_one_module_is_refused() -> Bool {
blocking_count(source: duplicate_definition_source) >= 1
}

// The positive control: the same module with ONE definition must stay at zero blocking
// diagnostics, so the row above cannot pass by the probe source being broken in some other way.
data single_definition_source: String = "module probe_single_definition\nimport std.types { Bool }\nfn which_one() -> Bool { true }\n"

test fn single_definition_module_is_clean() -> Bool {
blocking_count(source: single_definition_source) == 0
}
74 changes: 74 additions & 0 deletions docs/plans/compiler-guarantee-recovery-gap-analysis.md
Original file line number Diff line number Diff line change
Expand Up @@ -3302,6 +3302,80 @@ enforces end to end.
transport expressions newly RESOLVED by this cut. One monolithic diff would make every red
ambiguous between them, which is a poor shape for a change whose entire subject is ambiguity.

33. **Two definitions of ONE NAME in ONE MODULE are accepted with zero diagnostics, and the
SECOND silently wins.** BELOW FLOOR, not a rung that slipped: a name binding to two
definitions with no refusal is silent wrongness, which DESIGN §4b places outside the ladder
rather than on its bottom rung.

**Mechanism, confirmed by execution on a controlled fixture, in both directions.** A single
`.dag` module carrying `fn which_one() -> Bool { false }` followed by
`fn which_one() -> Bool { true }` compiles clean and answers `true`; with the two bodies
swapped, the same module compiles clean and answers `false`. Zero diagnostics at either
ordering — no error, no warning, no advisory. The direction test is what makes this a
binding fact rather than a coincidence: the answer tracks source ORDER, so the last
definition is the one that binds.

**A confirmed production victim, not a hypothetical.** gunbc#9081 commit `29088e133` landed
`dag/gunbc/fabric_cell_converge.dag` carrying two definitions each of `fabric_cell_ids` and
`fabric_cell_population_unobserved`. The compile was clean, the witness rows were 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. The reviewer's own
inference was that it "will fail to parse or typecheck"; that inference was wrong, which is
itself part of the finding: the defect defeats the expectation a reader brings to it.

**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, which is luck rather than structure.

**Census caveat, stated so the population is not overread.** The live-instance search was a
line-anchored regex over module text at main. It is a LOWER BOUND on the population, not a
closed census: it cannot see definitions that differ in spacing or that a formatter joined,
and it says nothing about `type`/`data` declarations.

**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, per DESIGN §4b's rule that a class's rung is the minimum across its in-scope paths and
that 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, needing no corpus walk, no name resolution and
no type information. DESIGN §5's decidability test is met, so a lens counting occurrences
would be validation standing exactly where construction was available.

**The evidence, and the honest statement of where it executes.**
`dag/test/claim/duplicate_definition_binding_probe.dag` asserts the CORRECT behaviour — the
compiler refuses the two-definition module. Written the other way round ("assert the second
definition binds") it would be green today and would become a defender of the defect. Run by
hand at the branch head it FAILS, while its positive control — the same module with one
definition — PASSES; that pair is what establishes the census reached its subject and
answered rather than failing to run (`CensusNotRunnable` maps to `-1`, which reds both and
greens neither).

It is NOT enrolled in `v2.workflow.floor_expected_red`, and the reason is this row's own
subject one layer out. The census resolves its synthetic source against
`build_module_path_index_from_witness_roots`, which walks the live tree, so the module
declares `ReadsLiveTree` — and `v1_compiler.cli_run` `run_required_floor` routes every such
site to `DeclinedLiveTree`: discovered, counted, never run. Enrolling asserts that a row
reaches its subject and answers; a declined row answers nothing, so the enrolment would have
been a false assertion wearing the shape of coverage. This is item 28's population
(the guarantee-probe corpus, discovered and declined) gaining one more member, not a new
condition.

An earlier revision of this row WAS enrolled, justified by a sibling census probe that
declares no disposition and was inferred to route and pass. That inference was wrong twice
over: undeclared is `ReadsLiveTree` by the fail-closed default (`cli_run`
`parse_entry_live_tree_disposition`), so the sibling is declined too, and its passing was
never measured — a population fit standing where mechanism confirmation was required.

**EXECUTION TRIGGER** (distinct from the next-rung trigger, which is the ingestion wall): the
deletion of the `DeclinedLiveTree` arm, which `v2.workflow.required_floor` already carries as
retained and staged for deletion at the root. When that lands, this row executes, reds, and
belongs on the expected-red roster the same day. When the WALL lands it flips green and
converts to a permanent regression control per DESIGN §4b meta-obligation (4).

## 12. Proposed sequencing (reconciled with the independent review; for operator sign-off)

**(2026-07-31 restructure.)** The canonical dependency order now lives in the roadmap
Expand Down
Loading