Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
2510fc1
The candidate rule is the chain, so an import becomes a binding on it…
Sep 21, 2026
f8c8015
Merge remote-tracking branch 'origin/main' into session/witty-cat-84
Sep 21, 2026
877bb48
The incumbent declaration counts as a claimant, and the test-code wal…
Sep 21, 2026
4d086a8
Binding rows bind to a fixed point, because a re-export chain is a ro…
Sep 21, 2026
9cef42a
A contested position answers nothing, on both spellings, and four dan…
Sep 21, 2026
808e5c6
Two more dangling declarations, a comment describing a route that doe…
Sep 22, 2026
7da1f90
Merge remote-tracking branch 'origin/session/witty-cat-84' into sessi…
Sep 22, 2026
6b7fac5
Merge remote-tracking branch 'origin/main' into session/witty-cat-84
Sep 22, 2026
894238a
A binding is not a declaration, so it stays out of the spelling census
Sep 22, 2026
5aee537
Delete the annotation fragment my own deletion orphaned
Sep 22, 2026
b5023bb
Resolution carries the declaring path to its consumers, so a resolved…
Sep 22, 2026
5e7c2b8
The live pair is OBSERVED: standing flips to required, and its rung d…
Sep 22, 2026
851d939
The XL-0 status arm stops citing the refusal this PR deletes, and nam…
Sep 22, 2026
21bed04
Merge remote-tracking branch 'origin/session/witty-cat-84' into sessi…
Sep 22, 2026
3bdadbf
The missing import row my own rule would have refused, and the warm r…
Sep 22, 2026
05d7394
A missing binding refuses with evidence too, not just a location
Sep 22, 2026
d5b6279
declaration_reference_path_optional: delete the dead length guard, an…
Sep 22, 2026
127e933
The instruments resolve the corpus the way production does, and the w…
Sep 22, 2026
cacd2ff
A re-export's declaring path is the home's, not the relay's
Sep 22, 2026
ba627a1
Enrol the four xl0r resolve producers the roster was missing, includi…
Sep 22, 2026
2f7ed92
Merge remote-tracking branch 'origin/session/witty-cat-84' into sessi…
Sep 22, 2026
e7e7abb
Delete a dangling leftover, and enrol the recompute my arity change e…
Sep 22, 2026
6f43000
Merge remote-tracking branch 'origin/session/witty-cat-84' into sessi…
Sep 22, 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
2 changes: 1 addition & 1 deletion dag/gunbc/compiler_frontend_program_status.dag
Original file line number Diff line number Diff line change
Expand Up @@ -947,7 +947,7 @@ fn stage_status(s: NamespaceCutStage) -> MilestoneStanding {
StageF0 => milestone_status(m: NamespaceWaveAdmissionEnrolled)
StageXL0Denominator =>
NotDerivable {
why: "XL-0 is the REPAIR-INPUT ORIGIN DENOMINATOR: source-declaration carriers whose DECLARING identity is what answered each mention. The producer EXISTS and ANSWERS on the production route -- v2.compiler.repair_input_origin_roster repair_input_origin_roster_over_roots is total and non-empty over a production-ingested fixture and carries the cross-module mention (gunbc#11582; re-run rather than trust: v2.test.claim.namespace_xl0.cross_module_reference_resolution, v2.test.claim.namespace_xl0.call_argument_mention_survival). THIS ARM READ CLEAR OFF THAT FOR ONE HEAD AND THAT WAS RUNG INFLATION (review 67708): the roster's RepairInputDeclared.declaring is derived from the authored SPELLING (v2.compiler.resolution_provenance resolve_reference_provenance confirms the index hit and rebuilds the declaration from the path; carrier_declaration_ref drops an owner prefix), while the compiler resolver refuses the same reference resolve_reason_qualified_target_identity_unrepresentable because it carries no exact declaring identity. The roster module's own frontier row (repair_input_declared_binding_frontier_dissolve_on) says the spelling-derived identity becomes a second authority the moment the roster produces on the production route, which is now. A denominator whose declaring identities are spelled rather than bound is not the population this stage is defined by (DESIGN section 3, one authority; section 4b(1), the reported rung equals the executed evidence). Derivable when the resolver answers a qualified reference with an exact declaring identity by execution and the roster's `declaring` is derived from that binding; the collector-side capability (the dotted-reference lowering) is landed and is not what is missing. The base-pinned execution remains ACT-0's DenominatorRosterDigest either way." as NonEmptyStr,
why: "XL-0 is the REPAIR-INPUT ORIGIN DENOMINATOR: source-declaration carriers whose DECLARING identity is what answered each mention. The producer EXISTS and ANSWERS on the production route -- v2.compiler.repair_input_origin_roster repair_input_origin_roster_over_roots is total and non-empty over a production-ingested fixture and carries the cross-module mention (gunbc#11582; re-run rather than trust: v2.test.claim.namespace_xl0.cross_module_reference_resolution, v2.test.claim.namespace_xl0.call_argument_mention_survival). THIS ARM READ CLEAR OFF THAT FOR ONE HEAD AND THAT WAS RUNG INFLATION (review 67708): the roster's RepairInputDeclared.declaring is derived from the authored SPELLING (v2.compiler.resolution_provenance resolve_reference_provenance confirms the index hit and rebuilds the declaration from the path; carrier_declaration_ref drops an owner prefix), while the roster's own `declaring` is still that spelling. THE RESOLVER HALF OF THIS CAPABILITY LANDED (gunbc#12048, fierce-wren-487): v2.compiler.resolve now decides ResolvedReferenceIdentity = ResolvedToKernelSymbol or ResolvedToDeclaration carrying a path, and mints every module-level reference through resolved_reference_node, so a qualified reference IS answered with its exact declaring containment path by execution, and the interim refusal resolve_reason_qualified_target_identity_unrepresentable that this arm previously cited is DELETED -- it is no longer what holds XL-0 open. The roster module's own frontier row (repair_input_declared_binding_frontier_dissolve_on) says the spelling-derived identity becomes a second authority the moment the roster produces on the production route, which is now. A denominator whose declaring identities are spelled rather than bound is not the population this stage is defined by (DESIGN section 3, one authority; section 4b(1), the reported rung equals the executed evidence). ResolverBoundDeclaringIdentity is a TWO-CONJUNCT capability and only the first conjunct is landed, so the instrument stays NotBuilt and this arm stays NotDerivable: what remains is the SECOND conjunct -- v2.compiler.repair_input_origin_roster deriving RepairInputDeclared.declaring from the resolved tree's ResolvedToDeclaration path instead of from resolve_reference_provenance's spelling rebuild (carrier_declaration_ref). That is the dissolution the roster module's own frontier row already names. The collector-side capability (the dotted-reference lowering) is landed and is not what is missing either. The base-pinned execution remains ACT-0's DenominatorRosterDigest either way." as NonEmptyStr,
cause: needs(i: ResolverBoundDeclaringIdentity)
}
StageXL1BaselineCapture =>
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
module gunbc.recurring_failure_mode.a_binding_position_recorded_as_a_declaring_identity

import std.types { NonEmptyStr }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data a_binding_position_recorded_as_a_declaring_identity: RecurringFailureMode = RecurringFailureMode {
identity: "a_binding_position_recorded_as_a_declaring_identity" as NonEmptyStr,
receipts: [
"**a position that merely BINDS a name is recorded as the position that DECLARES it** (INVALID STATE: an index that keys declarations by their declaring path takes a row's TARGET as that path. A target names a position the index can answer at, which is a declaration only when a declaration was written there; for a re-export it is another row's binding. v2.compiler.symbol_index_fill symbol_index_bind_pending_round passed p.row.target straight to symbol_index_bind_at as declaring_path.)",
"HARM. One declaration acquires one identity PER RELAY it is reached through, so the map that exists to make identity single-valued is the thing that forks it. Nothing refuses: every path resolves, and the reference is Accepted. It surfaces downstream as a wrong answer with no diagnostic -- a target that spells a declaration by its module emits a path into the relay module, which declares nothing and therefore has no item to name, so the emitted program refers to something that was never written.",
"DISTINGUISHING FACTS. refusal_reason_minted_as_canonical_identity is a value minted from the WRONG VOCABULARY (a diagnostic reason standing in a name's place); this row is a value from the RIGHT vocabulary read at the WRONG LAYER -- a real qualified path, naming a real position, that is a binding rather than a declaration. The recognition rule is a question, not a spelling: when a field is named for a DECLARATION, ask whether every writer of it can only have written a declaration there, and follow one re-export before answering. An index whose lookup succeeds at a relay will answer that question wrong and stay green.",
"RECEIPT (2026-09-22, fierce-wren-487, found by review 70003 on gunbc#12048). Uninhabited until resolution began CARRYING the declaring path: while a resolved reference was a bare leaf the recorded declaring path reached no consumer, so the fork existed in the index and was unobservable. The enrolled chain claim could not see it either -- it asserted only that the chain RESOLVES, and an index that stops at the relay resolves perfectly well. Repaired by chasing one step through symbol_index_claimants_at, which already answers who declares what lives at a position; a relay's own row was chased the same way when it bound, so one step reaches the home. Enrolled: v2.test.claim.namespace_xl0.cross_module_reference_resolution a_re_export_resolves_to_the_home_not_the_relay_holds, whose NEGATIVE conjunct is the discriminator -- measured FAIL before the chase and PASS after, with the sibling same-leaf row PASS in both runs.",
"RUNG FOUND AT: outside the ladder -- silent wrongness.",
"CEILING: structurally impossible. A binding position and a declaring position are different concepts sharing one carrier (QualifiedName), so either can be written where the other is owed. The wall is the type: a declaring identity a binding path cannot inhabit, which is the same wall refusal_reason_minted_as_canonical_identity names from its own direction.",
"NEXT-RUNG TRIGGER: a declaration-identity carrier distinct from the qualified path of an arbitrary position, so that symbol_index_bind_at cannot be handed a binding position at all; until then the enrolled row above is the wall, and it is a permanent regression control rather than an expecting-red probe.",
],
evidence: [
DeclarationRef { module_path: "v2.compiler.symbol_index_fill", decl_name: "symbol_index_bind_pending_round", field: WholeDeclaration },
DeclarationRef { module_path: "v2.std.symbol_index", decl_name: "symbol_index_declaring_path_of", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.claim.namespace_xl0.cross_module_reference_resolution", decl_name: "a_re_export_resolves_to_the_home_not_the_relay_holds", field: WholeDeclaration },
],
}
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,10 @@ data refusal_reason_minted_as_canonical_identity: RecurringFailureMode = Recurri
"RUNG FOUND AT: outside the ladder -- silent wrongness.",
"CEILING: structurally impossible. A reason symbol and a canonical identity are different concepts and should not share a carrier; a resolver that returns Symbol for both can write one where the other is owed. The wall is the type: resolution answering with a declaration identity carrier that a Diagnostic.reason cannot inhabit.",
"NEXT-RUNG TRIGGER: v2.compiler.resolve canonical identities carried as a declaration-identity type distinct from Symbol, so that the fallback argument cannot be spelled with a reason symbol; until then the enrolled row above is the wall.",
"CLIMB RECEIPT (2026-09-22, fierce-wren-487). The trigger fired: v2.compiler.resolve now decides ResolvedReferenceIdentity = ResolvedToKernelSymbol { symbol } | ResolvedToDeclaration { path } and mints every module-level reference through resolved_reference_node, so a corpus declaration reference is carried as its declaring QualifiedName -- the qualified-name spine -- and the `fallback:` argument, symbol_index_node_identity, and the interim refusal resolve_reason_qualified_target_identity_unrepresentable are deleted. A reason symbol can no longer reach the declaration arm (a path is not a Symbol), and the kernel arm admits only a symbol the language model declares canonical, which no reason symbol is. Rung: structurally guaranteed, not impossible -- an Atom naming a corpus declaration remains constructible by a fixture; no Accepted resolved body carries one because resolve is the only producer and its remaining canonical_atom sites are the frame-local binder, the literal and the kernel arm. Evidence, by execution: v2.test.claim.namespace_xl0.cross_module_reference_resolution -- two consumers importing one leaf from two providers resolved to EQUAL nodes before this change with no refusal at all (the silent collapse the ruling predicted), and now resolve to their two declaring paths; the found-fn and data-target rows flipped from the interim refusal to Accepted carrying the path.",
],
evidence: [
DeclarationRef { module_path: "v2.compiler.resolve", decl_name: "try_resolve_qualified_name_node", field: WholeDeclaration },
DeclarationRef { module_path: "v2.compiler.resolve", decl_name: "resolved_reference_node", field: WholeDeclaration },
],
}
6 changes: 4 additions & 2 deletions dag/gunbc/rung_drop/native_lane_live_pair_expected_red.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module gunbc.rung_drop.native_lane_live_pair_expected_red

