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

dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag

@@ -0,0 +1,25 @@
+module gunbc.recurring_failure_mode.round_trip_claim_passes_on_emitted_text_reread_as_another_construct
+
+import std.types { NonEmptyStr }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data round_trip_claim_passes_on_emitted_text_reread_as_another_construct: RecurringFailureMode = RecurringFailureMode {
+  identity: "round_trip_claim_passes_on_emitted_text_reread_as_another_construct" as NonEmptyStr,
+
+  receipts: [
+    "**a round-trip claim passes because malformed emitted text is re-read as a DIFFERENT valid construct** (INVALID STATE: an emit -> text -> ingest claim whose assertion is satisfied by a tree the emitter did not write.) The emitted text is wrong, the reader ACCEPTS it as something else, and the claim asks only a property both trees have: that the text parses, that a count is at least one, that no refusal fired. HARM: the claim is green, its assertion is true, and it establishes nothing about the round trip (DESIGN 3: the designed fixture reaching the same verdict through a different mechanism). Every later claim built on the same renderer inherits the pass.",
+    "RECEIPT, found by eager-crab-610 building gunbc#13099. The dag target declared no separation between tokens: its lex is `v2.extdeps.languages.dag` `dag_lex` and `dag_target_model` carried `token_class_emit_transforms` empty, and the flat token fold `v2.std.compilers.target_model` `bound_tokens_source_text` never read that map at all. A Bind rendered with `let` and `x` run together as `letx=(a)` inside its braces; `letx` lexes as one identifier, and the text was read as a bare assignment. A text-based version of that PR's Bind claims passed on it. EXECUTED on main a0a5c62161 (swift-lark-785, a scratch probe run by `gunbc run --function`, not landed): the six tokens `if true then 1 else x` render as `iftruethen1elsex`, which the dag grammar's `expr` production ACCEPTS as one identifier with no conditional in it; spaced, the same tokens read as one `if_expr`. EXECUTED on this change's tree: the unseparated nested Bind (each `let x` written `letx`) parses to TWO nested `let_expr` nodes, the same count the separated text gives, because `letx = (..)` reads as a bare-assignment binding. A claim counting lets cannot tell the two texts apart; the first draft of this change's own red asserted that count and was wrong.",
+    "DISTINGUISHING FACTS. (1) The reader is total enough to accept the damage: whitespace is the only thing separating a keyword from a name, so its loss yields a valid token, not a lex error. (2) The claim's oracle is weaker than identity: it inspects a property of the re-read tree rather than joining it to what was emitted. (3) The red is authorable and cheap: render the same tokens through the suspect renderer and compare the TOKEN CLASS SEQUENCE read back to the sequence emitted. That join needs no parse and fails on any merge or split of tokens.",
+    "RECOGNITION RULE. A round-trip claim must join what was read back to what was emitted at identity grain (the token class sequence, then the production stamps of the tree), never only ask that the text parses. A claim that would still pass if the emitted text were replaced by ANY valid expression is not a round-trip claim. Where the emitter's product is a token sequence, parsing those tokens directly (as `v2.test.emit.dag_bind_let_block_scoped` does) is a sound claim about the EMITTER and is silent about the TEXT; the text owes its own claim.",
+    "RUNG FOUND AT: silent wrongness on the text path (outside the ladder, DESIGN 4b): malformed text was Accepted as another construct. NOW: mechanically preventable. The dag target's separation is declared as rows on its token classes (`dag_token_class_emit_transforms`, one row per class the lex rule set declares) and both text folds read them; `v2.test.emit.dag_target_text_round_trip` holds the join and keeps the red enrolled (`mixed_expression_text_without_separation_is_one_identifier`, `nested_bind_text_without_separation_reads_back_as_other_tokens`). The state stays writable: a target may still declare no rows. CEILING: structurally guaranteed, because whether two adjacent spellings lex back as the two classes emitted is decidable from the lex rule set. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: the serializer derives or checks separation from the target's own lex rules for every adjacent pair it writes and refuses, located, a pair that would not lex back as itself, for every target rather than by rows authored per target. Sufficient for: no Accepted emission whose text lexes to a different token sequence.",
+  ],
+
+  evidence: [
+    DeclarationRef { module_path: "v2.extdeps.languages.dag", decl_name: "dag_token_class_emit_transforms", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.std.compilers.target_model", decl_name: "bound_tokens_source_text_with_transforms", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.emit.dag_target_text_round_trip", decl_name: "mixed_expression_text_without_separation_is_one_identifier", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.emit.dag_target_text_round_trip", decl_name: "trt_bind_text_round_trips", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.emit.dag_target_text_round_trip", decl_name: "the_dag_target_model_serializes_a_bind_with_its_tokens_separated", field: WholeDeclaration },
+  ],
+}

src/v2/compiler/target_serialize.dag

