Emission follows resolution: one authority for the kernel-identity fact, and the witness enrolled

[gunbai-bot]

Follow-up to #9850. This is a single-authority consolidation, not a repair — see the measurement below before citing it as coverage.

What it does

The infer-side rewire guard and the emit-side use-line filter were each re-deriving "is this resolved node the kernel identity for this name" from the ident_span file marker — and deriving it differently: exact equality on one side, string_contains(sp.file, "<kernel:") on the other. One semantic fact, two readers, one of them weaker. That is the shape of the defect they exist to repair.

Hoisted to v1.compiler.infer_env resolved_node_is_kernel_identity_for_name; both consume it. The emitter's additional condition — that the kernel node is a host-realized structureless scalar, which excludes structural kernels like Bool = True | False whose use-line is the path to the realization — composes beside it rather than folding into it.

import_name_resolves_to_kernel is renamed to import_name_resolves_to_host_realized_kernel_scalar, because the old name described only half of what the predicate now asks. Same function (emit_specific_import_block), same call site. Lanes grepping the old symbol after this lands will get a true-but-misleading absence.

The tightening does NOT discriminate — measured, not assumed

Exact equality and the substring test differ only when a name X resolves to a binding spanned "<kernel:Y>" with Y ≠ X. I tested whether that state is reachable:

fixture	emitted
type Char = Int (alias onto a kernel name), imported	pub use crate::probe_aliaskernel::{Char, Carrier}; — kept
type String = StringLeaf | StringNode {...}, imported	pub use crate::probe_kernelly::{Plain}; — String dropped

The second row is the positive control: the filter is live in that run and does drop names, which is what makes the first row a measurement rather than a silence. An alias carries its own ident_span, not the aliased kernel's — so the substring test already answered correctly there.

The kernel binding for a name is constructed with that name's own span (00_core.dag kernel_span_for), so a cross-name kernel span can only enter an env via a binding substituted across names — which #9850's guard now refuses. The strengthening half is therefore green by construction, and per §4b a permanently-green check is worse than an absent one because it gets cited. It is not claimed as a wall.

Witness

emit_import_lines_follow_resolved_binding_identity enrolled in v1.compiler.compiler_tests_rust: the discriminating RED (a kernel-resolved name must not emit a structural use-line shadow) plus two positive controls — a non-kernel import keeps its use-line, and a kernel-spelled name whose kernel binding is structural keeps its use-line, which stops a blanket kernel-name drop.

A second witness was written and pulled: it reds. std.nat's natively-realized Nat emits as Rc<Nat> at an explicit importer when an unrelated module declares a recursive Nat. That is not new — it is rostered as gunbc.guarantee_rung_drop two_nat_authorities_stall and #9842 already built the same fixture, so this is an independent third reproduction, not a discovery. It retires by the atomic Nat unification wave in gunbc.plans.dag_v2_defork_audit and by nothing less.

Rung drop

emitted_bytes_witness_required_lane — the witness executes in rust-unit-tests, which runs on every push and PR but is not a needs of the required aggregate, so a regression reddens a visible job without blocking. Trigger named at capability grain: a required-lane capability sufficient to assert, on the real acceptance path, that a named pub use line is absent for a sole-exporter type resolved to a host-realized kernel scalar and present for a structural kernel carrying a connective.

Regen

first_generation_equal=true on round 2 after rebuilding from the installed seed; --required-regen-fixed-point reports fixed_point_equal=true referenced_first_generation_equal=true at 20e5f08. The rebuild is load-bearing — the first pass runs a binary predating the change it emits, so one pass can self-verify at divergence 0 for the wrong reason.

Merged origin/main rather than rebasing (squash-merge means branch and main share no ancestry for this content). Four generated paths came back unmerged with no conflict markers and ours bytes in the worktree; the compile caught it via main's own LiteralUnfolding::UnicodeScalarSequenceUnfold. Resolved by regenerating from the merged authority, not by picking a side.

[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-09-01T02:56:40.188934Z	471e8d8	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: 471e8d8de3

ℹ️ 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]

Filter kernel-resolved names from wildcard imports

When a module uses an all-import such as import v2.std.text, passing module_env into emit_specific_import_block does not prevent the shadow this change targets: the wildcard arm still unconditionally emits use crate::v2_std_text::*;, which brings the structural String declaration into scope regardless of the filtered specific block. Such consumers therefore continue to bind emitted bare String references to the structural alias instead of the host/kernel type and can retain the same E0308 failures; the wildcard line itself must honor the resolution filter rather than only filtering the supplementary explicit imports.

Useful? React with 👍 / 👎.

[gunbai-bot]

DO NOT MERGE IN THIS STATE — converting to draft to prevent an accident.

This PR is CLEAN, green, and carries an approval bound to its exact head — and merging it would revert most of tonight's work.

Measured against origin/main (0e8c49ddee):

• PR head is 471e8d8de3, which is Emission follows resolution: remove the std::string::String ↔ Rc<im::Vector<i64>> expected/found family against the 155-row boundary #9850's already-merged head.
• Merge base is 1c67f50368.
• git diff origin/main 471e8d8de3 = 114 files changed, 3752 insertions(+), 11502 deletions(-).
• The branch's own delta since the merge base is only 4 files / +163 — i.e. the Emission follows resolution: remove the std::string::String ↔ Rc<im::Vector<i64>> expected/found family against the 155-row boundary #9850 content, which is already in main.

So essentially all of that 11,502-line deletion is main's newer content being removed. Seven PRs have landed tonight (#9720, #9850, #9858, #9773, #9866, #9851, #9865) and this branch predates them.

mergeStateStatus=CLEAN does not mean safe. It means no textual conflict. Under squash-merge a fully-merged branch is never an ancestor of main, so it looks permanently ahead while actually being behind — and a clean auto-merge of it is a revert. This is the fourth instance tonight (#9861, #9863, #9870); #9863 had the same shape and would have reverted the #9850 repair.

@bold-carp-449 — before pushing your follow-up: merge origin/main into this branch first, don't rebase and don't cherry-pick. Watch for ADD/ADD on files only one side created (the squash manufacturing a conflict), and if any generated path appears the merge driver refuses rather than resolving — it leaves the ours side with no conflict markers and the path merely unmerged, so git status unmerged paths is the check and regeneration from the merged authority is the resolution. Then flip back to ready.

Note the approval on this head does not survive that push, which is correct — it was a statement about a tree nobody should ship.

[gunbai-bot]

Correction to my previous comment — I was wrong about the revert.

I claimed merging this would delete main's newer content, based on git diff origin/main <head> showing a large deletion count. That is not what a merge does. For a branch that is behind main, that two-endpoint diff necessarily renders main's newer content as deletions — but squash-merge applies the branch's diff relative to the merge base, so main's newer content is never touched.

The check I should have run first:

git merge-tree origin/main <head>     # -> merge result tree
git diff origin/main <that tree>      # -> EMPTY

The merge result is byte-identical to main. This PR merges to a no-op — it was never a revert risk.

What stands: the branch contributes nothing beyond main, so closing it is still correct housekeeping and the content measurements in my earlier comment (added lines already present in main) were accurate. Only the "would revert" conclusion was false, and the alarm it raised was unjustified.

Reusable form, since this will bite someone else: a raw git diff main head on a behind-branch looks like a catastrophic revert and is not one. Judge a merge by git merge-tree, never by the two-endpoint diff.

Additionally: I converted this PR to draft on that false basis. It is safe to merge (as a no-op) or to build on. Leaving it as draft only because @bold-carp-449 is folding follow-up work in, which will supersede this head regardless — say the word and I will flip it back to ready.