Skip to content
Merged
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
64 changes: 58 additions & 6 deletions src/v2/compiler/02_parse.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1499,6 +1499,44 @@ fn parse_diags_to_non_empty(diags: List<Diagnostic>, 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<GrammarChoiceAmbiguityRow>) -> List<GrammarChoiceAmbiguityRow> {
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<Diagnostic>) -> 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<GrammarChoiceAmbiguityRow>) -> 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<ValidatedGrammarRoot> {
if grammar_has_undefined_nonterminals(root: root) {
Rejected { diagnostics: diagnostics_singleton(d: parse_grammar_undefined_nonterminal_diagnostic(at: at)) }
Expand All @@ -1510,12 +1548,16 @@ fn grammar_validate_for_parse(root: GrammarRoot, at: Locus) -> Outcome<Validated
Rejected { diagnostics: diagnostics_singleton(d: parse_grammar_left_recursive_diagnostic(at: at)) }
} else {
let ambiguity_roster = grammar_choice_ambiguity_roster(root: root)
if !is_empty(xs: ambiguity_roster) {
let nullable_rows = grammar_nullable_ambiguity_rows(roster: ambiguity_roster)
if !is_empty(xs: nullable_rows) {
Rejected {
diagnostics: grammar_choice_ambiguity_rejection_diagnostics(at: at, roster: ambiguity_roster)
diagnostics: grammar_choice_ambiguity_rejection_diagnostics(at: at, roster: nullable_rows)
}
} else {
Accepted { value: ValidatedGrammarRoot { root: root }, diagnostics: None }
Accepted {
value: ValidatedGrammarRoot { root: root },
diagnostics: grammar_overlap_residue_diagnostics(at: at, roster: ambiguity_roster)
}
}
}
}
Expand Down Expand Up @@ -2042,12 +2084,22 @@ fn parse_module(tokens: TokenStream, grammar: ParseGrammar) -> Outcome<ParseArti
ModeledGrammar { root: root } =>
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 {
Expand Down
21 changes: 15 additions & 6 deletions src/v2/test/claim/manual/grammar_choice_ambiguity_audit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,35 +4,44 @@ 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
}
}

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 {
Expand Down
16 changes: 8 additions & 8 deletions src/v2/test/claim/manual/python_wave1_grammar_claim.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}

Expand All @@ -72,17 +72,17 @@ fn python_wave1_grammar_parse_fixture() -> Outcome<ParseTree> {
}

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),
classification: TestClassification { tier: Tier1, layer: Unit }
}

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 }
}
66 changes: 61 additions & 5 deletions src/v2/test/claim/parse/grammar_validation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -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 }
}
Expand Down
Loading