Skip to content

mtcollins1_boot: narrow the fleet-key demand, or establish it cannot be - #11828

Merged
gunbai-bot[bot] merged 3 commits into
mainfrom
session/witty-swift-173
Sep 21, 2026
Merged

gunbai-bot[bot] merged 3 commits into
mainfrom
session/witty-swift-173

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 20, 2026

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session witty-swift-173.
Pushing to session/witty-swift-173 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

… and reproject the key step

MtCollins1Boot => FleetSshKeyNotConsumed in
gunbc.fleet_converge_workflow fleet_converge_mode_fleet_ssh_key_demand, with the
regenerated .github/workflows/fleet-converge.yml carrying the reprojected key-step
`if:` in the same commit.

#11777 gave this mode FleetSshKeyConsumed as the STATUS QUO under repair pressure,
not as a finding that it needs the key. This is the walk that settles it.

THE COUNTER-ARGUMENT, ANSWERED. SOL is a host session, so the mode plainly touches
a machine; the question is whether it resolves the FLEET KEY to do so. Every
transport reached from mtcollins1_boot_wet, enumerated from the REACHED SYMBOLS
rather than the module import closure (which is a superset and does contain
ssh-reaching modules this entry never calls into), with the credential each
presents:

  Filesystem.Read/Write/WriteOwnerOnly/WriteCreateNew/Delete  local, none
  http.Client.GetLocalhostBounded, PostJsonFromFile           loopback, approval submission MAC key
  megarac.Media.{OpenSession,GetRemoteConfigurations,
    GetRemoteImages,StartMedia,CloseSession,
    ProbeSessionOnMediaRoute}                                 HTTPS to BMC, pinned BMC credential file
  ipmi.Tool.{ChassisBootDevWithOptions,ChassisBootParamGet,
    ChassisPowerControl,SolDeactivate},
    sol_hold.ActivateHeld                                     ipmitool -I lanplus to BMC, same credential via -f
  shell.Env.Get, sleep.Delay.Seconds, Clock.Now               none

The SOL session is carried by IPMI to the BMC, not by an ssh channel to the host,
so it presents the BMC credential and never an identity from the agent. No reached
symbol resolves fleet_ssh_locus, constructs an SshTarget, or calls typed_argv_exec
over fleet SSH, on the first attempt or on any retry or fallback arm;
gunbc.remote_shell_command, gunbc.fleet_ssh_access and gunbc.fleet_reach are
outside the reached set entirely. The two imports that could suggest otherwise take
one inert symbol each -- host_reset_bmc_credential_path_env (an env-var NAME) and
operator_host_srv1 (a host record). The ungated steps of the fleet-converge job
(checkout, artifact download, unpack+verify, WIF auth, agent teardown) open no ssh
session either.

WHAT LANDS: for a mtcollins1_boot dispatch the pinned fleet key version is no
longer fetched, no 0600 key file is written under RUNNER_TEMP, and no ssh-agent is
loaded. ApprovalKeyringConverge is untouched and stays Consumed -- it really does
reach typed_argv_exec_over_fleet_ssh against srv1.

EXECUTED (not a CI check):
  claim_batch mtcollins1_boot_does_not_materialize_the_fleet_key -> PASS
  the same claim with the arm flipped back to FleetSshKeyConsumed -> FAIL
    (the discriminating red; the control assertion that
     'approval_keyring_converge' is still PRESENT in the same string keeps the
     negative from being satisfiable by an empty condition)
  claim_batch api_only_org_modes_do_not_materialize_the_fleet_key -> PASS
  tools.generated_artifact_gate main -> exit 0 (committed artifacts agree)
  tools.generated_artifact_gate main_wet -> wrote every registry artifact; the only
    resulting diff is the one key-step `if:` line

NOT executed: a wet run of the mode. That is the acceptance evidence the brief
names and it needs an operator dispatch of fleet-converge mode=mtcollins1_boot at
this head.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 20, 2026 08:04
# Conflicts:
#	dag/gunbc/fleet/fleet_converge_workflow.dag
@gunbai-bot

gunbai-bot Bot commented Sep 20, 2026

Copy link
Copy Markdown
Contributor Author

Merged main in; #11788 landed the same flip while this was in review, so the scope of this PR has changed. It is no longer the arm.

cdb6079b0da (#11788) already carries MtCollins1Boot => FleetSshKeyNotConsumed and the regenerated fleet-converge.yml. My diff against main is now zero on both: the YAML is byte-identical, and the arm agrees.

What remains — and the reason I did not just close this:

  1. The executing claim. mtcollins1_boot_does_not_materialize_the_fleet_key reads the derived fleet_converge_fleet_ssh_key_step_if and goes red if the arm regresses to Consumed (verified: I flipped it back and the claim FAILed). Main's flip currently has no consumer that would notice a regression — DESIGN §3c, a value with no executing reader.
  2. The transport enumeration, kept as // annotation beneath main's paragraph rather than beside it. Main's sentence names the route ("BMC/IPMI, SOL and HTTP approval submission"); this lists each operation with the credential it presents, and records that the walk is at reached-symbol grain — the module import closure of mtcollins1_boot_run does reach fleet_ssh_access and remote_shell_command, which is what made this arm look undecidable. I deliberately did not restate main's verdict sentence; that would be the meaning fork.

Re-ran after the merge: mtcollins1_boot_does_not_materialize_the_fleet_key → PASS.

The outstanding acceptance evidence is unchanged and is now against main, not against this PR: a wet dispatch of fleet-converge mode=mtcollins1_boot. Main is already not materializing the key for that mode.

— sent from witty-swift-173

@gunbai-bot

gunbai-bot Bot commented Sep 20, 2026

Copy link
Copy Markdown
Contributor Author

On review 69061's non-blocking note — it is correct, and I want to state the gap precisely rather than paper over it.

What the witness establishes: that the arm is NotConsumed and that the projected key-step condition consequently excludes the mode. That is machine-checked, with a discriminating red.

What only the annotation asserts: that mtcollins1_boot_wet's reached closure never resolves fleet_ssh_locus. §4c is right that an annotation is not evidence — no Accepted program can read it. So that fact currently sits at rung 1 (mitigatable: a human walked it, twice, independently — me and #11788), not at 2.

Why I am not closing it in this PR. The missing capability is a reachability lens over the Node tree: "which service operations does the closure of this entry reach". I checked for one — test.claim.workflow_capability_closure_witness annotates workflow steps by hand, and credential_argv_exposure_witness reads modeled prelude strings; neither computes a source closure, and grep finds no service_operation_closure / effect_closure anywhere in dag/ or src/. Building that is a substrate capability in its own right, not a polish item on a two-addition PR, and it would be worth far more than this one arm: it is the general wall for "this entry does not reach that credential", which today is answered by a careful human read every time.

So: the next-rung trigger for this class is a service-operation reachability lens over an entry's closure, and until it exists the closure fact is a walked argument recorded in the quarantine channel where §4c puts it, with the arm's consumption held at rung 2 by the witness. I would rather say that plainly than let the annotation read as proof.

— sent from witty-swift-173

@briansrls
briansrls added this pull request to the merge queue Sep 20, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Sep 20, 2026
# Conflicts:
#	dag/test/claim/machine_intake/mtcollins1_boot_run_witness_test.dag
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Sep 21, 2026
Merged via the queue into main with commit f730e41 Sep 21, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/witty-swift-173 branch September 21, 2026 00:36
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