@@ -97,7 +97,7 @@ import v2.std.compilers.target_model {
   target_type_expr_emitted_kind,
   type_expression_projection_from_target,
   lex_rules_literal,
-  bound_tokens_source_text,
+  bound_tokens_source_text_with_transforms,
   TargetText,
   text_atom,
   target_text_seq,
@@ -624,10 +624,11 @@ fn serialize_concrete_syntax_tokens_to_source_string(
   target: TargetModel,
   tokens: List<ConcreteSyntaxToken>
 ) -> Outcome<TargetText> {
-  bound_tokens_source_text(
+  bound_tokens_source_text_with_transforms(
     tokens: tokens,
     lex: target.lex,
-    binding_spellings: target.binding_spellings
+    binding_spellings: target.binding_spellings,
+    transforms: target.token_class_emit_transforms
   )
 }
 

src/v2/extdeps/languages/dag.dag

@@ -97,6 +97,8 @@ import v2.std.compilers.lexing {
   TriviaRule,
   WhitespaceChar,
   lex_rule_set_insert_token_classes,
+  lex_rule_set_matching_rules,
+  lex_rule_token_class_optional,
   lex_rule_set_token_class_map,
   lex_rule_set_keyword_class_member,
   lex_rule_set_token_class_member,
@@ -179,7 +181,7 @@ import v2.std.compilers.target_model {
   TargetValueExpressionProjection,
   grammar_relation_row_attach_bodied_scaffold,
   target_operator_realizations_catalog_node,
-  value_expr_projection_bundle_node, target_model_emit_transforms_empty,
+  value_expr_projection_bundle_node, EmitSpellingWrap, TokenClassEmitTransform,
   Prepend,
   BlockEvaluationMode,
   ValueProducing,
@@ -681,6 +683,25 @@ fn dag_lex() -> LexRules {
   ModeledLexRules { root: dag_lex_rules() }
 }
 
+// EVERY dag TOKEN CLASS IS WRITTEN WITH ONE SPACE AFTER IT. Whitespace is trivia in dag_lex_rules, so
+// a space after a token cannot change the tree read back; its absence can. Two adjacent word tokens
+// lex as one identifier ("let" "x" -> "letx"), and two adjacent punctuation tokens can spell a third
+// (">" "=" -> ">=", "/" "/" opens an annotation), so no token class is exempt. The rows are derived
+// from the lex rule set, the one authority for which token classes exist, in the shape the other
+// targets declare their separation in (v2.extdeps.languages.verilog verilog_emit_layout_transforms).
+fn dag_token_class_emit_transforms() -> Map<Symbol, TokenClassEmitTransform> {
+  fold_list(
+    xs: lex_rule_set_matching_rules(rules: dag_lex_rules()),
+    empty: empty_map(),
+    cons: fn(acc, rule) {
+      match lex_rule_token_class_optional(rule: rule) {
+        Present { value: c } => map_insert(m: acc, key: c, value: EmitSpellingWrap { prefix: "", suffix: " " })
+        Absent => acc
+      }
+    }
+  )
+}
+
 fn dag_grammar_atom(id: Symbol) -> Node {
   Node {
     kind: TypeNode {
@@ -3901,7 +3922,7 @@ fn dag_target_model_with_fidelity_quotient(quotient: Node) -> TargetModel {
     bundle: dag_target_model_bundle_with_fidelity_quotient(quotient: quotient),
     lex: dag_lex(),
     binding_spellings: dag_binding_spellings(),
-    token_class_emit_transforms: target_model_emit_transforms_empty,
+    token_class_emit_transforms: dag_token_class_emit_transforms(),
     authority_source_text: dag_source_text,
     runtime_row: target_emit_host_runtime_row_unconfigured
   }
@@ -6005,7 +6026,7 @@ fn dag_bodied_fn_target_model(
         bundle: dag_bodied_fn_target_model_bundle_node(spec: spec),
         lex: dag_lex(),
         binding_spellings: dag_binding_spellings(),
-        token_class_emit_transforms: target_model_emit_transforms_empty,
+        token_class_emit_transforms: dag_token_class_emit_transforms(),
         authority_source_text: spec.authority_source_text,
         runtime_row: row
       }
@@ -6015,7 +6036,7 @@ fn dag_bodied_fn_target_model(
         bundle: dag_bodied_fn_target_model_bundle_node(spec: spec),
         lex: dag_lex(),
         binding_spellings: dag_binding_spellings(),
-        token_class_emit_transforms: target_model_emit_transforms_empty,
+        token_class_emit_transforms: dag_token_class_emit_transforms(),
         authority_source_text: spec.authority_source_text,
         runtime_row: target_emit_host_runtime_row_unconfigured
       }
@@ -6346,7 +6367,7 @@ fn dag_target_model() -> TargetModel {
     bundle: dag_target_model_node(),
     lex: dag_lex(),
     binding_spellings: dag_binding_spellings(),
-    token_class_emit_transforms: target_model_emit_transforms_empty,
+    token_class_emit_transforms: dag_token_class_emit_transforms(),
     authority_source_text: dag_source_text,
     runtime_row: target_emit_host_runtime_row_unconfigured
   }

src/v2/extdeps/languages/rust_emit_small_fixtures.dag

@@ -46,8 +46,8 @@ fn rust_emit_small_translation_claim() -> TranslationClaim {
   }
 }
 
-// serialize_concrete_syntax_tokens_to_source_string reads only lex and
-// binding_spellings. No bundle lookup, host execution or produced declaration
+// serialize_concrete_syntax_tokens_to_source_string reads only lex,
+// binding_spellings and token_class_emit_transforms. No bundle lookup, host execution or produced declaration
 // occurs on this path.
 fn rust_emit_small_serialization_target(
   lex: LexRules,

src/v2/std/compilers/target_model.dag

@@ -1371,10 +1371,16 @@ fn target_text_is_empty(t: TargetText) -> Bool {
   t.empty
 }
 
-fn bound_tokens_source_text(
+// THE FLAT TOKEN FOLD CONSULTS THE SAME EMIT-TRANSFORM MAP AS THE RELATION-ROW ROUTE. It read only
+// the lexer and the binding spellings, so a target whose separation is declared on its token classes
+// (token_class_emit_transforms) lost it on this route and its tokens ran together: the dag target
+// wrote a Bind as "letx=ainx", one identifier. A transform is a fact about how a TOKEN CLASS
+// renders, whichever fold spells the token, so both folds reach layout_or_atom_in.
+fn bound_tokens_source_text_with_transforms(
   tokens: List<ConcreteSyntaxToken>,
   lex: LexRules,
-  binding_spellings: Map<Symbol, String>
+  binding_spellings: Map<Symbol, String>,
+  transforms: Map<Symbol, TokenClassEmitTransform>
 ) -> Outcome<TargetText> {
   fold_list(
     xs: tokens,
@@ -1388,14 +1394,20 @@ fn bound_tokens_source_text(
               bind_outcome(
                 o: lex_rules_literal_for_class(rules: lex, token_class: tc),
                 f: fn(spelling) {
-                  Accepted { value: target_text_seq(acc: partial, next: text_atom(lexeme: spelling)), diagnostics: ad }
+                  bind_outcome(
+                    o: layout_or_atom_in(transforms: transforms, token_class: tc, spelling: spelling),
+                    f: fn(text) { Accepted { value: target_text_seq(acc: partial, next: text), diagnostics: ad } }
+                  )
                 }
               )
-            BoundToken { token_class: _, binding: b } =>
+            BoundToken { token_class: tc, binding: b } =>
               bind_outcome(
                 o: bound_spelling_from_map(binding_spellings: binding_spellings, binding: b),
                 f: fn(spelling) {
-                  Accepted { value: target_text_seq(acc: partial, next: text_atom(lexeme: spelling)), diagnostics: ad }
+                  bind_outcome(
+                    o: layout_or_atom_in(transforms: transforms, token_class: tc, spelling: spelling),
+                    f: fn(text) { Accepted { value: target_text_seq(acc: partial, next: text), diagnostics: ad } }
+                  )
                 }
               )
           }
@@ -1404,6 +1416,19 @@ fn bound_tokens_source_text(
   )
 }
 
+fn bound_tokens_source_text(
+  tokens: List<ConcreteSyntaxToken>,
+  lex: LexRules,
+  binding_spellings: Map<Symbol, String>
+) -> Outcome<TargetText> {
+  bound_tokens_source_text_with_transforms(
+    tokens: tokens,
+    lex: lex,
+    binding_spellings: binding_spellings,
+    transforms: target_model_emit_transforms_empty
+  )
+}
+
 fn target_binding_spelling_lookup(
   target: TargetModel,
   binding: Symbol
@@ -1524,8 +1549,8 @@ fn bound_token_spelling_from_model(
   )
 }
 
-fn layout_or_atom(target: TargetModel, token_class: Symbol, spelling: String) -> Outcome<TargetText> {
-  match map_get(target.token_class_emit_transforms, token_class) {
+fn layout_or_atom_in(transforms: Map<Symbol, TokenClassEmitTransform>, token_class: Symbol, spelling: String) -> Outcome<TargetText> {
+  match map_get(transforms, token_class) {
     Accepted { value: Present { value: transform }, diagnostics: d } =>
       match transform {
         EmitLineBreaks { before: b, after: a } =>
@@ -1542,6 +1567,10 @@ fn layout_or_atom(target: TargetModel, token_class: Symbol, spelling: String) ->
   }
 }
 
+fn layout_or_atom(target: TargetModel, token_class: Symbol, spelling: String) -> Outcome<TargetText> {
+  layout_or_atom_in(transforms: target.token_class_emit_transforms, token_class: token_class, spelling: spelling)
+}
+
 // THE CARRIER-NATIVE TOKEN SPELLING: the lexeme (fixed: the lex literal; bound: the binding's
 // spelling) under the token class's emit transform, as TargetText, so an EmitLineBreaks class keeps
 // its line breaks. It takes the token already decoded: the serializer decodes each token node once to