XL-2: kernel String concat through the free-monoid roster; v2 templates in parse (hole-aware body)

[gunbai-bot]

Summary

Re-derives XL-2 on current main (does not rebase #13430 / #13638 / #13284). Kernel String concatenation is admitted through the free-monoid structure (not a coined concat type, and not Int's additive monoid): v2.std.algebra_structure_signature free_monoid_structure_type_node bounds the collection-roster carrier M on a BinderStructureEdge, and v2.compiler.infer infer_application_structure_bounds admits an instance only through the one inhabitance authority (dag_free_monoid_free_monoid_inhabitance / list_append, dag_host_text_free_monoid_inhabitance / v2.std.node.host_text_concatenation). Host text and v2.std.text String (FreeMonoid<Char>) stay distinct; the host-text row's generator is std.types.Char (Ruling 3 / the 2026-09-27 text ruling).

The dag surface also gains a string-template lex/grammar production (^dag_string_template), disjoint from a plain string literal by hole opener. Templates are the host-text crossing, not a seed to_string hack: a hole is an expression, not interpolated text. Lowering of a template shell to a concat chain is not in this PR (no 02_parse / body_lowering_fold decode); that remains a follow-up so a hole is a resolve reference.

Parse fix (this session, f11289a): dag_grammar_primary_expr_core was missing a matching close after the template alternative (expected RParen, found RBrace at that function). Isolated compile: gunbc compile --source-dir <only dag.dag> --output-dir /tmp/x --target dag — frontend succeeds after the paren repair. That was the witnesses self-host parse-failed / EmissionRefused on ac34899.

Real-path claim (was red)

fmb_kernel_text_concat_is_accepted_through_its_row refused infer_reason_caller_admission_callee_unresolved, located at the concat(a, b) application (correction suggested at the callee DeclarationReference).

Chain (DESIGN 6b): resolve binds bare concat to std.algebra.collection_concat_shape; infer types the call from the roster signature (collection_roster_signature_arrow). Caller admission then treated that mark as an indexed fn, looked it up in the subject's symbol index, and refused Unresolved — the row is a template value, not a callable with admit_callers. Earliest unjustified boundary: infer_caller_admission_roster_from_declarations / the unmarked-facts arm of infer_caller_admission_application_diags. Not call_result_of_a_declared_return_type_unjudged_in_v2_infer (kernel String result is judged). Fix: roster primitive-call heads impose no admission clause. Deleted the ActiveFillDebt row for this claim.

claim_batch (witnesses does not run claim files)

claim_batch --hermetic --source-root dag --source-root src/v2 \
  --entry src/v2/test/claim/compiler/free_monoid_structure_bound_test.dag \
  --functions fmb_kernel_text_concat_is_accepted_through_its_row

PASS, process exit 0. [witness] ... eval_steps=523863.

claim_batch --hermetic --source-root dag --source-root src/v2 \
  --entry src/v2/test/claim/caller_admission_native_wall_test.dag \
  --functions a_roster_primitive_call_callee_imposes_no_admission_holds,a_marked_callee_whose_declaration_is_unavailable_refuses_holds,an_unmarked_callee_is_not_judged_holds

PASS ×3, process exit 0.

Re-derived from / not carried

• Carried (intent of v2: kernel-String concat through a free-monoid structure bound on the roster carrier (XL-2) #13284 / concat half of XL-2 PR2b: string templates — disjoint lexer, one ^dag_string_template node, concat-chain lowering #13430): free-monoid structure bound, BinderStructureEdge vs BinderTypeEdge, host-text inhabitance row, infer bound check, roster signature over carrier M + generator E, claims v2.test.claim.compiler.free_monoid_structure_bound / concat / count updates, RFM receipts.
• Carried in part (XL-2 PR2b: string templates — disjoint lexer, one ^dag_string_template node, concat-chain lowering #13430 templates): lexer modes + one grammar production in v2.extdeps.languages.dag.
• Not carried: Unicode IdentStart hole-opener widening (Codex on XL-2 PR2b: string templates — disjoint lexer, one ^dag_string_template node, concat-chain lowering #13430; ASCII IdentStartChar + (/!/- as on the old head); v1 fused adjacent holes (seed defect, not reproduced); tplscan scratch; ServiceSetAside delete-first (XL-2 3c: enumerate ServiceSetAside consumers before delete-first #13637 plans-only — census on main: the type and accumulators still live in v2.compiler.body_lowering_fold, diagnostics feed normalize_census and the service/resource lowering claims; no delete in this change).
• Not reopened: old PR heads. History only.

ServiceSetAside census (asked by #13637)

Still present on main / this branch: ServiceSetAside / ServiceSetAsideKind in body_lowering_fold, service_set_aside_diagnostics, normalize_census advisory path, claims under src/v2/test/claim/normalize/service_* and resource_declaration_lowering_test. RFM service_interface_member_has_no_carrier still names the trigger. Not a delete-first in XL-2.

Receipts (head 8b6999f29eb6)

• gunbc test //gunbc/instruments:self-host — witnesses job 38084429587 step "emit and build //gunbc/instruments:self-host" success (process exit 0).
• gunbc test //gunbc/instruments:v2-native-cli — same run, step "emit and build //gunbc/instruments:v2-native-cli" success (process exit 0).
• Prior head f11289ac61e: witnesses run 38082349398 also success; this head is the escape-body follow-up after review 78468.
• srv1 from this session: Permission denied (publickey); instruments are the required-job steps above, not a local systemd-run.

Test plan

Seed: CTRL_BUILD_MODE=local CARGO_TARGET_DIR=/tmp/cargo-target-eager-ram-629 cargo build --release -p v1-compiler --bin gunbc and --bin claim_batch (control: cargo check -Z definitely-not-a-real-flag refused on stable as required).

Isolated parse of src/v2/extdeps/languages/dag.dag after f11289a: frontend green (remaining diagnostics on a one-file dir are unresolved imports).

claim_batch --source-root dag --source-root src/v2 --entry src/v2/test/claim/compiler/free_monoid_structure_bound_test.dag:

• PASS: fmb_kernel_text_concatenation_executes, fmb_bound_admits_kernel_text, fmb_int_refuses_at_the_free_monoid_bound, fmb_bool_refuses_at_the_free_monoid_bound, fmb_structure_bound_is_not_judged_as_a_kind_at_resolve, fmb_kernel_text_has_generator_char, fmb_int_has_no_free_monoid_generator, fmb_malformed_inhabitance_row_refuses_with_its_own_cause, fmb_mixed_carriers_refuse, fmb_list_of_edge_has_generator_edge, fmb_fixed_element_disagreeing_with_the_generator_refuses, fmb_structure_shaped_kind_is_still_kind_checked
• PASS (superseded the earlier FAIL recorded here): fmb_kernel_text_concat_is_accepted_through_its_row. The real-path claim now passes on 71162bc. Its refusal was infer_reason_caller_admission_callee_unresolved, fixed at caller admission (a roster primitive-call head imposes no admit_callers clause; see the chain above), and its former ActiveFillDebt row is deleted.

srv1: ssh srv1 from this session is Permission denied (publickey). Instruments //gunbc/instruments:self-host and //gunbc/instruments:v2-native-cli are left to the required witnesses job on this head (f11289a), not run in the 24 GiB session container.

Review 78460 (claude) approved ac34899; that approval is stale relative to f11289a (parse-only). No GitHub REQUEST_CHANGES.

Review 78485 (unicode escape vs hole)

dag_string_unicode_escape_prefix_pattern consumes \u{ as v1 scan_string_body does. claim_batch --entry src/v2/test/claim/tokenize/string_literal_raw_newline_test.dag --functions unicode_escape_letter_hex_lexes_as_one_string_literal,unicode_escape_digit_hex_lexes_as_one_string_literal PASS ×2, exit 0.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-10T19:36:24.706413Z	ac34899	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ac34899b9a

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Keep extended string escapes lexable

When a string contains a valid \xNN or \u{...} escape, the simple-escape branch does not match and this new predicate rejects the fallback branch solely because the next character is a backslash. Those forms are explicitly handled by dag_string_decode_* and are used in files such as dag/extdeps/render/ansi.dag and src/v2/extdeps/languages/bash_command_fold.dag, so the v2 tokenizer can no longer ingest those modules. Exclude only interpolation openers here, or otherwise add the extended escape patterns before rejecting backslashes.

Useful? React with 👍 / 👎.

[gunbai-bot]

Parse failure on head ac34899 (src/v2/extdeps/languages/dag.dag parse-failed / closure-load EmissionRefused on witnesses run 38080341195) is the extra/missing paren in dag_grammar_primary_expr_core after the string-template alternative. Isolated gunbc compile --source-dir on that file located expected RParen, found RBrace. Fixed on f11289a (same branch). Review 78460 approved ac34899 and will need a fresh look at this head.

[gunbai-bot]

Review 78468 (claude, APPROVE on f11289ac61):

• Squash the WIP commit with the parse fix before landing: not doing a history rewrite here. Merge policy is squash-merge; the operator flattens on land. The two commits stay as-is on the branch.
• Title vs what landed: the PR body already states the split — concat/free-monoid structure bound is the typing cut; templates in this PR are lex + one grammar production only, with parse/resolve/lowering of holes called out as not carried. No title change (the work item names the XL-2 pair); the body is the accurate description.

Codex inline on dag_string_body_element_pattern (excluding every backslash, not only the hole opener): that was a real regression against main. StringTextChar still admits \ so \x/\u{ were body characters then decoded; NotFollowedBy of backslash-or-hole made those unlexable. Fixed on 8b6999f by excluding only dag_string_hole_opener_pattern, which is the disjointness the template rule needs.

[gunbai-bot]

Review 78485 (first finding): agreed. dag_string_escape_sequence_pattern only admitted the eight single-character escapes, so in \u{E9} the backslash and u were StringTextChar and {E matched dag_string_hole_opener_pattern (E is IdentStartChar). That forked this module's own escape table.

Fix on 0894eb0: dag_string_unicode_escape_prefix_pattern consumes \u{ the way v1 scan_string_body does, so a unicode-escape brace is never a hole opener. Discriminating red: unicode_escape_letter_hex_lexes_as_one_string_literal (\u{E9} is one dag_token_string_literal). Green: unicode_escape_digit_hex_lexes_as_one_string_literal (\u{0002}).

Second finding: string_interpolation_read_as_literal_text_by_v2 no longer says the body pattern has no interpolation arm. It records the XL-2 split and this unicode-escape climb.

HOLD: fmb_kernel_text_concat_is_accepted_through_its_row PASSed on 7fd4c52 (claim_batch exit 0); its ActiveFillDebt row is gone. Unchanged here.

[gunbai-bot]

Review 78494: agreed. free_monoid_structure_generator_optional returned optional_absent() for a missing generator, NamedChildAmbiguous, and binder_node_parts Absent, so infer_bound_generator_agreement skipped the wall and a disagreeing argument-fixed E could be admitted. The row arm named that same collapse infer_reason_inhabitance_row_declares_no_generator.

Fix on 58b90d7: free_monoid_structure_generator_declaration is three-armed (GeneratorDeclared / GeneratorNotDeclared / GeneratorMalformed { cause }), matching algebra_inhabitance_field_declaration. Both call sites refuse Malformed with the cause, typed and located.

Reds: fmb_ambiguous_generator_binder_refuses_with_its_own_cause (two generators → algebra_free_monoid_generator_ambiguous) and fmb_unreadable_generator_binder_refuses_with_its_own_cause (non-binder generator → algebra_structure_field_not_a_binder). claim_batch PASS ×6 including those and fmb_kernel_text_concat_is_accepted_through_its_row.

Review 78485 (\u{ prefix + RFM) remains on this history (0894eb0 / 12490d8).