Parse engine: FIRST-set choice dispatch and fail-closed ambiguity validation

src/v2/test/claim/manual/grammar_choice_ambiguity_audit.dag

@@ -0,0 +1,54 @@
+module v2.test.manual.grammar_choice_ambiguity_audit
+
+import v2.compiler.parse {
+  grammar_choice_ambiguity_count,
+  grammar_choice_ambiguity_roster,
+  grammar_has_choice_ambiguity,
+  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.logic { Bool }
+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."
+
+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 {
+  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
+  }
+}
+
+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_grammar_validate_accepts() -> Bool {
+  let at = port_locus(port: ^parse_stage_locus_port)
+  match grammar_validate_for_parse(root: dag_wave1_grammar_root(), at: at) {
+    Accepted { value: _, diagnostics: _ } => true
+    Rejected { diagnostics: _ } => false
+  }
+}
+
+fn witness_dag_wave1_first_choice_ambiguity_production() -> Symbol {
+  match list_at_optional(
+    xs: grammar_choice_ambiguity_roster(root: dag_wave1_grammar_root()),
+    index: 0
+  ) {
+    Present { value: row } => row.production
+    Absent => ^grammar_choice_ambiguity_roster_empty
+  }
+}

src/v2/test/claim/manual/parse_mechanism_probe.dag

@@ -78,9 +78,52 @@ fn pmp_memo_stats_report_path(path: String) -> List<Int> {
   }
 }
 
-data pmp_through_decimal_path: String =
-  "src/v2/test/fixture/integer_census_trunc/through_decimal_compare.txt"
+data pmp_through_decimal_path: String = "src/v2/test/fixture/integer_census_trunc/through_decimal_compare.txt"
 
 fn pmp_through_decimal_memo_report() -> List<Int> {
   pmp_memo_stats_report_path(path: pmp_through_decimal_path)
 }
+
+fn exp_nest_d1_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/nest_d1.dag")
+}
+
+fn exp_nest_d2_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/nest_d2.dag")
+}
+
+fn exp_nest_d3_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/nest_d3.dag")
+}
+
+fn exp_nest_d4_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/nest_d4.dag")
+}
+
+fn exp_elseif_k4_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/elseif_k4.dag")
+}
+
+fn exp_elseif_k8_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/elseif_k8.dag")
+}
+
+fn exp_elseif_k16_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/elseif_k16.dag")
+}
+
+fn exp_elseif_k32_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/parse_mechanism/elseif_k32.dag")
+}
+
+fn exp_through_compose_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: "src/v2/test/fixture/integer_census_trunc/through_compose_types.txt")
+}
+
+fn pmp_through_compose_memo_report() -> List<Int> {
+  pmp_memo_stats_report_path(path: "src/v2/test/fixture/integer_census_trunc/through_compose_types.txt")
+}
+
+fn exp_through_decimal_parse_holds() -> Bool {
+  pmp_tokenize_parse_path(path: pmp_through_decimal_path)
+}

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: _ } => true
-    Rejected { diagnostics: _ } => false
+    Accepted { value: _, diagnostics: _ } => false
+    Rejected { diagnostics: _ } => true
   }
 }
 
-fn python_wave1_grammar_parse_accepted() -> Bool {
+fn python_wave1_grammar_parse_blocked_at_validate() -> Bool {
   match python_wave1_grammar_parse_fixture() {
-    Accepted { value: _, diagnostics: _ } => true
-    Rejected { diagnostics: _ } => false
+    Accepted { value: _, diagnostics: _ } => false
+    Rejected { diagnostics: _ } => true
   }
 }
 
@@ -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 passes grammar_validate_for_parse",
+  label: "python_wave1_grammar_root fails grammar_validate_for_parse (choice ambiguity count=1 until left-factored)",
   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 production parse_production accepts lexer output for def-add source",
+  label: "python MVP-1 parse blocked at grammar_validate_for_parse until stmt-suite choice overlap defactored",
   anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
-  lhs: python_claim_bool_atom(b: python_wave1_grammar_parse_accepted()),
+  lhs: python_claim_bool_atom(b: python_wave1_grammar_parse_blocked_at_validate()),
   rhs: python_claim_bool_atom(b: true),
   classification: TestClassification { tier: Tier1, layer: Unit }
 }

src/v2/test/claim/parse/grammar_validation.dag