import std.types { List, NonEmptyStr }
import gunbc.rung_drop { RungDrop, Standing, TypedDeclaration, ReplacementStaged }
import gunbc.rung_drop { RungDrop, Retired, TypedDeclaration, ReplacementStaged }
import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable }

// DECLARED 2026-09-21 (v2 foundation manager ruling, no-regression standard for gunbc#11952; the
Expand Down Expand Up @@ -34,7 +34,9 @@ data native_lane_live_pair_expected_red: RungDrop = RungDrop {

declared: "2026-09-21",

standing: Standing,
standing: Retired {
trigger_fired: "2026-09-22, gunbc#12009. All three conjuncts executed on the emitted route before the edit: (1) v2.native_lane_fixture.control RESOLVES under the namespace candidate rule -- measured on the real source bytes, not an isomorphic fixture; (2) a run through the emitted binary's native_test_eval_one observed native_lane_false_control = ReturnedFalse AND native_lane_true_control = Passed, the first observation of the pair on any head; (3) gunbc.witness_v2_native_route native_route_live_pair_standing set to LivePairRequired in the same change. The pair is now a permanent regression control (DESIGN 4b(4)), not retired evidence. Receipt -- dag head, emitter source, emitted-closure hash, both verdicts, command -- in gunbc#12009's body." as NonEmptyStr
},

declaration: TypedDeclaration {
previous: MechanicallyPreventable,
Expand Down
54 changes: 35 additions & 19 deletions dag/gunbc/witness/v2_native_route.dag
Original file line number Diff line number Diff line change
Expand Up @@ -904,29 +904,45 @@ data native_route_live_control_false_declaration: String = "native_lane_false_co
data native_route_live_control_true_declaration: String = "native_lane_true_control"

// THE LIVE PAIR'S STANDING: REQUIRED, OR ENROLLED AS AN EXPECTING-RED PROBE PINNED TO ITS CAUSE
// (manager ruling 2026-09-21). On main 79e745b4 and on gunbc#11952 alike, the module both controls
// live in, `v2.native_lane_fixture.control`, is refused at PREPARE with
// `resolve_ambiguous_on_global_bare` on the bare `SubstrateInputsOnly` (the emitted binary's own
// `census-resolve` names it), as is the whole population -- so neither control can be observed by
// any head until the native resolver admits that form. Leaving the clause required would make the
// lane unadmittable for a reason no lane change can move; dropping it would lose the control.
// Enrolling it keeps the evidence: the clause holds ONLY while both controls refuse at the pinned
// stage with the pinned FATAL reason and the pinned lookup CLASS in their chain. A DIFFERENT refusal is a moved wall and refuses as not
// observed; an OBSERVED control refuses as `LivePairObservedWhileEnrolledRed`, which is the flip
// signal -- the standing must then become `LivePairRequired`, and the pair is a required-green
// control from that head on (DESIGN 4b(4): the probe flips to a permanent regression control, it
// does not retire). RETIREMENT TRIGGER, the capability: the native resolver admits the retained
// forms (v2 foundation package 12, the namespace candidate rule).
// (manager ruling 2026-09-21). The enrolled arm was declared because, on main 79e745b4 and on
// gunbc#11952 alike, the module both controls live in -- `v2.native_lane_fixture.control` -- was
// refused at PREPARE with `resolve_ambiguous_on_global_bare` on the bare `SubstrateInputsOnly`, as
// was the whole population: no head could observe the pair until the native resolver admitted that
// form, and a required clause would have refused every receipt for a reason no lane change could
// move. THAT CONDITION ENDED on 2026-09-22 (gunbc#12009), and the standing below is now
// `LivePairRequired`; the enrolled arm is kept in the type because it is how a future stall would
// be declared, not because anything is enrolled in it today.
//
// WHY THE ENROLLED ARM PINS THREE AXES, worth keeping now that it is unused: the clause held ONLY
// while both controls refused at the pinned stage with the pinned FATAL reason and the pinned
// lookup CLASS in their chain. A DIFFERENT refusal is a moved wall and refuses as not observed; an
// OBSERVED control refuses as `LivePairObservedWhileEnrolledRed`, which is the flip signal. That
// is what makes the arm a probe rather than a hole: it cannot be satisfied by the subject getting
// worse in a new way, and it cannot outlive the condition it describes.
type NativeRouteLivePairStanding
= LivePairRequired
| LivePairExpectedRed { stage: NativeTestStage, fatal_reason: Symbol, class_reason: Symbol, trigger: String }

data native_route_live_pair_standing: NativeRouteLivePairStanding = LivePairExpectedRed {
stage: NativeTestStagePrepare,
fatal_reason: ^resolve_reason_ambiguous_symbol,
class_reason: ^resolve_ambiguous_on_global_bare,
trigger: "the native resolver admits the retained forms (v2 foundation package 12, the namespace candidate rule)"
}
// FLIPPED TO REQUIRED 2026-09-22 (gunbc#12009, v2 foundation package 12 -- the trigger this row
// named). The pair is OBSERVED. All three conjuncts of the retirement trigger were executed on the
// emitted route before this edit, which is the order DESIGN 4b(1) requires -- the reported rung
// must equal the rung executed evidence establishes, and flipping on "it resolves" alone would
// have been the inflation that section names:
// 1. v2.native_lane_fixture.control RESOLVES (real source bytes, not an isomorphic fixture);
// 2. native_lane_false_control observed ReturnedFalse AND native_lane_true_control observed
// Passed, through the emitted binary's own native_test_eval_one;
// 3. this standing set to LivePairRequired in the same change.
// The receipt -- head, emitter source, emitted-closure hash, both verdicts, the command -- is in
// gunbc#12009's body.
//
// IT DOES NOT RETIRE, IT FLIPS (DESIGN 4b(4)): the pair is now a permanent regression control, and
// a route that stops discriminating false from true reds this clause from here on. What the
// enrolled-red form bought was tolerance of a refusal no lane change could move; that refusal is
// gone, so the tolerance goes with it. The class it was pinned to -- resolve_ambiguous_on_global_bare
// -- no longer has a producer, which is why leaving the pin standing was not an option: an
// expecting-red probe pinned to an unproducible cause can never match, reads as a moved wall for
// every future head, and can never be retired by its own trigger.
data native_route_live_pair_standing: NativeRouteLivePairStanding = LivePairRequired

// A CONTROL MATCHES THE ENROLLMENT ONLY AS THE PINNED REFUSAL, ON ALL THREE AXES: the stage, the
// FATAL reason (`diagnostics_fatal_reason` -- the last diagnostic, never the head, which is
Expand Down
12 changes: 12 additions & 0 deletions dag/std/occurrence_binding.dag
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,18 @@ import std.types { String }
// by the v2 resolver instantiation and its DependencyView BindsTo projection. LexicalLookup is not
// an interim consumer: it has no exact reference-occurrence Node or occurrence containment
// identity, so binding it here would fabricate the relation this carrier preserves.
//
// WHAT THE V2 INSTANTIATION IS, READ FROM THE OTHER SIDE (fierce-wren-487, 2026-09-22, ruled a
// declared divergence and not a fork). v2.std.symbol_index LexicalLookup and v2.compiler.resolve
// SymbolIndexAtomLookup answer the SAME question this result type answers -- which declaration
// binds one reference occurrence: none, one, or more than one -- at the same grain (v2's hit is
// for one occurrence and carries its occurrence id), and v2's 0/1/many selection over its
// candidates (symbol_index_lexical_lookup) duplicates occurrence_binding_from_candidates. The two
// naming schemes agree: ContainmentPath<N> of nodes and v2's QualifiedName of Named edges are the
// same containment path read as nodes vs as labels, which is why v2 resolution now carries a
// declaration reference as that path. The candidate PRODUCERS are legitimately layered (a supplied
// population here, the index chain walk there) and are not what the trigger collapses; the
// trigger is v2's selection fold and result vocabulary retiring into OccurrenceBindingResult<Node>.

type ContainmentPath<N> {
ancestors: FreeMonoid<N>
Expand Down
Loading