Repository navigation
Grammar backward selection resolves each emitted tree once (stage 2 of #11741's rewire program) - #11835
Conversation
… top-down, instead of re-matching per candidate at every ancestor Selecting a production for an emitted node asks, for every candidate, whether its rhs matches the node, and a nonterminal slot asks the same of the slot's child. Written as a recursion from the root, a child's answer was re-derived once per candidate at every ancestor and again when the token edges were derived after selection -- exponential in depth, and only the eval-frame result memo made it look linear. On the required floor with that memo retired (run 35466872753) the formal_production_* family was ranks 2-10 of the within-claim recurrence census and the whole budget_interrupted population. std.materialization_ladder rule 1 names that AuthoredDuplication and prescribes Share: one EmittedProductionResolution per tree, resolved top-down against the set of left-hand sides the parents' candidates ask of each child (the population the old recursion explored), each child visited once; the unique-match selection, the per-lhs exact selection and the token-edge derivation read the carried resolution. Every existing entry point keeps its signature and diagnostics; the formal_production_matches_lhs_exact_child single-candidate reading is kept for its verilog consumer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Additional receipt, measured after opening: the docs-projection regen — the production route that never completed on the memo-retired binary (#11741, >48 min, killed) — completes on this branch with the memo-retired binary in 295 s wall ( |
What
Stage 2 of the rewire program behind #11741 (option-A ruling; stage 1 is #11784, independent — this branches off
main). Theformal_production_*grammar lookup family insrc/v2/std/grammar.dagwas ranks 2–10 of the required floor's within-claim recurrence census with the eval-frame memo retired, and the wholebudget_interruptedpopulation (effect_plan_bash_materialize_test,runner_slot_provision,witness_floor_workflow_consolidation,build_artifact_verification).Selecting a production for an emitted node asks, for every candidate, whether its rhs matches the node; a nonterminal slot asks the same of the slot's child. As a recursion from the root, a child's answer was re-derived once per candidate at every ancestor, and again when the token edges were derived after selection — exponential in depth; the memo made it look linear.
std.materialization_ladderrule 1: AuthoredDuplication, prescribed Share.Now: one
EmittedProductionResolutionper emitted tree — resolved top-down against the set of left-hand sides the parents' candidates place at each child's slot (exactly the population the old recursion explored), each child visited once;matchedper node is the set the oldformal_production_matches_emitted_childaccepted,slotsare the conj positional children's resolutions in order. The unique-match selection, the per-lhs exact selection and the token-edge derivation read the carried resolution. Every existing entry point (formal_production_for_lhs_exact,formal_production_unique_lhs_exact_match,formal_production_unique_emitted_match,derive_grammar_relation_row_node,grammar_relation_row_derived_from_productions,formal_production_matches_lhs_exact_child) keeps its signature and its diagnostics (grammar_relation_production_not_found/…_backward_selection_ambiguous/…_emitted_not_conj/…_conj_slot_missing/…_conj_slot_surplusat the same loci).Semantics-preserving on its face
By structural induction on the emitted tree: for an atom node the singleton checks are the old code verbatim; for a conj node the rhs walk is the old
formal_production_rhs_matches_emitted_conj_stepwith the nonterminal arm readingresolution_production_for_lhs_exact(slot, lhs)where it readformal_production_for_lhs_exact(productions, lhs, child)— equal by the inductive hypothesis, because the slot is that child's resolution and itsmatchedset is filtered by the same lhs and slot-count test the old fold applied. The root selection and the per-lhs selection then fold identical sets with identical None/One/Many arms. Theaskedrestriction loses nothing: a production whose lhs no parent candidate places at a slot was never a candidate in the old recursion either, and the root and the per-lhs entries ask for all lhs / the one lhs respectively. Executed receipts: every grammar-relation witness in the language modules holds on both trees —typescript_derive_grammar_relation_row_round_trip,verilog_interlock_emission(byte-equality of emitted output through the generic fold, token-spine read-back, production-order invariance),typescript_record_task_translate— and the 110 claims below: 110/110 PASS before and after under both realizations.Matched before/after on the claims it names — BOTH realizations, per claim
claim_batch --claim-run, six modules (the floor's interrupted population plus the bash fold witnesses), same host; "before" isorigin/main, "after" is this head. Memo-on is the required floor's live realization and is the landing condition; memo-retired is the #11741 head.an_active_authorized_required_retiree_is_masked_and_not_deletedan_inactive_slot_with_a_populated_cgroup_is_not_deleteda_permitted_surplus_slot_is_masked_and_not_deleted_on_the_first_passwitness_existence_check_no_mtimebash_serialization_is_total_at_8_distinct_commandsbash_fold_pipe_three_stage_holdsbash_serialization_is_total_at_4_distinct_commandsbash_fold_command_arbitrary_grep_triple_holdsbash_build_round_trip_pipe_holdsbash_fold_if_then_pipe_soundness_holdsbash_fold_with_redir_pipe_soundness_holdsbash_fold_pipe_echo_hi_wc_holdsbash_serialization_is_total_at_2_distinct_commandsbash_fold_pipe_and_then_left_holdsbash_fold_if_multi_then_holdsbash_fold_if_true_then_echo_holdsbash_fold_and_or_negation_preserves_posix_grouping_holdsbash_serialization_is_total_at_1_distinct_commandbash_fold_command_multi_lit_echo_hi_holdsbash_build_round_trip_command_tier_holdsbash_fold_direct_serialize_multi_lit_echo_hi_holdsbash_build_round_trip_and_then_holdsbash_fold_subshell_nested_and_then_holdsbash_fold_and_then_true_false_holdsbash_fold_or_else_true_false_holdsbash_fold_subshell_multi_stmt_holdsbash_fold_with_redir_redir_to_file_var_holdsbash_fold_negation_subshell_false_holdsbash_fold_with_redir_stderr_null_holdsbash_fold_with_redir_stdout_to_stderr_holdsbash_fold_with_redir_stdout_and_stderr_null_holdsbash_fold_subshell_true_holdsbash_fold_command_arbitrary_lit_quote_escape_holdsbash_fold_command_single_lit_true_holdsbash_fold_wrong_production_rejects_oracle_holdsbash_fold_direct_serialize_single_lit_true_holdsbash_fold_command_arbitrary_var_home_holdsbash_fold_command_var_ref_x_holdsbash_fold_direct_serialize_var_ref_x_holdsbash_build_round_trip_assign_foo_bar_holdsbash_fold_assign_wrong_production_rejects_oracle_holdsbash_fold_assign_lit_foo_bar_holdsbash_fold_assign_lit_quote_escape_holdsbash_fold_assign_var_x_home_holdsbash_fold_exit_wrong_production_rejects_oracle_holdsbash_build_round_trip_exit_42_holdsbash_fold_relation_row_true_witness_holdsan_unobserved_required_retiree_outside_membership_is_named_as_withheldan_observed_host_plans_the_missing_slotsan_active_surplus_slot_is_never_deletedbash_fold_with_redir_wrong_spellings_rejects_oracle_holdsbash_fold_exit_code_42_holdsbash_fold_exit_code_0_holdsbash_fold_negation_wrong_spellings_rejects_oracle_holdsbash_fold_negation_subshell_rawline_holdsbash_fold_raw_line_orch_emit_holdsbash_fold_raw_line_wrong_spellings_rejects_oracle_holdsbash_fold_raw_line_x_eq_holdsbash_fold_raw_line_cmdsubst_holdsbash_fold_raw_line_paren_holdsbash_fold_raw_line_quoted_holdsbash_fold_raw_line_mktemp_holdsbash_fold_raw_line_trailing_nl_holdsthe_registration_file_decodes_its_ephemeral_memberonly_the_fabric_host_loses_a_provisioning_targeta_retired_incarnation_is_owned_and_plans_removalthe_plan_realizes_removal_through_the_privileged_seamwitness_provision_plan_extracts_only_upsertsbash_fold_if_wrong_production_rejects_oracle_holdsbash_fold_subshell_wrong_production_rejects_oracle_holdsbash_fold_heredoc_wrong_production_rejects_oracle_holdsbash_fold_delegated_bundle_fail_closed_holdsbash_fold_and_then_wrong_production_rejects_oracle_holdsbash_fold_pipe_wrong_production_rejects_oracle_holdsbash_fold_env_prefixed_wrong_production_rejects_oracle_holdsbash_fold_heredoc_wrong_spellings_rejects_oracle_holdsbash_fold_with_redir_wrong_production_rejects_oracle_holdsbash_fold_negation_wrong_production_rejects_oracle_holdsbash_fold_raw_line_wrong_production_rejects_oracle_holdsbash_fold_env_prefixed_wrong_spellings_rejects_oracle_holdswitness_single_artifact_produces_two_checkswitness_srv3_deploy_row_names_its_declared_slotswitness_membership_reconcile_adds_delta_slotswitness_srv4_instance_roster_matches_its_declared_countthe_fabric_slot_is_not_a_provisioning_targeta_registered_or_active_or_enabled_tree_still_refuses_removalwitness_floor_covers_both_release_binswitness_runner_count_not_in_installer_argvevery_enrolled_host_resolves_and_none_is_unmodeledsrv2_resolves_as_refused_and_the_others_as_rowsno_deploy_row_out_commits_the_memory_budgethost_grammar_round_trips_through_the_allocation_renderera_dead_ephemeral_registration_is_a_retired_incarnationan_authored_count_enumerates_exactly_that_many_indexed_nameswitness_enumeration_postcondition_red_on_under_countan_unobserved_host_refuses_instead_of_planningan_active_ephemeral_registration_and_an_unreadable_one_still_refusewitness_actions_runner_release_cites_github_digesta_name_outside_the_host_grammar_refuses_even_when_deadan_unmodeled_host_has_no_deploy_rowbash_fold_heredoc_holdsbash_fold_env_prefixed_lit_t_holdsbash_fold_emitted_tree_differs_on_wrong_fixture_holdsa_pending_unmasked_standing_still_emits_the_inhibitora_completed_retirement_authorizes_exactly_that_tree_removala_completed_srv1_surplus_retirement_emits_the_teardown_argvan_unobserved_cgroup_withholds_the_removal_by_namea_completed_receipt_for_another_slot_authorizes_nothinga_surplus_slot_outside_the_authorized_scope_is_neither_masked_nor_deletedabsent_evidence_emits_neither_mask_nor_removal(a) Memo-on, the live path: 74 of 110 claims do more eval steps, +12% in total (3,475,905 → 3,886,850); the largest single increase is +38k (
witness_existence_check_no_mtime, 138k → 176k in claim_batch). No claim approaches its ceiling: the floor's own numbers for these claims are far below claim_batch's (the last column: the floor's cross-claim warm tier serves the bash productions, claim_batch installs no roster), and scaling each claim's base floor cost by its measured ratio puts the highest at ~40% of its line (bash_build_round_trip_pipe_holds, 29,434 → ~39k of 361,500 grandfathered; the new-witness-tierrunner_slot_provisionclaims 15.8–23.9k → ~19–29k of 72,300). The CI floor run on this PR is the authoritative reading of that.(b) Memo-retired, the win: 1,541,599,084 → 29,373,304 eval steps in total (52×); the
runner_slot_provisionclaims 442M → 1.0M;witness_existence_check_no_mtime126M → 2.4M; the seven memo-retired claims that timed out on the before run (not in the table) all complete after.What the +12% memo-on is: the resolution bookkeeping (asked-lhs sets per slot) the old recursion did not carry. A first bottom-up draft (match all productions at every node) measured +64% memo-on and was reworked into this asked-lhs form for that reason. The remaining caller-side duplication — language folds deriving a row per subtree, each re-resolving its subtree (
bash_fold_relation_row_witnessdemanded 3× per row in the trace) — is a consumer carry and is not attempted here.🤖 Generated with Claude Code