Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
5efe62a
A local coproduct arm must not re-bind when an unrelated pool type cl…
Sep 7, 2026
2a081d8
State the fixture consumer as local-only diligence, not merge-path ev…
Sep 7, 2026
a6878ef
Record that the isolated product and unit-arm fixtures do not close t…
Sep 7, 2026
eb6f274
Drop the cargo-test consumer so the four-file fixture has one executi…
Sep 7, 2026
11a8719
Regenerate docs/design-failure-modes.md from the edited failure-mode …
Sep 7, 2026
60e2cad
Record that an isolated unit-arm analogue is not the production Obser…
Sep 7, 2026
8c59d21
Cite the reproduce commands instead of a transcribed error count.
Sep 7, 2026
2abad0b
Enroll the inverted floor witness with the product-channel repair.
Sep 7, 2026
e922b91
Install the emitted stage0 mirror for the str_bindings-only lookup.
Sep 7, 2026
fbc8bd9
Drop the conjunction witness that recompiled both fixture arms.
Sep 7, 2026
80bf029
Merge origin/main to pick up the keyed declaration-index floor repair.
Sep 7, 2026
1502afe
Regenerate design-failure-modes.md from the merged ledger authorities.
Sep 7, 2026
b26dcc0
Repoint the fixture headers and keep imported products on-chain for w…
Sep 7, 2026
6c8aa41
Merge remote-tracking branch 'origin/main' into warm-wren-99-if-join-…
Sep 7, 2026
4b8fe66
Merge origin/main: keep both failure-mode receipts and leave the ledg…
Sep 7, 2026
b215837
Regenerate design-failure-modes.md from the merged ledger authorities.
Sep 7, 2026
01689bd
Merge origin/main: keep the inverted if-join witness after #10740 enr…
Sep 7, 2026
41e00b0
Regenerate ledger projections from the merged authorities.
Sep 7, 2026
3f4df43
Past-tense the failure-mode receipts that still described a red colli…
Sep 7, 2026
dfe0eb8
Name the on-chain binding walk once in infer_env.
Sep 7, 2026
db160b2
Merge origin/main; leave the failure-mode projection at the merge-bas…
Sep 8, 2026
33ad97c
Regenerate ledger projections from the merged authorities.
Sep 8, 2026
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
Original file line number Diff line number Diff line change
Expand Up @@ -36,23 +36,23 @@ data binding_chosen_by_pool_membership_rather_than_by_the_declared_rule: Recurri

"It lives in fixtures.if_join_pool_binding as four modules: declaring_module holds the subject and is byte-identical across both arms, colliding_module is the whole of the perturbation, and closure_with_collision and closure_without_collision are the two entry points. ",

"Reproduce with gunbc compile --source-root dag --source-root fixtures/if_join_pool_binding --entry fixtures/if_join_pool_binding/closure_with_collision.dag, which refuses at declaring_module with Coproduct(PoolSpecimenShape) vs Product(PoolSpecimenSquare), against the same command at closure_without_collision.dag, which reports 0 diagnostics. ",
"The merge-path consumer of those four files is test.claim.if_join_pool_binding_witness_test, admitted on required_gate_prefixes in THIS PR: it folds tools.multi_module_compile_fixture over two manifests that differ only in colliding_module membership, and both arms now expect compile-clean because the product-channel repair lands in the same tree. A v1-compiler-tests cargo-test module was added here and deleted: cargo test is compiled by clippy and run by nobody (gunbc.rung_drop rust_unit_tests_off_the_merge_path). gunbc#10740 authored the same consumer with the collided arm pinned RED as a defect; this PR supersedes that enrollment by landing the inverted (both-clean) witness with the repair, which is the option review 61772 named. Isolated off-chain PRODUCT collision is what the four-file fixture isolates. type_name_declares_own_type (widening) consumes v1.compiler.infer_env lookup_binding_on_chain: an imported product is on-chain and is not widened to a pool coproduct arm of the same spelling; an unimported pool product is not. The presence-census gate remains str_bindings-only. Reproduce the isolated product pair with gunbc compile --source-root dag --source-root fixtures/if_join_pool_binding --entry fixtures/if_join_pool_binding/closure_with_collision.dag against the same command at closure_without_collision.dag -- both entries compile clean after this repair; a revert of the widening carve-out reds the collided entry. THIS DOES NOT CLOSE THE CLASS. The production specimen that remains red under this same repair is Primitive(Observed) vs Coproduct(BeltObserve) at gunbc.roadmap.roadmap_belt_actuate, re-derived by running this binary on the gunbc#10683 tree as gunbc compile --source-root dag --source-root src/v2 --source-dir dag/gunbc/roadmap. This repair does not unblock that production specimen. An isolated unit-arm analogue of the four-file geometry (Dummy import, collider present, declaring_module unchanged) does not reproduce that production diagnostic under this repair, so this row does not record unit-arm as fixed; remaining-channel isolation from the production pair is a separate lane. ",

"THAT FIXTURE NOW HAS AN EXECUTING CONSUMER, which it did not when it landed: for its first weeks nothing in the tree named the directory -- no Rust test, no gate, no witness row -- so the class had a ratified rule, a committed synthetic and a next-rung trigger with NOTHING THAT COULD GO RED, which is the tier DESIGN section 4b rates worse than an absent check because a committed fixture is read as coverage. test.claim.if_join_pool_binding_witness_test reads those four files and hands them to tools.multi_module_compile_fixture as two manifests -- with and without colliding_module, the SAME declaring_module bytes in both -- and is admitted at exact module grain by v2.workflow.required_floor required_gate_prefixes, so the two arms fold on the required floor of every push. ",

"ITS RED ARM IS PINNED AS A DEFECT AND NOT AS A CONTRACT: when the repair below lands the collided manifest must COMPILE CLEAN and that arm must be rewritten, which is the wall landing rather than the witness breaking. ",
"ITS COLLIDED ARM WAS PINNED RED AS A DEFECT, NOT AS A CONTRACT, while the compiler still refused: gunbc#10740 enrolled that. THIS PR LANDED THE PRODUCT-CHANNEL REPAIR AND REWROTE THAT ARM -- both manifests now expect compile-clean, which is DESIGN section 4b(4)'s expecting-red probe flipping to a permanent regression control, not the witness breaking. A revert of the widening carve-out reds the collided arm again. ",

"THE DISCRIMINATION WAS DEMONSTRATED BY MUTATION rather than assumed: deleting colliding_module from the perturbed manifest reds exactly the two arms whose subject it is and leaves the positive control green, and pointing any manifest path at a file that does not exist refuses the read rather than rendering as zero diagnostics. ",
"THE DISCRIMINATION WAS DEMONSTRATED BY MUTATION rather than assumed, on the pre-repair witness: deleting colliding_module from the perturbed manifest redded the collided arm and left the positive control green, and pointing any manifest path at a file that does not exist refuses the read rather than rendering as zero diagnostics. After the repair both arms stay green under that same membership perturbation; the read-miss control is unchanged. ",

"The fixture is deliberately OUTSIDE the compiled source roots: an authentic collision committed into dag or src/v2 would be a real corpus fork, so the specimen is source handed to the compiler by a fixture, which is the position DESIGN section 4b names when it asks whether a RED is authorable. ",

"SO THE RED IS AUTHORABLE ON THE ENTRY-SCOPED PATH AND NEEDS NO WHOLE-CORPUS HARNESS, which is the DESIGN section 4b question asked before the check: nothing here is permanently green. ",
"SO THE RED WAS AUTHORABLE ON THE ENTRY-SCOPED PATH AND NEEDED NO WHOLE-CORPUS HARNESS, which is the DESIGN section 4b question asked before the check. The product-channel probe is now a regression control: both fixtures compile clean; a revert of the widening carve-out reds the collided entry. Remaining channels of the class are not permanently green. ",

