From bacf9b8909a427a187dc376dbf11bfde47b7f280 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 10:23:55 +0000 Subject: [PATCH 1/9] target_model: a Bind's separator is Optional; dag emits a Bind block-scoped, { let k = (v) { b } } Operator/parent ruling (stern-bear-500, ruling A): ahead of the dag grammar dropping 'let x = e in body' (#13056), TargetBindLetShape.in_token becomes Optional. C/Rust/TypeScript keep Present(';'); dag declares Absent and a core Bind is emitted as a block whose first statement is the binding and whose last is the body: the value is parenthesised and the body braced so no continuation of the value can absorb the body, and the outer braces give the binding a statement position wherever the Bind stands. Absent travels in the projection bundle as its own atom, so a bundle missing the field still refuses. The dag bind family's tokens and authority text move to that spelling. Controls (v2.test.emit.dag_bind_let_block_scoped): a Bind nested as the value of a Bind, and bodies that are a bare name, an empty brace literal, a '-'-led expression and a nested Bind, each emitted through the dag projection and reparsed by the dag grammar to the same binds. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/extdeps/languages/c.dag | 3 +- src/v2/extdeps/languages/dag.dag | 13 +- src/v2/extdeps/languages/rust.dag | 3 +- src/v2/extdeps/languages/typescript.dag | 3 +- src/v2/std/compilers/target_model.dag | 90 ++++++++++- .../emit/dag_bind_let_block_scoped_test.dag | 150 ++++++++++++++++++ 6 files changed, 251 insertions(+), 11 deletions(-) create mode 100644 src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag diff --git a/src/v2/extdeps/languages/c.dag b/src/v2/extdeps/languages/c.dag index bf766fe6bb2..459e3e45a61 100644 --- a/src/v2/extdeps/languages/c.dag +++ b/src/v2/extdeps/languages/c.dag @@ -62,6 +62,7 @@ import v2.std.grammar { grammar_relation_tokens_node } import v2.std.compilers.target_model { + target_bind_let_separator_present, IntLiteralUnwired, InfixToken, canonical_operation_op_add, @@ -1098,7 +1099,7 @@ fn c_value_expression_projection() -> TargetValueExpressionProjection { let_form: TargetBindLetShape { let_token: ^c_token_unwired_let, assign_token: ^c_token_unwired_assign, - in_token: ^c_token_semicolon + in_token: target_bind_let_separator_present(token: ^c_token_semicolon) }, loop_form: TargetLoopShape { loop_token: ^c_token_unwired_loop }, record_construct_form: TargetRecordConstructShape { diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index f80d4b5f612..cf442a8b4b1 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -238,8 +238,8 @@ data dag_pick_false_source_text: String = "fn one_or_two() -> Int { if false the data dag_loop_source_text: String = "fn one() -> Int { loop 1 }" data dag_loop_wrong_value_source_text: String = "fn one() -> Int { loop 2 }" -data dag_bind_source_text: String = "fn one() -> Int { let x = 1 in x }" -data dag_bind_wrong_value_source_text: String = "fn one() -> Int { let x = 2 in x }" +data dag_bind_source_text: String = "fn one() -> Int { { let x = (1) { x } } }" +data dag_bind_wrong_value_source_text: String = "fn one() -> Int { { let x = (2) { x } } }" data dag_match_source_text: String = "fn one_or_two() -> Int { match true { true => 1, false => 2 } }" @@ -332,12 +332,17 @@ fn dag_bind_concrete_tokens() -> List { FixedToken { token_class: ^dag_token_arrow }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_type_int }, FixedToken { token_class: ^dag_token_lbrace }, + FixedToken { token_class: ^dag_token_lbrace }, FixedToken { token_class: ^dag_token_kw_let }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_bind_x }, FixedToken { token_class: ^dag_token_eq }, + FixedToken { token_class: ^dag_token_lparen }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_pick_lit_one }, - FixedToken { token_class: ^dag_token_kw_in }, + FixedToken { token_class: ^dag_token_rparen }, + FixedToken { token_class: ^dag_token_lbrace }, BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_bind_x }, + FixedToken { token_class: ^dag_token_rbrace }, + FixedToken { token_class: ^dag_token_rbrace }, FixedToken { token_class: ^dag_token_rbrace } ] } @@ -5828,7 +5833,7 @@ fn dag_value_expression_projection() -> TargetValueExpressionProjection { let_form: TargetBindLetShape { let_token: ^dag_token_kw_let, assign_token: ^dag_token_eq, - in_token: ^dag_token_kw_in + in_token: Absent }, loop_form: TargetLoopShape { loop_token: ^dag_token_kw_loop diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index f02bf8e7c6a..5d1d12d5110 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -144,6 +144,7 @@ import v2.std.compilers.coproduct_variant_shape { coproduct_all_variants_nullary } import v2.std.compilers.target_model { + target_bind_let_separator_present, IntLiteralDecimal, TargetCapabilityKey, ProducedDeclSupport, @@ -1204,7 +1205,7 @@ fn rust_value_expression_projection() -> TargetValueExpressionProjection { let_form: TargetBindLetShape { let_token: ^rust_token_kw_let, assign_token: ^rust_token_equal, - in_token: ^rust_token_semicolon + in_token: target_bind_let_separator_present(token: ^rust_token_semicolon) }, loop_form: TargetLoopShape { loop_token: ^rust_token_unwired_loop }, record_construct_form: TargetRecordConstructShape { diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index 95ffe98acfc..b5f6a82b8cb 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -99,6 +99,7 @@ import v2.std.grounding { } import v2.std.node_query { find_named_child } import v2.std.compilers.target_model { + target_bind_let_separator_present, IntLiteralUnwired, ProducedDeclParamSegment, ProducedDeclRenderRows, @@ -656,7 +657,7 @@ fn ts_value_expression_projection_full( let_form: TargetBindLetShape { let_token: ^ts_token_kw_let, assign_token: ^ts_token_eq, - in_token: ^ts_token_unwired_bind_in + in_token: target_bind_let_separator_present(token: ^ts_token_unwired_bind_in) }, loop_form: TargetLoopShape { loop_token: ^ts_token_unwired_loop diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index da130f7bfa3..f91c8137d55 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -1824,12 +1824,38 @@ type TargetConditionalShape { delimiting: ConditionalDelimiting } +// THE TOKEN BETWEEN A BINDING AND ITS BODY, WHEN THE TARGET HAS ONE. `let k = v in b` (`in`) and the +// statement-sequenced C/Rust/TypeScript forms (`;`) name it. A target whose let is a STATEMENT and +// has no separator token (dag: statement `let` only, `let x = e in body` dropped by the 2026-10-02 +// zero-ambiguity decisions) declares Absent, and a core Bind is emitted as a block that holds the +// binding as its first statement and the body as its last: `{ let k = (v) { b } }` +// (bind_let_block_scoped_tokens). The value is parenthesised and the body braced so that no +// continuation of the value can absorb the body -- a call suffix, an operator or a brace literal +// cannot follow a closed group into a block -- whatever the value and body are; the outer braces give +// the binding a statement position wherever the Bind stands, an expression position included. type TargetBindLetShape { let_token: Symbol assign_token: Symbol - in_token: Symbol + in_token: Optional } +// Absent is carried in the projection bundle as its own atom, never as a missing field: a bundle that +// lost the field still refuses at decode rather than reading as "no separator". +fn target_bind_let_separator_atom(in_token: Optional) -> Symbol { + match in_token { + Present { value: t } => t + Absent => ^target_bind_let_no_separator + } +} + +fn target_bind_let_separator_of_atom(atom: Symbol) -> Optional { + if atom == ^target_bind_let_no_separator { target_bind_let_separator_absent() } else { target_bind_let_separator_present(token: atom) } +} + +fn target_bind_let_separator_absent() -> Optional { Absent } + +fn target_bind_let_separator_present(token: Symbol) -> Optional { Present { value: token } } + type TargetLoopShape { loop_token: Symbol } @@ -3011,7 +3037,7 @@ fn decode_bind_let_shape_bundle(bundle: Node) -> Outcome { TargetBindLetShape { let_token: let_token, assign_token: assign_token, - in_token: in_token + in_token: target_bind_let_separator_of_atom(atom: in_token) } ) } @@ -6491,6 +6517,62 @@ fn bind_let_value_producing_tokens( key_tokens: List, value_tokens: List, body_tokens: List +) -> List { + match projection.let_form.in_token { + Present { value: in_token } => + bind_let_separated_tokens(projection: projection, in_token: in_token, key_tokens: key_tokens, value_tokens: value_tokens, body_tokens: body_tokens) + Absent => + bind_let_block_scoped_tokens(projection: projection, key_tokens: key_tokens, value_tokens: value_tokens, body_tokens: body_tokens) + } +} + +// `{ let k = ( v ) { b } }`, with the target's own block and group delimiters (closure body and +// primitive apply). See TargetBindLetShape for why each delimiter is there. +fn bind_let_block_scoped_tokens( + projection: TargetValueExpressionProjection, + key_tokens: List, + value_tokens: List, + body_tokens: List +) -> List { + list_append( + left: list_append( + left: list_append( + left: list_append( + left: list_append( + left: [ + FixedToken { token_class: projection.closure_form.body_open }, + FixedToken { token_class: projection.let_form.let_token } + ], + right: key_tokens + ), + right: [ + FixedToken { token_class: projection.let_form.assign_token }, + FixedToken { token_class: projection.primitive_apply_form.open } + ] + ), + right: value_tokens + ), + right: [ + FixedToken { token_class: projection.primitive_apply_form.close }, + FixedToken { token_class: projection.closure_form.body_open } + ] + ), + right: list_append( + left: body_tokens, + right: [ + FixedToken { token_class: projection.closure_form.body_close }, + FixedToken { token_class: projection.closure_form.body_close } + ] + ) + ) +} + +fn bind_let_separated_tokens( + projection: TargetValueExpressionProjection, + in_token: Symbol, + key_tokens: List, + value_tokens: List, + body_tokens: List ) -> List { list_append( left: list_append( @@ -6509,7 +6591,7 @@ fn bind_let_value_producing_tokens( right: value_tokens ), right: [ - FixedToken { token_class: projection.let_form.in_token } + FixedToken { token_class: in_token } ] ), right: body_tokens @@ -8956,7 +9038,7 @@ fn value_expr_projection_bundle_node(projection: TargetValueExpressionProjection target_model_named_edge( name: ^target_value_expr_field_in_token, target: target_model_type_atom_node( - identity: projection.let_form.in_token + identity: target_bind_let_separator_atom(in_token: projection.let_form.in_token) ) ) ] diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag new file mode 100644 index 00000000000..2e5845aa421 --- /dev/null +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -0,0 +1,150 @@ +module v2.test.emit.dag_bind_let_block_scoped + +import v2.compiler.parse { parse_module_prepared } +import v2.compiler.program_assembly { dag_prepared_grammar } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { + dag_bind_target_model, + dag_lex, + dag_value_expression_projection, + parse_production_emitted_identity_optional +} +import v2.std.compilers.target_model { + BoundToken, + FixedToken, + ConcreteSyntaxToken, + bind_let_value_producing_tokens, + bound_tokens_source_text, + render_target_text +} +import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.algebra { list_append } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.optional { Absent, Present } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A CORE BIND EMITTED THROUGH THE dag TARGET PARSES BACK AS THE SAME BINDS, AT EXPRESSION POSITION. +// dag declares no separator (v2.std.compilers.target_model TargetBindLetShape, in_token Absent), so a +// Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of +// another -- the hardest position, inside the group -- emits it with the real emitter +// (bind_let_value_producing_tokens over dag_value_expression_projection), renders it with the dag +// target's own spellings, places it where a value is owed (a data initializer) and reparses it with +// the dag grammar. It must parse, hold exactly two let_expr nodes with one inside the other, and +// carry no `in`: the text the emitter writes is text the grammar reads, one way. +fn dbl_token(binding: Symbol) -> List { + [BoundToken { token_class: ^dag_token_ident, binding: binding }] +} + +fn dbl_bind(value: List) -> List { + dbl_bind_body(value: value, body: dbl_token(binding: ^dag_binding_bind_x)) +} + +fn dbl_bind_body(value: List, body: List) -> List { + bind_let_value_producing_tokens( + projection: dag_value_expression_projection(), + key_tokens: dbl_token(binding: ^dag_binding_bind_x), + value_tokens: value, + body_tokens: body + ) +} + +fn dbl_nested_text() -> Outcome { + dbl_text(tokens: dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)))) +} + +fn dbl_text(tokens: List) -> Outcome { + let model = dag_bind_target_model() + bind_outcome( + o: bound_tokens_source_text( + tokens: tokens, + lex: model.lex, + binding_spellings: model.binding_spellings + ), + f: fn(t) { Accepted { value: render_target_text(t: t), diagnostics: None } } + ) +} + +fn dbl_parse(text: String) -> Outcome { + match dag_prepared_grammar() { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: prepared, diagnostics: residue } => + bind_outcome( + o: tokenize(text: text, file: ^dbl_probe, rules: dag_lex()), + f: fn(token_stream) { + match parse_module_prepared(tokens: token_stream, prepared: prepared, validation_residue: residue) { + Rejected { diagnostics: r } => Rejected { diagnostics: r } + Accepted { value: artifact, diagnostics: d } => Accepted { value: artifact.tree, diagnostics: d } + } + } + ) + } +} + +fn dbl_is_let(node: Node) -> Bool { + match parse_production_emitted_identity_optional(node: node) { + Present { value: id } => id == ^dag_surface_let_expr + Absent => false + } +} + +fn dbl_count_lets(root: Node) -> Int { + let here = if dbl_is_let(node: root) { 1 } else { 0 } + fold(root.children, init: here, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) +} + +// A let with another let somewhere under it. +fn dbl_has_nested_let(root: Node) -> Bool { + if dbl_is_let(node: root) && fold(root.children, init: 0, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) == 1 { + true + } else { + fold(root.children, init: false, f: fn(found, e) { found || dbl_has_nested_let(root: e.target) }) + } +} + +fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { + match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { + Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) + Rejected { diagnostics: _ } => false + } +} + +// One Bind with the given body, at expression position: it parses, and it holds exactly `lets` let +// nodes (the binding, plus any the body itself holds) -- the body is read as the body, never +// absorbed into the value or into a literal. +fn dbl_body_round_trips(body: List, lets: Int) -> Bool { + match dbl_text(tokens: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { + Rejected { diagnostics: _ } => false + Accepted { value: text, diagnostics: _ } => + match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { + Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == lets + Rejected { diagnostics: _ } => false + } + } +} + +test fn a_bare_identifier_body_round_trips() -> Bool { + dbl_body_round_trips(body: dbl_token(binding: ^dag_binding_bind_x), lets: 1) +} + +test fn an_empty_brace_literal_body_round_trips() -> Bool { + dbl_body_round_trips(body: [FixedToken { token_class: ^dag_token_lbrace }, FixedToken { token_class: ^dag_token_rbrace }], lets: 1) +} + +test fn a_body_starting_with_minus_round_trips() -> Bool { + dbl_body_round_trips(body: list_append(left: [FixedToken { token_class: ^dag_token_minus }], right: dbl_token(binding: ^dag_binding_bind_x)), lets: 1) +} + +test fn a_bind_body_round_trips_nested() -> Bool { + dbl_body_round_trips(body: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)), lets: 2) +} + +test fn nested_bind_emitted_block_scoped_reparses_to_the_same_binds() -> Bool { + match dbl_nested_text() { + Rejected { diagnostics: _ } => false + Accepted { value: text, diagnostics: _ } => + !string_contains(s: text, pattern: " in ") && dbl_reparses_to_two_nested_lets(text: text) + } +} From c4cd047d1e21187a8e9b1a7a2ea11ce6839b63ee Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 11:43:10 +0000 Subject: [PATCH 2/9] dag_bind_let_block_scoped: one expression parse per claim, no target model per claim Floor refused the five round-trip claims on cost (74-112k against 72.3k). Each now renders with the dag lex rules and the two spellings its tokens bind instead of building dag_bind_target_model, and parses the emitted text as the dag grammar's expr production over the shared prepared grammar instead of a module around it. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../emit/dag_bind_let_block_scoped_test.dag | 72 ++++++++++++------- 1 file changed, 46 insertions(+), 26 deletions(-) diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag index 2e5845aa421..065b3fd2e05 100644 --- a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -1,10 +1,9 @@ module v2.test.emit.dag_bind_let_block_scoped -import v2.compiler.parse { parse_module_prepared } +import v2.compiler.parse { PreparedModeled, PreparedVoidGrammar, parse_production_prepared } import v2.compiler.program_assembly { dag_prepared_grammar } import v2.compiler.tokenize { tokenize } import v2.extdeps.languages.dag { - dag_bind_target_model, dag_lex, dag_value_expression_projection, parse_production_emitted_identity_optional @@ -17,12 +16,13 @@ import v2.std.compilers.target_model { bound_tokens_source_text, render_target_text } +import v2.std.collection { Map, empty_map, map_insert } import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.algebra { list_append } import v2.std.logic { Bool } import v2.std.node { Node, Symbol } -import v2.std.optional { Absent, Present } +import v2.std.optional { Absent, Optional, Present } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -31,9 +31,11 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of // another -- the hardest position, inside the group -- emits it with the real emitter // (bind_let_value_producing_tokens over dag_value_expression_projection), renders it with the dag -// target's own spellings, places it where a value is owed (a data initializer) and reparses it with -// the dag grammar. It must parse, hold exactly two let_expr nodes with one inside the other, and -// carry no `in`: the text the emitter writes is text the grammar reads, one way. +// lex rules, and reparses it with the dag grammar as an expression -- the `expr` production, where a +// value is owed. It must parse, hold exactly two let_expr nodes with one inside the other, and carry +// no `in`: the text the emitter writes is text the grammar reads, one way. The body cases below do +// the same for a bare name, an empty brace literal, a `-`-led expression and a nested Bind. Each +// claim pays one parse of its own tokens (DESIGN section 3's witness rule). fn dbl_token(binding: Symbol) -> List { [BoundToken { token_class: ^dag_token_ident, binding: binding }] } @@ -55,34 +57,52 @@ fn dbl_nested_text() -> Outcome { dbl_text(tokens: dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)))) } +// Rendered with the dag lex rules and the two spellings the tokens bind -- the target model would +// supply the same, at the cost of building the whole model inside every claim. +fn dbl_spellings() -> Map { + map_insert(m: map_insert(m: empty_map(), key: ^dag_binding_bind_x, value: "x"), key: ^dag_binding_pick_lit_one, value: "a") +} + fn dbl_text(tokens: List) -> Outcome { - let model = dag_bind_target_model() bind_outcome( o: bound_tokens_source_text( tokens: tokens, - lex: model.lex, - binding_spellings: model.binding_spellings + lex: dag_lex(), + binding_spellings: dbl_spellings() ), f: fn(t) { Accepted { value: render_target_text(t: t), diagnostics: None } } ) } -fn dbl_parse(text: String) -> Outcome { +// The emitted Bind is parsed as the expression it is (the dag grammar's `expr` production, over the +// shared prepared grammar), so a claim pays for its own tokens and no module around them. +fn dbl_parse(text: String) -> Optional { match dag_prepared_grammar() { - Rejected { diagnostics: d } => Rejected { diagnostics: d } - Accepted { value: prepared, diagnostics: residue } => - bind_outcome( - o: tokenize(text: text, file: ^dbl_probe, rules: dag_lex()), - f: fn(token_stream) { - match parse_module_prepared(tokens: token_stream, prepared: prepared, validation_residue: residue) { - Rejected { diagnostics: r } => Rejected { diagnostics: r } - Accepted { value: artifact, diagnostics: d } => Accepted { value: artifact.tree, diagnostics: d } + Rejected { diagnostics: _ } => Absent + Accepted { value: prepared, diagnostics: _ } => + match prepared { + PreparedVoidGrammar => Absent + PreparedModeled { modeled: modeled, materialization: m } => + match tokenize(text: text, file: ^dbl_probe, rules: dag_lex()) { + Rejected { diagnostics: _ } => Absent + Accepted { value: token_stream, diagnostics: _ } => + match parse_production_prepared( + tokens: token_stream.all, + validated: modeled.validated, + analysis: modeled.analysis, + production_name: ^dag_production_expr, + materialization: m + ) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => dbl_tree(node: artifact.tree) + } } - } - ) + } } } +fn dbl_tree(node: Node) -> Optional { Present { value: node } } + fn dbl_is_let(node: Node) -> Bool { match parse_production_emitted_identity_optional(node: node) { Present { value: id } => id == ^dag_surface_let_expr @@ -105,9 +125,9 @@ fn dbl_has_nested_let(root: Node) -> Bool { } fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { - match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { - Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) - Rejected { diagnostics: _ } => false + match dbl_parse(text: text) { + Present { value: tree } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) + Absent => false } } @@ -118,9 +138,9 @@ fn dbl_body_round_trips(body: List, lets: Int) -> Bool { match dbl_text(tokens: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { Rejected { diagnostics: _ } => false Accepted { value: text, diagnostics: _ } => - match dbl_parse(text: concat(concat("module p\ndata d: I = ", text), "\n")) { - Accepted { value: tree, diagnostics: _ } => dbl_count_lets(root: tree) == lets - Rejected { diagnostics: _ } => false + match dbl_parse(text: text) { + Present { value: tree } => dbl_count_lets(root: tree) == lets + Absent => false } } } From 0d1697681287425ab43eae7cda568b27dd3d13ba Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 13:02:23 +0000 Subject: [PATCH 3/9] dag_bind_let_block_scoped: parse the emitted tokens; pin the token sequence, not text Floor: the round trips were still 72-105k against 72.3k. The emitter's product is a token sequence, so each claim now hands those tokens to the expr production directly (no render, no lexer). The previous text route also passed for the wrong reason: dag text rendering puts no separation between tokens ({letx=(a){x}}), and 'letx = (a)' re-read as a bare assignment let. a_single_bind_emits_block_scoped_tokens pins the exact token sequence instead; the rendering defect predates this change and is reported separately. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../emit/dag_bind_let_block_scoped_test.dag | 136 ++++++++++-------- 1 file changed, 73 insertions(+), 63 deletions(-) diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag index 065b3fd2e05..2a5bda8eb33 100644 --- a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -2,9 +2,7 @@ module v2.test.emit.dag_bind_let_block_scoped import v2.compiler.parse { PreparedModeled, PreparedVoidGrammar, parse_production_prepared } import v2.compiler.program_assembly { dag_prepared_grammar } -import v2.compiler.tokenize { tokenize } import v2.extdeps.languages.dag { - dag_lex, dag_value_expression_projection, parse_production_emitted_identity_optional } @@ -12,14 +10,14 @@ import v2.std.compilers.target_model { BoundToken, FixedToken, ConcreteSyntaxToken, - bind_let_value_producing_tokens, - bound_tokens_source_text, - render_target_text + bind_let_value_producing_tokens } -import v2.std.collection { Map, empty_map, map_insert } -import v2.std.diagnostic { Accepted, None, Outcome, Rejected, bind_outcome } +import v2.std.diagnostic { Accepted, Rejected } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.algebra { list_append } +import v2.std.compilers.lexing { Token } +import v2.std.algebra { any, fold_list, length } +import std.algebra { list_snoc_item } import v2.std.logic { Bool } import v2.std.node { Node, Symbol } import v2.std.optional { Absent, Optional, Present } @@ -30,12 +28,12 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // dag declares no separator (v2.std.compilers.target_model TargetBindLetShape, in_token Absent), so a // Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of // another -- the hardest position, inside the group -- emits it with the real emitter -// (bind_let_value_producing_tokens over dag_value_expression_projection), renders it with the dag -// lex rules, and reparses it with the dag grammar as an expression -- the `expr` production, where a -// value is owed. It must parse, hold exactly two let_expr nodes with one inside the other, and carry -// no `in`: the text the emitter writes is text the grammar reads, one way. The body cases below do -// the same for a bare name, an empty brace literal, a `-`-led expression and a nested Bind. Each -// claim pays one parse of its own tokens (DESIGN section 3's witness rule). +// (bind_let_value_producing_tokens over dag_value_expression_projection), and parses the emitted tokens +// with the dag grammar as an expression (the `expr` production, where a value is owed). It must parse, +// hold exactly two let_expr nodes with one inside the other, and carry no `in` token: what the emitter +// writes is what the grammar reads, one way. The body cases below do the same for a bare name, an +// empty brace literal, a `-`-led expression and a nested Bind. Each claim pays one parse of its own +// tokens (DESIGN section 3's witness rule). fn dbl_token(binding: Symbol) -> List { [BoundToken { token_class: ^dag_token_ident, binding: binding }] } @@ -53,54 +51,61 @@ fn dbl_bind_body(value: List, body: List Outcome { - dbl_text(tokens: dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)))) -} - -// Rendered with the dag lex rules and the two spellings the tokens bind -- the target model would -// supply the same, at the cost of building the whole model inside every claim. -fn dbl_spellings() -> Map { - map_insert(m: map_insert(m: empty_map(), key: ^dag_binding_bind_x, value: "x"), key: ^dag_binding_pick_lit_one, value: "a") -} - -fn dbl_text(tokens: List) -> Outcome { - bind_outcome( - o: bound_tokens_source_text( - tokens: tokens, - lex: dag_lex(), - binding_spellings: dbl_spellings() - ), - f: fn(t) { Accepted { value: render_target_text(t: t), diagnostics: None } } - ) -} - -// The emitted Bind is parsed as the expression it is (the dag grammar's `expr` production, over the -// shared prepared grammar), so a claim pays for its own tokens and no module around them. -fn dbl_parse(text: String) -> Optional { +// The emitted TOKENS are parsed as the expression they form (the dag grammar's `expr` production, over +// the shared prepared grammar): the emitter's product is a token sequence, and rendering it to text +// is a separate step (see a_single_bind_emits_block_scoped_tokens). So a claim pays for its own +// tokens and no render, lexer or module around them. +fn dbl_parse(concrete: List) -> Optional { match dag_prepared_grammar() { Rejected { diagnostics: _ } => Absent Accepted { value: prepared, diagnostics: _ } => match prepared { PreparedVoidGrammar => Absent PreparedModeled { modeled: modeled, materialization: m } => - match tokenize(text: text, file: ^dbl_probe, rules: dag_lex()) { + match parse_production_prepared( + tokens: dbl_lexed(concrete: concrete), + validated: modeled.validated, + analysis: modeled.analysis, + production_name: ^dag_production_expr, + materialization: m + ) { Rejected { diagnostics: _ } => Absent - Accepted { value: token_stream, diagnostics: _ } => - match parse_production_prepared( - tokens: token_stream.all, - validated: modeled.validated, - analysis: modeled.analysis, - production_name: ^dag_production_expr, - materialization: m - ) { - Rejected { diagnostics: _ } => Absent - Accepted { value: artifact, diagnostics: _ } => dbl_tree(node: artifact.tree) - } + Accepted { value: artifact, diagnostics: _ } => dbl_tree(node: artifact.tree) } } } } +// The lexer's token for each emitted token: its class, and for a bound token its spelling. +fn dbl_lexed(concrete: List) -> List { + fold_list(xs: concrete, empty: [], cons: fn(acc, c) { + list_snoc_item(xs: acc, item: dbl_lexed_one(token: c, at: length(xs: acc))) + }) +} + +fn dbl_lexed_one(token: ConcreteSyntaxToken, at: Int) -> Token { + match token { + FixedToken { token_class: c } => Token { class: c, lexeme: "", file: ^dbl_probe, start: at, end: at + 1 } + BoundToken { token_class: c, binding: b } => + Token { class: c, lexeme: dbl_spelling(binding: b), file: ^dbl_probe, start: at, end: at + 1 } + } +} + +fn dbl_spelling(binding: Symbol) -> String { + if binding == ^dag_binding_bind_x { "x" } else { "a" } +} + +fn dbl_has_in(concrete: List) -> Bool { + any(xs: concrete, predicate: fn(c) { dbl_class(token: c) == ^dag_token_kw_in }) +} + +fn dbl_class(token: ConcreteSyntaxToken) -> Symbol { + match token { + FixedToken { token_class: c } => c + BoundToken { token_class: c, binding: _ } => c + } +} + fn dbl_tree(node: Node) -> Optional { Present { value: node } } fn dbl_is_let(node: Node) -> Bool { @@ -124,8 +129,8 @@ fn dbl_has_nested_let(root: Node) -> Bool { } } -fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { - match dbl_parse(text: text) { +fn dbl_reparses_to_two_nested_lets(concrete: List) -> Bool { + match dbl_parse(concrete: concrete) { Present { value: tree } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) Absent => false } @@ -135,13 +140,9 @@ fn dbl_reparses_to_two_nested_lets(text: String) -> Bool { // nodes (the binding, plus any the body itself holds) -- the body is read as the body, never // absorbed into the value or into a literal. fn dbl_body_round_trips(body: List, lets: Int) -> Bool { - match dbl_text(tokens: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { - Rejected { diagnostics: _ } => false - Accepted { value: text, diagnostics: _ } => - match dbl_parse(text: text) { - Present { value: tree } => dbl_count_lets(root: tree) == lets - Absent => false - } + match dbl_parse(concrete: dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: body)) { + Present { value: tree } => dbl_count_lets(root: tree) == lets + Absent => false } } @@ -162,9 +163,18 @@ test fn a_bind_body_round_trips_nested() -> Bool { } test fn nested_bind_emitted_block_scoped_reparses_to_the_same_binds() -> Bool { - match dbl_nested_text() { - Rejected { diagnostics: _ } => false - Accepted { value: text, diagnostics: _ } => - !string_contains(s: text, pattern: " in ") && dbl_reparses_to_two_nested_lets(text: text) - } + let concrete = dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one))) + !dbl_has_in(concrete: concrete) && dbl_reparses_to_two_nested_lets(concrete: concrete) +} + +// The token sequence the dag target writes for one Bind, exactly: `{ let k = ( v ) { b } }`. The claims +// above parse emitted TOKENS; this pins what those tokens are. Text is not the grain here: the dag +// target's rendering puts no separation between tokens (its lex is dag_lex, with no emit +// transforms), so a keyword and the name after it render fused -- a defect of dag text rendering that +// predates this change and is reported on its own, not something a text round trip could check. +test fn a_single_bind_emits_block_scoped_tokens() -> Bool { + map(dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)), fn(c) { dbl_class(token: c) }) == [ + ^dag_token_lbrace, ^dag_token_kw_let, ^dag_token_ident, ^dag_token_eq, ^dag_token_lparen, ^dag_token_ident, + ^dag_token_rparen, ^dag_token_lbrace, ^dag_token_ident, ^dag_token_rbrace, ^dag_token_rbrace + ] } From e2379718a1ebbf9e641e2cee0cc93d0eaee5db22 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 13:14:45 +0000 Subject: [PATCH 4/9] dag target: declare token separation as emit-transform rows; the flat token fold reads them Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/target_serialize.dag | 7 +++-- src/v2/extdeps/languages/dag.dag | 31 +++++++++++++++---- src/v2/std/compilers/target_model.dag | 43 ++++++++++++++++++++++----- 3 files changed, 66 insertions(+), 15 deletions(-) diff --git a/src/v2/compiler/target_serialize.dag b/src/v2/compiler/target_serialize.dag index 6a9f35a85e6..9251ea85280 100644 --- a/src/v2/compiler/target_serialize.dag +++ b/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 ) -> Outcome { - 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 ) } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index 62b36ecc17c..6584f219b32 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/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, @@ -676,6 +678,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 { + 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 { @@ -3896,7 +3917,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 } @@ -6000,7 +6021,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 } @@ -6010,7 +6031,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 } @@ -6341,7 +6362,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 } diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index da130f7bfa3..45117215666 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/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, lex: LexRules, - binding_spellings: Map + binding_spellings: Map, + transforms: Map ) -> Outcome { 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, + lex: LexRules, + binding_spellings: Map +) -> Outcome { + 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 { - match map_get(target.token_class_emit_transforms, token_class) { +fn layout_or_atom_in(transforms: Map, token_class: Symbol, spelling: String) -> Outcome { + 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 { + 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 From 97b54da780eeae705fe97678c22e5b3f3d9512ca Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 13:43:36 +0000 Subject: [PATCH 5/9] dag target text round trip: claims at the token join, kept red, inhabitance on the real route; failure-mode row Co-Authored-By: Claude Opus 5.5 (1M context) --- ...itted_text_reread_as_another_construct.dag | 25 ++ .../languages/rust_emit_small_fixtures.dag | 4 +- .../emit/dag_target_text_round_trip_test.dag | 223 ++++++++++++++++++ 3 files changed, 250 insertions(+), 2 deletions(-) create mode 100644 dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag create mode 100644 src/v2/test/claim/emit/dag_target_text_round_trip_test.dag diff --git a/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag b/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag new file mode 100644 index 00000000000..b07456f9572 --- /dev/null +++ b/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: "nested_bind_text_reads_back_as_the_same_tokens_and_two_nested_lets", 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 }, + ], +} diff --git a/src/v2/extdeps/languages/rust_emit_small_fixtures.dag b/src/v2/extdeps/languages/rust_emit_small_fixtures.dag index f0c008a08d2..9321075f3ce 100644 --- a/src/v2/extdeps/languages/rust_emit_small_fixtures.dag +++ b/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, diff --git a/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag new file mode 100644 index 00000000000..ac17168aeb4 --- /dev/null +++ b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag @@ -0,0 +1,223 @@ +module v2.test.emit.dag_target_text_round_trip + +import v2.compiler.parse { PreparedModeled, PreparedVoidGrammar, parse_production_prepared } +import v2.compiler.program_assembly { dag_prepared_grammar } +import v2.compiler.target_serialize { serialize_concrete_syntax_tokens_to_source_string } +import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { + dag_lex, + dag_target_model, + dag_token_class_emit_transforms, + dag_value_expression_projection, + parse_production_emitted_identity_optional +} +import v2.std.compilers.lexing { Token } +import v2.std.compilers.target_model { + BoundToken, + FixedToken, + ConcreteSyntaxToken, + TokenClassEmitTransform, + bind_let_value_producing_tokens, + bound_tokens_source_text_with_transforms, + render_target_text, + target_model_emit_transforms_empty +} +import v2.std.algebra { list_map } +import v2.std.collection { Map, empty_map, map_insert } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.std.optional { Absent, Optional, Present } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE TEXT THE dag TARGET WRITES IS TEXT THE dag GRAMMAR READS BACK AS THE SAME TREE. The dag target +// declared no separation between tokens, so a Bind rendered as "{letx=(a){x}}" and a conditional as +// "iftruethen1elsex": the first reads back with no binding in it and the second as one identifier, +// both ACCEPTED. Each claim here renders an emitted token sequence to text, lexes that text with the +// dag lex rules and (where a tree is owed) parses it once at the `expr` production. The inputs are +// supplied at the rendering interface (the lex rules, the spellings, the transform rows); the last +// claim is the inhabitance one, on the real route with the dag target model. +fn trt_ident(binding: Symbol) -> List { + [BoundToken { token_class: ^dag_token_ident, binding: binding }] +} + +fn trt_spellings() -> Map { + map_insert( + m: map_insert(m: map_insert(m: empty_map(), key: ^dag_binding_bind_x, value: "x"), key: ^dag_binding_pick_lit_one, value: "a"), + key: ^trt_binding_one, + value: "1" + ) +} + +fn trt_bind(value: List) -> List { + bind_let_value_producing_tokens( + projection: dag_value_expression_projection(), + key_tokens: trt_ident(binding: ^dag_binding_bind_x), + value_tokens: value, + body_tokens: trt_ident(binding: ^dag_binding_bind_x) + ) +} + +// A Bind as the VALUE of a Bind, from the real emitter. +fn trt_nested_bind() -> List { + trt_bind(value: trt_bind(value: trt_ident(binding: ^dag_binding_pick_lit_one))) +} + +// `if true then 1 else x`: keywords, a literal and an identifier, every one adjacent to another word. +fn trt_mixed() -> List { + [ + FixedToken { token_class: ^dag_token_kw_if }, + FixedToken { token_class: ^dag_token_kw_true }, + FixedToken { token_class: ^dag_token_kw_then }, + BoundToken { token_class: ^dag_token_int_literal, binding: ^trt_binding_one }, + FixedToken { token_class: ^dag_token_kw_else }, + BoundToken { token_class: ^dag_token_ident, binding: ^dag_binding_bind_x } + ] +} + +fn trt_text(tokens: List, transforms: Map) -> String { + match bound_tokens_source_text_with_transforms( + tokens: tokens, + lex: dag_lex(), + binding_spellings: trt_spellings(), + transforms: transforms + ) { + Accepted { value: t, diagnostics: _ } => render_target_text(t: t) + Rejected { diagnostics: _ } => "" + } +} + +fn trt_lex(text: String) -> List { + match tokenize(text: text, file: ^trt_probe, rules: dag_lex()) { + Accepted { value: stream, diagnostics: _ } => stream.all + Rejected { diagnostics: _ } => [] + } +} + +fn trt_emitted_classes(tokens: List) -> List { + list_map(xs: tokens, f: fn(t) { + match t { + FixedToken { token_class: c } => c + BoundToken { token_class: c, binding: _ } => c + } + }) +} + +// The token classes the text lexes to, in order: the emitted sequence, or it was not round-tripped. +fn trt_read_classes(text: String) -> List { + trt_token_classes(tokens: trt_lex(text: text)) +} + +fn trt_token_classes(tokens: List) -> List { + list_map(xs: tokens, f: fn(t) { t.class }) +} + +fn trt_parse(tokens: List) -> Optional { + match dag_prepared_grammar() { + Rejected { diagnostics: _ } => Absent + Accepted { value: prepared, diagnostics: _ } => + match prepared { + PreparedVoidGrammar => Absent + PreparedModeled { modeled: modeled, materialization: m } => + match parse_production_prepared( + tokens: tokens, + validated: modeled.validated, + analysis: modeled.analysis, + production_name: ^dag_production_expr, + materialization: m + ) { + Rejected { diagnostics: _ } => Absent + Accepted { value: artifact, diagnostics: _ } => trt_present(node: artifact.tree) + } + } + } +} + +fn trt_present(node: Node) -> Optional { Present { value: node } } + +fn trt_is(node: Node, production: Symbol) -> Bool { + match parse_production_emitted_identity_optional(node: node) { + Present { value: id } => id == production + Absent => false + } +} + +fn trt_count(root: Node, production: Symbol) -> Int { + let here = if trt_is(node: root, production: production) { 1 } else { 0 } + fold(root.children, init: here, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) +} + +fn trt_count_below(root: Node, production: Symbol) -> Int { + fold(root.children, init: 0, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) +} + +// A let with exactly one let under it. +fn trt_has_nested_let(root: Node) -> Bool { + if trt_is(node: root, production: ^dag_surface_let_expr) && trt_count_below(root: root, production: ^dag_surface_let_expr) == 1 { + true + } else { + fold(root.children, init: false, f: fn(found, e) { found || trt_has_nested_let(root: e.target) }) + } +} + +// The text reads back as the emitted token sequence AND as two binds, one inside the other. The +// token join is the discriminating half: see the claim below. +test fn nested_bind_text_reads_back_as_the_same_tokens_and_two_nested_lets() -> Bool { + let read = trt_lex(text: trt_text(tokens: trt_nested_bind(), transforms: dag_token_class_emit_transforms())) + trt_token_classes(tokens: read) == trt_emitted_classes(tokens: trt_nested_bind()) + && match trt_parse(tokens: read) { + Present { value: tree } => + trt_count(root: tree, production: ^dag_surface_let_expr) == 2 && trt_has_nested_let(root: tree) + Absent => false + } +} + +// THE RED, KEPT: the same tokens with no transform rows are the rendering the dag target had, and +// they do not read back as the tokens emitted (`let` `x` is the one identifier `letx`). That text +// still PARSES, and to two nested lets (`letx = (..)` reads as a bare-assignment binding), so a +// claim that counted lets passed on it; the token join is what refuses it. +test fn nested_bind_text_without_separation_reads_back_as_other_tokens() -> Bool { + trt_read_classes(text: trt_text(tokens: trt_nested_bind(), transforms: target_model_emit_transforms_empty)) + != trt_emitted_classes(tokens: trt_nested_bind()) +} + +test fn mixed_expression_text_reads_back_as_the_same_tokens_and_one_conditional() -> Bool { + let read = trt_lex(text: trt_text(tokens: trt_mixed(), transforms: dag_token_class_emit_transforms())) + trt_token_classes(tokens: read) == trt_emitted_classes(tokens: trt_mixed()) + && match trt_parse(tokens: read) { + Present { value: tree } => trt_count(root: tree, production: ^dag_surface_if_expr) == 1 + Absent => false + } +} + +// THE CLASS, at its cheapest specimen: unseparated, the six tokens are ONE identifier, which is a +// valid expression. A claim that only asked "does the emitted text parse" passes on it. +test fn mixed_expression_text_without_separation_is_one_identifier() -> Bool { + trt_read_classes(text: trt_text(tokens: trt_mixed(), transforms: target_model_emit_transforms_empty)) == [^dag_token_ident] +} + +// Punctuation is not exempt: `>` then `=` unseparated is the one token `>=`. +test fn adjacent_punctuation_reads_back_as_two_tokens() -> Bool { + let pair = [FixedToken { token_class: ^dag_token_gt }, FixedToken { token_class: ^dag_token_eq }] + trt_read_classes(text: trt_text(tokens: pair, transforms: dag_token_class_emit_transforms())) == [^dag_token_gt, ^dag_token_eq] + && trt_read_classes(text: trt_text(tokens: pair, transforms: target_model_emit_transforms_empty)) == [^dag_token_gte] +} + +// INHABITANCE, ON THE REAL ROUTE: the dag target model carries the rows, and the serializer the +// emitter calls (v2.compiler.target_serialize) reads them. Dropping the rows from dag_target_model, +// or the map from that serializer, runs the tokens together and fails this. The value is the name +// `x`: the model spells its other bindings as digits, which lex as literals, not as the identifier +// class these tokens carry. +fn trt_model_bind() -> List { + trt_bind(value: trt_ident(binding: ^dag_binding_bind_x)) +} + +test fn the_dag_target_model_serializes_a_bind_with_its_tokens_separated() -> Bool { + match serialize_concrete_syntax_tokens_to_source_string(target: dag_target_model(), tokens: trt_model_bind()) { + Accepted { value: t, diagnostics: _ } => + trt_read_classes(text: render_target_text(t: t)) == trt_emitted_classes(tokens: trt_model_bind()) + Rejected { diagnostics: _ } => false + } +} From b8ace9bc8c3b18718d3ab1660d0196b95a948e49 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 13:56:13 +0000 Subject: [PATCH 6/9] target_text_layout: the flat token route applies the target's transform rows (verilog) Co-Authored-By: Claude Opus 5.5 (1M context) --- .../claim/emit/target_text_layout_test.dag | 26 ++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/src/v2/test/claim/emit/target_text_layout_test.dag b/src/v2/test/claim/emit/target_text_layout_test.dag index 8afa801430b..b848362803a 100644 --- a/src/v2/test/claim/emit/target_text_layout_test.dag +++ b/src/v2/test/claim/emit/target_text_layout_test.dag @@ -7,6 +7,7 @@ import v2.std.grammar { Holds, Violates } import v2.std.compilers.target_model { TargetModel, TargetText, + FixedToken, target_text_line_breaks, text_atom, target_text_seq, @@ -16,7 +17,7 @@ import v2.std.compilers.target_model { render_target_text, fixed_token_spelling_from_model } -import v2.compiler.target_serialize { target_serialize_relation_row_from_model_bounded } +import v2.compiler.target_serialize { serialize_concrete_syntax_tokens_to_source_string, target_serialize_relation_row_from_model_bounded } import v2.extdeps.languages.verilog { verilog_interlock_emitted, verilog_relation_row_for, @@ -73,6 +74,29 @@ test fn a_layout_token_class_refuses_the_flat_spelling() -> Bool { } } +// THE FLAT TOKEN ROUTE SPELLS A TOKEN CLASS AS THE RELATION-ROW ROUTE DOES. The flat fold +// (v2.compiler.target_serialize serialize_concrete_syntax_tokens_to_source_string) read no +// transform rows, so the same class rendered two ways depending on which fold spelled it. Here the +// consuming target's own rows apply: `assign` keeps its trailing space, `=` its two, and `;` its +// line break instead of refusing or dropping it. +test fn the_flat_token_route_applies_the_targets_transform_rows() -> Bool { + match verilog_relation_row_for(lhs: ^verilog_production_ansi_module_decl, emitted: verilog_interlock_emitted()) { + Holds { value: row } => + match serialize_concrete_syntax_tokens_to_source_string( + target: verilog_target_model_with_single_row(row: row), + tokens: [ + FixedToken { token_class: ^verilog_token_kw_assign }, + FixedToken { token_class: ^verilog_token_equals }, + FixedToken { token_class: ^verilog_token_semicolon } + ] + ) { + Accepted { value: t, diagnostics: _ } => render_target_text(t: t) == "assign = ;\n" + Rejected { diagnostics: _ } => false + } + Violates { diagnostic: _ } => false + } +} + // A nested occurrence whose unit the target does not spell refuses rather than indenting by the // symbol's own name; the same module with the unit spelled emits. test fn an_unspelled_nest_unit_refuses_and_a_spelled_one_emits() -> Bool { From d5996ae720d2c5fd827a20915d51ded724a031f3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 3 Oct 2026 14:23:12 +0000 Subject: [PATCH 7/9] dag_bind_let_block_scoped: nested Binds by composition; parses shared once (warm producer) The nested-value and nested-body claims parsed ~21 tokens each (87-105k steps). They are replaced by two composition claims (the emitter places a Bind's tokens verbatim in the value group and the body block) and two slot parses (a Bind inside a value group, a Bind as a body statement), which with the lone-Bind parse cover nesting in a context-free grammar. The five parses run once in dbl_verdicts, enrolled warm in floor_pure_producer_share; claims read stored Bools. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../emit/dag_bind_let_block_scoped_test.dag | 112 ++++++++++++++---- src/v2/workflow/floor_pure_producer_share.dag | 5 + 2 files changed, 92 insertions(+), 25 deletions(-) diff --git a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag index 2a5bda8eb33..2697657d68e 100644 --- a/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag +++ b/src/v2/test/claim/emit/dag_bind_let_block_scoped_test.dag @@ -26,14 +26,12 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // A CORE BIND EMITTED THROUGH THE dag TARGET PARSES BACK AS THE SAME BINDS, AT EXPRESSION POSITION. // dag declares no separator (v2.std.compilers.target_model TargetBindLetShape, in_token Absent), so a -// Bind is emitted block-scoped: `{ let k = (v) { b } }`. The control nests one Bind as the VALUE of -// another -- the hardest position, inside the group -- emits it with the real emitter -// (bind_let_value_producing_tokens over dag_value_expression_projection), and parses the emitted tokens -// with the dag grammar as an expression (the `expr` production, where a value is owed). It must parse, -// hold exactly two let_expr nodes with one inside the other, and carry no `in` token: what the emitter -// writes is what the grammar reads, one way. The body cases below do the same for a bare name, an -// empty brace literal, a `-`-led expression and a nested Bind. Each claim pays one parse of its own -// tokens (DESIGN section 3's witness rule). +// Bind is emitted block-scoped: `{ let k = (v) { b } }`. The controls emit Binds with the real emitter +// (bind_let_value_producing_tokens over dag_value_expression_projection) and parse the emitted TOKENS +// with the dag grammar as an expression (the `expr` production, where a value is owed), carrying no +// `in` token. Bodies that are a bare name, an empty brace literal and a `-`-led expression each read +// back as one Bind; a nested Bind is covered by composition (see dbl_inner). The parses run once, in +// dbl_verdicts (DESIGN section 3's witness rule). fn dbl_token(binding: Symbol) -> List { [BoundToken { token_class: ^dag_token_ident, binding: binding }] } @@ -120,18 +118,29 @@ fn dbl_count_lets(root: Node) -> Int { fold(root.children, init: here, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) } -// A let with another let somewhere under it. -fn dbl_has_nested_let(root: Node) -> Bool { - if dbl_is_let(node: root) && fold(root.children, init: 0, f: fn(acc, e) { acc + dbl_count_lets(root: e.target) }) == 1 { - true - } else { - fold(root.children, init: false, f: fn(found, e) { found || dbl_has_nested_let(root: e.target) }) - } +// A NESTED BIND IS PROVED BY COMPOSITION, NOT BY ONE LONG PARSE. The emitter puts a Bind's tokens +// verbatim into the value group `( .. )` and into the body block `{ .. }` (the two composition claims); +// a lone Bind parses as one whole expression (a_bare_identifier_body_round_trips); and a Bind parses +// both inside a value group and as a body block's statement (the two slot claims). The grammar is +// context-free in those slots, so the nested emission reads as nested Binds. Parsing the whole +// nested text in one claim costs more than a claim may (DESIGN section 3's witness rule). +fn dbl_inner() -> List { + dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)) +} + +fn dbl_fixed(classes: List) -> List { + map(classes, fn(c) { dbl_fixed_one(token_class: c) }) +} + +fn dbl_fixed_one(token_class: Symbol) -> ConcreteSyntaxToken { FixedToken { token_class: token_class } } + +fn dbl_wrapped(open: List, inner: List, close: List) -> List { + list_append(left: list_append(left: open, right: inner), right: close) } -fn dbl_reparses_to_two_nested_lets(concrete: List) -> Bool { +fn dbl_parses_to_one_let(concrete: List) -> Bool { match dbl_parse(concrete: concrete) { - Present { value: tree } => dbl_count_lets(root: tree) == 2 && dbl_has_nested_let(root: tree) + Present { value: tree } => dbl_count_lets(root: tree) == 1 Absent => false } } @@ -146,25 +155,78 @@ fn dbl_body_round_trips(body: List, lets: Int) -> Bool { } } +// THE FIVE PARSE VERDICTS, ONE PARSE EACH. Nullary and pure, enrolled WARM in +// v2.workflow.floor_pure_producer_share: each emitted token sequence is parsed once at preparation and +// every claim reads its stored Bool, so no claim pays a parse. +type DblVerdicts { + bare_body: Bool + empty_literal_body: Bool + minus_body: Bool + in_value_group: Bool + as_body_statement: Bool +} + +fn dbl_verdicts() -> DblVerdicts { + DblVerdicts { + bare_body: dbl_body_round_trips(body: dbl_token(binding: ^dag_binding_bind_x), lets: 1), + empty_literal_body: dbl_body_round_trips(body: dbl_fixed(classes: [^dag_token_lbrace, ^dag_token_rbrace]), lets: 1), + minus_body: dbl_body_round_trips(body: list_append(left: dbl_fixed(classes: [^dag_token_minus]), right: dbl_token(binding: ^dag_binding_bind_x)), lets: 1), + in_value_group: dbl_parses_to_one_let(concrete: dbl_wrapped(open: dbl_fixed(classes: [^dag_token_lparen]), inner: dbl_inner(), close: dbl_fixed(classes: [^dag_token_rparen]))), + as_body_statement: dbl_parses_to_one_let(concrete: dbl_wrapped(open: dbl_fixed(classes: [^dag_token_lbrace]), inner: dbl_inner(), close: dbl_fixed(classes: [^dag_token_rbrace]))) + } +} + test fn a_bare_identifier_body_round_trips() -> Bool { - dbl_body_round_trips(body: dbl_token(binding: ^dag_binding_bind_x), lets: 1) + dbl_verdicts().bare_body } test fn an_empty_brace_literal_body_round_trips() -> Bool { - dbl_body_round_trips(body: [FixedToken { token_class: ^dag_token_lbrace }, FixedToken { token_class: ^dag_token_rbrace }], lets: 1) + dbl_verdicts().empty_literal_body } test fn a_body_starting_with_minus_round_trips() -> Bool { - dbl_body_round_trips(body: list_append(left: [FixedToken { token_class: ^dag_token_minus }], right: dbl_token(binding: ^dag_binding_bind_x)), lets: 1) + dbl_verdicts().minus_body +} + +test fn a_bind_as_the_value_is_placed_verbatim_in_the_value_group() -> Bool { + let nested = dbl_bind(value: dbl_inner()) + !dbl_has_in(concrete: nested) + && nested == dbl_wrapped( + open: list_append( + left: dbl_fixed(classes: [^dag_token_lbrace, ^dag_token_kw_let]), + right: list_append(left: dbl_token(binding: ^dag_binding_bind_x), right: dbl_fixed(classes: [^dag_token_eq, ^dag_token_lparen])) + ), + inner: dbl_inner(), + close: list_append( + left: dbl_fixed(classes: [^dag_token_rparen, ^dag_token_lbrace]), + right: list_append(left: dbl_token(binding: ^dag_binding_bind_x), right: dbl_fixed(classes: [^dag_token_rbrace, ^dag_token_rbrace])) + ) + ) +} + +test fn a_bind_as_the_body_is_placed_verbatim_in_the_body_block() -> Bool { + dbl_bind_body(value: dbl_token(binding: ^dag_binding_pick_lit_one), body: dbl_inner()) == dbl_wrapped( + open: list_append( + left: dbl_fixed(classes: [^dag_token_lbrace, ^dag_token_kw_let]), + right: list_append( + left: dbl_token(binding: ^dag_binding_bind_x), + right: list_append( + left: dbl_fixed(classes: [^dag_token_eq, ^dag_token_lparen]), + right: list_append(left: dbl_token(binding: ^dag_binding_pick_lit_one), right: dbl_fixed(classes: [^dag_token_rparen, ^dag_token_lbrace])) + ) + ) + ), + inner: dbl_inner(), + close: dbl_fixed(classes: [^dag_token_rbrace, ^dag_token_rbrace]) + ) } -test fn a_bind_body_round_trips_nested() -> Bool { - dbl_body_round_trips(body: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one)), lets: 2) +test fn a_bind_parses_inside_a_value_group() -> Bool { + dbl_verdicts().in_value_group } -test fn nested_bind_emitted_block_scoped_reparses_to_the_same_binds() -> Bool { - let concrete = dbl_bind(value: dbl_bind(value: dbl_token(binding: ^dag_binding_pick_lit_one))) - !dbl_has_in(concrete: concrete) && dbl_reparses_to_two_nested_lets(concrete: concrete) +test fn a_bind_parses_as_a_body_block_statement() -> Bool { + dbl_verdicts().as_body_statement } // The token sequence the dag target writes for one Bind, exactly: `{ let k = ( v ) { b } }`. The claims diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 58bae12f992..50cb77cd67d 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -634,6 +634,10 @@ import v2.std.collection { List } // THE XL-2 LET-IN CAST ROW: v2.test.claim.body_cast_node bcn_let_in_value_cast_verdict assembles one // inline module through the production route and stores one Bool (the lowered body carries exactly // one cast node with its target), portable because it holds no Node and no closure. +// THE dag BIND BLOCK-SCOPED ROW: v2.test.emit.dag_bind_let_block_scoped dbl_verdicts parses five emitted +// token sequences once each and stores five Bool verdicts; each claim that paid its own parse measured +// over the new-witness budget on the floor runs of #13099 (eval steps 72-105k). Portable because it +// holds only Bools. // THE XL-2 IF-ARM AND STATEMENT-SPINE ROW IS THE SAME GROUND AT THIRTEEN SPECIMENS: // v2.test.claim.namespace_xl0.if_arm_and_statement_lowering_refusal iasl_outcomes drives one front // end over thirteen inline modules and stores one verdict arm per module, portable for the same reason. @@ -885,6 +889,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.namespace_xl0.call_argument_value_resolve_refusal.cav_outcomes", "v2.test.claim.normalize.authored_marker_spelling.ams_verdicts", "v2.test.claim.body_lowering.caret_symbol_value_lowering.csv_verdicts", + "v2.test.emit.dag_bind_let_block_scoped.dbl_verdicts", "v2.test.parse.type_decl_modifier_g0_parse_probe.caret_tree_atom_identities", "v2.test.claim.body_lowering.string_literal_value_lowering.slv_verdicts", "v2.test.claim.body_cast_node.bcn_let_in_value_cast_verdict", From d568f118e30c5e77f133d9f0e880c307c685a937 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 14:41:16 +0000 Subject: [PATCH 8/9] dag_target_text_round_trip: the nested-Bind claim stops at the token join (its parse alone is over the new-witness budget) Co-Authored-By: Claude Opus 5.5 (1M context) --- ...itted_text_reread_as_another_construct.dag | 2 +- .../emit/dag_target_text_round_trip_test.dag | 31 +++++-------------- 2 files changed, 9 insertions(+), 24 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag b/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag index b07456f9572..db802fd7251 100644 --- a/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag +++ b/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag @@ -19,7 +19,7 @@ data round_trip_claim_passes_on_emitted_text_reread_as_another_construct: Recurr 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: "nested_bind_text_reads_back_as_the_same_tokens_and_two_nested_lets", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.test.emit.dag_target_text_round_trip", decl_name: "nested_bind_text_reads_back_as_the_same_tokens", 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 }, ], } diff --git a/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag index ac17168aeb4..a4c4502a1f1 100644 --- a/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag +++ b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag @@ -149,29 +149,14 @@ fn trt_count(root: Node, production: Symbol) -> Int { fold(root.children, init: here, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) } -fn trt_count_below(root: Node, production: Symbol) -> Int { - fold(root.children, init: 0, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) -} - -// A let with exactly one let under it. -fn trt_has_nested_let(root: Node) -> Bool { - if trt_is(node: root, production: ^dag_surface_let_expr) && trt_count_below(root: root, production: ^dag_surface_let_expr) == 1 { - true - } else { - fold(root.children, init: false, f: fn(found, e) { found || trt_has_nested_let(root: e.target) }) - } -} - -// The text reads back as the emitted token sequence AND as two binds, one inside the other. The -// token join is the discriminating half: see the claim below. -test fn nested_bind_text_reads_back_as_the_same_tokens_and_two_nested_lets() -> Bool { - let read = trt_lex(text: trt_text(tokens: trt_nested_bind(), transforms: dag_token_class_emit_transforms())) - trt_token_classes(tokens: read) == trt_emitted_classes(tokens: trt_nested_bind()) - && match trt_parse(tokens: read) { - Present { value: tree } => - trt_count(root: tree, production: ^dag_surface_let_expr) == 2 && trt_has_nested_let(root: tree) - Absent => false - } +// THE NESTED BIND'S TEXT READS BACK AS THE TOKEN SEQUENCE EMITTED, class for class. This claim stops +// at that boundary on purpose: parsing these tokens is a second subject, already claimed over the +// same emitter output by v2.test.emit.dag_bind_let_block_scoped, and that parse alone exceeds a new +// witness's eval-step budget (measured on the floor at this PR). The text -> lex -> parse path is +// run for real, once, by the mixed-expression claim below. +test fn nested_bind_text_reads_back_as_the_same_tokens() -> Bool { + trt_read_classes(text: trt_text(tokens: trt_nested_bind(), transforms: dag_token_class_emit_transforms())) + == trt_emitted_classes(tokens: trt_nested_bind()) } // THE RED, KEPT: the same tokens with no transform rows are the rendering the dag target had, and From d475a8a87cf47572a56bfdf229afb2ac1cfa3f9c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 3 Oct 2026 15:31:05 +0000 Subject: [PATCH 9/9] dag_target_text_round_trip: block-scoped Bind at text grain for four bodies and a Bind value; token join then one parse, shared once (warm producer) Co-Authored-By: Claude Opus 5.5 (1M context) --- ...itted_text_reread_as_another_construct.dag | 2 +- .../emit/dag_target_text_round_trip_test.dag | 120 +++++++++++++++--- src/v2/workflow/floor_pure_producer_share.dag | 5 + 3 files changed, 111 insertions(+), 16 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag b/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag index db802fd7251..f4302823e0d 100644 --- a/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag +++ b/dag/gunbc/recurring_failure_mode/round_trip_claim_passes_on_emitted_text_reread_as_another_construct.dag @@ -19,7 +19,7 @@ data round_trip_claim_passes_on_emitted_text_reread_as_another_construct: Recurr 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: "nested_bind_text_reads_back_as_the_same_tokens", 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 }, ], } diff --git a/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag index a4c4502a1f1..df3c6de4f7f 100644 --- a/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag +++ b/src/v2/test/claim/emit/dag_target_text_round_trip_test.dag @@ -22,6 +22,7 @@ import v2.std.compilers.target_model { render_target_text, target_model_emit_transforms_empty } +import std.algebra { list_append } import v2.std.algebra { list_map } import v2.std.collection { Map, empty_map, map_insert } import v2.std.diagnostic { Accepted, Rejected } @@ -149,14 +150,108 @@ fn trt_count(root: Node, production: Symbol) -> Int { fold(root.children, init: here, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) } -// THE NESTED BIND'S TEXT READS BACK AS THE TOKEN SEQUENCE EMITTED, class for class. This claim stops -// at that boundary on purpose: parsing these tokens is a second subject, already claimed over the -// same emitter output by v2.test.emit.dag_bind_let_block_scoped, and that parse alone exceeds a new -// witness's eval-step budget (measured on the floor at this PR). The text -> lex -> parse path is -// run for real, once, by the mixed-expression claim below. -test fn nested_bind_text_reads_back_as_the_same_tokens() -> Bool { - trt_read_classes(text: trt_text(tokens: trt_nested_bind(), transforms: dag_token_class_emit_transforms())) - == trt_emitted_classes(tokens: trt_nested_bind()) +fn trt_count_below(root: Node, production: Symbol) -> Int { + fold(root.children, init: 0, f: fn(acc, e) { acc + trt_count(root: e.target, production: production) }) +} + +// A let with exactly one let under it. +fn trt_has_nested_let(root: Node) -> Bool { + if trt_is(node: root, production: ^dag_surface_let_expr) && trt_count_below(root: root, production: ^dag_surface_let_expr) == 1 { + true + } else { + fold(root.children, init: false, f: fn(found, e) { found || trt_has_nested_let(root: e.target) }) + } +} + +fn trt_fixed(classes: List) -> List { + list_map(xs: classes, f: fn(c) { trt_fixed_one(token_class: c) }) +} + +fn trt_fixed_one(token_class: Symbol) -> ConcreteSyntaxToken { FixedToken { token_class: token_class } } + +// One Bind `{ let x = (a) { body } }` from the real emitter, with the given body. +fn trt_bind_with_body(body: List) -> List { + bind_let_value_producing_tokens( + projection: dag_value_expression_projection(), + key_tokens: trt_ident(binding: ^dag_binding_bind_x), + value_tokens: trt_ident(binding: ^dag_binding_pick_lit_one), + body_tokens: body + ) +} + +// THE TEXT-GRAIN ROUND TRIP OF ONE EMITTED TOKEN SEQUENCE: rendered with the dag target's rows, the +// text lexes back to the emitted token classes in order (the join: any merge or split of tokens +// fails here), and those lexed tokens parse at `expr` to ONE tree holding exactly `lets` bindings. +// `let_under_let` is the tree's shape: a Bind in the VALUE group sits under the outer let node, a +// Bind in the BODY block does not (the block follows the let as its own statement). The let count is +// asked only AFTER the join, never instead of it: the unseparated text has the same count. +fn trt_bind_text_round_trips(tokens: List, lets: Int, let_under_let: Bool) -> Bool { + let read = trt_lex(text: trt_text(tokens: tokens, transforms: dag_token_class_emit_transforms())) + trt_token_classes(tokens: read) == trt_emitted_classes(tokens: tokens) + && match trt_parse(tokens: read) { + Present { value: tree } => + trt_count(root: tree, production: ^dag_surface_let_expr) == lets && trt_has_nested_let(root: tree) == let_under_let + Absent => false + } +} + +fn trt_mixed_text_round_trips() -> Bool { + let read = trt_lex(text: trt_text(tokens: trt_mixed(), transforms: dag_token_class_emit_transforms())) + trt_token_classes(tokens: read) == trt_emitted_classes(tokens: trt_mixed()) + && match trt_parse(tokens: read) { + Present { value: tree } => trt_count(root: tree, production: ^dag_surface_if_expr) == 1 + Absent => false + } +} + +// THE SIX TEXT ROUND TRIPS, ONE RENDER, ONE LEX AND ONE PARSE EACH. Nullary and pure, enrolled WARM +// in v2.workflow.floor_pure_producer_share: one expression parse is at or past a new witness's +// eval-step budget (this PR's first floor run: 67k for the conditional, 122k for the nested Bind, +// against 72.3k), so each text is round-tripped once at preparation and every claim reads its Bool. +type TrtVerdicts { + bare_body: Bool + empty_literal_body: Bool + minus_body: Bool + bind_body: Bool + bind_value: Bool + mixed: Bool +} + +fn trt_verdicts() -> TrtVerdicts { + TrtVerdicts { + bare_body: trt_bind_text_round_trips(tokens: trt_bind_with_body(body: trt_ident(binding: ^dag_binding_bind_x)), lets: 1, let_under_let: false), + empty_literal_body: trt_bind_text_round_trips(tokens: trt_bind_with_body(body: trt_fixed(classes: [^dag_token_lbrace, ^dag_token_rbrace])), lets: 1, let_under_let: false), + minus_body: trt_bind_text_round_trips( + tokens: trt_bind_with_body(body: list_append(left: trt_fixed(classes: [^dag_token_minus]), right: trt_ident(binding: ^dag_binding_bind_x))), + lets: 1, + let_under_let: false + ), + bind_body: trt_bind_text_round_trips(tokens: trt_bind_with_body(body: trt_bind(value: trt_ident(binding: ^dag_binding_pick_lit_one))), lets: 2, let_under_let: false), + bind_value: trt_bind_text_round_trips(tokens: trt_nested_bind(), lets: 2, let_under_let: true), + mixed: trt_mixed_text_round_trips() + } +} + +// THE BLOCK-SCOPED BIND `{ let k = (v) { b } }`, AT TEXT GRAIN, for each body the emitter may be +// handed: a bare name, an empty brace literal, a `-`-led expression, and a Bind. +test fn a_bind_with_a_bare_name_body_round_trips_as_text() -> Bool { + trt_verdicts().bare_body +} + +test fn a_bind_with_an_empty_brace_literal_body_round_trips_as_text() -> Bool { + trt_verdicts().empty_literal_body +} + +test fn a_bind_with_a_minus_led_body_round_trips_as_text() -> Bool { + trt_verdicts().minus_body +} + +test fn a_bind_with_a_bind_body_round_trips_as_text() -> Bool { + trt_verdicts().bind_body +} + +test fn a_bind_with_a_bind_value_round_trips_as_text() -> Bool { + trt_verdicts().bind_value } // THE RED, KEPT: the same tokens with no transform rows are the rendering the dag target had, and @@ -168,13 +263,8 @@ test fn nested_bind_text_without_separation_reads_back_as_other_tokens() -> Bool != trt_emitted_classes(tokens: trt_nested_bind()) } -test fn mixed_expression_text_reads_back_as_the_same_tokens_and_one_conditional() -> Bool { - let read = trt_lex(text: trt_text(tokens: trt_mixed(), transforms: dag_token_class_emit_transforms())) - trt_token_classes(tokens: read) == trt_emitted_classes(tokens: trt_mixed()) - && match trt_parse(tokens: read) { - Present { value: tree } => trt_count(root: tree, production: ^dag_surface_if_expr) == 1 - Absent => false - } +test fn mixed_expression_text_round_trips() -> Bool { + trt_verdicts().mixed } // THE CLASS, at its cheapest specimen: unseparated, the six tokens are ONE identifier, which is a diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 298d2528144..65f8c290e4b 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -638,6 +638,10 @@ import v2.std.collection { List } // token sequences once each and stores five Bool verdicts; each claim that paid its own parse measured // over the new-witness budget on the floor runs of #13099 (eval steps 72-105k). Portable because it // holds only Bools. +// THE dag TARGET TEXT ROUND-TRIP ROW: v2.test.emit.dag_target_text_round_trip trt_verdicts renders six +// emitted token sequences to text, lexes each and parses each once, and stores six Bool verdicts. The +// floor of #13113 measured one such claim at 67k and one at 122k eval steps when each paid its own +// parse. Portable because it holds only Bools. // THE XL-2 IF-ARM AND STATEMENT-SPINE ROW IS THE SAME GROUND AT THIRTEEN SPECIMENS: // v2.test.claim.namespace_xl0.if_arm_and_statement_lowering_refusal iasl_outcomes drives one front // end over thirteen inline modules and stores one verdict arm per module, portable for the same reason. @@ -902,6 +906,7 @@ data floor_cross_claim_pure_producers_warm: List = [ "v2.test.claim.normalize.authored_marker_spelling.ams_verdicts", "v2.test.claim.body_lowering.caret_symbol_value_lowering.csv_verdicts", "v2.test.emit.dag_bind_let_block_scoped.dbl_verdicts", + "v2.test.emit.dag_target_text_round_trip.trt_verdicts", "v2.test.parse.type_decl_modifier_g0_parse_probe.caret_tree_atom_identities", "v2.test.claim.body_lowering.string_literal_value_lowering.slv_verdicts", "v2.test.claim.body_cast_node.bcn_let_in_value_cast_verdict",