From 7692619dc7aacfaf2195a0e7475dc04463554518 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 25 Sep 2026 17:57:36 +0000 Subject: [PATCH 1/5] WIP: body lowering carries a value or arm refusal instead of re-reading it as navigation Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/body_lowering_fold.dag | 122 ++++++++++++------------- 1 file changed, 59 insertions(+), 63 deletions(-) diff --git a/src/v2/compiler/body_lowering_fold.dag b/src/v2/compiler/body_lowering_fold.dag index ce60b8e39b8..fdccf50b35c 100644 --- a/src/v2/compiler/body_lowering_fold.dag +++ b/src/v2/compiler/body_lowering_fold.dag @@ -3620,7 +3620,7 @@ fn body_lower_value_lowered(node: Node) -> Outcome> { outcome_with_diagnostics(value: optional_present(value: lowered), diagnostics: d) Absent => body_lower_body_subtree_lower(captured: raw) } - Rejected { diagnostics: _ } => body_lower_body_subtree_lower(captured: raw) + Rejected { diagnostics: r } => Rejected { diagnostics: r } } } } @@ -4965,6 +4965,32 @@ fn body_lower_pattern_lowered(pattern_capture: Node) -> Outcome { } } +// ONE ARM-BODY READER FOR EVERY ARM POSITION. An arm body is a value, so it is read by +// body_lower_value_lowered, whose refusal is carried with its own cause and locus; only a body that +// reader returns Absent for falls to the operand reader. The sequence and spine navigations used to +// differ here: the spine arms (every arm the sequence capture does not reach) went to the operand +// reader alone, so a refused value came back Absent and surfaced as match_arm_navigation_refused +// with the arm as its only locus. +fn body_lower_match_arm_wired(pat_node: Node, body_capture: Node, arm_capture: Node) -> Outcome { + match body_lower_value_lowered(node: body_capture) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: lowered_opt, diagnostics: d } => + match lowered_opt { + Present { value: body } => + outcome_with_diagnostics( + value: body_lower_match_arm_wire(pat_node: pat_node, body: body), + diagnostics: d + ) + Absent => + match body_lower_match_arm_body_optional(body_capture: body_capture) { + Present { value: body } => + outcome_accepted(value: body_lower_match_arm_wire(pat_node: pat_node, body: body)) + Absent => body_lower_match_arm_navigation_reject(arm_capture: arm_capture) + } + } + } +} + // THE ARM BODY IS LOWERED BY THE BODY WALKER FIRST. The arm-body reader // (body_lower_match_arm_body_optional) is an operand reader: it answers a nested `match` or `if` // in arm position with that form's first atom (`dag_token_kw_if`), which is how every arm of @@ -4982,25 +5008,11 @@ fn body_lower_match_arm_wire_from_sequence(stripped: Node) -> Outcome { Accepted { value: pat_node, diagnostics: _ } => match body_lower_match_arm_body_capture_optional(stripped: stripped) { Present { value: body_capture } => - match body_lower_value_lowered(node: body_capture) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: lowered_opt, diagnostics: d } => - match lowered_opt { - Present { value: body } => - outcome_with_diagnostics( - value: body_lower_match_arm_wire(pat_node: pat_node, body: body), - diagnostics: d - ) - Absent => - match body_lower_match_arm_body_optional(body_capture: body_capture) { - Present { value: body } => - outcome_accepted( - value: body_lower_match_arm_wire(pat_node: pat_node, body: body) - ) - Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) - } - } - } + body_lower_match_arm_wired( + pat_node: pat_node, + body_capture: body_capture, + arm_capture: stripped + ) Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) } } @@ -5018,19 +5030,11 @@ fn body_lower_match_arm_wire_from_sequence(stripped: Node) -> Outcome { if arrow == ^dag_token_fat_arrow { match body_lower_match_spine_right(spine: right) { Present { value: body_capture } => - match body_lower_match_arm_body_optional( - body_capture: body_capture - ) { - Present { value: body } => - outcome_accepted( - value: body_lower_match_arm_wire( - pat_node: pat_node, - body: body - ) - ) - Absent => - body_lower_match_arm_navigation_reject(arm_capture: stripped) - } + body_lower_match_arm_wired( + pat_node: pat_node, + body_capture: body_capture, + arm_capture: stripped + ) Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped) } @@ -5045,19 +5049,11 @@ fn body_lower_match_arm_wire_from_sequence(stripped: Node) -> Outcome { match node_atom_identity_optional(node: after_pattern.left) { Present { value: arrow } => if arrow == ^dag_token_fat_arrow { - match body_lower_match_arm_body_optional( - body_capture: after_pattern.right - ) { - Present { value: body } => - outcome_accepted( - value: body_lower_match_arm_wire( - pat_node: pat_node, - body: body - ) - ) - Absent => - body_lower_match_arm_navigation_reject(arm_capture: stripped) - } + body_lower_match_arm_wired( + pat_node: pat_node, + body_capture: after_pattern.right, + arm_capture: stripped + ) } else { body_lower_match_arm_navigation_reject(arm_capture: stripped) } @@ -5083,25 +5079,25 @@ fn body_lower_is_match_arm_navigate_emitted(emitted: Symbol) -> Bool { || body_lower_is_pass_through_emitted(emitted: emitted) } -fn body_lower_match_arm_from_comma_repeat_elem(repeat_elem: Node) -> Outcome { - let stripped = body_lower_deep_unwrap_optional(node: repeat_elem) - match sugar_sequence_pair_optional(node: stripped) { - Present { value: pair } => - body_lower_wire_match_arm_capture( - arm_capture: body_lower_postfix_optional_unwrap(node: pair.right) - ) - Absent => - body_lower_wire_match_arm_capture(arm_capture: stripped) - } -} - +// AN ARM, OR A COMMA-REPEAT ELEMENT CARRYING ONE, DECIDED BY SHAPE BEFORE ANY ARM IS WIRED. A +// repeat element is Seq(optional-comma, arm), and its left side is a separator +// (body_lower_match_arm_repeat_elem_is_separator); an arm's left side is its pattern, which never +// is. The arm is wired once and its Rejected stands. This reader used to wire the node as an arm +// first and, on ANY refusal, discard the diagnostics and retry it as a repeat element: an arm that +// refused for its own located cause (a list literal in its body) was re-read under the wrong shape +// and surfaced as match_arm_navigation_refused with the arm as its only locus. fn body_lower_extract_comma_list_arm_head(node: Node) -> Outcome { let stripped = body_lower_deep_unwrap_optional(node: node) - match body_lower_wire_match_arm_capture(arm_capture: stripped) { - Rejected { diagnostics: _ } => - body_lower_match_arm_from_comma_repeat_elem(repeat_elem: stripped) - Accepted { value: arm, diagnostics: d } => - Accepted { value: arm, diagnostics: d } + match sugar_sequence_pair_optional(node: stripped) { + Present { value: pair } => + if body_lower_match_arm_repeat_elem_is_separator(node: pair.left) { + body_lower_wire_match_arm_capture( + arm_capture: body_lower_postfix_optional_unwrap(node: pair.right) + ) + } else { + body_lower_wire_match_arm_capture(arm_capture: stripped) + } + Absent => body_lower_wire_match_arm_capture(arm_capture: stripped) } } From 1e19a6932ebfe59d575473eaf08f910cc5ad021b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 25 Sep 2026 19:19:01 +0000 Subject: [PATCH 2/5] Witness: a match arm's own refusal cause survives in every arm position; share its front end Co-Authored-By: Claude Opus 5.5 (1M context) --- .../match_arm_refusal_carried_test.dag | 163 ++++++++++++++++++ src/v2/workflow/floor_pure_producer_share.dag | 5 + 2 files changed, 168 insertions(+) create mode 100644 src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag diff --git a/src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag b/src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag new file mode 100644 index 00000000000..47a7860a8e6 --- /dev/null +++ b/src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag @@ -0,0 +1,163 @@ +module v2.test.claim.namespace_xl0.match_arm_refusal_carried + +import v2.compiler.compile { NativeTestContext, native_test_context_from_ingest } +import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest } +import v2.std.algebra { fold_list } +import v2.std.artifact { Artifact, SourceFile } +import v2.std.cross_tree.import_model { DagTree } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Symbol } +import v2.std.optional { Absent, Optional, Present, optional_absent, optional_present } +import v2.std.text { String } +import std.algebra { Cons, Empty } +import extdeps.communication.medium { Lossless, Medium } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// AN ARM THAT REFUSES FOR ITS OWN CAUSE KEEPS THAT CAUSE, IN EVERY ARM POSITION. +// +// THE SUBJECT IS THE NATIVE LANE'S FRONT END: which fatal cause a module's file refusal carries. +// v2.compiler.body_lowering_fold body_lower_extract_comma_list_arm_head used to wire a repeat +// element as an arm and, on ANY refusal, discard the diagnostics and retry the same node as a +// comma-repeat element. The first arm does not pass through that reader, so a list literal there +// refused located; in the second arm, or in a comma-separated arm, the list literal's own refusal +// was discarded and the retry under the wrong shape answered body_lowering_reason_match_arm_navigation_refused +// with the arm as its only locus. The reader now decides the shape first (a separator on the left is +// a repeat element; an arm's left is its pattern) and wires the arm once, so its Rejected stands. +// +// The two red modules are the list literal in a second arm, on its own line and comma-separated. +// The controls: the same literal in the FIRST arm refuses under the same cause on both sides (so +// the red claims assert the cause the first arm already reached, not a new one); and the same two +// layouts with no refusable value are not refused at all, so the shape decision did not stop +// reading ordinary arms. +data marc_second_arm_list_source: String = "module v2.test.marc_second_arm_list\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List) -> List { acc }\n\nfn marc_probe(b: Bool, acc: List) -> List {\n match b {\n false => acc\n true => marc_g(acc: [])\n }\n}\n" + +data marc_comma_arm_list_source: String = "module v2.test.marc_comma_arm_list\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List) -> List { acc }\n\nfn marc_probe(b: Bool, acc: List) -> List {\n match b { false => acc, true => marc_g(acc: []) }\n}\n" + +data marc_first_arm_list_source: String = "module v2.test.marc_first_arm_list\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List) -> List { acc }\n\nfn marc_probe(b: Bool, acc: List) -> List {\n match b {\n true => marc_g(acc: [])\n false => acc\n }\n}\n" + +data marc_second_arm_ctl_source: String = "module v2.test.marc_second_arm_ctl\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List) -> List { acc }\n\nfn marc_probe(b: Bool, acc: List) -> List {\n match b {\n false => acc\n true => marc_g(acc: acc)\n }\n}\n" + +data marc_comma_arm_ctl_source: String = "module v2.test.marc_comma_arm_ctl\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List) -> List { acc }\n\nfn marc_probe(b: Bool, acc: List) -> List {\n match b { false => acc, true => marc_g(acc: acc) }\n}\n" + +fn marc_read(source: String, id: Symbol, unit: Symbol, path: String) -> DagSourceReadWitness { + DagSourceReadWitness { + source: Medium { carried: source, fidelity: Lossless }, + artifact: Artifact { kind: SourceFile, id: id, file_path: path }, + compilation_unit: unit, + source_root: DagTree + } +} + +data marc_ingest: SourceRootIngest = Cons { + head: marc_read(source: marc_second_arm_list_source, id: ^marc_second_arm_list_artifact, unit: ^marc_second_arm_list_cu, path: "src/v2/test/fixture/namespace_xl0/marc_second_arm_list.dag"), + tail: Cons { + head: marc_read(source: marc_comma_arm_list_source, id: ^marc_comma_arm_list_artifact, unit: ^marc_comma_arm_list_cu, path: "src/v2/test/fixture/namespace_xl0/marc_comma_arm_list.dag"), + tail: Cons { + head: marc_read(source: marc_first_arm_list_source, id: ^marc_first_arm_list_artifact, unit: ^marc_first_arm_list_cu, path: "src/v2/test/fixture/namespace_xl0/marc_first_arm_list.dag"), + tail: Cons { + head: marc_read(source: marc_second_arm_ctl_source, id: ^marc_second_arm_ctl_artifact, unit: ^marc_second_arm_ctl_cu, path: "src/v2/test/fixture/namespace_xl0/marc_second_arm_ctl.dag"), + tail: Cons { + head: marc_read(source: marc_comma_arm_ctl_source, id: ^marc_comma_arm_ctl_artifact, unit: ^marc_comma_arm_ctl_cu, path: "src/v2/test/fixture/namespace_xl0/marc_comma_arm_ctl.dag"), + tail: Empty + } + } + } + } + } + +// ONE FRONT END FOR EVERY CLAIM. The stored value is one verdict per module: the fatal cause of its +// file refusal, or that it was not refused. No context, Node or closure is kept. +type MarcVerdict + = MarcNotRefused + | MarcFileRefused { fatal_reason: Symbol } + +type MarcOutcomes + = MarcContextRefused + | MarcOutcomesDecided { + second_arm_list: MarcVerdict + comma_arm_list: MarcVerdict + first_arm_list: MarcVerdict + second_arm_ctl: MarcVerdict + comma_arm_ctl: MarcVerdict + } + +fn marc_verdict_in(context: NativeTestContext, unit: Symbol) -> MarcVerdict { + fold_list( + xs: context.file_refusals, + empty: MarcNotRefused, + cons: fn(acc, refusal) { + if refusal.path == unit { MarcFileRefused { fatal_reason: refusal.fatal_reason } } else { acc } + } + ) +} + +fn marc_outcomes() -> MarcOutcomes { + match native_test_context_from_ingest(ingest: marc_ingest) { + Rejected { diagnostics: _ } => MarcContextRefused + Accepted { value: context, diagnostics: _ } => + MarcOutcomesDecided { + second_arm_list: marc_verdict_in(context: context, unit: ^marc_second_arm_list_cu), + comma_arm_list: marc_verdict_in(context: context, unit: ^marc_comma_arm_list_cu), + first_arm_list: marc_verdict_in(context: context, unit: ^marc_first_arm_list_cu), + second_arm_ctl: marc_verdict_in(context: context, unit: ^marc_second_arm_ctl_cu), + comma_arm_ctl: marc_verdict_in(context: context, unit: ^marc_comma_arm_ctl_cu) + } + } +} + +fn marc_is_list_literal_refused(v: MarcVerdict) -> Bool { + match v { + MarcFileRefused { fatal_reason: r } => r == ^body_lowering_reason_list_literal_unlowered + MarcNotRefused => false + } +} + +fn marc_is_not_refused(v: MarcVerdict) -> Bool { + match v { + MarcNotRefused => true + MarcFileRefused { fatal_reason: _ } => false + } +} + +test fn a_list_literal_in_a_second_arm_refuses_under_its_own_cause() -> Bool { + match marc_outcomes() { + MarcOutcomesDecided { second_arm_list: v, comma_arm_list: _, first_arm_list: _, second_arm_ctl: _, comma_arm_ctl: _ } => + marc_is_list_literal_refused(v: v) + MarcContextRefused => false + } +} + +test fn a_list_literal_in_a_comma_separated_arm_refuses_under_its_own_cause() -> Bool { + match marc_outcomes() { + MarcOutcomesDecided { second_arm_list: _, comma_arm_list: v, first_arm_list: _, second_arm_ctl: _, comma_arm_ctl: _ } => + marc_is_list_literal_refused(v: v) + MarcContextRefused => false + } +} + +test fn a_list_literal_in_a_first_arm_refuses_under_the_same_cause() -> Bool { + match marc_outcomes() { + MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: v, second_arm_ctl: _, comma_arm_ctl: _ } => + marc_is_list_literal_refused(v: v) + MarcContextRefused => false + } +} + +test fn a_second_arm_with_no_refusable_value_is_not_refused() -> Bool { + match marc_outcomes() { + MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: _, second_arm_ctl: v, comma_arm_ctl: _ } => + marc_is_not_refused(v: v) + MarcContextRefused => false + } +} + +test fn a_comma_separated_arm_with_no_refusable_value_is_not_refused() -> Bool { + match marc_outcomes() { + MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: _, second_arm_ctl: _, comma_arm_ctl: v } => + marc_is_not_refused(v: v) + MarcContextRefused => false + } +} diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 2185e25c17b..81668435cdd 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -608,6 +608,10 @@ import v2.std.collection { List } // THE XL-2 IF-ARM AND STATEMENT-SPINE ROW IS THE SAME GROUND AT THIRTEEN SPECIMENS: // v2.test.claim.namespace_xl0.if_arm_and_statement_lowering_refusal iasl_outcomes drives one front // end over thirteen inline modules and stores one verdict arm per module, portable for the same reason. +// THE XL-2 MATCH-ARM REFUSAL ROW IS THE SAME GROUND AT FIVE SPECIMENS: +// v2.test.claim.namespace_xl0.match_arm_refusal_carried marc_outcomes drives one front end over five +// inline modules and stores one verdict arm per module (a fatal cause Symbol or not-refused), +// portable for the same reason. // THE XL-2 BOUND-VALUE RESOLVE ROW IS THE SAME GROUND AT ELEVEN SPECIMENS: // v2.test.claim.namespace_xl0.bound_value_resolve_refusal bvr_outcomes drives one front end over // eleven inline modules and stores one verdict arm per module, portable for the same reason. @@ -680,6 +684,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal.cav_outcomes", "v2.test.claim.namespace_xl0.if_arm_and_statement_lowering_refusal.iasl_outcomes", "v2.test.claim.namespace_xl0.bound_value_resolve_refusal.bvr_outcomes", + "v2.test.claim.namespace_xl0.match_arm_refusal_carried.marc_outcomes", "v2.test.cli.v2_native_cli.cli_probe_trailing_outcome", "v2.test.emit.closure_emit_arrow_body_refusal.arrow_body_probe_verdict", "v2.test.emit.closure_emit_arrow_body_refusal.arrow_body_mixed_probe_verdict", From 5e2eb7efec92a8ad3b25fe203d3e956477b6a9c0 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 25 Sep 2026 19:49:35 +0000 Subject: [PATCH 3/5] Witness claims are relational: arm position must not change the cause (survives #12208 deleting the list-literal cause) Co-Authored-By: Claude Opus 5.5 (1M context) --- .../match_arm_refusal_carried_test.dag | 52 +++++++++++++------ 1 file changed, 37 insertions(+), 15 deletions(-) diff --git a/src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag b/src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag index 47a7860a8e6..0d7a01fb3e4 100644 --- a/src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag +++ b/src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag @@ -27,9 +27,8 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // with the arm as its only locus. The reader now decides the shape first (a separator on the left is // a repeat element; an arm's left is its pattern) and wires the arm once, so its Rejected stands. // -// The two red modules are the list literal in a second arm, on its own line and comma-separated. -// The controls: the same literal in the FIRST arm refuses under the same cause on both sides (so -// the red claims assert the cause the first arm already reached, not a new one); and the same two +// The two red modules are a list literal in a second arm, on its own line and comma-separated. +// The controls: the same literal in the FIRST arm refuses located on both sides; and the same two // layouts with no refusable value are not refused at all, so the shape decision did not stop // reading ordinary arms. data marc_second_arm_list_source: String = "module v2.test.marc_second_arm_list\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List) -> List { acc }\n\nfn marc_probe(b: Bool, acc: List) -> List {\n match b {\n false => acc\n true => marc_g(acc: [])\n }\n}\n" @@ -108,10 +107,33 @@ fn marc_outcomes() -> MarcOutcomes { } } -fn marc_is_list_literal_refused(v: MarcVerdict) -> Bool { +// THE CLAIMS ARE RELATIONAL. The subject is that arm POSITION does not change the cause, so the +// second-arm and comma-arm modules must refuse under the SAME cause the first-arm module refuses +// under, and that cause must not be the navigation cause. No claim names the list literal's own +// cause: gunbc#12208 lowers list literals and deletes that cause, and a claim pinned to it would read +// that landing as this defect's return. The specimen is still a list literal because it is the +// shape the corpus specimen (gunbc.accelerator_demo_eval) refused on; if a later change lowers it, +// a_first_arm_specimen_still_refuses_located goes red by name and the specimen value is replaced, +// which is the honest reading rather than the relational claims greening over three accepts. +fn marc_cause(v: MarcVerdict) -> Optional { match v { - MarcFileRefused { fatal_reason: r } => r == ^body_lowering_reason_list_literal_unlowered - MarcNotRefused => false + MarcFileRefused { fatal_reason: r } => optional_present(value: r) + MarcNotRefused => optional_absent() + } +} + +fn marc_same_located_cause(v: MarcVerdict, first: MarcVerdict) -> Bool { + match marc_cause(v: first) { + Absent => false + Present { value: f } => + if f == ^body_lowering_reason_match_arm_navigation_refused { + false + } else { + match marc_cause(v: v) { + Present { value: c } => c == f + Absent => false + } + } } } @@ -122,26 +144,26 @@ fn marc_is_not_refused(v: MarcVerdict) -> Bool { } } -test fn a_list_literal_in_a_second_arm_refuses_under_its_own_cause() -> Bool { +test fn a_second_arm_refuses_under_the_cause_the_first_arm_reaches() -> Bool { match marc_outcomes() { - MarcOutcomesDecided { second_arm_list: v, comma_arm_list: _, first_arm_list: _, second_arm_ctl: _, comma_arm_ctl: _ } => - marc_is_list_literal_refused(v: v) + MarcOutcomesDecided { second_arm_list: v, comma_arm_list: _, first_arm_list: f, second_arm_ctl: _, comma_arm_ctl: _ } => + marc_same_located_cause(v: v, first: f) MarcContextRefused => false } } -test fn a_list_literal_in_a_comma_separated_arm_refuses_under_its_own_cause() -> Bool { +test fn a_comma_separated_arm_refuses_under_the_cause_the_first_arm_reaches() -> Bool { match marc_outcomes() { - MarcOutcomesDecided { second_arm_list: _, comma_arm_list: v, first_arm_list: _, second_arm_ctl: _, comma_arm_ctl: _ } => - marc_is_list_literal_refused(v: v) + MarcOutcomesDecided { second_arm_list: _, comma_arm_list: v, first_arm_list: f, second_arm_ctl: _, comma_arm_ctl: _ } => + marc_same_located_cause(v: v, first: f) MarcContextRefused => false } } -test fn a_list_literal_in_a_first_arm_refuses_under_the_same_cause() -> Bool { +test fn a_first_arm_specimen_still_refuses_located() -> Bool { match marc_outcomes() { - MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: v, second_arm_ctl: _, comma_arm_ctl: _ } => - marc_is_list_literal_refused(v: v) + MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: f, second_arm_ctl: _, comma_arm_ctl: _ } => + marc_same_located_cause(v: f, first: f) MarcContextRefused => false } } From 8d33883ea876937dab802421828e948fd4a40abb Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 26 Sep 2026 14:15:53 +0000 Subject: [PATCH 4/5] Witness: a refused arm is located at its own offending value, not its enclosing arm Co-Authored-By: Claude Opus 5.5 (1M context) --- .../match_arm_refusal_locus_test.dag | 193 ++++++++++++++++++ 1 file changed, 193 insertions(+) create mode 100644 src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag diff --git a/src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag b/src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag new file mode 100644 index 00000000000..d238738315d --- /dev/null +++ b/src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag @@ -0,0 +1,193 @@ +module v2.test.claim.namespace_xl0.match_arm_refusal_locus + +import v2.compiler.name_resolve { Admission, ResolutionSubject } +import v2.compiler.program_assembly { IngestAssembly, assemble_program_from_ingest_located } +import v2.compiler.source_authority { DagSourceReadWitness } +import v2.extdeps.languages.dag { dag_language_model } +import v2.std.algebra { fold_list, length } +import v2.std.artifact { Artifact, SourceFile } +import v2.std.cross_tree.import_model { DagTree } +import v2.std.diagnostic { Accepted, ByteRange, Diagnostic, NodeLocus, Rejected, Textual } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Symbol } +import v2.std.optional { Absent, Optional, Present, optional_absent, optional_present } +import v2.std.provenance { node_occurrence_id_optional, span_index_textual_locus_optional } +import v2.std.text { String } +import std.algebra { Cons, Empty } +import extdeps.communication.medium { Lossless, Medium } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE REFUSAL IS LOCATED AT THE OFFENDING VALUE, IN EVERY ARM POSITION. +// +// v2.test.claim.namespace_xl0.match_arm_refusal_carried establishes that a refused arm keeps its own +// CAUSE; its file-refusal verdict carries no locus, so it cannot establish WHERE the refusal points. +// This module reads the refusal diagnostic itself, one level lower: each specimen is assembled +// through v2.compiler.program_assembly assemble_program_from_ingest_located, the diagnostic whose +// reason is the list literal's cause is taken from the refused program's chain (the chain's head is a +// parse-stage residue advisory, so the head is not the refusal), its NodeLocus node is resolved +// through the assembly's own SpanIndex to a Textual byte range, and that range is compared with the +// offending literal's extent IN THAT SPECIMEN'S OWN SOURCE. +// +// THE EXPECTED EXTENT IS CONSTRUCTED, NOT TRANSCRIBED. Each specimen's source is written as a prefix, +// the offending literal `[]`, and a suffix, so the literal starts at length(prefix) in that source +// and no offset is compared across specimens or copied from a measurement. The fixtures are ASCII, +// so a character count is a byte count. The locus resolves to the literal's opening bracket. +// +// THE WRONG-LOCUS CONTROL. The navigation refusal this change removed located the ARM (the arm +// capture was its only locus). Each specimen's arm start is constructed the same way (the offset of +// its `true =>` pattern), and a claim asserts the refusal is NOT there, so an implementation that +// kept the cause but pointed at the enclosing arm is red here while the cause claims stay green. +// Its executed mutation (the list-literal refusal re-pointed at the enclosing value capture) is +// recorded in gunbc#12321. + +data marl_prelude: String = "module v2.test.marl\n\nfn marl_g(acc: List) -> List { acc }\n\nfn marl_probe(b: Bool, acc: List) -> List {\n" + +data marl_second_before_arm: String = " match b {\n false => acc\n " +data marl_second_arm_head: String = "true => marl_g(acc: " +data marl_second_suffix: String = ")\n }\n}\n" + +data marl_comma_before_arm: String = " match b { false => acc, " +data marl_comma_arm_head: String = "true => marl_g(acc: " +data marl_comma_suffix: String = ") }\n}\n" + +data marl_first_before_arm: String = " match b {\n " +data marl_first_arm_head: String = "true => marl_g(acc: " +data marl_first_suffix: String = ")\n false => acc\n }\n}\n" + +data marl_literal: String = "[]" + +type MarlSpecimen { + source: String + literal_start: Int + arm_start: Int +} + +fn marl_specimen(before_arm: String, arm_head: String, suffix: String) -> MarlSpecimen { + let arm_start = length(xs: marl_prelude) + length(xs: before_arm) + MarlSpecimen { + source: marl_prelude + before_arm + arm_head + marl_literal + suffix, + literal_start: arm_start + length(xs: arm_head), + arm_start: arm_start + } +} + +fn marl_second() -> MarlSpecimen { + marl_specimen(before_arm: marl_second_before_arm, arm_head: marl_second_arm_head, suffix: marl_second_suffix) +} + +fn marl_comma() -> MarlSpecimen { + marl_specimen(before_arm: marl_comma_before_arm, arm_head: marl_comma_arm_head, suffix: marl_comma_suffix) +} + +fn marl_first() -> MarlSpecimen { + marl_specimen(before_arm: marl_first_before_arm, arm_head: marl_first_arm_head, suffix: marl_first_suffix) +} + +// The offending refusal's resolved start, or Absent when the specimen did not refuse under the +// literal's cause, or refused under it at a locus that does not resolve to a byte range. +type MarlLocated + = MarlNotRefusedUnderTheCause + | MarlUnresolved + | MarlAt { start: Int, end: Int } + +fn marl_assemble(source: String) -> IngestAssembly { + assemble_program_from_ingest_located( + ingest: [DagSourceReadWitness { + source: Medium { carried: source, fidelity: Lossless }, + artifact: Artifact { kind: SourceFile, id: ^marl_read, file_path: "src/v2/test/fixture/namespace_xl0/marl.dag" }, + compilation_unit: ^marl_cu, + source_root: DagTree + }], + admission: Admission { subject: ResolutionSubject { name: [^v2, ^test, ^marl] }, imports: Empty }, + lm: dag_language_model() + ) +} + +fn marl_resolve(a: IngestAssembly, d: Diagnostic) -> MarlLocated { + match d.at { + NodeLocus { anchor: an } => + match node_occurrence_id_optional(node: an.at) { + Absent => MarlUnresolved + Present { value: id } => + match span_index_textual_locus_optional(index: a.spans, id: id) { + Absent => MarlUnresolved + Present { value: l } => + match l { + Textual { file: _, extent: ByteRange { start: s, end: e } } => MarlAt { start: s, end: e } + _ => MarlUnresolved + } + } + } + _ => MarlUnresolved + } +} + +fn marl_located(source: String) -> MarlLocated { + let a = marl_assemble(source: source) + match a.program { + Accepted { value: _, diagnostics: _ } => MarlNotRefusedUnderTheCause + Rejected { diagnostics: ds } => + fold_list( + xs: Cons { head: ds.head, tail: ds.tail }, + empty: MarlNotRefusedUnderTheCause, + cons: fn(acc, d) { + match acc { + MarlNotRefusedUnderTheCause => + if d.reason == ^body_lowering_reason_list_literal_unlowered { marl_resolve(a: a, d: d) } else { acc } + _ => acc + } + } + ) + } +} + +// One located verdict per specimen, computed once and shared by the claims below. +type MarlOutcomes { + second: MarlLocated + comma: MarlLocated + first: MarlLocated +} + +fn marl_outcomes() -> MarlOutcomes { + MarlOutcomes { + second: marl_located(source: marl_second().source), + comma: marl_located(source: marl_comma().source), + first: marl_located(source: marl_first().source) + } +} + +fn marl_starts_at(v: MarlLocated, at: Int) -> Bool { + match v { + MarlAt { start: s, end: e } => (s == at) && (e > s) + _ => false + } +} + +fn marl_resolved_elsewhere_than(v: MarlLocated, at: Int) -> Bool { + match v { + MarlAt { start: s, end: _ } => s != at + _ => false + } +} + +test fn a_second_arm_refusal_is_located_at_its_own_literal() -> Bool { + marl_starts_at(v: marl_outcomes().second, at: marl_second().literal_start) +} + +test fn a_comma_separated_arm_refusal_is_located_at_its_own_literal() -> Bool { + marl_starts_at(v: marl_outcomes().comma, at: marl_comma().literal_start) +} + +test fn a_first_arm_refusal_is_located_at_its_own_literal() -> Bool { + marl_starts_at(v: marl_outcomes().first, at: marl_first().literal_start) +} + +test fn a_second_arm_refusal_is_not_located_at_its_enclosing_arm() -> Bool { + marl_resolved_elsewhere_than(v: marl_outcomes().second, at: marl_second().arm_start) +} + +test fn a_comma_separated_arm_refusal_is_not_located_at_its_enclosing_arm() -> Bool { + marl_resolved_elsewhere_than(v: marl_outcomes().comma, at: marl_comma().arm_start) +} From d14dc350c9c2a7e4cdaa785ab672a021c527e72a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 26 Sep 2026 14:34:36 +0000 Subject: [PATCH 5/5] Locus witness: drop the not-at-arm claims (fooled by the comma layout under the mutation they named); share marl_outcomes Co-Authored-By: Claude Opus 5.5 (1M context) --- .../match_arm_refusal_locus_test.dag | 36 ++++++------------- src/v2/workflow/floor_pure_producer_share.dag | 3 ++ 2 files changed, 14 insertions(+), 25 deletions(-) diff --git a/src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag b/src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag index d238738315d..124e32fe8ae 100644 --- a/src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag +++ b/src/v2/test/claim/namespace_xl0/match_arm_refusal_locus_test.dag @@ -35,13 +35,16 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // and no offset is compared across specimens or copied from a measurement. The fixtures are ASCII, // so a character count is a byte count. The locus resolves to the literal's opening bracket. // -// THE WRONG-LOCUS CONTROL. The navigation refusal this change removed located the ARM (the arm -// capture was its only locus). Each specimen's arm start is constructed the same way (the offset of -// its `true =>` pattern), and a claim asserts the refusal is NOT there, so an implementation that -// kept the cause but pointed at the enclosing arm is red here while the cause claims stay green. -// Its executed mutation (the list-literal refusal re-pointed at the enclosing value capture) is -// recorded in gunbc#12321. - +// THE WRONG-LOCUS MUTATION, AND WHY THERE IS NO "NOT AT THE ARM" CLAIM. The navigation refusal this +// change removed located the ARM. Re-pointing the arm refusal at its enclosing arm while keeping its +// cause (v2.compiler.body_lowering_fold body_lower_match_arm_wired answering the same reason at +// arm_capture) reds all three located claims below while +// v2.test.claim.namespace_xl0.match_arm_refusal_carried's cause claims stay green; that run is +// recorded in gunbc#12321. A companion claim "not located at the arm's start" was written and +// DELETED: under that exact mutation it stayed green for the comma-separated specimen, because a +// comma arm's capture does not begin at its pattern, so it was fooled by the defect it named. The +// exact-start claims are the discriminator. +// data marl_prelude: String = "module v2.test.marl\n\nfn marl_g(acc: List) -> List { acc }\n\nfn marl_probe(b: Bool, acc: List) -> List {\n" data marl_second_before_arm: String = " match b {\n false => acc\n " @@ -61,15 +64,13 @@ data marl_literal: String = "[]" type MarlSpecimen { source: String literal_start: Int - arm_start: Int } fn marl_specimen(before_arm: String, arm_head: String, suffix: String) -> MarlSpecimen { let arm_start = length(xs: marl_prelude) + length(xs: before_arm) MarlSpecimen { source: marl_prelude + before_arm + arm_head + marl_literal + suffix, - literal_start: arm_start + length(xs: arm_head), - arm_start: arm_start + literal_start: arm_start + length(xs: arm_head) } } @@ -165,13 +166,6 @@ fn marl_starts_at(v: MarlLocated, at: Int) -> Bool { } } -fn marl_resolved_elsewhere_than(v: MarlLocated, at: Int) -> Bool { - match v { - MarlAt { start: s, end: _ } => s != at - _ => false - } -} - test fn a_second_arm_refusal_is_located_at_its_own_literal() -> Bool { marl_starts_at(v: marl_outcomes().second, at: marl_second().literal_start) } @@ -183,11 +177,3 @@ test fn a_comma_separated_arm_refusal_is_located_at_its_own_literal() -> Bool { test fn a_first_arm_refusal_is_located_at_its_own_literal() -> Bool { marl_starts_at(v: marl_outcomes().first, at: marl_first().literal_start) } - -test fn a_second_arm_refusal_is_not_located_at_its_enclosing_arm() -> Bool { - marl_resolved_elsewhere_than(v: marl_outcomes().second, at: marl_second().arm_start) -} - -test fn a_comma_separated_arm_refusal_is_not_located_at_its_enclosing_arm() -> Bool { - marl_resolved_elsewhere_than(v: marl_outcomes().comma, at: marl_comma().arm_start) -} diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index c435b998128..e9761b8f13e 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -612,6 +612,8 @@ import v2.std.collection { List } // v2.test.claim.namespace_xl0.match_arm_refusal_carried marc_outcomes drives one front end over five // inline modules and stores one verdict arm per module (a fatal cause Symbol or not-refused), // portable for the same reason. +// v2.test.claim.namespace_xl0.match_arm_refusal_locus marl_outcomes assembles three inline +// specimens and stores one resolved byte range per specimen (Ints, no Node or SpanIndex). // THE XL-2 BOUND-VALUE RESOLVE ROW IS THE SAME GROUND AT ELEVEN SPECIMENS: // v2.test.claim.namespace_xl0.bound_value_resolve_refusal bvr_outcomes drives one front end over // eleven inline modules and stores one verdict arm per module, portable for the same reason. @@ -688,6 +690,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.namespace_xl0.if_arm_and_statement_lowering_refusal.iasl_outcomes", "v2.test.claim.namespace_xl0.bound_value_resolve_refusal.bvr_outcomes", "v2.test.claim.namespace_xl0.match_arm_refusal_carried.marc_outcomes", + "v2.test.claim.namespace_xl0.match_arm_refusal_locus.marl_outcomes", "v2.test.claim.namespace_xl0.wildcard_arm_resolve.wc_outcomes", "v2.test.cli.v2_native_cli.cli_probe_trailing_outcome", "v2.test.emit.closure_emit_arrow_body_refusal.arrow_body_probe_verdict",