shell→dag bucket A: last shell.Exec off host_runner_memory_cap_verify; meta-exec roster 3→0 + per-PR emptiness wall

[gunbai-bot]

shell→dag bucket A. Roster 3 → 0, every behavioral change green-by-execution with a discriminating RED.

1. host_runner_memory_cap_verify — last shell.Exec off the intent layer

The brief said "2 live shell.Exec" — there was 1 (the memory-property reads had already gone typed via systemctl_show_read). The remaining one was probed_at:

• shell.Exec.Run(retained_runtime("date -Iseconds")) → clock_now_probed_at() (gunbc.clock_read → extdeps.clock Clock.Now) — the same single authority host_converge_slice1 already uses, so this removes a §3 fork rather than just a shell call.
• Deleted with it: the extdeps.shell import, the retained_shell_script bridge, and host_runner_memory_cap_verify_transport_script_scaffold (its medium-as-string dissolution trigger no longer has a subject).
• The refusal decision is factored into runner_memory_cap_verify_result_from_live_read(host, read: RunnerUnitMemoryLiveRead?), so the read-absent arm is executable hermetically. runner_memory_cap_verify_run keeps the knobs-absent guard before the live read, so no read-only op fires on a host with no knobs.

RED control (by execution): perturbing the absent arm to fabricate an empty read and report it Observed — the exact §5 widen — turns srv3_runner_memory_cap_plan_verify_holds FAIL; restored → PASS. Paired witnesses: none → Refused with the located reason, Present → Observed.

2. SetHostnameCas → os.Hostname.Set — already landed on main (#7194)

Verified, not assumed: host_effect_realize.dag's arm calls gunbc.hostname_set hostname_set_cas, whose hostname_set_local is os.Hostname.Set(desired:); SSH goes through typed_argv_exec_over_ssh; the CAS read reuses os.Hostname.ReadShort. host_effect_set_hostname_cas_script does not exist anywhere in tree. No code change was needed — recorded as DONE in the census instead. (Consequently no contact with host_effect_realize.dag, so no overlap with #7237.)

3. Roster 3 → 0

Both stale rows verified at 0 live shell.Exec before deletion:

• dag/gunbc/tools/review.dag — imports only extdeps.git.
• dag/gunbc/ci_deploy_target_host.dag — imports extdeps.shell for shell.Env.Get, which is not the confined extdeps.shell.exec (non_exec_import_is_not_leak_holds is the standing receipt).
• dag/gunbc/host_runner_memory_cap_verify.dag — the genuine remainder, dissolved by item 1.

rostered_consumer_import_is_not_leak_holds was re-parameterized onto a synthetic roster: spelled against the canonical roster it would have passed for the wrong reason (no row to exempt) and silently stopped discriminating. It now asserts both directions, plus a new empty_canonical_roster_grants_no_exception_holds.

4. The dark-lane fix — measured, then designed

The diagnosis is confirmed: meta_exec_roster_sound_live existed but ran on no per-PR cadence; the only enrolled roster RED was synthetic (hand-written fact rows, blind to the live roster). That is why two stale rows survived merges.

The literal fix does not fit, and the measurement is part of the receipt: the live receipt evaluates in 13470ms cold over meta_exec_consumer_scan_roots, and still 11485ms over dag/gunbc alone, against a 5s fast-lane budget — next to an enrolled sibling costing 2ms. The cost is intrinsic to layer_import_facts_live over a real tree, so no narrower root rescues it. (Behind an already-warmed scan it reports 1852ms — borrowed warmth, not a cost this row may declare.)

What runs per-PR instead is stronger than soundness and needs no scan (§5 construction over validation): a stale row is only possible because the roster is a hand-written second representation of a fact the tree already carries. stale_count is bounded above by roster length, so length 0 proves soundness outright. meta_exec_roster_shrunk_to_empty_holds walls that state, costs 0ms, and reds by name in the same PR that re-adds a row — precisely the event that went unnoticed before.

The live receipt stays as a backstop in the long lane, now with a non-degeneracy control: over a clean tree a live scan is true either because nothing is stale or because the walk read nothing (⊤-as-answer vs ⊤-as-ignorance), and leak-candidate paths are legitimately empty, so the control asserts the underlying fact set is non-empty.

Named residue, not papered over: that long lane is still dark (not roster-enrolled). Dissolve-on is a falsifier batch admitting live-tree lens receipts; batch 6 exists but is declared for SubstrateInputsOnly fixture-shaped rows, so enrolling there is a lane-owner call, not mine to take silently.

5. Census true-up

§4.A/§4.C rows marked DONE for the hostname and date -Iseconds clusters; a 2026-07-25 ledger true-up block ahead of the stale 07-22 snapshot. Every claimed PR verified against origin/main — which corrected a line I had drafted from the brief: §5.A is COMPLETE, not partially remaining (ListUnits, Status, os.Id.Uid all landed on #7194 and are cited at their post-#7231 homes). §5.E is marked LANDED (#7184), so the wall-first pause on §5.B is discharged.

Receipts

• gunbc compile --target dag — 0 blocking errors (2576 pre-existing advisories).
• All fast-lane witnesses PASS post-merge; commit_witness_claim_roster_holds PASS (every enrolled (entry, check_fn) pair resolves — the Layering-imports gate: repoint fact producer onto reference-derived edges (Phase 1) #7060 stale-roster class).
• Long-lane live receipts PASS incl. the planted-stale RED against real live leak paths.
• ci.yml: witness roster is not embedded in any generated artifact (0 hits) — no drift. gunbc ci fails identically on baseline with my changes stashed, i.e. a pre-existing local env issue, not this PR.
• Main integrated by merge commit (Operator's pass flips: row column gutter splits to space-8; h-row and ellipsis deferral signed #7239); no conflicts.

🤖 Generated with Claude Code