From 435429333486be29e834e29f533f61fc810f554a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 04:28:07 +0000 Subject: [PATCH 01/17] Genericity is declared, not inferred from a failed lookup At the census-borrowed declaration route, absence from a lookup was standing as positive evidence of generic ownership -- and the environment that lookup consulted has no bindings at all, so the evidence was unconditional rather than occasional. census_declaration_type_env builds bindings, str_bindings, ancestry_str_bindings and intern_table as empty maps, seeded only with the declaration's type-parameter bindings. In that environment lookup_binding_by_name_local can only ever find a tp_name. Two sites read a miss there as "this leaf is a generic": the roster producer declaration_unbound_leaf_names, whose results were concatenated into the generic-name roster, and the stamp producer declaration_substitution_basis, whose second disjunct repeated the same test. So for every census-borrowed declaration, every unqualified non-kernel concrete type name in every parameter was enrolled as a generic parameter and stamped TypeVariable { id: } -- always, not sometimes. The harm is at the DESIGN 4b floor. direct_call_argument_inhabitance_diags takes the substitution basis as the declared side whenever it carries an unbound type variable, and declared_type_inhabitance reads that stamp as a generic formal and declines with UndecidableGenericFormal. A value of any constructor reaching a NonEmptyStr or HostIdentity position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. That is DESIGN section 5's absorbing fallback: unable to resolve, so widen to generic, so decline. The authority was already in hand one field over. borrowed_census_callable_candidate computes borrowed_generic_param_names on its first line and classifies the RETURN type of the same declaration positively with it, via qualify_borrowed_type_names: roster members stay variables, every other bare leaf resolves to its owner module and is qualified. The parameter types, in the next field of the same record literal, went through the guess. One question, two answers (DESIGN section 3). The parameter side now consumes the same roster and the same qualifier, and the absence disjunct is deleted from both sites together, because they were one classification authority written twice. The roster reads a declared fact, not a naming convention: parse_optional_type_params mints one param per name in the angle-bracket clause whose name and whose type-expr name are both that name, and no authored parameter of that shape exists in the corpus. fn_type_param_names and param_is_generic_decl already read the same encoding. Declared limit: a synthesized or member declaration that borrows an enclosing owner's generic without restating it is not on its own roster, so that leaf stays bare and is reported UndecidableFormalUnresolved -- the reason that means exactly that -- rather than claiming a genericity the declaration does not carry. Its next-rung trigger is an owner-generic carrier on the borrowed declaration. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_env.dag | 12 +++++++---- src/v1/04_lookup.dag | 47 ++++++++++---------------------------------- 2 files changed, 18 insertions(+), 41 deletions(-) diff --git a/src/v1/04_env.dag b/src/v1/04_env.dag index 2905a358e45..8ba07bfdf32 100644 --- a/src/v1/04_env.dag +++ b/src/v1/04_env.dag @@ -1095,13 +1095,17 @@ fn declaration_substitution_basis(n: Node, env: TypeEnv, generic_names: List map(ch => declaration_substitution_basis(n: ch, env: env, generic_names: generic_names)) let with_children = node_with_children(n: n, children: children) let name = authored_name_at(source_indices: env.source_indices, node: n) + // THE ROSTER IS THE WHOLE TEST. A second disjunct used to stamp any bare, unqualified, + // non-kernel leaf that `lookup_binding_by_name_local` missed, which read absence from a + // lookup as positive evidence of generic ownership (DESIGN section 5's absorbing fallback) + // and, at the census caller whose declaration env carries no bindings at all, was total over + // every concrete type name a parameter mentions. `generic_names` is the authority for this + // question and is now the only one consulted; a leaf that is not on it and resolves nowhere + // is UNRESOLVED, which is a different fact with its own reported reason. let generic_leaf = n.connective == NoConnective && (n.children |> count) == 0 && name != "" - && ((generic_names |> any(g => g == name)) - || (!contains(name, ".") - && !is_kernel_type(name: name) - && lookup_binding_by_name_local(env: env, name: name) == none)) + && (generic_names |> any(g => g == name)) if generic_leaf { node_with_inferred(n: with_children, inferred: Present { value: TypeVariable { id: name } }) } else { diff --git a/src/v1/04_lookup.dag b/src/v1/04_lookup.dag index f2213f91889..a3d16b78fd9 100644 --- a/src/v1/04_lookup.dag +++ b/src/v1/04_lookup.dag @@ -627,27 +627,6 @@ fn borrowed_census_callable_candidate(type_env: TypeEnv, name: String, candidate } } -// A global-bare hit still names one exact declaration and its completed census. Resolve each -// formal at that declaration's containment position, once while that authority is present, rather -// than reconstructing it later through the caller TypeEnv. -// SEED WALKER DISPOSITION (DESIGN section 6): v1's canonical traversal idiom is a purpose-specific -// self-recursive Node collector; importing v2 fold_node/node_query here would invert the bootstrap -// because v1 compiles v2. This collector walks only the finite declaration type tree and dissolves -// with the sibling v1 walkers at the v2 self-host cut. A one-off shared walker for this carrier -// would add a traversal representation rather than consolidate the seed's existing population. -fn declaration_unbound_leaf_names(n: Node, env: TypeEnv) -> List { - let name = authored_name_at(source_indices: env.source_indices, node: n) - let here = if n.connective == NoConnective - && (n.children |> count) == 0 - && name != "" - && !contains(name, ".") - && !is_kernel_type(name: name) - && lookup_binding_by_name_local(env: env, name: name) == none { - [name] - } else { [] } - concat(here, n.children |> flat_map(ch => declaration_unbound_leaf_names(n: ch, env: env))) -} - fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String, node: Node) -> List { let tp_names = fn_type_param_names(item: node, source_indices: type_env.source_indices) let declaration_env = census_declaration_type_env( @@ -656,31 +635,25 @@ fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String tp_names: tp_names, source_indices: type_env.source_indices ) - let return_type = match node.inferred { - Present { value: Resolved { node: resolved_return } } => resolved_return - _ => match node.type_annotation { - Present { value: annotated_return } => annotated_return - Absent => error_type - } - } - let declaration_generic_names = concat( - tp_names, - concat( - declaration_unbound_leaf_names(n: return_type, env: declaration_env), - node.params |> flat_map(p => declaration_unbound_leaf_names(n: param_node_type_expr(n: p), env: declaration_env)) - ) - ) + let declaration_generic_names = borrowed_generic_param_names( + params: node.params, source_indices: type_env.source_indices) node.params |> filter(p => !(tp_names |> any(tp => tp == param_node_name_at(n: p, source_indices: type_env.source_indices)))) |> map(p => { - let declared_type = param_node_type_expr(n: p) + let declared_type = qualify_borrowed_type_names( + n: param_node_type_expr(n: p), + owner_module_path: owner_module_path, + env: type_env, + excluded: declaration_generic_names + ) ResolvedFormal { parameter_identity: param_node_name_at(n: p, source_indices: type_env.source_indices), declared_type: declared_type, declaration_bound_conformance: preserve_outer_optional_cardinality( outer: declared_type, inner: peel_nominal_alias_identity(n: declared_type, env: declaration_env, module_name: owner_module_path)), - substitution_basis: declaration_substitution_basis(n: declared_type, env: declaration_env, generic_names: declaration_generic_names) + substitution_basis: declaration_substitution_basis( + n: declared_type, env: declaration_env, generic_names: map_keys(declaration_generic_names)) } }) } From f5a1e535e62f12c2f5db95a7ea48e89d7a494ff2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 04:50:38 +0000 Subject: [PATCH 02/17] Attach the roster annotation at module-item grain DESIGN 4c admits only standalone leading blocks attached to module-scope declarations; the block sat inside declaration_substitution_basis's body and the v2 self-compile refused it seven times, once per line. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_env.dag | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/v1/04_env.dag b/src/v1/04_env.dag index 8ba07bfdf32..dfa88052576 100644 --- a/src/v1/04_env.dag +++ b/src/v1/04_env.dag @@ -1091,17 +1091,17 @@ fn lookup_type_by_name(env: TypeEnv, name: String) -> Node? { // substitution basis. Synthesized constructors can mention a parent generic that is not exposed // as one of their own generic params; after resolution that leaf otherwise looks like a concrete // Primitive(T). No consumer may reconstruct this distinction through the caller environment. +// THE ROSTER IS THE WHOLE TEST. A second disjunct used to stamp any bare, unqualified, +// non-kernel leaf that lookup_binding_by_name_local missed, which read absence from a lookup as +// positive evidence of generic ownership (DESIGN section 5's absorbing fallback) and, at the +// census caller whose declaration env carries no bindings at all, was total over every concrete +// type name a parameter mentions. generic_names is the authority for this question and is now +// the only one consulted; a leaf that is not on it and resolves nowhere is UNRESOLVED, which is +// a different fact with its own reported reason. fn declaration_substitution_basis(n: Node, env: TypeEnv, generic_names: List) -> Node { let children = n.children |> map(ch => declaration_substitution_basis(n: ch, env: env, generic_names: generic_names)) let with_children = node_with_children(n: n, children: children) let name = authored_name_at(source_indices: env.source_indices, node: n) - // THE ROSTER IS THE WHOLE TEST. A second disjunct used to stamp any bare, unqualified, - // non-kernel leaf that `lookup_binding_by_name_local` missed, which read absence from a - // lookup as positive evidence of generic ownership (DESIGN section 5's absorbing fallback) - // and, at the census caller whose declaration env carries no bindings at all, was total over - // every concrete type name a parameter mentions. `generic_names` is the authority for this - // question and is now the only one consulted; a leaf that is not on it and resolves nowhere - // is UNRESOLVED, which is a different fact with its own reported reason. let generic_leaf = n.connective == NoConnective && (n.children |> count) == 0 && name != "" From 8e3835f1bc0393642547724be9c20357d0205993 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 05:20:19 +0000 Subject: [PATCH 03/17] Narrow the change to the roster: declared_type stays authored Routing declared_type through qualify_borrowed_type_names was a second, wider claim riding under this one's title. Every consumer of ResolvedFormal.declared_type would have read a qualified name where it read a bare one, and one of them -- direct_call_generic_type_argument_inhabitance_diags -- compares authored_name_at of the declared node against the actual's for EQUALITY. A population delta after that change could not be attributed to the genericity repair. Only the roster moves: declaration_generic_names is now borrowed_generic_param_names (the declaration's own generic clause) rather than a census of lookup failures, and declaration_substitution_basis consults that roster alone. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_lookup.dag | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/v1/04_lookup.dag b/src/v1/04_lookup.dag index a3d16b78fd9..17474068992 100644 --- a/src/v1/04_lookup.dag +++ b/src/v1/04_lookup.dag @@ -640,12 +640,7 @@ fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String node.params |> filter(p => !(tp_names |> any(tp => tp == param_node_name_at(n: p, source_indices: type_env.source_indices)))) |> map(p => { - let declared_type = qualify_borrowed_type_names( - n: param_node_type_expr(n: p), - owner_module_path: owner_module_path, - env: type_env, - excluded: declaration_generic_names - ) + let declared_type = param_node_type_expr(n: p) ResolvedFormal { parameter_identity: param_node_name_at(n: p, source_indices: type_env.source_indices), declared_type: declared_type, From 8da9b48813587fc2ee0198286b3d54144778c12f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 06:30:36 +0000 Subject: [PATCH 04/17] Land the regenerated stage0 mirrors and the failure-mode row with the repair The .dag edit without its emitted seed is drift: heal-generated-artifacts succeeded on the previous head while required-witnesses-build refused on exactly v1_compiler_infer_env.rs and v1_compiler_infer_lookup.rs. Leaning on heal to launder that is relying on one mechanism to answer for a lane that is separately refusing, so the mirrors are regenerated and committed here, verified by content: the env mirror loses the lookup disjunct, and the lookup mirror loses declaration_unbound_leaf_names entirely. Regenerated by target/release/claim_executor --required-ci --required-lane build into target/stage0-regen-candidate and installed from there. Files the class row adds: gunbc.recurring_failure_mode lookup_miss_read_as_positive_classification, enrolled in the roster, with its projection into docs/design-failure-modes.md. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- ...p_miss_read_as_positive_classification.dag | 28 ++++++++ dag/gunbc/recurring_failure_mode/roster.dag | 2 + docs/design-failure-modes.md | 2 + src/v1/stage0/src/v1_compiler_infer_env.rs | 7 +- src/v1/stage0/src/v1_compiler_infer_lookup.rs | 68 ++----------------- 5 files changed, 38 insertions(+), 69 deletions(-) create mode 100644 dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag diff --git a/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag new file mode 100644 index 00000000000..c681d6629ec --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag @@ -0,0 +1,28 @@ +module gunbc.recurring_failure_mode.lookup_miss_read_as_positive_classification + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data lookup_miss_read_as_positive_classification: RecurringFailureMode = RecurringFailureMode { + identity: "lookup_miss_read_as_positive_classification" as NonEmptyStr, + + receipts: [ + "**a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. ", + + "WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. ", + + "SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. ", + + "Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable \{ id: \}`. Unconditional on that route, not sporadic. ", + + "THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable \{ UndecidableGenericFormal \}`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. ", + + "THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. ", + + "RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. ", + + "REPAIR AND ITS OWN LIMIT: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. A leaf that is not on the roster and resolves nowhere is UNRESOLVED, a different fact, reported `UndecidableFormalUnresolved`. NEXT-RUNG TRIGGER for the residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.)", + ], + + evidence: [], +} diff --git a/dag/gunbc/recurring_failure_mode/roster.dag b/dag/gunbc/recurring_failure_mode/roster.dag index 82ce4fe4b1e..21212095b55 100644 --- a/dag/gunbc/recurring_failure_mode/roster.dag +++ b/dag/gunbc/recurring_failure_mode/roster.dag @@ -174,6 +174,7 @@ import gunbc.recurring_failure_mode.native_stack_recursion_unbounded_over_corpus import gunbc.recurring_failure_mode.binder_renaming_changes_variant_field_lookup { binder_renaming_changes_variant_field_lookup } import gunbc.recurring_failure_mode.permissiveness_promoted_into_a_higher_safety_rung { permissiveness_promoted_into_a_higher_safety_rung } import gunbc.recurring_failure_mode.evaluation_model_cleanup_undeclared { evaluation_model_cleanup_undeclared } +import gunbc.recurring_failure_mode.lookup_miss_read_as_positive_classification { lookup_miss_read_as_positive_classification } data recurring_failure_mode_roster: List = [ a_type_name_asserts_an_algebra_the_arithmetic_does_not_carry, @@ -338,4 +339,5 @@ data recurring_failure_mode_roster: List = [ permissiveness_promoted_into_a_higher_safety_rung, native_stack_recursion_unbounded_over_corpus_shaped_structure, evaluation_model_cleanup_undeclared, + lookup_miss_read_as_positive_classification, ] diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 30dec706ad5..3d2ac4256cd 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -166,6 +166,7 @@ The exact `RecurringFailureMode.identity` population, which no other projection - `permissiveness_promoted_into_a_higher_safety_rung` - `native_stack_recursion_unbounded_over_corpus_shaped_structure` - `evaluation_model_cleanup_undeclared` +- `lookup_miss_read_as_positive_classification` --- @@ -347,3 +348,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **a refusal that is the FINAL policy is written up as a rung below a more capable one, and a next-rung trigger is filed promising to admit the case it deliberately refuses** (INVALID STATE: a class refuses some input; an author reasons that a future mechanism could HANDLE that input rather than refuse it, concludes the refusal is therefore below its ceiling, and files a DESIGN 4b(2) next-rung trigger naming the more capable mechanism. HARM: the trigger becomes a standing obligation to BREAK the semantics the refusal was chosen to protect, and it is discharged by making the system MORE PERMISSIVE, which moves the class DOWN the ladder while the roster records a climb. The row then reads as a known gap on the way to being closed, so the deliberate boundary loses its author and the next person to touch it satisfies the trigger in good faith. **THE RECOGNITION RULE, SCOPED TO WHAT IT CAN ACTUALLY CARRY: EXPANDING A DELIBERATELY CHOSEN REFUSAL BOUNDARY IS NOT A SAFETY CLIMB MERELY BECAUSE IT ADMITS MORE CASES.** Read the proposed trigger and ask whether discharging it would make the system ACCEPT AN INPUT THE DESIGN DELIBERATELY REFUSES. If so, the trigger is a capability request wearing a safety rung's clothes and belongs in a product decision rather than on the ladder. THE LADDER MEASURES HOW A DECISION IS ENFORCED, NOT HOW MANY CASES IT ADMITS -- but only the DECISION's enforcement, which is why the boundary must be a chosen one for this row to apply. **THE RULE WAS STATED TOO WIDELY IN THIS ROW'S FIRST WRITING AND IS CORRECTED HERE RATHER THAN SOFTENED.** It said a genuine next-rung trigger ALWAYS preserves which inputs are admitted and which refused, changing only whether the refusal is checked or unwritable. THAT IS FALSE ACROSS THE LADDER, and the counterexample is an ordinary rung-1 to rung-2 climb: a failure that previously OCCURRED and was contained -- by a total operation, a rollback, an isolation boundary -- begins being BLOCKED once a gate exposes it, so the admitted set genuinely shrinks and behaviour genuinely changes. A universal rule that forbids that would refuse most real climbs, and a row whose recognition rule fires on legitimate work is worse than no row: it teaches reviewers to discount it. So the class is scoped to a DELIBERATELY CHOSEN refusal boundary, which is the population both receipts below actually inhabit. **THE ORDER OF THE TWO QUESTIONS IS WHAT ACTUALLY GOES WRONG, AND IT IS AN ORDER ERROR RATHER THAN AN IGNORANCE ERROR.** 4b(2) says a class below its ceiling must name its next-rung trigger. That obligation is CONDITIONAL, and the condition is the part that gets skipped: the class must first be ESTABLISHED to sit below a ceiling. An author who feels the obligation before performing the derivation will always find a trigger, because a more capable mechanism can be imagined for any refusal. So the diligent-seeming move -- 'the rule says name a trigger, so I will name one' -- is exactly the move that manufactures the defect, and reviewers reward it because a row with a trigger looks more complete than a row without one. **BOUNDARY AGAINST ceiling_never_exercised_for_a_population_the_census_cannot_plan AND AGAINST AN UNDERIVED CEILING, which are the two nearest neighbours and arrive from the opposite direction.** Asserting a ceiling NUMBER without deriving it claims the class cannot climb; this class assumes without deriving that the class CAN climb. Both skip the same derivation and they fail in opposite directions, which is why they are separate rows rather than one: the repair for an underived ceiling is to derive it and possibly climb, and the repair here is to derive it and possibly DELETE THE TRIGGER. A single row would make one of those two repairs invisible. **RECEIPT, gunbc.scm.merge_base, 2026-09-06.** The squash merge refuses divergent per-path content at MANIFEST GRAIN rather than merging file contents line by line. This author wrote that absent line-level merging was 'a stated scope with a next-rung trigger: a text-difference capability'. The side-chat reviewer refused it: refusing divergent file contents can be the FINAL safety policy of the operation, and a text-difference capability increases ADMITTED MERGE POWER rather than safety. If the semantics are deliberately 'never synthesize file content neither author supplied', then text-level auto-merge VIOLATES those semantics instead of climbing toward them, and the trigger would have been an obligation to break the design. The trigger was not written; what was written instead is that manifest-grain conflict is a deliberate semantic boundary, with whether line-level merging is wanted AT ALL left open as a product question rather than presumed. **A SECOND RECEIPT ON THE SAME LANE AND THE SAME DAY, WHICH IS WHY THIS IS A CLASS AND NOT AN ANECDOTE.** gunbc.scm.integration records the consumed source as a commit reference, which stops being a durable anchor if source commit records are ever PHYSICALLY DELETED rather than merely kept out of target ancestry. The reflex was to file that as a next-rung trigger. It is not one: retirement is a capability nobody has asked for, nothing establishes that this cut sits below a ceiling, and a trigger would have committed a future author to build durable provenance for a deletion feature that may never exist. It is recorded in that module as a FUTURE BOUNDARY -- what would have to be designed IF the capability is ever wanted -- which carries the same information and creates no obligation. THE REPAIR IS USUALLY A RESTATEMENT, NOT A DELETION: the knowledge is worth keeping, and only its status as a debt is false. **CEILING: UNDERIVED, AND STATED SO RATHER THAN GUESSED, on this row's own rule.** Deciding mechanically whether a proposed trigger widens the admitted set requires comparing the semantics before and after a mechanism that does not exist yet, and this author has not established that comparison is decidable from modeled facts. Asserting a rung here would be the underived-ceiling error in a row about underived ceilings. What is honest today: the class is caught by review, it has been caught twice by one reviewer on one lane, and the instrument that found both was a question a person asked rather than anything executed. NEXT TRIGGER: none is named, because naming one would require knowing the ceiling. - **a walk whose native-stack depth grows with the depth of corpus-shaped data, with no declared bound** (the compiler recurses once per level of a structure whose depth is an input, not a constant. Past some corpus the process aborts on stack exhaustion. HARM: the abort is not a diagnostic -- it is a SIGSEGV turned into `thread ... has overflowed its stack` and an abort, so it carries no span, no diagnostic identity, and no partial result. The run neither succeeds nor refuses, and every downstream reader sees a crashed process rather than a located refusal. Worse, the abort is silent about its own cause -- it kills the process before the summary line, so the very output that would characterise the input is the output you lose. **THE DISTINGUISHING FACT IS THAT THE RECURSION NEED NOT APPEAR IN OUR SOURCE AT ALL.** The class has two instances and they differ in exactly this, which is why one row covers both and why looking only for authored recursion finds half of it. AUTHORED INSTANCE: `v1.compiler.infer_types` `node_type_shape` and `node_type_shape_argument_list` are mutually recursive over type structure with no depth bound, rendering `Primitive(...)`, `Named(...)`, `Product(...)`, `Coproduct(...)` by descending into children. A reader can find this one, and grep for `fn` names finds it. COMPILER-GENERATED INSTANCE: `v1.std.core` `Node` carries `children: Rc>>` (and `params`, `uses`, `properties`, `body`, `type_annotation` likewise) with no hand-written `Drop`, so the DESTRUCTOR rustc synthesises recurses once per level on every release of a deep graph. **No reading of our own source can find it, because it is not in our source.** Grepping for recursion, auditing every `fn`, and eliminating every in-window candidate by inspection all report health -- and did, on the specimen below, where three code candidates in the failing window were correctly eliminated by reading while the actual recursion was in glue no one had written. **RECOGNITION RULE, and it is about the DATA, not about the code: any type whose values are trees or chains of unbounded depth carries this class in every operation that touches a whole value -- including the ones you did not write.** Construction, traversal, rendering, cloning, comparison, hashing, serialisation and RELEASE are all depth-recursive by default. The question to ask of a recursive carrier is not `which of my functions recurse` but `what happens to a value of this type at 10^6 levels`, and the honest answer is usually that nobody knows because nobody has one. **RECEIPT, EXECUTED, WITH A PAIRED CONTROL AND ONE CHANGED LINE** (2026-09-05, quick-heron-85, during the NS-N containment cut). A two-file subject -- `std.measure` plus `test.claim.long.reference_closure_equivalence_test`, compiled with `src/v2` and `src/v1` as name-pool roots -- aborts with `stack overflow` after four pipeline phases and before its diagnostic summary prints. THE STACK-THRESHOLD INSTRUMENT TURNS THE BINARY INTO A SCALAR: bisecting `ulimit -s` gives the minimum stack at which each configuration completes. Each file ALONE completes at 1024 KiB; the PAIR completes at 147456 KiB and overflows at 139264 KiB. A factor of at least 144, closed on both sides, which is what establishes the recursion as FINITE AND DEEP rather than unbounded-in-the-limit -- an unlimited stack completes. THE DISCRIMINATOR IS THE ONE-LINE PROBE, not the threshold: `std::mem::forget(resolved.clone())` at the head of `v1.compiler.compile` `emit_resolved_for_target_selected`, holding files, binary invocation, source roots, stack size and diagnostics fixed and changing ONLY whether the tree is ever released. Paired at the same stock 8192 KiB: unpatched OVERFLOW, leaked binary exit 1, zero `stack overflow`, and the summary line prints (496 blocking, 2643 advisory). The destructor was the recursion. **THE PROBE MUST FORGET A CLONE, NOT THE VALUE**, and this is the part worth carrying to the next investigator: `resolved` is an `Rc`, so forgetting IT merely drops one handle and moves the destructor to whoever holds the last one -- reading as a false PERSIST and killing a true hypothesis. Forgetting a CLONE pins the outer refcount above zero, so the contents can never be released no matter who else holds a handle. That converts `check the precondition` into `remove the failure mode`, which is the difference between a probe you have to trust and one that cannot lie. **WHAT DID NOT DISCRIMINATE, recorded because each looked decisive and cost a cycle:** diagnostic COUNT is blind -- a probe rendering 8,000 diagnostics does not overflow while this configuration's 3,139 does; per-diagnostic SHAPE is blind unless the shape is in the graph; and a 2,000-level-deep authored expression chain completes. The depth that matters is the depth of the structure RELEASED, which no probe varying the diagnostic list can reach. **RUNG FOUND AT: 1, MITIGATABLE, by fail-stop and process isolation -- AND SECTION 5's FAIL-CLOSED INTERFACE IS STILL VIOLATED. Both halves belong in the sentence.** The mitigation is real and is what earns the rung: the abort is a fail-stop at a process boundary, and that boundary PREVENTS AN ACCEPTED RESULT OR ANY OTHER SUCCESS PUBLICATION -- the run dies before its summary line, so no consumer receives a partial or fabricated answer. Section 4b names isolation among rung-1 mechanisms, so the absence of a typed result does not deny rung 1. **BUT RUNG 1 DOES NOT REHABILITATE THE SIGSEGV**: section 5 independently requires every path to succeed fully or fail with a TYPED, LOCATED diagnostic, and an abort carrying no subject, no span and no diagnostic identity fails that badly. The deficit is a rung-1 class with a standing section 5 interface violation, which is what makes it rank for repair. **AN EARLIER REVISION OF THIS ROW PLACED THE CLASS OUTSIDE THE LADDER, AND THAT WAS WRONG IN A WAY WORTH KEEPING VISIBLE** (corrected 2026-09-06, native review 5124409497). Section 4b's only exclusions are silent wrongness below the floor and the adjacent column of external reality, undecidable properties and undeclared intent; this class is none of those, and the row REFUTED ITS OWN EXCLUSION two sentences later by stating that the depth property is decidable, that nothing waits on external reality, and that both a declared bound and an iterative implementation are authorable. **EXCUSING A CLASS FROM HAVING A RUNG HAS THE SAME PRACTICAL EFFECT AS INFLATING ONE -- IT NEVER RANKS**, which is the failure this ledger exists to prevent, arriving from the low side rather than the high one. **CEILING: 3, STRUCTURALLY GUARANTEED -- NOT 4, BECAUSE DECIDABLE DOES NOT IMPLY RUNG 4.** Depth is decidable and nothing waits on external reality, but decidability establishes only that a structural decision procedure is POSSIBLE. If an unbounded recursive carrier remains WRITABLE while the compiler derives a proof or a refusal for it, that is rung 3. **RUNG 4 REQUIRES THAT THE INVALID STATE HAVE NO CONSTRUCTOR IN THE CANONICAL MODEL, AND THIS ROW CANNOT NAME THE CONSTRUCTOR-ELIMINATION PATH**: no canonical carrier model is in hand in which data-dependent native-stack recursion is inexpressible, and a recursive carrier is a thing the substrate is meant to be able to declare. The ceiling is therefore raised to 4 only by a future row that NAMES that model; until then, claiming 4 here would be the inflation this ledger refuses. **THE REPAIR MAY NOT BE A BIGGER STACK, A FATTER THREAD, OR A RAISED BUDGET, AND THE LEAK IS AN INSTRUMENT RATHER THAN AN ARM.** All four leave the abort exactly where it was and move the corpus at which it fires, which is section 5's absorbing fallback in its purest form: the failure arm WIDENS instead of refusing, the widening is denominated in the corpus rather than the change, and the deficit stops ranking for repair because the symptom moved. The two honest arms are a release and traversal whose depth does not grow with the data -- an explicit iterative teardown and an explicit worklist walk -- or a DECLARED depth bound enforced at construction, refusing a too-deep structure with a typed, located diagnostic naming the carrier and the level. **THE TRIGGER BELOW IS A DELIBERATE 1-TO-3 JUMP, STATED SO IT IS NOT MISREAD AS THE ADJACENT RUNG.** Deriving the risk from the declared carrier and failing compilation when an unbounded carrier lacks an iterative release or a declared bound is a STRUCTURAL GUARANTEE, rung 3 -- it skips rung 2 rather than passing through it. The rung-2 form, if the jump proves too large to take in one step, is a generated lens or an adversarial-depth witness that reliably exposes and blocks the class WHILE THE INVALID IMPLEMENTATION STAYS WRITABLE and safety depends on that mechanism executing and staying enrolled. **NEXT-RUNG TRIGGER, and it names a CAPABILITY rather than a repair to one carrier:** a mechanism that derives, from a declared carrier, whether any operation on it -- including generated ones -- can recurse without a bound, so that authoring an unbounded-depth carrier without an iterative release or a declared bound fails to compile. Repairing `Node` alone does not retire this row; it removes one instance, and `node_type_shape` would still stand, as would every carrier authored tomorrow. **BOUNDED AGAINST TWO NEIGHBOURS.** Section 5's absorbing fallback is a mechanism that WIDENS when it cannot answer precisely; here nothing widens and nothing is answered -- the process dies. And `right_censored_cost_read_as_exact` concerns a measurement truncated by a limit; the resemblance is superficial, because there the run completes and reports a bounded number, whereas here the limit destroys the run and its report together, which is precisely why the threshold instrument had to be built to get any number at all. **WHY THIS RECEIPT NAMES NO PRODUCER, STATED RATHER THAN LEFT AS AN OMISSION** (raised as a section 6 objection, review 61308). Section 6 requires a measurement to be cited by naming the producer that re-derives it, because A TRANSCRIBED NUMBER IS UNREACHABLE FROM THE THING THAT OWNS IT AND ROTS WITHOUT ANYONE TOUCHING EITHER END. **THE OWNER OF THESE FIGURES NO LONGER EXISTS.** Every number here was observed on a configuration requiring a resolver rule that is not on main and, by ruling, never lands in that shape; the specimen is extinct, so NO ENTRY POINT CAN RE-DERIVE IT AND NONE IS OWED -- which is the case section 6 names in its own final clause, a one-off rather than an instrument. What is recorded is therefore a HISTORICAL OBSERVATION OF AN EXTINCT CONDITION, not a standing measurement, and it cannot rot in section 6's sense because it asserts nothing about the current tree. Without this sentence a reader concludes the producer was omitted rather than impossible, which is why the absence is declared instead of left to be noticed. **THE POPULATION ON MAIN IS UNMEASURED AND THE ROW DOES NOT CLAIM OTHERWISE, WHICH IS A DENOMINATOR FACT AND NOT BOOKKEEPING** (established 2026-09-06, after this row was first written, by the three-cell probe that identified what builds the chain). THE SOLE SPECIMEN WAS PRODUCED BY A RESOLVER RULE THAT IS NOT PRESENT ON MAIN: admitting the one refused callable owner collapses the specimen from 1,800,008 to 85, with the deepest site moving to an unrelated module, and the same instrument reads 85 under main and under the merge base. **THE TWO LEVELS ARE CONDITIONAL OBSERVATIONS AND MUST NOT BE LIFTED OUT AS PROPERTIES OF "MAIN" AND "THE CUT".** They were measured under one fixed execution condition -- that corpus, that traversal order, that pool construction, that binary and instrumentation -- and the pool construction in force is itself order-dependent, so the absolute levels are traversal-order-contaminated. WHAT GENERALISES IS THE DISCRIMINATING EFFECT OF CHANGING THE PREDICATE, not the numbers: a defective traversal regime can move the absolute state presented to every cell alike, but it cannot manufacture a DIFFERENCE between cells when that regime was held fixed. So the collapse stands as causal evidence with its held condition attached, and 85 is not a fact about main. **WHETHER ORDINARY CORPUS GROWTH ALONE CAN REACH COMPARABLE DEPTH IS UNMEASURED, AND NOBODY HAS SHOWN THAT IT CAN.** THE PRODUCING DEFECT IS NAMED SO THE TWO ROWS CONNECT RATHER THAN LEAVING THE NEXT READER TO RE-DERIVE IT: the depth was reached because an UNRESOLVABLE CALL WAS ELABORATED RATHER THAN REFUSED, which is filed as the call-site form of `gunbc.recurring_failure_mode.state_space_conflation` -- the callable-lookup carrier collapses builtin, locally-bound and genuinely-missing into one constructor, and the consumer reads that collapsed absence as affirmative formal authority. **STATED IN BOTH DIRECTIONS, BECAUSE EACH HALF GUARDS AGAINST THE OPPOSITE MISREAD.** A reader must not conclude that corpus growth alone reaches this depth -- that is the unmeasured half above. A reader must ALSO not conclude that the structure was a harness artefact: NOTHING WAS FORCED IN THE RUN THAT PRODUCED IT. The 1,800,008 baseline is an ordinary compile under an ordinary resolver rule; the forced admissions were the two PROBES placed either side of that baseline to identify its cause. The structure was real, an accepted compile built it, and the class it exhibits is independent of whichever defect supplied the depth -- which is why this row stands on its own and does not wait on that defect's repair. **THE SECOND DEFECT THIS SPECIMEN EXPOSES IS NOT THIS ROW AND MUST NOT BE ABSORBED INTO IT:** nothing in two source files is 10^5 levels deep, so some pipeline stage BUILDS a structure far deeper than its input -- a chain where a flat structure was intended. That is a separate defect, for which this class is only the reporter, and it will be pathological for every consumer that walks the structure rather than only the one that releases it.) - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. REPAIR AND ITS OWN LIMIT: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. A leaf that is not on the roster and resolves nowhere is UNRESOLVED, a different fact, reported `UndecidableFormalUnresolved`. NEXT-RUNG TRIGGER for the residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) diff --git a/src/v1/stage0/src/v1_compiler_infer_env.rs b/src/v1/stage0/src/v1_compiler_infer_env.rs index ca167b72ba9..b950bd34fb7 100644 --- a/src/v1/stage0/src/v1_compiler_infer_env.rs +++ b/src/v1/stage0/src/v1_compiler_infer_env.rs @@ -1790,7 +1790,7 @@ pub fn declaration_substitution_basis( let generic_leaf = ((((n.connective.clone() == Connective::NoConnective) && ((n.children.clone().len() as i64) == 0)) && (name.clone() != "".to_string())) - && ({ + && { let mut __found = false; for g in generic_names.iter().cloned() { if (g.clone() == name.clone()) { @@ -1799,10 +1799,7 @@ pub fn declaration_substitution_basis( } } __found - } || ((!v1_rt::contains(name.clone(), ".".to_string()) - && !crate::std_types::is_kernel_type(name.clone())) - && (lookup_binding_by_name_local(env.clone(), name.clone()) - == std::option::Option::None)))); + }); if generic_leaf.clone() { node_with_inferred( with_children.clone(), diff --git a/src/v1/stage0/src/v1_compiler_infer_lookup.rs b/src/v1/stage0/src/v1_compiler_infer_lookup.rs index 2e1f41289d0..2a8fcc7e751 100644 --- a/src/v1/stage0/src/v1_compiler_infer_lookup.rs +++ b/src/v1/stage0/src/v1_compiler_infer_lookup.rs @@ -684,40 +684,6 @@ pub fn borrowed_census_callable_candidate( } } -pub fn declaration_unbound_leaf_names(n: Rc, env: Rc) -> Rc> { - stacker::maybe_grow(512 * 1024, 2 * 1024 * 1024, || { - let name = crate::v1_std_core::authored_name_at(env.source_indices.clone(), n.clone()); - let here = if ((((((n.connective.clone() == Connective::NoConnective) - && ((n.children.clone().len() as i64) == 0)) - && (name.clone() != "".to_string())) - && !v1_rt::contains(name.clone(), ".".to_string())) - && !crate::std_types::is_kernel_type(name.clone())) - && (crate::v1_compiler_infer_env::lookup_binding_by_name_local( - env.clone(), - name.clone(), - ) == std::option::Option::None)) - { - Rc::new(vec![name.clone()]) - } else { - Rc::new(vec![]) - }; - v1_rt::concat( - here.clone(), - Rc::new({ - let mut __result = Vec::new(); - for ch in n.children.clone().iter().cloned() { - __result.extend( - (*declaration_unbound_leaf_names(ch.clone(), env.clone())) - .iter() - .cloned(), - ); - } - __result - }), - ) - }) -} - pub fn census_declaration_bound_formals( type_env: Rc, owner_module_path: String, @@ -734,35 +700,9 @@ pub fn census_declaration_bound_formals( tp_names.clone(), type_env.source_indices.clone(), ); - let return_type = match node.inferred.clone().as_deref().cloned() { - Some(InferredNode::Resolved { - node: resolved_return, - .. - }) => resolved_return.clone(), - _ => match node.type_annotation.clone() { - Some(annotated_return) => annotated_return.clone(), - std::option::Option::None => error_type(), - }, - }; - let declaration_generic_names = v1_rt::concat( - tp_names.clone(), - v1_rt::concat( - declaration_unbound_leaf_names(return_type.clone(), declaration_env.clone()), - Rc::new({ - let mut __result = Vec::new(); - for p in node.params.clone().iter().cloned() { - __result.extend( - (*declaration_unbound_leaf_names( - crate::v1_std_core::param_node_type_expr(p.clone()), - declaration_env.clone(), - )) - .iter() - .cloned(), - ); - } - __result - }), - ), + let declaration_generic_names = crate::v1_compiler_infer_env::borrowed_generic_param_names( + node.params.clone(), + type_env.source_indices.clone(), ); Rc::new({ let mut __result = Vec::new(); @@ -813,7 +753,7 @@ pub fn census_declaration_bound_formals( crate::v1_compiler_infer_env::declaration_substitution_basis( declared_type.clone(), declaration_env.clone(), - declaration_generic_names.clone(), + Rc::new(v1_rt::map_keys(&declaration_generic_names)), ), }) }); From ec6783fbaa9b47896a6121d5b5c77680a5e1ffe5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 07:44:16 +0000 Subject: [PATCH 05/17] Refinement inhabitance: widening admits, introduction declines, from one chain Removing the generic-formal stamp made a question reachable that had never been put: a value whose type sits on the same refinement chain as its declared position. Measured the moment the stamp came out, two corpus sites refused -- HostIdentity flowing into a NonEmptyStr formal, in dag/test/claim/ci/ ci_deploy_target_host_witness_test.dag -- which is widening to its own declared base and is correct code. v1.compiler.infer declared_type_conformance_note had already measured that exact class from the other side and classified it as correct code falsely refused. Two causes, both fixed here. nominal_product_head_name_if_declared_product read a where-refinement as a nominal product: `NonEmptyStr = String where non_empty` carries connective Conj with one child, which is also the shape of a one-field record, so the bare Conj-with-children test admitted refinements to an arm whose contract is "concrete named products and their transparent aliases". is_where_refinement_type already existed to tell them apart and is now consulted. refinement_inhabitance decides the pair from where_refinement_chain -- the peel authority peel_where_refinement_base already consumes, so this adds a relation over the existing single authority and not a second peel. Widening (the produced type carries the declared one on its chain) INHABITS. The other two arms decline. WHY NARROWING DECLINES RATHER THAN REFUSING, and this is a measurement. std's brand prose refuses narrowing, and the first build of this relation did too: 10 corpus refusals became 4928, of which 3870 were a plain String reaching a NonEmptyStr formal. That is not four thousand defects. Refinement values are introduced by literal elaboration and declared casts, and a produced node no longer carries which introduction made it, so the type pair does not settle the question and refusing on it would fabricate a verdict in the direction DESIGN section 5 forbids exactly as firmly as fabricating a success. The pair is reported UndecidableRefinementIntroduction: located, per-reason, countable, so the deficit can rank. Next-rung trigger: the refinement-introduction authority reaching this seam, carried on the produced node. nominal_opaque is not touched: `type Secret nominal_opaque = String` is not a where-refinement, its chain is one link, and the relation returns absent for it -- Secret does not ground to String, which is the wall that form exists to provide. Measured, same tree, locally built binaries frozen before running, partitioned by site identity: the refusal set is IDENTICAL to main's -- none gained, none lost -- while generic-formal declines fall 13643 to 5078 and 4920 pairs reach the new typed refinement decline. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_infer.dag | 140 +++++++++++++++-- src/v1/stage0/src/v1_compiler_infer.rs | 204 +++++++++++++++++++++---- 2 files changed, 303 insertions(+), 41 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index ce6c134cb3a..3e418782541 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3269,6 +3269,7 @@ type InhabitanceUndecidableReason | UndecidableOptionalCarrier | UndecidableFormalUnresolved | UndecidableProducedIdentityErased + | UndecidableRefinementIntroduction type InhabitanceRefusalReason = RefusedPayloadAtParent @@ -3276,6 +3277,7 @@ type InhabitanceRefusalReason | RefusedDistinctProductConstructor | RefusedDistinctAppliedTypeArgument + type InhabitanceVerdict = Inhabits | InhabitanceRefused { reason: InhabitanceRefusalReason } @@ -3300,6 +3302,91 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) } } +// REFINEMENT INHABITANCE, DECIDED FROM THE CHAIN AND IN BOTH DIRECTIONS BY ONE AUTHORITY. +// +// std.types declares refinements in layers -- NonEmptyStr = String where non_empty, +// PathSegment = NonEmptyStr where brand("PathSegment"), Char = Int where unicode_scalar, +// brand("Char") -- so a refinement pair is not two unrelated names, it is two positions on one +// chain, and which position each side occupies is the whole verdict. std states the direction it +// cares about on the RenderedTerminalText declaration: a raw stdout pipe cannot inhabit the brand, +// so feeding one to a parser that requires it is a type error. That is NARROWING refused. It says +// nothing against widening, and the PathSegment note reasons about a branded NonEmptyStr as +// though it simply is one. +// +// ONE RELATION, EVERY DIRECTION, DELIBERATELY. Deciding widening in one predicate and the other +// directions in another lets them drift apart, and only one would carry a test. All three arms +// are read off where_refinement_chain rather than off any particular pair, so a brand over Int +// decides the same way a brand over NonEmptyStr does and a two-level chain decides the same way a +// one-level chain does. +// +// THE NARROWING DIRECTION DECLINES, AND THAT IS A MEASUREMENT, NOT A PREFERENCE. std's brand +// prose refuses narrowing, and the first build of this relation refused it here -- which turned +// 10 corpus refusals into 4928, of which 3870 were a plain String reaching a NonEmptyStr formal. +// That is not four thousand defects. Refinement values are INTRODUCED through literal elaboration +// and declared casts, and by the time a produced node reaches this seam it no longer carries +// which introduction produced it. So "the produced type sits at or above the declared refinement" +// does not settle inhabitance, and refusing on it would fabricate a verdict in the direction +// DESIGN section 5 forbids just as firmly as fabricating a success. The pair is reported +// UndecidableRefinementIntroduction: located, per-reason and countable, so the deficit can rank. +// NEXT-RUNG TRIGGER: the refinement-introduction authority reaching this seam -- the elaboration +// or declared cast that produced the value, carried on the produced node -- at which point this +// arm refuses narrowing instead of declining it. +// +// WHY IT IS REACHABLE ONLY NOW. Every site this relation answers had its declared side rewritten +// into a generic formal before any arm ran, so the refinement question was never put. Measured on +// the corpus at the moment that stamp was removed: HostIdentity flowing into a NonEmptyStr formal +// -- widening to its own declared base, correct code -- refused as a distinct product +// constructor. This is the arm that state was hiding, not a widening of scope. +fn refinement_chain_names(n: Node, scope: InferScope) -> List { + let source_indices = scope.type_env.source_indices + let name = authored_name_at(source_indices: source_indices, node: n) + if name == "" { + [] + } else { + match lookup_type_by_name(env: scope.type_env, name: name) { + Present { value: decl } => + where_refinement_chain(ty: decl, type_env: scope.type_env) + |> map(link => qualified_last_segment(name: authored_name_at(source_indices: source_indices, node: link))) + |> filter(link_name => link_name != "") + Absent => [qualified_last_segment(name: name)] + } + } +} + +type RefinementInhabitance + = RefinementWidensToDeclaredBase + | RefinementNarrowsToDeclaredBrand + | RefinementSiblingBrands + +// ABSENT MEANS "NOT THIS RELATION'S SUBJECT", NEVER "COMPATIBLE". Every guard hands the pair back +// to the arms below rather than admitting it, so this can only convert a silence into a decision +// for a pair whose two chains are both established and actually meet. +fn refinement_inhabitance(declared: Node, produced: Node, scope: InferScope) -> RefinementInhabitance? { + let declared_chain = refinement_chain_names(n: declared, scope: scope) + let produced_chain = refinement_chain_names(n: produced, scope: scope) + match declared_chain |> first { + Absent => none + Present { value: declared_head } => + match produced_chain |> first { + Absent => none + Present { value: produced_head } => + if declared_head == produced_head { + none + } else if (declared_chain |> count) <= 1 && (produced_chain |> count) <= 1 { + none + } else if produced_chain |> any(link => link == declared_head) { + Present { value: RefinementWidensToDeclaredBase } + } else if declared_chain |> any(link => link == produced_head) { + Present { value: RefinementNarrowsToDeclaredBrand } + } else if declared_chain |> any(d => produced_chain |> any(p => p == d)) { + Present { value: RefinementSiblingBrands } + } else { + none + } + } + } +} + // THE SINGLE DECISION PROCEDURE. It CONSUMES the established predicates rather than restating // them: coproduct_payload_where_parent_required already peels transparent aliases through // transparent_alias_identity_agrees, so alias identity is decided in exactly one place in the @@ -3332,16 +3419,26 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } } else if coproduct_at_record_declared_type(declared: declared, produced: produced, scope: scope) { InhabitanceRefused { reason: RefusedKernelAtStructured } - } else if kernel_value_declared_type_mismatch( - formal: declared, actual: produced, - type_env: scope.type_env, source_indices: source_indices) { - InhabitanceRefused { reason: RefusedKernelAtStructured } - } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { - InhabitanceRefused { reason: RefusedPayloadAtParent } } else { - match nominal_product_inhabitance_refusal(declared: declared, produced: produced, scope: scope) { - Present { value: r } => InhabitanceRefused { reason: r } - Absent => Inhabits + match refinement_inhabitance(declared: declared, produced: produced, scope: scope) { + Present { value: RefinementWidensToDeclaredBase } => Inhabits + Present { value: RefinementNarrowsToDeclaredBrand } => + InhabitanceUndecidable { reason: UndecidableRefinementIntroduction } + Present { value: RefinementSiblingBrands } => + InhabitanceUndecidable { reason: UndecidableRefinementIntroduction } + Absent => + if kernel_value_declared_type_mismatch( + formal: declared, actual: produced, + type_env: scope.type_env, source_indices: source_indices) { + InhabitanceRefused { reason: RefusedKernelAtStructured } + } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { + InhabitanceRefused { reason: RefusedPayloadAtParent } + } else { + match nominal_product_inhabitance_refusal(declared: declared, produced: produced, scope: scope) { + Present { value: r } => InhabitanceRefused { reason: r } + Absent => Inhabits + } + } } } } @@ -3545,6 +3642,26 @@ fn nominal_product_head_name(n: Node, scope: InferScope) -> String { } } +// A WHERE-REFINEMENT IS NOT A NOMINAL PRODUCT, and the Conj test alone cannot tell them apart. +// `type NonEmptyStr = String where non_empty` and `type HostIdentity = NonEmptyStr where +// brand("HostIdentity")` both carry connective Conj with one child, which is the shape a +// one-field record also has -- so the bare Conj-with-children test admitted them to the +// nominal-product arm, where two distinct refinement names disagree and the pair refuses. +// Measured on the corpus: HostIdentity flowing into a NonEmptyStr formal, which is WIDENING TO +// ITS OWN DECLARED BASE and is correct code, refused as RefusedDistinctProductConstructor. +// +// WHY THE EXCLUSION IS THE HONEST FIX RATHER THAN A WIDENING. This arm's own contract is +// "concrete named products and their transparent aliases", and it names the shapes it does not +// handle rather than implying coverage. A where-refinement is a fourth such shape: deciding it +// needs the refinement CHAIN and its direction -- widening to a base admits, narrowing to a +// brand must not -- which is a different judgment with a different authority +// (where_refinement_chain), not a case of this one. Refusing it here would fabricate a verdict +// from a name comparison that carries no direction at all. It reaches this arm only because the +// declared side used to be stamped a generic formal and declined before any arm ran. +// +// NEXT-RUNG TRIGGER: a refinement-inhabitance relation that consumes where_refinement_chain and +// decides the two directions separately, at which point brand narrowing becomes a refusal here +// rather than an abstention. fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope) -> String { let representative = transparent_alias_representative( index: scope.type_env.symbol_index, name: name) @@ -3552,7 +3669,9 @@ fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope Present { value: decl } => let peeled = peel_nominal_alias_identity( n: decl, env: scope.type_env, module_name: scope.module_name) - if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } + if is_where_refinement_type(ty: peeled) { + "" + } else if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } Absent => "" } } @@ -3735,6 +3854,7 @@ fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape" UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against" UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam" + UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain, and whether it was INTRODUCED at that refinement is carried by the elaboration or declared cast that produced it, not by the type pair at this seam" } } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index aa756d07de4..9c6c38a6b44 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -9,6 +9,7 @@ use self::InhabitanceRefusalReason::*; use self::InhabitanceUndecidableReason::*; use self::InhabitanceVerdict::*; use self::LiteralBoundary::*; +use self::RefinementInhabitance::*; use self::ServiceConfigFieldJudgment::*; pub use crate::extdeps_container_oci_digest::{ oci_other_digest_algorithm, oci_other_digest_encoded, @@ -4584,6 +4585,7 @@ pub enum InhabitanceUndecidableReason { UndecidableOptionalCarrier, UndecidableFormalUnresolved, UndecidableProducedIdentityErased, + UndecidableRefinementIntroduction, } #[derive( @@ -4638,6 +4640,141 @@ pub fn declared_type_position_label(position: DeclaredTypePosition, subject: Str } } +pub fn refinement_chain_names(n: Rc, scope: Rc) -> Rc> { + { + let source_indices = scope.type_env.clone().source_indices.clone(); + let name = crate::v1_std_core::authored_name_at(source_indices.clone(), n.clone()); + if (name.clone() == "".to_string()) { + Rc::new(vec![]) + } else { + match crate::v1_compiler_infer_env::lookup_type_by_name( + scope.type_env.clone(), + name.clone(), + ) { + Some(decl) => Rc::new({ + let mut __result = Vec::new(); + for link_name in Rc::new({ + let mut __result = Vec::new(); + for link in where_refinement_chain(decl.clone(), scope.type_env.clone()) + .iter() + .cloned() + { + __result.push(crate::v1_std_core::qualified_last_segment( + crate::v1_std_core::authored_name_at( + source_indices.clone(), + link.clone(), + ), + )); + } + __result + }) + .iter() + .cloned() + { + if (link_name.clone() != "".to_string()) { + __result.push(link_name); + } + } + __result + }), + std::option::Option::None => { + Rc::new(vec![crate::v1_std_core::qualified_last_segment( + name.clone(), + )]) + } + } + } + } +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum RefinementInhabitance { + RefinementWidensToDeclaredBase, + RefinementNarrowsToDeclaredBrand, + RefinementSiblingBrands, +} + +pub fn refinement_inhabitance( + declared: Rc, + produced: Rc, + scope: Rc, +) -> Option { + { + let declared_chain = refinement_chain_names(declared.clone(), scope.clone()); + let produced_chain = refinement_chain_names(produced.clone(), scope.clone()); + match declared_chain.clone().first().cloned() { + std::option::Option::None => std::option::Option::None, + Some(declared_head) => match produced_chain.clone().first().cloned() { + std::option::Option::None => std::option::Option::None, + Some(produced_head) => { + if (declared_head.clone() == produced_head.clone()) { + std::option::Option::None + } else { + if (((declared_chain.clone().len() as i64) <= 1) + && ((produced_chain.clone().len() as i64) <= 1)) + { + std::option::Option::None + } else { + if { + let mut __found = false; + for link in produced_chain.iter().cloned() { + if (link.clone() == declared_head.clone()) { + __found = true; + break; + } + } + __found + } { + Some(RefinementInhabitance::RefinementWidensToDeclaredBase) + } else { + if { + let mut __found = false; + for link in declared_chain.iter().cloned() { + if (link.clone() == produced_head.clone()) { + __found = true; + break; + } + } + __found + } { + Some(RefinementInhabitance::RefinementNarrowsToDeclaredBrand) + } else { + if { + let mut __found = false; + for d in declared_chain.iter().cloned() { + if { + let mut __found = false; + for p in produced_chain.iter().cloned() { + if (p.clone() == d.clone()) { + __found = true; + break; + } + } + __found + } { + __found = true; + break; + } + } + __found + } { + Some(RefinementInhabitance::RefinementSiblingBrands) + } else { + std::option::Option::None + } + } + } + } + } + } + }, + } + } +} + pub fn declared_type_inhabitance( obligation: Rc, scope: Rc, @@ -4712,41 +4849,33 @@ pub fn declared_type_inhabitance( InhabitanceRefusalReason::RefusedKernelAtStructured, }) } else { - if kernel_value_declared_type_mismatch( - declared.clone(), - produced.clone(), - scope.type_env.clone(), - source_indices.clone(), - ) { + match refinement_inhabitance(declared.clone(), produced.clone(), scope.clone()) { + Some(RefinementInhabitance::RefinementWidensToDeclaredBase) => Rc::new(InhabitanceVerdict::Inhabits), + Some(RefinementInhabitance::RefinementNarrowsToDeclaredBrand) => Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableRefinementIntroduction, +}), + Some(RefinementInhabitance::RefinementSiblingBrands) => Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableRefinementIntroduction, +}), + std::option::Option::None => if kernel_value_declared_type_mismatch(declared.clone(), produced.clone(), scope.type_env.clone(), source_indices.clone()) { Rc::new(InhabitanceVerdict::InhabitanceRefused { reason: InhabitanceRefusalReason::RefusedKernelAtStructured, }) } else { - if coproduct_payload_where_parent_required( - declared.clone(), - produced.clone(), - scope.clone(), - ) { + if coproduct_payload_where_parent_required(declared.clone(), produced.clone(), scope.clone()) { Rc::new(InhabitanceVerdict::InhabitanceRefused { reason: InhabitanceRefusalReason::RefusedPayloadAtParent, }) } else { - match nominal_product_inhabitance_refusal( - declared.clone(), - produced.clone(), - scope.clone(), - ) { - Some(r) => Rc::new( - InhabitanceVerdict::InhabitanceRefused { - reason: r.clone(), - }, - ), - std::option::Option::None => { - Rc::new(InhabitanceVerdict::Inhabits) - } - } + match nominal_product_inhabitance_refusal(declared.clone(), produced.clone(), scope.clone()) { + Some(r) => Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: r.clone(), +}), + std::option::Option::None => Rc::new(InhabitanceVerdict::Inhabits), +} } - } + }, +} } } } @@ -4972,12 +5101,16 @@ pub fn nominal_product_head_name_if_declared_product( scope.type_env.clone(), scope.module_name.clone(), ); - if ((peeled.connective.clone() == Connective::Conj) - && ((peeled.children.clone().len() as i64) > 0)) - { - name.clone() - } else { + if is_where_refinement_type(peeled.clone()) { "".to_string() + } else { + if ((peeled.connective.clone() == Connective::Conj) + && ((peeled.children.clone().len() as i64) > 0)) + { + name.clone() + } else { + "".to_string() + } } } std::option::Option::None => "".to_string(), @@ -5153,6 +5286,7 @@ pub fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason InhabitanceUndecidableReason::UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape".to_string(), InhabitanceUndecidableReason::UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against".to_string(), InhabitanceUndecidableReason::UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam".to_string(), + InhabitanceUndecidableReason::UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain, and whether it was INTRODUCED at that refinement is carried by the elaboration or declared cast that produced it, not by the type pair at this seam".to_string(), } } @@ -26561,6 +26695,8 @@ pub struct UndecidableFormalUnresolved; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct UndecidableProducedIdentityErased; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableRefinementIntroduction; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedPayloadAtParent; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedKernelAtStructured; @@ -26568,3 +26704,9 @@ pub struct RefusedKernelAtStructured; pub struct RefusedDistinctProductConstructor; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedDistinctAppliedTypeArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefinementWidensToDeclaredBase; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefinementNarrowsToDeclaredBrand; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefinementSiblingBrands; From 97cdc102b3481436be9b3cf8b216a4842a574d56 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 08:04:23 +0000 Subject: [PATCH 06/17] Correct the refinement-decline premise: an explicit cast IS visible at this seam The first account of why narrowing declines said the produced node no longer carries which introduction made it. An executed check refutes that half. dag/test/fixture/compile_phase_frontier_receipt_fixture calls sha256_digest(hex: "..." as NonEmptyStr) -- a String literal at a refinement formal, carrying an explicit cast -- and this relation produces NO diagnostic for it at all. Its four diagnostics are optional-carrier and nothing else. Meanwhile every site that does decline is a bare literal handed straight to a refinement formal with no cast: "feedFwdOffsetCoeff" at a NonEmptyStr, 168 at a numeric refinement, "declaration-worker" at a NonEmptyStr. So one of the two introduction forms is already read here, and the blanket claim was wrong. The remaining form is literal elaboration at the declared boundary, which std.literal_elaboration owns and this relation does not consult -- the same shape the numeric-realization note in this file already records, where the class was never undecidable, it was UNCONSULTED. Declining is still right, because refusing on a fact one is declining to look up fabricates a verdict; but the trigger is now named at the capability that actually decides it: the elaboration verdict for a literal at its destination refinement reaching this seam on the produced node. Annotation and the reported reason both corrected. No behaviour change. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_infer.dag | 37 +++++++++++++++++--------- src/v1/stage0/src/v1_compiler_infer.rs | 2 +- 2 files changed, 25 insertions(+), 14 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 3e418782541..118cbc394cb 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3319,18 +3319,29 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // decides the same way a brand over NonEmptyStr does and a two-level chain decides the same way a // one-level chain does. // -// THE NARROWING DIRECTION DECLINES, AND THAT IS A MEASUREMENT, NOT A PREFERENCE. std's brand -// prose refuses narrowing, and the first build of this relation refused it here -- which turned -// 10 corpus refusals into 4928, of which 3870 were a plain String reaching a NonEmptyStr formal. -// That is not four thousand defects. Refinement values are INTRODUCED through literal elaboration -// and declared casts, and by the time a produced node reaches this seam it no longer carries -// which introduction produced it. So "the produced type sits at or above the declared refinement" -// does not settle inhabitance, and refusing on it would fabricate a verdict in the direction -// DESIGN section 5 forbids just as firmly as fabricating a success. The pair is reported -// UndecidableRefinementIntroduction: located, per-reason and countable, so the deficit can rank. -// NEXT-RUNG TRIGGER: the refinement-introduction authority reaching this seam -- the elaboration -// or declared cast that produced the value, carried on the produced node -- at which point this -// arm refuses narrowing instead of declining it. +// THE NARROWING DIRECTION DECLINES, AND BOTH HALVES OF THAT ARE MEASURED, NOT REASONED. +// std's brand prose refuses narrowing, and the first build of this relation refused it here -- +// which turned 10 corpus refusals into 4928, every one of them a base value at a refinement +// formal, 3870 of those a plain String at a NonEmptyStr formal. That is not four thousand +// defects, so the refusal was withdrawn and the pair is declined instead. +// +// WHAT THE DECLINE IS AND IS NOT, because the first account of it was wrong and the check that +// refuted it is cheap. It is NOT that introduction is uncarried: an EXPLICIT CAST IS ALREADY +// VISIBLE HERE. dag/test/fixture/compile_phase_frontier_receipt_fixture calls +// sha256_digest(hex: "..." as NonEmptyStr) at a refinement formal and produces no diagnostic from +// this relation at all, while the sites that do decline are bare literals -- "feedFwdOffsetCoeff", +// 168, "declaration-worker" -- handed straight to a refinement formal with no cast. So the +// discriminating fact exists and the seam already reads one of its two forms. +// +// The remaining form is LITERAL ELABORATION at the declared boundary, which std.literal_elaboration +// owns and this relation does not consult -- the same shape the numeric note above records, where +// the class was never undecidable, it was unconsulted. Refusing on a fact one is declining to look +// up would fabricate a verdict in the direction DESIGN section 5 forbids as firmly as fabricating +// a success, so the pair is reported UndecidableRefinementIntroduction: located, per-reason and +// countable, so the deficit ranks instead of vanishing. +// NEXT-RUNG TRIGGER: the elaboration verdict for a literal at its destination refinement reaching +// this seam on the produced node, at which point this arm refuses an unelaborated base value at a +// refinement formal instead of declining it. // // WHY IT IS REACHABLE ONLY NOW. Every site this relation answers had its declared side rewritten // into a generic formal before any arm ran, so the refinement question was never put. Measured on @@ -3854,7 +3865,7 @@ fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape" UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against" UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam" - UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain, and whether it was INTRODUCED at that refinement is carried by the elaboration or declared cast that produced it, not by the type pair at this seam" + UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain and carries no cast to it, so whether it was INTRODUCED at that refinement is the literal-elaboration verdict for its destination, which this seam does not consult" } } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 9c6c38a6b44..127862c9192 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -5286,7 +5286,7 @@ pub fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason InhabitanceUndecidableReason::UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape".to_string(), InhabitanceUndecidableReason::UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against".to_string(), InhabitanceUndecidableReason::UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam".to_string(), - InhabitanceUndecidableReason::UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain, and whether it was INTRODUCED at that refinement is carried by the elaboration or declared cast that produced it, not by the type pair at this seam".to_string(), + InhabitanceUndecidableReason::UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain and carries no cast to it, so whether it was INTRODUCED at that refinement is the literal-elaboration verdict for its destination, which this seam does not consult".to_string(), } } From 2bc8190daca9c5d25a0dac7445c155835a718b52 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 08:42:53 +0000 Subject: [PATCH 07/17] Record why the sibling arm declines: the brand wall already exists Two measurements, one section 3 answer, no behaviour change (annotations are erased from the semantic projection, so the stage0 mirror is unchanged). FIRST, the refinement-introduction trigger is not speculative. An empty string literal handed to a NonEmptyStr formal compiles with NO diagnostic from anything in the tree. So the 4875 sites this relation newly declines are real unchecked refinement introductions -- the predicate is not verified at introduction today, and this relation is the first thing that makes the population visible, located and countable. SECOND, the horizontal case is already walled and must not be walled twice. where_refinement_brand_nominal_verdict, reached through where_refinement_mismatch_diags on the expected-type path, compares brand DECLARATION SITES rather than spellings and refuses BrandNominalDistinctDeclarations. Refusing sibling pairs in this relation as well would be a second authority for one judgment. It would also be wrong at this grain, measured rather than reasoned: refusing every sibling pair produced FilePath at a NonEmptyStr formal, GcpProjectId at a NonEmptyStr formal and Sha512DigestHex at a NonEmptyStr formal -- peer predicate refinements over the same base carrying no conflicting brand at all, whose chains fail to nest only because each is declared over String directly rather than over NonEmptyStr. A sibling relation is not a brand conflict, and only the brand authority can tell the two apart. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_infer.dag | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 118cbc394cb..123ccbe5521 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3341,7 +3341,21 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // countable, so the deficit ranks instead of vanishing. // NEXT-RUNG TRIGGER: the elaboration verdict for a literal at its destination refinement reaching // this seam on the produced node, at which point this arm refuses an unelaborated base value at a -// refinement formal instead of declining it. +// refinement formal instead of declining it. The trigger is not speculative: an empty string +// literal handed to a NonEmptyStr formal compiles with no diagnostic from anything in the tree, +// so the predicate is genuinely unchecked at introduction today. +// +// THE SIBLING ARM DECLINES TOO, AND THAT IS A SECTION 3 ANSWER RATHER THAN A GAP. Two refinements +// that share a base without either being the other's ancestor look like the horizontal case brands +// exist to refuse -- but DISTINCT BRAND DECLARATIONS ARE ALREADY WALLED, by +// where_refinement_brand_nominal_verdict through where_refinement_mismatch_diags, which compares +// brand DECLARATION SITES rather than spellings and refuses BrandNominalDistinctDeclarations. +// Refusing here as well would be a second authority for one judgment. It would also be wrong at +// this grain, and that was measured rather than reasoned: refusing every sibling pair turned up +// FilePath at a NonEmptyStr formal, GcpProjectId at a NonEmptyStr formal, Sha512DigestHex at a +// NonEmptyStr formal -- peer predicate refinements over the same base, carrying no conflicting +// brand at all, whose chains fail to nest only because each is declared over String directly. A +// sibling relation is not a brand conflict, and only the brand authority can tell them apart. // // WHY IT IS REACHABLE ONLY NOW. Every site this relation answers had its declared side rewritten // into a generic formal before any arm ran, so the refinement question was never put. Measured on From e2674dfe11ff5d26f51ae72c265f0aa5c84c451d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 7 Sep 2026 10:09:39 +0000 Subject: [PATCH 08/17] chore: regenerate drifted generated artifacts (ci auto-heal) Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md lookup_miss_read_as_positive_classification Ledger-Repair-Judged: docs/design-rung-drops.md --- docs/design-failure-modes.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 3af32b45425..d8df52008de 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -170,6 +170,7 @@ The exact `RecurringFailureMode.identity` population, which no other projection - `evaluation_model_cleanup_undeclared` - `docs_markdown_projections_have_no_completing_actuator` - `type_name_field_carries_rendered_value` +- `lookup_miss_read_as_positive_classification` --- @@ -355,3 +356,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. - **generated `docs/*.md` ledger projections have no ProcessExit actuator and no regen coverage, so an EDIT to a still-present row can sit in the authority, absent from the projection, with every completing instrument green** (INVALID STATE: `gunbc.recurring_failure_mode` is the authority; `docs/design-failure-modes.md` is the projection DESIGN.md points readers at. `expected_design_failure_modes_md` returns `String`. The refusal exits 2 with EMPTY STDOUT and interpolates the rendered value into the diagnostic on stderr: classify_exit's non-variant arm is type_name: ctx.format_value(other). Executed: wise-badger-902, EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown heading; quick-heron-85, proj3.err 1062137 bytes, same delimiters. The enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` forbids print-AND-SUCCEED, and holds. The content is therefore obtainable ONLY by scraping a half-megabyte stderr diagnostic between delimiters that are message prose (returned-open-quote and not-ProcessExit-close-quote), unversioned and enrolled by nothing. Extractable only by scraping an unversioned diagnostic — which is why the ProcessExit regen is the repair. `claim_executor --required-regen` compares only `is_compared_generated_basename` = ends_with .rs into `target/stage0-regen-candidate`. HARM: three rows can be edited in `.dag` after the last projection and nothing that exits 0 will say the markdown is stale. The meaning-fork in the field named type_name is a separate row, `type_name_field_carries_rendered_value`, not this class. SPECIMEN, measured by another lane while regenerating the projection, 2026-09-06: `instrument_answers_outside_its_domain`, `stale_claim_survives_its_own_correct_edit`, and `native_stack_recursion_unbounded_over_corpus_shaped_structure` had been edited in their authorities after the doc was last projected and had grown by 2349, 5519 and 1152 characters. Regenerating carried the repairs through. On origin/main as of 3531d30bb82 those three `.dag` files are older than `docs/design-failure-modes.md` (`81686f7bea8`), so CURRENT main is not claimed still stale; the class is that nothing completing could have said so while they were. SPECIMEN, review 58567 on gunbc#9864, on the host comment above `exit_status_for_class`: a relocation dropped the `status: refused — printing the value and exiting 0 would report success for a run whose outcome is unknown.` sentence while the comment claimed byte-for-byte equivalence. The doc lied, not the code. The sentence was restored rather than the claim weakened. That is this class on a different pair: an authority and its projection disagreeing with nothing completing to say so, and a real specimen rather than an injected literal. INCIDENT, not a fixture and not a perturbation ordered for this PR, produced by quick-heron-85 without looking for this class, commit b1c6378c6d: their authority row unresolved_callee_conflated_with_dispatched_elsewhere was UNPARSEABLE for a full commit. An authored receipt contained a quoted phrase using bare double quotes inside a double-quoted string; the string terminated early and the parser refused undefined variable this and undefined variable leaf. THE AUTHORITY DID NOT COMPILE, so docs/design-failure-modes.md kept rendering the previous vintage while presenting as current. They found it only by running the projection; reading the row does not surface the break. This PR's gate would go red on that commit because an unparseable authority makes the projector refuse — from the committed markdown alone, STALE bytes and an UNBUILDABLE authority are indistinguishable. THIS ROW IS THE DETECTOR GAP. The quoting injury that silently disabled the row they were filing is a neighbouring class they are filing separately; its next-rung trigger is string escaping in the .dag lexer. This gate makes that injury loud; it does not make it unwritable. Do not read this row as closing that class. THE IDENTITY-JOIN CORRECTION, which is the transferable part and which corrects a rule this project holds. Completeness is an identity join, not a count equality — and AN IDENTITY JOIN OVER ROW NAMES WOULD HAVE REPORTED THAT FILE COMPLETE AND CORRECT: every identity present, none missing, none extra. The drift was pure EDIT. Only a regenerated byte diff sees an edit. Worse: a first pass comparing line SETS read the three as REORDERINGS, because the changed rows shared an 80-character prefix with their old text, so the cheap check does not merely miss the drift, it manufactures a benign explanation for it. An identity join proves MEMBERSHIP, not CONTENT. THE TWO NEIGHBOURS THIS IS NOT. `authority_merges_unprotected_while_its_projection_is_guarded` is MERGE POLARITY: the generated projection is driver-bound while the hand-authored authority is not. Adjacent files, distinct defect — this row is the absence of a completing actuator or content gate, reachable with no merge in sight. `green_reported_over_a_population_the_instrument_does_not_own` is a split of actuators whose GREEN is read as covering the half it does not enumerate; that climb joined registry-projections to stage0-mirrors inside one required phase, and still does not give `gunbc run` a ProcessExit projector for the markdown, nor put `.md` in `--required-regen`. RECOGNITION RULE: when a generated file is what readers are pointed at, ask (1) whether any `ProcessExit` entry writes those exact bytes and exits 0, (2) whether regen's compared population includes that path, and (3) whether the gate compares CONTENT, not row-name membership. A complete identity set of names is not a content agreement. RUNG FOUND AT: outside the ladder until a completing content agreement exists — silent wrongness, not a weak wall. After a ProcessExit projector and a required content compare execute, mechanically preventable: the stale file remains writable. CEILING: structurally guaranteed when membership of every committed generated `docs/` path in a content-agreement adjudicator is derived from `gunbc.generated_artifact` `committed_generated_artifacts`, so omitting the arm is a compile refusal. NEXT-RUNG TRIGGER, a capability: required-run dispatch consumes a content agreement — byte identity of generated vs committed — over every committed generated artifact whose location directory is `docs`, derived from the registry so adding a committed `docs/` path without that agreement will not compile. A trigger naming one command, one test file, or `docs_projection_gate.dag` is less than the capability and would fire while edit-only drift can still sit uncompared.) - **a field named type_name holds a type name on three arms and a fully rendered value on the fourth** (INVALID STATE: ExitClass::NotProcessExit is one spelling whose payload field is called type_name. `classify_exit` Variant arms that are not ProcessExit put ctx.resolve of the variant type symbol, or ProcessExit plus the unknown variant, into it — an actual type or variant name. The final other arm puts ctx.format_value of the non-variant value — the rendered value — into the same field. `exit_status_for_class` interpolates that field into the returned-quote slot with no second match, so every refusal path reads one name for two facts. HARM: a reader of the interpolation site infers the field's contents from its NAME and concludes a String projector yields the word String; a reader of the producer and a live stderr file concludes the markdown body is in the diagnostic. Both readings of adjacent code are correct; the name is a third surface and it lied. SPECIMEN, 2026-09-06, executed both ways. clever-otter-298 read `exit_status_for_class` and the enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` (which constructs NotProcessExit with a fixture type_name Bool and never goes through `classify_exit`) and asserted the diagnostic names the type. wise-badger-902 read the interpolation site and ruled the same. quick-heron-85 held proj3.err at 1062137 bytes. The manager then RAN the projector: EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown. The field name said type; the field held format_value. WHY THE FORK SURVIVED, and it is a section 4b evidence gap not a naming smell. `non_process_exit_refuses_rather_than_printing_and_succeeding` hand-constructs ExitClass::NotProcessExit with type_name the literal Bool and starts from an already-classified value. It never calls `classify_exit`. Nothing executing joins the field's name to its contents on the non-variant path — the only enrolled evidence feeds the field a literal that matches its name, which is exactly the input that cannot discriminate. The control's RED is unauthorable for this defect, so it was permanently green over the case that mattered and got cited as coverage. A field carrying two facts is ordinary; a field carrying two facts with a control that only ever sees one of them is why three of us read adjacent code correctly and reached three answers. THIS IS NOT `docs_markdown_projections_have_no_completing_actuator`. That row is the absence of a ProcessExit actuator and a content gate over generated `docs/*.md`. This row is a meaning fork inside `ExitClass`, reachable with no docs file in sight. Neighbour `meaning_fork` is the generic class; this instance is filed because the fork sat in the struct every refusal path reads and produced the three-way contradiction. Neighbour `diagnostic_name_mechanism_silent` is a diagnostic NAME silent about its predicate; here the FIELD name is accurate for three arms and false for the fourth. RECOGNITION RULE: when a field is named for a kind of contents, read every constructor, not the interpolation site. If one constructor writes a different kind, the name has forked. RUNG FOUND AT: mitigatable — the wrong inference is a human reading; the runtime still refuses with exit 2 and does not print-and-succeed. CEILING: structurally impossible when `NotProcessExit` cannot be constructed with a rendered value under a field named for a type — two variants, or a field named for what it actually holds. NEXT-RUNG TRIGGER, a capability: `ExitClass` distinguishes a type-name refusal from a rendered-value refusal in the type, so interpolating one as the other will not compile.) +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. REPAIR AND ITS OWN LIMIT: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. A leaf that is not on the roster and resolves nowhere is UNRESOLVED, a different fact, reported `UndecidableFormalUnresolved`. NEXT-RUNG TRIGGER for the residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) From 9e6479a43fce0e3351a3ac59a058fc4a48c12d90 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 11:09:31 +0000 Subject: [PATCH 09/17] Enrol six controls; correct two claims measurement refuted CONTROLS, all measured live on the merged tree before enrolment. Producer grain, the paired mutations that a diagnostic-count drop cannot prove. Both go through the GLOBAL-BARE CENSUS route -- callee named without an import, so it resolves through the corpus census and reaches the producer this repair changed. positive: optional_present still declines UndecidableGenericFormal (1). Silencing borrowed_generic_param_names leaves the leaf unstamped, resolving nowhere, producing NO diagnostic -- the arm reds on zero. negative: sha256_digest_wire_form(digest: Sha256Digest) declines nothing (0). Restoring the local-miss classification in either deleted site stamps TypeVariable { id: "Sha256Digest" } and the arm reds on one. Together they prove both halves: declared implies generic, failed lookup does not. Refinement grain. a branded refinement at its own declared base INHABITS (0 refused, 0 undecided -- the second count is the discriminating half, since zero refusals alone would also hold if the arm merely stopped deciding); two distinct brands over one base are not refused twice: this relation declines and the existing brand wall refuses, measured AT THE DIRECT-CALL ARGUMENT SEAM rather than assumed from the cast path; nominal_opaque does not ground through the chain; a bare literal declines and a cast one does not, at the same formal. TWO CLAIMS OF MINE WITHDRAWN, both refuted by fixtures rather than argued down. The annotation said an explicit cast is not carried at this seam. It is: takes_non_empty(s: "x" as NonEmptyStr) produces nothing from this relation. The annotation then said the predicate goes unchecked at introduction, on a probe that reported no diagnostic for an empty literal. A three-way pair refutes it: takes_non_empty(s: "") is REFUSED by the where-refinement machinery with `type mismatch: expected Product(NonEmptyStr), got Primitive(String)`, while takes_non_empty(s: "x") is admitted by it, and this relation declines both. So the introduction question is ALREADY DECIDED by an authority this relation does not consult -- the same "never undecidable, merely unconsulted" shape the numeric note in this file records. The next-rung trigger is correspondingly cheaper: consult that verdict, not carry a new elaboration fact to the seam. The recurring_failure_mode row asserted that the roster residue reports UndecidableFormalUnresolved. The census moved that population by zero across the repair, so the row now records it as an ASSERTED AND UNEXERCISED boundary. A row is the durable artifact and a disposition nothing executed is specification-without-execution. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- ...p_miss_read_as_positive_classification.dag | 6 ++- ...e_inhabitance_direct_call_witness_test.dag | 53 +++++++++++++++++++ src/v1/04_infer.dag | 38 ++++++------- 3 files changed, 78 insertions(+), 19 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag index c681d6629ec..b7216cafac2 100644 --- a/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag +++ b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag @@ -21,7 +21,11 @@ data lookup_miss_read_as_positive_classification: RecurringFailureMode = Recurri "RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. ", - "REPAIR AND ITS OWN LIMIT: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. A leaf that is not on the roster and resolves nowhere is UNRESOLVED, a different fact, reported `UndecidableFormalUnresolved`. NEXT-RUNG TRIGGER for the residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.)", + "REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. ", + + "THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. ", + + "NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.)", ], evidence: [], diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index 14aba50e346..ec5122875db 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -374,3 +374,56 @@ data nominal_opaque_not_grounded_source: String = "module probe_nominal_opaque_n test fn w_a_nominal_opaque_alias_does_not_ground_through_the_refinement_chain() -> Bool { violation_count(source: nominal_opaque_not_grounded_source, wanted: "DeclaredTypeInhabitanceUndecided") == 0 } + +// THE ROSTER SURVIVED, AND THIS IS THE HALF A DIAGNOSTIC-COUNT DROP CANNOT PROVE. Deleting the +// absence classification lowers the generic-formal population; so does deleting generic +// classification altogether. These two arms are the paired mutations that separate them, and +// neither subsumes the other. Both go through the GLOBAL-BARE CENSUS route -- the callee is named +// without an import, so it resolves through the corpus census and reaches +// census_declaration_bound_formals, which is the producer this repair changed. +// +// POSITIVE: a genuine angle-bracket generic is STILL classified generic. v2.std.optional declares +// fn optional_present(value: T), the parser mints its clause as a param spelled T: T, and +// borrowed_generic_param_names carries it, so the leaf reaches the substitution basis stamped a +// type variable and the seam declines UndecidableGenericFormal. DISCRIMINATING MUTATION: feed +// census_declaration_bound_formals an empty roster and the leaf is unstamped, resolves nowhere, +// and the site produces NO diagnostic at all -- this arm goes red on zero. +data generic_via_global_bare_source: String = "module probe_generic_via_global_bare\nimport std.types { Int }\nfn probe() -> Int {\n match optional_present(value: 1) {\n Present { value: v } => v\n Absent => 0\n }\n}\n" + +test fn w_a_declared_generic_clause_is_still_classified_generic_through_the_census() -> Bool { + violation_count(source: generic_via_global_bare_source, wanted: "DeclaredTypeInhabitanceUndecided") == 1 +} + +// NEGATIVE: a CONCRETE declared leaf is no longer classified generic. std.content_hash declares +// fn sha256_digest_wire_form(digest: Sha256Digest) -> NonEmptyStr; Sha256Digest is an ordinary +// declared type and nothing about it is generic. Before this repair the census declaration +// environment carried no bindings at all, so the local-only lookup missed it and it was enrolled +// as one of that declaration's generic parameters and stamped TypeVariable { id: "Sha256Digest" }, +// and the seam declined. DISCRIMINATING MUTATION: restore the deleted local-miss classification in +// either declaration_unbound_leaf_names or declaration_substitution_basis and this arm goes red on +// one UndecidableGenericFormal. +data concrete_via_global_bare_source: String = "module probe_concrete_via_global_bare\nimport std.content_hash { Sha256Digest }\nimport std.types { NonEmptyStr, Int }\nfn probe(d: Sha256Digest) -> NonEmptyStr { sha256_digest_wire_form(digest: d) }\n" + +test fn w_a_concrete_declared_leaf_is_not_classified_generic_through_the_census() -> Bool { + violation_count(source: concrete_via_global_bare_source, wanted: "DeclaredTypeInhabitanceUndecided") == 0 +} + +// THE REFINEMENT DECLINE IS THE INTRODUCTION QUESTION, NOT EVERY REFINEMENT PAIR. A reviewer's +// natural suspicion is that refinement_inhabitance simply made refinement pairs undecidable; these +// two arms refuse that reading by pairing a bare literal against a cast one at the SAME formal. +// The bare literal declines and the cast one does not, so the relation is discriminating on the +// carried introduction rather than on the refinement relation. +// +// AND THE PREDICATE IS ALREADY ENFORCED, which is why the decline is redundant ignorance rather +// than an exposed hole: takes_non_empty(s: "") is REFUSED by the where-refinement machinery with +// `type mismatch: expected Product(NonEmptyStr), got Primitive(String)`, while +// takes_non_empty(s: "x") is admitted by it. Measured live before enrolment. That is what fixes +// this relation's next-rung trigger at CONSULTING the existing verdict. +data bare_literal_at_refinement_source: String = "module probe_bare_literal_at_refinement\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: \"x\") }\n" + +data cast_literal_at_refinement_source: String = "module probe_cast_literal_at_refinement\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: \"x\" as NonEmptyStr) }\n" + +test fn w_a_bare_literal_at_a_refinement_formal_declines_and_a_cast_one_does_not() -> Bool { + violation_count(source: bare_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") == 1 + && violation_count(source: cast_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") == 0 +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 123ccbe5521..588b2ba1851 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3325,25 +3325,27 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // formal, 3870 of those a plain String at a NonEmptyStr formal. That is not four thousand // defects, so the refusal was withdrawn and the pair is declined instead. // -// WHAT THE DECLINE IS AND IS NOT, because the first account of it was wrong and the check that -// refuted it is cheap. It is NOT that introduction is uncarried: an EXPLICIT CAST IS ALREADY -// VISIBLE HERE. dag/test/fixture/compile_phase_frontier_receipt_fixture calls -// sha256_digest(hex: "..." as NonEmptyStr) at a refinement formal and produces no diagnostic from -// this relation at all, while the sites that do decline are bare literals -- "feedFwdOffsetCoeff", -// 168, "declaration-worker" -- handed straight to a refinement formal with no cast. So the -// discriminating fact exists and the seam already reads one of its two forms. +// WHAT THE DECLINE IS, AND TWO WRONG ACCOUNTS OF IT THAT MEASUREMENT KILLED. It is NOT that +// introduction is uncarried: an EXPLICIT CAST IS ALREADY VISIBLE HERE -- +// takes_non_empty(s: "x" as NonEmptyStr) produces nothing from this relation, while bare literals +// decline. And it is NOT that the predicate goes unchecked: a three-way fixture pair settles it. +// takes_non_empty(s: "") -> REFUSED, `type mismatch: expected Product(NonEmptyStr), got +// Primitive(String)`, from the where-refinement predicate machinery +// takes_non_empty(s: "x") -> admitted by that same machinery, no mismatch +// both -> this relation declines with UndecidableRefinementIntroduction // -// The remaining form is LITERAL ELABORATION at the declared boundary, which std.literal_elaboration -// owns and this relation does not consult -- the same shape the numeric note above records, where -// the class was never undecidable, it was unconsulted. Refusing on a fact one is declining to look -// up would fabricate a verdict in the direction DESIGN section 5 forbids as firmly as fabricating -// a success, so the pair is reported UndecidableRefinementIntroduction: located, per-reason and -// countable, so the deficit ranks instead of vanishing. -// NEXT-RUNG TRIGGER: the elaboration verdict for a literal at its destination refinement reaching -// this seam on the produced node, at which point this arm refuses an unelaborated base value at a -// refinement formal instead of declining it. The trigger is not speculative: an empty string -// literal handed to a NonEmptyStr formal compiles with no diagnostic from anything in the tree, -// so the predicate is genuinely unchecked at introduction today. +// So the introduction question IS ALREADY DECIDED, by an authority this relation does not consult. +// That is the same shape the numeric note above records: the class was never undecidable, it was +// UNCONSULTED. Refusing here would fabricate a verdict in the direction DESIGN section 5 forbids +// as firmly as fabricating a success, and admitting here would assert a proof this relation did +// not perform; so the pair is reported UndecidableRefinementIntroduction -- located, per-reason, +// countable -- and the deficit ranks instead of vanishing. +// +// NEXT-RUNG TRIGGER, and it is CHEAPER than the one first written here: this relation consulting +// the where-refinement predicate verdict that already decides the pair, rather than a new +// elaboration fact reaching the seam. An earlier draft of this annotation claimed the predicate +// was unchecked at introduction, on a probe that reported no diagnostic for an empty literal; the +// fixture pair above refutes that, and the claim is withdrawn rather than defended. // // THE SIBLING ARM DECLINES TOO, AND THAT IS A SECTION 3 ANSWER RATHER THAN A GAP. Two refinements // that share a base without either being the other's ancestor look like the horizontal case brands From 4722b031ef669b0605abd840a4343b64b1c5caa5 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 7 Sep 2026 11:37:59 +0000 Subject: [PATCH 10/17] chore: regenerate drifted generated artifacts (ci auto-heal) Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md lookup_miss_read_as_positive_classification Ledger-Repair-Judged: docs/design-rung-drops.md --- docs/design-failure-modes.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index d8df52008de..4bd988f3142 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -356,4 +356,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. - **generated `docs/*.md` ledger projections have no ProcessExit actuator and no regen coverage, so an EDIT to a still-present row can sit in the authority, absent from the projection, with every completing instrument green** (INVALID STATE: `gunbc.recurring_failure_mode` is the authority; `docs/design-failure-modes.md` is the projection DESIGN.md points readers at. `expected_design_failure_modes_md` returns `String`. The refusal exits 2 with EMPTY STDOUT and interpolates the rendered value into the diagnostic on stderr: classify_exit's non-variant arm is type_name: ctx.format_value(other). Executed: wise-badger-902, EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown heading; quick-heron-85, proj3.err 1062137 bytes, same delimiters. The enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` forbids print-AND-SUCCEED, and holds. The content is therefore obtainable ONLY by scraping a half-megabyte stderr diagnostic between delimiters that are message prose (returned-open-quote and not-ProcessExit-close-quote), unversioned and enrolled by nothing. Extractable only by scraping an unversioned diagnostic — which is why the ProcessExit regen is the repair. `claim_executor --required-regen` compares only `is_compared_generated_basename` = ends_with .rs into `target/stage0-regen-candidate`. HARM: three rows can be edited in `.dag` after the last projection and nothing that exits 0 will say the markdown is stale. The meaning-fork in the field named type_name is a separate row, `type_name_field_carries_rendered_value`, not this class. SPECIMEN, measured by another lane while regenerating the projection, 2026-09-06: `instrument_answers_outside_its_domain`, `stale_claim_survives_its_own_correct_edit`, and `native_stack_recursion_unbounded_over_corpus_shaped_structure` had been edited in their authorities after the doc was last projected and had grown by 2349, 5519 and 1152 characters. Regenerating carried the repairs through. On origin/main as of 3531d30bb82 those three `.dag` files are older than `docs/design-failure-modes.md` (`81686f7bea8`), so CURRENT main is not claimed still stale; the class is that nothing completing could have said so while they were. SPECIMEN, review 58567 on gunbc#9864, on the host comment above `exit_status_for_class`: a relocation dropped the `status: refused — printing the value and exiting 0 would report success for a run whose outcome is unknown.` sentence while the comment claimed byte-for-byte equivalence. The doc lied, not the code. The sentence was restored rather than the claim weakened. That is this class on a different pair: an authority and its projection disagreeing with nothing completing to say so, and a real specimen rather than an injected literal. INCIDENT, not a fixture and not a perturbation ordered for this PR, produced by quick-heron-85 without looking for this class, commit b1c6378c6d: their authority row unresolved_callee_conflated_with_dispatched_elsewhere was UNPARSEABLE for a full commit. An authored receipt contained a quoted phrase using bare double quotes inside a double-quoted string; the string terminated early and the parser refused undefined variable this and undefined variable leaf. THE AUTHORITY DID NOT COMPILE, so docs/design-failure-modes.md kept rendering the previous vintage while presenting as current. They found it only by running the projection; reading the row does not surface the break. This PR's gate would go red on that commit because an unparseable authority makes the projector refuse — from the committed markdown alone, STALE bytes and an UNBUILDABLE authority are indistinguishable. THIS ROW IS THE DETECTOR GAP. The quoting injury that silently disabled the row they were filing is a neighbouring class they are filing separately; its next-rung trigger is string escaping in the .dag lexer. This gate makes that injury loud; it does not make it unwritable. Do not read this row as closing that class. THE IDENTITY-JOIN CORRECTION, which is the transferable part and which corrects a rule this project holds. Completeness is an identity join, not a count equality — and AN IDENTITY JOIN OVER ROW NAMES WOULD HAVE REPORTED THAT FILE COMPLETE AND CORRECT: every identity present, none missing, none extra. The drift was pure EDIT. Only a regenerated byte diff sees an edit. Worse: a first pass comparing line SETS read the three as REORDERINGS, because the changed rows shared an 80-character prefix with their old text, so the cheap check does not merely miss the drift, it manufactures a benign explanation for it. An identity join proves MEMBERSHIP, not CONTENT. THE TWO NEIGHBOURS THIS IS NOT. `authority_merges_unprotected_while_its_projection_is_guarded` is MERGE POLARITY: the generated projection is driver-bound while the hand-authored authority is not. Adjacent files, distinct defect — this row is the absence of a completing actuator or content gate, reachable with no merge in sight. `green_reported_over_a_population_the_instrument_does_not_own` is a split of actuators whose GREEN is read as covering the half it does not enumerate; that climb joined registry-projections to stage0-mirrors inside one required phase, and still does not give `gunbc run` a ProcessExit projector for the markdown, nor put `.md` in `--required-regen`. RECOGNITION RULE: when a generated file is what readers are pointed at, ask (1) whether any `ProcessExit` entry writes those exact bytes and exits 0, (2) whether regen's compared population includes that path, and (3) whether the gate compares CONTENT, not row-name membership. A complete identity set of names is not a content agreement. RUNG FOUND AT: outside the ladder until a completing content agreement exists — silent wrongness, not a weak wall. After a ProcessExit projector and a required content compare execute, mechanically preventable: the stale file remains writable. CEILING: structurally guaranteed when membership of every committed generated `docs/` path in a content-agreement adjudicator is derived from `gunbc.generated_artifact` `committed_generated_artifacts`, so omitting the arm is a compile refusal. NEXT-RUNG TRIGGER, a capability: required-run dispatch consumes a content agreement — byte identity of generated vs committed — over every committed generated artifact whose location directory is `docs`, derived from the registry so adding a committed `docs/` path without that agreement will not compile. A trigger naming one command, one test file, or `docs_projection_gate.dag` is less than the capability and would fire while edit-only drift can still sit uncompared.) - **a field named type_name holds a type name on three arms and a fully rendered value on the fourth** (INVALID STATE: ExitClass::NotProcessExit is one spelling whose payload field is called type_name. `classify_exit` Variant arms that are not ProcessExit put ctx.resolve of the variant type symbol, or ProcessExit plus the unknown variant, into it — an actual type or variant name. The final other arm puts ctx.format_value of the non-variant value — the rendered value — into the same field. `exit_status_for_class` interpolates that field into the returned-quote slot with no second match, so every refusal path reads one name for two facts. HARM: a reader of the interpolation site infers the field's contents from its NAME and concludes a String projector yields the word String; a reader of the producer and a live stderr file concludes the markdown body is in the diagnostic. Both readings of adjacent code are correct; the name is a third surface and it lied. SPECIMEN, 2026-09-06, executed both ways. clever-otter-298 read `exit_status_for_class` and the enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` (which constructs NotProcessExit with a fixture type_name Bool and never goes through `classify_exit`) and asserted the diagnostic names the type. wise-badger-902 read the interpolation site and ruled the same. quick-heron-85 held proj3.err at 1062137 bytes. The manager then RAN the projector: EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown. The field name said type; the field held format_value. WHY THE FORK SURVIVED, and it is a section 4b evidence gap not a naming smell. `non_process_exit_refuses_rather_than_printing_and_succeeding` hand-constructs ExitClass::NotProcessExit with type_name the literal Bool and starts from an already-classified value. It never calls `classify_exit`. Nothing executing joins the field's name to its contents on the non-variant path — the only enrolled evidence feeds the field a literal that matches its name, which is exactly the input that cannot discriminate. The control's RED is unauthorable for this defect, so it was permanently green over the case that mattered and got cited as coverage. A field carrying two facts is ordinary; a field carrying two facts with a control that only ever sees one of them is why three of us read adjacent code correctly and reached three answers. THIS IS NOT `docs_markdown_projections_have_no_completing_actuator`. That row is the absence of a ProcessExit actuator and a content gate over generated `docs/*.md`. This row is a meaning fork inside `ExitClass`, reachable with no docs file in sight. Neighbour `meaning_fork` is the generic class; this instance is filed because the fork sat in the struct every refusal path reads and produced the three-way contradiction. Neighbour `diagnostic_name_mechanism_silent` is a diagnostic NAME silent about its predicate; here the FIELD name is accurate for three arms and false for the fourth. RECOGNITION RULE: when a field is named for a kind of contents, read every constructor, not the interpolation site. If one constructor writes a different kind, the name has forked. RUNG FOUND AT: mitigatable — the wrong inference is a human reading; the runtime still refuses with exit 2 and does not print-and-succeed. CEILING: structurally impossible when `NotProcessExit` cannot be constructed with a rendered value under a field named for a type — two variants, or a field named for what it actually holds. NEXT-RUNG TRIGGER, a capability: `ExitClass` distinguishes a type-name refusal from a rendered-value refusal in the type, so interpolating one as the other will not compile.) -- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. REPAIR AND ITS OWN LIMIT: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. A leaf that is not on the roster and resolves nowhere is UNRESOLVED, a different fact, reported `UndecidableFormalUnresolved`. NEXT-RUNG TRIGGER for the residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) From dd87b10982c7ba60915b9bec0b6a8fa3022cd205 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 16:11:15 +0000 Subject: [PATCH 11/17] Keep tp_names in the roster; re-author the controls as fixture pairs Three repairs, each from a measurement or a review finding, not from taste. THE ROSTER IS A UNION AGAIN. Deleting the absence disjunct was the repair; replacing fn_type_param_names with borrowed_generic_param_names alongside it was a second, uncontrolled change. The two predicates are not the same: the borrowed roster is wider on one axis and NARROWER on two, so a declared type param whose type expression is not a childless NoConnective leaf would have been reclassified as a concrete unresolved name -- the exact failure the negative control exists to prevent, arriving through the other door. declaration_generic_names is now concat(tp_names, map_keys(borrowed_generic_param_names(...))). Review finding, tidy-lynx-804, 2026-09-07. THE CONTROLS WERE AUTHORED AGAINST THE WRONG ORACLE AND ALL SIX WERE FALSE. violation_count reports every row of the class in the WHOLE census, not the fixture's contribution, and the literals in those arms were copied from a probe DELTA. That is precisely what DESIGN 5 refuses: a merge-blocking test comparing a live population to a numeric literal that is not grounded in a controlled fixture. Each arm is now a PAIR of fixtures differing on exactly one axis, so the shared corpus contribution cancels and only the axis is measured. Measured on this head, with the same instrument on both halves: declared NonEmptyStr <- produced HostIdentity == its exact-match partner the horizontal brand pair > its exact-match partner bare literal at a refinement formal > the cast form concrete leaf via global-bare == a fixture with no call THE POSITIVE CENSUS ARM IS WITHDRAWN BECAUSE ITS RED IS NOT AUTHORABLE. The fixture contributes zero rows of the class -- equal to a fixture with no call at all -- so the seam emits nothing there whether the classification is right or wrong. An arm asserting one is false; an arm asserting zero is green by construction and would later be cited as coverage of something it never measured. The cause is a harness boundary, not a fixture shape: src/v1 is not a source root under the required floor, so no witness there can observe the substitution basis. NEXT-RUNG TRIGGER, at capability grain: a floor-executable surface that can observe the substitution basis's classification -- src/v1 on a floor source root, or a black-box seam that renders the stamp distinguishably. What is measured is the REMOVAL OF A FALSE POSITIVE, which the negative arm measures directly. What stays unmeasured is the survival of the positive authority. The union above makes that safer by construction; construction is not evidence and this does not claim it is. Also regenerates docs/design-failure-modes.md, which drifted because the merge resolution took main's projection without re-projecting the new row. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- ...e_inhabitance_direct_call_witness_test.dag | 54 ++++++++++--------- docs/design-failure-modes.md | 2 +- src/v1/04_lookup.dag | 11 +++- src/v1/stage0/src/v1_compiler_infer_lookup.rs | 5 +- 4 files changed, 45 insertions(+), 27 deletions(-) diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index ec5122875db..021d38ab3e3 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -330,11 +330,23 @@ test fn w_a_phantom_type_argument_with_identical_representation_is_still_separat // also hold if the arm merely stopped deciding, which is the failure mode this lane exists to // refuse; requiring zero UNDECIDED as well pins the site to INHABITS. Measured live before // enrolment: undecided=0, refused=0. +// THE PARTNERS EXIST BECAUSE THE COUNT IS CORPUS-WIDE, NOT FIXTURE-LOCAL. violation_count reports +// every row of the class in the census, so a per-fixture literal can never be its oracle -- the +// literal would be a measurement of the current tree copied into the assertion, which DESIGN 5 +// refuses by name. Each control below is therefore a PAIR differing on exactly one axis, so the +// shared corpus contribution cancels and only the axis is measured. +data refinement_baseline_source: String = "module probe_refinement_baseline\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { 0 }\n" + +data probe_exact_refinement_source: String = "module probe_exact_refinement\nimport std.types { NonEmptyStr, Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host_x: HostIdentity = \"srv1\" as HostIdentity\nfn takes_host(s: HostIdentity) -> Int { 1 }\nfn probe() -> Int { takes_host(s: probe_host_x) }\n" + +data probe_exact_brand_source: String = "module probe_exact_brand\nimport std.types { Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host_y: HostIdentity = \"srv1\" as HostIdentity\nfn takes_host2(x: HostIdentity) -> Int { 1 }\nfn probe() -> Int { takes_host2(x: probe_host_y) }\n" + data refinement_widening_source: String = "module probe_refinement_widening\nimport std.types { NonEmptyStr, Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host: HostIdentity = \"srv1\" as HostIdentity\nfn takes_base(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_base(s: probe_host) }\n" test fn w_a_branded_refinement_at_its_own_declared_base_inhabits() -> Bool { violation_count(source: refinement_widening_source, wanted: "DeclaredTypeNotInhabited") == 0 - && violation_count(source: refinement_widening_source, wanted: "DeclaredTypeInhabitanceUndecided") == 0 + && violation_count(source: refinement_widening_source, wanted: "DeclaredTypeInhabitanceUndecided") + == violation_count(source: probe_exact_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") } // THE HORIZONTAL CASE IS REFUSED BY THE BRAND AUTHORITY, NOT BY THIS RELATION, AND THAT @@ -355,7 +367,8 @@ data brand_horizontal_at_argument_source: String = "module probe_brand_horizonta test fn w_two_distinct_brands_over_one_base_are_not_refused_twice() -> Bool { violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeNotInhabited") == 0 - && violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeInhabitanceUndecided") == 1 + && violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeInhabitanceUndecided") + > violation_count(source: probe_exact_brand_source, wanted: "DeclaredTypeInhabitanceUndecided") } // nominal_opaque DOES NOT GROUND TO ITS BASE, and the control exists because the chain walk is @@ -372,27 +385,19 @@ test fn w_two_distinct_brands_over_one_base_are_not_refused_twice() -> Bool { data nominal_opaque_not_grounded_source: String = "module probe_nominal_opaque_not_grounded\nimport std.types { NonEmptyStr, Secret, Int }\ndata probe_secret: Secret = \"shh\" as Secret\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: probe_secret) }\n" test fn w_a_nominal_opaque_alias_does_not_ground_through_the_refinement_chain() -> Bool { - violation_count(source: nominal_opaque_not_grounded_source, wanted: "DeclaredTypeInhabitanceUndecided") == 0 + violation_count(source: nominal_opaque_not_grounded_source, wanted: "DeclaredTypeNotInhabited") == 1 } -// THE ROSTER SURVIVED, AND THIS IS THE HALF A DIAGNOSTIC-COUNT DROP CANNOT PROVE. Deleting the -// absence classification lowers the generic-formal population; so does deleting generic -// classification altogether. These two arms are the paired mutations that separate them, and -// neither subsumes the other. Both go through the GLOBAL-BARE CENSUS route -- the callee is named -// without an import, so it resolves through the corpus census and reaches -// census_declaration_bound_formals, which is the producer this repair changed. -// -// POSITIVE: a genuine angle-bracket generic is STILL classified generic. v2.std.optional declares -// fn optional_present(value: T), the parser mints its clause as a param spelled T: T, and -// borrowed_generic_param_names carries it, so the leaf reaches the substitution basis stamped a -// type variable and the seam declines UndecidableGenericFormal. DISCRIMINATING MUTATION: feed -// census_declaration_bound_formals an empty roster and the leaf is unstamped, resolves nowhere, -// and the site produces NO diagnostic at all -- this arm goes red on zero. -data generic_via_global_bare_source: String = "module probe_generic_via_global_bare\nimport std.types { Int }\nfn probe() -> Int {\n match optional_present(value: 1) {\n Present { value: v } => v\n Absent => 0\n }\n}\n" - -test fn w_a_declared_generic_clause_is_still_classified_generic_through_the_census() -> Bool { - violation_count(source: generic_via_global_bare_source, wanted: "DeclaredTypeInhabitanceUndecided") == 1 -} +// THE POSITIVE CENSUS ARM IS NOT AUTHORABLE HERE, AND THAT IS THE FINDING RATHER THAN AN OMISSION. +// It was to assert that a DECLARED generic clause is still classified generic through the census +// route, over a bare cross-module call (optional_present). Measured on this head: that fixture +// contributes ZERO rows of this class -- its count equals a fixture with no call at all -- so the +// seam emits nothing there whether the classification is right or wrong. An arm asserting a count +// of one is then false, and an arm asserting zero would be green by construction and would be +// cited later as coverage of a thing it never measured, which DESIGN 4b forbids by name: ask +// whether the RED is authorable BEFORE writing the check. The negative arm below IS authorable and +// is enrolled. The residue -- no executing positive control for the census route's generic half -- +// is stated in the PR body rather than papered over with a decoration. // NEGATIVE: a CONCRETE declared leaf is no longer classified generic. std.content_hash declares // fn sha256_digest_wire_form(digest: Sha256Digest) -> NonEmptyStr; Sha256Digest is an ordinary @@ -405,7 +410,8 @@ test fn w_a_declared_generic_clause_is_still_classified_generic_through_the_cens data concrete_via_global_bare_source: String = "module probe_concrete_via_global_bare\nimport std.content_hash { Sha256Digest }\nimport std.types { NonEmptyStr, Int }\nfn probe(d: Sha256Digest) -> NonEmptyStr { sha256_digest_wire_form(digest: d) }\n" test fn w_a_concrete_declared_leaf_is_not_classified_generic_through_the_census() -> Bool { - violation_count(source: concrete_via_global_bare_source, wanted: "DeclaredTypeInhabitanceUndecided") == 0 + violation_count(source: concrete_via_global_bare_source, wanted: "DeclaredTypeInhabitanceUndecided") + == violation_count(source: refinement_baseline_source, wanted: "DeclaredTypeInhabitanceUndecided") } // THE REFINEMENT DECLINE IS THE INTRODUCTION QUESTION, NOT EVERY REFINEMENT PAIR. A reviewer's @@ -424,6 +430,6 @@ data bare_literal_at_refinement_source: String = "module probe_bare_literal_at_r data cast_literal_at_refinement_source: String = "module probe_cast_literal_at_refinement\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: \"x\" as NonEmptyStr) }\n" test fn w_a_bare_literal_at_a_refinement_formal_declines_and_a_cast_one_does_not() -> Bool { - violation_count(source: bare_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") == 1 - && violation_count(source: cast_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") == 0 + violation_count(source: bare_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") + > violation_count(source: cast_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") } diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index d8df52008de..4bd988f3142 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -356,4 +356,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. - **generated `docs/*.md` ledger projections have no ProcessExit actuator and no regen coverage, so an EDIT to a still-present row can sit in the authority, absent from the projection, with every completing instrument green** (INVALID STATE: `gunbc.recurring_failure_mode` is the authority; `docs/design-failure-modes.md` is the projection DESIGN.md points readers at. `expected_design_failure_modes_md` returns `String`. The refusal exits 2 with EMPTY STDOUT and interpolates the rendered value into the diagnostic on stderr: classify_exit's non-variant arm is type_name: ctx.format_value(other). Executed: wise-badger-902, EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown heading; quick-heron-85, proj3.err 1062137 bytes, same delimiters. The enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` forbids print-AND-SUCCEED, and holds. The content is therefore obtainable ONLY by scraping a half-megabyte stderr diagnostic between delimiters that are message prose (returned-open-quote and not-ProcessExit-close-quote), unversioned and enrolled by nothing. Extractable only by scraping an unversioned diagnostic — which is why the ProcessExit regen is the repair. `claim_executor --required-regen` compares only `is_compared_generated_basename` = ends_with .rs into `target/stage0-regen-candidate`. HARM: three rows can be edited in `.dag` after the last projection and nothing that exits 0 will say the markdown is stale. The meaning-fork in the field named type_name is a separate row, `type_name_field_carries_rendered_value`, not this class. SPECIMEN, measured by another lane while regenerating the projection, 2026-09-06: `instrument_answers_outside_its_domain`, `stale_claim_survives_its_own_correct_edit`, and `native_stack_recursion_unbounded_over_corpus_shaped_structure` had been edited in their authorities after the doc was last projected and had grown by 2349, 5519 and 1152 characters. Regenerating carried the repairs through. On origin/main as of 3531d30bb82 those three `.dag` files are older than `docs/design-failure-modes.md` (`81686f7bea8`), so CURRENT main is not claimed still stale; the class is that nothing completing could have said so while they were. SPECIMEN, review 58567 on gunbc#9864, on the host comment above `exit_status_for_class`: a relocation dropped the `status: refused — printing the value and exiting 0 would report success for a run whose outcome is unknown.` sentence while the comment claimed byte-for-byte equivalence. The doc lied, not the code. The sentence was restored rather than the claim weakened. That is this class on a different pair: an authority and its projection disagreeing with nothing completing to say so, and a real specimen rather than an injected literal. INCIDENT, not a fixture and not a perturbation ordered for this PR, produced by quick-heron-85 without looking for this class, commit b1c6378c6d: their authority row unresolved_callee_conflated_with_dispatched_elsewhere was UNPARSEABLE for a full commit. An authored receipt contained a quoted phrase using bare double quotes inside a double-quoted string; the string terminated early and the parser refused undefined variable this and undefined variable leaf. THE AUTHORITY DID NOT COMPILE, so docs/design-failure-modes.md kept rendering the previous vintage while presenting as current. They found it only by running the projection; reading the row does not surface the break. This PR's gate would go red on that commit because an unparseable authority makes the projector refuse — from the committed markdown alone, STALE bytes and an UNBUILDABLE authority are indistinguishable. THIS ROW IS THE DETECTOR GAP. The quoting injury that silently disabled the row they were filing is a neighbouring class they are filing separately; its next-rung trigger is string escaping in the .dag lexer. This gate makes that injury loud; it does not make it unwritable. Do not read this row as closing that class. THE IDENTITY-JOIN CORRECTION, which is the transferable part and which corrects a rule this project holds. Completeness is an identity join, not a count equality — and AN IDENTITY JOIN OVER ROW NAMES WOULD HAVE REPORTED THAT FILE COMPLETE AND CORRECT: every identity present, none missing, none extra. The drift was pure EDIT. Only a regenerated byte diff sees an edit. Worse: a first pass comparing line SETS read the three as REORDERINGS, because the changed rows shared an 80-character prefix with their old text, so the cheap check does not merely miss the drift, it manufactures a benign explanation for it. An identity join proves MEMBERSHIP, not CONTENT. THE TWO NEIGHBOURS THIS IS NOT. `authority_merges_unprotected_while_its_projection_is_guarded` is MERGE POLARITY: the generated projection is driver-bound while the hand-authored authority is not. Adjacent files, distinct defect — this row is the absence of a completing actuator or content gate, reachable with no merge in sight. `green_reported_over_a_population_the_instrument_does_not_own` is a split of actuators whose GREEN is read as covering the half it does not enumerate; that climb joined registry-projections to stage0-mirrors inside one required phase, and still does not give `gunbc run` a ProcessExit projector for the markdown, nor put `.md` in `--required-regen`. RECOGNITION RULE: when a generated file is what readers are pointed at, ask (1) whether any `ProcessExit` entry writes those exact bytes and exits 0, (2) whether regen's compared population includes that path, and (3) whether the gate compares CONTENT, not row-name membership. A complete identity set of names is not a content agreement. RUNG FOUND AT: outside the ladder until a completing content agreement exists — silent wrongness, not a weak wall. After a ProcessExit projector and a required content compare execute, mechanically preventable: the stale file remains writable. CEILING: structurally guaranteed when membership of every committed generated `docs/` path in a content-agreement adjudicator is derived from `gunbc.generated_artifact` `committed_generated_artifacts`, so omitting the arm is a compile refusal. NEXT-RUNG TRIGGER, a capability: required-run dispatch consumes a content agreement — byte identity of generated vs committed — over every committed generated artifact whose location directory is `docs`, derived from the registry so adding a committed `docs/` path without that agreement will not compile. A trigger naming one command, one test file, or `docs_projection_gate.dag` is less than the capability and would fire while edit-only drift can still sit uncompared.) - **a field named type_name holds a type name on three arms and a fully rendered value on the fourth** (INVALID STATE: ExitClass::NotProcessExit is one spelling whose payload field is called type_name. `classify_exit` Variant arms that are not ProcessExit put ctx.resolve of the variant type symbol, or ProcessExit plus the unknown variant, into it — an actual type or variant name. The final other arm puts ctx.format_value of the non-variant value — the rendered value — into the same field. `exit_status_for_class` interpolates that field into the returned-quote slot with no second match, so every refusal path reads one name for two facts. HARM: a reader of the interpolation site infers the field's contents from its NAME and concludes a String projector yields the word String; a reader of the producer and a live stderr file concludes the markdown body is in the diagnostic. Both readings of adjacent code are correct; the name is a third surface and it lied. SPECIMEN, 2026-09-06, executed both ways. clever-otter-298 read `exit_status_for_class` and the enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` (which constructs NotProcessExit with a fixture type_name Bool and never goes through `classify_exit`) and asserted the diagnostic names the type. wise-badger-902 read the interpolation site and ruled the same. quick-heron-85 held proj3.err at 1062137 bytes. The manager then RAN the projector: EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown. The field name said type; the field held format_value. WHY THE FORK SURVIVED, and it is a section 4b evidence gap not a naming smell. `non_process_exit_refuses_rather_than_printing_and_succeeding` hand-constructs ExitClass::NotProcessExit with type_name the literal Bool and starts from an already-classified value. It never calls `classify_exit`. Nothing executing joins the field's name to its contents on the non-variant path — the only enrolled evidence feeds the field a literal that matches its name, which is exactly the input that cannot discriminate. The control's RED is unauthorable for this defect, so it was permanently green over the case that mattered and got cited as coverage. A field carrying two facts is ordinary; a field carrying two facts with a control that only ever sees one of them is why three of us read adjacent code correctly and reached three answers. THIS IS NOT `docs_markdown_projections_have_no_completing_actuator`. That row is the absence of a ProcessExit actuator and a content gate over generated `docs/*.md`. This row is a meaning fork inside `ExitClass`, reachable with no docs file in sight. Neighbour `meaning_fork` is the generic class; this instance is filed because the fork sat in the struct every refusal path reads and produced the three-way contradiction. Neighbour `diagnostic_name_mechanism_silent` is a diagnostic NAME silent about its predicate; here the FIELD name is accurate for three arms and false for the fourth. RECOGNITION RULE: when a field is named for a kind of contents, read every constructor, not the interpolation site. If one constructor writes a different kind, the name has forked. RUNG FOUND AT: mitigatable — the wrong inference is a human reading; the runtime still refuses with exit 2 and does not print-and-succeed. CEILING: structurally impossible when `NotProcessExit` cannot be constructed with a rendered value under a field named for a type — two variants, or a field named for what it actually holds. NEXT-RUNG TRIGGER, a capability: `ExitClass` distinguishes a type-name refusal from a rendered-value refusal in the type, so interpolating one as the other will not compile.) -- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. REPAIR AND ITS OWN LIMIT: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. A leaf that is not on the roster and resolves nowhere is UNRESOLVED, a different fact, reported `UndecidableFormalUnresolved`. NEXT-RUNG TRIGGER for the residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) diff --git a/src/v1/04_lookup.dag b/src/v1/04_lookup.dag index 17474068992..6d8423df90b 100644 --- a/src/v1/04_lookup.dag +++ b/src/v1/04_lookup.dag @@ -627,6 +627,14 @@ fn borrowed_census_callable_candidate(type_env: TypeEnv, name: String, candidate } } +// THE ROSTER IS THE UNION OF TWO FACTS AND NEITHER SUBSUMES THE OTHER. fn_type_param_names reads +// the DECLARED clause; borrowed_generic_param_names reads params whose type expression is a +// childless NoConnective leaf spelled as the parameter or its type name. The second is wider on one +// axis and NARROWER on two -- it drops any declared type param whose type expression is not such a +// leaf, and any with an empty name -- so passing it alone would reclassify such a param as a +// concrete unresolved name: the exact failure the negative control below exists to prevent, +// arriving through the other door. Review finding, tidy-lynx-804, 2026-09-07. The union is what the +// pre-repair code passed and it is what is passed here; only the ABSENCE disjunct is deleted. fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String, node: Node) -> List { let tp_names = fn_type_param_names(item: node, source_indices: type_env.source_indices) let declaration_env = census_declaration_type_env( @@ -648,7 +656,8 @@ fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String outer: declared_type, inner: peel_nominal_alias_identity(n: declared_type, env: declaration_env, module_name: owner_module_path)), substitution_basis: declaration_substitution_basis( - n: declared_type, env: declaration_env, generic_names: map_keys(declaration_generic_names)) + n: declared_type, env: declaration_env, + generic_names: concat(tp_names, map_keys(declaration_generic_names))) } }) } diff --git a/src/v1/stage0/src/v1_compiler_infer_lookup.rs b/src/v1/stage0/src/v1_compiler_infer_lookup.rs index 2a8fcc7e751..afbfb33e19e 100644 --- a/src/v1/stage0/src/v1_compiler_infer_lookup.rs +++ b/src/v1/stage0/src/v1_compiler_infer_lookup.rs @@ -753,7 +753,10 @@ pub fn census_declaration_bound_formals( crate::v1_compiler_infer_env::declaration_substitution_basis( declared_type.clone(), declaration_env.clone(), - Rc::new(v1_rt::map_keys(&declaration_generic_names)), + v1_rt::concat( + tp_names.clone(), + Rc::new(v1_rt::map_keys(&declaration_generic_names)), + ), ), }) }); From ded6f36812c485dc135377b6c739c5c3cd175b60 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 19:05:31 +0000 Subject: [PATCH 12/17] The relation stops collapsing distinctions the rest of the file keeps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Six items, all from review, all on the relation this PR adds. They are one shape stated once: the new relation collapsed distinctions its neighbours preserve -- two facts under one reason, two identities under one spelling, and a missing identity repaired by lowering the grain until something compared equal. 1. THE PEER ARM CARRIES ITS OWN REASON. Narrowing and siblings both reported UndecidableRefinementIntroduction, whose label describes introduction only. The measured population proves they differ: declared NonEmptyStr <- produced FilePath, GcpProjectId, Sha512DigestHex are peer predicates over one base, neither introductions nor brand conflicts. A mixed bucket is not located, per-reason or countable -- the property that note claims for itself -- and it would mis-aim the next trigger, discharging it while leaving a peer residue under a name asserting it had been handled. (Review 62043, cursor/auto.) 2. THE CONSTRUCTOR IS RENAMED WITH THE REASON. RefinementSiblingBrands -> RefinementPeerChains: the measured population contains no brands, so the old name encoded the same conflation one level above the reason. 3. THE CHAIN IS COMPARED AT DECLARATION SITE, NOT SPELLING. It consumed qualified_last_segment -- a module-stripped last segment -- while where_refinement_brand_declaration_site in the same file builds file#name identity for the same question. Two homonymous refinements would have compared EQUAL and widening would have returned Inhabits for a pair that does not inhabit. This file already suffered that class: a second HostIdentity was minted beside product.placement_supply's and did not surface as a duplicate declaration. Only one survives today because the incident was CLEANED UP, not avoided -- so this is a reintroduction, not a hypothetical. 4. THE LOOKUP-MISS ARM REFUSES INSTEAD OF WIDENING. It manufactured a singleton chain from the name's last segment when no declaration was established, so callers treating both chains as established compared something that was never resolved -- DESIGN §5's absorbing fallback, and under declaration-site keying it would fabricate an identity the subject does not have, at the one grain where unrelated things compare equal. ABSENCE OF IDENTITY CANNOT BE REPAIRED BY LOWERING THE IDENTITY GRAIN UNTIL SOMETHING COMPARES EQUAL. 5. THE FAILURE-MODE ROW'S CEILING STATES BOTH POPULATIONS. It claimed ceiling 3 from a premise about the CLAUSE while the subject is the CLASSIFICATION, which a predicate decides and an authored shape can satisfy: eight structural producers cannot mint `pname == type-expr name`, four authored-dependent sites can. Now 3 for the clause-derived population, 2 for authored parameters, with the authored shape named as what stands between it and 3. The row's repair sentence also records that the roster passed is a UNION. 6. BOTH HALVES OF THE BRAND DELEGATION ARE ASSERTED. The witness asserted only that this relation abstains. If the brand wall regressed or stopped reaching the argument path, that stayed green while the horizontal pair was admitted in silence by both relations -- green for a reason other than the one it claims, which is the defect this whole lane exists to remove. The wall's TypeMismatch firing is now a conjunct of the same witness, against the same exact-match partner so the corpus term cancels. The whole required floor is green locally with all six in. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- ...p_miss_read_as_positive_classification.dag | 4 +- ...e_inhabitance_direct_call_witness_test.dag | 11 ++ docs/design-failure-modes.md | 2 +- src/v1/04_infer.dag | 65 ++++++++++-- src/v1/stage0/src/v1_compiler_infer.rs | 100 +++++++++++------- 5 files changed, 135 insertions(+), 47 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag index b7216cafac2..7cb15ea3fa5 100644 --- a/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag +++ b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag @@ -19,9 +19,9 @@ data lookup_miss_read_as_positive_classification: RecurringFailureMode = Recurri "THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. ", - "RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. ", + "RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed) FOR THE CLAUSE-DERIVED POPULATION, AND MECHANICALLY PREVENTABLE (2) FOR AUTHORED PARAMETERS -- the two are stated separately because a bare ceiling 3 would send a reader past the exception. Generic ownership IS a declared fact: `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the CLAUSE has. But the classification is decided by a PREDICATE over that shape, not by the clause, and an authored shape can satisfy it: the `make_param_node` producer census found EIGHT structural producers that cannot mint `pname == type-expr name`, and FOUR authored-dependent sites that can -- an author writing `fn f(Vendor: Vendor)` produces a parameter the roster predicate cannot distinguish from a generic clause. The subject of this row is the CLASSIFICATION, not the clause, so the reported rung is the minimum across both populations. WHAT STANDS BETWEEN THIS AND 3 OUTRIGHT: the authored `pname == type-expr name` shape, which no clause-side encoding can exclude. ", - "REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. ", + "REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE ROSTER PASSED IS A UNION AND THAT HALF IS NOT OPTIONAL: the declared `` clause and the borrowed-parameter roster are two facts and neither subsumes the other -- the borrowed predicate is narrower on two axes, so passing it ALONE would reclassify a declared type param whose type expression is not a childless leaf as a concrete unresolved name, reintroducing the same misclassification through the opposite door. Deleting the absence disjunct is the repair; replacing the declared-clause predicate beside it was a second change and is not part of it. ", "THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. ", diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index 021d38ab3e3..f004919914c 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -349,6 +349,15 @@ test fn w_a_branded_refinement_at_its_own_declared_base_inhabits() -> Bool { == violation_count(source: probe_exact_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") } +// +// BOTH HALVES OF THE DELEGATION ARE ASSERTED HERE, AND THE SECOND IS WHY THIS WITNESS IS NOT +// GREEN-FOR-THE-WRONG-REASON. The abstain half -- this relation adds an undecided and no refusal -- +// says only that WE did not decide. If the brand wall regressed, stopped reaching the argument +// path, or lost its consumer, that half would stay green while the horizontal pair was admitted in +// silence by both relations, and the abstention would be a hole rather than a delegation with the +// only record of the difference sitting in a PR body. So the refuse half is asserted in the same +// witness, against the same exact-match partner so the corpus term cancels: the wall's TypeMismatch +// FIRES on the horizontal pair and does not on the matching one. Review finding, tidy-lynx-804. // THE HORIZONTAL CASE IS REFUSED BY THE BRAND AUTHORITY, NOT BY THIS RELATION, AND THAT // DIVISION IS THE POINT. HostIdentity and PhysicalAssetIdentity are both // `NonEmptyStr where brand(...)`, so their chains meet at NonEmptyStr with neither an ancestor of @@ -369,6 +378,8 @@ test fn w_two_distinct_brands_over_one_base_are_not_refused_twice() -> Bool { violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeNotInhabited") == 0 && violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeInhabitanceUndecided") > violation_count(source: probe_exact_brand_source, wanted: "DeclaredTypeInhabitanceUndecided") + && violation_count(source: brand_horizontal_at_argument_source, wanted: "TypeMismatch") + > violation_count(source: probe_exact_brand_source, wanted: "TypeMismatch") } // nominal_opaque DOES NOT GROUND TO ITS BASE, and the control exists because the chain walk is diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 4bd988f3142..9789a1ddbd7 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -356,4 +356,4 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. - **generated `docs/*.md` ledger projections have no ProcessExit actuator and no regen coverage, so an EDIT to a still-present row can sit in the authority, absent from the projection, with every completing instrument green** (INVALID STATE: `gunbc.recurring_failure_mode` is the authority; `docs/design-failure-modes.md` is the projection DESIGN.md points readers at. `expected_design_failure_modes_md` returns `String`. The refusal exits 2 with EMPTY STDOUT and interpolates the rendered value into the diagnostic on stderr: classify_exit's non-variant arm is type_name: ctx.format_value(other). Executed: wise-badger-902, EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown heading; quick-heron-85, proj3.err 1062137 bytes, same delimiters. The enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` forbids print-AND-SUCCEED, and holds. The content is therefore obtainable ONLY by scraping a half-megabyte stderr diagnostic between delimiters that are message prose (returned-open-quote and not-ProcessExit-close-quote), unversioned and enrolled by nothing. Extractable only by scraping an unversioned diagnostic — which is why the ProcessExit regen is the repair. `claim_executor --required-regen` compares only `is_compared_generated_basename` = ends_with .rs into `target/stage0-regen-candidate`. HARM: three rows can be edited in `.dag` after the last projection and nothing that exits 0 will say the markdown is stale. The meaning-fork in the field named type_name is a separate row, `type_name_field_carries_rendered_value`, not this class. SPECIMEN, measured by another lane while regenerating the projection, 2026-09-06: `instrument_answers_outside_its_domain`, `stale_claim_survives_its_own_correct_edit`, and `native_stack_recursion_unbounded_over_corpus_shaped_structure` had been edited in their authorities after the doc was last projected and had grown by 2349, 5519 and 1152 characters. Regenerating carried the repairs through. On origin/main as of 3531d30bb82 those three `.dag` files are older than `docs/design-failure-modes.md` (`81686f7bea8`), so CURRENT main is not claimed still stale; the class is that nothing completing could have said so while they were. SPECIMEN, review 58567 on gunbc#9864, on the host comment above `exit_status_for_class`: a relocation dropped the `status: refused — printing the value and exiting 0 would report success for a run whose outcome is unknown.` sentence while the comment claimed byte-for-byte equivalence. The doc lied, not the code. The sentence was restored rather than the claim weakened. That is this class on a different pair: an authority and its projection disagreeing with nothing completing to say so, and a real specimen rather than an injected literal. INCIDENT, not a fixture and not a perturbation ordered for this PR, produced by quick-heron-85 without looking for this class, commit b1c6378c6d: their authority row unresolved_callee_conflated_with_dispatched_elsewhere was UNPARSEABLE for a full commit. An authored receipt contained a quoted phrase using bare double quotes inside a double-quoted string; the string terminated early and the parser refused undefined variable this and undefined variable leaf. THE AUTHORITY DID NOT COMPILE, so docs/design-failure-modes.md kept rendering the previous vintage while presenting as current. They found it only by running the projection; reading the row does not surface the break. This PR's gate would go red on that commit because an unparseable authority makes the projector refuse — from the committed markdown alone, STALE bytes and an UNBUILDABLE authority are indistinguishable. THIS ROW IS THE DETECTOR GAP. The quoting injury that silently disabled the row they were filing is a neighbouring class they are filing separately; its next-rung trigger is string escaping in the .dag lexer. This gate makes that injury loud; it does not make it unwritable. Do not read this row as closing that class. THE IDENTITY-JOIN CORRECTION, which is the transferable part and which corrects a rule this project holds. Completeness is an identity join, not a count equality — and AN IDENTITY JOIN OVER ROW NAMES WOULD HAVE REPORTED THAT FILE COMPLETE AND CORRECT: every identity present, none missing, none extra. The drift was pure EDIT. Only a regenerated byte diff sees an edit. Worse: a first pass comparing line SETS read the three as REORDERINGS, because the changed rows shared an 80-character prefix with their old text, so the cheap check does not merely miss the drift, it manufactures a benign explanation for it. An identity join proves MEMBERSHIP, not CONTENT. THE TWO NEIGHBOURS THIS IS NOT. `authority_merges_unprotected_while_its_projection_is_guarded` is MERGE POLARITY: the generated projection is driver-bound while the hand-authored authority is not. Adjacent files, distinct defect — this row is the absence of a completing actuator or content gate, reachable with no merge in sight. `green_reported_over_a_population_the_instrument_does_not_own` is a split of actuators whose GREEN is read as covering the half it does not enumerate; that climb joined registry-projections to stage0-mirrors inside one required phase, and still does not give `gunbc run` a ProcessExit projector for the markdown, nor put `.md` in `--required-regen`. RECOGNITION RULE: when a generated file is what readers are pointed at, ask (1) whether any `ProcessExit` entry writes those exact bytes and exits 0, (2) whether regen's compared population includes that path, and (3) whether the gate compares CONTENT, not row-name membership. A complete identity set of names is not a content agreement. RUNG FOUND AT: outside the ladder until a completing content agreement exists — silent wrongness, not a weak wall. After a ProcessExit projector and a required content compare execute, mechanically preventable: the stale file remains writable. CEILING: structurally guaranteed when membership of every committed generated `docs/` path in a content-agreement adjudicator is derived from `gunbc.generated_artifact` `committed_generated_artifacts`, so omitting the arm is a compile refusal. NEXT-RUNG TRIGGER, a capability: required-run dispatch consumes a content agreement — byte identity of generated vs committed — over every committed generated artifact whose location directory is `docs`, derived from the registry so adding a committed `docs/` path without that agreement will not compile. A trigger naming one command, one test file, or `docs_projection_gate.dag` is less than the capability and would fire while edit-only drift can still sit uncompared.) - **a field named type_name holds a type name on three arms and a fully rendered value on the fourth** (INVALID STATE: ExitClass::NotProcessExit is one spelling whose payload field is called type_name. `classify_exit` Variant arms that are not ProcessExit put ctx.resolve of the variant type symbol, or ProcessExit plus the unknown variant, into it — an actual type or variant name. The final other arm puts ctx.format_value of the non-variant value — the rendered value — into the same field. `exit_status_for_class` interpolates that field into the returned-quote slot with no second match, so every refusal path reads one name for two facts. HARM: a reader of the interpolation site infers the field's contents from its NAME and concludes a String projector yields the word String; a reader of the producer and a live stderr file concludes the markdown body is in the diagnostic. Both readings of adjacent code are correct; the name is a third surface and it lied. SPECIMEN, 2026-09-06, executed both ways. clever-otter-298 read `exit_status_for_class` and the enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` (which constructs NotProcessExit with a fixture type_name Bool and never goes through `classify_exit`) and asserted the diagnostic names the type. wise-badger-902 read the interpolation site and ruled the same. quick-heron-85 held proj3.err at 1062137 bytes. The manager then RAN the projector: EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown. The field name said type; the field held format_value. WHY THE FORK SURVIVED, and it is a section 4b evidence gap not a naming smell. `non_process_exit_refuses_rather_than_printing_and_succeeding` hand-constructs ExitClass::NotProcessExit with type_name the literal Bool and starts from an already-classified value. It never calls `classify_exit`. Nothing executing joins the field's name to its contents on the non-variant path — the only enrolled evidence feeds the field a literal that matches its name, which is exactly the input that cannot discriminate. The control's RED is unauthorable for this defect, so it was permanently green over the case that mattered and got cited as coverage. A field carrying two facts is ordinary; a field carrying two facts with a control that only ever sees one of them is why three of us read adjacent code correctly and reached three answers. THIS IS NOT `docs_markdown_projections_have_no_completing_actuator`. That row is the absence of a ProcessExit actuator and a content gate over generated `docs/*.md`. This row is a meaning fork inside `ExitClass`, reachable with no docs file in sight. Neighbour `meaning_fork` is the generic class; this instance is filed because the fork sat in the struct every refusal path reads and produced the three-way contradiction. Neighbour `diagnostic_name_mechanism_silent` is a diagnostic NAME silent about its predicate; here the FIELD name is accurate for three arms and false for the fourth. RECOGNITION RULE: when a field is named for a kind of contents, read every constructor, not the interpolation site. If one constructor writes a different kind, the name has forked. RUNG FOUND AT: mitigatable — the wrong inference is a human reading; the runtime still refuses with exit 2 and does not print-and-succeed. CEILING: structurally impossible when `NotProcessExit` cannot be constructed with a rendered value under a field named for a type — two variants, or a field named for what it actually holds. NEXT-RUNG TRIGGER, a capability: `ExitClass` distinguishes a type-name refusal from a rendered-value refusal in the type, so interpolating one as the other will not compile.) -- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed), because generic ownership is a DECLARED fact -- `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the clause has. REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed) FOR THE CLAUSE-DERIVED POPULATION, AND MECHANICALLY PREVENTABLE (2) FOR AUTHORED PARAMETERS -- the two are stated separately because a bare ceiling 3 would send a reader past the exception. Generic ownership IS a declared fact: `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the CLAUSE has. But the classification is decided by a PREDICATE over that shape, not by the clause, and an authored shape can satisfy it: the `make_param_node` producer census found EIGHT structural producers that cannot mint `pname == type-expr name`, and FOUR authored-dependent sites that can -- an author writing `fn f(Vendor: Vendor)` produces a parameter the roster predicate cannot distinguish from a generic clause. The subject of this row is the CLASSIFICATION, not the clause, so the reported rung is the minimum across both populations. WHAT STANDS BETWEEN THIS AND 3 OUTRIGHT: the authored `pname == type-expr name` shape, which no clause-side encoding can exclude. REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE ROSTER PASSED IS A UNION AND THAT HALF IS NOT OPTIONAL: the declared `` clause and the borrowed-parameter roster are two facts and neither subsumes the other -- the borrowed predicate is narrower on two axes, so passing it ALONE would reclassify a declared type param whose type expression is not a childless leaf as a concrete unresolved name, reintroducing the same misclassification through the opposite door. Deleting the absence disjunct is the repair; replacing the declared-clause predicate beside it was a second change and is not part of it. THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 588b2ba1851..683e35703bd 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3270,6 +3270,7 @@ type InhabitanceUndecidableReason | UndecidableFormalUnresolved | UndecidableProducedIdentityErased | UndecidableRefinementIntroduction + | UndecidableRefinementPeerChains type InhabitanceRefusalReason = RefusedPayloadAtParent @@ -3341,6 +3342,20 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // not perform; so the pair is reported UndecidableRefinementIntroduction -- located, per-reason, // countable -- and the deficit ranks instead of vanishing. // +// THE PEER ARM CARRIES ITS OWN NAME AND ITS OWN REASON, BECAUSE IT IS A DIFFERENT FACT AND ONE +// NAME MAY NOT HOLD TWO -- and the CONSTRUCTOR was renamed with the reason, since calling them +// sibling BRANDS encoded the same conflation one level up: the measured population is not brands. +// Narrowing is introduction: the produced type sits at or above the declared refinement on +// its own chain. Peers MEET on a shared link with neither nesting inside the other, and the +// measured population makes the difference concrete -- declared NonEmptyStr <- produced FilePath, +// GcpProjectId, Sha512DigestHex are peer predicates over one base, not introductions and not +// conflicting brands. Filing them under a reason whose text says they are introductions is the +// meaning fork DESIGN section 3 names, and it would defeat the very property this note claims: +// a mixed bucket is not located, per-reason or countable. It would also mis-aim the trigger +// below -- consulting the introduction verdict would discharge the trigger while leaving a sibling +// residue behind under a name asserting it had been handled. Review finding, cursor/auto on +// review 62043, upheld by tidy-lynx-804, 2026-09-07. +// // NEXT-RUNG TRIGGER, and it is CHEAPER than the one first written here: this relation consulting // the where-refinement predicate verdict that already decides the pair, rather than a new // elaboration fact reaching the seam. An earlier draft of this annotation claimed the predicate @@ -3364,6 +3379,39 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // the corpus at the moment that stamp was removed: HostIdentity flowing into a NonEmptyStr formal // -- widening to its own declared base, correct code -- refused as a distinct product // constructor. This is the arm that state was hiding, not a widening of scope. +// THE CHAIN IS COMPARED AT DECLARATION SITE, NOT AT SPELLING, AND THAT IS DELIBERATE. +// An earlier form of this function compared qualified_last_segment -- a module-STRIPPED last +// segment -- so two branded refinements declared in different modules sharing a last segment would +// have compared EQUAL, and RefinementWidensToDeclaredBase would have returned Inhabits for a pair +// that does not inhabit: a fail-open in the relation whose whole purpose is that some pairs must +// not be admitted. It was latent rather than live (measured: zero duplicated where-refinement type +// names across dag and src/v2), and it is fixed rather than recorded because n here is the number +// of homonymous refinement types, which is exactly the kind of number that goes from zero to one +// when someone adds a module -- DESIGN 6's bare-minimum-cost rule, where "n is small here" is not +// a time-stable fact. Review finding, tidy-lynx-804, 2026-09-07. +// +// It CONSUMES where_refinement_brand_declaration_site rather than minting a second identity: that +// is the same file-qualified identity the brand wall already uses to refuse distinct DECLARATIONS +// rather than distinct spellings, so this file now answers "are these the same type?" exactly once. +// A link whose site is Absent is DROPPED, which shortens the chain and can only turn an admission +// into a decline -- the conservative direction, never a new admission. +// +// AND THE LOOKUP-FAILURE ARM RETURNS THE EMPTY CHAIN, WHICH MAKES THE PAIR NOT THIS RELATION'S +// SUBJECT. It previously manufactured a singleton chain from the name's last segment, so a +// declaration that was never established still produced something the arms below would compare -- +// DESIGN section 5's absorbing fallback exactly: unable to compute the precise answer, substitute +// the weaker one that always produces something. Under declaration-site keying it would be worse +// than weak, because the surrogate would be an identity the subject does not have, at the one +// grain where unrelated things compare equal. ABSENCE OF IDENTITY CANNOT BE REPAIRED BY LOWERING +// THE IDENTITY GRAIN UNTIL SOMETHING COMPARES EQUAL: the arm refuses, it does not widen. +fn refinement_chain_link_identities(links: List, source_indices: Map) -> List { + links + |> map(link => where_refinement_brand_declaration_site(ty: link, source_indices: source_indices)) + |> filter(site => site != none) + |> map(site => match site { Present { value: id } => id Absent => "" }) + |> filter(id => id != "") +} + fn refinement_chain_names(n: Node, scope: InferScope) -> List { let source_indices = scope.type_env.source_indices let name = authored_name_at(source_indices: source_indices, node: n) @@ -3372,10 +3420,10 @@ fn refinement_chain_names(n: Node, scope: InferScope) -> List { } else { match lookup_type_by_name(env: scope.type_env, name: name) { Present { value: decl } => - where_refinement_chain(ty: decl, type_env: scope.type_env) - |> map(link => qualified_last_segment(name: authored_name_at(source_indices: source_indices, node: link))) - |> filter(link_name => link_name != "") - Absent => [qualified_last_segment(name: name)] + refinement_chain_link_identities( + links: where_refinement_chain(ty: decl, type_env: scope.type_env), + source_indices: source_indices) + Absent => [] } } } @@ -3383,7 +3431,7 @@ fn refinement_chain_names(n: Node, scope: InferScope) -> List { type RefinementInhabitance = RefinementWidensToDeclaredBase | RefinementNarrowsToDeclaredBrand - | RefinementSiblingBrands + | RefinementPeerChains // ABSENT MEANS "NOT THIS RELATION'S SUBJECT", NEVER "COMPATIBLE". Every guard hands the pair back // to the arms below rather than admitting it, so this can only convert a silence into a decision @@ -3406,7 +3454,7 @@ fn refinement_inhabitance(declared: Node, produced: Node, scope: InferScope) -> } else if declared_chain |> any(link => link == produced_head) { Present { value: RefinementNarrowsToDeclaredBrand } } else if declared_chain |> any(d => produced_chain |> any(p => p == d)) { - Present { value: RefinementSiblingBrands } + Present { value: RefinementPeerChains } } else { none } @@ -3451,8 +3499,8 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco Present { value: RefinementWidensToDeclaredBase } => Inhabits Present { value: RefinementNarrowsToDeclaredBrand } => InhabitanceUndecidable { reason: UndecidableRefinementIntroduction } - Present { value: RefinementSiblingBrands } => - InhabitanceUndecidable { reason: UndecidableRefinementIntroduction } + Present { value: RefinementPeerChains } => + InhabitanceUndecidable { reason: UndecidableRefinementPeerChains } Absent => if kernel_value_declared_type_mismatch( formal: declared, actual: produced, @@ -3881,6 +3929,7 @@ fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape" UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against" UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam" + UndecidableRefinementPeerChains => "refinement peer chains: the declared and produced refinements MEET on a shared link with neither nesting inside the other -- PEER PREDICATES over one base, measured as FilePath, GcpProjectId and Sha512DigestHex at NonEmptyStr, which are not brands at all -- so this is neither an introduction nor a brand conflict, and neither this seam nor the brand wall decides the pair" UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain and carries no cast to it, so whether it was INTRODUCED at that refinement is the literal-elaboration verdict for its destination, which this seam does not consult" } } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 127862c9192..8b531a4ab67 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -4586,6 +4586,7 @@ pub enum InhabitanceUndecidableReason { UndecidableFormalUnresolved, UndecidableProducedIdentityErased, UndecidableRefinementIntroduction, + UndecidableRefinementPeerChains, } #[derive( @@ -4640,6 +4641,56 @@ pub fn declared_type_position_label(position: DeclaredTypePosition, subject: Str } } +pub fn refinement_chain_link_identities( + links: Rc>>, + source_indices: Rc>>, +) -> Rc> { + Rc::new({ + let mut __result = Vec::new(); + for id in Rc::new({ + let mut __result = Vec::new(); + for site in Rc::new({ + let mut __result = Vec::new(); + for site in Rc::new({ + let mut __result = Vec::new(); + for link in links.iter().cloned() { + __result.push(where_refinement_brand_declaration_site( + link.clone(), + source_indices.clone(), + )); + } + __result + }) + .iter() + .cloned() + { + if (site.clone() != std::option::Option::None) { + __result.push(site); + } + } + __result + }) + .iter() + .cloned() + { + __result.push(match site.clone() { + Some(id) => id.clone(), + std::option::Option::None => "".to_string(), + }); + } + __result + }) + .iter() + .cloned() + { + if (id.clone() != "".to_string()) { + __result.push(id); + } + } + __result + }) +} + pub fn refinement_chain_names(n: Rc, scope: Rc) -> Rc> { { let source_indices = scope.type_env.clone().source_indices.clone(); @@ -4651,37 +4702,11 @@ pub fn refinement_chain_names(n: Rc, scope: Rc) -> Rc Rc::new({ - let mut __result = Vec::new(); - for link_name in Rc::new({ - let mut __result = Vec::new(); - for link in where_refinement_chain(decl.clone(), scope.type_env.clone()) - .iter() - .cloned() - { - __result.push(crate::v1_std_core::qualified_last_segment( - crate::v1_std_core::authored_name_at( - source_indices.clone(), - link.clone(), - ), - )); - } - __result - }) - .iter() - .cloned() - { - if (link_name.clone() != "".to_string()) { - __result.push(link_name); - } - } - __result - }), - std::option::Option::None => { - Rc::new(vec![crate::v1_std_core::qualified_last_segment( - name.clone(), - )]) - } + Some(decl) => refinement_chain_link_identities( + where_refinement_chain(decl.clone(), scope.type_env.clone()), + source_indices.clone(), + ), + std::option::Option::None => Rc::new(vec![]), } } } @@ -4694,7 +4719,7 @@ pub fn refinement_chain_names(n: Rc, scope: Rc) -> Rc Rc::new(InhabitanceVerdict::InhabitanceUndecidable { reason: InhabitanceUndecidableReason::UndecidableRefinementIntroduction, }), - Some(RefinementInhabitance::RefinementSiblingBrands) => Rc::new(InhabitanceVerdict::InhabitanceUndecidable { - reason: InhabitanceUndecidableReason::UndecidableRefinementIntroduction, + Some(RefinementInhabitance::RefinementPeerChains) => Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableRefinementPeerChains, }), std::option::Option::None => if kernel_value_declared_type_mismatch(declared.clone(), produced.clone(), scope.type_env.clone(), source_indices.clone()) { Rc::new(InhabitanceVerdict::InhabitanceRefused { @@ -5286,6 +5311,7 @@ pub fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason InhabitanceUndecidableReason::UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape".to_string(), InhabitanceUndecidableReason::UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against".to_string(), InhabitanceUndecidableReason::UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam".to_string(), + InhabitanceUndecidableReason::UndecidableRefinementPeerChains => "refinement peer chains: the declared and produced refinements MEET on a shared link with neither nesting inside the other -- PEER PREDICATES over one base, measured as FilePath, GcpProjectId and Sha512DigestHex at NonEmptyStr, which are not brands at all -- so this is neither an introduction nor a brand conflict, and neither this seam nor the brand wall decides the pair".to_string(), InhabitanceUndecidableReason::UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain and carries no cast to it, so whether it was INTRODUCED at that refinement is the literal-elaboration verdict for its destination, which this seam does not consult".to_string(), } } @@ -26697,6 +26723,8 @@ pub struct UndecidableProducedIdentityErased; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct UndecidableRefinementIntroduction; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableRefinementPeerChains; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedPayloadAtParent; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedKernelAtStructured; @@ -26709,4 +26737,4 @@ pub struct RefinementWidensToDeclaredBase; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefinementNarrowsToDeclaredBrand; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] -pub struct RefinementSiblingBrands; +pub struct RefinementPeerChains; From 64b2f7366601a0f4a9bda1c116abd3312a84bafa Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 19:36:12 +0000 Subject: [PATCH 13/17] Re-project the failure-mode row after the merge, and check by content The merge took main's side of docs/design-failure-modes.md, which is the declared repair route for that path's merge driver, but the route leaves the projection carrying main's rows and not this branch's until something re-derives it. So the row was declared and rostered and NOT projected -- the generated artifact drift the build lane refuses. Verified by CONTENT in both directions rather than by exit code: every row main carries is present, and this branch's row is present. That check is the one that matters after a MERGE, not only after a regeneration -- this is the second generated artifact on this branch lost that way (the stage0 mirrors were the first), and in both cases the loss was invisible in the merge itself: no conflict markers, no complaint, a file quietly holding the other side. The stage0 mirrors were re-derived on the merged tree in the same step and agree by content, so they are unchanged here. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- docs/design-failure-modes.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 24a8ced774c..ce67f600e24 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -171,6 +171,7 @@ The exact `RecurringFailureMode.identity` population, which no other projection - `evaluation_model_cleanup_undeclared` - `docs_markdown_projections_have_no_completing_actuator` - `type_name_field_carries_rendered_value` +- `lookup_miss_read_as_positive_classification` - `capability_arrives_outside_the_converged_path` --- @@ -358,4 +359,5 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. - **generated `docs/*.md` ledger projections have no ProcessExit actuator and no regen coverage, so an EDIT to a still-present row can sit in the authority, absent from the projection, with every completing instrument green** (INVALID STATE: `gunbc.recurring_failure_mode` is the authority; `docs/design-failure-modes.md` is the projection DESIGN.md points readers at. `expected_design_failure_modes_md` returns `String`. The refusal exits 2 with EMPTY STDOUT and interpolates the rendered value into the diagnostic on stderr: classify_exit's non-variant arm is type_name: ctx.format_value(other). Executed: wise-badger-902, EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown heading; quick-heron-85, proj3.err 1062137 bytes, same delimiters. The enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` forbids print-AND-SUCCEED, and holds. The content is therefore obtainable ONLY by scraping a half-megabyte stderr diagnostic between delimiters that are message prose (returned-open-quote and not-ProcessExit-close-quote), unversioned and enrolled by nothing. Extractable only by scraping an unversioned diagnostic — which is why the ProcessExit regen is the repair. `claim_executor --required-regen` compares only `is_compared_generated_basename` = ends_with .rs into `target/stage0-regen-candidate`. HARM: three rows can be edited in `.dag` after the last projection and nothing that exits 0 will say the markdown is stale. The meaning-fork in the field named type_name is a separate row, `type_name_field_carries_rendered_value`, not this class. SPECIMEN, measured by another lane while regenerating the projection, 2026-09-06: `instrument_answers_outside_its_domain`, `stale_claim_survives_its_own_correct_edit`, and `native_stack_recursion_unbounded_over_corpus_shaped_structure` had been edited in their authorities after the doc was last projected and had grown by 2349, 5519 and 1152 characters. Regenerating carried the repairs through. On origin/main as of 3531d30bb82 those three `.dag` files are older than `docs/design-failure-modes.md` (`81686f7bea8`), so CURRENT main is not claimed still stale; the class is that nothing completing could have said so while they were. SPECIMEN, review 58567 on gunbc#9864, on the host comment above `exit_status_for_class`: a relocation dropped the `status: refused — printing the value and exiting 0 would report success for a run whose outcome is unknown.` sentence while the comment claimed byte-for-byte equivalence. The doc lied, not the code. The sentence was restored rather than the claim weakened. That is this class on a different pair: an authority and its projection disagreeing with nothing completing to say so, and a real specimen rather than an injected literal. INCIDENT, not a fixture and not a perturbation ordered for this PR, produced by quick-heron-85 without looking for this class, commit b1c6378c6d: their authority row unresolved_callee_conflated_with_dispatched_elsewhere was UNPARSEABLE for a full commit. An authored receipt contained a quoted phrase using bare double quotes inside a double-quoted string; the string terminated early and the parser refused undefined variable this and undefined variable leaf. THE AUTHORITY DID NOT COMPILE, so docs/design-failure-modes.md kept rendering the previous vintage while presenting as current. They found it only by running the projection; reading the row does not surface the break. This PR's gate would go red on that commit because an unparseable authority makes the projector refuse — from the committed markdown alone, STALE bytes and an UNBUILDABLE authority are indistinguishable. THIS ROW IS THE DETECTOR GAP. The quoting injury that silently disabled the row they were filing is a neighbouring class they are filing separately; its next-rung trigger is string escaping in the .dag lexer. This gate makes that injury loud; it does not make it unwritable. Do not read this row as closing that class. THE IDENTITY-JOIN CORRECTION, which is the transferable part and which corrects a rule this project holds. Completeness is an identity join, not a count equality — and AN IDENTITY JOIN OVER ROW NAMES WOULD HAVE REPORTED THAT FILE COMPLETE AND CORRECT: every identity present, none missing, none extra. The drift was pure EDIT. Only a regenerated byte diff sees an edit. Worse: a first pass comparing line SETS read the three as REORDERINGS, because the changed rows shared an 80-character prefix with their old text, so the cheap check does not merely miss the drift, it manufactures a benign explanation for it. An identity join proves MEMBERSHIP, not CONTENT. THE TWO NEIGHBOURS THIS IS NOT. `authority_merges_unprotected_while_its_projection_is_guarded` is MERGE POLARITY: the generated projection is driver-bound while the hand-authored authority is not. Adjacent files, distinct defect — this row is the absence of a completing actuator or content gate, reachable with no merge in sight. `green_reported_over_a_population_the_instrument_does_not_own` is a split of actuators whose GREEN is read as covering the half it does not enumerate; that climb joined registry-projections to stage0-mirrors inside one required phase, and still does not give `gunbc run` a ProcessExit projector for the markdown, nor put `.md` in `--required-regen`. RECOGNITION RULE: when a generated file is what readers are pointed at, ask (1) whether any `ProcessExit` entry writes those exact bytes and exits 0, (2) whether regen's compared population includes that path, and (3) whether the gate compares CONTENT, not row-name membership. A complete identity set of names is not a content agreement. RUNG FOUND AT: outside the ladder until a completing content agreement exists — silent wrongness, not a weak wall. After a ProcessExit projector and a required content compare execute, mechanically preventable: the stale file remains writable. CEILING: structurally guaranteed when membership of every committed generated `docs/` path in a content-agreement adjudicator is derived from `gunbc.generated_artifact` `committed_generated_artifacts`, so omitting the arm is a compile refusal. NEXT-RUNG TRIGGER, a capability: required-run dispatch consumes a content agreement — byte identity of generated vs committed — over every committed generated artifact whose location directory is `docs`, derived from the registry so adding a committed `docs/` path without that agreement will not compile. A trigger naming one command, one test file, or `docs_projection_gate.dag` is less than the capability and would fire while edit-only drift can still sit uncompared.) - **a field named type_name holds a type name on three arms and a fully rendered value on the fourth** (INVALID STATE: ExitClass::NotProcessExit is one spelling whose payload field is called type_name. `classify_exit` Variant arms that are not ProcessExit put ctx.resolve of the variant type symbol, or ProcessExit plus the unknown variant, into it — an actual type or variant name. The final other arm puts ctx.format_value of the non-variant value — the rendered value — into the same field. `exit_status_for_class` interpolates that field into the returned-quote slot with no second match, so every refusal path reads one name for two facts. HARM: a reader of the interpolation site infers the field's contents from its NAME and concludes a String projector yields the word String; a reader of the producer and a live stderr file concludes the markdown body is in the diagnostic. Both readings of adjacent code are correct; the name is a third surface and it lied. SPECIMEN, 2026-09-06, executed both ways. clever-otter-298 read `exit_status_for_class` and the enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` (which constructs NotProcessExit with a fixture type_name Bool and never goes through `classify_exit`) and asserted the diagnostic names the type. wise-badger-902 read the interpolation site and ruled the same. quick-heron-85 held proj3.err at 1062137 bytes. The manager then RAN the projector: EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown. The field name said type; the field held format_value. WHY THE FORK SURVIVED, and it is a section 4b evidence gap not a naming smell. `non_process_exit_refuses_rather_than_printing_and_succeeding` hand-constructs ExitClass::NotProcessExit with type_name the literal Bool and starts from an already-classified value. It never calls `classify_exit`. Nothing executing joins the field's name to its contents on the non-variant path — the only enrolled evidence feeds the field a literal that matches its name, which is exactly the input that cannot discriminate. The control's RED is unauthorable for this defect, so it was permanently green over the case that mattered and got cited as coverage. A field carrying two facts is ordinary; a field carrying two facts with a control that only ever sees one of them is why three of us read adjacent code correctly and reached three answers. THIS IS NOT `docs_markdown_projections_have_no_completing_actuator`. That row is the absence of a ProcessExit actuator and a content gate over generated `docs/*.md`. This row is a meaning fork inside `ExitClass`, reachable with no docs file in sight. Neighbour `meaning_fork` is the generic class; this instance is filed because the fork sat in the struct every refusal path reads and produced the three-way contradiction. Neighbour `diagnostic_name_mechanism_silent` is a diagnostic NAME silent about its predicate; here the FIELD name is accurate for three arms and false for the fourth. RECOGNITION RULE: when a field is named for a kind of contents, read every constructor, not the interpolation site. If one constructor writes a different kind, the name has forked. RUNG FOUND AT: mitigatable — the wrong inference is a human reading; the runtime still refuses with exit 2 and does not print-and-succeed. CEILING: structurally impossible when `NotProcessExit` cannot be constructed with a rendered value under a field named for a type — two variants, or a field named for what it actually holds. NEXT-RUNG TRIGGER, a capability: `ExitClass` distinguishes a type-name refusal from a rendered-value refusal in the type, so interpolating one as the other will not compile.) +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed) FOR THE CLAUSE-DERIVED POPULATION, AND MECHANICALLY PREVENTABLE (2) FOR AUTHORED PARAMETERS -- the two are stated separately because a bare ceiling 3 would send a reader past the exception. Generic ownership IS a declared fact: `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the CLAUSE has. But the classification is decided by a PREDICATE over that shape, not by the clause, and an authored shape can satisfy it: the `make_param_node` producer census found EIGHT structural producers that cannot mint `pname == type-expr name`, and FOUR authored-dependent sites that can -- an author writing `fn f(Vendor: Vendor)` produces a parameter the roster predicate cannot distinguish from a generic clause. The subject of this row is the CLASSIFICATION, not the clause, so the reported rung is the minimum across both populations. WHAT STANDS BETWEEN THIS AND 3 OUTRIGHT: the authored `pname == type-expr name` shape, which no clause-side encoding can exclude. REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE ROSTER PASSED IS A UNION AND THAT HALF IS NOT OPTIONAL: the declared `` clause and the borrowed-parameter roster are two facts and neither subsumes the other -- the borrowed predicate is narrower on two axes, so passing it ALONE would reclassify a declared type param whose type expression is not a childless leaf as a concrete unresolved name, reintroducing the same misclassification through the opposite door. Deleting the absence disjunct is the repair; replacing the declared-clause predicate beside it was a second change and is not part of it. THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) - **a host holds a capability that no modeled path put there, so every later green on that host is uninterpretable.** INVALID STATE: a host answers ready for some capability while the convergence that is supposed to be the only way that capability arrives has not delivered it. The harm is not the capability -- it usually works -- it is that a receipt naming the host can no longer distinguish the modeled path working from a hand-run answering, and the ambiguity is permanent and travels with every future citation of that host. DISTINGUISHING FACTS, against neighbours it is easy to file as. It is not `execution_provenance_loss`: there an observation may never have run, whereas here the observation runs and reports faithfully -- the host really does hold the capability. It is not `head_landed_by_hand_before_its_own_verification_reported`: that is an artifact landing uncertified, this is DURABLE HOST STATE whose origin is unrecorded. The tell is a convergence that reports `already satisfied` for a host it never satisfied. THE STRUCTURAL CAUSE IS A CAPABILITY AUTHORIZED BY ONE MODULE, DISCLAIMED BY ANOTHER, AND EXECUTED BY NEITHER, which is DESIGN section 6's out-of-band actuation wearing convergence vocabulary. `gunbc.runner.runner_host_grants` emits EnsureSupplementaryGroupMembership and `runner_host_sudoers_content` renders permission to run its argv; `gunbc.runner_microvm_host_ready` explicitly disclaims applying it, naming the result 'a hole an operator falls into once per host, by hand'. A modeled capability with no executor is a manual step, and the roster row that grants it makes the manual step look converged. SPECIMEN A, srv2 KVM (2026-09-05): an operator ran `sudo usermod -aG kvm ghrunner` by hand, the argv already rendered at provisioning/srv2/gunbc-ghrunner.sudoers. srv2 has read kvm=writable ever since while every sibling host reads present-not-writable. The module's own annotation recording the earlier measurement went stale at that moment and COULD NOT GO RED, because DESIGN section 4c says no Accepted program reads an annotation; it was caught only because someone asked whether the grant was converged. SPECIMEN B, srv1 Firecracker (2026-09-06, this row's occasion): a session ran the modeled `runner_microvm_host_converge_wet` by hand on srv1, which installed Firecracker v1.16.1-aarch64 into the executor-owned root -- 30 paths under ~/.local/share/gunbc-firecracker, the root directory itself created by the run, so nothing pre-existed. It was digest-verified, idempotent, and spent no host grant, and it was STILL wrong: srv1 is the canary of record, and its capability would not have come from the host-image path that is supposed to own it. THE RULING, AND WHY DECLARING THE DEVIATION WAS REJECTED AS THE WEAKER ARM. The first recommendation was to keep the install and write it down. The operator overrode it: declaring makes the ambiguity legible but leaves every later srv1 receipt carrying a provenance caveat forever, whereas removing it makes the question stop existing. CONVERGENCE IS ONLY MEANINGFUL IF IT IS THE ONLY WAY STATE ARRIVES. Specimen B was reverted the same day -- the enumerated tree removed and nothing adjacent touched -- and the honest post-revert state is that srv1 cannot run a guest, which is what makes the convergence gap visible instead of papered over. RUNG FOUND AT: BELOW THE FLOOR, which is not a rung -- DESIGN section 4b puts silent wrongness outside the ladder and forbids it outright, and that is where both specimens sit. Nothing executed distinguishes a converged capability from a hand-placed one: `runner_microvm_host_ready` observes WHETHER the host holds a capability and never WHAT PLACED IT, so a hand-run host and a converged host produce byte-identical standing. The srv2 specimen is the measured proof -- the writability persisted from 2026-09-05 through every subsequent standing read, the annotation recording the pre-hand-run measurement went stale at that instant and could not go red because no Accepted program reads one, and it surfaced only when a human asked whether the grant was converged. The srv1 specimen adds that the converge itself reports success without recording that its operator was a hand session. Provenance has no mechanism at all, not a weak one. CEILING, DERIVED AND DIFFERENT FOR TWO HOST SHAPES, so a single number would be dishonest. On a host whose runtime root is reconstructed from a repository-built image at every boot, the ceiling is STRUCTURALLY IMPOSSIBLE: no persistent root survives to hold a capability the image did not place, so the invalid state has no constructor and the question stops being askable rather than being checked. On a MUTABLE persistent host the ceiling is MECHANICALLY PREVENTABLE and no higher, because an operator holding sudo can always place state -- the best reachable is an observation that refuses a capability it cannot attribute, which depends on that check executing and staying enrolled. Per DESIGN section 4b(1) a class's rung is the MINIMUM across its in-scope paths, so while any mutable host remains in the population the class's attainable ceiling is mechanically preventable, and the structural arm is available only to the hosts that stop being mutable. NEXT-RUNG TRIGGER, A CAPABILITY AND NOT AN ARTIFACT, stated at the grain of the loss. The loss is plural -- every host, every capability -- so a trigger naming one host or one grant would be satisfied while the class stayed dead. FROM BELOW-THE-FLOOR TO MECHANICALLY PREVENTABLE: a host-standing observation that reports, for each capability, the identity of the converge run that placed it, such that a capability with no attributable placing run is a typed refusal rather than a ready standing. That is the whole capability; a receipt that merely RECORDS provenance without refusing on its absence does not reach it, because the srv2 specimen was already recorded in prose and still could not go red. FROM MECHANICALLY PREVENTABLE TO STRUCTURALLY IMPOSSIBLE, and only for hosts that reach it: a runtime root reconstructed from a repository-built image on every boot, so that no capability persists that the image did not place. Naming a specific host-image pull request would be naming an artifact; what discharges this row is the property that a rebooted host cannot carry unattributed capability, whichever change delivers it. THE APPLIER IS BUILT AND UNREACHABLE, NOT MISSING, AND THE DISTINCTION DECIDES THE REPAIR. This row's first draft implied the executing half had to be written. It does not: `gunbc.executor_privileged_apply apply_executor_privileged_operations_wet` exists, elevates with `sudo -n` so an uncovered command REFUSES instead of hanging on a prompt no automated converge will answer, and renders its argv through the SAME `executor_privileged_operation_argv` the sudoers line is rendered from -- so what is permitted and what is executed are one fact by construction rather than by review. It has ZERO callers anywhere in the corpus, test modules included; the only other occurrence is a decl_ref citation. So DESIGN section 4b(2)'s three-way split lands on its strongest arm -- not `cannot climb`, not `can climb after one grounding`, but CAN CLIMB NOW WITH THE MECHANISM ALREADY WRITTEN -- and the remaining work is one wiring into the converge path. Recording this is load-bearing because the opposite reading sends the next author to build a second applier beside the first, which is precisely the argv fork that module's own annotation says it exists to prevent. AND THE REASON IT HAS NO CALLER IS ITSELF A NAMED CLASS, WHICH IS WHY THE WIRING NEVER HAPPENED. The module was not deferred pending an ownership decision and it is not a half-finished design: #10628 introduced it WHOLE, expressly to close this gap -- that commit's own account is that `executor_privileged_operation_argv` had no production consumer, that `runner_host_privileged_operations` fed only the sudoers renderer, and that this module 'closes it, and executes THE SAME argv function' -- and then landed it without the caller it was written for. That is DESIGN section 3c exactly, down to the tell that section lists in its own words: consumption described in the PR body but absent from the diff. So the repair that was supposed to end this class was itself an instance of a neighbouring one, and the two facts are the same fact: 'one wiring remains' and 'a section 3c dangling consumer' describe the same missing edge, but only the second says WHY it is missing and therefore why waiting will not produce it. REPAIR, IN PREFERENCE ORDER: bake the capability into a host image so the question cannot be asked, or close it in fleet converge. NOT an applier bolted beside the disclaiming module, and never the sudoers argv by hand -- that converts a modeled hole into a second undeclared deviation, which is how specimen A was produced. The reviewer's question for any host-capability claim: which run put it there, and can you name it. From d9fa2950690d32f0c635a7d4c76620c9859d8650 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 7 Sep 2026 19:36:46 +0000 Subject: [PATCH 14/17] chore: regenerate drifted generated artifacts (ci auto-heal) Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Rows-Repaired: docs/design-failure-modes.md lookup_miss_read_as_positive_classification Ledger-Repair-Judged: docs/design-rung-drops.md --- docs/design-failure-modes.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 24a8ced774c..ce67f600e24 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -171,6 +171,7 @@ The exact `RecurringFailureMode.identity` population, which no other projection - `evaluation_model_cleanup_undeclared` - `docs_markdown_projections_have_no_completing_actuator` - `type_name_field_carries_rendered_value` +- `lookup_miss_read_as_positive_classification` - `capability_arrives_outside_the_converged_path` --- @@ -358,4 +359,5 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. - **generated `docs/*.md` ledger projections have no ProcessExit actuator and no regen coverage, so an EDIT to a still-present row can sit in the authority, absent from the projection, with every completing instrument green** (INVALID STATE: `gunbc.recurring_failure_mode` is the authority; `docs/design-failure-modes.md` is the projection DESIGN.md points readers at. `expected_design_failure_modes_md` returns `String`. The refusal exits 2 with EMPTY STDOUT and interpolates the rendered value into the diagnostic on stderr: classify_exit's non-variant arm is type_name: ctx.format_value(other). Executed: wise-badger-902, EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown heading; quick-heron-85, proj3.err 1062137 bytes, same delimiters. The enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` forbids print-AND-SUCCEED, and holds. The content is therefore obtainable ONLY by scraping a half-megabyte stderr diagnostic between delimiters that are message prose (returned-open-quote and not-ProcessExit-close-quote), unversioned and enrolled by nothing. Extractable only by scraping an unversioned diagnostic — which is why the ProcessExit regen is the repair. `claim_executor --required-regen` compares only `is_compared_generated_basename` = ends_with .rs into `target/stage0-regen-candidate`. HARM: three rows can be edited in `.dag` after the last projection and nothing that exits 0 will say the markdown is stale. The meaning-fork in the field named type_name is a separate row, `type_name_field_carries_rendered_value`, not this class. SPECIMEN, measured by another lane while regenerating the projection, 2026-09-06: `instrument_answers_outside_its_domain`, `stale_claim_survives_its_own_correct_edit`, and `native_stack_recursion_unbounded_over_corpus_shaped_structure` had been edited in their authorities after the doc was last projected and had grown by 2349, 5519 and 1152 characters. Regenerating carried the repairs through. On origin/main as of 3531d30bb82 those three `.dag` files are older than `docs/design-failure-modes.md` (`81686f7bea8`), so CURRENT main is not claimed still stale; the class is that nothing completing could have said so while they were. SPECIMEN, review 58567 on gunbc#9864, on the host comment above `exit_status_for_class`: a relocation dropped the `status: refused — printing the value and exiting 0 would report success for a run whose outcome is unknown.` sentence while the comment claimed byte-for-byte equivalence. The doc lied, not the code. The sentence was restored rather than the claim weakened. That is this class on a different pair: an authority and its projection disagreeing with nothing completing to say so, and a real specimen rather than an injected literal. INCIDENT, not a fixture and not a perturbation ordered for this PR, produced by quick-heron-85 without looking for this class, commit b1c6378c6d: their authority row unresolved_callee_conflated_with_dispatched_elsewhere was UNPARSEABLE for a full commit. An authored receipt contained a quoted phrase using bare double quotes inside a double-quoted string; the string terminated early and the parser refused undefined variable this and undefined variable leaf. THE AUTHORITY DID NOT COMPILE, so docs/design-failure-modes.md kept rendering the previous vintage while presenting as current. They found it only by running the projection; reading the row does not surface the break. This PR's gate would go red on that commit because an unparseable authority makes the projector refuse — from the committed markdown alone, STALE bytes and an UNBUILDABLE authority are indistinguishable. THIS ROW IS THE DETECTOR GAP. The quoting injury that silently disabled the row they were filing is a neighbouring class they are filing separately; its next-rung trigger is string escaping in the .dag lexer. This gate makes that injury loud; it does not make it unwritable. Do not read this row as closing that class. THE IDENTITY-JOIN CORRECTION, which is the transferable part and which corrects a rule this project holds. Completeness is an identity join, not a count equality — and AN IDENTITY JOIN OVER ROW NAMES WOULD HAVE REPORTED THAT FILE COMPLETE AND CORRECT: every identity present, none missing, none extra. The drift was pure EDIT. Only a regenerated byte diff sees an edit. Worse: a first pass comparing line SETS read the three as REORDERINGS, because the changed rows shared an 80-character prefix with their old text, so the cheap check does not merely miss the drift, it manufactures a benign explanation for it. An identity join proves MEMBERSHIP, not CONTENT. THE TWO NEIGHBOURS THIS IS NOT. `authority_merges_unprotected_while_its_projection_is_guarded` is MERGE POLARITY: the generated projection is driver-bound while the hand-authored authority is not. Adjacent files, distinct defect — this row is the absence of a completing actuator or content gate, reachable with no merge in sight. `green_reported_over_a_population_the_instrument_does_not_own` is a split of actuators whose GREEN is read as covering the half it does not enumerate; that climb joined registry-projections to stage0-mirrors inside one required phase, and still does not give `gunbc run` a ProcessExit projector for the markdown, nor put `.md` in `--required-regen`. RECOGNITION RULE: when a generated file is what readers are pointed at, ask (1) whether any `ProcessExit` entry writes those exact bytes and exits 0, (2) whether regen's compared population includes that path, and (3) whether the gate compares CONTENT, not row-name membership. A complete identity set of names is not a content agreement. RUNG FOUND AT: outside the ladder until a completing content agreement exists — silent wrongness, not a weak wall. After a ProcessExit projector and a required content compare execute, mechanically preventable: the stale file remains writable. CEILING: structurally guaranteed when membership of every committed generated `docs/` path in a content-agreement adjudicator is derived from `gunbc.generated_artifact` `committed_generated_artifacts`, so omitting the arm is a compile refusal. NEXT-RUNG TRIGGER, a capability: required-run dispatch consumes a content agreement — byte identity of generated vs committed — over every committed generated artifact whose location directory is `docs`, derived from the registry so adding a committed `docs/` path without that agreement will not compile. A trigger naming one command, one test file, or `docs_projection_gate.dag` is less than the capability and would fire while edit-only drift can still sit uncompared.) - **a field named type_name holds a type name on three arms and a fully rendered value on the fourth** (INVALID STATE: ExitClass::NotProcessExit is one spelling whose payload field is called type_name. `classify_exit` Variant arms that are not ProcessExit put ctx.resolve of the variant type symbol, or ProcessExit plus the unknown variant, into it — an actual type or variant name. The final other arm puts ctx.format_value of the non-variant value — the rendered value — into the same field. `exit_status_for_class` interpolates that field into the returned-quote slot with no second match, so every refusal path reads one name for two facts. HARM: a reader of the interpolation site infers the field's contents from its NAME and concludes a String projector yields the word String; a reader of the producer and a live stderr file concludes the markdown body is in the diagnostic. Both readings of adjacent code are correct; the name is a third surface and it lied. SPECIMEN, 2026-09-06, executed both ways. clever-otter-298 read `exit_status_for_class` and the enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` (which constructs NotProcessExit with a fixture type_name Bool and never goes through `classify_exit`) and asserted the diagnostic names the type. wise-badger-902 read the interpolation site and ruled the same. quick-heron-85 held proj3.err at 1062137 bytes. The manager then RAN the projector: EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown. The field name said type; the field held format_value. WHY THE FORK SURVIVED, and it is a section 4b evidence gap not a naming smell. `non_process_exit_refuses_rather_than_printing_and_succeeding` hand-constructs ExitClass::NotProcessExit with type_name the literal Bool and starts from an already-classified value. It never calls `classify_exit`. Nothing executing joins the field's name to its contents on the non-variant path — the only enrolled evidence feeds the field a literal that matches its name, which is exactly the input that cannot discriminate. The control's RED is unauthorable for this defect, so it was permanently green over the case that mattered and got cited as coverage. A field carrying two facts is ordinary; a field carrying two facts with a control that only ever sees one of them is why three of us read adjacent code correctly and reached three answers. THIS IS NOT `docs_markdown_projections_have_no_completing_actuator`. That row is the absence of a ProcessExit actuator and a content gate over generated `docs/*.md`. This row is a meaning fork inside `ExitClass`, reachable with no docs file in sight. Neighbour `meaning_fork` is the generic class; this instance is filed because the fork sat in the struct every refusal path reads and produced the three-way contradiction. Neighbour `diagnostic_name_mechanism_silent` is a diagnostic NAME silent about its predicate; here the FIELD name is accurate for three arms and false for the fourth. RECOGNITION RULE: when a field is named for a kind of contents, read every constructor, not the interpolation site. If one constructor writes a different kind, the name has forked. RUNG FOUND AT: mitigatable — the wrong inference is a human reading; the runtime still refuses with exit 2 and does not print-and-succeed. CEILING: structurally impossible when `NotProcessExit` cannot be constructed with a rendered value under a field named for a type — two variants, or a field named for what it actually holds. NEXT-RUNG TRIGGER, a capability: `ExitClass` distinguishes a type-name refusal from a rendered-value refusal in the type, so interpolating one as the other will not compile.) +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed) FOR THE CLAUSE-DERIVED POPULATION, AND MECHANICALLY PREVENTABLE (2) FOR AUTHORED PARAMETERS -- the two are stated separately because a bare ceiling 3 would send a reader past the exception. Generic ownership IS a declared fact: `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the CLAUSE has. But the classification is decided by a PREDICATE over that shape, not by the clause, and an authored shape can satisfy it: the `make_param_node` producer census found EIGHT structural producers that cannot mint `pname == type-expr name`, and FOUR authored-dependent sites that can -- an author writing `fn f(Vendor: Vendor)` produces a parameter the roster predicate cannot distinguish from a generic clause. The subject of this row is the CLASSIFICATION, not the clause, so the reported rung is the minimum across both populations. WHAT STANDS BETWEEN THIS AND 3 OUTRIGHT: the authored `pname == type-expr name` shape, which no clause-side encoding can exclude. REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE ROSTER PASSED IS A UNION AND THAT HALF IS NOT OPTIONAL: the declared `` clause and the borrowed-parameter roster are two facts and neither subsumes the other -- the borrowed predicate is narrower on two axes, so passing it ALONE would reclassify a declared type param whose type expression is not a childless leaf as a concrete unresolved name, reintroducing the same misclassification through the opposite door. Deleting the absence disjunct is the repair; replacing the declared-clause predicate beside it was a second change and is not part of it. THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) - **a host holds a capability that no modeled path put there, so every later green on that host is uninterpretable.** INVALID STATE: a host answers ready for some capability while the convergence that is supposed to be the only way that capability arrives has not delivered it. The harm is not the capability -- it usually works -- it is that a receipt naming the host can no longer distinguish the modeled path working from a hand-run answering, and the ambiguity is permanent and travels with every future citation of that host. DISTINGUISHING FACTS, against neighbours it is easy to file as. It is not `execution_provenance_loss`: there an observation may never have run, whereas here the observation runs and reports faithfully -- the host really does hold the capability. It is not `head_landed_by_hand_before_its_own_verification_reported`: that is an artifact landing uncertified, this is DURABLE HOST STATE whose origin is unrecorded. The tell is a convergence that reports `already satisfied` for a host it never satisfied. THE STRUCTURAL CAUSE IS A CAPABILITY AUTHORIZED BY ONE MODULE, DISCLAIMED BY ANOTHER, AND EXECUTED BY NEITHER, which is DESIGN section 6's out-of-band actuation wearing convergence vocabulary. `gunbc.runner.runner_host_grants` emits EnsureSupplementaryGroupMembership and `runner_host_sudoers_content` renders permission to run its argv; `gunbc.runner_microvm_host_ready` explicitly disclaims applying it, naming the result 'a hole an operator falls into once per host, by hand'. A modeled capability with no executor is a manual step, and the roster row that grants it makes the manual step look converged. SPECIMEN A, srv2 KVM (2026-09-05): an operator ran `sudo usermod -aG kvm ghrunner` by hand, the argv already rendered at provisioning/srv2/gunbc-ghrunner.sudoers. srv2 has read kvm=writable ever since while every sibling host reads present-not-writable. The module's own annotation recording the earlier measurement went stale at that moment and COULD NOT GO RED, because DESIGN section 4c says no Accepted program reads an annotation; it was caught only because someone asked whether the grant was converged. SPECIMEN B, srv1 Firecracker (2026-09-06, this row's occasion): a session ran the modeled `runner_microvm_host_converge_wet` by hand on srv1, which installed Firecracker v1.16.1-aarch64 into the executor-owned root -- 30 paths under ~/.local/share/gunbc-firecracker, the root directory itself created by the run, so nothing pre-existed. It was digest-verified, idempotent, and spent no host grant, and it was STILL wrong: srv1 is the canary of record, and its capability would not have come from the host-image path that is supposed to own it. THE RULING, AND WHY DECLARING THE DEVIATION WAS REJECTED AS THE WEAKER ARM. The first recommendation was to keep the install and write it down. The operator overrode it: declaring makes the ambiguity legible but leaves every later srv1 receipt carrying a provenance caveat forever, whereas removing it makes the question stop existing. CONVERGENCE IS ONLY MEANINGFUL IF IT IS THE ONLY WAY STATE ARRIVES. Specimen B was reverted the same day -- the enumerated tree removed and nothing adjacent touched -- and the honest post-revert state is that srv1 cannot run a guest, which is what makes the convergence gap visible instead of papered over. RUNG FOUND AT: BELOW THE FLOOR, which is not a rung -- DESIGN section 4b puts silent wrongness outside the ladder and forbids it outright, and that is where both specimens sit. Nothing executed distinguishes a converged capability from a hand-placed one: `runner_microvm_host_ready` observes WHETHER the host holds a capability and never WHAT PLACED IT, so a hand-run host and a converged host produce byte-identical standing. The srv2 specimen is the measured proof -- the writability persisted from 2026-09-05 through every subsequent standing read, the annotation recording the pre-hand-run measurement went stale at that instant and could not go red because no Accepted program reads one, and it surfaced only when a human asked whether the grant was converged. The srv1 specimen adds that the converge itself reports success without recording that its operator was a hand session. Provenance has no mechanism at all, not a weak one. CEILING, DERIVED AND DIFFERENT FOR TWO HOST SHAPES, so a single number would be dishonest. On a host whose runtime root is reconstructed from a repository-built image at every boot, the ceiling is STRUCTURALLY IMPOSSIBLE: no persistent root survives to hold a capability the image did not place, so the invalid state has no constructor and the question stops being askable rather than being checked. On a MUTABLE persistent host the ceiling is MECHANICALLY PREVENTABLE and no higher, because an operator holding sudo can always place state -- the best reachable is an observation that refuses a capability it cannot attribute, which depends on that check executing and staying enrolled. Per DESIGN section 4b(1) a class's rung is the MINIMUM across its in-scope paths, so while any mutable host remains in the population the class's attainable ceiling is mechanically preventable, and the structural arm is available only to the hosts that stop being mutable. NEXT-RUNG TRIGGER, A CAPABILITY AND NOT AN ARTIFACT, stated at the grain of the loss. The loss is plural -- every host, every capability -- so a trigger naming one host or one grant would be satisfied while the class stayed dead. FROM BELOW-THE-FLOOR TO MECHANICALLY PREVENTABLE: a host-standing observation that reports, for each capability, the identity of the converge run that placed it, such that a capability with no attributable placing run is a typed refusal rather than a ready standing. That is the whole capability; a receipt that merely RECORDS provenance without refusing on its absence does not reach it, because the srv2 specimen was already recorded in prose and still could not go red. FROM MECHANICALLY PREVENTABLE TO STRUCTURALLY IMPOSSIBLE, and only for hosts that reach it: a runtime root reconstructed from a repository-built image on every boot, so that no capability persists that the image did not place. Naming a specific host-image pull request would be naming an artifact; what discharges this row is the property that a rebooted host cannot carry unattributed capability, whichever change delivers it. THE APPLIER IS BUILT AND UNREACHABLE, NOT MISSING, AND THE DISTINCTION DECIDES THE REPAIR. This row's first draft implied the executing half had to be written. It does not: `gunbc.executor_privileged_apply apply_executor_privileged_operations_wet` exists, elevates with `sudo -n` so an uncovered command REFUSES instead of hanging on a prompt no automated converge will answer, and renders its argv through the SAME `executor_privileged_operation_argv` the sudoers line is rendered from -- so what is permitted and what is executed are one fact by construction rather than by review. It has ZERO callers anywhere in the corpus, test modules included; the only other occurrence is a decl_ref citation. So DESIGN section 4b(2)'s three-way split lands on its strongest arm -- not `cannot climb`, not `can climb after one grounding`, but CAN CLIMB NOW WITH THE MECHANISM ALREADY WRITTEN -- and the remaining work is one wiring into the converge path. Recording this is load-bearing because the opposite reading sends the next author to build a second applier beside the first, which is precisely the argv fork that module's own annotation says it exists to prevent. AND THE REASON IT HAS NO CALLER IS ITSELF A NAMED CLASS, WHICH IS WHY THE WIRING NEVER HAPPENED. The module was not deferred pending an ownership decision and it is not a half-finished design: #10628 introduced it WHOLE, expressly to close this gap -- that commit's own account is that `executor_privileged_operation_argv` had no production consumer, that `runner_host_privileged_operations` fed only the sudoers renderer, and that this module 'closes it, and executes THE SAME argv function' -- and then landed it without the caller it was written for. That is DESIGN section 3c exactly, down to the tell that section lists in its own words: consumption described in the PR body but absent from the diff. So the repair that was supposed to end this class was itself an instance of a neighbouring one, and the two facts are the same fact: 'one wiring remains' and 'a section 3c dangling consumer' describe the same missing edge, but only the second says WHY it is missing and therefore why waiting will not produce it. REPAIR, IN PREFERENCE ORDER: bake the capability into a host image so the question cannot be asked, or close it in fleet converge. NOT an applier bolted beside the disclaiming module, and never the sudoers argv by hand -- that converts a modeled hole into a second undeclared deviation, which is how specimen A was produced. The reviewer's question for any host-capability claim: which run put it there, and can you name it. From 150c78c4e53e4d8ddbf99e11c6a0bfe1f16b3e4d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 20:48:56 +0000 Subject: [PATCH 15/17] No arm compares a closure population to a literal; no chain is compacted Two review findings, both correct, both falsifying something this diff asserted about itself. EVERY ARM IS NOW A DIFFERENCE, INCLUDING THE ZEROES AND THE ONES. The nominal_opaque arm asserted `DeclaredTypeNotInhabited == 1` -- a merge-blocking equality against a population the census draws from the fixture's whole import closure, with a bare literal recording today's tree. This file's own standing note says why that cannot be an oracle, seventy lines above the arm that did it. Re-authored against a Secret-free partner differing only on the nominal_opaque axis. Re-checking the others against the same question rather than trusting an earlier pass found the same shape in the `== 0` conjuncts, which look fixture-local and are not: refusal counts happen to be zero across that closure today, which is the coincidence that makes the absolute form look safe and is not a time-stable fact. All five arms are now differences between two fixtures. (Review 62112, claude/opus.) A CHAIN WITH ANY UNIDENTIFIED LINK IS DISCARDED, NOT COMPACTED. The annotation claimed dropping a link "can only turn an admission into a decline -- the conservative direction, never a new admission." THAT CLAIM IS FALSE, and the counterexample is the HEAD: drop the declared side's head and its BASE is promoted to head, so the produced chain contains it, the widening arm fires, and a value is admitted at a strictly narrower declared refinement it was never shown to inhabit. Compaction is not the conservative direction; it is the widening one, one link up -- the same move the sibling paragraph forbids by name. The function now returns the empty chain unless every link is identified, and the annotation states what is true rather than what was convenient. (Review 62130, claude/opus.) The whole required floor is green locally with both in. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- ...e_inhabitance_direct_call_witness_test.dag | 22 ++++++- src/v1/04_infer.dag | 18 +++++- src/v1/stage0/src/v1_compiler_infer.rs | 57 +++++++++++-------- 3 files changed, 66 insertions(+), 31 deletions(-) diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index f004919914c..a81d4b1f02e 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -335,6 +335,14 @@ test fn w_a_phantom_type_argument_with_identical_representation_is_still_separat // literal would be a measurement of the current tree copied into the assertion, which DESIGN 5 // refuses by name. Each control below is therefore a PAIR differing on exactly one axis, so the // shared corpus contribution cancels and only the axis is measured. +// +// AND THAT INCLUDES THE ZEROES AND THE ONES. An arm reading `== 0` or `== 1` looks fixture-local +// and is not: the census carries the fixture's whole import closure, so any unrelated change in +// std.types that adds or removes a row of the class flips it, and the literal records TODAY'S TREE +// rather than the mutation the arm claims to discriminate. Refusal counts happen to be zero across +// that closure at this writing, which is exactly the coincidence that makes the absolute form look +// safe -- and is not a time-stable fact. So EVERY arm below is a difference between two fixtures, +// with no exception for the ones whose number is small. Review 62112, claude/opus. data refinement_baseline_source: String = "module probe_refinement_baseline\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { 0 }\n" data probe_exact_refinement_source: String = "module probe_exact_refinement\nimport std.types { NonEmptyStr, Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host_x: HostIdentity = \"srv1\" as HostIdentity\nfn takes_host(s: HostIdentity) -> Int { 1 }\nfn probe() -> Int { takes_host(s: probe_host_x) }\n" @@ -344,7 +352,8 @@ data probe_exact_brand_source: String = "module probe_exact_brand\nimport std.ty data refinement_widening_source: String = "module probe_refinement_widening\nimport std.types { NonEmptyStr, Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host: HostIdentity = \"srv1\" as HostIdentity\nfn takes_base(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_base(s: probe_host) }\n" test fn w_a_branded_refinement_at_its_own_declared_base_inhabits() -> Bool { - violation_count(source: refinement_widening_source, wanted: "DeclaredTypeNotInhabited") == 0 + violation_count(source: refinement_widening_source, wanted: "DeclaredTypeNotInhabited") + == violation_count(source: probe_exact_refinement_source, wanted: "DeclaredTypeNotInhabited") && violation_count(source: refinement_widening_source, wanted: "DeclaredTypeInhabitanceUndecided") == violation_count(source: probe_exact_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") } @@ -375,7 +384,8 @@ test fn w_a_branded_refinement_at_its_own_declared_base_inhabits() -> Bool { data brand_horizontal_at_argument_source: String = "module probe_brand_horizontal_at_argument\nimport std.types { Int }\nimport product.placement_supply { HostIdentity, PhysicalAssetIdentity }\ndata probe_host2: HostIdentity = \"srv1\" as HostIdentity\nfn takes_asset(x: PhysicalAssetIdentity) -> Int { 1 }\nfn probe() -> Int { takes_asset(x: probe_host2) }\n" test fn w_two_distinct_brands_over_one_base_are_not_refused_twice() -> Bool { - violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeNotInhabited") == 0 + violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeNotInhabited") + == violation_count(source: probe_exact_brand_source, wanted: "DeclaredTypeNotInhabited") && violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeInhabitanceUndecided") > violation_count(source: probe_exact_brand_source, wanted: "DeclaredTypeInhabitanceUndecided") && violation_count(source: brand_horizontal_at_argument_source, wanted: "TypeMismatch") @@ -393,10 +403,16 @@ test fn w_two_distinct_brands_over_one_base_are_not_refused_twice() -> Bool { // nominal_opaque alias, Secret's chain would become [Secret, String] and would meet NonEmptyStr's // [NonEmptyStr, String] at String -- a sibling pair, which this relation declines. So the // discriminating mutation produces exactly one UNDECIDED here, and asserting zero reds on it. +// THE Secret-FREE PARTNER, differing on exactly the nominal_opaque axis: same module shape, same +// imports, same formal, same call -- the produced value is a NonEmptyStr rather than a Secret. Its +// refusal count is the closure's contribution, so the difference is this fixture's own refusal. +data nominal_opaque_partner_source: String = "module probe_nominal_opaque_partner\nimport std.types { NonEmptyStr, Int }\ndata probe_plain: NonEmptyStr = \"shh\" as NonEmptyStr\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: probe_plain) }\n" + data nominal_opaque_not_grounded_source: String = "module probe_nominal_opaque_not_grounded\nimport std.types { NonEmptyStr, Secret, Int }\ndata probe_secret: Secret = \"shh\" as Secret\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: probe_secret) }\n" test fn w_a_nominal_opaque_alias_does_not_ground_through_the_refinement_chain() -> Bool { - violation_count(source: nominal_opaque_not_grounded_source, wanted: "DeclaredTypeNotInhabited") == 1 + violation_count(source: nominal_opaque_not_grounded_source, wanted: "DeclaredTypeNotInhabited") + > violation_count(source: nominal_opaque_partner_source, wanted: "DeclaredTypeNotInhabited") } // THE POSITIVE CENSUS ARM IS NOT AUTHORABLE HERE, AND THAT IS THE FINDING RATHER THAN AN OMISSION. diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 683e35703bd..4aa2527cac9 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3393,8 +3393,15 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // It CONSUMES where_refinement_brand_declaration_site rather than minting a second identity: that // is the same file-qualified identity the brand wall already uses to refuse distinct DECLARATIONS // rather than distinct spellings, so this file now answers "are these the same type?" exactly once. -// A link whose site is Absent is DROPPED, which shortens the chain and can only turn an admission -// into a decline -- the conservative direction, never a new admission. +// A CHAIN WITH ANY UNIDENTIFIED LINK IS NOT ESTABLISHED AT ALL, AND THE WHOLE CHAIN IS DISCARDED. +// An earlier form of this function COMPACTED the list, dropping unidentified links, on the claim +// that a shorter chain can only turn an admission into a decline. THAT CLAIM IS FALSE, and the +// counterexample is the HEAD: drop the declared side's head and its BASE is promoted to head, so +// the produced chain contains it, RefinementWidensToDeclaredBase fires, and a value is admitted at +// a strictly narrower declared refinement it was never shown to inhabit -- a silent admission +// manufactured out of a missing identity, which is the same move the paragraph below forbids by +// name. Compaction is not the conservative direction; it is the widening one, one link up. +// Review 62130, claude/opus, 2026-09-07. // // AND THE LOOKUP-FAILURE ARM RETURNS THE EMPTY CHAIN, WHICH MAKES THE PAIR NOT THIS RELATION'S // SUBJECT. It previously manufactured a singleton chain from the name's last segment, so a @@ -3405,11 +3412,16 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // grain where unrelated things compare equal. ABSENCE OF IDENTITY CANNOT BE REPAIRED BY LOWERING // THE IDENTITY GRAIN UNTIL SOMETHING COMPARES EQUAL: the arm refuses, it does not widen. fn refinement_chain_link_identities(links: List, source_indices: Map) -> List { - links + let identified = links |> map(link => where_refinement_brand_declaration_site(ty: link, source_indices: source_indices)) |> filter(site => site != none) |> map(site => match site { Present { value: id } => id Absent => "" }) |> filter(id => id != "") + if (identified |> count) == (links |> count) { + identified + } else { + [] + } } fn refinement_chain_names(n: Node, scope: InferScope) -> List { diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 8b531a4ab67..4ab5a0cf745 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -4645,50 +4645,57 @@ pub fn refinement_chain_link_identities( links: Rc>>, source_indices: Rc>>, ) -> Rc> { - Rc::new({ - let mut __result = Vec::new(); - for id in Rc::new({ + { + let identified = Rc::new({ let mut __result = Vec::new(); - for site in Rc::new({ + for id in Rc::new({ let mut __result = Vec::new(); for site in Rc::new({ let mut __result = Vec::new(); - for link in links.iter().cloned() { - __result.push(where_refinement_brand_declaration_site( - link.clone(), - source_indices.clone(), - )); + for site in Rc::new({ + let mut __result = Vec::new(); + for link in links.iter().cloned() { + __result.push(where_refinement_brand_declaration_site( + link.clone(), + source_indices.clone(), + )); + } + __result + }) + .iter() + .cloned() + { + if (site.clone() != std::option::Option::None) { + __result.push(site); + } } __result }) .iter() .cloned() { - if (site.clone() != std::option::Option::None) { - __result.push(site); - } + __result.push(match site.clone() { + Some(id) => id.clone(), + std::option::Option::None => "".to_string(), + }); } __result }) .iter() .cloned() { - __result.push(match site.clone() { - Some(id) => id.clone(), - std::option::Option::None => "".to_string(), - }); + if (id.clone() != "".to_string()) { + __result.push(id); + } } __result - }) - .iter() - .cloned() - { - if (id.clone() != "".to_string()) { - __result.push(id); - } + }); + if ((identified.clone().len() as i64) == (links.clone().len() as i64)) { + identified.clone() + } else { + Rc::new(vec![]) } - __result - }) + } } pub fn refinement_chain_names(n: Rc, scope: Rc) -> Rc> { From 774a0489378635336bf029845ad59bacf7e60ca5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 7 Sep 2026 21:21:33 +0000 Subject: [PATCH 16/17] One principle, stated once: absence of identity is not repairable by degrading what you compare Both arms in this relation reached for a weaker comparison when the precise one was unavailable -- one lowering the GRAIN to a spelling, one shortening the CHAIN past a link it could not identify -- and both were assessed as conservative in general while reversing direction at a particular position. That is one principle with two instances, not two patches, and the file now says it once above the function that carries both rather than twice inside it. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_infer.dag | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 4aa2527cac9..9dd2ded4bbc 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3403,14 +3403,20 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // name. Compaction is not the conservative direction; it is the widening one, one link up. // Review 62130, claude/opus, 2026-09-07. // +// ONE PRINCIPLE, TWO POSITIONS, AND IT IS WORTH STATING ONCE RATHER THAN PATCHING TWICE: +// ABSENCE OF IDENTITY IS NOT REPAIRABLE BY DEGRADING WHAT YOU COMPARE. Both arms below reached +// for a weaker comparison when the precise one was unavailable -- one lowering the GRAIN to a +// spelling, one shortening the CHAIN past a link it could not identify -- and both were assessed +// as conservative in general while reversing direction at a particular position. A failure arm +// refuses; it does not widen, and it does not compare something else instead. +// // AND THE LOOKUP-FAILURE ARM RETURNS THE EMPTY CHAIN, WHICH MAKES THE PAIR NOT THIS RELATION'S // SUBJECT. It previously manufactured a singleton chain from the name's last segment, so a // declaration that was never established still produced something the arms below would compare -- // DESIGN section 5's absorbing fallback exactly: unable to compute the precise answer, substitute // the weaker one that always produces something. Under declaration-site keying it would be worse // than weak, because the surrogate would be an identity the subject does not have, at the one -// grain where unrelated things compare equal. ABSENCE OF IDENTITY CANNOT BE REPAIRED BY LOWERING -// THE IDENTITY GRAIN UNTIL SOMETHING COMPARES EQUAL: the arm refuses, it does not widen. +// grain where unrelated things compare equal. So the arm refuses rather than substituting. fn refinement_chain_link_identities(links: List, source_indices: Map) -> List { let identified = links |> map(link => where_refinement_brand_declaration_site(ty: link, source_indices: source_indices)) From 3b563e7c21a1f425ecf310c426bf7e3d2a439ad8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 8 Sep 2026 00:01:03 +0000 Subject: [PATCH 17/17] Resolve chain identity through lookup_type_for; unavailable on any miss Blocker 2 of the REQUEST_CHANGES on 774a048937, verified in source before accepting and not argued. THE KEY WAS NOT AN IDENTITY. where_refinement_chain falls back to the raw base node on a lookup miss, and where_refinement_brand_declaration_site keys on ident_span -- which default_ident_span sets from the node's OWN name_span at construction. So on a fallback link the key was a REFERENCE-site key, wrong in both directions at once: two distinct declarations referenced from one file key EQUAL, one declaration referenced from two files keys UNEQUAL. A key that both merges distinct things and splits identical ones is not an identity, and there is no tightening that repairs one, so the fallback is gone rather than sharpened. THE ENTRY POINT RESOLVED BY SPELLING. refinement_chain_names took authored_name_at and then looked the type up BY NAME, so a node already carrying identity was rebound by spelling at the head of a relation whose whole subject is spelling collision. Both it and every link now resolve through lookup_type_for, the node-aware authority that matches node.ident first, and the site is taken from the resolved DECLARATION. THE COMPLETENESS CHECK MEASURED THE WRONG THING. The count equality compared ident_span PRESENCE, which every named node has, so it proved the links were NAMED and could not fail for the reason it existed. It now compares RESOLVED links, and any miss discards the whole chain: the pair is not this relation's subject. Refuse, never widen -- no falling through to the raw node. Also drops the where-refinement blinding of the nominal-product arm, which was unnecessary: the refinement arm runs first, so widening is admitted before that arm is consulted, and every control stays green without it. It is NOT claimed to repair the disjoint-pair case from review 62172 -- measured on both sides, main's compiler does not refuse that pair either, so that defect is pre-existing and is being enrolled separately rather than attributed here. The whole required floor is green locally. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF --- src/v1/04_infer.dag | 110 +++++++++++++------------ src/v1/stage0/src/v1_compiler_infer.rs | 53 ++++++------ 2 files changed, 82 insertions(+), 81 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 9dd2ded4bbc..e79aa4f3633 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3379,47 +3379,61 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) // the corpus at the moment that stamp was removed: HostIdentity flowing into a NonEmptyStr formal // -- widening to its own declared base, correct code -- refused as a distinct product // constructor. This is the arm that state was hiding, not a widening of scope. -// THE CHAIN IS COMPARED AT DECLARATION SITE, NOT AT SPELLING, AND THAT IS DELIBERATE. -// An earlier form of this function compared qualified_last_segment -- a module-STRIPPED last -// segment -- so two branded refinements declared in different modules sharing a last segment would -// have compared EQUAL, and RefinementWidensToDeclaredBase would have returned Inhabits for a pair -// that does not inhabit: a fail-open in the relation whose whole purpose is that some pairs must -// not be admitted. It was latent rather than live (measured: zero duplicated where-refinement type -// names across dag and src/v2), and it is fixed rather than recorded because n here is the number -// of homonymous refinement types, which is exactly the kind of number that goes from zero to one -// when someone adds a module -- DESIGN 6's bare-minimum-cost rule, where "n is small here" is not -// a time-stable fact. Review finding, tidy-lynx-804, 2026-09-07. +// THE CHAIN IS COMPARED AT RESOLVED DECLARATION IDENTITY, AND IT IS UNAVAILABLE ON ANY MISS. +// Three corrections live here, each from a review and each falsifying something an earlier form of +// this function asserted about itself. // -// It CONSUMES where_refinement_brand_declaration_site rather than minting a second identity: that -// is the same file-qualified identity the brand wall already uses to refuse distinct DECLARATIONS -// rather than distinct spellings, so this file now answers "are these the same type?" exactly once. -// A CHAIN WITH ANY UNIDENTIFIED LINK IS NOT ESTABLISHED AT ALL, AND THE WHOLE CHAIN IS DISCARDED. -// An earlier form of this function COMPACTED the list, dropping unidentified links, on the claim -// that a shorter chain can only turn an admission into a decline. THAT CLAIM IS FALSE, and the -// counterexample is the HEAD: drop the declared side's head and its BASE is promoted to head, so -// the produced chain contains it, RefinementWidensToDeclaredBase fires, and a value is admitted at -// a strictly narrower declared refinement it was never shown to inhabit -- a silent admission -// manufactured out of a missing identity, which is the same move the paragraph below forbids by -// name. Compaction is not the conservative direction; it is the widening one, one link up. -// Review 62130, claude/opus, 2026-09-07. +// FIRST, it compared qualified_last_segment -- a module-STRIPPED last segment -- so two homonymous +// refinements would have compared EQUAL and widening would have admitted a pair that does not +// inhabit. This file already suffered that class: a second HostIdentity was minted beside +// product.placement_supply's and did not surface as a duplicate declaration. Only one survives +// because the incident was CLEANED UP, not avoided. // -// ONE PRINCIPLE, TWO POSITIONS, AND IT IS WORTH STATING ONCE RATHER THAN PATCHING TWICE: -// ABSENCE OF IDENTITY IS NOT REPAIRABLE BY DEGRADING WHAT YOU COMPARE. Both arms below reached -// for a weaker comparison when the precise one was unavailable -- one lowering the GRAIN to a -// spelling, one shortening the CHAIN past a link it could not identify -- and both were assessed -// as conservative in general while reversing direction at a particular position. A failure arm -// refuses; it does not widen, and it does not compare something else instead. +// SECOND, it keyed on where_refinement_brand_declaration_site applied to the node in hand, and +// ident_span IS NOT DECLARATION PROVENANCE: default_ident_span sets it from the node's OWN +// name_span at construction, so on a link that did not resolve the key was a REFERENCE-site key. +// That is wrong in BOTH directions at once -- two distinct declarations referenced from one file +// key EQUAL, one declaration referenced from two files keys UNEQUAL -- and a key that can both +// merge distinct things and split identical ones is not an identity at all. There is no tightening +// that repairs a non-identity, so the fallback is gone rather than sharpened: every link is +// resolved through lookup_type_for, the NODE-AWARE authority that matches node.ident first, and the +// site is taken from the resolved DECLARATION. // -// AND THE LOOKUP-FAILURE ARM RETURNS THE EMPTY CHAIN, WHICH MAKES THE PAIR NOT THIS RELATION'S -// SUBJECT. It previously manufactured a singleton chain from the name's last segment, so a -// declaration that was never established still produced something the arms below would compare -- -// DESIGN section 5's absorbing fallback exactly: unable to compute the precise answer, substitute -// the weaker one that always produces something. Under declaration-site keying it would be worse -// than weak, because the surrogate would be an identity the subject does not have, at the one -// grain where unrelated things compare equal. So the arm refuses rather than substituting. -fn refinement_chain_link_identities(links: List, source_indices: Map) -> List { +// THIRD, the entry point took authored_name_at and then looked the type up BY NAME, so a node that +// already carried identity was rebound by spelling at the head of a relation whose whole subject is +// spelling collision. It resolves through lookup_type_for too. +// +// AND THE COMPLETENESS CHECK NOW MEASURES RESOLUTION RATHER THAN NAMING. The count equality below +// used to compare ident_span PRESENCE, which every named node has, so it proved the links were +// NAMED and could not fail for the reason it existed. It now compares RESOLVED links, and any miss +// discards the whole chain: the pair is simply not this relation's subject. +// +// WHY DISCARD RATHER THAN COMPACT, since the earlier form dropped unidentified links and claimed +// that was conservative. IT IS NOT, and the counterexample is the HEAD: drop the declared side's +// head and its BASE is promoted to head, so the produced chain contains it, the widening arm fires, +// and a value is admitted at a strictly narrower declared refinement it was never shown to inhabit. +// Compaction is not the conservative direction; it is the widening one, one link up. +// +// ONE PRINCIPLE, THREE POSITIONS, AND IT IS WORTH STATING ONCE RATHER THAN PATCHING THREE TIMES: +// ABSENCE OF IDENTITY IS NOT REPAIRABLE BY DEGRADING WHAT YOU COMPARE. Every arm above reached for +// a weaker comparison when the precise one was unavailable -- lowering the GRAIN to a spelling, +// shortening the CHAIN past a link it could not identify, substituting a REFERENCE for a +// declaration -- and each was assessed as conservative in general while reversing direction at some +// particular position. A failure arm refuses; it does not widen, and it does not compare something +// else instead. Reviews 62130 and 62172, and GitHub review 5135375330, 2026-09-07. + +fn refinement_chain_link_identity(link: Node, type_env: TypeEnv) -> String? { + match lookup_type_for(env: type_env, node: link) { + Present { value: declaration } => + where_refinement_brand_declaration_site( + ty: declaration, source_indices: type_env.source_indices) + Absent => Absent + } +} + +fn refinement_chain_link_identities(links: List, type_env: TypeEnv) -> List { let identified = links - |> map(link => where_refinement_brand_declaration_site(ty: link, source_indices: source_indices)) + |> map(link => refinement_chain_link_identity(link: link, type_env: type_env)) |> filter(site => site != none) |> map(site => match site { Present { value: id } => id Absent => "" }) |> filter(id => id != "") @@ -3431,18 +3445,12 @@ fn refinement_chain_link_identities(links: List, source_indices: Map List { - let source_indices = scope.type_env.source_indices - let name = authored_name_at(source_indices: source_indices, node: n) - if name == "" { - [] - } else { - match lookup_type_by_name(env: scope.type_env, name: name) { - Present { value: decl } => - refinement_chain_link_identities( - links: where_refinement_chain(ty: decl, type_env: scope.type_env), - source_indices: source_indices) - Absent => [] - } + match lookup_type_for(env: scope.type_env, node: n) { + Present { value: declaration } => + refinement_chain_link_identities( + links: where_refinement_chain(ty: declaration, type_env: scope.type_env), + type_env: scope.type_env) + Absent => [] } } @@ -3762,9 +3770,7 @@ fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope Present { value: decl } => let peeled = peel_nominal_alias_identity( n: decl, env: scope.type_env, module_name: scope.module_name) - if is_where_refinement_type(ty: peeled) { - "" - } else if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } + if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } Absent => "" } } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 4ab5a0cf745..02aaf22693c 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -4641,9 +4641,19 @@ pub fn declared_type_position_label(position: DeclaredTypePosition, subject: Str } } +pub fn refinement_chain_link_identity(link: Rc, type_env: Rc) -> Option { + match crate::v1_compiler_infer_env::lookup_type_for(type_env.clone(), link.clone()) { + Some(declaration) => where_refinement_brand_declaration_site( + declaration.clone(), + type_env.source_indices.clone(), + ), + std::option::Option::None => std::option::Option::None, + } +} + pub fn refinement_chain_link_identities( links: Rc>>, - source_indices: Rc>>, + type_env: Rc, ) -> Rc> { { let identified = Rc::new({ @@ -4655,9 +4665,9 @@ pub fn refinement_chain_link_identities( for site in Rc::new({ let mut __result = Vec::new(); for link in links.iter().cloned() { - __result.push(where_refinement_brand_declaration_site( + __result.push(refinement_chain_link_identity( link.clone(), - source_indices.clone(), + type_env.clone(), )); } __result @@ -4699,23 +4709,12 @@ pub fn refinement_chain_link_identities( } pub fn refinement_chain_names(n: Rc, scope: Rc) -> Rc> { - { - let source_indices = scope.type_env.clone().source_indices.clone(); - let name = crate::v1_std_core::authored_name_at(source_indices.clone(), n.clone()); - if (name.clone() == "".to_string()) { - Rc::new(vec![]) - } else { - match crate::v1_compiler_infer_env::lookup_type_by_name( - scope.type_env.clone(), - name.clone(), - ) { - Some(decl) => refinement_chain_link_identities( - where_refinement_chain(decl.clone(), scope.type_env.clone()), - source_indices.clone(), - ), - std::option::Option::None => Rc::new(vec![]), - } - } + match crate::v1_compiler_infer_env::lookup_type_for(scope.type_env.clone(), n.clone()) { + Some(declaration) => refinement_chain_link_identities( + where_refinement_chain(declaration.clone(), scope.type_env.clone()), + scope.type_env.clone(), + ), + std::option::Option::None => Rc::new(vec![]), } } @@ -5133,16 +5132,12 @@ pub fn nominal_product_head_name_if_declared_product( scope.type_env.clone(), scope.module_name.clone(), ); - if is_where_refinement_type(peeled.clone()) { - "".to_string() + if ((peeled.connective.clone() == Connective::Conj) + && ((peeled.children.clone().len() as i64) > 0)) + { + name.clone() } else { - if ((peeled.connective.clone() == Connective::Conj) - && ((peeled.children.clone().len() as i64) > 0)) - { - name.clone() - } else { - "".to_string() - } + "".to_string() } } std::option::Option::None => "".to_string(),