"MECHANISM, stated because the obvious reading is wrong: resolution is LOCAL-FIRST -- v1.compiler.infer_env lookup_binding_by_name tries the module's own bindings, then its ancestry bindings, then the intern table, and only on a miss reaches global_bare_lookup -- so a local declaration is not being outranked. ",

"A coproduct ARM is simply not a local binding under its own spelling, so the arm reference misses local lookup entirely and lands in the pool beside the foreign top-level type. ",

"Downstream, v1.compiler.infer lookup_variant_parent_enum and variant_owner_node widen a record literal to its owner coproduct only when the binding resolves to a Disj owning that name, so the uncollided arm widens and the collided arm stays bare -- which is the whole of the asymmetry the diagnostic reports. ",
"Downstream, v1.compiler.infer lookup_variant_parent_enum and variant_owner_node widen a record literal to its owner coproduct only when the binding does not declare its own type on-chain. Before this repair an unimported pool product made type_name_declares_own_type true via global_bare, so the collided arm stayed bare; after it, only str_bindings and ancestry_str_bindings count, so the declaring module's arm still widens. ",

"THE RULE THIS SUBSTRATE ALREADY HAS, AND THE REASON THIS IS NOT A CALL FOR A NEW ONE: namespace-resolution-design.md section 13, operator-ratified 2026-07-21, is ANCESTOR-CHAIN UNIQUENESS -- exactly one on-chain candidate resolves, two-plus on-chain refuses as a typed AmbiguousReference, zero on-chain refuses as UnresolvedType -- and its host bracket NAME_RESOLUTION_POLICY_NAMESPACE_ONLY defaults to TRUE. ",

Expand Down Expand Up @@ -232,7 +232,7 @@ data binding_chosen_by_pool_membership_rather_than_by_the_declared_rule: Recurri
],

