Skip to content

The launch requires proof the credential snapshot was taken - #13750

Merged
gunbai-bot[bot] merged 4 commits into
mainfrom
session/warm-crane-219-snapshot-proof
Oct 12, 2026
Merged

gunbai-bot[bot] merged 4 commits into
mainfrom
session/warm-crane-219-snapshot-proof

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 11, 2026 •

Copy link
Copy Markdown
Contributor

The defect

A Claude or Cursor launch argv named the attempt's credential snapshot by a path re-derived from the attempt identity at spawn time (dispatch_credential_snapshot_path_for_instance). Deriving the path is right — it is the identity of where the take writes — but nothing carried the proof that the take ran: an argv for an unwritten snapshot was the same value as one for a written one. The only refusal was the child's wrapper exiting 78 after a worktree, attempt state and a session/unit were staged. Two routes on main built exactly that: the instance-less dispatch_provider_inner_argv (Claude launched with no credential) and the uncalled dispatch_spawn_commands_for_inventory Claude arm.

The change

  • gunbc.dispatch_credential_snapshot (new leaf; the seal is per file, so this confines the mint to the take): TakenCredentialSnapshot sole_constructor { subject, path }, built only by dispatch_credential_snapshot_take, which is now given the attempt it takes for (CredentialSnapshotSubject: instance, host, node, attempt, provider); dispatch_credential_snapshot_discard(snapshot, attempt) removes the file only when the snapshot was taken for that attempt; AttemptCredentialSnapshot = NoCredentialSnapshot | CredentialSnapshotHeld { snapshot }.
  • Carrier: DispatchActuatorSelectionOk gains the required field credential_snapshot (same rationale as its required model field). The Claude and Cursor draws hold what they took; harness, vendor and Codex selections state none.
  • Boundary: claude_inner_argv_for_credential and cursor_worker_turn_argv take the sealed value, never a path. dispatch_provider_inner_argv_for_instance refuses a Claude/Cursor launch holding no snapshot, and refuses a held snapshot an executor never reads (CredentialSnapshotNotConsumed → DispatchSpawnRefused { step: credential-snapshot-unconsumed }) so the belt discards it instead of leaving it on disk.
  • Attempt binding (review round 1): proof that a take ran is not proof that this attempt's take ran — carried alone, attempt A's snapshot could launch attempt B, which the re-derived path never allowed. dispatch_credential_snapshot_subject_for_instance is the one derivation of the subject, used by the take and by the check; the spawn fold refuses a held snapshot whose subject is not the attempt being launched (CredentialSnapshotForAnotherAttempt → DispatchSpawnRefused { step: credential-snapshot-other-attempt }), before anything is staged. The subject is compared rather than the path because the path is only where the bytes are (in production derived from the same attempt; in a witness a directory the witness owns).
  • Belt: discards the snapshot the selection carried — no re-derivation — for its own attempt: an attempt ending with another attempt's snapshot leaves that file for its owner instead of deleting what another child is about to read.
  • Meaning fork removed: claude_credential_custody_source returned the snapshot's CredentialSnapshotTaken arm for a custody path; it now returns its own ClaudeCredentialCustody.
  • Delete-first, consumers enumerated by name: dispatch_spawn_commands_for_provider, dispatch_spawn_commands (no callers anywhere), dispatch_spawn_commands_for_instance, dispatch_spawn_commands_for_inventory, the instance-less dispatch_provider_inner_argv, GunbcHarnessSpawnNeedsInstance and its two reason rows. Test consumers migrated: witness_selected_provider_shapes_codex_tmux_command (now selection → dispatch_spawn_commands_for_resolved_instance), witness_inner_argv_carries_pinned_model_for_both_vendors (codex half hermetic, Claude half wet). Stale symbol citations in gunbc.roadmap_belt and the belt/actuator comments updated.
  • Failure mode a_launch_argv_names_a_credential_snapshot_no_take_wrote: found at mitigatable, now structurally guaranteed at the launch boundary on the seed route; residuals named with their closing capabilities (native route seal; bytes-present-at-exec stays the wrapper's exit 78; take-source rests on its two production callers; subject agreement is a typed refusal at the fold, not a construction — closes when the selection carries its attempt sealed and the spawn reads the subject from it; the take's host is not recorded, as on main).

Declared follow-up, not done here: codex_spawn_argv and dispatch_codex_home lose their last production consumer.

Witness layout (a consequence of sealing, stated plainly)

A sealed value cannot be supplied by a witness, so every claim that needs a taken snapshot now runs the real take over an mktemp fixture — the pairing obligation met by construction. Filesystem.Write/Mktemp have no hermetic response, so those claims live in the new wet test.claim.dispatch_credential_snapshot_wet_witness (declined by the CI wet lane, as every *_wet_witness_test.dag is). The hermetic files keep everything else and gain the REDs: a Claude/Cursor launch holding no snapshot refuses by name. The lab-instance claim — red on main, because Claude now runs in a transient systemd unit rather than tmux — is re-homed to the wet witness and asserts the unit shape; its codex half stays hermetic.

Verification (remote, cgroup-bounded seed runs)

