Skip to content

Factor reference_derived_use_lines' per-candidate decision into a typed disposition (survived / registry-absent / export-proof-failed) and expose the census: the emitter already computes the value-position unlisted-use population every Rust emit and consumes it to silently synthesize the missing use - #9478

Closed
gunbai-bot[bot] wants to merge 2 commits into
mainfrom
session/clever-boar-140

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 27, 2026

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session clever-boar-140.
Pushing to session/clever-boar-140 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

gunbc-ci-auto-heal and others added 2 commits August 27, 2026 12:17
…typed disposition and count it: the population it silently repairs was already computed every Rust emit and never named

Since PR 6848 a cross-module name resolves whether or not it is imported. At TYPE positions the
resolver says so advisorily (UnlistedImportUse, is_error_diagnostic false). At VALUE positions it
says nothing at all, and v1.compiler.emit_rust reference_derived_use_lines synthesizes the use-line
the author did not write. The emitter's own note already recorded the gap in its own words -- "a
candidate that registry-resolves to nothing, or resolves but fails export proof, is left
unsynthesized (typed refusal at step-2 is future work)" -- and the deficit's frequency was zero by
construction, so it never ranked for fixing.

WHAT CHANGED: the per-candidate decision was inline in a flat_map whose every non-surviving arm
returned the empty list. It is now reference_derived_candidate_disposition, one function, one call
per candidate, four arms -- CandidateSurvived, CandidateOwnModule, CandidateRegistryAbsent,
CandidateExportProofFailed -- with two consumers of the SAME rows: the use-lines are the survived
arm's names, and reference_derived_census counts them. A census disagreeing with the emitter is
unrepresentable rather than unlikely; there is no second copy of the decision to drift from.

FOUR ARMS, NOT THREE. CandidateOwnModule is not-applicable -- the module provides the name itself, no
import was ever owed -- while CandidateRegistryAbsent is a genuine unresolvable cross-module
reference. Opposite owners, opposite repairs; folding them is the state-space conflation DESIGN keeps
recording.

BYTE-IDENTITY, MEASURED RATHER THAN ARGUED, AND THE FIRST CUT FAILED IT. On a scoped emit of
src/v2/compiler/00_compile.dag (175 files, roots dag + src/v2), the first cut moved one file:
v2_lens_enforcement_vocab.rs, two pub use lines swapped in order, reproduced across three builds
against a byte-identical same-source control. The cause was not the decision -- it was the evaluation
ORDER of emit_rust's preamble, which the factoring had rearranged. Restoring the original order
restored byte-identity. The order-sensitivity is RECORDED as an annotation on the preamble with its
specimen, its reproduction and its next-rung trigger, and the ordering is named as
order-preserving-by-necessity so it is not "simplified" back. The structural argument -- bytes cannot
move unless the decision moves -- was true and covered only the decision, not the scaffolding.

VERIFIED: required-regen first_generation_equal=true; required-ci --required-lane build green
(v2-emission blocking=0, partition-crates 14/14, phases_run=3 failed=0); baseline-vs-change emit
BYTE-IDENTICAL.

WHAT IS NOT CLAIMED. No corpus figure is quoted anywhere, because none is producible: reaching the
census needs a resolved graph, and the only .dag route is a nested compile the interpreter refuses
(NoSuchField Node.ident, measured on three subjects) -- which is why the corpus's two nested-compile
instruments both go through a host builtin. An instrument that cannot execute was written and then
deleted rather than landed and cited. The declared rung is mitigatable, with three independent
next-rung triggers: the class joining the fail-closed wall, an executing home for src/v1 witnesses,
and a nested-compile route to a figure. Five witness rows over the four arms pass when run directly
and are declared NOT run by CI, because src/v1/tests/claim has had no executing consumer since the
2026-08-15 floor cut.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…§4c annotation, and stop calling a pre-existing defect a workaround

TWO REVIEW FINDINGS, one accepted as a defect and one accepted as a wording defect over a correct
substance. Emitted bytes re-verified BYTE-IDENTICAL against a real main baseline after both edits.

1. §4c VIOLATION, ACCEPTED AND FIXED. reference_derived_census_rung_note was a
`data ... : String` row carrying a declared rung, three next-rung triggers, a dated receipt and a
dissolution condition -- the §4c list verbatim, and the #6262 hoisted-prose shape that section names
as the measured failure, where intent is mechanically indistinguishable from program data. It is now
a leading `//` annotation. The review offered the typed rung carrier as the first alternative and
that is the right destination, but no such carrier exists to route to today: DESIGN's own declared
rung drops sit as prose in Building-&-checks, and the executable claims carrier that would hold them
is Stage 1 of the compiler-guarantee recovery plan and is unbuilt. The annotation says so and names
the migration as its dissolution. The conversion also removes a `pub fn` from the emitted seed
(mirror -9 lines), so the seed shrinks rather than grows. The other 30 `data _note` rows in this file
are the pre-existing convention and are NOT touched -- widening into them is a separate change.

2. SELF-AUTHORIZED SCAFFOLD, SUBSTANCE REFUSED, WORDING FIXED. The order-dependence is PRE-EXISTING:
a property of the emitter before this change, not introduced by it, and the ordering kept is the
ordering that was already there, so no artifact is added that must later be deleted and there is no
admitted debt for an operator to approve. The 2026-08-10 ruling governs CREATING temporary work; what
§4b(2) requires of a DISCOVERED class below its ceiling is exactly a named next-rung trigger, so the
trigger is an obligation rather than a permission. The word "workaround" invited the reviewer's
reading and is removed -- and DESIGN's workaround rule is about routing around an obstacle without
diagnosing it, which is the opposite of what happened: the line was stopped, the bytes measured, the
cause located to the preamble, the original order restored. The annotation now states all of this.

VERIFIED after both edits: required-regen first_generation_equal=true planned=137 executed=137;
scoped emit of src/v2/compiler/00_compile.dag against a main baseline fetched at 9917d4a --
BYTE-IDENTICAL, with a same-binary two-run control confirming the instrument discriminates.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 27, 2026

Copy link
Copy Markdown
Contributor Author

Closing as a duplicate. This was auto-opened on session/clever-boar-140, which already has #9439 — same branch, same commits, already reviewed and approved (review 56613 addressed, review 56672 approved), with build/floor/witnesses green.

Work continues on #9439. Closing this one so there is exactly one PR per branch and no ambiguity about which the operator merges.

— sent from clever-boar-140

@gunbai-bot gunbai-bot Bot closed this Aug 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants