Say what the staging arm establishes, instead of a construction law the type does not have

[gunbai-bot]

Comment-only. No behaviour change, no new declarations, no witness changes — every changed line is a comment line (git diff --numstat totals 57, all //). So it needs no re-take of evidence.

Why

#11677 landed carrying three sentences stronger than its own source. The side-chat review that parked that PR named them; the PR was enqueued and merged before the correction could be pushed (its branch was frozen by the merge queue at the time), so the correction lands here.

The hazard is not runtime behaviour — nothing in production selects this code. It is that the prose asserts a structural law the types do not have, stated strongly enough that a later reader would treat it as the already-solved boundary and build on it without reopening the argument.

Verify in one read, on main before this PR:

• dag/gunbc/runner/runner_attempt_launch.dag — type AttemptLaunchPlan has no sole_constructor (grep -c 'type AttemptLaunchPlan sole_constructor' → 0), while the comment above it said no admitted credential means "no device AND no VMM process — the two cannot come apart".
• same file — "the jailer command is reachable only inside one [receipt] — so a caller cannot mint 'staging passed'…", while the same command is a plain readable field on the unsealed LaunchAuthorized.

The three corrections

1. runner_attempt_launch, the plan arm. Now says what the arm actually establishes: a plan built by this planner carries a staging plan and a jailer together or neither. It states plainly that the type is not sole_constructor, that LaunchAuthorized is assemblable outside the module, and that its jailer field is readable by any holder — so the arm does not establish that the value came from admit_jit_credential, that staging ran, that the readbacks happened, or that the jailer cannot be obtained first. The reported rung (Mitigatable) was already honest; the prose was not.
2. runner_attempt_launch, the sealed receipt. Sealing AttemptStagingReceipt is real, but it proves less than claimed, twice: it withholds nothing while the same jailer command sits on the unsealed plan, and the gate accepts caller-authored positive outcomes — a JitDeviceStaged value is constructible without stage_jit_device ever running, and this module's own witnesses construct one to drive the foreign-device case. So the receipt proves the gate was called with positive-shaped arguments, not that the host effects and their readbacks occurred.
3. github_effect_perform, the commit-ambiguous arm. The classification is correct and stays — reporting an unanswered mutation POST as a refusal would assert a fact nobody observed. What is retracted is the promise beside it: JitMintStepNotSucceeded carries only the step and the performance, dropping the attempt, runner name, dispatch and organization, so it does not give an operator what reconciling a possibly-created registration needs.

Also recorded

The reframed guarantee, because it is what a future implementer needs and it is not obvious: device-without-launch is not the state that must be impossible — a staged device with no VMM is safe provided teardown removes it. The dangerous state is a VMM launched without an effect-bound, read-back credential device for this attempt. Closing that means withholding the raw jailer capability until after effect-bound staging, the staging realization itself constructing the executable jailer from its own observations. That is a substantive redesign and is explicitly not attempted here.

🤖 Generated with Claude Code

[gunbai-bot]

Pushed the four substitutions from the review as 69ce2d88cba, then composed current main (f05e170a330) at f0f0afa39a3 — conflict-free.

The finding worth recording above the list: a PR whose entire purpose was removing overstated commentary introduced three smaller overstatements of its own. That is the repair-is-the-least-audited-code class.

1. 'this verdict read' attributed I/O the gate never performs. attempt_staging_verdict RECEIVES JitDeviceStagingOutcome and WorkspaceStagingObservation as caller-supplied values; sealing the receipt establishes nothing about where they came from. Now: the receipt carries the planned JIT-device path and workspace path the supplied outcomes were judged against.
2. 'it withholds nothing' was broader than the defect. Sealing DOES withhold direct construction of AttemptStagingReceipt. What it does not withhold is the jailer capability — which is the actual hole, and is now what the sentence says.
3. The reconciliation paragraph swapped one overclaim for two. Something does consume perform_organization_jit_mint (a witness calls it); what is absent is a PRODUCTION consumer. And attempt identity alone is not the complete reconciliation subject — it derives the runner name but does not identify the ORGANIZATION a possibly-created registration must be queried in. The arm now names the dispatch, or an equivalent sealed carrier holding at least the attempt, the organization and the derived runner name.
4. Refinement: 'Closing it means withholding the raw jailer capability' asserted the only possible construction. It is now ONE mechanically preventing repair, with the redesign caveat kept.

Comment-only, re-confirmed against current main (the check re-run because main advanced past the old base): non-comment, non-blank ADDED lines = 0; removed = 0. Three files, +51/-13, all comment or blank.

Per the review's landing treatment: no witness execution, no generated-artifact run, no substantive re-review.