diff --git a/src/v2/compiler/02_parse.dag b/src/v2/compiler/02_parse.dag index f6b4e10ff1f..584ad0f0654 100644 --- a/src/v2/compiler/02_parse.dag +++ b/src/v2/compiler/02_parse.dag @@ -1499,6 +1499,44 @@ fn parse_diags_to_non_empty(diags: List, default: Diagnostic) -> Non } } +data grammar_overlap_residue_disposition: String = "Choice-FIRST overlap splits into two states that must not conflate: both_nullable=true is genuine ambiguity (two arms can accept the same token with an empty derivation in play) and stays a fail-closed Rejected; both_nullable=false is a non-LL(1) choice point the runtime handles by construction (parse_choice_first_dispatch routes disjoint FIRST directly and sends overlap to parse_choice_residue_backtrack), so it is a counted, typed Accepted-residue diagnostic (reason parse_grammar_choice_overlap_residue, one per row), never a rejection and never a silent drop. Receipt: dag_wave1 carries 5 non-nullable overlap rows (expr, arg, match_arm, field_pattern, if_expr); rejecting them made parse_module refuse every input on main 2026-07-06 while the backtrack arm sat dead - the wall refused what its own runtime handles." + +fn grammar_nullable_ambiguity_rows(roster: List) -> List { + filter(xs: roster, predicate: fn(row) { row.both_nullable }) +} + +fn parse_grammar_choice_overlap_residue_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: ^parse_grammar_choice_overlap_residue, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + +fn diagnostics_from_diagnostic_list(items: List) -> Diagnostics { + match list_at_optional(xs: items, index: 0) { + Absent => None + Present { value: first } => + match list_tail(xs: items) { + TailAbsent => Some { diagnostics: NonEmptyDiagnostics { head: first, tail: Empty } } + TailFound { tail: rest } => + Some { diagnostics: NonEmptyDiagnostics { head: first, tail: rest } } + } + } +} + +fn grammar_overlap_residue_diagnostics(at: Locus, roster: List) -> Diagnostics { + diagnostics_from_diagnostic_list( + items: fold_list( + xs: roster, + empty: Empty, + cons: fn(acc, row) { + list_snoc_item(xs: acc, item: parse_grammar_choice_overlap_residue_diagnostic(at: at)) + } + ) + ) +} + fn grammar_validate_for_parse(root: GrammarRoot, at: Locus) -> Outcome { if grammar_has_undefined_nonterminals(root: root) { Rejected { diagnostics: diagnostics_singleton(d: parse_grammar_undefined_nonterminal_diagnostic(at: at)) } @@ -1510,12 +1548,16 @@ fn grammar_validate_for_parse(root: GrammarRoot, at: Locus) -> Outcome Outcome match grammar_validate_for_parse(root: root, at: at) { Rejected { diagnostics: diags } => Rejected { diagnostics: diags } - Accepted { value: validated, diagnostics: _ } => - parse_production( + Accepted { value: validated, diagnostics: validation_residue } => + match parse_production( tokens: token_stream_remaining(stream: tokens), validated: validated, production_name: root.start - ) + ) { + Accepted { value: artifact, diagnostics: parse_diags } => + Accepted { + value: artifact, + diagnostics: diagnostics_merge(outer: validation_residue, inner: parse_diags) + } + Rejected { diagnostics: parse_rejected } => + Rejected { + diagnostics: rejected_with_pending(pending: validation_residue, rejected: parse_rejected) + } + } } } } else { diff --git a/src/v2/test/claim/manual/grammar_choice_ambiguity_audit.dag b/src/v2/test/claim/manual/grammar_choice_ambiguity_audit.dag index c79ae2c8b40..a9b1c3bde28 100644 --- a/src/v2/test/claim/manual/grammar_choice_ambiguity_audit.dag +++ b/src/v2/test/claim/manual/grammar_choice_ambiguity_audit.dag @@ -4,26 +4,29 @@ import v2.compiler.parse { grammar_choice_ambiguity_count, grammar_choice_ambiguity_roster, grammar_has_choice_ambiguity, + grammar_nullable_ambiguity_rows, grammar_validate_for_parse } import v2.extdeps.languages.dag { dag_wave1_grammar_root } import v2.extdeps.languages.python { python_wave1_grammar_root } import v2.std.collection { list_at_optional, Present, Absent } import v2.std.diagnostic { Accepted, Rejected, port_locus } +import v2.std.algebra { is_empty, length } import v2.std.logic { Bool } +import v2.std.integer { Int } import v2.std.node { Symbol } -data gca_audit_note: String = "Manual ambiguity stomper receipt (not CI-enrolled). dag_wave1: zero FIRST overlaps; grammar_validate_for_parse fail-closed on ambiguity (rejection carries grammar_choice_ambiguity_rejection_diagnostics roster). Runtime choice: FIRST-dispatch when disjoint, named backtrack residue when overlap. python_wave1 count=1 positive control (validate rejects). Remaining parser fallback: match_arm_stmt_body memo bypass. dag_wave1 grammar root: extdeps authority (dag_wave1_grammar_root), not re-extracted from LanguageModel." +data gca_audit_note: String = "Manual ambiguity stomper receipt (not CI-enrolled). Disposition since the overlap-residue split (2026-07-06): both_nullable=true FIRST overlap is genuine ambiguity and grammar_validate_for_parse stays fail-closed Rejected; both_nullable=false overlap is a non-LL(1) choice point the runtime handles (FIRST-dispatch when disjoint, parse_choice_residue_backtrack when overlapping) and validates Accepted with counted residue diagnostics. Receipt for the split: dag_wave1 carries 5 non-nullable overlap rows (expr, arg, match_arm, field_pattern, if_expr) and python_wave1 carries 1; the prior reject-all-overlap wall made parse_module refuse every input on main while the backtrack arm sat dead, and the zero-ambiguity witnesses here were enrolled green early but not re-executed as the FIRST fold evolved - green by authoring is not green by execution. Counts below are PINS: residue growth must be a loud diff, not silence. dag_wave1 grammar root: extdeps authority (dag_wave1_grammar_root), not re-extracted from LanguageModel." fn witness_python_wave1_choice_ambiguity_count() -> Int { grammar_choice_ambiguity_count(root: python_wave1_grammar_root()) } -fn witness_python_wave1_grammar_validate_rejects_ambiguity() -> Bool { +fn witness_python_wave1_grammar_validate_accepts_with_overlap_residue() -> Bool { let at = port_locus(port: ^parse_stage_locus_port) match grammar_validate_for_parse(root: python_wave1_grammar_root(), at: at) { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false } } @@ -31,8 +34,14 @@ fn witness_dag_wave1_choice_ambiguity_count() -> Int { grammar_choice_ambiguity_count(root: dag_wave1_grammar_root()) } -fn witness_dag_wave1_grammar_has_zero_choice_ambiguity() -> Bool { - !grammar_has_choice_ambiguity(root: dag_wave1_grammar_root()) +fn witness_dag_wave1_zero_nullable_choice_ambiguity() -> Bool { + is_empty(xs: grammar_nullable_ambiguity_rows( + roster: grammar_choice_ambiguity_roster(root: dag_wave1_grammar_root()) + )) +} + +fn witness_dag_wave1_overlap_residue_row_count() -> Int { + length(xs: grammar_choice_ambiguity_roster(root: dag_wave1_grammar_root())) } fn witness_dag_wave1_grammar_validate_accepts() -> Bool { diff --git a/src/v2/test/claim/manual/python_wave1_grammar_claim.dag b/src/v2/test/claim/manual/python_wave1_grammar_claim.dag index 6dd576d20ed..8afc79a4d67 100644 --- a/src/v2/test/claim/manual/python_wave1_grammar_claim.dag +++ b/src/v2/test/claim/manual/python_wave1_grammar_claim.dag @@ -38,15 +38,15 @@ fn python_claim_bool_atom(b: Bool) -> Node { fn python_wave1_grammar_validates_fixture() -> Bool { let at = port_locus(port: ^parse_stage_locus_port) match grammar_validate_for_parse(root: python_wave1_grammar_root(), at: at) { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false } } -fn python_wave1_grammar_parse_blocked_at_validate() -> Bool { +fn python_wave1_grammar_parse_accepts() -> Bool { match python_wave1_grammar_parse_fixture() { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false } } @@ -72,7 +72,7 @@ fn python_wave1_grammar_parse_fixture() -> Outcome { } data claim_python_wave1_grammar_validates: TestClaim = EqualsClaim { - label: "python_wave1_grammar_root fails grammar_validate_for_parse (choice ambiguity count=1 until left-factored)", + label: "python_wave1_grammar_root validates: its single Choice FIRST overlap is non-nullable, accepted as counted residue (overlap-residue split 2026-07-06)", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), lhs: python_claim_bool_atom(b: python_wave1_grammar_validates_fixture()), rhs: python_claim_bool_atom(b: true), @@ -80,9 +80,9 @@ data claim_python_wave1_grammar_validates: TestClaim = EqualsClaim { } data claim_python_wave1_grammar_parses_tokens: TestClaim = EqualsClaim { - label: "python MVP-1 parse blocked at grammar_validate_for_parse until stmt-suite choice overlap defactored", + label: "python MVP-1 parses end-to-end: non-nullable overlap routed to parse_choice_residue_backtrack at runtime", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: python_claim_bool_atom(b: python_wave1_grammar_parse_blocked_at_validate()), + lhs: python_claim_bool_atom(b: python_wave1_grammar_parse_accepts()), rhs: python_claim_bool_atom(b: true), classification: TestClassification { tier: Tier1, layer: Unit } } diff --git a/src/v2/test/claim/parse/grammar_validation.dag b/src/v2/test/claim/parse/grammar_validation.dag index 512fe0bf493..a0297adb94f 100644 --- a/src/v2/test/claim/parse/grammar_validation.dag +++ b/src/v2/test/claim/parse/grammar_validation.dag @@ -26,7 +26,7 @@ import v2.compiler.parse { parse_skip_to_sync, } import v2.std.witness { Holds, Violates } -import v2.std.diagnostic { Accepted, Outcome, Rejected, port_locus } +import v2.std.diagnostic { Accepted, Diagnostics, None, Outcome, Rejected, Some, port_locus } import v2.std.algebra { Cons, Empty } import v2.std.collection { List } import v2.std.node { Atom, Node, Symbol, TypeNode, SyntheticOccurrence } @@ -171,14 +171,54 @@ data validation_disjoint_choice_root: GrammarRoot = GrammarRoot { sync_tokens: grammar_empty_sync_tokens() } -fn validation_choice_ambiguity_validate_rejects() -> Bool { +fn validation_overlap_choice_validate_accepts_with_residue() -> Bool { let at = port_locus(port: ^parse_stage_locus_port) match grammar_validate_for_parse(root: validation_ambiguous_choice_root, at: at) { + Accepted { value: _, diagnostics: d } => + match d { + Some { diagnostics: residue } => residue.head.reason == ^parse_grammar_choice_overlap_residue + None => false + } + Rejected { diagnostics: _ } => false + } +} + +data validation_nullable_ambiguous_choice_root: GrammarRoot = GrammarRoot { + start: ^validation_start, + productions: Cons { + head: GrammarProduction { + name: ^validation_start, + expression: Choice { + left: Optional { element: Terminal { token_class: ^validation_tok_class, stamp: StampClass } }, + right: Optional { element: Terminal { token_class: ^validation_tok_class, stamp: StampClass } } + }, + emitted: grammar_atom(identity: ^validation_start) + }, + tail: Empty + }, + sync_tokens: grammar_empty_sync_tokens() +} + +fn validation_nullable_ambiguity_validate_rejects() -> Bool { + let at = port_locus(port: ^parse_stage_locus_port) + match grammar_validate_for_parse(root: validation_nullable_ambiguous_choice_root, at: at) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: _ } => true } } +fn validation_disjoint_choice_residue_is_none() -> Bool { + let at = port_locus(port: ^parse_stage_locus_port) + match grammar_validate_for_parse(root: validation_disjoint_choice_root, at: at) { + Accepted { value: _, diagnostics: d } => + match d { + None => true + Some { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + fn validation_disjoint_choice_validate_accepts() -> Bool { let at = port_locus(port: ^parse_stage_locus_port) match grammar_validate_for_parse(root: validation_disjoint_choice_root, at: at) { @@ -331,10 +371,26 @@ data claim_disjoint_choice_not_ambiguous: TestClaim = EqualsClaim { classification: TestClassification { tier: Tier1, layer: Unit } } -data claim_validate_rejects_choice_ambiguity: TestClaim = EqualsClaim { - label: "grammar_validate_for_parse rejects grammars with overlapping Choice FIRST sets", +data claim_validate_accepts_overlap_with_counted_residue: TestClaim = EqualsClaim { + label: "grammar_validate_for_parse accepts non-nullable Choice FIRST overlap as counted typed residue (reason parse_grammar_choice_overlap_residue); runtime routes it to parse_choice_residue_backtrack", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: validation_bool_atom(b: validation_overlap_choice_validate_accepts_with_residue()), + rhs: validation_bool_atom(b: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_validate_rejects_nullable_choice_ambiguity: TestClaim = EqualsClaim { + label: "grammar_validate_for_parse stays fail-closed on genuine ambiguity: both-nullable Choice arms sharing a FIRST terminal are Rejected", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + lhs: validation_bool_atom(b: validation_nullable_ambiguity_validate_rejects()), + rhs: validation_bool_atom(b: true), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data claim_disjoint_choice_validate_residue_none: TestClaim = EqualsClaim { + label: "disjoint-FIRST Choice validates with zero residue diagnostics (residue channel discriminates overlap from clean)", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - lhs: validation_bool_atom(b: validation_choice_ambiguity_validate_rejects()), + lhs: validation_bool_atom(b: validation_disjoint_choice_residue_is_none()), rhs: validation_bool_atom(b: true), classification: TestClassification { tier: Tier1, layer: Unit } }