dag target: tokens are written separated, so emitted text reads back as the tokens emitted

[gunbai-bot]

#13099 (eager-crab-610) has merged; this branch has main merged in and the diff is now only this change's eight files.

Coordination with #13043 (royal-deer-478). This PR adds one hand-roster row, v2.test.emit.dag_target_text_round_trip.trt_verdicts, to v2.workflow.floor_pure_producer_share floor_cross_claim_pure_producers_warm. #13043 deletes that roster in favour of derived cross-claim demand. If #13043 lands first, I drop the row here and confirm the six parses are derived as shared, with the floor at 0 over cost. If this lands first, royal-deer-478 dispositions the row.

Defect

The dag target wrote its tokens with nothing between them. let x came out as letx, one identifier; if true then 1 else x came out as iftruethen1elsex, which the dag grammar's expr production accepts as a single name. Text round trips through the dag target were reading back a different construct and passing.

There were two causes, not one:

• dag_target_model (and its three sibling constructors) declared token_class_emit_transforms empty.
• The flat token fold bound_tokens_source_text, which serialize_concrete_syntax_tokens_to_source_string calls for every value-expression body, never read that map at all. Only the relation-row route did. So rows on the dag model alone would not have fixed a Bind.

Change

• Separation is rows on the token classes, in the shape verilog already uses (EmitSpellingWrap { prefix: "", suffix: " " }); no new mechanism. dag_token_class_emit_transforms derives one row per token class from dag_lex_rules, so the lex rule set stays the one list of classes.
• Every class gets a row, not only words. Punctuation glues too: > then = unseparated is the one token >= (claimed below), and / / opens an annotation. Whitespace is trivia in the dag lexer, so the space cannot change the tree.
• The flat fold reads the map. bound_tokens_source_text_with_transforms is the fold; bound_tokens_source_text is that fold with the empty map, so its direct callers (bash) are byte-identical. serialize_concrete_syntax_tokens_to_source_string passes the target's map. Both folds now reach one layout_or_atom_in.

Controls

v2.test.emit.dag_target_text_round_trip. Every round trip is: tokens from the real emitter -> text through the dag rows -> lexed with dag_lex -> the lexed token classes equal the emitted ones, in order -> those lexed tokens parsed once at expr to one tree of the expected shape. The join comes first; a let count is never asked in its place.

• (a) the block-scoped Bind { let k = (v) { b } } at text grain, one claim per body: a bare name, an empty brace literal {}, a --led expression, and a Bind. Plus a Bind as the value.
  • Shape asserted: one let_expr for the first three; two for the nested ones. A Bind in the value group sits under the outer let; a Bind in the body block does not (the block is its own statement after the let). The claims state which.
• (a) mixed expression if true then 1 else x: the join, and one if_expr.
• (b) the red, kept enrolled: the same tokens with the empty map (the renderer main has) read back as other tokens; the mixed expression reads back as exactly [ident].
• punctuation: > = reads back as two tokens with the rows and as >= without.
• inhabitance on the real route: serialize_concrete_syntax_tokens_to_source_string over dag_target_model() writes a Bind that lexes back as emitted. Dropping the rows from the model, or the map from the serializer, fails it.

