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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,9 @@ data lowering_accessor_collapses_a_sequence_operand: RecurringFailureMode = Recu
"WHAT KEEPS THE TRIGGER OPEN, stated at the capability's grain: the Optional accessor `body_lower_operand_ref_optional` -- and so `body_lower_named_arg_value_optional` above it -- answers Absent, not a located refusal, when an operator expression under it is unreadable. No element is dropped any more, but an unread operand is still indistinguishable from `not an operand` to an Optional caller. The trigger stands as written: the accessor returns the whole value OR A LOCATED REFUSAL. A sibling found by the same probe and NOT in this class: a call argument inside an if-arm (`if c { g(p: x) } else { .. }`) reaches no reference site on main or after this repair; its reader is `body_lower_if_arm_operand_optional`, not the operator tower.",
"EXPOSED, NOT REGRESSED: THE OTHER CONSUMERS OF THE SAME READER (2026-09-24). Closing the narrowing arm (gunbc#12145) was correct, and it was proven only at the consumer it was about (`v2.test.claim.namespace_xl0.sequence_operand_resolve_refusal`). The same reader, `body_lower_operand_ref_optional`, was also the value reader of three other consumers in `v2.compiler.body_lowering_fold`: call arguments, match scrutinees, and `body_lower_operator_operand`'s fallback. For a call or a lambda there, the narrowing had been this row's silent truncation (`match f(x)` read as `f`, `f => body` read as `f`). Once it was closed, they refused their whole module (`call_argument_unread`, `match_arm_navigation_refused`, `operator_operand_unread`: 85 (cause, path) identities added and 4 removed across the native lane). This is a PAIRING / COVERAGE GAP, not a regression: the change's claims were reachability witnesses for one consumer and were read as completeness evidence for the reader, and no control exercised the reader's other consumers. The repair reads call arguments and scrutinees through `body_lower_value_lowered` (gunbc#12173, `v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal`); gunbc#12198 adds the production-route SHAPE control (`v2.test.claim.namespace_xl0.value_position_whole_read`: callee, arity and argument at the authored atom) as a permanent regression control. Operator operands are gunbc#12194's. A LAMBDA ARGUMENT REMAINS THE FRONTIER: carrying its shell whole was tried and measured (srv1, 8fc9f27377) -- the module normalizes but the parameter is unscoped at resolve, a refusal moved rather than repaired -- so it was dropped, and the two lambda claims are enrolled expected-red in `v2.workflow.floor_expected_red` `floor_expected_red_chunk_lambda_argument_lowering` until lambda lowering lands. An operator-operand fallback added in the same episode was DEAD: no bare, parenthesised or mutated operand ever reached it (M1/M2 green), and removing it regressed none of the six operand files -- a second instance of this row's lesson that a claim must assert its route, not only its answer",
"TWO LESSONS FROM THE WHOLE-ROUTE IDENTITY DIFF THAT FOUND IT. (1) An identity diff cannot tell INTRODUCED from EXPOSED. Of the rows new relative to the parent, two (`dag/std/keyed_roster.dag`, `src/v2/std/compilers/sugar.dag`, head `parse_grammar_choice_overlap_residue`) had never refused: the narrowing had silently read a parse residue. Most of the others were parent `parse_g0_tokens_remain` files moving to a LATER stage (`else_less_if_unlowered`, `list_literal_unlowered`, `wrapper_retention_not_normalized`) once they parsed. Each row must be classified against the parent's (cause, path) set, not counted. (2) A net count hides the structure: 11 -> 92 was reported as 81 new refusals, while at identity grain it was 85 added and 4 removed, with cause SWAPS on the same path (`02_parse.dag`, `target_model.dag` and `grammar.dag` removed under wrapper_retention and re-added under match_arm_navigation)",
"THE INSTRUMENT'S OWN GAP: the native lane's driver rows carry (fatal_reason, head_reason, path) and NO LOCUS. So a file refusal names a file and a cause but not the construct, and every consumer of the diff (the author, the manager, the operator) must re-derive the span by rerunning a front end over that file; three rows in this episode could not be attributed from the rows alone. A span-less file refusal is DESIGN section 5's located-diagnostic obligation unmet at the reporting boundary, and the identity diff is sufficient as a regression control only once its rows carry the refusal's locus"
"THE INSTRUMENT'S OWN GAP: the native lane's driver rows carry (fatal_reason, head_reason, path) and NO LOCUS. So a file refusal names a file and a cause but not the construct, and every consumer of the diff (the author, the manager, the operator) must re-derive the span by rerunning a front end over that file; three rows in this episode could not be attributed from the rows alone. A span-less file refusal is DESIGN section 5's located-diagnostic obligation unmet at the reporting boundary, and the identity diff is sufficient as a regression control only once its rows carry the refusal's locus",

