D13 cut (c) final-base census: restatement uses rows deleted, the rest retained at row identity

[gunbai-bot]

Follow-up to #11993, which landed at 885ad19 before its last review conditions were done. This PR discharges them.

The census (receipt; the counts live here, not in the tree)

• Base: taken at main 4446f2e990f, the tip of the range recorded in gunbc.plans.demand_restatement_follow_up. The rows were measured with the seed resolver built from the merged tree at be3a2f28d42. The rows present at d759da1c50e were first measured with that base's resolver. The be3a2f28d42..4446f2e990f delta changes only v2 .dag compiler sources, not the seed the census reads.
• Grain: one row identity is USES-0's (module, declaration, alias, type).
• Procedure: every authored uses clause is enumerated. Every ordinary fn that carries one is resolved, and ItemInfo.service_names is read.

	clauses	identities
population	201	227
nonempty derived demand: deleted	174	198
empty derived demand (a deletion would flip effectful → pure)	0	0
retained (= the record's two lists)	27	29

The 29 retained identities:

• 8 are on pattern declarations, under CriterionDoesNotRangeOverPatterns.
• 2 are in gunbc.auth.patterns, which refuses on a pre-existing type error. They carry ModuleResolutionBlocked.
• 2 are in test.probe.census_app_acquisition_forged_probe, which refuses by design. They carry ProbeLeavesCorpus.
• 17 are in test.manual.runner_microvm_lifecycle_wet_receipt. Each is measured deletable. But editing that module plans ten wet witnesses onto the hermetic route, which has no extdeps.linux.cgroup_v2 ReadInterfaceFile arm: route gap, floor red. They carry EditedWitnessHasNoHermeticRoute, whose trigger is: ReadInterfaceFile gains a mock_response.

Other notes:

• v41_runtime_image_converge: gunbc.spark.v41_runtime_image_converge refused at the first census base and resolves at this one, so its rows were measured and deleted.
• Imports: std.resources imports that the deletions left dead are removed.
• Re-resolved: every changed module resolves.
• Counts: per DESIGN §6 and review 70493, the counts are not transcribed into the module annotation. The resolver has no entry point in the tree, so a figure there could not be re-derived. The tree-checkable fact is stated instead: every authored uses row left is a retained identity or a new arrival.

Also from the #11993 review conditions

• Duplicate import: the duplicate fabric_purpose_handover_registration_unobserved_stall import in gunbc.guarantee_stall.roster is removed. The merge with The 2026-09-23 floor sizing receipt: uncensored at the 26 GiB row, the microVM shape resolves, the fit stall retires #12117, which retired runner_microvm_floor_fit_stall, is resolved.
• DER constructed bit: egress-encoding-0-cbor-der-landing defect (4) requires the DER constructed bit to refuse in both directions, with a control for each.

🤖 Generated with Claude Code

[briansrls]

HOLD at exact head ab51438e9b3796f7651839a0fcfd4c65ddaa0e91. The deletion set, duplicate-import cleanup, and two-direction DER obligation look structurally aligned, but the committed census authority has two grain defects that CI cannot repair.

1. The 181 / 167 / 14 arithmetic is clause-grain while the PR and carrier call it row-identity grain. docs/plans/uses-occurrence-census.md defines one authored row by (module file, declaration, alias, type). The retained carrier in this head contains 15 DemandRestatementRetainedRow identities: seven ordinary-function entries plus eight pattern entries. The forged probe alone contributes two distinct identities (net: Network and fs: Filesystem), even though they share one syntactic uses clause. Yet the title, body, commit, and demand_restatement_follow_up say 14 retained rows and reconcile 181 = 167 + 14. Several deleted clauses also bind two aliases (net, fs or net, clock), so merely changing 14 to 15 would still leave 167 mislabeled as an identity-row count. Recompute and record the population at one grain: preferably exact total/deleted/retained identity counts, with retained = the roster's derived count; otherwise explicitly call 181/167/14 syntactic clause/declaration counts and separately reconcile the identity population. The current text cannot be true under USES-0's own identity definition.

2. ModuleIsARefusalProbe is a disposition, not the RetainedRowTrigger it inhabits. Its renderer literally says trigger: none while the probe stands, while the carrier immediately above says every retained row carries the trigger true for it. Model the intentional-refusal reason separately or make the arm name/render the actual lifecycle condition—e.g. the probe/declaration leaves the corpus (or a future criterion can inspect its demand without requiring the refusal probe to resolve). A field named trigger must not carry “no trigger.”

At review time GitHub had attached no check runs to this SHA. Green CI is still required after these authority repairs, but it would not discharge either source finding.

[briansrls]

REQUEST_CHANGES at exact head 3a746c41f6deb8a65ae641b218e17ae82b56d6f8.

The two findings from ab51438 are discharged:

• the census now distinguishes 194 clauses from 220 USES-0 identities and reconciles 208 deleted + 12 retained;
• ProbeLeavesCorpus names the event that ends the forged-probe retention, rather than calling the current refusal-probe disposition a trigger;
• v41_runtime_image_converge is correctly reclassified after it became resolvable, and its three rows are deleted rather than retained.

Two remaining findings:

1. The durable authority still names the wrong evidence base. gunbc.roadmap_authority says every authored row was measured “at the #11993 landing.” #11993 landed at 4716b4c9954; this census is explicitly at 834148a3177. Correct the EFFECTS-1 boundary to name the actual census base/range. In the same repair, rewrite the stale header in gunbc.plans.demand_restatement_follow_up: it still says the rows rostered below “arrived” over the range after the measured population was fixed. The unmeasured-arrival roster is gone, and the surviving rows are retained criterion exceptions, not a population that all arrived over that range.

2. 834148a3177 is no longer the intended landing base, and main changed the measurement machinery itself. Current main is d759da1c50e8aa8c16346bf6f759fd5857eb40f9; #12116 changed resolve/census from first-refusal projection to an occurrence-complete failure-chain population. This PR’s deletion criterion is explicitly obtained by resolving modules and reading ItemInfo.service_names, so the exact head does not yet establish the census under the resolver that will be on the landing tree. Merge the intended final base and rerun the census, or provide and commit an exact delta proof that the newer resolver and source delta leave every USES-0 identity/disposition unchanged. Update the recorded base/range and projections accordingly.

CI cannot discharge either authority/base issue. Return the frozen successor head after that remeasurement or delta proof; exact-head green gates are then the remaining condition.

[gunbai-bot]

Re review 70493. Fixed in 5ed63ea.

• Title and body: the title is no longer stale, and the body carries the current receipt: 220 identities, 191 deleted, 29 retained.
• Annotation: the transcribed counts are removed from gunbc.plans.demand_restatement_follow_up. The retained population is read off its lists.
• Why no entry point: I did not add one for the census. The resolver I used is a scratch reader over v1_compiler::cli_run::resolve_entry_graph. Committing it would grow the hand-Rust seed only to re-derive a one-time receipt. So the counts are the change's receipt, in the PR body and commit messages, and the module states only what the tree makes checkable.

— sent from fierce-seal-607

[gunbai-bot]

Re review 70525's risk note. Some functions lose uses fs: Filesystem while still calling Filesystem.Read/Write directly. Two examples are decode_entry_for_cell and confirm_persisted in gunbc.runner_microvm_cell_readiness_store. Verified against the code:

• Main had the rows: both functions carried uses fs: Filesystem on main, and this PR deletes them.
• Derived demand: the census's resolver reads Filesystem in both functions' ItemInfo.service_names from the operation references. That is D13's derived demand, the criterion under which cut (c) was ruled. Primitive-egress wind-down (split A): OpenBMC Optional repairs, roadmap authority, main repairs, EFFECTS-1 cut (c) #11993's landed cut deleted rows of this same shape.
• Admitted today: every changed module still resolves on this head, and the floor on 5ed63ea was FloorClean. Its only red was the two stale projections, since regenerated in 78a51c4. So the typecheck that lands with this PR admits the direct operation without an authored row.

Collision to record, not a defect here: open #12047 adds ResourceRequirementUnestablished at the direct-call join. That wall compares a callee's authored uses against the caller's. After D13 cut (c), the authored rows are exactly what is being deleted as restatements. So whichever of #12047 and this PR lands second must reconcile: #12047's wall would need to read derived demand, or treat a callee with no authored row as requiring nothing.

— sent from fierce-seal-607

[briansrls]

REQUEST_CHANGES at exact head 78a51c4251e99cc07bbade92ac95be5e0cd3176d.

The prior findings are discharged: the census is re-measured at d759da1c50e with the post-#12116 resolver; the interval/header now describe the actual evidence base and retained exceptions; the merge with 3ba7f6c is resolved; ProbeLeavesCorpus is a real trigger; counts stay in the PR receipt; and exact-head compiler, clippy, floor, emit-build, and witnesses are green.

One authority inconsistency remains. The retained carrier correctly distinguishes 17 test.manual.runner_microvm_lifecycle_wet_receipt identities that are measured, have nonempty derived demand, and are deletable by the D13 criterion, but whose deletion cannot yet land because editing the module sends ten wet witnesses to a hermetic route with no ReadInterfaceFile realization. However:

• gunbc.plans.demand_engine_program still says the final census “deleted each one whose derived demand was nonempty” and then says “What remains are the rows the criterion cannot type,” even while its same sentence includes the measured-deletable wet witnesses.
• The EFFECTS-1 roadmap boundary likewise says each nonempty-demand row was deleted and only rows the criterion cannot type were retained. Its “What remains open” also omits the EditedWitnessHasNoHermeticRoute population, which E2 does not retire.

Those statements erase the exact exception the retained-row carrier now models. Rewrite both authorities to partition the survivors without transcribing counts: (a) criterion-untyped identities retained with their triggers; and (b) nonempty, measured-deletable identities explicitly retained under EditedWitnessHasNoHermeticRoute until extdeps.linux.cgroup_v2.ReadInterfaceFile gains mock_response. State that all other nonempty-demand identities were deleted. Keep the numeric receipt in the PR body, regenerate the projections, and return the successor exact head.

The open #12047 collision is real but not a defect in this PR. After this lands, #12047 must derive call requirements from derived demand rather than treating absence of an authored restatement as absence of a requirement.

[briansrls]

REQUEST_CHANGES at exact head 8a2bce0e333e0c1f5e2165e4167b4272bb087c74.

The prior projection finding is substantially repaired: demand_engine_program and the EFFECTS-1 boundary now distinguish criterion-untyped rows from the measured-deletable EditedWitnessHasNoHermeticRoute population, and EFFECTS-1 correctly says E2 does not retire the route-blocked rows.

Two findings remain:

1. The recorded “final census base” is already behind the tree this PR would merge into, and the delta contains new authored uses rows. This head records and is based through be3a2f28d42, while current main is 4446f2e990ff2042fd3a5b8df3c3abddec6f2f47, four commits ahead. This is not a row-free delta: new gunbc.runner_microvm_network_observe alone carries at least five new USES-0 identities (admin_read_outcome, read_privileged_over_admin_edge, runner_microvm_network_observe_wet, observe_bound_host_wet, and observe_admitted_host_wet, each uses net: Network). Nothing walls those arrivals out. Merge the intended landing base, run the census over the whole four-commit delta, delete/classify the new identities under the same criterion, update the receipt and range tip, regenerate, and return the successor head. A merge-queue tree containing those rows would otherwise falsify this PR’s “final-base census” claim on arrival.

2. The census module’s opening description still collapses the two retained classes. It says the lists are “the identities the criterion cannot type at that base,” but the same lists intentionally contain 17 identities that the criterion did type as deletable and that are retained only because editing the witness module has no hermetic route. The later paragraph states the correct two-class model. Make the opening sentence agree: retained exceptions are either criterion-untyped identities or measured-deletable identities blocked by EditedWitnessHasNoHermeticRoute.

At review time compiler, clippy, and emit-build were green; floor was still running and witnesses had not yet appeared. Those final gates remain required after the source/base repair.

Superseded by exact-head review of 14ba4a7; the clause/identity grain and trigger findings were repaired.

[briansrls]

APPROVE-MERGE at exact head 14ba4a741f089297d3b856036f332ebbb604d421.

All prior findings are discharged. The census authority now partitions retained exceptions correctly; the recorded range tip is 4446f2e990f; the five gunbc.runner_microvm_network_observe identities introduced after the previous base are measured nonempty and deleted; the receipt reconciles 227 identities as 198 deleted plus 29 retained; and the duplicate-import and bidirectional DER obligations remain repaired.

Exact-head compiler, clippy, floor, emit-build, and witnesses are green. The current-main delta after 4446f2e consists of two row-free commits and does not change the seed resolver used by this census, so it does not reopen the population. Queue this PR; the merge-group gates remain the final integration check.

No remaining findings.