The six parsing round trips are computed once, in trt_verdicts, a nullary pure producer enrolled WARM in v2.workflow.floor_pure_producer_share (the same arrangement #13099 uses for dbl_verdicts); each claim reads its Bool. See Cost for why.

One thing I got wrong first, and it is the class itself. My first red asserted that the unseparated nested Bind does not parse to two lets. It returned false: that text does parse to two nested lets, because letx = (..) reads as a bare-assignment binding. So a let count cannot tell the good text from the bad one; only the token join does. The red is now the token join, and the receipt is in the failure-mode row.

Recorded red on main (a0a5c62), by scratch probe, not landed: iftruethen1elsex parses at expr with one token and no if_expr; spaced, six tokens and one if_expr. Nested let … in text is rejected at expr on main in either spelling, which is why (a) needs #13099's block form.

What ran

All by gunbc run --function locally, one claim per process. The binary was borrowed from another worktree and is one commit behind main in the seed, so CI is the authority; none of this is a floor run.

• the ten claims in dag_target_text_round_trip: true. The six parsing round trips were re-run after the rewrite; the two reds, the punctuation claim and the inhabitance claim were run before it and their code is unchanged
• dag_bind_let_block_scoped (nested_bind_emitted_block_scoped_reparses_to_the_same_binds, a_single_bind_emits_block_scoped_tokens): true
• (c) rust_bind_let_emit_holds and ts_bind_let_iife_emit_exact_holds (exact text): true. Rust and TypeScript models keep the empty map.
• bind_emit_holds (dag emit equals serialize): true

Other targets on the flat route (asked by stern-bear-500)

Precisely what changed: bound_tokens_source_text itself still passes the empty map, so its direct callers (bash, bash_orch_if) cannot change. Only serialize_concrete_syntax_tokens_to_source_string now passes the target's map. It is reached from four places: a bodied arrow's value-expression tokens, an import projection, a produced declaration, and a semantic declaration. The last builds its own serialize target with the empty map (semantic_decl_serialize_target), so it cannot change either.

No target's emitted bytes changed. None of verilog, swift rows, sql, gha or bash declares a value-expression projection, an import projection, a bodied scaffold or produced-declaration support, so their own emission never reaches that serializer. One exact-text claim per target, executed after the change, all true:

target	claim (exact text)	result
verilog	w_interlock_emits_expected_bytes_through_the_generic_fold	true
bash fold	bash_fold_command_var_ref_x_holds, bash_fold_command_arbitrary_lit_quote_escape_holds	true
bash	bash_emit_embedded_quote_holds, bash_emit_bound_words_holds	true
sql fold	sql_fold_create_table_with_pk_holds	true
gha fold	gha_fold_pilot_job_byte_identical_holds	true
swift rows	string_literals_escape_statically_and_keep_extended_text_verbatim, a_member_with_a_body_is_blank_separated_and_nested	true
rust directive fixture	emit_directive_rust_escapes_string_literal_holds	true
bash directive	emit_directive_bash_message_flows_holds	true

These claims run each target's own route, which is the point: that route is not the flat serializer. I did not run sql_target (only its fold) or every claim in each file.

What does change is a direct call to the flat serializer with a transformed class, which no production path makes today. New claim v2.test.emit.target_text_layout the_flat_token_route_applies_the_targets_transform_rows pins it on verilog: assign = ; now render "assign = ;\n". Before, that fold wrote the bare lex literals with no rows (assign=;, no line break); I derive the before text from the old fold, I did not execute it. This is a fix: it is the spelling the relation-row route already gives those classes.

Cost, read from the floor run on head b8ace9b (budget 72,300 eval steps per new witness)

That run executed 677 claims, 667 passed, 5 known-red held, 0 failed, and refused on cost alone:

• my nested-Bind claim, as first written (render, lex and parse): 122,092 steps, over.
• my mixed-expression claim (render, lex, parse): 67,139, under.
• my other four claims did not appear on the over-cost line (under the 100 ms line).
• two of target_model: Optional Bind separator; dag emits a Bind block-scoped (ahead of #13056's let-in drop) #13099's claims were also over (87,238 and 90,020); eager-crab-610 has since reworked them on that branch, merged here.

One expression parse is at or past a new witness's budget, and the nested one is far past it. The second floor run (head 5097bbc, nested claim cut to the token join only) passed. The text-grain controls then required (sharp-raven-357, via stern-bear-500) put a parse back in every Bind case, so the parsing round trips now run once each in the warm producer trt_verdicts and no claim pays a parse. The floor run on head d475a8a passed: 683 claims executed, 673 passed, 5 known-red held, 0 failed, 0 over the cost requirement, and none of this PR's claims on the over-cost line.

Ledger

New row gunbc.recurring_failure_mode.round_trip_claim_passes_on_emitted_text_reread_as_another_construct. Rung now: mechanically preventable. Next-rung trigger: the serializer checks, from the target's own lex rules, that each adjacent pair it writes lexes back as itself, for every target.

dag_target_emits_only_its_fixture_row still says the dag model's transform map is empty. That was true at the commit it cites; I left the receipt alone.

🤖 Generated with Claude Code