Represent and verify the agent-held fleet credential, so the runner route can carry trust facts

[gunbai-bot]

Stacked on #8329 (base is session/bright-ferret-335-cred). #8329 closes the identity-file half; this closes the agent half and the representation gap underneath it. Merge #8329 first and this retargets to main.

The defect, in two parts

Part one is the same fail-open in a second place. gunbc.fleet_multi_principal_probe modeled_fleet_automation_credential_identity hashed the declared material and stamped it onto every PrincipalReachObservation, so the receipt's credential_identity — the field whose entire job is to say which key authenticated — named a key nothing had observed. #8329 closed exactly this on the identity-file route; it was open here too.

Part two is why the CI route had no trust facts at all. FleetSshCredentialBinding required an identity_file. An agent-held key has none. So the runner route could not construct a binding, could not construct a FleetSshExecutionContext, and SparkServingSliceRunnerAgent fell back to a bare SshShell { ssh_host: "user@host" } — no anchor, no credential, no posture. The missing representation is what forced the bypass.

The change

FleetSshCredentialLocus — where the private half lives — becomes a coproduct (FleetSshIdentityFileHeld | FleetSshAgentHeld) carried inside the still-sealed binding record.

The seal deliberately does not move onto the coproduct. sole_constructor seals a record, so making FleetSshCredentialBinding itself a coproduct would have made every arm publicly constructible and dropped the wall this module exists to hold. A forged locus is inert — it names a socket and a file. A forged binding would be a credential claim nobody observed.

The agent arm is verified against the agent's own listing. ssh-add -l against an explicitly named socket (not inherited SSH_AUTH_SOCK — which agent answered is a modeled fact), matched against fleet_automation_ssh_key_fingerprint. That is the same authority the hand-authored CI shell already compares against, so the model and that fragment cannot disagree about which key is expected.

The membership test is space-delimited rather than a bare substring, so a fingerprint carrying the declared one as a prefix does not match. Exit 1 (the agent has no identities) and exit 2 (cannot connect) both refuse; an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm — the empty string does not contain the fingerprint.

openssh_exact_agent_credential_options is the agent posture. IdentityFile there is not redundant and does not name a private key: with IdentitiesOnly=yes it is what selects one identity out of an agent that may hold several. Without a selector, OpenSSH falls back to default identity files; without IdentitiesOnly, it offers every key the agent holds. In both cases a success stops being evidence about the modeled key, which is the property these options exist to preserve.

Options are derived from the locus, so an agent binding cannot be paired with identity-file options or the reverse, and the receipt names where the credential was held rather than leaving a reader to infer it from which function was called.

Evidence

compile (dag + src/v2)                       0 diagnostics from changed files
                                             (identical to the pre-change run)
fleet_ssh_credential_verify_witness_test     21/21   (13 identity-file + 8 agent)
non_fold_residue_no_unrostered_or_stale      PASS
non_fold_residue_synthetic_unrostered_red    PASS

Mutation control. Neutering the fingerprint membership test to a vacuous containment, in an isolated detached worktree at this commit:

18 PASS / 3 FAIL
FAIL an_agent_holding_only_other_keys_refuses
FAIL a_fingerprint_extending_the_declared_one_refuses
FAIL an_empty_listing_on_a_zero_exit_does_not_verify

Exactly the three claims that depend on the membership test, and nothing else.

What this does NOT do

Stated because the tempting summary is "the agent route is now exact", and it is not yet.

fleet_multi_principal_probe's legs still run over typed_argv_probe_over_ssh, which carries no anchor and no options. What this PR changes for that probe is that its credential_identity is no longer fabricated — the run refuses outright unless the named agent is observed to hold the declared key — and that the binding needed to route those legs through shape_fleet_ssh_exec now exists. Routing them is the next step, not this one.

SparkServingSliceRunnerAgent is likewise still present and still produces a bare SshShell. It is now deletable rather than deleted: with an agent binding representable, both loci can become FleetSshExecutionContext values, and that arm becomes deletion population. That cutover also needs the runner job to materialize a known-hosts anchor, which is ci_spec work, so it is its own change.

Rung

Structurally guaranteed at the mint, on both arms: sole_constructor plus admit_callers leaves exactly one path to a binding per locus, and each runs its comparison first.

Outside the modeled guarantee, unchanged from #8329: that the key verified is the key that authenticated. The agent is observed to hold the fingerprint at verification time; OpenSSH then asks the same socket for a signature. An agent mutated between the two is not something ssh-add -l can close.

No dissolution obligations added.

— sent from bright-ferret-335