Scope rank-view step 2: the carriers and their executing equivalence laws

[briansrls]

Step 2 of scope-rank-view-design.md §8. The model landed as #9825 with no seed consumer; this lands the carriers beside the fold plus the laws that make them consumed rather than dangling (DESIGN §3c).

No reader moves and no map is deleted. §8 forbids a leaf-first cutover — "a surviving map is DESIGN §3's attractor" — so readers and materialized maps go together in step 3, in one motion.

Why this is the slice

The floor's [floor-scope-split] names the cost and the tree names the correction beside it: "a scope that is a view rather than a rebuild costs nothing to enter." A per-scope winner map stores the answer to "of the subject's declarers of this key, which one ranks first in this scope?" — already determined by the subject-wide claimant relation and the scope's ordered admission. There is no single winner to share across scopes (it legitimately differs with order), so §2's "carry the first value" applies to the claimant relation, and the winner is derived from its join with rank at the ask.

What's here

• SubjectItemDeclarers — the subject-wide claimant relation, module identity taken from module.func_env.name and declarations from module.item_registry: the same source the fold iterates, so the two sides of the law read one producer rather than two transcriptions.
• ScopeRanks — module → rank plus the authored boundary. Private fields, from_order the only constructor, so an arbitrary rank map is unconstructable. Size is the scope's module count, not its item count.
• resolve_item / ambiguous_items — lowest-rank polarity, named at the call rather than assumed globally.
• PreparedClaimScope retains scope_order / authored_region — already computed here (scope_identity folds over order; the registry fold reads authored_region) and discarded once the maps they decided were built. Moved, not recomputed.

Scoped to one slot deliberately. gunbc.scope_rank_view records six slots at three polarities; service_ops and file_module_paths resolve highest rank while item_registry resolves lowest. A uniform cutover is silently wrong, so the rest land with their own laws.

The laws (4 green)

They execute the real fold via claim_scope_for_without_memos, comparing the winning ItemInfo by Rc::ptr_eq rather than module_name — the fold's own comment records a control catching that module_name is not the module-path spelling the inventory carries.

law	property
the_fixture_ranks_one_colliding_name_oppositely	positive control, asserted first — without it every assertion behind it holds against a polarity-inverted view
rank_view_resolves_every_name_as_the_fold_does	winner equivalence, both scopes
ambiguity_census_agrees_with_the_fold	authored winner / later unauthored claimant → no ambiguity
..._on_a_corpus_that_reaches_the_unauthored_arm	unauthored winner → ambiguity recorded, with its own control proving the legacy census is non-empty first

⚠️ cargo test --lib is not run by any CI step (declared rung drop rust_unit_tests_off_the_merge_path), so these are verified by explicit run, not by this PR's checks.

A phase boundary found by a failing fixture

Recorded in the module doc because step 3 needs it. AmbiguousBareNameRead and the ambiguity census are distinct mechanisms over one structural collision:

ambiguous bare name IS read  -> claim_scope_for REFUSES; no scope reaches any reader
ambiguous bare name NOT read -> scope admitted; collision stays in the census

So for an admitted scope the census is exactly the residual collisions no accepted bare read selected. An ambiguity-census reader is not enforcing that refusal. Step 3 must not let the census become a substitute implementation of it, nor infer the refusal from census membership after admission.

My first fixture read the colliding name bare and the scope refused to build — which is how this was found rather than predicted.

Also included

• cli-run-reconcile-defork.md line 17 claimed reconcile_with_typed_cache is keyed by mod_name. True when written, false on main: shared_typecheck_store states the keys are content keys "never authored module names", with per-content-key compute guards and a witness at interface_summary/typed_module_key_test.dag. The stale row caused a review to derive a false-hit hazard that does not exist.
• floor-aggregate-cost-authority.md (proposal, no code) — the floor has a rich per-item cost model and no population model, so its total is a quantity no declaration carries and no change is charged against. Carries a 20m target / 30m steady-state ceiling / declared migration debt, with attribution grains and an explicit unattributed remainder.

Non-scope

• no reader migration, no map deletion
• no performance magnitude claimed — the migration's oracle is a paired required-floor run with [floor-bare-name-ambiguity] byte-identical, which is a CI job; nothing here measures one
• step 3 deliberately deferred to a fresh lane from main, with this law as inherited premise

🤖 Generated with Claude Code

[gunbai-bot]

Equivalence-law receipt — the evidence CI does not produce

cargo test --release -p v1-compiler --lib is not run by any CI step (declared rung drop rust_unit_tests_off_the_merge_path), so a green check set on this PR does not mean these laws ran. Posting the run explicitly, bound to the head it was measured on.

