v2 parse: occurrence ids minted once per parse across a rejected attempt (single_arm_match 6/6, #13056 regression)

[gunbai-bot]

What broke

v2.test.claim.body_lowering.single_arm_match was 4/6 starting at #13056. The failing claims are two_arm_match_still_accepts_holds and three_arm_match_keeps_every_arm_holds. They sat in floor_cost_debt censored chunk 03, so the red was masked.

Re-derivation (DESIGN §6b)

The symptom link was conservation, and conservation was correct. The red was conservation_reason_unmeasured / AtomExtentUnreadable, one per arm after the first. No arm was dropped: every arm is present in the normalized tree.

Walking back up the chain:

• dag grammar: expr/stmt/let/if/arg/match_arm overlap rows to zero by restructuring #13056 makes every arm body the statement repetition guarded by !(pattern =>) (dag_grammar_match_arm_stmt_body_statement).
• At arm 2 the guard parses pattern, and the miss path memoizes it. The guard then rejects.
• A rejected subparse returns no provenance, so the occurrence allocator rewinds. The memo keeps the nodes minted under it.
• The repetition stamp and the arm wraps then reissue those ids.
• Arm 2 is served pattern from the memo. parse_prov_merge advances the allocator only after the reuse has already happened. span_index_adopt keeps the index's earlier event, so the arm-2 atom (_, Unconditional SetIamPolicy preflight #130) resolves to the repetition stamp.

Earliest unjustified boundary: the allocator is parse-global, but it was carried in path-local ParseProvenanceState.

Repair

• ParseTableRealization.minted_through is part of the state every result threads, whether accepted or rejected.

• Only a stored accepted memo entry raises it (parse_table_note_retained in parse_table_insert).

• Provenance resumes past it (parse_prov_past_memo) only where a parse resumes after a rejection, not on every accept. An accepted path never rewinds. The five resume sites are:

  • the next ordered alternative of a Choice;
  • an absorbed Optional;
  • a stopped repetition;
  • a repetition element that accepts without progress (parse_expr_repeat_step's no-progress arm, added in review);
  • a not-predicate whose element failed.

  Every other rejection propagates to one of these. parse_expr_not_predicate's FIRST-skip arm attempts nothing, so it needs no resume. The final artifact wrap also resumes past the high-water.

• The advance is a comparison. In the common case it returns provenance unchanged.

• A parse that retains nothing mints exactly as before.

• Cost: an earlier head advanced at parse_expr_with_first entry and exit on every subparse, which pushed two parse_test_fn_decl_return_clause claims over the new-witness step budget. Advancing only at resume sites fixed this.

  claim	main	this head
  nfbcp_hazard_no_return_type_retains_wrapper_holds	76820	77567
  nfbcp_repeated_declaration_refuses_at_the_second...	69830	70547

  Numbers are eval_steps from claim_batch on BuildBuddy.

Evidence

All runs used claim_batch on BuildBuddy, with the fixed tree and the ed68b5573b parse in the same dispatch.

claim	before	after
single_arm_match (6)	4/6	6/6
RED parse_memo_frame_replay parse_memo_entry_from_a_rejected_guard_resolves_like_a_memo_free_parse (hand grammar of the arm-body guard shape; Memoize vs Recompute oracle; asserts a memo hit)	FAIL	PASS
RED parse_memo_entry_from_a_discarded_empty_element_resolves_like_a_memo_free_parse (S = H P y, H = x ((P z)?)*, P = a; the no-progress repetition arm)	FAIL at 33bc475	PASS
positive control parse_without_a_stored_entry_mints_the_ids_it_minted_before (same guard, store refused; ids pinned to the pre-repair parse)	PASS	PASS
other parse_memo_frame_replay, parse_table_content_key, parse_table_memo_governed claims	PASS	PASS

Real corpus, measured with reference_conservation_census_for_paths on src/v2/std/node.dag:

• unmeasured went from 253 to 0
• conserved rose by 253
• dropped stayed at 88

So the same defect was silently degrading corpus files, not only the fixture.

Other sites with the memo-across-reject shape

Every rejection path is closed by this change, because the table is the only state that crosses a reject. The sites that produce such paths are:

• Choice: every failed alternative.
• Optional / Repeat: an absorbed rejection.
• Not-predicates in v2.extdeps.languages.dag:
  • dag_grammar_declared_path_expr
  • dag_grammar_stmt_expr
  • dag_grammar_let_in_refusal_expr
  • dag_grammar_expr_expr (×2)
  • dag_grammar_additive_newline_minus_guard
  • dag_grammar_arg_expr
  • dag_grammar_match_arm_stmt_body_statement
  • dag_grammar_match_arm_expr
  • dag_grammar_arrow_lambda_body_expr
  • dag_grammar_status_pattern_expr
  • dag_grammar_op_requires_expr
  • dag_grammar_module_expr

Next-rung trigger, recorded on the RFM row: the parse's mint sites read the allocator from the table itself.

Also

• single_arm_match now imports LiveTreeDisposition / SubstrateInputsOnly. Without them its entry resolution was refused. Its roster row moves from ActiveDebt to ImportsFixed.
• The two- and three-arm identities are removed from censored chunk 03. The floor decides whether they fit its budget.
• New RFM row: memo_retained_occurrence_id_reminted_after_a_rejected_attempt. It corrects the triage reading on match_arms_after_the_second_are_dropped_at_v2_body_lowering: this was not an arm drop.

🤖 Generated with Claude Code

[briansrls]

REQUEST_CHANGES at exact head 33bc4755ab153898981dcb1c86d0e6f167b9c20e, against DESIGN.md §§3 and 5. One remaining allocator-resume defect; the regression diagnosis, preserved conservation checks and bounded-cost direction are accepted.

Accepted

minted_through belongs to the table state that survives speculative parsing. parse_table_insert advances it only for a stored accepted entry, and takes the maximum; refused stores and rejected entries do not invent retained nodes. parse_prov_past_memo advances only the allocator, leaving the caller's index and frame unchanged. The four changed rejection-resume arms consume that mark, and all table reconstructions in this diff retain it.

The existing guarded-memo RED runs the real parser, requires a memo hit, and compares its node loci with a Recompute run. The no-store control keeps its pre-repair occurrence-id sequence. The two single_arm_match claims return from censored chunk 03 to the ordinary floor, the missing imports and corresponding keyed retirement agree, and neither conservation nor a budget is relaxed.

Blocker: Repeat also discards provenance on an ACCEPTED, zero-progress result

In v2.compiler.parse::parse_expr_repeat_step, the ParseExprAccepted arm compares the two stream positions. When they are equal, it returns:

ParseRepeatAcc {
  ...
  done: true,
  prov: acc.prov,
  table: table1
}

That retains the attempted element's memo but restores the pre-attempt allocator. parse_expr_repeat immediately calls parse_stamp_derived_repeat(..., prov: result.prov) without advancing it. Thus the premise that the accepted path never rewinds is false at this branch. The new advance on Repeat's ParseExprRejected arm does not cover it.

A bounded specimen, using the same grammar/token helpers as the existing witness:

S = H P y
H = x ((P z)?)*
P = a
input = x a y

Here ? is v2.std.grammar.Optional; the repeated element is Optional(Sequence(Nonterminal(P), Terminal(z))). There are no undefined or duplicate productions, no left-recursion cycle and no Choice ambiguity. The current grammar preparation does not reject a nullable Repeat element; the repeat loop explicitly handles its no-progress acceptance.

At a, the optional's element parses and memoizes P, then fails at z. Optional correctly returns zero-width acceptance with its allocator advanced past the retained P atom. Repeat then takes the equal-position arm above and drops that advance while retaining P's memo. The empty-repeat stamp reuses P's retained atom id. Later S serves P from the memo; parse_prov_replay_frame reaches span_index_adopt, which keeps the existing repeat-stamp event for that id instead of P's source event. The final production-wrapper advance is too late to repair this collision.

This is a source-derived counterexample, not an executed claim or a claim that single_arm_match remains red. It is the same retained-memo/rolled-back-allocator class this PR repairs. The existing guarded specimen stops Repeat through rejection, so it does not exercise this accepted/no-progress exit.

Bounded correction and control

Advance the allocator on this provenance-discard boundary too. For example, the equal-position arm can use:

prov: parse_prov_past_memo(prov: acc.prov, table: table1)

Keep acc.prov's index and frame: copying prov1 wholesale would retain provenance for a capture the repetition discarded. No return to per-expression entry/exit checks, budget increase, cost row, or full allocator migration is required.

Add the nullable-element specimen through grammar validation and the real parser, with a Memoize/Recompute locus comparison and an asserted memo hit. It should fail at this head and pass with the bounded repair; removing this branch's advance should fail that control. Preserve the existing rejected-guard, abandoned-frame, nested-frame and no-store controls. Describe the boundary as discarded provenance, not rejection alone, in the existing receipt.

Evidence

Reviewed the eight-file diff, exact-head DESIGN, table insertion/copying, memo replay and wrapping, choice/optional/repeat/predicate paths, grammar validation/preparation, and the witness bodies. Verified GitHub run 37262411168: floor, generated, emit-build and aggregate witnesses all succeeded on the requested SHA. The reported BuildBuddy before/after counts, approximately 1% cost delta and native corpus census remain author-reported; I did not execute the compiler, claims or mutants in this session. The PR head was unchanged immediately before submission.

[gunbai-bot]

Review follow-up (side-chat, at 33bc475):

• Fixed a fifth resume site: parse_expr_repeat_step's no-progress arm discarded the element's provenance while its memo entries stayed. It now resumes past the high-water.
• New RED parse_memo_entry_from_a_discarded_empty_element_resolves_like_a_memo_free_parse (S = H P y, H = x ((P z)?)*, P = a). It fails at 33bc475 and passes now.
• Audit of arms that return pre-attempt provenance: parse_expr_not_predicate's FIRST-skip arm makes no attempt, so it is sound. Every other rejection propagates to one of the five resume sites: next ordered alternative, absorbed optional, repetition stopped by a rejected element, repetition element accepted without progress, and not-predicate whose element failed.
• eval_steps on BuildBuddy (main / head): nfbcp_hazard_no_return_type_retains_wrapper 76820 / 77567; nfbcp_repeated_declaration_refuses 69830 / 70547. These are unchanged by this fix.

[gunbai-bot]

Re the REQUEST_CHANGES at 33bc475: the remaining allocator-resume defect is fixed at 5c555ab. parse_expr_repeat_step's no-progress arm now resumes past minted_through.

• RED: parse_memo_entry_from_a_discarded_empty_element_resolves_like_a_memo_free_parse (S = H P y, H = x ((P z)?)*, P = a) fails at 33bc475 and passes at 5c555ab. It uses the memo-hit locus oracle and asserts a hit.
• Audit: the only other arm that returns pre-attempt provenance is parse_expr_not_predicate's FIRST-skip arm, which attempts nothing.
• eval_steps (main / head): 76820 / 77567 and 69830 / 70547.

The block comment above parse_memo_entry_retains_through names all five resume sites. Please re-review when convenient.

— sent from sunny-ant-198

[briansrls]

APPROVE at exact requested head 5c555ab1b27af6a9c5c157a54bfc3c90230d28ab, against DESIGN.md §3's executing pairing obligation and §5. The allocator-resume blocker in review 5410417820 is closed. This is a source approval, not permission to bypass required CI. The current branch has advanced to c4a9a023a0ed87abf1e51979cad43ce564bdd61c; that later head is not covered.

The missing boundary is repaired

v2.compiler.parse::parse_expr_repeat_step now calls parse_prov_past_memo(prov: acc.prov, table: table1) in the accepted-but-zero-progress arm. The next repetition stamp therefore allocates beyond the nodes the attempted element left in the memo. Crucially, it retains the pre-attempt index and frame; it does not copy prov1 wholesale and import provenance for the discarded capture.

The four previously repaired resume sites remain: ordered choice's next alternative, Optional's absorbed rejection, Repeat's rejected element, and the not-predicate whose attempted element failed. The fifth is this accepted/no-progress exit. The not-predicate FIRST-skip arm retains its original provenance and table without attempting its element, so it creates no new retained-memo obligation. The ordinary accepted/progress arms continue threading the producer's provenance rather than restoring pre-attempt state. No per-expression entry/exit check is reintroduced.

The new control exercises the defect's real route

parse_memo_entry_from_a_discarded_empty_element_resolves_like_a_memo_free_parse uses the requested specimen:

S = H P y
H = x ((P z)?)*
P = a
input = x a y

The fixture passes through grammar_validate_for_parse, grammar analysis and the existing real-parser runner. It is not a supplied allocator/result record. Its Optional memoizes P, absorbs failure at z, and makes Repeat take precisely its accepted/no-progress exit before S later serves P from the memo.

The oracle requires the Memoize run to have a hit, the Recompute run to have none, and a nonempty, equal sequence of node-locus readings, with missing index entries failing the claim. This discriminates the retained P atom being attributed to the repetition stamp. The reported FAIL at 33bc475 / PASS here is consistent with the inspected producer and claim; I did not execute that comparison myself.

The complete increment from 33bc4755ab153898981dcb1c86d0e6f167b9c20e is one commit changing only the parser's one resume line and adding this witness. Existing rejected-guard, abandoned-frame, nested-frame and pinned no-store-ID controls are unchanged. Conservation, budget declarations and cost-debt membership are unchanged by this increment. The previously accepted single_arm_match repair and return of its two retired identities to ordinary floor checks remain accepted.

CI correction and review scope

I cannot confirm the request's statement that GitHub's floor is green at this SHA. The exact-head PR-triggered run returned by GitHub is 37274427994, overall CANCELLED. Its floor job 111648223024 failed, with:

ChangedWitnessObservationFailed
UnimportedBareProvider RosterRetirementChanged
  dag/gunbc/machine_intake/mtcollins1_bmc_sensor_observation.dag#filter
  (Retired FileDeleted -> Retired ImportsFixed) base=origin/main

The job log confirms checkout of the requested SHA. That is a roster/base-comparison refusal, not a reported failure of the new parser claim; neither that roster nor its reader changes in this two-file increment. It is not an additional source blocker for this repair, but required CI must still pass on the eventual landing head. Any main merge or later-head resolution needs its own exact-head reconfirmation.

The reported single_arm_match 6/6, baseline/fixed RED and unchanged budget measurements remain author-reported. I executed no local claims, mutants or provider effects. The fetched PR body still describes an older per-entry/exit implementation; this approval covers the inspected five-resume-site implementation, not that stale description or a structural guarantee that every future mint must use the high-water mark.

[briansrls]

APPROVE at exact head f0e73e57412ad82aa0187932e34400658a814aa0. This closes my allocator-resume REQUEST_CHANGES at 33bc4755ab (review 5410417820). No new blocking finding. Land through the normal merge queue after its required checks pass on the composed revision; this is not a request to bypass those checks or merge from this session.

The outstanding parser defect is closed

The accepted/no-progress arm in parse_expr_repeat_step now keeps the pre-attempt index/frame but advances its allocator with parse_prov_past_memo(prov: acc.prov, table: table1). It no longer discards the allocator advance while retaining the element's memo. The rejected-element arm and the other three discard/resume boundaries retain the same protection. The not-predicate FIRST-skip arm attempts nothing and correctly returns the unchanged table/provenance.

The high-water mark advances only for an actually stored accepted memo entry, using a maximum; rejected entries and refused stores do not invent retained nodes. Table reconstructions preserve the mark. The advance changes the allocator alone, not the span index or frame. The final production-wrap guard remains. No conservation rule, grammar acceptance assertion, or cost budget is relaxed.

The added parse_memo_entry_from_a_discarded_empty_element_resolves_like_a_memo_free_parse uses the requested S = H P y; H = x ((P z)?)*; P = a; input x a y specimen. It validates the grammar and uses the real parser. Alongside the rejected-guard specimen, it requires a positive memo-hit count, zero Recompute hits, nonempty loci, and equality of the memoized and memo-free locus lists. Absent parse/locus results return false. The no-store control retains the pre-repair occurrence-ID list. An unexercised memo route or a parse that simply refuses cannot satisfy these controls.

Merge resolution preserves the repair

The parser file and complete replay-witness file are byte-identical to the repaired pre-merge commit 5c555ab1b2, independently checked by their Git blob IDs:

• 02_parse.dag: 812ff35dcfc6e61da63ac7a4b68e0eab945dd206.
• parse_memo_frame_replay_test.dag: fd71d697d04b802f01bd81f51619588206e1019e.

The final merge names only floor_unimported_bare_provider_debt_roster.dag as conflicted. Relative to its main parent, the net roster edit is exactly the keyed single_arm_match_test.dag / SubstrateInputsOnly standing changing from ActiveDebt to Retired { cause: ImportsFixed }; the added import supports that retirement. There are no roster-member additions or deletions in that net diff. The two- and three-arm identities remain removed from censored cost chunk 03, and their assertions are not rewritten.

Independently checked execution and prerequisite status

The commit-filtered workflow 37321867556 is successful. Its four jobs—floor, generated, emit-build and aggregate witnesses—all succeeded. Artifact 11352868508 identifies this exact SHA and was created on 2026-10-05. I downloaded its ZIP and verified SHA256 3b6741b214e767e2fe4fb121c93516d949f7015dafce144e546db1925443ce0a against GitHub's digest.

The TSV records all three newly added replay claims with outcome=pass, verdict_reached=true and cost_reading=observed: discarded-empty-element 15,853 eval steps / 65ms CPU; rejected-guard 16,235 / 67ms; no-store ID control 334 / recorded 0ms. This establishes exact-head execution of the repair discriminators, not merely compilation. The full single_arm_match 6/6 and baseline-red/native-corpus experiments remain author-run evidence; that six-claim suite is not present in this retrieved cost receipt, so I do not credit the receipt as independently rerunning it.

GitHub confirms #13400 merged on October 7 and #13458 merged on October 8. They postdate this head's October 5 CI, so the old green run does not establish today's composed-main result. The merge queue's fresh required execution remains the landing check, not a reason to invent another preparatory lane.

Non-blocking metadata: the PR body's Repair section still describes the earlier per-expression entry/exit advancement and parse_table_note_retained. Align it with the current five discard/resume boundaries, retained final-wrap guard and parse_memo_entry_retains_through; no further parser or witness change is requested.

Reviewed the pinned eight-file diff, prior review, relevant parser and witness bodies, merge metadata, prerequisite status and CI evidence. Local execution was limited to hashing and parsing the downloaded receipt. I did not run a compiler build, new mutation, corpus census or merge/enqueue operation.