"THE SAME COLLAPSE AT THE STATEMENT GRAIN (2026-09-24, adhoc-9d86ad93-96c, gunbc#12230). `v2.compiler.body_lowering_fold` `body_lower_try_statement_spine` routed a statement spine to `body_lower_stmt_spine` only when it was LET-HEADED, and handed every other multi-statement spine back to the expression walker, which answered with ONE statement and dropped the rest: `fn f() -> Int { 1 \\n 2 }` normalized clean. It is this row's shape one level up -- a sequence read as a proper part of itself, with no refusal -- and the claim that guards it, `v2.test.claim.body_lowering.statement_let_bind` `unbound_statement_prefix_refuses_holds`, was RED ON MAIN, visible only because MQ-6's reference-conservation admission then refused the dropped statement as `conservation_reason_dropped_reference` (srv1, neat-boar-16, round 1). REPAIR: gunbc#12221 (`body_lower_stmt_spine_has_successor`) admits every spine with a following statement, so a non-binding head refuses as `body_lowering_reason_statement_precedes_without_binding`, located. THE COVERAGE LESSON IS THE WITHHOLD: no required lane ran the claim, because its module matched no required-gate selector AND all six of its identities were withheld as cost debt in `v2.workflow.floor_cost_debt`, so even an admitted run would have declined them. gunbc#12230 removes the six from the cost-debt roster and admits the module in `v2.workflow.required_floor` `required_gate_authored_modules`. The discriminating evidence is a mutant restoring the let-headed guard, which must turn that required floor red on `unbound_statement_prefix_refuses_holds`."
],

evidence: [],
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
module gunbc.recurring_failure_mode.unresolved_signature_type_surfaces_as_a_distant_field_read_cascade

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data unresolved_signature_type_surfaces_as_a_distant_field_read_cascade: RecurringFailureMode = RecurringFailureMode {
identity: "unresolved_signature_type_surfaces_as_a_distant_field_read_cascade" as NonEmptyStr,

receipts: [
"INVALID STATE: a function signature names a type the declaring module never resolves (here `Optional<Node>` in a module with no import of v2.std.optional), and the module is still EVALUATED. The unresolved annotation silently becomes the error type, so every value bound out of that return (a `Present { value: x }` payload) is error-typed, and the run fails only when something reads a FIELD of it: `x.kind` refuses as `type error: error type cascade` at the READ, possibly many calls away from the annotation that caused it. A value that is only passed on to a typed parameter never trips it, so two helpers with the same defect can differ in whether they fail.",

"SPECIMEN, found 2026-09-24 by adhoc-9d86ad93-96c (gunbc#12230). v2.test.claim.body_lowering.wave1_gate1_b1_bare_call_helpers declared `fn wave1_gate1_b1_find_named_fn_arrow_body(root: Node, fn_lexeme: String) -> Optional<Node>` with no Optional import. v2.test.long.wave1_gate1_b1_bare_call_body_producer_witness wave1_gate1_b1_bare_call_lowers_to_transform_witness_holds failed on srv1 claim_batch with `runtime error [type-error]: type error: error type cascade` at the helper's `body.kind`. The sibling a1 helper had the same missing import and PASSED, because it never field-reads a payload it binds out of Optional; gunbc#12230 adds the import there too, so the defect is not left latent for the next field read.",

"THE ISOLATING PROBE. Renaming the binder (`body` to `found`) did not change the failure, which ruled out the name, and the helper already returned `tree.root`, which ruled out the NormalizedTree-for-Node confusion that had reddened the same helper. Adding `import v2.std.optional { Absent, Optional, Present }` and changing nothing else made the same read return TRANSFORM and the witness PASS (srv1, neat-boar-16, b93a0eec0a). So the import alone flips the verdict.",

"WHAT IS NOT YET ESTABLISHED, stated so this row does not inflate its rung: whether seed resolve emitted an unresolved-type diagnostic for the annotation that the claim_batch route did not treat as blocking, or emitted none at all. gunbc.recurring_failure_mode bare_reference_channel_declines_a_pull_in_silence records a compile route that DOES refuse `unresolved type <Name>` for a bare type reference in a module with imports, so the refusal exists on at least one path. This class is the path on which it did not stop the run. Rung found at: below the ladder (silent until an unrelated read, and located at the wrong place).",

"ATTAINABLE CEILING: structurally guaranteed. Whether a type name in a signature resolves is decidable from the module and its imports, so no Accepted program, and no module a claim route evaluates, should carry an unresolved annotation. NEXT-RUNG TRIGGER, at capability grain: seed resolve refuses an unbound type name in a function signature AT THE ANNOTATION, with a typed, located diagnostic, on EVERY route that evaluates the module, including the claim_batch and required-floor claim routes, so no route evaluates a function whose declared types did not resolve. Its discriminating RED is fixture source: a module declaring `fn f() -> Optional<Int>` without the import, whose refusal must name `Optional` at that signature. The positive control is the same module with the import, accepted.",

"RECOGNITION RULE: `error type cascade` at a field read whose base is a pattern-bound or let-bound value is a signature-resolution defect upstream until proven otherwise. Read the declared return type of the function that produced the value, and check that the declaring module imports every type it names, before suspecting the value or the field.",
],

evidence: [],
}
10 changes: 9 additions & 1 deletion src/v2/compiler/body_lowering_fold.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5928,7 +5928,15 @@ fn body_lower_stmt_spine_has_successor(spine: Node) -> Bool {
Present { value: rest } =>
match body_lower_stmt_spine_head_optional(spine: rest) {
Absent => false
Present { value: _ } => true
Present { value: _ } =>
match body_lower_stmt_spine_head_optional(spine: spine) {
Absent => false
Present { value: head } =>
match body_lower_statement_let_captured_optional(stmt: head) {
Absent => false
Present { value: _ } => true
}
}
}
}
}
Expand Down
29 changes: 17 additions & 12 deletions src/v2/test/claim/body_lowering/statement_let_bind_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ import v2.compiler.reference_conservation_admission {
StatementLetBinder,
conservation_subject_of_text,
conserved_normalize,
conserved_normalize_of_text,
no_explained_drops
}
import std.algebra { Cons, Empty, FreeMonoid }
Expand All @@ -31,14 +30,6 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
// one, which is exactly the silent-wrong-answer class the refusal exists to prevent. It does not
// retire when the capability lands; it is the standing control that the capability stayed honest.

