Skip to content

Gate block_headed_operand_class: fragments at expr plus one real-route claim (census phase 3) - #13410

Merged
gunbai-bot[bot] merged 2 commits into
mainfrom
gate/parse-test-block-headed-operand-class
Oct 6, 2026
Merged

gunbai-bot[bot] merged 2 commits into
mainfrom
gate/parse-test-block-headed-operand-class

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor

Phase 3 of the census plan (#13372). This PR gates v2.test.parse.block_headed_operand_class_parse, which becomes test.claim.parse_test_block_headed_operand_class. In the census all 7 of its claims were over the 72.3k budget, at 77k–80k each.

The rework, per DESIGN §3 (a witness discriminates at one interface):

  • Fragment claims. The 7 per-operator claims now parse only the expression fragment (match w {…} <op> <rhs>) at dag_production_expr on the real prepared grammar, with the stream's own layout. The module header and data declaration are no longer re-parsed for each claim.
  • Why the fragment claims still discriminate. A production parse refuses leftover tokens. If a block alternative came back ahead of binary_expr, the operator and right operand would be left over, so the claim would refuse and go red. Each claim also checks that a match_expr shell is in the tree.
  • Dropped check. I removed the binary_expr-shell check from the route assertion. A probe showed a bare match also produces that shell, so it discriminated nothing.
  • One real-route claim. a_block_headed_left_operand_parses_on_the_real_module_route_holds runs the whole-module census route (parse_acceptance_of_text) end to end. It is the census's own text, shortened to module p\ndata d: Int = match w { _ => 1 } + 2\n.

Measured with claim_batch on BuildBuddy (invocation f9700a4f, then a follow-up run on this tree):

claim eval steps
mul / add / sub / cmp / eq / or / pipe fragments 56,181 / 56,766 / 56,945 / 57,050 / 57,211 / 59,725 / 58,759
real-route claim 71,718

The real-route claim fits with only 582 steps to spare; whole-module parse cost is mostly fixed. With the original two-line arm it measured 75,091. If a grammar change pushes it over, the remedy is a floor_eval_step_cost_drop plus a rung drop, not reworking the fragments.

Controls from the probe run (the probes are not committed):

  • Leftover operator match w {…} * is refused.
  • - on the next line after } is refused.
  • Without the stream layout, the same-line - case refused. That is why the fragment parse carries the layout.

Rosters: neither the grandfathered roster nor the cost-basis receipts held any of these identities. Old identities v2.test.parse.block_headed_operand_class_parse.a_block_headed_left_operand_of_<op>_parses_holds (op = mul, add, sub, cmp, eq, or, pipe) become test.claim.parse_test_block_headed_operand_class.<same>. One claim is new: …real_module_route_holds.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 2 commits October 5, 2026 14:16
…ts 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) <noreply@anthropic.com>
… claims

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

review 76578 was right. When I removed my measurement probes, the edit was never staged, so the head you reviewed still carried 5 dangling probe fns and the old two-line real-route text (75,091 steps, over budget). The new head removes them; bc_add_module_source is now the one-line text measured at 71,718.

The two controls are now test fns, negated correctly: a_dangling_operator_after_a_block_is_refused_holds and a_next_line_minus_after_a_block_is_refused_holds. In the probe run their unnegated bodies measured 52,339 and 51,292 eval steps and came out false, so the negated claims hold and both fit the budget.

— sent from calm-crab-469

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 5, 2026
Merged via the queue into main with commit b235ed1 Oct 6, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the gate/parse-test-block-headed-operand-class branch October 6, 2026 11:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants