XL-0N: generic LiteralElaboration/OperatorRealization authority — typed literal-to-Zero/Succ homomorphism, operator realization by exact operand structure, structural Peano Nat (no i64 row)

[gunbai-bot]

Summary

XL-0N (node://adhoc-aec65f93-b00). v2.std.nat.Nat = Zero | Succ stays the structural Peano coproduct; no Nat -> i64 realization row is added. Instead the compiler gains its first generic authorities for the two things the emitted v2 closure was getting wrong by spelling:

1. Literal elaboration (std.literal_elaboration, dag/std/literal_elaboration.dag): a kernel literal at a typed boundary whose exact destination DeclarationRef declares a homomorphism from the kernel value is replaced, in the typed tree, by a new core carrier ExprElaboratedLiteral { value, elaboration } whose child is the literal's image under that homomorphism (Succ { prev: … Zero } for the Peano unfolding), typed as the destination. v1.compiler.infer applies it at every position that already supplies an expected type (call argument, declared return, record field, data initializer, annotated let, list element, map value, block tail) and at the other operand of a binary operator when one side is a literal. Emission renders the image as ordinary constructors and never re-decides from spelling, imports, or rustc expectations. Outcomes: DirectLiteral | ViaHomomorphism | LiteralElaborationRefused { HomomorphismDuplicated }. The interpreter evaluates the image (its numeric grounding folds Succ/Zero exactly as authored ones) — 2 hand-Rust arms in v1_interpreter.rs, the only hand-Rust in this change.
2. Operator realization (std.operator_realization, dag/std/operator_realization.dag): emit_typed_bin_op decides by the operand's exact declaration — HostOperator when the declaration realizes natively on Rust (v1.compiler.coercion declaration_realizes_natively_on_rust: exact binding, then the identity-gated checkpoint), StructuralEquality (the emitted enum's derived PartialEq), StructuralComparison (a call to the declared comparison tested against std.algebra.Ordering), or a typed compile_error! refusal for infix arithmetic on a structural operand.