Witness main this PR
worker_turn_dispatch_witness_test rc=0 rc=0
claude_code_dispatch_witness_test rc=0 rc=0
roadmap/roadmap_dispatch_actuator_witness_test rc=1 (witness_lab_instance_moves_repo_tmux_and_attempt_state_together) rc=0
worker_turn_standing_witness_test, cursor_harness_credential_witness_test, sessions_panel_witness_test, roadmap/roadmap_launch_deployment_receipt_witness_test rc=0 rc=0
roadmap/roadmap_belt_actuate_witness_test rc=1 (3 pre-existing: band fold vocabulary, exemplar roster, verify deferral) rc=1, same 3, none new
new dispatch_credential_snapshot_seal_witness_test — 4/4 PASS (forged literal, cast, nested in carrier each ==1; lawful carry ==0 on the subject and adds no blocking diagnostic beyond a baseline importing the same closure)
new dispatch_credential_snapshot_wet_witness_test — 17/17 PASS (take/refuse/discard by real I/O; Claude and Cursor launches name the snapshot taken for them; abandonment removes it, a launch keeps it; codex/harness refuse a held one; lab unit shape; REDs: another attempt's / provider's / instance's snapshot refuses at launch; a discard and a failed attempt leave another attempt's snapshot in place)
mutation: strip sole_constructor from TakenCredentialSnapshot — all three forge claims RED, green stays green
mutation: disable both subject checks (launch fold + discard) — exactly the five new REDs fail; the other 12 stay green
mutation: break the lawful carrier (take called without its subject) — only the green control fails

Round-1 receipts at head 5d4bbbab55: wet, seal, worker_turn_dispatch, claude_code_dispatch, roadmap_dispatch_actuator all rc=0. The earlier green control asserted total_blocking_count_for(...) == 0; the census counts the whole compile (gunbc.compile_diagnostic_census CompileDiagnosticCensus), so that was a corpus property and broke once the leaf imported RoadmapNodeId — it is now a differential.

The required witnesses job evaluates no witness (gunbc.rung_drop v1_required_lanes_withdrawn) and none of these modules is in its emitted closures, so these runs are the executed evidence.

Part of the construction-conformance program (session warm-crane-219); siblings #13746 and #13749 (both merged), #13752.

🤖 Generated with Claude Code

A Claude or Cursor launch argv named the attempt's credential snapshot by a path
re-derived from the attempt identity, so an argv for a snapshot no take had written was
the same value as one for a written snapshot; the only refusal was the child's wrapper
exiting 78 after a worktree, state and a session or unit were staged.

- gunbc.dispatch_credential_snapshot (new leaf, so the per-file seal confines the mint to
  the take): TakenCredentialSnapshot sole_constructor, built only by
  dispatch_credential_snapshot_take; discard takes the taken value; AttemptCredentialSnapshot
  is what a selection carries.
- DispatchActuatorSelectionOk gains the required field credential_snapshot. The Claude and
  Cursor draws hold the snapshot they took; every other selection states none.
- claude_inner_argv_for_credential and cursor_worker_turn_argv take the sealed value, never
  a path. dispatch_provider_inner_argv_for_instance refuses a Claude or Cursor launch that
  holds no snapshot, and refuses a held snapshot an executor never reads
  (CredentialSnapshotNotConsumed), so it is discarded rather than left on disk.
- The belt discards the snapshot the selection carried, never a re-derived path.
- claude_credential_custody_source returns its own ClaudeCredentialCustody instead of
  reusing the snapshot's arm for a custody path (one name, two meanings).
- Delete-first, consumers enumerated: dispatch_spawn_commands_for_provider,
  dispatch_spawn_commands (no callers), dispatch_spawn_commands_for_instance,
  dispatch_spawn_commands_for_inventory, and the instance-less dispatch_provider_inner_argv
  (its Claude arm launched with no credential), with GunbcHarnessSpawnNeedsInstance and its
  two reason rows. Their two test consumers migrate to the resolved-selection route.

Witnesses: the claims that need a taken snapshot run the real take over an mktemp
fixture in the new wet witness test.claim.dispatch_credential_snapshot_wet_witness; the
hermetic files keep everything else and gain the no-snapshot refusals;
test.claim.dispatch_credential_snapshot_seal_witness shows a forged literal, cast and
nested spelling each refuse exactly once (each goes red with the seal stripped). The lab
instance claim, red on main because Claude now runs in a transient systemd unit rather
than tmux, is re-homed to the wet witness and asserts the unit shape.

Recurring failure mode a_launch_argv_names_a_credential_snapshot_no_take_wrote records
the class, its rung (mitigatable -> structurally guaranteed at the launch boundary on the
seed route) and its residuals.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Brian Searls and others added 3 commits October 12, 2026 03:54
Proof that a take ran is not proof that this attempt's take ran. The sealed
TakenCredentialSnapshot now records the attempt it was taken for (instance,
host, node, attempt, provider); the spawn fold refuses a held snapshot whose
subject is not the attempt being launched, typed, before anything is staged.
The wet witness takes each snapshot for the attempt its claim launches and adds
one RED per subject dimension.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Holding a snapshot is not owning it. The discard names the attempt it discards
for and removes the file only when the snapshot was taken for that attempt, so
an attempt ending with another attempt's snapshot leaves it for its owner.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…with zero

The diagnostic census counts the whole compile, imported closure included, so a
total against zero asserted a property of the corpus; it broke as soon as the
leaf's closure grew. Compare against a baseline importing the same closure.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot merged commit ff6dca6 into main Oct 12, 2026
1 check passed
@gunbai-bot
gunbai-bot Bot deleted the session/warm-crane-219-snapshot-proof branch October 12, 2026 05:07
gunbai-bot Bot pushed a commit that referenced this pull request Oct 12, 2026
Conflicts were the credential-snapshot lifecycle (#13750) against the module
renames: main's side taken for the four regions it rewrote (cursor_harness_credential,
roadmap_belt_actuate, roadmap_dispatch_actuator, worker_turn_dispatch_witness,
which also drops the abandoned-cursor control main deleted), then every
main-changed module passed through the cutover rename map so main's imports and
citations name the modules by their positions. The two witnesses #13750 added
(dispatch_credential_snapshot_seal_witness, dispatch_credential_snapshot_wet_witness)
take the non-_test file names; their module lines already carried them.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants