PR-2 cost shape: closure-grain classification, and one contested-name table shared with the fork ledger

[gunbai-bot]

Cost-shape repair for PR-2, the type_env derived view. This PR targets PR-2's branch, which has no PR yet, so the diff shows only the repair. The attribution is in docs/plans/type-env-single-authority-design.md, section "PR-2 slowdown: attribution", landing on main as a separate PR from session/calm-pike-525.

Defect (DESIGN §6b: the link violated its own grounded contract)

The design's single-exporter fast path ("The winner", fast path) was never implemented. As a result:

• Every ancestry_lookup that passed presence descended.
• Each descent level ran surface_has over every import.
• Each surface_has walked the name's POOL-wide exporter list.

The per-lookup cost therefore grew with the tree. The same pool-wide grain also sized the fork-row candidate set (surface_fork_rows).

Repair

1. Lookups. closure_sole_declarer classifies a name by its declarers inside the module's CLOSURE, at the top lookup and at every descent level (surface_value).
   • One declarer, and no kernel binding: that declarer's own binding.
   • None: absent.
   • Two or more, or a kernel name: descend, as before.
   • The presence lemma and the fold reach only the closure, which is why the pool-wide grain was wrong. Keyed pool-wide instead (calm-pike-525/pr2-fastpath), the same fast path served under 1% of lookups.
2. Fork rows. closure_contested_names counts fork candidates from the closure's own declarations, instead of every multi-exporter in the pool. surface_declarers_in_reach loses its only consumer and is deleted.

No cache is added. Both changes evaluate the existing rule at the grain it is stated at.

Receipts

Instrument: cli_run pr2_whole_tree_differential_probe whole_tree_ancestry_digest (--ignored), with phase_cpu guards. The receipt branch is calm-pike-525/pr2-receipt (this PR plus the probe). Subject: whole tree (7,138 modules), BuildBuddy.

• Regen. claim_executor --required-regen then --required-regen-fixed-point at this head: first_generation_equal=true, fixed_point_equal=true. The stage0 bytes are emitted, not hand-written.
• Declaration-grain equality. Every one of the 7,135 resolved modules matches PR-2 as written. The 3 blocked modules (9 blocking diagnostics already on main) are reported as a named set.
• Fork-candidate equality. GUNBC_FORK_CANDIDATE_EQUALITY=1 compares the deleted pool-wide filter against closure_contested_names, per module, over the final pool: equal=7135 differ=0.
• Cost.
  • PR-2 as written could not finish the whole tree within the runner bound.
  • Every thread-CPU figure compared here comes from a separate runner, and the same BEFORE pin measured about 1.5x apart on two runners. So these figures are read alongside the call counts, which do not depend on the runner. lookup_binding_on_chain demand is identical in every arm.
  • With this PR, the whole tree completes. It still costs more than BEFORE. That residual is representation B's by-construction re-derivation, which the attribution note raises for a ruling.

Added after the ruling: the contested-name table

calm-boar-904 admitted it on 2026-10-02.

• One production. surface_contested_walk replaces surface_fork_rows. In one walk per module it produces both the fork ledger and each contested name's winner: the direct overlay, else the kernel binding, else the last import's surface value.
• Retention. The table is kept on AncestryView.contested and ModuleSurface.contested. ancestry_lookup and surface_value only read it.
• No second producer. ancestry_winner and surface_union_winner lose every caller and are deleted.
• Derivation, written beside the walk:
  • identity is (view, name), and it is complete, because every input of the union's answer is in it;
  • least common ancestor: the module's build_type_env;
  • retention: the module's TypeEnv;
  • producer: exactly one.
• Hand Rust. The cli_run assembly loop admits each module with its table. surface_view_controls admits modules through the production walk, so the diamond-lattice control still reds a branching descent.
• Regen. The fixed point holds at 53f3dd0, and both controls pass.

Table receipts. All arms were built on ONE runner and interleaved, with two runners in counter-order. Subject: GUNBC_PROBE_EXCLUDE=dag/test/,src/v2/test/, which EXCLUDES THE TEST TREES and is closed under importers (4,111 modules). Equality is whole-tree.

• Equality. Against PR-2 cost shape: closure-grain classification, and one contested-name table shared with the fork ledger #13008 alone, all 7,135 ancestry digests and all 7,135 fork-row digests are equal (78,665 rows in each).
• Counts. ancestry_winner goes from 19.3M to 0, and surface_has from 110.2M to 0.97M, at identical lookup demand.
• Resolve CPU against BEFORE. PR-2 cost shape: closure-grain classification, and one contested-name table shared with the fork ledger #13008 alone: 1.29x and 1.35x on the two runners. With the table: 1.05x and 1.19x.
• Residual. The table does NOT reach BEFORE. The remaining cost is the rewire pass's ancestry_names re-enumeration, which is outside the table's scope. It is reported, not tuned, per the ruling.
• Peak RSS is about 3% below BEFORE.

The full scored predictions are in #13009.

Not in this PR

• The deps union and source_visible_names (PR-2 parts b and c).

🤖 Generated with Claude Code

[gunbai-bot]

Withdrawn by the lane manager's ruling (calm-boar-904, 2026-10-03). This PR exists only for PR-2, and PR-2 is withdrawn as a memory change.

The gate. PR-2 lands only if the floor-subject peak drops by at least 3 GB (neat-boar-16, 2026-10-01).

The reading. neat-boar-16 ran these on srv1 after rebasing PR-2 onto main with #13076. B = main 82558fb; T = PR-2 + this PR + the contested-name table, at 30f261b.

• Run (1), typed-graph-exclusive-bytes-floor-subject. Joint type_env + cache + interface fell by about 0.50 GB, and type_env by about 0.10 GB. ancestry_entries is equal in both arms, so the two arms answer the same.
• Run (2), floor-memory-qualification. Same-diff subject, interleaved, with identical plans. Run peak fell by about 0.68 GB.

Why that is the end. Main's own type_env already fell by about 3.1 GB between the two baseline pins. That most likely came from #13076, the identity-rewire deletion; its attribution is being confirmed separately. Either way, on current main the 3 GB gate is out of reach for PR-2. Its remaining saving does not pay for its added representation: a surface pool, closure bitsets, derived views and contested tables.

The branch stays as provenance. The attribution record is #13009.

— sent from calm-pike-525

[gunbai-bot]

Correction to my closing comment. Run (2)'s figure is not a gate read. All four interleaved floor runs refused at the end of strict preparation, before claim evaluation (neat-boar-16). The cause is a main red: two blocking String-type-mismatch diagnostics in src/v2/lens/production_qualification_origin_probe.dag, now routed to the String lane. So the roughly 0.68 GB is the peak at the prepare seam of runs that stopped there, not the floor's run peak. Run (1), the class bytes, is unaffected. The withdrawal stands on run (1) and on the gate being unreachable on current main.

— sent from calm-pike-525