Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included by gunbai-bot[bot] · Pull Request #8356 · gunb-ai/gunbc

gunbai-bot · 2026-08-17T02:51:07Z

Stacked on #8334 (base session/bright-ferret-335-selector), which is stacked on #8332 → #8329. Retargets to main as the one below it merges.

The defect

spark_serving_desired_members builds the full desired population — runtime root, user unit, primary model slot, linger — and had zero production consumers. Only its own definition.

The live plan is spark_serving_linger_membership_plan, whose desired side is the single-element list [spark_serving_desired_linger_member(host)]. So three of the four modeled members were never planned.

This corrects something I told the operator: that what remained was "realizing WriteUserUnitFile, then InstallRuntimePackage and PullModelArtifact." Those arms would have been unreachable by the live workflow — a plan that never plans a member never selects the effect that converges it. Adding executor arms above a linger-only plan is specification-without-execution: it typechecks, it witnesses green, and it converges nothing.

The change

The desired side already existed and was correct. What was missing is the observed side.

spark_serving_observed_members projects observed membership from an observation, and the desired release is deliberately not a parameter of it. Deriving an observed state digest from the desired one would make every member reconcile as converged by construction — the reconcile would compare a value to itself and the plan would always be empty. That is the failure this lane exists to avoid.

Two states an observation genuinely cannot establish are typed rather than guessed:

UserUnitStateUnobserved — the live observer reads LoadState and is-active, not the unit file's bytes and not is-enabled. "We did not look" stays separate from "the unit is absent"; they have different remedies. unit_observed travels beside the members so a consumer can tell a plan built on a complete observation from one built on a partial one without inferring it from list length, and spark_serving_projection_supports_empty_replan is what a caller reads instead of re-deriving it.
SparkServingObservationRefused refuses the whole projection. Rendering it as an empty population would plan every member as an addition against a host nobody saw — the empty-observation narrow, the mirror of the absorbing fallback. SparkServingAbsent is the opposite and is a real observation: the host was reached and the runtime is not there, so the members are genuinely absent and the plan adds them. That is the bare-srv6 path.

spark_serving_full_membership_plan reconciles the two and propagates the refusal.

Evidence

spark_serving_full_plan_witness_test        12/12
spark_serving_converge_slice_witness_test   23/23  (regression, unchanged)
non_fold_residue_no_unrostered_or_stale     PASS
non_fold_residue_synthetic_unrostered_red   PASS

Mutation control, run in an isolated detached worktree at this commit. Reverting the full plan's desired side to the linger-only list it supersedes:

FAIL a_bare_host_plans_all_four_members_not_only_linger
FAIL a_bare_host_with_linger_already_enabled_plans_three
PASS the_superseded_linger_plan_writes_exactly_one

The keystone reds on exactly the mutation it exists to catch, and the contrast claim — which measures the superseded function, not this one — correctly stays green. Distinct constants (4, 3, 1) rather than a Boolean, so a plan that happened to write something does not satisfy it.

The witness takes its release from spark_serving_desired_admission, the declared authority, rather than a fixture that could drift from it; a refused admission has no release to plan against and the witness says so instead of substituting one.

Not claimed: no whole-tree corpus compile — three attempts were OOM-killed under shared-slice pressure, so verification here is entry-scoped.

Rung

Mechanically preventable that the plan covers the full population: the keystone is a discriminating RED on the real plan function with an executed mutation control. Not structural — a future caller can still hand membership_reconcile a narrower desired list.

What this does not yet deliver: the four effects are planned, but WriteUserUnitFile still runs through the weaker tee path rather than converge_typed_remote_file, and InstallOwnedRuntimeClosure / PullModelArtifact are unimplemented. Unit-bytes and is-enabled observation are also still missing, so unit_observed is false on the live route and a second plan cannot yet honestly be empty. Those are the next commits, and they are now reachable, which is what this PR buys.

No dissolution obligations added.

— sent from bright-ferret-335

`spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

gunbai-bot · 2026-08-17T03:28:59Z

The finding is right and the title was the wrong claim. Retitled: "Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included."

Two things came out of chasing it.

Why the cutover is not in this PR

spark_serving_full_membership_plan cannot be switched on yet because the observation behind it is incomplete, not because the plan is. The live observer reads LoadState and is-active — not the unit file's bytes and not is-enabled — so unit_observed is false on the live route. Cutting over today would plan the unit member as an addition on every run and a second plan could never be empty. spark_serving_projection_supports_empty_replan exists precisely so that condition is read rather than assumed, and it currently answers false.

The unit-bytes and is-enabled observation is the next commit, and the cutover rides with it.

Worth recording against your specification-without-execution concern: spark_serving_converge_realize already refuses on WriteUserUnitFile, InstallOwnedRuntimeClosure and PullModelArtifact with located reasons. So the cutover cannot silently converge — it surfaces three loud refusals, which is the honest census of what is unimplemented rather than a green run that converged nothing.

The hole your finding led me to, now fixed

Chasing "what happens when this plan is actually consumed" found a real one on the path the cutover takes.

fleet_converge_spark_serving_typed_actions was a flat_map whose Absent arm returned []. A planned member action that does not translate was discarded, and the artifact then froze fewer typed rows than its own plan had actions with no diagnostic at all. The only action reaching that arm is MemberRemovalRefused — so the drop erased a refusal by silently succeeding.

Its frequency was zero by construction: the only live plan is linger-only and linger always translates, so nothing ever exercised it. A four-member plan is exactly the input that reaches it. Had the cutover landed first, three members could have vanished from the frozen artifact and the row count would have reported converged.

It now refuses with a counted cause naming both numbers, witnessed:

a_plan_whose_member_cannot_translate_refuses_the_typed_projection   PASS
an_ordinary_linger_plan_still_projects_its_rows                     PASS  (positive control)

The refusal's cause is propagated but not carried — FleetConvergePlanArtifact? has no arm for one, so the wet slice renders the generic plan-refused verdict. That is annotated in-code as a bounded gap with its trigger rather than left to be found: the cutover has to widen that return type anyway, and that is where the cause gets somewhere to go.

Evidence

spark_serving_full_plan_witness_test        14/14   (12 + the 2 above)
spark_serving_converge_slice_witness_test   23/23   (regression, unchanged)
non_fold_residue_no_unrostered_or_stale     PASS
non_fold_residue_synthetic_unrostered_red   PASS
compile (dag + src/v2)                      0 diagnostics

Mutation control unchanged and still discriminating.

— sent from bright-ferret-335

…selects an observed key (#8334) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `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` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- 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 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. 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. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector file is what makes a success evidence about the modeled key, so a path naming a file that does not exist -- or one holding a DIFFERENT public key -- silently removes the exactness the option set was chosen for. A path string is not a selector; the bytes are. `AgentSelectorFile` is now `sole_constructor` with one production mint, `materialize_agent_public_selector`, which writes the declared public key line, reads it back, and seals only when the content identities agree -- the same write/readback/compare construction `KnownHostsAnchor` already uses, for the same reason. `classify_agent_key_listing` takes the sealed value, so a literal path cannot reach the mint at all. The path is attempt-owned, as the anchor path is: two concurrent runs must not write one another's selector, and a stale file from another attempt must never be readable as this one's. The probe threads its attempt identity through and refuses before any observation when that identity is not a safe path segment. The file carries PUBLIC material only. The private half stays in the agent and is never written by this module. The hermetic witness fixture is admitted to the seal explicitly, exactly as the known-hosts anchor admits its own -- a witness has no filesystem, and what the seal buys is that no OTHER module can hand the classifier a path it merely named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the trust-free Spark credential locus: the runner route builds a sealed context (#8336) `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back (#8339) * Delete the trust-free Spark credential locus: the runner route builds a sealed context `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back typed_remote_file_write_authority_note reserved a convergence arm and said what it would take: "A zero tee exit proves only that the remote process accepted stdin — not that bytes landed at the declared path with declared mode. A future TypedRemoteFileWriteConverged variant requires independent read-back (operator ruling msg_71f67aa9); stage-and-rename + mode + read-back land before that arm is writable." This is that arm. FOUR STEPS, AND THE ORDER IS THE PROPERTY. Stage to a sibling path, set the mode there, `mv -f` within the one directory (POSIX-atomic), then read the DESTINATION back and compare. Writing straight to the destination and chmod-ing afterwards publishes incomplete bytes under the real name; on a unit file that is a window in which systemd can read something that was never a valid unit. Each step's failure is located by name, so a converge that stops says which invariant did not hold rather than returning one opaque false. dd status=none, NOT tee. tee copies stdin to stdout, so every byte written is echoed back across the channel and into whatever captures it. That doubles transfer and puts file content in the run log -- for a credential or config file that is a disclosure, not a style preference. READ-BACK BY CONTENT, NOT BY DIGEST, and the reason is a real constraint rather than a shortcut: a digest comparison needs a digest of the INTENDED bytes, and .dag has no SHA-256 over a String -- extdeps.crypto.hash Digest carries a hex its caller supplies. Comparing a remote sha256sum of the staged file to one of the destination would prove the rename moved the same bytes while saying nothing about whether those bytes were the ones declared, which is the whole question. Reading the file back answers it directly, and the comparison happens in the model where a witness can exercise it. The comparison is exact. Normalizing trailing whitespace would let a real difference pass, and a file whose trailing bytes differ from the declared content is not the file that was declared. Mode is a closed two-arm enum rather than an octal string, so a nonsensical mode has no constructor. Admission is unchanged and still governs: a path outside the declared scope produces no admitted write, hence no staging path and no steps. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the attempt-identity match one expression per arm Review 52733 (cosmetic): the credential gate was a `match` nested inside the attempt-identity `match` but indented back to the outer column, which parses fine and reads as though the outer match had ended. It was an artifact of patching the gate in rather than a shape anyone chose. The gate moves to `spark_managed_access_standing_for_attempt`, so each arm of the outer match is one expression and the nesting is visible in the call structure instead of hidden by indentation. No behavior change: same three verification arms, same refusal reasons, same order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included (#8356) * Plan all four serving members, not only linger `spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an untranslatable planned member instead of dropping it `fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the declared-residue annotation to module-item grain The comment sat inside `spark_serving_fleet_converge_plan_artifact`'s body, which DESIGN 4c does not model: annotations attach at module-item grain only. The compile-clean gate located it exactly; `gunbc compile --target dag` does not run that gate, which is why it passed locally. Same text, moved above the declaration it describes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>

…8361) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `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` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- 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 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. 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. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector file is what makes a success evidence about the modeled key, so a path naming a file that does not exist -- or one holding a DIFFERENT public key -- silently removes the exactness the option set was chosen for. A path string is not a selector; the bytes are. `AgentSelectorFile` is now `sole_constructor` with one production mint, `materialize_agent_public_selector`, which writes the declared public key line, reads it back, and seals only when the content identities agree -- the same write/readback/compare construction `KnownHostsAnchor` already uses, for the same reason. `classify_agent_key_listing` takes the sealed value, so a literal path cannot reach the mint at all. The path is attempt-owned, as the anchor path is: two concurrent runs must not write one another's selector, and a stale file from another attempt must never be readable as this one's. The probe threads its attempt identity through and refuses before any observation when that identity is not a safe path segment. The file carries PUBLIC material only. The private half stays in the agent and is never written by this module. The hermetic witness fixture is admitted to the seal explicitly, exactly as the known-hosts anchor admits its own -- a witness has no filesystem, and what the seal buys is that no OTHER module can hand the classifier a path it merely named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the trust-free Spark credential locus: the runner route builds a sealed context (#8336) `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back (#8339) * Delete the trust-free Spark credential locus: the runner route builds a sealed context `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back typed_remote_file_write_authority_note reserved a convergence arm and said what it would take: "A zero tee exit proves only that the remote process accepted stdin — not that bytes landed at the declared path with declared mode. A future TypedRemoteFileWriteConverged variant requires independent read-back (operator ruling msg_71f67aa9); stage-and-rename + mode + read-back land before that arm is writable." This is that arm. FOUR STEPS, AND THE ORDER IS THE PROPERTY. Stage to a sibling path, set the mode there, `mv -f` within the one directory (POSIX-atomic), then read the DESTINATION back and compare. Writing straight to the destination and chmod-ing afterwards publishes incomplete bytes under the real name; on a unit file that is a window in which systemd can read something that was never a valid unit. Each step's failure is located by name, so a converge that stops says which invariant did not hold rather than returning one opaque false. dd status=none, NOT tee. tee copies stdin to stdout, so every byte written is echoed back across the channel and into whatever captures it. That doubles transfer and puts file content in the run log -- for a credential or config file that is a disclosure, not a style preference. READ-BACK BY CONTENT, NOT BY DIGEST, and the reason is a real constraint rather than a shortcut: a digest comparison needs a digest of the INTENDED bytes, and .dag has no SHA-256 over a String -- extdeps.crypto.hash Digest carries a hex its caller supplies. Comparing a remote sha256sum of the staged file to one of the destination would prove the rename moved the same bytes while saying nothing about whether those bytes were the ones declared, which is the whole question. Reading the file back answers it directly, and the comparison happens in the model where a witness can exercise it. The comparison is exact. Normalizing trailing whitespace would let a real difference pass, and a file whose trailing bytes differ from the declared content is not the file that was declared. Mode is a closed two-arm enum rather than an octal string, so a nonsensical mode has no constructor. Admission is unchanged and still governs: a path outside the declared scope produces no admitted write, hence no staging path and no steps. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the attempt-identity match one expression per arm Review 52733 (cosmetic): the credential gate was a `match` nested inside the attempt-identity `match` but indented back to the outer column, which parses fine and reads as though the outer match had ended. It was an artifact of patching the gate in rather than a shape anyone chose. The gate moves to `spark_managed_access_standing_for_attempt`, so each arm of the outer match is one expression and the nesting is visible in the call structure instead of hidden by indentation. No behavior change: same three verification arms, same refusal reasons, same order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included (#8356) * Plan all four serving members, not only linger `spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an untranslatable planned member instead of dropping it `fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the declared-residue annotation to module-item grain The comment sat inside `spark_serving_fleet_converge_plan_artifact`'s body, which DESIGN 4c does not model: annotations attach at module-item grain only. The compile-clean gate located it exactly; `gunbc compile --target dag` does not run that gate, which is why it passed locally. Same text, moved above the declaration it describes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the systemd unit file so a Spark serving unit can become bytes SparkServingUserUnitSpec is typed fields and deliberately not systemd INI syntax. That left a gap rather than a decision: nothing could turn the spec into a file, so WriteUserUnitFile had no bytes to deliver and the unit member had nothing to be observed against. extdeps.systemd.unit_file models the format, cited to systemd.unit(5) and systemd.service(5). One directive type per section, so `ExecStart=` in [Unit] and `WantedBy=` in [Service] have no representation -- the misplacement class is structurally impossible rather than validated. The file is a record of three sections, so a transposed or duplicated section is likewise unwritable. extdeps.ollama.server_env owns OLLAMA_HOST / OLLAMA_MODELS. They previously appeared in the tree only inside a prose comment, so any consumer had to spell the literals itself -- a second authority for ollama's own names. gunbc.spark_serving_unit_render maps the spec onto that authority and is the single rendering, so the write side and the observe side cannot drift into two renderings of one spec and report a permanent MemberChanged against itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the two new extdeps modules in scope_carrier_paths The placement gate refused: a new dag/extdeps file must both declare extdeps_model_scope AND join scope_carrier_paths. Both modules already declared the scope; neither was rostered, and the frozen legacy manifest is not a landing state for a new file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>

… and refuse producer/consumer disagreement (#8349) * R1: locate the wrap-decision root at fourteen field occurrences, and correct the census's own emitter attribution The lane's problem statement said the Rust emitter wraps every shared_types member. Measured against two independently produced emitted trees, that is not what happens, and the difference decides what a fix may be. Three findings, none of which change code: The emitter that produced the 55-site census is frozen v1, not v2. The emitted files are named v2_* because their SOURCE modules are v2 .dag files; stage0 carries v1_compiler_emit_rust.rs and no v2_compiler_translate.rs at all, so wrap_decision_gate was dormant throughout. An earlier cross-lane inference that joined the v2 catalog's position fork to these numbers is retired here. The root is a type-level fact consumed through occurrence-level keys. build_shared_types computes membership once per type; three seams then consult it through properties of each occurrence's syntax, and no arm refuses when they disagree -- render_rust_shared_type_if_needed returns the unwrapped rendering on a miss, silently. The inconsistency is far narrower than a position rule: ten types, fourteen bare field occurrences, every one wrapped at every signature occurrence and bare at one or more field occurrences, with zero bare signature occurrences in the population. Two instruments agree type for type and line for line. That makes R1 one defect producing both signs -- a signature returning Rc<T> into a bare field is the over, a bare field into a parameter typed Rc<T> is the under -- so one fix moves both counts, where a position-based fix would have moved half and worsened half. Two position-based readings are recorded as retired rather than deleted: that signature wraps while field does not, and that generic enclosing items force bare. Both were held with confidence; the first came from a sample selected by the failing sites themselves, the second was predicted from the arm cascade and falsified at 17 of 17 and 6 of 6. Disposition ruled (b) -- specification for the v2 emitter, not a v1 repair -- with the resulting coverage gap declared: the v1 image stays red and the burn-down is unmeasurable until the emitter flips. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * R1: decide the flow, not the position — wrap_decision_flow_gate refuses producer/consumer disagreement Follows the (b) ruling: the fix is a concept v2 is missing, not a repair in the frozen v1 seed. wrap_decision_gate answers one position at a time, and every consumer acts on that answer alone. A value does not live at one position -- it is produced at one and consumed at another -- so when the two answers differ, the emitted program carries a type error no stage located, because no stage compared them. Measured, that is ten types and fourteen occurrences, and it produces BOTH error directions from one inconsistency. wrap_decision_flow_gate makes the flow the decided unit. It projects the same authority at both ends -- never a second lookup, so the ends cannot disagree about the catalog -- and refuses, typed and located, when the catalog's answers for the two positions differ. wrap_decisions_equal compares reference layers, not merely by-value against by-reference. Deliberately NOT a fifth TargetOwnershipUseSite inhabitant. Adding OwnershipAtCallArgument would be a fifth position opinion about a defect whose cause is that every position already holds its own; a missing inhabitant is the right fix only when the missing position is the one that should decide. This is also why "53 of 54 at call-argument position" does not locate the defect: that is where rustc points, and the cause is in the field declaration. Rung: silent wrongness -> mitigatable. NOT structural impossibility -- the invalid state stays writable, since a catalog may still state different layers at two positions and the only answer here is refusal. Next rung is a modeled layer transition, which is a carrier change and is sequenced ahead of the pipeline edit rather than inside it. Not wired into 06_translate here. Evidence by execution: six new witnesses green, six pre-existing unregressed, both directions drawn from the live catalog by varying only flow direction over Diagnostics. Two mutations executed; the profile is not uniform and is reported as measured -- forcing agreement reds the two directions and the layer control but NOT the missing-row witness, which is therefore a propagation regression control and not a disagreement control; layer-blind equality reds only the distinct-layer witness, which is what earns it its place. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct my own overclaim: two traversals of one catalog, not one lookup The flow-gate note said "never a second lookup". That is the loose form and it is an overclaim. What the construction rules out is a divergent AUTHORITY -- one function over one catalog, so no second opinion exists to drift -- not a repeated read. It performs two traversals of the row list. The repeated read is a real cost shape and is now named rather than waved off as small, per DESIGN section 6's rule that a proven cost shape is fixed regardless of the realized n. It is not fixed here because the per-carrier policy that would serve both ends from one fold is the same carrier the next rung needs; building half of it now to save one fold would fork what the transition work has to own. Trigger recorded: that carrier landing. Also drops two statements the construction commit made stale: the section no longer claims to change no code, and the seam-2 figure is fourteen occurrences across ten types rather than the pre-sweep ten across six. Re-verified: module compiles clean, six flow witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the two new rationale blocks from prose rows to authored // annotations DESIGN section 4c calls a `data NAME_note: String` whose sole purpose is commentary modeling debt, and names the leading `//` block as where irreducible rationale belongs. Both rows this branch introduced are converted. Worth stating why this is not a no-op that the gate would have waved through: `prose_row_introduction_gate` enforces only under `prose_row_migration_scope`, and none of this branch's three touched paths are among its 262 entries -- so these rows would have been COUNTED as out-of-scope residue and never refused. Legal, and still debt in the direction the migration exists to remove. Writing new prose rows into an unmigrated path because the wall does not reach there yet is the same move as relying on a check not to fire. Verified rather than assumed, against a gunbc built from this tree rather than the shim (which the annotation class is known not to be an oracle for): both compile-clean annotation refusal classes are clear -- no indented `//` inside a declaration body, and no trailing block at EOF naming no subject -- the module compiles clean, and all witnesses stay green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Two-arm artifact diff: my prediction was wrong twice, and the excuse was refuted Tested the claim that this changes no emitted output outside its own module, rather than asserting it. Same entry, same command, same source roots, same binary; only the commit differs, so M is fixed by construction. Prediction written before the run, in both directions. Whole artifact diffed -- all 177 files, no grep for the shape I believed I touched, since the hazard is a second consequence the author did not predict. Two files differ, not one, and both halves of the prediction were wrong in detail: the predicted file lost a GLOB IMPORT rather than the two note constants (which turn out never to have emitted at all, in either arm), and a module I never touched -- v2_std_cross_tree_resolution.rs -- moved two pub use lines. The tempting reading of the second file is emission nondeterminism. The control refutes it: B vs B-prime, same commit re-run, is 0 differing files, and A vs B-prime reproduces the reorder exactly. It is deterministically caused by this change, by widening an import list in an unrelated module. Ownerships stated separately because they have different answers: the ARTIFACT change is mine; there is no DEFECT -- sorted line multisets are identical, so it is a pure reorder of explicit named re-exports, order-irrelevant to resolution, with no non-pub-use line involved. The whole-artifact form buys a positive argument an absence cannot: 177 files, 2 differ, 46 lines, every other byte identical -- so a path keying on emitted text this change perturbed would have had to surface elsewhere, and nothing does. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retract an unsupported emission claim I made against my own receipt, and restore a space I ate Two corrections, one substantive. THE SUBSTANTIVE ONE. This receipt read the note constants' absence from both arms as evidence that a `data NAME_note: String` prose row emits nothing. That is the vacuous-closure error the same section warns about, committed against its own author: the prose rows existed only on an intermediate commit, so NEITHER ARM EVER CONTAINED ONE, and an absence measured over a closure that never held the shape proves nothing about the shape. The general form is independently known false -- another lane watched a `_note` row appear in generated `.rs`. Whether a prose row emits is a per-site fact needing its own two-arm receipt, and this receipt does not carry one. The prose-to-annotation conversion here is justified by section 4c modeling debt alone, which was always its only real argument. A discipline follows and is recorded with it: do not convert prose rows on a PR whose emission measurement is already banked, because the conversion may be an artifact change that invalidates it. Worth being plain about the shape of the mistake, since it is the one I spent the evening catching in other people's claims: I did not measure the thing I reported. I measured something adjacent that could not have come out any other way, and read the result as though it had been at risk. THE COSMETIC ONE. An earlier edit's replacement pattern ate the space after `=` on the pre-existing `wrap_decision_composite_note` line -- a line this branch had no business touching. Restored. Caught independently in review. Re-verified: test module compiles clean, six flow witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retract the reorder causal claim: the null produces the same two lines in the same file (#8349) The receipt read a pub-use reorder in v2_std_cross_tree_resolution.rs as deterministically caused by widening an import list, on the strength of a repeat-emit control at 0 differing files. Another lane obtained the identical shape from the null alone, with the same flag and the same SHA, moving the same two lines. A control can only accumulate failures to refute, so the file is excluded from attribution rather than explained, and the repeat count is stated as n rather than as proof. The substitution half of the receipt and the construction itself never rested on this paragraph. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the order test's false-fire arm: it misreported this branch's own subject file (#8349) The common-line relative-order test reported REORDERED on a file that is a pure addition of four functions. Adding code adds copies of high-multiplicity boilerplate lines, and a greedy multiplicity cap mis-pairs them, so surviving content lines appear transposed. The verdict resolved to SAME-ORDER only after excluding boilerplate, while a genuinely reordered file stayed REORDERED at every filter level and both controls behaved correctly throughout — the instrument passes its own validation while answering wrongly on a real file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rest the reorder read on the unique-valued restriction, not the boilerplate heuristic (#8349) Restricting the common set to values appearing exactly once on both sides reproduces both verdicts without any judgement about which lines are boilerplate: SAME-ORDER at 93 for the subject file, REORDERED at 134 for the re-export file. The heuristic filter is kept only as the route by which the false fire was found. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rest the reorder read on the diff-based instrument, which names the moved lines (#8349) A reorder exists iff some line is both deleted and added by the alignment. That asks the question directly rather than extracting a common subsequence, so it is immune to the multiplicity family that broke three earlier variants. It reports SAME-ORDER for the subject file and REORDERED for the re-export file, naming the two qualified_name re-exports as the movers. The boilerplate heuristic and the unique-valued restriction are kept only as the route: the first can hide a reorder of boilerplate, the second cannot see a reorder of repeated lines. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * State why naming a mover is sound here: the two transposed groups are unequal (#8349) A transposition admits two alignments, and a symmetric one has no fact of the matter about which side moved. This case is a block of two qualified_name re-exports crossing a block of four cross_tree_import_model lines, so minimality picks the smaller group. Where the groups are equal size the honest output is the unordered pair. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Ground the mover naming in the forward/reverse test, and mark it a wager (#8349) The size clause is dropped: an implementer holds the forward and reverse mover sets, which are equal in size for any transposition, so a size test refuses the cases it exists to preserve. Agreement between directions is the test; disagreement is the signature of a symmetric transposition. Both directions return the same two lines here. Minimality is a cost argument rather than an observation, so the naming is recorded as the likelier mover. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Stop citing the repeat count as a clearing argument; the flip rate is 4 of 12 (#8349) The receipt justified its four clean pairs by a never-one-repeat rule that has since been withdrawn. At the measured rate a four-pair control misses a genuinely unstable file often, so no repeat count is offered as a clearing argument here. What excludes the file is membership in the known-unstable set. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Complete the witness note's enumeration: it listed one surface and there are now two (#8349) The row a session greps to learn what this file covers named only wrap_decision_gate and its two RED controls, while this PR adds a second authority over a producer/consumer pair and six witnesses with a deliberately non-uniform mutation profile. Not false — incomplete, which is the shape that sponsors re-deriving an arm that already exists. The profile is stated so it says which witness guards which arm. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare the census denominator incomplete by execution: +18 proven, 306 candidates, direction open (#8349) The 55/28/27 count is keyed on rendered diagnostic text. A two-arm run varying only a carrier deletion left 18 sites textually identical while the realization changed underneath them, and those 18 are disjoint from the 55 — so the census misses them. The same mechanism also renders under two signatures the renderer picks between inconsistently, splitting 43 sites of one cause across two roots. A 306-row one-layer pool is a candidate set, not a hidden population; its largest block is a genuine carrier disagreement wearing the same shape. Direction of the error is unestablished in general. The mechanism and the construction are unaffected — neither reads a printed type name. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Withdraw the +18 and the renderer-inconsistency reading; the 55 stands (#8349) The correction published one commit ago rested on a specimen read from one module's artifact and applied to sites in another: 01_tokenize's Nat is an enum and its closure carries no algebra alias, so those 18 sites did not move because nothing about their type changed, and an enum against an integer is a carrier disagreement rather than a wrap decision. The two spellings were two different types sharing a leaf name, not one type printed twice, so there is no 43-site mechanism. What survives is a real hazard with no measured cost here: a leaf name can denote different types under different module authorities, so a census pooled across modules is keyed on a name that is not unique over the population it pools. Alias expansion does not fix that; resolved type identity per artifact does. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Vias: what makes a net legitimately present on two layers, and the refusal that narrows because of it (#8331) * Vias: what makes a net legitimately present on two layers, and the refusals that follow Rebased onto main after the copper base merged; this now carries only the via delta. The copper increment refused ANY net realized on more than one layer, having no way to tell a routed layer change from two conductors forking one name. A via is that distinction, so NetRealizedMoreThanOnce is DELETED and replaced rather than joined - a superseded refusal that still has a constructor is a second authority for one question. Both via endpoints are CopperLayerRefs, so a via inherits the stackup binding for free and cannot join one board's layer to another's. What a reference cannot carry is the endpoints being DIFFERENT, so a via from a layer to itself is a checked refusal reporting its ordinal. THE KEYSTONE ASSERTS BOTH DIRECTIONS IN ONE RUN: the identical split refuses with no via and admits with one. A via on a DIFFERENT net does not route this one, and that control is built so counting cannot pass it - same two layers, same via count, only net identity differs. AND THE HOLE NARROWING OPENED, found in review and confirmed by execution before fixing: vcc realized twice on layer 0 plus a vcc via 0 to 1 was ADMITTED, because both rows sit on a layer some via reaches. Narrowing a refusal is a DELETION - it drops every case the old form caught for reasons the new form does not model, and nothing fails when it happens because the dropped cases are the ones no witness named. Same-layer duplication is now its own cause, and the same probe refuses. DECLARED: via reachability is the WEAK form - each realized layer must be touched by some via of that net, but the vias are not required to connect those layers into one component, so a net on layers 0,1,2,3 with vias 0-1 and 2-3 passes and is still two islands. Via geometry is absent entirely. 15 witnesses green by execution. * Copper: real connectivity, retained evidence, and a name that matches the object Four corrections, all of them modeling defects this branch shipped and its approvals did not catch. Modeling accuracy outranks the approved shape. 1. TWO ISLANDS ADMITTED. net_split_is_unrouted asked only whether every realized layer was TOUCHED by some connection of its net, and said so in a rung note. A net on layers 0,1,2,3 joined 0-1 and 2-3 satisfied that and is two electrically separate conductors. It is now the real question: reachability from each realized layer, expanded to a fixpoint over the net's own connections, refusing unless every realized layer lands in one component. The iteration bound is the realization count, which is exact rather than a guess -- each pass adds an ordinal or the set is closed, and the set cannot exceed the realized layers. Asked from every realized layer rather than a chosen seed, so no sentinel head extraction is needed. Proven by sabotage: restoring the weak form turns w_two_islands_of_one_net_refuse FAIL while the bridged case still passes. 2. THE ADMITTED VALUE DROPPED THE CONNECTIONS IT JUDGED. admit_copper read the connection population to decide the verdict and returned only the realizations, so two different connection populations justified one admitted result and no renderer, DRC or projection could recover which joins made the split nets whole. AdmittedCopper is now a sole_constructor record carrying board, realizations and connections, minted at one admit_callers-sealed site. 3. AN ENDPOINT ON A LAYER THE NET DOES NOT OCCUPY ADMITTED. Every check a connection faced was about the layer -- does this board have it, does it belong to this stackup -- and none about the join. A VCC connection could terminate where no VCC copper exists. New counted refusal InterlayerConnectionEndpointHasNoConductor, naming net and ordinal. 4. IT WAS NOT A VIA. The object carries a net and two layer references and no coordinate, drill, annular ring, span, plating or keepout. Calling it Via invites a renderer to draw a hole no fabricator could build. Renamed InterlayerConnection throughout; ManufacturableVia is the later carrier once geometry is grounded. 19 witnesses PASS (4 new). Compile gate contributes no diagnostic naming any pcb file; the 41 pre-existing Empty diagnostics are in src/v2/lens/complexity_accumulator_copy/analyze.dag, untouched here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the duplicated match arm and the comment vias made false review 52813 (claude-opus-4-7): NetHasTwoConductorsOnOneLayer was written twice in one RED control - a copy-paste artifact the substrate accepted because a second arm for a variant already matched is unreachable rather than illegal. Deleted; 19 witnesses still pass. review 52810 (cursor): the comment above realizations_of_net still said a split net with vias was something this increment does not model, which InterlayerConnection makes false. Rewritten to say what the two refusals now separate: same-layer duplication is a fork, multi-layer presence is a connectivity question. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Unbreak the doc graph's dangling half: two links that pointed at nothing (#8358) Main is red on doc reachability and has been for four consecutive runs. Two distinct causes; this fixes the one that is decidable without guessing. DANGLING LINK 1 - a relative-path defect, not a missing file. docs/plans/effect-namespace-grants.md linked to docs/plans/node-subtree-visibility-grants.md, which EXISTS - but the link was written repo-root-relative from inside docs/plans, so it resolves to docs/plans/docs/plans/... and lands nowhere. Broken on GitHub too, for anyone who clicked it. Now relative to the file that carries it. DANGLING LINK 2 - a target no commit has ever added. docs/probes/root_b_primitive_repr_fork_2026-08-16.md, landed by #8337, cites docs/plans/self-host-cargo-refusal-root-partition.md. That path is in no commit in this repository. I did not invent the document and did not guess which existing plan was meant: the citation survives as text naming the plan and stating that the link pointed at a file which does not exist, so the intent is preserved and the false link is gone. If the plan exists under another name its author can restore the link in one edit. MEASURED: doc_graph_has_no_dangling_links goes FAIL to PASS. WHAT THIS DOES NOT FIX, stated rather than left for the next reader to rediscover: doc_graph_has_no_orphan_docs still fails. Two probe docs carry no HandAuthoredDocBind row in gunbc.doc_graph_roots - class_b_trim_pool_coincidence_receipt and root_b_primitive_repr_fork_2026-08-16. A bind row must name the .dag work the document binds to, which is a statement about whose evidence supports which declaration. Authoring that for another session's probe would be guessing at their modeling, so those two rows are owed by their authors rather than supplied here. Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Root K: variant qualification without a use-line — 109 of 132 sites are Name::Variant paths in pattern and nested-argument positions (#8351) * Root K: admit a parent-enum import from its authored variant, not from the parent's own spelling The emitter qualifies a variant by its parent (`Parent::Variant`) in patterns and nested constructions, at sites where the .dag source spells only the VARIANT. The authored-source gate inside `reference_derived_use_lines` asked whether the PARENT was spelled in the module, so every such parent's use-line was refused and the emitted `Parent::Variant` had no import — 109 of Root K's 132 sites. Measured, not assumed. Compiling `v2.lens.complexity_accumulator_copy.analyze` (86-file closure, gunbc built from this tree): - 7 distinct parent enums appear as qualified heads while the .dag source contains ZERO occurrences of any of their names. - Opening the gate outright admitted 6 of the 7 (EdgeLabel, NamedEdgeTargetLookup, NodeKind, LetBindingFact, Outcome, ParseSubtreeFind) — so collection was never the wall, the gate was — and ALSO admitted AuthoredTokenOrdinal and FiniteSet, neither of which the module references: exactly the fabrication class the gate exists to refuse. So the gate is not relaxed, the question is corrected. A parent-enum candidate is admitted when an authored VARIANT of that same enum is spelled, and only on the UNAMBIGUOUS binding: `derive_variant_to_enum` maps a variant shared by two enums to the empty string, so a homonym variant admits NEITHER enum rather than picking one. After: unimported qualified-head sites across that closure 56 -> 19 (31 -> 7 in the module itself), no file worse, and both fabricated names stay absent. Regen reaches a fixed point with no seed drift — v1 seed modules are HostNative import-bearing and receive [] from this pass, confirmed by execution. Residue, declared not hidden: a corpus-wide ambiguous variant leaves its parent unimported even where the emitter qualifies it from the scrutinee type, and a parent reached by neither its own spelling nor an unambiguous authored variant (measured: `Behavior`) stays unsynthesized. Both refuse rather than fabricate. Dissolve-on is the one the text gate already carries: derive use-lines from the module's bound-reference structure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Carry the rationale as an annotation, and re-check the fix with a two-arm artifact diff Two changes, neither altering emitter behaviour. DESIGN 4c: the two `data NAME_note: String` rows this change introduced are the misplaced form — a String declaration whose sole purpose is commentary. Both are converted to leading `//` blocks above the declarations they explain. Both paths are outside `prose_row_migration_scope` (checked against all 262 entries), so this was not forced by the gate; it is the form DESIGN asks for. The dated measurement moves out of the tree entirely and lives in the commit and PR, where it cannot rot. The variant-induced arm also stops minting a dissolution condition of its own: it dissolves with the text gate it corrects, on the trigger `reference_derived_authored_source_gate_note` already declares. RE-CHECK, prompted by a sibling lane's finding that a fix's removed output can be load-bearing for an unrelated consumer — a class no refusal-counting instrument can see, because nothing refuses. An error histogram cannot distinguish unmasking from new emission, so I diffed the emitted ARTIFACT across both arms at the same entry and the same commit (identical closure by construction — no module-count mismatch): use-lines added 33 use-lines removed (line grain) 4 names lost (name grain) 0 <- the 4 are the same lines rewritten with MORE names files whose NON-import body changed 0 glob variant clashes, 256 emitted enums 0 So the change is purely additive at name grain and touches nothing but imports. Unimported qualified-head sites stay at 19 (from 56), confirming the annotation conversion changed no emitted behaviour. regen --verify: regen_divergence_count=0. All five witness controls still PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Say what the gate now admits: the note described one arm while the code had two review 52768 (cursor/composer-2.5, REQUEST_CHANGES) found the typed carrier contradicting its own implementation. Verified: after Root K the gate decision is reference_derived_candidate_authored, a disjunction, while reference_derived_authored_source_gate_note still opened "only when the candidate name appears in this module's authored source text" — false as written — and the new annotation cited that note as its dissolution anchor, so the citation pointed at text denying the change. DESIGN section 3 stale-citation, in the carrier a reader consults to learn what the gate does. The note now states both attesting forms (direct spelling; variant-induced, where a unit-only enum is admitted by an unambiguously-binding spelled variant), the homonym refusal that makes the second arm fail-closed (derive_variant_to_enum maps a shared variant to the empty string, so it never equals the enum name), and the declared residue both arms still refuse. The AuthoredTokenOrdinal receipt gains the reason it cannot be readmitted: it is a record, not a unit-only enum -- verified against dag/std/occurrence_identity.dag rather than asserted. Also completes the sibling witness note, which named the direct predicate as "the" gate law. Not false, but incomplete in a live carrier -- the file a session greps to learn the surface, so it silently invited re-deriving an arm that already exists. It now scopes itself to the direct arm and points at the second witness. Asked the directive question separately from the mention grep: no plan carrier instructs anyone to extend the single-arm behavior. Receipts, by execution: 8 of 8 witnesses PASS across both files. regen fixed point confirmed the hard way -- regenerate, rebuild the seed from the new mirror, regenerate again, byte-identical (md5). Emitted delta is exactly one line, the note value, with no behavioral change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the residue class this gate cannot reach, measured rather than reasoned The residue clause added in 5678180 said the remaining sites are "refused by both arms." Two of the three residual enum heads are not refused — they never reach the arms. Behavior's variant Transform is spelled bare in a pattern position in an import-free module and binds unambiguously, so the variant-induced arm's preconditions hold, and no use-line is emitted anyway. Established by execution, not inference: forcing the gate to admit unconditionally, regenerating, rebuilding the seed, and re-emitting v2.lens.complexity_accumulator_copy.analyze still yields no Behavior use-line. The gate is a filter over a candidate set, so a name the collector never proposes cannot be admitted by any gate decision. The homonym explanation was checked and refuted first -- Transform, Loop and OpBitCast each belong to exactly one enum. That distinction matters because the two classes have different fixes and only one of them lives here. The clause now separates refused-here from never-reaching-here and points the remaining work upstream at the candidate producer, which is where the existing dissolve-on already aims. Pre-existing and unchanged by Root K: Behavior:: occurs 7 times in both the base and fix arms. No regression, and the probe was reverted before this commit -- the tree was clean, and this diff carries only the note. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Root D half 1: a zero-parameter alias is emitted carrying its resolved definition's arguments (~73 sites) — and an enrolled witness asserts the broken shape (#8350) * Stop discarding the TypeEnv at the applied-binding renderer, so the closed-alias peel can answer A reference to a zero-parameter alias reaches the emitter carrying the RESOLVED DEFINITION's type arguments as its children, while its authored spelling is still the alias name. A renderer that prints name-plus-children therefore emits ClosedCarrierAlias<ProbeQuantity, ProbeScale, ProbeMagnitude> for a Rust alias declared with no parameters at all -- E0107, "type alias takes 0 generic arguments but 3 were supplied". Four renderers already refuse that shape by asking the one peel authority rust_fn_sig_peel_closed_alias. render_rust_type_with_applied_binding is the fifth path and it was not missing the guard: it reaches render_rust_applied_type, which asks, and was answered with an EMPTY TypeEnv the function constructed inline, plus an empty_emit_graph_info() it handed to render_rust_type. An empty env resolves no binding, and the peel predicate returns false for "I could not look this up" exactly as for "this declaration has parameters" -- so the unanswerable case widened into the applied form instead of refusing. Every one of its twelve callers already held the TypeEnv it was throwing away. So this passes it through rather than adding a check: the peel authority stays the single authority and is simply told the truth. Measured with an instrumented seed on the minimal fixture: base="ClosedCarrierAlias" children=3 envbindings=0. The witness that covered this fixture asserted the broken shape and was green, so the defect had a defender. It now asserts the emitted declaration and the bare use site together and excludes the applied spelling, which is a pair that has to agree. The next rung is upstream and deliberately not taken here: an alias reference that preserved its AUTHORED arity would make the shape unwritable rather than refused, and then no renderer would need to ask. * Drop the trailing semicolon that made the new note an item-declaration parse error A .dag data declaration is terminated by the newline, not by a semicolon. The trailing ; put a second, empty item where the parser expected a declaration, so 05_emit_rust.dag stopped parsing at that point -- which is why the regen job reported 'expected item declaration', then 26 orphaned source annotations and three unresolved v1.compiler.emit_rust imports downstream of it. One cause, 29 diagnostics. * Regenerate the stage0 seed for the applied-binding env change Mechanical output of regen_stage0 over the edited .dag, not hand-written. One file changes, v1_compiler_emit_rust.rs, +34/-45: the twelve callers gain env.clone(), the signature gains the parameter, and the two inline empty TypeEnv literals collapse into it -- which is where the 45 deletions come from. Round 2 over the rebuilt seed produces a byte-identical diff to round 1, so the self-host fixed point settles in one round rather than oscillating. MEASURED, on the emitted closures rather than on the fixture alone: src/v2/lens/coverage.dag 39 applied-use sites -> 0 src/v2/compiler/03_ingest.dag 74 applied-use sites -> 1 The fixture now emits the declaration and the use site in agreement: pub type ClosedCarrierAlias = Rc<Root4AliasCarrier<ProbeQuantity, ProbeScale, ProbeMagnitude>>; pub fn witness(items: Rc<Vec<ClosedCarrierAlias>>) -> Rc<Vec<ClosedCarrierAlias>> THE ONE REMAINING SITE IS NOT CLOSED AND IS NOT THIS ROOT. std_integer.rs emits pub type PositiveInt = Rc<Nat<Magnitude>>; from type PositiveInt = Nat where gt_zero, where dag/std/nat.dag declares type Nat = CommutativeSemiring<Magnitude> with no parameters. Same symptom class, different cause: that path is render_rust_alias_rhs_type, which already holds a real env and asks alias_base_is_zero_param_decl -- so the failure is that the lookup does not find Nat under the resolved def_mod, and that predicate's Absent arm also answers false. The conflation is the same shape one layer over; the cause is module resolution across two same-named nat modules, which this change does not touch. Stated as located residue, not as a fix. --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * Doc graph: one bind per document — drop the duplicate Root B probe row (#8364) main at 8a346ec3 carries two HandAuthoredDocBind rows with home ProbeDoc and slug root_b_primitive_repr_fork_2026-08-16, so both derive the key probe/root_b_primitive_repr_fork_2026-08-16, hand_authored_key_collision_count is nonzero, and doc_graph_bind_identities_unique fails. main is red. Not a bad merge: two lanes independently authored a bind for the same document. 76d64357 (#8362) bound the probe; 8a346ec3 (#8333, mine) bound it again while landing the plan it cites. The rows are not identical, so the resolution is a content judgement rather than a dedupe. Deleted MINE and kept #8362's, which is the strictly more informative of the two: it names rust_seed_host_numeric_alias as an additional work, and its dissolution states the specific condition — RustCorpusRepr's two fused axes split into independent facts — where mine restated roughly the same idea with no second work and a looser trigger. That is also the condition eager-deer's Root B cut (#8357) is actually executing against, so the surviving row is the one a reader can act on. Claude-Session: https://claude.ai/code/session_01FwPMTY6Myy3scaMNn33cg5 Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Root D half 2: delete the Witness checkpoint-scalar rows, derive scalar arity from its single authority (#8341) * Root D receipt: E0107 generic-arity root-caused to the checkpoint-scalar arity strip Witness is registered as a Rust checkpoint scalar while std.types records arity 1, so every Witness<T> in type position loses its argument. Measured live on 06_translate and localised by probe-then-revert instrumentation of the generated emitter. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Root D half 2: delete the Witness checkpoint-scalar rows and derive scalar arity from its single authority extdeps.languages.rust.types carried { dag_name: Witness, target_type: Witness } and a lowercase twin. A TypeCheckpoint row states target SPELLING and cannot state arity, so membership of that table is read by v1.compiler.05_emit_rust rust_render_checkpoint_scalar_bare as the proposition 'arity 0 in Rust' — the E0109 phantom-param wall. Witness is the generic enum v2.std.witness.Witness<C>, arity 1 by std.types container_type_arity, so every Witness<T> in type position lost its argument and emitted as Rc<Witness>: rustc E0107 'missing generics for enum Witness'. Delete the rows, and consult the declared-arity authority before the strip so no leaf with declared arity can be classified a checkpoint scalar however the spelling table is later edited. Measured on src/v2/compiler/06_translate.dag, same route and same single entry on both sides: E0107 21 -> 17, the four Witness sites gone, every other error code identical. The dag/std/integer.dag closure is byte-identical, which is the collateral control. Witness: dag/test/claim/root_d_checkpoint_scalar_declared_arity_witness_test.dag — green with the change, red with the change reverted and the binary rebuilt. Receipt: docs/probes/root_d_generic_arity_2026-08-16.md Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Escape the braces in rust_checkpoint_scalar_arity_note so the emitted prose reads Present{false} Review 52707 caught it: an unescaped {false} inside a data String is a format placeholder, so the generated projection was a format!(...) call rendering 'Presentfalse'. Escaped as \{false\}; the regenerated extdeps_languages_rust_types.rs now carries a plain literal with no format! at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Add the two-arm artifact diff over the full 06_translate closure Per smart-ram-730's re-check: a per-code histogram cannot distinguish unmasking from newly introduced emission, and a defect's output can be load-bearing for an unrelated consumer. Diffing the emitted trees instead: 91 files both arms, 2 differ, 8 lines = the 4 targeted Witness sites and nothing else. Same entry both arms, so M is fixed by construction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Re-take the before-arm from a detached worktree at the merge-base SHA Section 9's arm was defended by chronology, which is an account rather than an audit: an emit reads the working tree, so an uncommitted edit leaves no trace a timestamp reveals. Re-taken from git worktree add --detach 5e1a73fa339, zero dirty tracked files, real compile output. Byte-identical to the original before-arm (0 files differ), same 2-file/8-line delta to the after arm, and the introduced construct Witness<T> is absent from the base arm — the WHAT read that a timestamp cannot give. Also records that the same include counts 1 -> 5 tree-wide against 0 -> 4 per-file, so scope is stated with the number. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Bind the Root D probe receipt so it is not a doc-graph orphan docs/probes/root_d_generic_arity_2026-08-16.md was introduced by this PR with no inbound markdown link. The doc graph reaches documents only through `](...)` edges from ROADMAP.md / DESIGN.md / docs/runbooks/README.md plus the typed HandAuthoredDocBind extra roots, so a probe cited exclusively from `.dag` carrier prose -- which is how the three notes in this PR cite it -- is unreachable and `doc_graph_has_no_orphan_docs` reds. Discriminated by execution rather than by reading, because main currently carries an unrelated orphan that reds the SAME row name: this worktree does not contain that file at all, and the witness FAILS with the probe present and PASSES with it moved aside. The defect is this PR's, not the one inherited from main, and it is not an unrelated fix riding a single-seam PR. Bound at subject grain per the existing ProbeDoc precedent: primary_work is the guard this probe measures, additional_works the table whose rows it removed. The retirement names the identity-keying change that makes both halves the probe localises structurally unreachable, at which point row and probe delete together. doc_graph_has_no_orphan_docs, doc_graph_has_no_dangling_links, doc_graph_works_refs_carry_symbols, doc_graph_bind_identities_unique, doc_graph_hand_authored_slugs_not_registered and production_doc_binds_all_carry_a_retirement all PASS locally. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key (#8334) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `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` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- 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 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. 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. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector file is what makes a success evidence about the modeled key, so a path naming a file that does not exist -- or one holding a DIFFERENT public key -- silently removes the exactness the option set was chosen for. A path string is not a selector; the bytes are. `AgentSelectorFile` is now `sole_constructor` with one production mint, `materialize_agent_public_selector`, which writes the declared public key line, reads it back, and seals only when the content identities agree -- the same write/readback/compare construction `KnownHostsAnchor` already uses, for the same reason. `classify_agent_key_listing` takes the sealed value, so a literal path cannot reach the mint at all. The path is attempt-owned, as the anchor path is: two concurrent runs must not write one another's selector, and a stale file from another attempt must never be readable as this one's. The probe threads its attempt identity through and refuses before any observation when that identity is not a safe path segment. The file carries PUBLIC material only. The private half stays in the agent and is never written by this module. The hermetic witness fixture is admitted to the seal explicitly, exactly as the known-hosts anchor admits its own -- a witness has no filesystem, and what the seal buys is that no OTHER module can hand the classifier a path it merely named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the trust-free Spark credential locus: the runner route builds a sealed context (#8336) `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back (#8339) * Delete the trust-free Spark credential locus: the runner route builds a sealed context `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back typed_remote_file_write_authority_note reserved a convergence arm and said what it would take: "A zero tee exit proves only that the remote process accepted stdin — not that bytes landed at the declared path with declared mode. A future TypedRemoteFileWriteConverged variant requires independent read-back (operator ruling msg_71f67aa9); stage-and-rename + mode + read-back land before that arm is writable." This is that arm. FOUR STEPS, AND THE ORDER IS THE PROPERTY. Stage to a sibling path, set the mode there, `mv -f` within the one directory (POSIX-atomic), then read the DESTINATION back and compare. Writing straight to the destination and chmod-ing afterwards publishes incomplete bytes under the real name; on a unit file that is a window in which systemd can read something that was never a valid unit. Each step's failure is located by name, so a converge that stops says which invariant did not hold rather than returning one opaque false. dd status=none, NOT tee. tee copies stdin to stdout, so every byte written is echoed back across the channel and into whatever captures it. That doubles transfer and puts file content in the run log -- for a credential or config file that is a disclosure, not a style preference. READ-BACK BY CONTENT, NOT BY DIGEST, and the reason is a real constraint rather than a shortcut: a digest comparison needs a digest of the INTENDED bytes, and .dag has no SHA-256 over a String -- extdeps.crypto.hash Digest carries a hex its caller supplies. Comparing a remote sha256sum of the staged file to one of the destination would prove the rename moved the same bytes while saying nothing about whether those bytes were the ones declared, which is the whole question. Reading the file back answers it directly, and the comparison happens in the model where a witness can exercise it. The comparison is exact. Normalizing trailing whitespace would let a real difference pass, and a file whose trailing bytes differ from the declared content is not the file that was declared. Mode is a closed two-arm enum rather than an octal string, so a nonsensical mode has no constructor. Admission is unchanged and still governs: a path outside the declared scope produces no admitted write, hence no staging path and no steps. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the attempt-identity match one expression per arm Review 52733 (cosmetic): the credential gate was a `match` nested inside the attempt-identity `match` but indented back to the outer column, which parses fine and reads as though the outer match had ended. It was an artifact of patching the gate in rather than a shape anyone chose. The gate moves to `spark_managed_access_standing_for_attempt`, so each arm of the outer match is one expression and the nesting is visible in the call structure instead of hidden by indentation. No behavior change: same three verification arms, same refusal reasons, same order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included (#8356) * Plan all four serving members, not only linger `spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an untranslatable planned member instead of dropping it `fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the declared-residue annotation to module-item grain The comment sat inside `spark_serving_fleet_converge_plan_artifact`'s body, which DESIGN 4c does not model: annotations attach at module-item grain only. The compile-clean gate located it exactly; `gunbc compile --target dag` does not run that gate, which is why it passed locally. Same text, moved above the declaration it describes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com> * Model the systemd unit file so a Spark serving unit can become bytes (#8361) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `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` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- 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 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. 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. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector…

#8366) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `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` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- 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 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. 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. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector file is what makes a success evidence about the modeled key, so a path naming a file that does not exist -- or one holding a DIFFERENT public key -- silently removes the exactness the option set was chosen for. A path string is not a selector; the bytes are. `AgentSelectorFile` is now `sole_constructor` with one production mint, `materialize_agent_public_selector`, which writes the declared public key line, reads it back, and seals only when the content identities agree -- the same write/readback/compare construction `KnownHostsAnchor` already uses, for the same reason. `classify_agent_key_listing` takes the sealed value, so a literal path cannot reach the mint at all. The path is attempt-owned, as the anchor path is: two concurrent runs must not write one another's selector, and a stale file from another attempt must never be readable as this one's. The probe threads its attempt identity through and refuses before any observation when that identity is not a safe path segment. The file carries PUBLIC material only. The private half stays in the agent and is never written by this module. The hermetic witness fixture is admitted to the seal explicitly, exactly as the known-hosts anchor admits its own -- a witness has no filesystem, and what the seal buys is that no OTHER module can hand the classifier a path it merely named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the trust-free Spark credential locus: the runner route builds a sealed context (#8336) `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back (#8339) * Delete the trust-free Spark credential locus: the runner route builds a sealed context `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back typed_remote_file_write_authority_note reserved a convergence arm and said what it would take: "A zero tee exit proves only that the remote process accepted stdin — not that bytes landed at the declared path with declared mode. A future TypedRemoteFileWriteConverged variant requires independent read-back (operator ruling msg_71f67aa9); stage-and-rename + mode + read-back land before that arm is writable." This is that arm. FOUR STEPS, AND THE ORDER IS THE PROPERTY. Stage to a sibling path, set the mode there, `mv -f` within the one directory (POSIX-atomic), then read the DESTINATION back and compare. Writing straight to the destination and chmod-ing afterwards publishes incomplete bytes under the real name; on a unit file that is a window in which systemd can read something that was never a valid unit. Each step's failure is located by name, so a converge that stops says which invariant did not hold rather than returning one opaque false. dd status=none, NOT tee. tee copies stdin to stdout, so every byte written is echoed back across the channel and into whatever captures it. That doubles transfer and puts file content in the run log -- for a credential or config file that is a disclosure, not a style preference. READ-BACK BY CONTENT, NOT BY DIGEST, and the reason is a real constraint rather than a shortcut: a digest comparison needs a digest of the INTENDED bytes, and .dag has no SHA-256 over a String -- extdeps.crypto.hash Digest carries a hex its caller supplies. Comparing a remote sha256sum of the staged file to one of the destination would prove the rename moved the same bytes while saying nothing about whether those bytes were the ones declared, which is the whole question. Reading the file back answers it directly, and the comparison happens in the model where a witness can exercise it. The comparison is exact. Normalizing trailing whitespace would let a real difference pass, and a file whose trailing bytes differ from the declared content is not the file that was declared. Mode is a closed two-arm enum rather than an octal string, so a nonsensical mode has no constructor. Admission is unchanged and still governs: a path outside the declared scope produces no admitted write, hence no staging path and no steps. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the attempt-identity match one expression per arm Review 52733 (cosmetic): the credential gate was a `match` nested inside the attempt-identity `match` but indented back to the outer column, which parses fine and reads as though the outer match had ended. It was an artifact of patching the gate in rather than a shape anyone chose. The gate moves to `spark_managed_access_standing_for_attempt`, so each arm of the outer match is one expression and the nesting is visible in the call structure instead of hidden by indentation. No behavior change: same three verification arms, same refusal reasons, same order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included (#8356) * Plan all four serving members, not only linger `spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an untranslatable planned member instead of dropping it `fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the declared-residue annotation to module-item grain The comment sat inside `spark_serving_fleet_converge_plan_artifact`'s body, which DESIGN 4c does not model: annotations attach at module-item grain only. The compile-clean gate located it exactly; `gunbc compile --target dag` does not run that gate, which is why it passed locally. Same text, moved above the declaration it describes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the systemd unit file so a Spark serving unit can become bytes SparkServingUserUnitSpec is typed fields and deliberately not systemd INI syntax. That left a gap rather than a decision: nothing could turn the spec into a file, so WriteUserUnitFile had no bytes to deliver and the unit member had nothing to be observed against. extdeps.systemd.unit_file models the format, cited to systemd.unit(5) and systemd.service(5). One directive type per section, so `ExecStart=` in [Unit] and `WantedBy=` in [Service] have no representation -- the misplacement class is structurally impossible rather than validated. The file is a record of three sections, so a transposed or duplicated section is likewise unwritable. extdeps.ollama.server_env owns OLLAMA_HOST / OLLAMA_MODELS. They previously appeared in the tree only inside a prose comment, so any consumer had to spell the literals itself -- a second authority for ollama's own names. gunbc.spark_serving_unit_render maps the spec onto that authority and is the single rendering, so the write side and the observe side cannot drift into two renderings of one spec and report a permanent MemberChanged against itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the two new extdeps modules in scope_carrier_paths The placement gate refused: a new dag/extdeps file must both declare extdeps_model_scope AND join scope_carrier_paths. Both modules already declared the scope; neither was rostered, and the frozen legacy manifest is not a landing state for a new file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Realize WriteUserUnitFile: widen remote operations to carry file bytes The realizer produced List<List<String>> -- argv and nothing else -- so WriteUserUnitFile was UNREALIZABLE rather than unimplemented: a file write is bytes, bytes ride stdin (there is no sh -c arm), and no argv-shaped verdict could express it. The refusal was reporting a missing type. RemoteOperation = RemoteArgv | RemoteFileBytes, each carrying an already-sealed payload. There is no command-string or script-body arm; the absence of that constructor is what keeps the typed-write module's guarantee shut. The outcome carrier had to widen too. converge_typed_remote_file answers in its own type, and coercing it into TypedArgvExecOutcome would mean inventing an exit code and a stdout it never had -- a fabricated plausible output at the seam that decides whether the sequence continues. Both map into RemoteOperationOutcome. A file write refuses on any non-FleetSsh transport by construction: the convergence needs the SshTarget and sealed context, and SshShell has neither. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Dissolve two Bool predicates; refresh two stale authority notes Review 52874, all four findings. The predicates were parallel discriminator surfaces over coproducts that already discriminate. `remote_operation_succeeded` had one caller, an `if` in the sequence step, which now matches the outcome directly. `remote_operation_is_file_write` had two, both of which match directly now; the count folds through a match rather than a Bool filter. The two authority notes described the argv-only world this PR replaced -- "portable remote argv" and "an ORDERED SEQUENCE of portable remote argvs" -- while the code had already gained a file-bytes kind. A machine-carried note asserting a superseded mechanism is the stale-authority class, and it sat in the modules whose behavior changed. Both now state the two kinds, the per-kind dispatch, the FleetSsh-only refusal for file writes, and why the outcomes are mapped rather than coerced. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Create the unit's parent directory, so a bare host can actually be written WriteUserUnitFile realized to a single RemoteFileBytes, but ~/.config/systemd/user does not exist on a machine that has never run a user unit, and the file convergence opens a staging sibling with `dd` -- it does not create missing parents. The first step therefore refused on exactly the bare host this effect exists to restore, so the PR had not realized the effect for its declared first consumer. The effect now realizes to two ordered operations: a non-privileged `mkdir -p` of the modeled directory, then the file bytes. sudo would be an unnecessary privilege escalation for a write under the executor's own home, and `-p` keeps it idempotent across repeated converges. The absolute directory is a function in the install-path authority rather than string surgery on the unit path inside the realizer -- one fact, one derivation, and one that does not break if the unit basename ever gains a separator. Witnesses assert POSITION, not just counts: a count-only claim is satisfied by any permutation, including the one that puts the write before its own directory. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare the symbols these modules use, instead of resolving by pool coincidence Review 52902. spark_serving_converge_apply used RemoteOperation and its arms, the RemoteOperationOutcome arms, all four HostEffectTransport variants, and the typed-file-write constructors while importing none of them -- its import block was still the argv-only one. It compiled anyway, which is the point: bare cross-module references resolve when some unrelated import elsewhere in the assembled closure has already dragged the target module into the pool. That is accidental coverage, not declared dependency, and it breaks under a narrower closure -- exactly what the scoped compile-clean gate builds on an all-.dag diff. Swept the class rather than the site: spark_serving_converge_realize matches thirteen ServingInstallEffect variants and imported three. The other ten resolved the same accidental way, and this PR added an eleventh use. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Stop claiming both RemoteOperation arms carry a sealed payload They do not, and the difference is exactly where the guarantee stops. RemoteFileBytes carries a TypedRemoteFileWrite whose sole mint checks path containment and far-side portability, so its payload cannot be forged. RemoteArgv carries a bare List<String>: the type does NOT make an arbitrary argv unwritable. What actually holds for argv is upstream and downstream -- the realizer admits words through portable_remote_words and both SSH execution seams re-check them -- so it is a property of those paths, not of this constructor. Claiming the constructor for it invites a reader to skip checking the paths that carry it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>

…ation, and the credential-bound privilege bootstrap (#8377) * Verify the fleet SSH credential against the identity file, instead of declaring it `FleetSshCredentialBinding` names which credential an SSH leg authenticated with. On the identity-file route nothing established that name: the mint took `identity_file` and `public_material` as two independent parameters and hashed the second, so `spark_credential_workflow` fetched Secret Manager versions/1 into a file and then asserted the file held `fleet_automation_ssh_key.material` without ever reading it. A rotated secret, a wrong pinned version, a truncated fetch or a bad materialization all produce the same binding and the same receipt -- the check was satisfiable by editing the declaration while the realization lied. The corpus already knew the question: `gunbc.ci_spec` `gunbc_ci_fleet_key_agent_script` derives the public key with `ssh-keygen -y` and compares its fingerprint, in hand-authored GitHub Actions shell, on the OTHER route. Two answers to one question and one of them unfounded. `gunbc.fleet_ssh_credential_verify` becomes the single authority. Observation and judgment are separated: `classify_derived_public_key_line` is pure and total over the process observation, so every arm is reachable hermetically, and the effectful half only runs the command. The mint is admitted to the classifier alone and the unverified route is deleted, so a binding cannot exist without a derivation that produced the material being hashed. Fail-closed by consequence rather than by special case: a zero exit with empty or unexpected output is a mismatch, because the empty string neither equals the expected line nor carries it as a prefix. The trailing-space form admits ssh-keygen's optional comment while refusing a longer material that merely carries the expected one as a prefix. The hermetic fixture now goes THROUGH the classifier rather than around it -- there is no other mint, so it must present a synthetic derivation that matches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Represent and verify the agent-held fleet credential, so the runner route can carry trust facts The identity-file route was the half that asserted its credential; the agent route had the same defect in a second place and one more besides. `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` named a key nothing had observed -- and the probe's legs run over `typed_argv_probe_over_ssh` with no anchor, no credential and no posture at all. The root cause of the second half is a representation gap: `FleetSshCredentialBinding` required an `identity_file`, an agent-held key has none, so the CI route could not build one and `SparkServingSliceRunnerAgent` fell back to a bare `SshShell`. WHERE the private half lives becomes a `FleetSshCredentialLocus` coproduct (identity-file | agent-held) carried INSIDE the still-sealed binding record. The seal does not move onto the coproduct deliberately: `sole_constructor` seals a record, so making the binding itself a coproduct would have made every arm publicly constructible and dropped the wall. A forged locus is inert; a forged binding would be a credential claim nobody observed. The agent arm is verified against the agent's own listing: `ssh-add -l` on an explicitly named socket, matched against `fleet_automation_ssh_key_fingerprint` -- 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 (no identities) and exit 2 (cannot connect) both refuse, and an empty listing on a zero exit is a mismatch by the same construction as the identity-file arm. `openssh_exact_agent_credential_options` is the agent posture. `IdentityFile` is not redundant there and does not name a private key: with `IdentitiesOnly=yes` it is what selects one identity out of an agent that may hold several, which is what keeps a success evidence about the modeled key. 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. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Materialize and read back the agent selector file, so IdentitiesOnly selects an observed key The agent arm shipped with `public_selector_file` as a path a caller passed in, and nothing established that anything was at it. That is the same shape as the defect the arm was built to close, one level down: with `IdentitiesOnly=yes` the selector file is what makes a success evidence about the modeled key, so a path naming a file that does not exist -- or one holding a DIFFERENT public key -- silently removes the exactness the option set was chosen for. A path string is not a selector; the bytes are. `AgentSelectorFile` is now `sole_constructor` with one production mint, `materialize_agent_public_selector`, which writes the declared public key line, reads it back, and seals only when the content identities agree -- the same write/readback/compare construction `KnownHostsAnchor` already uses, for the same reason. `classify_agent_key_listing` takes the sealed value, so a literal path cannot reach the mint at all. The path is attempt-owned, as the anchor path is: two concurrent runs must not write one another's selector, and a stale file from another attempt must never be readable as this one's. The probe threads its attempt identity through and refuses before any observation when that identity is not a safe path segment. The file carries PUBLIC material only. The private half stays in the agent and is never written by this module. The hermetic witness fixture is admitted to the seal explicitly, exactly as the known-hosts anchor admits its own -- a witness has no filesystem, and what the seal buys is that no OTHER module can hand the classifier a path it merely named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the trust-free Spark credential locus: the runner route builds a sealed context (#8336) `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back (#8339) * Delete the trust-free Spark credential locus: the runner route builds a sealed context `SparkServingSliceCredentialLocus` had two arms. The second, `SparkServingSliceRunnerAgent`, was nullary and projected to a bare `SshShell { ssh_host: "user@host" }` -- no known-hosts anchor, no credential, no OpenSSH posture. Its own authority note said it "carries NO trust facts of its own; the job establishes them out of band". Every exactness property the fleet SSH machinery exists to hold was absent on the route that actually runs against the Sparks. It existed because of a representation gap rather than a decision: a binding required an identity file, an agent-held key has none, so the runner route could not build a context and had nothing to pass. With the agent-held locus and its verification landed, that arm stopped being a second KIND of run and became a second NAME for one, so it is deleted rather than kept beside what replaced it. With one arm left the coproduct was itself a nickname for `FleetSshExecutionContext`, so it is gone too and the helpers take the context directly. `prepare_spark_serving_agent_context` is what the CI entries now call: verify the named agent holds the declared fleet key, materialize the selector and the known-hosts anchor under attempt-owned paths, and refuse before any host is contacted if any step fails. The entries previously carried a trust_line reading "established by the runner job, not by this entry" -- an accurate sentence describing a precondition they had no way to check, so a job step that stopped materializing the anchor produced the same receipt and the same legs. That line is now the receipt of what this entry itself observed. Both CI entries therefore carry an attempt identity, because they now perform materializations that must not collide with another run's. The receipt's credential locus label is read off the sealed binding rather than chosen by the caller, so a run cannot claim a posture it did not obtain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converge a remote file: stage, mode, atomic rename, then read the destination back typed_remote_file_write_authority_note reserved a convergence arm and said what it would take: "A zero tee exit proves only that the remote process accepted stdin — not that bytes landed at the declared path with declared mode. A future TypedRemoteFileWriteConverged variant requires independent read-back (operator ruling msg_71f67aa9); stage-and-rename + mode + read-back land before that arm is writable." This is that arm. FOUR STEPS, AND THE ORDER IS THE PROPERTY. Stage to a sibling path, set the mode there, `mv -f` within the one directory (POSIX-atomic), then read the DESTINATION back and compare. Writing straight to the destination and chmod-ing afterwards publishes incomplete bytes under the real name; on a unit file that is a window in which systemd can read something that was never a valid unit. Each step's failure is located by name, so a converge that stops says which invariant did not hold rather than returning one opaque false. dd status=none, NOT tee. tee copies stdin to stdout, so every byte written is echoed back across the channel and into whatever captures it. That doubles transfer and puts file content in the run log -- for a credential or config file that is a disclosure, not a style preference. READ-BACK BY CONTENT, NOT BY DIGEST, and the reason is a real constraint rather than a shortcut: a digest comparison needs a digest of the INTENDED bytes, and .dag has no SHA-256 over a String -- extdeps.crypto.hash Digest carries a hex its caller supplies. Comparing a remote sha256sum of the staged file to one of the destination would prove the rename moved the same bytes while saying nothing about whether those bytes were the ones declared, which is the whole question. Reading the file back answers it directly, and the comparison happens in the model where a witness can exercise it. The comparison is exact. Normalizing trailing whitespace would let a real difference pass, and a file whose trailing bytes differ from the declared content is not the file that was declared. Mode is a closed two-arm enum rather than an octal string, so a nonsensical mode has no constructor. Admission is unchanged and still governs: a path outside the declared scope produces no admitted write, hence no staging path and no steps. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give the attempt-identity match one expression per arm Review 52733 (cosmetic): the credential gate was a `match` nested inside the attempt-identity `match` but indented back to the outer column, which parses fine and reads as though the outer match had ended. It was an artifact of patching the gate in rather than a shape anyone chose. The gate moves to `spark_managed_access_standing_for_attempt`, so each arm of the outer match is one expression and the nesting is visible in the call structure instead of hidden by indentation. No behavior change: same three verification arms, same refusal reasons, same order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included (#8356) * Plan all four serving members, not only linger `spark_serving_desired_members` builds the full desired population -- runtime root, user unit, primary model slot, linger -- and had ZERO production consumers. The live plan was `spark_serving_linger_membership_plan`, whose desired side is the single-element `[spark_serving_desired_linger_member(host)]`. Three of the four modeled members were never planned, so the install effects that act on them could never be SELECTED however well implemented. What was missing is the OBSERVED side. `spark_serving_observed_members` projects it from an observation, never from the desired release: deriving an observed digest from the desired one would make every member reconcile as converged by construction and the plan would always be empty. A refused observation refuses the projection rather than rendering as an empty population -- the empty-observation narrow, which would plan every member as an addition against a host nobody saw. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an untranslatable planned member instead of dropping it `fleet_converge_spark_serving_typed_actions` was a flat_map whose `Absent` arm returned the empty list, so a planned member action carrying no install effects was discarded and the artifact froze fewer typed rows than its own plan had actions, with no diagnostic. The only action reaching that arm is `MemberRemovalRefused` -- so the drop erased a refusal by silently succeeding. Its observed frequency was zero BY CONSTRUCTION: the only live plan is linger-only and linger always translates. A four-member plan is exactly the input that reaches it, which is why this closes before the plan widens. The refusal's cause is propagated but not carried: FleetConvergePlanArtifact? has no arm for one. Declared in-code as a bounded gap with its trigger -- the cutover widens that return type anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the declared-residue annotation to module-item grain The comment sat inside `spark_serving_fleet_converge_plan_artifact`'s body, which DESIGN 4c does not model: annotations attach at module-item grain only. The compile-clean gate located it exactly; `gunbc compile --target dag` does not run that gate, which is why it passed locally. Same text, moved above the declaration it describes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the systemd unit file so a Spark serving unit can become bytes SparkServingUserUnitSpec is typed fields and deliberately not systemd INI syntax. That left a gap rather than a decision: nothing could turn the spec into a file, so WriteUserUnitFile had no bytes to deliver and the unit member had nothing to be observed against. extdeps.systemd.unit_file models the format, cited to systemd.unit(5) and systemd.service(5). One directive type per section, so `ExecStart=` in [Unit] and `WantedBy=` in [Service] have no representation -- the misplacement class is structurally impossible rather than validated. The file is a record of three sections, so a transposed or duplicated section is likewise unwritable. extdeps.ollama.server_env owns OLLAMA_HOST / OLLAMA_MODELS. They previously appeared in the tree only inside a prose comment, so any consumer had to spell the literals itself -- a second authority for ollama's own names. gunbc.spark_serving_unit_render maps the spec onto that authority and is the single rendering, so the write side and the observe side cannot drift into two renderings of one spec and report a permanent MemberChanged against itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the two new extdeps modules in scope_carrier_paths The placement gate refused: a new dag/extdeps file must both declare extdeps_model_scope AND join scope_carrier_paths. Both modules already declared the scope; neither was rostered, and the frozen legacy manifest is not a landing state for a new file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Realize WriteUserUnitFile: widen remote operations to carry file bytes The realizer produced List<List<String>> -- argv and nothing else -- so WriteUserUnitFile was UNREALIZABLE rather than unimplemented: a file write is bytes, bytes ride stdin (there is no sh -c arm), and no argv-shaped verdict could express it. The refusal was reporting a missing type. RemoteOperation = RemoteArgv | RemoteFileBytes, each carrying an already-sealed payload. There is no command-string or script-body arm; the absence of that constructor is what keeps the typed-write module's guarantee shut. The outcome carrier had to widen too. converge_typed_remote_file answers in its own type, and coercing it into TypedArgvExecOutcome would mean inventing an exit code and a stdout it never had -- a fabricated plausible output at the seam that decides whether the sequence continues. Both map into RemoteOperationOutcome. A file write refuses on any non-FleetSsh transport by construction: the convergence needs the SshTarget and sealed context, and SshShell has neither. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Dissolve two Bool predicates; refresh two stale authority notes Review 52874, all four findings. The predicates were parallel discriminator surfaces over coproducts that already discriminate. `remote_operation_succeeded` had one caller, an `if` in the sequence step, which now matches the outcome directly. `remote_operation_is_file_write` had two, both of which match directly now; the count folds through a match rather than a Bool filter. The two authority notes described the argv-only world this PR replaced -- "portable remote argv" and "an ORDERED SEQUENCE of portable remote argvs" -- while the code had already gained a file-bytes kind. A machine-carried note asserting a superseded mechanism is the stale-authority class, and it sat in the modules whose behavior changed. Both now state the two kinds, the per-kind dispatch, the FleetSsh-only refusal for file writes, and why the outcomes are mapped rather than coerced. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Observe the unit file's bytes, so unit_observed can stop being false The live observer reads LoadState and is-active. Neither answers what the user unit member is keyed on: a unit can be loaded and active while its file on disk differs from the desired spec, which is exactly the drift the member exists to catch. So unit_observed was false, the unit planned as an addition on every run, and a second plan could never be empty. classify_observed_user_unit compares the read bytes against the single rendering. That is a real measurement, not a derivation from desired state: what is observed is a byte equality. Equal bytes establish the address holds the spec and carry the same digest; different bytes carry a digest OF THE OBSERVED CONTENT and reconcile as a change. A failed read is NOT absence. `cat` exits non-zero both when the file is missing and when it cannot be read, and only the first means the member is absent -- the remedies differ, so the two stay distinct states. systemctl is-enabled joins the extdeps authority: it is the INSTALL state, a different question from is-active, and asked of the user manager because a system-manager query answers about a different unit namespace. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * One identity domain for unit content, and consume is-enabled Three defects in the classifier, all found in review. IDENTITY DOMAIN. The equal-bytes arm returned the DESIRED spec's digest while the unequal arm hashed observed bytes -- two domains, so the same file on disk changed identity whenever desired state changed, and the equality arm imported the answer it was meant to establish. There is now one spark_serving_user_unit_content_identity taken over bytes, used by the desired member and the observation alike; equality falls out of byte equality. The desired member's digest moved with it, since hashing the typed spec on one side and bytes on the other is the same fused-domain bug that made the runtime and model members unreachable. EMPTY FILE. The identity is taken over String, so "" needs no NonEmptyStr cast. An empty file is a real observation and ordinary drift, and forcing a cast was a lie about what was read. ENABLEMENT. is-enabled was declared and never consumed, so a unit with exactly the right bytes that is DISABLED reported as matching desired -- claiming a convergence the next reboot refutes. systemd's answers are modeled rather than collapsed: enabled, disabled, not-found and unobserved are four states, because treating every nonzero exit as infrastructure failure would render a healthy disabled unit unobservable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Wire the unit probes onto the real SSH legs, one level short of a caller spark_serving_observe_user_unit runs `cat <unit>` and `systemctl --user is-enabled <unit>` through the same spark_serving_probe_leg every other observation uses, and feeds classify_observed_user_unit. The classifier and both probe argvs now have production callers. Two decoding facts that a naive read would get wrong. is-enabled EXITS NON-ZERO for a disabled unit while printing "disabled" -- a successful observation of a real state -- so the word is classified and the exit code only distinguishes "could not ask". And a failed `cat` is absence only when stderr names a missing file; any other failure is unobserved, because absence and unreadable have different remedies. STATED PLAINLY: spark_serving_observe_user_unit itself has ZERO callers. The gap moved up one level rather than closing. Its caller is the full-population cutover, which is gated on the typed row freezing the RemoteOperation -- so this is reachable-pending-cutover, not reachable. Claiming otherwise is the mistake this lane has already made twice. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Freeze the realized operations in the plan row, and cut the production planner over to the full population Two changes that had to land together: the freeze is the recorded precondition on the cutover, and the cutover is what gives the freeze a consumer that plans more than one member. THE FREEZE. The typed row carried MemberAction + install_effects, and WriteUserUnitFile is a bare variant carrying no bytes -- so apply resolved the unit content, path and mode from the repository's CURRENT authorities when it ran, not from the plan. Plan and apply could disagree and the frozen bundle hash could not detect it, because the bytes were never in the bundle. Realization now happens at plan time and its RemoteOperation values are frozen into the row; apply executes them verbatim, and refuses when a row carries effects but no operations rather than executing nothing while reporting the effects applied. THE CUTOVER. spark_serving_fleet_converge_plan_artifact planned a single-element linger desired list, so three of the four modeled members were never planned at all. It now takes the observed-member projection and reconciles the declared population -- which gives spark_serving_observe_user_unit its first production caller. The return type widens to a verdict carrying a CAUSE, dissolving the residue that module declared: every distinct refusal previously rendered as the single word "plan-refused", so a reader could not tell an unreachable host from a wrong one. It refuses on a PARTIAL observation rather than planning through one. An unobserved unit is absent from the observed list, and absence is what makes reconcile plan an addition -- so planning against it would write the unit on every run while no replan could ever be empty. WHAT THIS DOES NOT DO. A bare host still refuses: InstallOwnedRuntimeClosure and PullModelArtifact are unrealized, so the typed-action projection cannot produce their rows and refuses the whole plan rather than freezing a short list. That is the honest census, and it is witnessed as such -- with a unit-only drift freezing exactly one row, so the refusal is provably about those two effects and not about the widening. Evidence: spark_serving_full_plan_witness_test 24/24 (6 new) spark_serving_converge_slice_witness_test 23/23 (6 callers migrated) spark_serving_write_unit_operation 8/8 spark_serving_unit_observation 15/15 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Cover the frozen operations with the bundle hash, and put the observed Spark population in the CAS baseline CORRECTION TO THE PRECEDING COMMIT. Its message said freezing the operations made "the bundle hash cover the exact bytes a file write will deliver". That was false, and I asserted it without checking. fleet_converge_spark_serving_action_line serializes kind, member key and EFFECT NAMES. It did not serialize row.operations, and the bundle hash is computed over that wire -- so the unit bytes were frozen into the row and left outside the hash. An artifact whose unit content had been swapped wholesale hashed identically and still admitted. Frozen and covered are two properties. Freezing stopped apply from RE-DERIVING the bytes, which did hold and still holds. Being covered by the hash is separate, and I collapsed the two. WHAT CLOSES IT. remote_operation_wire: argv words inline, file writes as path + mode + content identity. Deliberately NOT remote_operation_label, which renders a write as "write-file <path>" -- a hash over labels is the exact hole. Content enters as its own identity rather than inline because the wire is a fingerprint input, and a multi-kilobyte unit file pasted in buys no additional discrimination. The witness asserts two writes differing ONLY in content produce different wires WHILE their labels stay equal, so nothing but the bytes can be doing the work; and that argv words discriminate too, since freezing an argv and swapping its words would be the same hole one kind over. THE CAS BASELINE. The observed Spark population was not in member_set_fingerprint or observed_baseline_hex, so a Spark member could change between plan and apply -- a model replaced, a unit rewritten, linger turned off -- without invalidating the approved plan. Each member now contributes its address AND its state_digest; the address alone would let a value change without moving the fingerprint, which is the drift being guarded. A frozen operation is only as good as the baseline it was planned against. observed_spark is threaded explicitly rather than defaulted. The generic timers/caps CLI passes [] -- honest, since that producer observes no Spark members, and self-consistent because the same value is recomputed on its own admits side -- but the fingerprinted population is now visible at each call site instead of absent from the model. AND THE LINGER FAIL-OPEN. LingerUnobservedState and LingerObservedDisabled both projected to an empty member list, and absence is what makes reconcile plan a change -- so a FAILED probe was indistinguishable from disabled and would have selected the privileged enable-linger effect. linger_observed now travels beside the members and the plan refuses on it with its own cause, with a disabled-linger control proving the refusal is not just linger observation being broken outright. Evidence (76 witnesses, full roster): fleet_converge_plan_witness_test 16/16 spark_serving_full_plan_witness_test 26/26 spark_serving_converge_slice_witness_test 23/23 spark_serving_write_unit_operation 11/11 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Put the member values in the hashed wire, and prove what the artifact hash discriminates Residue inside the operation-coverage fix, found by review against a stale head but real against the current one. spark_serving_member_key is host x principal x ADDRESS -- correctly, since that is what reconcile keys on. But the wire carried only the key, so a row whose `to` digest moved from one model manifest to another serialized IDENTICALLY, and the approved artifact still admitted after exactly the drift the CAS baseline exists to catch. Key answers which resource; the digests answer from what, to what. An approval is over both. `from` renders explicitly as <none> where the arm has none rather than being omitted, so an add and a change to the same value cannot collide on one string. FIVE TAMPER CONTROLS, and the fifth is the one that makes the others mean anything. Changing a state digest, changing one argv word, reordering two operations, and dropping an operation each change the wire. Reordering is its own tamper rather than a variant of substitution: the same operations in the other order is a different program, and writing the unit before creating its directory is precisely the bare-host failure the mkdir ordering prevents -- a set-shaped wire would call them equal. All four are INEQUALITIES, and an inequality is satisfied by a wire that is merely nondeterministic. So two structurally identical rows must produce the same wire; without that control the other four prove nothing about tamper detection. spark_serving_converge_slice_witness_test 28/28 (5 new) No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Converged means the whole population reconciles, not that linger came back yes The read-back after apply was the linger probe alone. That was survivable only while linger was the only member anything could plan: once the runtime, unit and model effects execute, a linger=yes answer returns wet-applied-converged over a missing model, a wrong runtime, or a unit that was written and never enabled. Applying N operations and verifying one of them is a fail-open, and it sits at the actuation boundary where the verdict becomes a receipt. The bar is now the SECOND PLAN: re-observe every member, reconcile against the unchanged desired population, require zero writes. That is the property an operator wants -- not "the commands exited 0" but "the host is now in the declared state" -- and it is what distinguishes convergence from execution. A nonempty replan reports its row count rather than a bare mismatch. NOT CLAIMED, and stated in-code rather than left to be assumed: this does not run a generation. An empty replan says the modeled members match; it does not say the server answers. Terminal serving evidence -- a non-streaming generate returning done=true, the planned model identity, and exactly pong -- is owed by the run that first restores a host and belongs with that wet receipt. spark_serving_converge_slice_witness_test 28/28 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make an effects-but-no-operations row unconstructible, rather than checked by an aggregate that cannot catch it The refusal I added with the freeze was over AGGREGATES: length(frozen_effects) > 0 && length(frozen_operations) == 0 That cannot catch the case it exists for. One row carrying effects and ZERO operations, sitting beside a row that has operations, leaves both totals nonzero -- the check passes, and that row's effect is reported applied while nothing ran for it. A fabricated plausible output at the actuation seam, which is the class the freeze was meant to close. Head plus tail removes the state instead of catching it: first_operation plus further_operations, so a row with no operations has no constructor. The aggregate check is not tightened, it is deleted as unnecessary -- construction over validation. Same shape StagedIntermediates uses, for the same reason. NOT DONE, named in the type so it is not mistaken for done: this makes each ROW nonempty, not each EFFECT attributed to its own operations. A row carrying two effects still cannot say which operation belongs to which. That is the PlannedEffectExecution restructure, with a wider blast radius. spark_serving_converge_slice_witness_test 28/28 spark_serving_full_plan_witness_test 26/26 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enablement is its own resource, not a prefix on the unit's content digest The unit member carried ONE digest and enablement was folded into it by prefixing the bytes: join(["disabled:", read_stdout]). That is a product -- content x enablement -- collapsed into a scalar, and the collapse produced a wrong REMEDY, not merely an imprecise report. Byte-perfect content that happened to be disabled hashed differently, read as content drift, and selected WriteUserUnitFile plus a manager reload: rewriting a correct file in order to enable it. On a host being converged without disturbance that is the difference between touching a correct file and leaving it alone. The comment defending it was right that a disabled unit is not converged. The modeling was wrong, and a wrong model produces a wrong remedy no matter how sound the reasoning layered on top. Repaired by modeling the subjects, not by adding a rule: - SparkServingUserUnitEnablementAddress is its own resource address - content identity is identity-of-bytes on both sides, nothing folded in - enablement reconciles separately; EnableUserUnit falls out as its own minimal effect rather than being computed by a rule over a fused value - unobserved enablement projects to NO member, so absence cannot be read as drift -- the same law the other unobserved states already follow - both facts come from ONE pair of probes, not two callers each paying the round trips again The declared desired population is consequently FIVE members, not four. Three witnesses asserted the old count and failed exactly as they should when a population changes; their names moved with their assertions, since a test named ..._is_four_members that checks five is a stale citation. spark_serving_full_plan_witness_test 26/26 spark_serving_converge_slice_witness_test 28/28 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Decouple the unit's content observation from its enablement observation, and pin subject independence Two defects in the commit before this one, both mine, both found by review rather than by any passing test. MY COMMIT MESSAGE WAS FALSE. It said both facts come from ONE pair of probes. The production caller invoked spark_serving_observe_user_unit_pair TWICE -- once for .state, once for .enablement -- paying four remote legs and, worse, joining content read at one moment with enablement read at another. Two facts about one unit taken from two different observations is not an observation of that unit. spark_serving_observed_members_for_unit takes the bound pair, so the join is structural rather than a caller's discipline. THE COLLAPSE I CLAIMED TO REMOVE WAS STILL THERE, ONE LEVEL UP. Splitting the member addresses did not separate the subjects: classify_observed_user_unit still took the enablement, and UserUnitEnablementUnobserved turned a SUCCESSFULLY READ FILE into UserUnitStateUnobserved. Failure to establish one fact erased an established fact about a different one -- the exact failure the split was supposed to end. I fixed the symptom's representation and reported the class as closed. Content now reads only file-read evidence. Enablement carries its own enablement_observed completeness fact rather than borrowing unit_observed=false as an indirect refusal wall, which only ever worked because the classifier was erasing itself on the enablement's behalf. THREE WITNESSES, and the first two are a different KIND than anything else in this file. Everything else here confirms what a subject reports when observed; these assert that a subject's FAILURE stays in its own lane: an unobserved enablement leaves the observed content intact an unobserved unit leaves the observed enablement intact a correct but disabled unit plans exactly one member The mirror is not redundant -- without it the first passes on a projection that simply reports everything as observed. The third is the direct refutation of the disabled: encoding, which planned a rewrite plus a reload for a byte-perfect file. If the layers are real, a failure in one is invisible to the others. That is testable, and nothing was testing it, which is why the coupling survived the split and needed an outside reader. spark_serving_full_plan_witness_test 29/29 (3 new) spark_serving_converge_slice_witness_test 28/28 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Migrate the unit-observation witnesses off the removed parameter, and retire the three that asserted the old model CI red at c35ca81. I changed classify_observed_user_unit's signature and then ran the two witness files that do NOT call it. The file with fifteen direct callers is the one I did not run. Three of those tests encoded the OLD model and needed reading, not a signature migration. The compiler found every call site; only reading each assertion found the three asserting a world that no longer exists. RETIRED WITH ITS RECEIPT: an_unobserved_enablement_leaves_the_unit_unobserved ASSERTED THE DEFECT. It required a failed enablement probe to erase a successfully read file -- the exact coupling removed one commit earlier. A signature-only migration would have left it passing and quietly re-legislating the bug, which is how obsolete behavior grants itself immortality. Replaced by its inverse: the read succeeded, so the content is established, and the enablement's failure scopes to the enablement. RETIRED AND RELOCATED: exact_bytes_that_are_disabled_do_not_match_desired was true only under the `disabled:` prefix. The claim it protected -- a disabled unit is not converged -- is real and survives on the ENABLEMENT member; the content claim inverts to exact bytes matching desired. REHOMED: a_not_found_enablement_is_distinct_from_disabled is now a claim about the enablement classifier, since the content identity no longer carries enablement at all. THE PROCESS DEFECT, which is the same shape as the code ones. Nine witness files import the eleven modules this branch changes; I had been running four, chosen by recollection. The set is derivable in one command -- I had both facts, which modules changed and which witnesses import them, and was joining them by memory instead of computing the join. All nine now run, 139 witnesses: spark_serving_unit_observation 15/15 spark_serving_effect_wire + member_realization 9/9 spark_serving_membership + observe 47/47 spark_serving_full_plan 29/29 spark_serving_converge_slice 28/28 spark_serving_write_unit_operation 11/11 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the runtime identity for what it hashes: materialization inputs, not an extracted closure The name was doing the collapsing. `closure_digest` reads as "an identity for the extracted runtime tree"; it hashes version, architecture, variant and the ARCHIVE digest, and nothing in it has ever seen an extracted file. That is the domain mismatch waiting to happen. Comparing it against an executable digest observed on a host manufactures drift out of two different subjects sharing one field -- the same class as folding enablement into a content identity, one layer over. It is also why a corrupted extraction under a correctly named root is NOT runtime drift. Renamed to ollama_runtime_materialization_identity: the identity of the inputs that determine what materializing this release must produce. Knowable from admitted upstream bytes plus an admitted recipe, without claiming the tree exists anywhere -- which is what makes it usable as a desired value at plan time. TWO INPUTS THE RELEASE ALREADY CARRIED are now hashed, because both determine the materialized result and neither was in the identity: executable_relative_path decides where the binary lands inside the root, and the archive CODEC decides how the bytes are unpacked. Two releases differing only in either produced ONE identity while materializing to DIFFERENT trees. THE CODEC, NOT THE DISTRIBUTION SUFFIX. My first attempt hashed archive_format_distribution_suffix because it was the function that rendered a format as a string. The suffix is a filename convention -- `.tgz` and `.tar.gz` are one codec spelled two ways and unpack identically -- so hashing it would split one materialization into two identities, and a correctly materialized host would report drift over how its release row spelled a suffix. A call-shape error caught it. STILL NOT IN IT, named so the gap is not mistaken for closed: a structured extraction recipe. archive_layout_note is prose and stays prose; promoting an unparsed sentence into an identity would be worse than leaving it out. The changed-module set grew, so the derived witness set grew with it -- ollama_capability and spark_serving_runtime_receipt were not in the previous nine. spark_serving_observe 32/32 ollama_capability + spark_serving_runtime_receipt 19/19 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * A runtime observation says absent, incomplete, complete, or refused -- and incomplete is its own arm RuntimeMaterializationObservation, derived by asking what a runtime observation can honestly say rather than by copying a failure taxonomy. The layering is the residue of that, not the goal. INCOMPLETE IS ITS OWN ARM, which is the whole point of the carrier. A correct path name is not proof of a correct runtime: the root is content-addressed by the materialization identity, so its NAME is derivable from the release alone, and a directory bearing it proves only that something once decided to create it. Whether the executable is there, and whether it is the one the identity names, are separate facts. Folding incomplete into Absent would report nothing installed while a partial tree sits on disk, and the remedies differ -- materialize versus repair. Folding it into ObservationRefused would be worse: the corruption was SUCCESSFULLY OBSERVED, and calling an established fact an inability to establish it is the collapse this lane has now found at four separate layers. Refusal is reserved for genuinely not knowing. NOTHING ABOUT A RUNNING PROCESS IS IN IT. /api/version reports what a live server exposes -- a fact about a process, not an installation -- and a runtime can be perfectly materialized with nothing running. Keeping that out is what lets a host mid-install be observed at all, which is the property whose absence made every partial state unhealable. Defects are head plus tail: "incomplete with nothing wrong" has no constructor. SIX WITNESSES, written to break the model rather than confirm it. Three would pass if the arms were folded -- corrupted-under-a-correct-root is incomplete; incomplete and absent agree on the member and differ as facts; only a refusal reports the runtime unobserved. Three are the controls that stop those passing vacuously, since "projects no identity" is satisfied by an accessor that never answers. Also verified rather than assumed: the runtime member was ALREADY keyed on the stable address with the digest in its value. The ruling's warning against keying on a digest was about a mistake this tree had not made. runtime_materialization_observation 6/6 spark_serving_observe 32/32 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Thread the enablement completeness fact into the plan, and stop a failed probe selecting EnableUserUnit A P0 I introduced one commit earlier, and the mechanism matters more than the fix. I added enablement_observed to the projection correctly. But spark_serving_full_membership_plan destructures SparkServingObservedMembers with TWO of its THREE completeness fields, and that typechecks -- adding a field forced no consumer to handle it. So the fact was carried and silently dropped: enablement probe unobserved -> no observed enablement member -> desired member reads as absent -> MemberAdded -> EnableUserUnit selected off a probe that never answered That is the exact fail-open closed for linger one commit before, reintroduced by adding an address without threading its completeness. Refused now with its own cause, and supports_empty_replan requires all three facts rather than two. THE WITNESS HAD TO GO AT THE PRODUCTION ENTRY. The projection was already correct, so a projection-level claim would have passed for the whole life of the bug -- the same lesson as the derived witness set, in a different costume: I keep testing the layer I just edited rather than the layer where the consequence lands. THE NEW RULE THEN CORRECTED MY FIXTURES, which is the first red today that meant "your model is now strict enough to notice this". Four fixtures paired an ABSENT unit with UNOBSERVED enablement -- a host state that cannot occur. systemctl --user is-enabled answers not-found for a unit that was never written; that is a real observation with a real remedy, not ignorance. Unobserved is what a probe that never answered gives. Which changes what a bare host IS: not a blank slate, but a host with one observable fact. Its registration member is present and drifted, so write-then-enable falls out of reconcile as two independent remedies rather than an ordering the code has to remember. The renamed a_bare_host_observes_only_its_unit_registration says so; a test asserting one member while named "no members" is the stale-citation class. spark_serving_full_plan 31/31 (2 new) No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the rung the runtime observation carrier actually occupies RuntimeMaterializationComplete is a PUBLIC CONSTRUCTOR. Any caller can author one carrying any identity, so nothing makes "complete" a fact EARNED BY EVIDENCE rather than a claim asserted by whoever assembles the value. The six witnesses prove the arms are DISTINCT; they prove nothing about whether a Complete was ever observed. Not sealed now, deliberately rather than by oversight: the filesystem probe that would supply the evidence does not exist yet, so sole_constructor plus admit_callers today would be a wall around an empty room -- nothing to admit through, reading as a guarantee while guarding nothing. The obligation is that Complete becomes reachable ONLY from a probe result, and it lands WITH the probe. Recorded because a carrier named for a guarantee it does not hold is rung inflation, and an inflated class never ranks for repair. This is a vocabulary with correct distinctions, not a guarantee, and the code now says so. runtime_materialization_observation 6/6 No dissolution obligations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Stop freezing two enable operations for one unit Splitting the user unit into a content address and an enablement address gave enabling its own owner, but the content address kept EnableUserUnit in its remedy. On a bare host both members drift, so the plan froze the enable twice for one unit: adding an address does not divide a responsibility; removing it from the old owner does. spark_serving_user_unit_install_effects() is now [WriteUserUnitFile, ReloadUserManager]. Enabling belongs to SparkServingUserUnitEnablementAddress alone, which already mapped to [EnableUserUnit]. Witnesses: a_bare_host_freezes_exactly_one_enable_operation and the_unit_content_member_does_not_enable pin both halves. w_member_realization_user_unit_change_includes_write_reload_enable asserted the old bundle and is retired with a receipt, replaced by w_member_realization_user_unit_content_change_writes_and_reloads_without_enabling -- the claim it protected (a content change writes and reloads) survives; the EnableUserUnit half is retired because content no longer owns enabling. Executed: full_plan 33/33, member_realization 7/7, unit_observation 15/15. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * An incomplete runtime materialization is a differing member, not an absent one The observation carrier distinguished absent from incomplete and then `runtime_materialization_observed_identity` answered `none` for both -- so the distinction died one function after the type made it, before reconcile could ever act on it. The consequence is not cosmetic. Absence yields MemberAdded and a differing value yields MemberChanged, so a partially-extracted root reported as absent selects a fresh materialization where a repair was owed, and hands that repair no `from` value to be safe about. Incomplete now projects a state value derived from its defects: not the desired identity, so a corrupted root cannot compare converged, and not a constant, so a root that lost its executable and one that merely lost the executable bit are two different observed values rather than one indistinguishable "broken". Absent still projects no member because nothing is at the address; refusal also projects none but is separated by the completeness bit, which is what keeps it from reading as a fact. The witness previously asserted the collapse outright -- it was named `incomplete_and_absent_agree_on_the_member_and_differ_as_facts` and pinned the erasure as the contract. It is replaced by two discriminating controls: that incomplete projects a value while absent does not and that value differs from the desired identity, and that two distinct defects project two distinct values. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Observe the runtime root from the filesystem; attribute operations to their effect Two changes that arrived together because the second is what the first's successor needs. Both are in this commit; neither is described by the other. ── The runtime member was produced from the wrong evidence ────────────────── It came from `/api/version` joined with the archive-admission receipt -- a pair that proves a running server reported a version and an archive was once downloaded and digest-admitted, and says nothing about whether the runtime root was extracted, placed, or published correctly. That is precisely what the runtime-root ADDRESS is about, so a host whose root was half-extracted while a previously-installed server still answered reported the member converged. The two facts also have different lifetimes: a runtime can be perfectly materialized with nothing running, and a process can answer long after its root was corrupted underneath it. Reading the address from the thing the address names is what makes a host mid-install observable at all. So `RuntimeMaterializationObservation` gains a producer and stops being a vocabulary with no consumer. The probe is three `test` legs -- root, executable, executable bit -- with a fourth listing leg taken only when the root exists and the executable does not, because an interrupted extraction and a wrong recipe are different failures. A leg that did not run refuses; a leg that ran and exited nonzero is a successful measurement of a negative, and collapsing those would let an unreachable host report a bare runtime and select a full materialization out of ignorance. The runtime travels as its own observed subject with its own completeness bit, beside unit, enablement and linger, and is projected in BOTH observation arms so a materialized-but-not-running root is not indistinguishable from a bare host. THE ROOT IS NOW CONTENT-ADDRESSED by the materialization identity. A fixed path made a runtime's location independent of which runtime it is: upgrading meant mutating a directory in place, so a failed extraction left a tree that is neither the old runtime nor the new one at the only address either could occupy, and rollback had nowhere to roll back to. Deriving the leaf from the identity makes materialization additive and the name checkable. The membership key stays the stable logical slot; the identity is that member's desired value. `ExecStart` also stops spelling "/bin/ollama". That was a second statement of `executable_relative_path`, which the cited release row already carries and the probe already reads -- and the one that would drift silently, since a release whose layout moved the binary would be observed and materialized at the right path and then started from the wrong one. Not yet observed, named rather than implied: the completion receipt and the local executable's own reported version. `Complete` means the expected executable is in the expected place and is executable -- not that the tree is the one the identity names. ── Each effect now owns its own operations ────────────────────────────────── The typed row carried two PARALLEL populations: a list of effects, and one flat operation sequence covering all of them. Nothing related the two, so a row carrying three effects could not say which operation belonged to which, and no apply receipt could report "the download succeeded, the digest verified, the extraction failed" against the effect that owns those steps. The previous revision said as much in a comment naming this restructure as owed. Parallel lists are also the shape that goes wrong silently as sequences get long: a linger effect contributing one argv and a runtime install contributing nine cannot be told apart in a flat list of ten, so a receipt would have to guess an attribution -- a guess at the actuation seam. `PlannedEffectExecution` binds one effect to the operations that realize it, head plus tail, so an effect with zero operations has no constructor. The row is nonempty in executions rather than in operations. Realization is now per effect, so the attribution is established where it is known rather than reconstructed from list offsets afterwards; one effect refusing still refuses the whole row. Both the effect roster and the flat sequence the actuator consumes are DERIVED from the executions rather than stored beside them, which is what retires the parallel population: there is no second list left to fall out of step. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Keep each remote execution's natural result; name steps; record the unreached tail `RemoteOperationOutcome = Succeeded{label} | Refused{reason}` flattened two incomparable kinds of evidence into one word. A `RemoteArgv` answers with an exit code, a stdout and a stderr. A `RemoteFileBytes` answers with a four-step staged convergence whose success arm is established by an INDEPENDENT READ-BACK. Calling both `Succeeded` reported them at one rung when only one had earned it -- and it pulled the higher-rung evidence DOWN to meet the lower one, since the file arm is the one already ruled to be not-convergence-until-read-back. The repair is not a stronger success predicate. It is keeping each arm's own answer: `RemoteOperationExecution` carries `TypedArgvExecOutcome` on one side and `TypedRemoteFileConvergence` on the other, and NEITHER means the resource converged. Exit zero says the invoked program reported completion. `systemctl enable --now` exiting zero is not proof the unit stays enabled and active; `tar` exiting zero is not proof the entrypoint is there; `ollama pull` exiting zero is not proof the manifest and blob closure are present. Resource convergence comes from the resource's own observer and the empty replan, and from nowhere else. `remote_execution_permits_continuation` is named for progression precisely so that advancing the sequence cannot be misread as establishing anything. WHAT THIS DELIBERATELY DOES NOT ADD. An earlier proposal was a third operation arm carrying an expected stdout. That would have made output mechanics into a generic business-logic language, and it would have left the original fail-open representable -- a caller could still pick plain `RemoteArgv` for a command whose value needed interpreting. The digest case needs no such arm: a checksum manifest is written as `RemoteFileBytes` and verified by `sha256sum --check --status`, an invocation whose exit status IS the comparison, so the artifact hash covers the expected digest, the target path, the manifest bytes and the verifying argv. STEPS ARE NAMED WHERE THEY ARE BUILT. `PlannedRemoteStep { identity, operation }`, with identities assigned at construction rather than derived from list position -- a positional name silently renames every later step when one is inserted, and a receipt saying "step 4 failed" reports a position, not a fact. AND THE HALT LEAVES A RECORD. The fold collapsed to one outcome, so every step after a failure was indistinguishable from one that ran and every step before it was forgotten. `RemoteStepStanding = Completed | Failed | Unattempted` records each step and explicitly marks the frozen tail that was never reached -- which is what makes "download succeeded, digest verified, extraction failed, publish unattempted" representable in the OUTCOME rather than only in the plan. The previous commit supplied the plan-side half of that and the flattening one function later dropped it. `halted` rides on the accumulator instead of being re-derived by scanning the standings, because a scan must decide what an empty list means and "nothing ran yet" and "everything ran and none failed" are different states a length check cannot separate. TWO FIXES THAT FELL OUT. The converged no-op reported itself as `RemoteOperationRefused`, so a fully converged host rendered as `wet-apply-exec-refused` -- a success condition wearing the failure constructor because the type had no arm for it; it has one now. And `spark_serving_observe_user_unit` is deleted: it had zero call sites while still paying for an enablement probe it discarded, being the leftover half of the fused content-and-enablement observation this branch already split apart. The apply module's authority note described the old flattening as the design, so it is rewritten rather than left as a stale citation in the file a reader trusts most. Verified per closure, because typechecking is per-import-closure and one entry is not a gate: the wet slice reported zero errors while the realizer still carried three unmigrated destructurings that only the slice witness's closure reaches. Green: wet slice 0 errors; full-plan witness converged-zero, bare-host-five and unit-only-drift; slice witness two-effects-two-commands and linger-frozen-row. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Migrate the last witness off the renamed field, and realize InstallOwnedRuntimeClosure TWO THINGS, and the first is a regression I introduced. ── The break ──────────────────────────────────────────────────────────────── `spark_serving_write_unit_operation_witness_test` still destructured `SparkServingInstallRemoteCommandsPresent { operations: ... }` after the previous commit renamed that field to `steps`. CI compiles all 3,663 modules in strict preparation and refused there, before any witness ran. WHY LOCAL CHECKS MISSED IT, since the same gap will recur otherwise: typechecking is per-IMPORT-CLOSURE. I verified the wet slice and two witness files; none of their closures reaches this one. The previous commit's own message noted that one entry is not a gate and then gated on three entries anyway. The instrument nearly hid it too. Grepping the run for `required-floor: FAIL` and diffing against main returned ZERO for this branch -- which reads as "no failures" and actually meant "preparation refused, so no witness ever ran". A zero from an instrument that did not fire is indistinguishable from a clean zero unless you check what the run did; only the incoherence of zero-failures-and-a-failure-verdict caught it. The gate is now a corpus-wide grep for every renamed symbol plus a typecheck sweep over every file importing a changed module, rather than a hand-picked set of entries. ── InstallOwnedRuntimeClosure is realized ─────────────────────────────────── The effect refused entirely, so a bare host's plan could never select it however well the rest of the vertical worked. Ten named steps: ensure-runtimes-parent / reset-attempt-staging / create-attempt-staging / download-archive / write-checksum-manifest / admit-archive-digest / extract-archive / require-staged-entrypoint / publish-runtime-root / write-materialization-receipt THE DIGEST IS COMPARED, NOT COMPUTED. `sha256sum <path>` exits zero whenever the file is merely READABLE and puts its answer on stdout, so freezing that would install a step that passes on any downloaded bytes at all. `--check --status` is silent and its EXIT STATUS is the comparison, so the expected digest travels as FILE BYTES -- a checksum manifest written through the same typed file-write path the unit file uses -- and the verifying argv names only the manifest. The frozen artifact hash therefore covers the expected digest, the archive path it is claimed of, the manifest bytes, the manifest's destination, and the exact verifying argv; an apply cannot substitute a different expectation because the expectation is inside the thing that was hashed. STAGING IS A SIBLING OF THE PUBLISHED ROOT, because `mv` is atomic only within one directory and staging elsewhere would make publication an interruptible copy. Its name is DERIVED from the materialization identity rather than randomised per attempt: a random path cannot be hashed into a frozen plan, so apply would be choosing a location the plan never saw. Ownership comes from removing it first, not from being unguessable -- and without that removal a previous interrupted attempt's partial tree is extracted over, producing a tree that is neither attempt. THE EXTRACTION FLAG COMES FROM THE CITED CODEC, not the filename suffix: `.tgz` and `.tar.gz` are one codec spelled two ways, so selecting by suffix would read a nickname where the release row carries the fact. NOTHING HERE ESTABLISHES THAT THE RUNTIME IS CORRECT. Every step exiting zero means the invoked program reported completion. `tar` exiting zero is not proof the entrypoint is present; `mv` exiting zero is not proof the published tree has the intended contents. `require-staged-entrypoint` halts before publishing something visibly wrong -- it is not that proof. The runtime observer reads the published root independently, and the plan must come back empty. The receipt is written last, inside the published root, so its presence is evidence every prior step completed and it cannot outlive a failed publish. Green by execution: ten steps…

gunbai-bot Bot changed the base branch from main to session/bright-ferret-335-selector August 17, 2026 02:58

gunbai-bot Bot changed the title ~~sparks v2~~ Plan all four serving members, not only linger Aug 17, 2026

gunbai-bot Bot marked this pull request as ready for review August 17, 2026 03:03

gunbai-bot Bot changed the title ~~Plan all four serving members, not only linger~~ Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included Aug 17, 2026

briansrls merged commit d31bee2 into session/bright-ferret-335-selector Aug 17, 2026

briansrls deleted the session/bright-ferret-335-plan branch August 17, 2026 04:28

gunbai-bot Bot mentioned this pull request Aug 17, 2026

Realize WriteUserUnitFile: widen remote operations to carry file bytes #8366

Merged

Navigation Menu

Repository navigation

Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included - #8356

Plan the full serving population (observed side + typed-action refusal); production cutover deliberately not included#8356
briansrls merged 2 commits into
session/bright-ferret-335-selectorfrom
session/bright-ferret-335-plan

gunbai-bot Bot commented Aug 17, 2026 •

edited

Loading

Uh oh!

gunbai-bot Bot commented Aug 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gunbai-bot Bot commented Aug 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

The defect

The change

Evidence

Rung

Uh oh!

gunbai-bot Bot commented Aug 17, 2026

Why the cutover is not in this PR

The hole your finding led me to, now fixed

Evidence

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

gunbai-bot Bot commented Aug 17, 2026 •

edited

Loading