Rows live in gunbc.structural_realization_bindings: KernelIntLiteral -> v2.std.nat.Nat via Zero/Succ/prev; KernelBoolLiteral -> v2.std.logic.Bool via True/False (BooleanUnfold, the manager's Bool addition — the interpreter realizes Bool natively and evaluates an elaborated literal as its kernel value, so the Bool image is evidenced on the emitted path only); v2.std.nat.Nat ordering via nat_compare. where-refined declarations (NonEmptyStr, Char, VersionIdentity) resolve to the parser's one-child Conj refinement wrapper, so the operand decision hops is_where_refinement_type → base (resolved through the env) — the type renderer's own route (render_rust_alias_rhs_type) — before judging; measured under regen, where the earlier alias-item hop could never fire. Every BinOp match in std.operator_realization is total over the 14 closed variants (no non-fold-residue rows). XL-0T adds its FreeMonoid unfolding arm and one row; nothing per-destination exists in inference or emission.

The census subject is repaired at its source too: v2.std.nat gains a structural nat_compare (the old body was if a == b … if a < b — the host < rustc refused), nat_sub (typed underflow), nat_div_rem (NatDivisionByZero arm) and nat_div_rem_by_succ (the zero divisor has no constructor). v2.std.integer's decimal conversion is rewritten onto them, with one digit-glyph table shared by the Peano and machine-integer renderers; the two Int-valued callers that passed an Int into the Nat renderer (native_agreement, realization_sweep — E0308 sites) now call a real Int formatter.

floor_expected_red chunk 14 (w_kernel_numeric_at_the_peano_nat_is_refused) is retired by its own stated trigger ("the expected-type-directed literal introduction judgment is NOT built"); the witness now asserts the ruled admission through the homomorphism and stays enrolled as a control (DESIGN §4b(4)).

Identity at the boundary (measured; read once at inference, carried on the typed tree)

v2.std.nat.Nat is recursive (Succ { prev: Nat }), and the resolver leaves a recursive type reference in place (resolve_node leaf arm, is_recursive_type_for → resolved: n, no inferred). The identity lookup matched the reference-site span against the declaration span and answered Absent, so every Peano boundary fell to its "identity unavailable" arm while v2.std.logic.Bool (not recursive) worked on the same compiler. Fix (v1.compiler.infer_env type_reference_declaration): resolve the reference through its scoped env binding (lookup_type_for) before span-matching. That binding is live at inference and gone at emission (only the module env survives), which is why the literal rows passed and the operator rows kept the host token: a by-name fallback tried for the emitter was refuted by construction — it answered the pool-precedence homonym std.nat.Nat (native, i64) for a module importing v2.std.nat.Nat, and the span match confirmed that homonym exactly. So the operand's declaration is now read once, at inference, and stamped on the typed tree as ExprBinOp.operand: OperandDeclaration { declaration, decl_file } (after hopping a where-refinement to its base); emit_typed_bin_op consumes it and never re-reads identity. The by-name arm is deleted.

An operand whose type node names no declaration (inference-synthesized field-access / method-return nodes: no span, no file) is OperandIdentityUnavailable { facts } and decides by operator class, never by a default: ==/!=/&&/||/?? are the host token by construction (structural and host equality are one token on the target — the emitted enum derives PartialEq), ordering and arithmetic refuse carrying the shape facts. The pre-lane Unavailable => HostOperator arm was the absorbing fallback (DESIGN §5) that hid this lane's own defect; the refusal census that replaced it measured the whole v1 closure at 50 sites / 139 refusals, every one under ==/!=. Kernel-minted types (<kernel:…>), generic type parameters and host containers are their own named arm (HostRealizedOperand).

Partition layout: std.literal_elaboration / std.operator_realization registered in the std-core partition and gunbc.structural_realization_bindings in the v1-infer binding unit (v2.workflow.rust_crate_partition), with module-dag edges; the generated artifact gunbc.stage0_crate_partition_generated regenerated via generated_artifact_gate main_wet and the partition crates re-rendered by claim_executor --emit-partition-crates --write (never hand-edited).

A second, separate defect surfaced on the way and is fixed at its single site: a record literal nested in field position (Succ { prev: Succ { … } }) was rendered with the outer type's name as its head (Nat::Nat) because emit_field_value_with_context handed the raw resolved type to the constructor namer while the top-level path expanded it first (expand_type_for_field_access); the nested site now expands the same way.

Falsifiers (required seed prefixes)

• v2.test.claim.self_host.peano_nat_structural_realization_test — 26 rows: nontrivial Succ values compare/subtract/divide/convert correctly; divide-by-zero is typed; the generic decisions by row and identity, including removing the row returns the literal to DirectLiteral (the E0308 shape) and duplicated rows refuse; an operand without a readable declaration refuses under <// and is host under ==; the Bool row is found by exact destination, Direct once removed, and Direct at the native std.types.Bool (no variant of Bool is matched by name in interpreter-run rows).
• test.claim.self_host_peano_literal_operator_realization_witness_test — emitted bytes through the production emitter: literal at argument/return/operand boundary emits its Zero/Succ image (forbidden tokens are the pre-lane rendering), </<= call nat_compare against Ordering, infix / on Nat refuses in the bytes, a kernel true/false at a v2.std.logic.Bool boundary emits Bool::True/Bool::False while the native std.types.Bool keeps the keyword, and three host controls (native Int, and std.nat.Nat — same spelling, different declaration — keep the host token and the bare digit).

Test plan

• claim_batch … --entry src/v2/test/claim/self_host/peano_nat_structural_realization_test.dag --functions <all 26> in the interpreter on the fixed-point binary: 26/26 PASS (regen20).

• claim_batch … --entry dag/test/claim/self_host_peano_literal_operator_realization_witness_test.dag --functions <all 12> through the production emitter on the fixed-point binary: 12/12 PASS (regen20; was 9/12 before the typed-tree operand carrier, 6/12 before the nested-head fix + layout).

• gunbc compile (prebuilt seed) over the model modules, v1.compiler.coercion, v1.compiler.infer_env and the rewritten v2.std.integer closure: 0 blocking diagnostics.

• Seed regen (BuildBuddy, bootstrapped from the committed mirrors, rounds to first_generation_equal=true): every head on this branch since 370f5fa converged at round 2; the mirrors are committed at each step. CI on earlier commits was red by construction (pre-lane mirror, then mirror drift between a .dag change and its regen round).

• Whole-closure census, src/v2/compiler/00_compile.dag emitted through the production pipeline (gunbc compile -> cssl_assemble -> cargo build --lib --message-format=json, BuildBuddy 20 GB runner; the instrument's 16 KiB stderr capture truncates this closure, so the rows are read from the JSON messages) -- identity diff, row = (rustc code, emitted file, message), lane head 2177446 vs main head 0a6d177: main 57 rows -> lane 52 rows; 5 rows gone, 0 rows new, and no row mentioning Nat remains. Gone: E0369 v2_std_nat.rs binary operation < … Rc<v2_std_nat::Nat>, E0369 v2_std_integer.rs binary operation < …, E0369 v2_std_integer.rs cannot divide Rc<v2_std_nat::Nat> by {integer}, and two E0308 v2_std_subject_evidence.rs rows. The remaining 52 are other lanes' classes (E0004 Edge exhaustiveness, E0223, E0277, the Rc<i64> wraps of the agreed follow-up). The E0308 literal-at-Nat sites share the generic mismatched types message with unrelated sites, so at this row grain they are witnessed by the per-file rows above and by the emitted-path battery rather than as distinct identities.

  A CORRECTION TO AN EARLIER RUN OF THIS SAME MEASUREMENT, recorded rather than quietly restated. The first pass keyed rows on ^E\d{4} and so DROPPED every rustc error carrying no code -- which is exactly what a compile_error! refusal is, the shape this lane introduces. Under it the head reported 52 rows against a TOTAL 53, and the discrepancy was the whole finding: the hidden row was a refusal THIS lane produced at v2/compiler/02_parse.dag parse_current_position (t.start + 1, where t binds the value of a generic ListHeadResult<T> and the field-access type node inference builds carries no authored name). So "0 new" was true only of the codes the filter could see. The arm is fixed at its cause -- an operand type node with NO authored name is not a reference to a declaration, and is HostRealizedOperand { UnnamedSynthesizedType } -- and the numbers above are from the corrected instrument, where mine 52 = TOTAL 52 closes the same gap by identity rather than by assertion.

• Required floor: new witnesses planned/passed by identity in required_floor_disposition.tsv.

🤖 Generated with Claude Code

https://claude.ai/code/session_013koFunEtpLQCnvUiz85k7Y

[gunbai-bot]

On review 57758 — three of the four findings are fixed in e1e14c8; this is the reasoning for the part of finding 3 I am not changing.

Fixed

• src/v2/std/nat.dag:119 prose in a String row — converted to a module-scope // annotation on nat_max. The row predates this lane (The emission ratchet's subject is { root, kind, resolution policy }, and membership is observed beside it rather than folded into it #9238), but the file is this PR's to fix, so it is fixed rather than inherited.
• The fork narrated without a dissolution schedule — now gunbc.guarantee_rung_drop two_nat_authorities_stall: current Mitigatable, ceiling StructurallyImpossible, AwaitsOneGrounding, bounded population, and a trigger naming the capability (one Nat declaration with the other derived from it) rather than an artifact. Deleting either declaration without deriving its operations would remove the operations its consumers call, which is why the trigger is written that way.
• binop_label as a parallel operator-spelling authority — the concern is right in direction, so I went further than relabelling it. OperatorRealizationRefusal now carries BinOp itself in both variants instead of String; producers pass the variant; the spelling happens exactly once, at the human-readable message boundary. Nothing downstream can compare operators by string any more. On "the parser/emitter already owns it": I checked the corpus before keeping the table and could not find an owner — no BinOp-to-glyph producer exists anywhere in the tree, src/v1/compile.dag renders the variant name (Add), and glyph recognition happens in the tokenizer against token kinds, not a .dag row. So it is the first authority for that mapping, not a second one; the annotation above it now records that check. The rendered message text is unchanged, so the emitted-path witness pins the same bytes.

Not changing: OperandShapeFacts.connective / decl_file

connective cannot inhabit the connective coproduct without creating an import cycle. The value written into that field is v1.compiler.core's Connective (src/v1/00_core.dag:54), and v1.compiler.emit_rust already imports std.operator_realization (src/v1/05_emit_rust.dag:135). Typing the field as that coproduct makes std.operator_realization import v1.compiler.core, closing a cycle — and acyclicity is the substrate's one structural law under DESIGN §4, so it is not a trade I can make locally. v2.std.node's Connective is a different declaration and would not accept the value. The honest fix is one Connective authority both layers can import, which is a substrate move well outside an operator-realization change.

decl_file is deliberately not a citation. OperandShapeFacts is the payload of the arm where declaration identity could not be read, so a DeclarationRef is unconstructible there by construction — the whole point of the record is to report the shape the compiler actually saw instead of widening to a host token. This module does use std.decl_ref.DeclarationRef everywhere identity is available.

— sent from loyal-raven-297

[gunbai-bot]

Closing: superseded by #9710, which merged this lane's substance to main (main@6ef73334e0b carries std.operator_realization, std.literal_elaboration, OperandDeclaration, and the Peano Nat operations).

Measured rather than assumed — a two-dot diff against the new main, since three-dot overstated (this branch's merge-base is old). What main lacked was exactly the review findings raised here after the 2177446 snapshot main carries: the String-typed refusal operator, the consumerless binop_is_ordering, the §4c prose row in src/v2/std/nat.dag, and the missing two_nat_authorities_stall. Those are rebuilt against main in #9794 rather than landed from this stale branch, which is now behind main and would revert newer work.

One row from here was deliberately dropped rather than carried: structural_connective_stall. Main declares StructuralConnectiveBinding and routes And/Or through structural_connective_realization, which is the capability that row named as its next-rung trigger — so it is retired, and re-adding it would have declared a stall its own trigger had dissolved.

— sent from loyal-raven-297