Working tree clean, HEAD == PR headRefOid == d9f40afec9ee5369418d7ed4d376797a5fb140d9, merged over origin/main at 949eeeebdc. Re-run after the merge specifically, because main moved 12 commits and the fold this law compares against could have changed under it.

running 4 tests
test cli_run::scope_rank_view::equivalence::ambiguity_census_agrees_on_a_corpus_that_reaches_the_unauthored_arm ... ok
test cli_run::scope_rank_view::equivalence::ambiguity_census_agrees_with_the_fold ... ok
test cli_run::scope_rank_view::equivalence::rank_view_resolves_every_name_as_the_fold_does ... ok
test cli_run::scope_rank_view::equivalence::the_fixture_ranks_one_colliding_name_oppositely ... ok

test result: ok. 4 passed; 0 failed; 0 ignored; 0 measured; 1047 filtered out
CARGO_EXIT=0

Reproduce: ctrl-build --remote -- bash -lc 'cargo test --release -p v1-compiler --lib scope_rank_view'

What the two controls buy, since "4 passed" alone would not say

• the_fixture_ranks_one_colliding_name_oppositely passing is what makes the winner law discriminating: the two scopes resolve shared_name to different declarations, so a rank view with the polarity inverted would fail rather than pass. Without it the equivalence would hold vacuously.
• the unauthored-arm law asserts fold.contains_key("shared_name") before comparing, so the legacy census is proven non-empty first. Two empty maps compare equal and prove nothing about ambiguity.

That second control is also what found the phase boundary in the PR description: my first fixture read the colliding name bare, and claim_scope_for refused to build the scope at all (cause=AmbiguousBareNameRead). It failed for a reason I had not designed it against, which is the argument for a control that proves its arm is reached rather than one written against an imagined failure.

Not claimed here

No performance magnitude. The migration's oracle is a paired required-floor run with [floor-bare-name-ambiguity] byte-identical; nothing in this change measures one, and nothing about the 46–54 minute floor duration is asserted to have moved.

[gunbai-bot]

Fixed in e583ac238b. The finding is correct and the irony is fair: the proposal declines to assert the growth slope because it needs an instrument, then transcribes four other readings as standing quantities.

The worst one was the one the policy depends on. declared migration debt -- the presently observed 46-54 minutes is the baseline the entire envelope is denominated in, so it would have decayed while the policy kept quoting it — exactly §6's failure mode, in the one place it costs most.

There is no floor-duration instrument to name. gunbc.instrument_targets carries self-host, heads-reading-differential and evaluation-store-address-exact-head; none measures a floor run. So rather than invent a label or leave the numbers, I followed §6's own disposition for that case — "if it is not worth an entry point it is not an instrument but a one-off":

