From fe5c15113b9cdb68cc4282a6a64b99013eee78d7 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 14:16:15 +0000 Subject: [PATCH 1/3] Gate block_headed_operand_class into test.claim.parse_test_*: fragments at expr, one real-route claim (census phase 3) Seven claims parse their fragment at dag_production_expr with the stream's layout (leftover tokens refuse); one claim keeps the whole-module census route. Measured by claim_batch (BuildBuddy f9700a4f and the follow-up run): fragments 51-60k eval steps, the real-route claim 71,718, all under 72,300. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../block_headed_operand_class_parse_test.dag | 67 --------- ...e_test_block_headed_operand_class_test.dag | 140 ++++++++++++++++++ 2 files changed, 140 insertions(+), 67 deletions(-) delete mode 100644 src/v2/test/claim/parse/block_headed_operand_class_parse_test.dag create mode 100644 src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag diff --git a/src/v2/test/claim/parse/block_headed_operand_class_parse_test.dag b/src/v2/test/claim/parse/block_headed_operand_class_parse_test.dag deleted file mode 100644 index 8e4a2d8f6a5..00000000000 --- a/src/v2/test/claim/parse/block_headed_operand_class_parse_test.dag +++ /dev/null @@ -1,67 +0,0 @@ -module v2.test.parse.block_headed_operand_class_parse - -import v2.compiler.parse_acceptance_census { parse_acceptance_of_text } -import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } -import v2.std.text { String } - -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly - -// A BLOCK-HEADED EXPRESSION IS AN OPERAND OF EVERY BINARY OPERATOR CLASS. `match`, `if` and `loop` are -// primaries of binary_expr (v2.extdeps.languages.dag dag_grammar_primary_expr_core), so a block heads -// a chain of any operator, as the seed reads it (v1.compiler.parse parse_expr_bp). -// v2.test.parse.block_expr_as_binary_operand_parse holds `&&` with a `match` and with an `if`, the -// bare forms and their lowered shape (so an `if` heading a chain is held there); these claims hold the -// remaining operator classes, one each, with a `match` as the LEFT operand. They are what fails if a block-form alternative returns ahead of -// binary_expr in dag_grammar_expr_expr, or if an operator class stops admitting a primary block. One -// `data` declaration each, classified by the census's own route (v2.compiler.parse_acceptance_census -// parse_acceptance_of_text), so a census run and these claims cannot disagree on the same text. - -// multiplicative `*` -data bc_mul_source: String = "module probe.bc_mul\n\ndata d: Int = match w {\n _ => 1\n} * 2\n" - -// additive `+` -data bc_add_source: String = "module probe.bc_add\n\ndata d: Int = match w {\n _ => 1\n} + 2\n" - -// additive `-`, same line as the closing brace -data bc_sub_source: String = "module probe.bc_sub\n\ndata d: Int = match w {\n _ => 1\n} - 2\n" - -// comparison `<` -data bc_cmp_source: String = "module probe.bc_cmp\n\ndata d: Int = match w {\n _ => 1\n} < 2\n" - -// equality `==` -data bc_eq_source: String = "module probe.bc_eq\n\ndata d: Int = match w {\n _ => 1\n} == 2\n" - -// logical `||` -data bc_or_source: String = "module probe.bc_or\n\ndata d: Int = match w {\n _ => true\n} || t\n" - -// pipe `|>` -data bc_pipe_source: String = "module probe.bc_pipe\n\ndata d: Int = match w {\n _ => 1\n} |> g\n" - -test fn a_block_headed_left_operand_of_mul_parses_holds() -> Bool { - parse_acceptance_of_text(text: bc_mul_source, path: "probe/bc_mul.dag") == "accepted" -} - -test fn a_block_headed_left_operand_of_add_parses_holds() -> Bool { - parse_acceptance_of_text(text: bc_add_source, path: "probe/bc_add.dag") == "accepted" -} - -test fn a_block_headed_left_operand_of_sub_parses_holds() -> Bool { - parse_acceptance_of_text(text: bc_sub_source, path: "probe/bc_sub.dag") == "accepted" -} - -test fn a_block_headed_left_operand_of_cmp_parses_holds() -> Bool { - parse_acceptance_of_text(text: bc_cmp_source, path: "probe/bc_cmp.dag") == "accepted" -} - -test fn a_block_headed_left_operand_of_eq_parses_holds() -> Bool { - parse_acceptance_of_text(text: bc_eq_source, path: "probe/bc_eq.dag") == "accepted" -} - -test fn a_block_headed_left_operand_of_or_parses_holds() -> Bool { - parse_acceptance_of_text(text: bc_or_source, path: "probe/bc_or.dag") == "accepted" -} - -test fn a_block_headed_left_operand_of_pipe_parses_holds() -> Bool { - parse_acceptance_of_text(text: bc_pipe_source, path: "probe/bc_pipe.dag") == "accepted" -} - diff --git a/src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag b/src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag new file mode 100644 index 00000000000..001d05a9835 --- /dev/null +++ b/src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag @@ -0,0 +1,140 @@ +module test.claim.parse_test_block_headed_operand_class + +import v2.compiler.parse { PreparedModeled, PreparedVoidGrammar, parse_production_prepared_measured_seeded } +import v2.compiler.parse_acceptance_census { parse_acceptance_of_text } +import v2.compiler.program_assembly { dag_prepared_grammar, dag_prepared_lex } +import v2.compiler.tokenize { tokenize_prepared } +import v2.extdeps.languages.dag { parse_production_emitted_identity_optional } +import std.occurrence_identity { occurrence_id_allocator_initial } +import v2.std.compilers.lexing { token_stream_layout, token_stream_remaining } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.node { Node, Symbol } +import v2.std.optional { Absent, Present } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.text { String } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A BLOCK-HEADED EXPRESSION IS AN OPERAND OF EVERY BINARY OPERATOR CLASS. `match`, `if` and `loop` are +// primaries of binary_expr (v2.extdeps.languages.dag dag_grammar_primary_expr_core), so a block heads +// a chain of any operator, as the seed reads it (v1.compiler.parse parse_expr_bp). +// v2.test.parse.block_expr_as_binary_operand_parse holds `&&` with a `match` and with an `if`, the +// bare forms and their lowered shape (so an `if` heading a chain is held there); these claims hold the +// remaining operator classes, one each, with a `match` as the LEFT operand. They are what fails if a block-form alternative returns ahead of +// binary_expr in dag_grammar_expr_expr, or if an operator class stops admitting a primary block. One +// fragment each, parsed at the ONE production the claims are about (dag_production_expr) rather than +// inside a whole module, whose header and declaration are not their subject (DESIGN section 3, a witness +// discriminates at one interface). A production parse refuses leftover tokens, so a block alternative +// returned ahead of binary_expr would leave the operator and its right operand unconsumed and refuse; +// each claim also asserts the match_expr shell is in the tree. (Every expression parses through a +// binary_expr shell, a bare `match` included, so that shell would discriminate nothing.) The one +// claim that runs the real module route end to end is the `+` case through the census's own route +// (v2.compiler.parse_acceptance_census parse_acceptance_of_text), so a census run and this module +// cannot disagree on the same text. + +// One fragment parsed at one production of the real prepared grammar, with the stream's own layout +// (the dual-role `-` asks whether a line break precedes it, and a stream without layout refuses). +fn bc_parse_at(text: String, production: Symbol) -> Outcome { + match tokenize_prepared(text: text, file: ^block_headed_operand_class_probe, prepared: dag_prepared_lex()) { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: ts, diagnostics: _ } => + match dag_prepared_grammar() { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: PreparedVoidGrammar, diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: PreparedModeled { modeled: modeled, materialization: materialization }, diagnostics: _ } => + match parse_production_prepared_measured_seeded( + tokens: token_stream_remaining(stream: ts), + validated: modeled.validated, + analysis: modeled.analysis, + production_name: production, + seed: occurrence_id_allocator_initial(), + layout: token_stream_layout(stream: ts), + materialization: materialization + ).outcome { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: artifact, diagnostics: d } => Accepted { value: artifact.tree, diagnostics: d } + } + } + } +} + +// Whether a shell emitted as `emitted` lies at or beneath n. +fn bc_has_shell(n: Node, emitted: Symbol) -> Bool { + let here = match parse_production_emitted_identity_optional(node: n) { + Present { value: e } => e == emitted + Absent => false + } + here || fold(n.children, init: false, f: fn(acc, e) { acc || bc_has_shell(n: e.target, emitted: emitted) }) +} + +// The fragment parses whole at `expr` (leftover tokens refuse), with a match_expr shell in its tree. +fn bc_block_headed_chain_holds(text: String) -> Bool { + match bc_parse_at(text: text, production: ^dag_production_expr) { + Rejected { diagnostics: _ } => false + Accepted { value: tree, diagnostics: _ } => + bc_has_shell(n: tree, emitted: ^dag_surface_match_expr) + } +} + +// The one end-to-end claim's whole-module text. +data bc_add_module_source: String = "module probe.bc_add\n\ndata d: Int = match w {\n _ => 1\n} + 2\n" + +// multiplicative `*` +data bc_mul_source: String = "match w {\n _ => 1\n} * 2" + +// additive `+` +data bc_add_source: String = "match w {\n _ => 1\n} + 2" + +// additive `-`, same line as the closing brace +data bc_sub_source: String = "match w {\n _ => 1\n} - 2" + +// comparison `<` +data bc_cmp_source: String = "match w {\n _ => 1\n} < 2" + +// equality `==` +data bc_eq_source: String = "match w {\n _ => 1\n} == 2" + +// logical `||` +data bc_or_source: String = "match w {\n _ => true\n} || t" + +// pipe `|>` +data bc_pipe_source: String = "match w {\n _ => 1\n} |> g" + +test fn a_block_headed_left_operand_of_mul_parses_holds() -> Bool { + bc_block_headed_chain_holds(text: bc_mul_source) +} + +test fn a_block_headed_left_operand_of_add_parses_holds() -> Bool { + bc_block_headed_chain_holds(text: bc_add_source) +} + +test fn a_block_headed_left_operand_of_sub_parses_holds() -> Bool { + bc_block_headed_chain_holds(text: bc_sub_source) +} + +test fn a_block_headed_left_operand_of_cmp_parses_holds() -> Bool { + bc_block_headed_chain_holds(text: bc_cmp_source) +} + +test fn a_block_headed_left_operand_of_eq_parses_holds() -> Bool { + bc_block_headed_chain_holds(text: bc_eq_source) +} + +test fn a_block_headed_left_operand_of_or_parses_holds() -> Bool { + bc_block_headed_chain_holds(text: bc_or_source) +} + +test fn a_block_headed_left_operand_of_pipe_parses_holds() -> Bool { + bc_block_headed_chain_holds(text: bc_pipe_source) +} + + +test fn a_block_headed_left_operand_parses_on_the_real_module_route_holds() -> Bool { + parse_acceptance_of_text(text: bc_add_module_source, path: "probe/bc_add.dag") == "accepted" +} + +fn probe_leftover_operator_refuses() -> Bool { bc_block_headed_chain_holds(text: "match w {\n _ => 1\n} * ") } +fn probe_e2e_short_name() -> Bool { parse_acceptance_of_text(text: "module p\n\ndata d: Int = match w {\n _ => 1\n} + 2\n", path: "p.dag") == "accepted" } +fn probe_e2e_one_line() -> Bool { parse_acceptance_of_text(text: "module p\ndata d: Int = match w { _ => 1 } + 2\n", path: "p.dag") == "accepted" } +fn probe_sub_next_line_refuses() -> Bool { bc_block_headed_chain_holds(text: "match w {\n _ => 1\n}\n- 2") } +fn probe_parse_at_accepts_bare_match() -> Bool { match bc_parse_at(text: "match w {\n _ => 1\n}", production: ^dag_production_expr) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } } From f422eb3dfb90c29167105363bc3b1d9fbf214640 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 14:19:16 +0000 Subject: [PATCH 2/3] Drop the unstaged-probe residue; enrol the two discriminating reds as claims Co-Authored-By: Claude Opus 5.5 (1M context) --- ...e_test_block_headed_operand_class_test.dag | 25 +++++++++++++------ 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag b/src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag index 001d05a9835..0495853bc90 100644 --- a/src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag +++ b/src/v2/test/claim/parse/parse_test_block_headed_operand_class_test.dag @@ -76,8 +76,10 @@ fn bc_block_headed_chain_holds(text: String) -> Bool { } } -// The one end-to-end claim's whole-module text. -data bc_add_module_source: String = "module probe.bc_add\n\ndata d: Int = match w {\n _ => 1\n} + 2\n" +// The one end-to-end claim's whole-module text: the smallest module carrying the `+` chain. Its arm +// sits on the match's own line because a whole-module parse of this shape lands near the floor's +// per-claim eval-step budget, and the arm's layout is the fragment claims' subject, not this one's. +data bc_add_module_source: String = "module p\ndata d: Int = match w { _ => 1 } + 2\n" // multiplicative `*` data bc_mul_source: String = "match w {\n _ => 1\n} * 2" @@ -130,11 +132,18 @@ test fn a_block_headed_left_operand_of_pipe_parses_holds() -> Bool { test fn a_block_headed_left_operand_parses_on_the_real_module_route_holds() -> Bool { - parse_acceptance_of_text(text: bc_add_module_source, path: "probe/bc_add.dag") == "accepted" + parse_acceptance_of_text(text: bc_add_module_source, path: "p.dag") == "accepted" } -fn probe_leftover_operator_refuses() -> Bool { bc_block_headed_chain_holds(text: "match w {\n _ => 1\n} * ") } -fn probe_e2e_short_name() -> Bool { parse_acceptance_of_text(text: "module p\n\ndata d: Int = match w {\n _ => 1\n} + 2\n", path: "p.dag") == "accepted" } -fn probe_e2e_one_line() -> Bool { parse_acceptance_of_text(text: "module p\ndata d: Int = match w { _ => 1 } + 2\n", path: "p.dag") == "accepted" } -fn probe_sub_next_line_refuses() -> Bool { bc_block_headed_chain_holds(text: "match w {\n _ => 1\n}\n- 2") } -fn probe_parse_at_accepts_bare_match() -> Bool { match bc_parse_at(text: "match w {\n _ => 1\n}", production: ^dag_production_expr) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false } } + +// THE DISCRIMINATING REDS. A fragment whose operator has no right operand leaves tokens over and must +// refuse, and a `-` on the line after the closing brace is no continuation (the dual-role operator +// rule), so neither may read as a block-headed chain. If production parses stopped refusing leftover +// tokens, every claim above would hold vacuously; these go red first. +test fn a_dangling_operator_after_a_block_is_refused_holds() -> Bool { + !bc_block_headed_chain_holds(text: "match w {\n _ => 1\n} * ") +} + +test fn a_next_line_minus_after_a_block_is_refused_holds() -> Bool { + !bc_block_headed_chain_holds(text: "match w {\n _ => 1\n}\n- 2") +} From ffff020b4944ca181b46d85afc867c6c5f7c7eba Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 14:30:57 +0000 Subject: [PATCH 3/3] Gate parse_acceptance_census into test.claim.parse_test_*: the accepted arm on the smallest module (census phase 3) Co-Authored-By: Claude Opus 5.5 (1M context) --- ...=> parse_test_parse_acceptance_census_test.dag} | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) rename src/v2/test/claim/parse/{parse_acceptance_census_test.dag => parse_test_parse_acceptance_census_test.dag} (62%) diff --git a/src/v2/test/claim/parse/parse_acceptance_census_test.dag b/src/v2/test/claim/parse/parse_test_parse_acceptance_census_test.dag similarity index 62% rename from src/v2/test/claim/parse/parse_acceptance_census_test.dag rename to src/v2/test/claim/parse/parse_test_parse_acceptance_census_test.dag index 44c0ffc9962..eb10988ffb0 100644 --- a/src/v2/test/claim/parse/parse_acceptance_census_test.dag +++ b/src/v2/test/claim/parse/parse_test_parse_acceptance_census_test.dag @@ -1,4 +1,4 @@ -module v2.test.parse.parse_acceptance_census +module test.claim.parse_test_parse_acceptance_census import v2.compiler.parse_acceptance_census { parse_acceptance_of_text } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } @@ -10,15 +10,19 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // reports `accepted`, `refused ..`, or `unreadable`; everything but the read // is parse_acceptance_of_text, a pure function of the text. These claims supply the text (DESIGN // section 3: the input belongs at the interface as a supplied value) and pin the exact line the census -// prints for each arm a grammar comparison reads: a block-headed operand accepted, and a refusal named -// by its typed reason at its byte range. The read is the hand-run entry the module header names. +// prints for each arm: an accepted module, and a refusal named by its typed reason at its byte range. +// The read is the hand-run entry the module header names. The accepted text is the smallest module +// with one declaration, because WHICH construct is accepted is not this claim's subject: a +// block-headed operand accepted through this same route is held by +// test.claim.parse_test_block_headed_operand_class +// a_block_headed_left_operand_parses_on_the_real_module_route_holds. -data census_accepted_source: String = "module probe.census_ok\n\ndata d: Int = match w {\n _ => 1\n} + 2\n" +data census_accepted_source: String = "module p\ndata d: Int = 1\n" // The `-` that begins the last line is at bytes 45..46. data census_refused_source: String = "module probe.census_refused\n\ndata d: Int = x\n- 1\n" -test fn the_census_reports_a_block_headed_operand_accepted_holds() -> Bool { +test fn the_census_reports_an_accepted_module_holds() -> Bool { parse_acceptance_of_text(text: census_accepted_source, path: "probe/census_ok.dag") == "accepted" }