fn normalize_outcome(src: String) -> String {
match conserved_normalize_of_text(path: "statement_let_bind_subject", text: src, explained: no_explained_drops()) {
Rejected { diagnostics: ds } => symbol_lexeme(sym: ds.head.reason)
Accepted { value: _, diagnostics: _ } => "ACCEPTED"
}
}


// A statement-form let's binder -- and, when it has one, its type annotation -- is lost by
// lowering today, pinned by
// v2.test.claim.namespace_xl0.reference_conservation a_statement_let_binder_is_reported_dropped_holds.
Expand Down Expand Up @@ -79,12 +70,18 @@ test fn statement_let_chain_lowers_holds() -> Bool {
}

test fn unbound_statement_prefix_refuses_holds() -> Bool {
normalize_outcome(src: unbound_statement_prefix_source)
== "body_lowering_reason_statement_precedes_without_binding"
match conserved_normalize(subject: unbound_prefix_subject(), explained: no_explained_drops()) {
Rejected { diagnostics: ds } =>
symbol_lexeme(sym: ds.head.reason) == "body_lowering_reason_statement_precedes_without_binding"
Accepted { value: _, diagnostics: _ } => false
}
}

test fn single_statement_body_unchanged_holds() -> Bool {
normalize_outcome(src: single_statement_source) == "ACCEPTED"
match conserved_normalize(subject: single_statement_subject(), explained: no_explained_drops()) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
}