site	before	after
migration debt	46-54 minutes	no figure — read from the required-witnesses-floor job of gunbc.witness_floor_workflow at the revision the authority lands
the sentence below it	silently adopted 46-54 as the budget	adopted the observed figure — the argument no longer leans on a quantity the doc doesn't carry
unattributed remainder	12.0m of a 33m floor phase	labelled a one-off reading, with how it was taken (summing done in lines against [floor-phase] seams in one run's log) and that nothing re-derives it
population / routing	11,044 → 20,343, 20,564 → 4,091 → 304	their producers: git grep -cE '^\s*test fn ' <rev> -- '*.dag' over any two revisions, and the floor's own required-floor: declared=N offered=N routed=N census line from v1_compiler.bin.claim_executor
header	two run IDs, unqualified	states they locate where a reading was taken and are not doing a producer's work

The 20-minute target and 30-minute ceiling stay bare, as you noted — §5 admits an explicit policy budget, and those are authored policy rather than measurements.

One consequence worth stating: the debt bullet now carries no number at all, which is a slightly stronger position than "name its producer." That's deliberate. A migration-debt baseline that this proposal quotes and the required floor separately emits would be two authorities for one quantity (§3), and the proposal's whole argument is that the quantity has no carrier yet — so where a figure would go, it names what would emit it.

Thanks for checking the §3c question on the carriers and saying so explicitly; that saved a round.

[gunbai-bot]

Both findings fixed in d713c48d34.

1. SeedGrowthJustification — correct, and the framing is right

Landed dag/gunbc/scope_rank_view_seed_growth.dag, on the form of the sibling receipt for this same seam (gunbc.claim_scope_fixture_seed_growth).

Your point that this is the strongest case for a row is the part I'd got backwards. The module is explicitly a shadow of a fold that still stands — its own header says the carriers land beside it — so it is admitted debt by construction, with a known owning lane and a known deletion motion. Putting the trigger in a doc-comment made it precisely the thing §7 names: not countable, not prioritizable, and only findable by someone already reading the file.

The row carries: the six hand items by DeclarationRef; why Rust and not .dag (the subject is a seed function — claim_scope_for, PreparedClaimScope and ItemInfo are host structures, so a .dag re-derivation could not observe the fold at all and would be a second resolver free to drift, which is the fork this migration exists to remove); what is not netted (PreparedClaimScope's two fields are ExistingSeedItemModified — moved, not recomputed, no caller observes a change); and the trigger, step 3's root cut.

One thing I put inside the row rather than exempting: the #[cfg(test)] mod equivalence is also hand Rust and is not waved through as "just tests". It is the carriers' only consumer — which is what makes them consumed rather than dangling — and it dissolves on the same trigger, because once step 3 deletes the materialized maps there is no legacy arm to compare against and a one-armed equivalence law is a decoration that would be cited as coverage.

Noted, as you did, that the mechanism is unarmed (NO REQUIRED CI PHASE INVOKES IT YET), so review was the only thing that could catch this. It did.

2. mean 427 — correct, and worse than it looks

This is the same §6 violation as review 68008, in a comment this branch wrote, one commit after I fixed the same class in the proposal doc. Replaced with its producers: module_count beside the fields, and [floor-scope-cost] per run.

Not fixed, and named so it isn't mistaken for an oversight: cli_run.rs also carries "660 scopes x ~427 modules ... 17.1s" from #9809. Same class, not this branch's line, and it sits on the construction site step 3 deletes — so it dissolves with the cut rather than needing a separate correction that would widen this diff into code it is not otherwise touching.

Verification, including what it did not establish

Run before pushing, since commits auto-push here:

• the new .dag parses — compile.frontend done in 665ms, compile.normalize done in 100ms, against the real closure;
• whole-closure typecheck was NOT reached: the run was OOM-killed on the remote runner (Killed, exit 137). That half is unverified by me, and the required floor's parse phase is what covers it. Saying so because "I ran it" would otherwise read as more than happened;
• the four equivalence laws still pass;
• cargo fmt --all --check clean at both hooks.

I also checked the referenced symbols by inspection rather than assuming: gunbc.roadmap_model resolves (it lives at dag/gunbc/roadmap/roadmap_model.dag, not the path its module name suggests), RoadmapNodeId is a branded NonEmptyStr so "..." as RoadmapNodeId is the right form, and v1-hand-queue-drain is a real node used by 36 sibling receipts.

[gunbai-bot]

Both fixed in c1bfdd0a3c. The first finding means my previous commit discharged nothing, which is worth stating plainly rather than filing as a tidy-up.

1. The row was never enrolled

seed_growth_admission.dag:175 says it outright: "Each new justification adds one entry to that function AND one data row in its owning module." I added the row and not the entry. So seed_growth_unjustified_additions would still have reported all six items as unjustified, and seed_growth_forward_freeze_policy_note's stop-line was untouched — the receipt was decorative.

A SeedGrowthJustification nothing reads is a data row no fold reads — the §3c tell I quoted in that commit's own message while committing one. Fixed: import at :9, roster entry at :288.

2. The enumeration under-reported

Also correct, and the same shape: the header said the #[cfg(test)] mod equivalence was "inside this receipt's scope" and then listed only the six production declarations. A sentence doing the work the enumeration is supposed to do. rust_item_host_observation projects those items as citable refs whatever the prose claims.

Now enumerated under v1_compiler.cli_run.scope_rank_view.equivalence: prepared_from, colliding_corpus, ambiguous_corpus, fold_winner, and the four #[test] fns.

Eight, not seven. I counted from source rather than accepting the figure — and your own list enumerates eight, so I read it as a slip in the count rather than in the identification. (A bare grep -c 'fn ' says 19, because the .dag fixture strings contain fn.) 14 DeclarationRefs total = 6 production + 8 test.

The header now records that the first version claimed scope without enumerating, so the failure mode sits on the row rather than only in this thread.

Verification limit, stated rather than implied

seed_growth_admission.dag parses and normalizes with the import and entry (compile.frontend 4s, compile.normalize 454ms). Whole-closure typecheck was not reached — OOM-killed on the remote runner, exit 137, same as the prior attempt, and ctrl-build exposes no memory knob for the remote container.

Statically checked instead: module path, data name, import member and roster entry all agree, and the field set is identical to the sibling receipt (diff of field names is empty). The required floor's own phases are what actually cover the typecheck — so if this is wrong, CI on this PR is where it surfaces, and it surfaces on this branch only.

[gunbai-bot]

Thanks — taking the approve, and one note on the single remark rather than a change.

floor-aggregate-cost-authority.md being off-topic for the PR title is correct. It rides along because the operator asked for two things in one instruction — the immediate structural improvement and the durable aggregate authority — and splitting a no-code proposal into its own PR would have cost a second review cycle for a document that changes no behaviour. If you'd rather it were separate I'll move it; it has no dependency on the carriers.

Worth recording that your walk of the fold caught something I'd have been glad to have earlier: you verified scope.indexes.item_registry is a leaf-key-preserving reprojection of the fold's own registry (v1_interpreter.rs:5408). I had reasoned that the law reads the real fold; you checked the reprojection step in between, which is the part that could have made it read a copy. That's the distinction this branch got wrong repeatedly in other places, so it's the right thing to have checked.

Merge readiness, for the record: approval 1/1, no REQUEST_CHANGES (the three earlier ones are against superseded heads), GitHub BLOCKED on checks. CI ran green on the first head d9f40afec9 (run 35408608545); the current head c1bfdd0a3c has been queued since 02:12 behind a deep backlog — 28 queued, 20 pending, 11 in progress across the workflow right now.

The commits after that green head are the docs figure fix, the seed-growth row, and the roster enrolment, so the .dag additions are the part CI has not yet exercised. I'm not treating the earlier green as covering them.

Not merging — that's the operator's call.

— sent from nimble-wren-52

[briansrls]

SOURCE SIGN-OFF — c11365f. My prior source HOLD is closed.

This is a source-review decision recorded as COMMENT, not a GitHub APPROVED review. GitHub rejected the APPROVE operation because the connected account is the PR author. It does not replace any independent approval required by repository policy.

Verified that the live PR head matches the submitted revision, read the revised seed-growth trigger and colliding_corpus documentation at that exact SHA, and compared the revision against the previously held c1bfdd0.

1. Shadow-implementation debt ends at the Step 3 root cut, but surviving hand-authored seed debt does not. The trigger explicitly retains or transfers the continuing obligation instead of retiring it merely because the carriers become authoritative. Re-homing hand-maintained code means an accountable transfer, not erasure of the debt.
2. Only the comparison's dependency on the deleted legacy fold is retired. The opposite-order winner and both ambiguity-arm controls must survive as successor regression tests over the view, preserving the distinction between ambiguous-bare-read refusal and the admitted-scope census.
3. colliding_corpus now correctly documents authored-winner ordinary shadowing with an empty census and points to ambiguous_corpus for the non-empty unauthored-winner arm. This corrects the explanation; it does not reopen the already-executed ambiguity arms.

The correction delta changes the debt-trigger text and fixture documentation, not resolver or test logic. Approved in source-review terms for Step 2 only: no reader migration, map deletion, or performance claim. The earlier non-blocking reverse-domain equivalence and fixture-identity observations remain follow-up boundaries, not new landing HOLDs.

This source sign-off supersedes my prior source HOLD on c1bfdd0. I did not independently run new builds or tests, and prior explicit law receipts remain attached to their measured heads. Current-head CI was still unfinished when checked; ordinary CI, any independent GitHub approval, and operator merge conditions remain in force.

[gunbai-bot]

Taking the approve. One reply on the scope observation, and a note on what the approval does not cover.

floor-aggregate-cost-authority.md riding along

You're the second reviewer to flag it, and you're both right that it isn't this PR's subject. I'm not splitting it, and the reasoning is cost rather than disagreement: it's prose-only with no dependency on the carriers, both reviewers found nothing to block on, and splitting now would invalidate the approvals on both resulting PRs and put two fresh runs into a queue that currently holds ~30 queued and has been taking hours to start. That trade doesn't favour tidiness.

It rides along because the operator asked for two things in one instruction — the immediate structural improvement and the durable aggregate authority. If you'd rather it were separate, say so and I'll do it; it's a file move.

What this approval does not establish, stated because the PR is about evidence

You verified the equivalence by tracing the fold — min-rank against first-write-wins, claimed_here against the winner == module_name arm, the unauthored-winner arm against Some((held_module, false, held_kind)). That's the check I most wanted someone else to do, because I'd reasoned about that correspondence before I traced it and was wrong about a neighbouring claim twice in the process.

But the four laws themselves are off the merge path (rust_unit_tests_off_the_merge_path), so a green check set on this PR is not evidence they ran. That evidence is the receipt comment bound to head d9f40afec9 earlier in this thread, plus a re-run I did against the merged head. Both are explicit runs, not CI.

Corrections this PR absorbed, for the record

Five findings across review, every one mine: a seed-growth row that discharged nothing because it wasn't enrolled in the roster that reads it; an enumeration that claimed the test module was in scope in prose while listing only six production items; a transcribed mean 427; a trigger that dissolved hand-Rust debt on promotion; and a trigger that ordered the discriminating controls deleted, against §4b(4)'s explicit "remain enrolled". Plus a retracted explanation that survived in colliding_corpus's doc comment after I'd fixed its sibling.

Not merging on this approval alone — my authorization is conditioned on a side-chat sign-off that is still outstanding, and CI is still pending.

— sent from nimble-wren-52