evidence: [
DeclarationRef { module_path: "test.claim.if_join_pool_binding_witness_test", decl_name: "an_unrelated_pool_member_refuses_the_declaring_modules_own_if_join", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.if_join_pool_binding_witness_test", decl_name: "the_declaring_module_compiles_clean_with_the_unrelated_pool_member", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.if_join_pool_binding_witness_test", decl_name: "the_same_declaring_module_compiles_clean_without_the_pool_member", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.if_join_pool_binding_witness_test", decl_name: "the_fixture_modules_are_readable", field: WholeDeclaration },
],
Expand Down
89 changes: 12 additions & 77 deletions dag/test/claim/if_join_pool_binding_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -16,40 +16,27 @@ import tools.multi_module_compile_fixture {

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

// THE EXECUTING CONSUMER FOR fixtures.if_join_pool_binding, WHICH HAD NONE.
// THE EXECUTING CONSUMER FOR fixtures.if_join_pool_binding.
//
// gunbc.recurring_failure_mode binding_chosen_by_pool_membership_rather_than_by_the_declared_rule
// committed its isolating synthetic rather than describing it, on the stated ground that a row
// citing a probe nobody runs is a transcription wearing a citation's clothes. The four modules
// landed and nothing read them: no Rust test, no gate, no witness row named the directory, so the
// class had a ratified rule, a fixture and a next-rung trigger and NOTHING THAT COULD GO RED. That
// is the tier DESIGN section 4b calls worse than an absent check, because a committed fixture is
// cited as coverage by the next reader. This file is the routing, and it adds no new specimen:
// the bytes it compiles are read from those four files, so the fixture stays the single authority
// for the specimen and this row is its consumer (DESIGN section 3, section 3c).
// committed its isolating synthetic rather than describing it. This file is the routing, and it
// adds no new specimen: the bytes it compiles are read from those four files, so the fixture stays
// the single authority for the specimen and this row is its consumer (DESIGN section 3, section 3c).
//
// WHAT IT WITNESSES IS THE INVARIANT, NOT A MESSAGE. The row names it IRRELEVANT-SCOPE EXTENSION
// INVARIANCE: for source S with resolved closure C, an environment E1 derived from C and an E2
// that is E1 plus declarations UNREACHABLE from S must typecheck S the same. Both manifests below
// supply the SAME BYTES of declaring_module -- one read, handed to both -- and differ only in
// whether colliding_module is a member. So a difference in verdict is a difference the subject's
// own text cannot explain, which is the whole instrument.
// whether colliding_module is a member.
//
// WHY THE MANIFEST INSTRUMENT AND NOT THE CLI COMMAND THE ROW QUOTES. Both are real; only one
// executes on the merge path. tools.multi_module_compile_fixture compiles a caller-authored source
// vector with NO module index and NO corpus roots, so the pool is EXACTLY the manifest -- which is
// what makes pool membership the isolated variable here rather than a property of whatever else
// the checkout contains. The quoted --source-root command remains correct and remains the way a
// human reproduces it by hand.
// vector with NO module index and NO corpus roots, so the pool is EXACTLY the manifest.
//
// THE RED ARM IS PINNED, AND IT IS PINNED AS A DEFECT RATHER THAN AS A CONTRACT. Today the collided
// manifest REFUSES, at an innocent site, with a branch-join mismatch; that refusal is the harm the
// row records, not behaviour to preserve. When the repair the row names lands -- a declaration
// identity authority deciding a reference's binder from the referencing module's own containment
// chain -- this arm must FLIP: declaring_module compiles clean under both manifests, and the
// remaining refusal, if any, is located at the reference rather than at the join. A flip is the
// wall landing, not this witness breaking, and whoever lands it rewrites this file's red arm and
// says so. Until then the arm asserts what the compiler DOES, so any silent change to it is loud.
// THIS PR LANDS THE PRODUCT-CHANNEL REPAIR with this consumer. The collided manifest used to refuse
// at the if-join; that refusal was the harm, not a contract. After on-chain widening (locals and
// imports, not the pool), declaring_module compiles clean under BOTH manifests. A later revert
// of that carve-out makes the with-collision arm red again. Remaining channels of the class stay open.

data if_join_declaring_path: String = "fixtures/if_join_pool_binding/declaring_module.dag"
data if_join_colliding_path: String = "fixtures/if_join_pool_binding/colliding_module.dag"
Expand All @@ -64,8 +51,6 @@ fn if_join_source(path: String) -> FixtureSource {
fixture_source(path: path, content: if_join_text(path: path))
}

// THE PERTURBED MANIFEST. Three modules; colliding_module is the whole of the difference and the
// entry does not name its colliding SPELLING for the class to fire -- membership is the variable.
fn if_join_with_collision_outcome() -> MultiModuleCompileFixtureOutcome {
compile_fixture(MultiModuleCompileFixture {
sources: [
Expand All @@ -77,9 +62,6 @@ fn if_join_with_collision_outcome() -> MultiModuleCompileFixtureOutcome {
})
}

// THE POSITIVE CONTROL. Same declaring_module bytes, colliding_module absent from the manifest.
// Without it the red arm above is equally satisfied by a broken harness, an unreadable fixture and
// a specimen that is simply ill-typed -- three failures indistinguishable from the red side.
fn if_join_without_collision_outcome() -> MultiModuleCompileFixtureOutcome {
compile_fixture(MultiModuleCompileFixture {
sources: [
Expand All @@ -90,25 +72,6 @@ fn if_join_without_collision_outcome() -> MultiModuleCompileFixtureOutcome {
})
}

// THE OUTCOME IS READ BY MATCHING, NEVER BY AN ACCESSOR, so FixtureInstrumentRefused -- the arm
// that says the HARNESS broke rather than the subject -- returns false to every reader here and
// therefore fails BOTH claims instead of silently satisfying the control.
fn if_join_refused_at_the_branch_join(o: MultiModuleCompileFixtureOutcome) -> Bool {
match o {
FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } =>
count(rows |> filter(r =>
r.blocking
&& (r.diagnostic_class as String) == "InternalError"
&& string_contains(
s: r.subject_name,
pattern: "if branches resolve to incompatible types: Coproduct(PoolSpecimenShape)"
)
)) > 0,
FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false,
FixtureInstrumentRefused { cause: c } => false
}
}

fn if_join_completed_clean(o: MultiModuleCompileFixtureOutcome) -> Bool {
match o {
FixtureCompileCompleted { module_count: n, emitted_files: files, diagnostics: rows, source_digest: sd, compiler_digest: cd } =>
Expand All @@ -118,10 +81,6 @@ fn if_join_completed_clean(o: MultiModuleCompileFixtureOutcome) -> Bool {
}
}

// THE HARNESS CONTROL, READ FIRST. An empty read renders as an empty module and every downstream
// claim would then be measuring the reader rather than the compiler; the subject-shaped assertion
// on declaring_module's own text is what distinguishes "the fixture was read" from "a file with
// that name exists".
test fn the_fixture_modules_are_readable() -> Bool {
string_length(s: if_join_text(path: if_join_declaring_path)) > 0
&& string_length(s: if_join_text(path: if_join_colliding_path)) > 0
Expand All @@ -131,34 +90,10 @@ test fn the_fixture_modules_are_readable() -> Bool {
&& string_contains(s: if_join_text(path: if_join_colliding_path), pattern: "type PoolSpecimenSquare")
}

// THE DISCRIMINATING RED. An unrelated module joins the pool and declaring_module -- which neither
// declares, imports nor is imported by it -- stops typechecking, at its own if-join.
test fn an_unrelated_pool_member_refuses_the_declaring_modules_own_if_join() -> Bool {
if_join_refused_at_the_branch_join(o: if_join_with_collision_outcome())
test fn the_declaring_module_compiles_clean_with_the_unrelated_pool_member() -> Bool {
if_join_completed_clean(o: if_join_with_collision_outcome())
}

// A THIRD ARM STOOD HERE AND WAS DELETED AS A DECORATION, recorded rather than silently removed
// because the reasoning is the same one this whole fixture exists to demonstrate (review 61981).
//
// `the_verdict_flips_on_pool_membership_alone` asserted
// `refused(with) != refused(without)`. Its RED IS UNAUTHORABLE while its two neighbours are green,
// and that follows from the outcome type rather than from any tree: arm 2 green means the without
// outcome is `FixtureCompileCompleted`, and `if_join_refused_at_the_branch_join` answers false on
// that constructor by construction. So with arm 1 green the third arm is `true != false` on every
// tree where its siblings hold, and on every tree where they do not, one of THEM reds first. It
// could never be the arm that discovered anything.
//
// THE JUSTIFICATION WRITTEN ABOVE IT NAMED THE ONE IMPOSSIBLE CASE: "a future tree in which both
// arms happen to agree cannot leave this file green". If the two arms agreed, arm 1 or arm 2 is
// already red by construction -- the state it claimed to guard against cannot be reached. That is
// DESIGN section 4b's question asked too late: whether the RED is authorable is decidable BEFORE
// the check is written, and a rostered identity on the required floor is priced per run.
//
// The flip is not lost with it. Arms 1 and 2 assert it between them, each with a LOCATED subject --
// one pins the specific if-join diagnostic, the other pins clean completion -- so a failure says
// which side moved, which the single combined proposition could not.
//
// THE SAME BYTES, WITHOUT THE POOL MEMBER, COMPILE CLEAN.
test fn the_same_declaring_module_compiles_clean_without_the_pool_member() -> Bool {
if_join_completed_clean(o: if_join_without_collision_outcome())
}
Loading
Loading