@@ -3,6 +3,7 @@ module v2.test.parse.grammar_validation
 import v2.std.compilers.lexing { Token }
 import v2.std.grammar {
   StampClass,
+  Choice,
   GrammarProduction,
   GrammarRoot,
   Nonterminal,
@@ -15,6 +16,7 @@ import v2.std.grammar {
 }
 import v2.compiler.parse {
   ParseSyncState,
+  grammar_has_choice_ambiguity,
   grammar_has_duplicate_productions,
   grammar_has_left_recursion,
   grammar_has_undefined_nonterminals,
@@ -137,6 +139,54 @@ data validation_two_distinct_root: GrammarRoot = GrammarRoot {
   sync_tokens: grammar_empty_sync_tokens()
 }
 
+data validation_ambiguous_choice_root: GrammarRoot = GrammarRoot {
+  start: ^validation_start,
+  productions: Cons {
+    head: GrammarProduction {
+      name: ^validation_start,
+      expression: Choice {
+        left: Terminal { token_class: ^validation_tok_class, stamp: StampClass },
+        right: Terminal { token_class: ^validation_tok_class, stamp: StampClass }
+      },
+      emitted: grammar_atom(identity: ^validation_start)
+    },
+    tail: Empty
+  },
+  sync_tokens: grammar_empty_sync_tokens()
+}
+
+data validation_disjoint_choice_root: GrammarRoot = GrammarRoot {
+  start: ^validation_start,
+  productions: Cons {
+    head: GrammarProduction {
+      name: ^validation_start,
+      expression: Choice {
+        left: Terminal { token_class: ^validation_tok_class, stamp: StampClass },
+        right: Terminal { token_class: ^validation_tok_class_b, stamp: StampClass }
+      },
+      emitted: grammar_atom(identity: ^validation_start)
+    },
+    tail: Empty
+  },
+  sync_tokens: grammar_empty_sync_tokens()
+}
+
+fn validation_choice_ambiguity_validate_rejects() -> 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: _ } => false
+    Rejected { diagnostics: _ } => true
+  }
+}
+
+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) {
+    Accepted { value: _, diagnostics: _ } => true
+    Rejected { diagnostics: _ } => false
+  }
+}
+
 fn validation_lookup_present_holds_named() -> Bool {
   match grammar_lookup_production(root: validation_two_distinct_root, name: ^validation_other) {
     Holds { value: production } => production.name == ^validation_other
@@ -264,3 +314,35 @@ data claim_right_recursive_parse_succeeds: TestClaim = EqualsClaim {
   rhs: validation_bool_atom(b: true),
   classification: TestClassification { tier: Tier1, layer: Unit }
 }
+
+data claim_choice_ambiguity_detected: TestClaim = EqualsClaim {
+  label: "grammar_has_choice_ambiguity returns true when Choice branches share a FIRST terminal",
+  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
+  lhs: validation_bool_atom(b: grammar_has_choice_ambiguity(root: validation_ambiguous_choice_root)),
+  rhs: validation_bool_atom(b: true),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}
+
+data claim_disjoint_choice_not_ambiguous: TestClaim = EqualsClaim {
+  label: "grammar_has_choice_ambiguity returns false when Choice FIRST sets are disjoint",
+  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
+  lhs: validation_bool_atom(b: grammar_has_choice_ambiguity(root: validation_disjoint_choice_root)),
+  rhs: validation_bool_atom(b: false),
+  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",
+  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
+  lhs: validation_bool_atom(b: validation_choice_ambiguity_validate_rejects()),
+  rhs: validation_bool_atom(b: true),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}
+
+data claim_validate_accepts_disjoint_choice: TestClaim = EqualsClaim {
+  label: "grammar_validate_for_parse accepts grammars whose Choice branches have disjoint FIRST sets",
+  anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
+  lhs: validation_bool_atom(b: validation_disjoint_choice_validate_accepts()),
+  rhs: validation_bool_atom(b: true),
+  classification: TestClassification { tier: Tier1, layer: Unit }
+}

src/v2/test/claim/parse/parse_table_claims_test.dag

@@ -253,8 +253,10 @@ test fn parse_table_parse_expr_combinator_holds() -> Bool {
   }
   let tok_a = parse_table_token(class: ^pt_parse_expr_tok_a)
   let tok_b = parse_table_token(class: ^pt_parse_expr_tok_b)
+  let tok_c = parse_table_token(class: ^pt_parse_expr_tok_c)
   let toks_a = Cons { head: tok_a, tail: Empty }
   let toks_b = Cons { head: tok_b, tail: Empty }
+  let toks_c = Cons { head: tok_c, tail: Empty }
   let toks_ab = Cons { head: tok_a, tail: Cons { head: tok_b, tail: Empty } }
   let toks_aab = Cons { head: tok_a, tail: Cons { head: tok_a, tail: Cons { head: tok_b, tail: Empty } } }
   let r1 = match parse_expr(
@@ -325,5 +327,16 @@ test fn parse_table_parse_expr_combinator_holds() -> Bool {
     ParseExprAccepted { remaining: _, captured: _, diagnostics: _, prov: _, table: _ } => false
     ParseExprRejected { diagnostics: _, table: _ } => true
   }
-  r1 && r2 && r3 && r4 && r5 && r6 && r7 && r8
+  let r9 = match parse_expr(
+    expr: Choice {
+      left: Optional { element: Terminal { token_class: ^pt_parse_expr_tok_a, stamp: StampClass } },
+      right: Terminal { token_class: ^pt_parse_expr_tok_b, stamp: StampClass }
+    },
+    tokens: toks_c, all_tokens: toks_c, root: root, table: table, prov: prov
+  ) {
+    ParseExprAccepted { remaining: rest, captured: _, diagnostics: _, prov: _, table: _ } =>
+      length(xs: rest) == 1
+    ParseExprRejected { diagnostics: _, table: _ } => false
+  }
+  r1 && r2 && r3 && r4 && r5 && r6 && r7 && r8 && r9
 }

src/v2/test/claim/parse/parse_table_content_key_test.dag

@@ -1,20 +1,22 @@
 module v2.test.parse.parse_table_content_key
 
-import v2.compiler.parse { ParseTable, ParseTableRealization, ParsePositionKey, parse_table_subject }
-import v2.std.collection { empty_map }
+import v2.compiler.parse { ParseTable, ParseTableRealization, ParsePositionKey, parse_table_empty, parse_table_subject }
 import v2.std.node { Hash }
 import v2.std.logic { Bool }
 
 fn mk_table(grammar: Hash, tokens: Hash) -> ParseTable {
+  let base = parse_table_empty()
   ParseTableRealization {
-    artifact_kind: ^parse_table,
-    interface: ^parse_table_memo,
+    artifact_kind: base.artifact_kind,
+    interface: base.interface,
     grammar_digest: grammar,
     token_stream_digest: tokens,
-    entries: empty_map(),
-    memo_hits: 0,
-    memo_misses: 0,
-    memo_lookup_calls: 0
+    entries: base.entries,
+    memo_hits: base.memo_hits,
+    memo_misses: base.memo_misses,
+    memo_lookup_calls: base.memo_lookup_calls,
+    nullable_set: base.nullable_set,
+    first_rows: base.first_rows
   }
 }
 

src/v2/test/fixture/parse_mechanism/elseif_k16.dag

@@ -0,0 +1,24 @@
+module synthetic.parse_mechanism.elseif_k16
+
+import v2.std.logic { Bool }
+import v2.std.nat { Nat }
+
+fn else_if_chain(x: Nat) -> Nat {
+  if x == 0 { 0 }
+  else if x == 1 { 1 }
+  else if x == 2 { 2 }
+  else if x == 3 { 3 }
+  else if x == 4 { 4 }
+  else if x == 5 { 5 }
+  else if x == 6 { 6 }
+  else if x == 7 { 7 }
+  else if x == 8 { 8 }
+  else if x == 9 { 9 }
+  else if x == 10 { 10 }
+  else if x == 11 { 11 }
+  else if x == 12 { 12 }
+  else if x == 13 { 13 }
+  else if x == 14 { 14 }
+  else if x == 15 { 15 }
+  else { 16 }
+}

src/v2/test/fixture/parse_mechanism/elseif_k32.dag

@@ -0,0 +1,40 @@
+module synthetic.parse_mechanism.elseif_k32
+
+import v2.std.logic { Bool }
+import v2.std.nat { Nat }
+
+fn else_if_chain(x: Nat) -> Nat {
+  if x == 0 { 0 }
+  else if x == 1 { 1 }
+  else if x == 2 { 2 }
+  else if x == 3 { 3 }
+  else if x == 4 { 4 }
+  else if x == 5 { 5 }
+  else if x == 6 { 6 }
+  else if x == 7 { 7 }
+  else if x == 8 { 8 }
+  else if x == 9 { 9 }
+  else if x == 10 { 10 }
+  else if x == 11 { 11 }
+  else if x == 12 { 12 }
+  else if x == 13 { 13 }
+  else if x == 14 { 14 }
+  else if x == 15 { 15 }
+  else if x == 16 { 16 }
+  else if x == 17 { 17 }
+  else if x == 18 { 18 }
+  else if x == 19 { 19 }
+  else if x == 20 { 20 }
+  else if x == 21 { 21 }
+  else if x == 22 { 22 }
+  else if x == 23 { 23 }
+  else if x == 24 { 24 }
+  else if x == 25 { 25 }
+  else if x == 26 { 26 }
+  else if x == 27 { 27 }
+  else if x == 28 { 28 }
+  else if x == 29 { 29 }
+  else if x == 30 { 30 }
+  else if x == 31 { 31 }
+  else { 32 }
+}

src/v2/test/fixture/parse_mechanism/elseif_k4.dag

@@ -0,0 +1,12 @@
+module synthetic.parse_mechanism.elseif_k4
+
+import v2.std.logic { Bool }
+import v2.std.nat { Nat }
+
+fn else_if_chain(x: Nat) -> Nat {
+  if x == 0 { 0 }
+  else if x == 1 { 1 }
+  else if x == 2 { 2 }
+  else if x == 3 { 3 }
+  else { 4 }
+}