test fn let_in_form_unchanged_holds() -> Bool {
Expand Down Expand Up @@ -115,6 +112,14 @@ fn let_in_form_subject() -> ReferenceConservationSubject {
conservation_subject_of_text(path: "statement_let_bind_subject", text: let_in_form_source)
}

fn unbound_prefix_subject() -> ReferenceConservationSubject {
conservation_subject_of_text(path: "statement_let_bind_subject", text: unbound_statement_prefix_source)
}

fn single_statement_subject() -> ReferenceConservationSubject {
conservation_subject_of_text(path: "statement_let_bind_subject", text: single_statement_source)
}

fn typed_let_subject() -> ReferenceConservationSubject {
conservation_subject_of_text(path: "statement_let_bind_subject", text: typed_statement_let_source)
}
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module v2.test.claim.body_lowering.wave1_gate1_a1_symbol_index_helpers

import v2.compiler.reference_conservation_admission { conserved_normalize_of_text, no_explained_drops }
import v2.std.optional { Absent, Optional, Present }


data wave1_gate1_a1_add_module_source: String = "module add_probe\n\nfn add(x: Int, y: Int) -> Int { x + y }\n"
Expand Down Expand Up @@ -44,7 +45,7 @@ fn wave1_gate1_a1_parsed_add_module() -> Optional<Node> {
fn wave1_gate1_a1_normalized_add_module() -> Optional<Node> {
match conserved_normalize_of_text(path: "wave1_gate1_a1_add_probe_file", text: wave1_gate1_a1_add_module_source, explained: no_explained_drops()) {
Rejected { diagnostics: _ } => Absent
Accepted { value: tree, diagnostics: _ } => Present { value: tree }
Accepted { value: tree, diagnostics: _ } => Present { value: tree.root }
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ module v2.test.claim.body_lowering.wave1_gate1_b1_bare_call_helpers

import v2.compiler.reference_conservation_admission { conserved_normalize_of_text, no_explained_drops }
import v2.extdeps.languages.dag { qualified_name_from_module_node }
import v2.std.optional { Absent, Optional, Present }


data wave1_gate1_b1_bare_call_module_source: String = "module wave1_gate1_b1_bare_call\n\nfn helper(x: Int) -> Int { x + x }\n\nfn caller(x: Int) -> Int { helper(x) }\n"
Expand Down Expand Up @@ -35,7 +36,7 @@ fn wave1_gate1_b1_resolve_source(source: String) -> Bool {
fn wave1_gate1_b1_normalized_module(source: String) -> Optional<Node> {
match conserved_normalize_of_text(path: "wave1_gate1_b1_probe_file", text: source, explained: no_explained_drops()) {
Rejected { diagnostics: _ } => Absent
Accepted { value: tree, diagnostics: _ } => Present { value: tree }
Accepted { value: tree, diagnostics: _ } => Present { value: tree.root }
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/v2/workflow/floor_cost_debt.dag
Original file line number Diff line number Diff line change
Expand Up @@ -717,7 +717,7 @@ fn floor_cost_debt_proven_chunk_05() -> List<String> {
}

fn floor_cost_debt_proven_chunk_06() -> List<String> {
Cons { head: "v2.test.claim.body_lowering.statement_let_bind.let_in_form_unchanged_holds", tail: Cons { head: "v2.test.claim.body_lowering.statement_let_bind.single_statement_body_unchanged_holds", tail: Cons { head: "v2.test.claim.body_lowering.statement_let_bind.statement_let_chain_lowers_holds", tail: Cons { head: "v2.test.claim.body_lowering.statement_let_bind.statement_let_then_reference_lowers_holds", tail: Cons { head: "v2.test.claim.body_lowering.statement_let_bind.typed_statement_let_lowers_holds", tail: Cons { head: "v2.test.claim.body_lowering.statement_let_bind.unbound_statement_prefix_refuses_holds", tail: Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_gate.a_readable_clean_subject_is_established_clean", tail: Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_gate.an_unreadable_subject_is_not_established_rather_than_clean", tail: Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_gate.red_control_planted_copy_still_alarms", tail: Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_standing.malformed_source_reports_tokenization_rejection", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_absent_concept_is_false", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_coproduct_arms_live", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_enumeration_nonempty", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_fieldref_self_projection", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_local_record_enumerated", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_qualified_concept_self_projection", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_blocks_infer_behind_a_failed_resolve", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_infer_row_for_a_resolvable_candidate_is_determinate", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_locates_a_resolve_death_at_resolve", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_resolve_contract_accepts_a_resolvable_candidate", tail: Empty {} } } } } } } } } } } } } } } } } } } } }
Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_gate.a_readable_clean_subject_is_established_clean", tail: Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_gate.an_unreadable_subject_is_not_established_rather_than_clean", tail: Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_gate.red_control_planted_copy_still_alarms", tail: Cons { head: "v2.test.claim.complexity.accumulator_copy_roster_standing.malformed_source_reports_tokenization_rejection", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_absent_concept_is_false", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_coproduct_arms_live", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_enumeration_nonempty", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_fieldref_self_projection", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_local_record_enumerated", tail: Cons { head: "v2.test.claim.concept_index_enumeration.witness_qualified_concept_self_projection", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_blocks_infer_behind_a_failed_resolve", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_infer_row_for_a_resolvable_candidate_is_determinate", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_locates_a_resolve_death_at_resolve", tail: Cons { head: "v2.test.claim.dag_acceptance.acceptance_resolve_contract_accepts_a_resolvable_candidate", tail: Empty {} } } } } } } } } } } } } } }
}

fn floor_cost_debt_proven_chunk_07() -> List<String> {
Expand Down
Loading
Loading