From 6f9a829d82e53e071b9e70c9068a83120d7a2668 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 20 Sep 2026 20:05:43 +0000 Subject: [PATCH 1/6] The three source findings the reviewer raised against #11679, after it merged MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #11679's park verdict arrived after it landed, so all three findings are on main. Repaired here in one change. (a) THE ORDER WAS COMMENT-VERSUS-CODE, AND WORSE, IT WAS ENCODED IN TWO WITNESS NAMES. converge_controller_app_key called ensure_key_dir, which runs `install -d` and THEN observes, before observe_upper_ancestors -- so a host mutation preceded the observation entitled to refuse the whole converge. No key was ever written (controller_app_key_action decides after every observation), so the residue was an empty root-owned directory rather than a custody hole. But an_unsafe_directory_refuses_before_any_write and a_writable_ancestor_refuses_before_any_write call only the pure decision with supplied observations, so they stayed green while advertising a property the production route did not have. Both repairs, not one: the create is now gated on the ancestor reading (on the refusing arm the directory is only OBSERVED, which is a read), and the two witnesses are renamed to what a claim over a pure function can establish -- refuses before any KEY-CONTENT write. controller_app_key_action is untouched, so the decision keeps its single authority. (b) CUSTODY WAS COUPLED TO RUNNER WIDTH. The entry resolved its host through runner_host_file_subject, which requires an admitted RunnerHostDeploy -- a spec plus an admitted WIDTH. srv2's width is unresolved, so srv2 has no deploy row and the mode terminated on srv2 while describing itself as covering srv1 and srv2. The App key's location, administrator target and custody do not depend on how many slots a host admits, so the module now resolves its own subject from runner_host_spec_for, which names srv2's address and principals independently of width. The privilege law is NOT dropped with the deploy row: the writer may not be the account CI jobs run as, and that comparison keeps its one authority -- gunbc.runner_host_grants gains bootstrap_principal_is_not_the_job_user, and the existing deploy-shaped predicate now calls it rather than being duplicated. The new subject deliberately carries no unit populations: this module verifies no teardown, so a value with empty unit lists would lie about what was established. (c) THE STAGING ABSENCE PROBE COULD FALSELY CONFIRM. `test -e` exit 1 became StagingAbsent, and GNU test -e is stat(path) == 0, so EACCES, ELOOP, ENOTDIR and EIO all answer 1 with an empty stderr -- and StagingAbsent is an input to ControllerAppKeyHeld, so a metadata failure would have been reported as custody held with no residue. Absence is now established by a successful listing of the PARENT, which is gunbc.live_deploy.member_observe's rule rather than a second vocabulary. The departure from that authority is stated rather than silent (DESIGN §3b): entry_presence reaches the far side as the bootstrap principal, and this parent is the key directory at root:root 0700, so an unelevated listing can only ever refuse -- it would answer Indeterminate on every host whether or not residue exists. The same membership question therefore runs over this module's elevated leg. classify_staging_residue is now pure over a listing that SUCCEEDED, so StagingUnobservable has no constructor inside it; that arm belongs to the leg. EXECUTED EVIDENCE: all 21 witnesses in microvm_controller_app_key_converge_witness_test pass, including three new discriminating ones -- srv2 resolves a custody subject although the deploy route still refuses it (which is the pair that would go red if custody were re-coupled to width), and the parent listing establishing absence, residue and the empty-listing case. Retained untouched, as the reviewer asked: the key path consumed from the signer's own JwsSigningKeyRef, the placement refusing the fabric-cell tree, RemoteFileModeOwnerRead closing the octal vocabulary at 0400, the byte-for-byte comparison against the resolved SM version, the full re-read after mutation, no key bytes in any receipt, and the old runner-owned key left alone. Co-Authored-By: Claude Opus 5 (1M context) --- .../microvm_controller_app_key_converge.dag | 171 ++++++++++++++---- dag/gunbc/runner/runner_host_grants.dag | 14 +- ...ntroller_app_key_converge_witness_test.dag | 110 +++++++++-- 3 files changed, 248 insertions(+), 47 deletions(-) diff --git a/dag/gunbc/runner/microvm_controller_app_key_converge.dag b/dag/gunbc/runner/microvm_controller_app_key_converge.dag index a5efdfc1c1a..103f9e99f74 100644 --- a/dag/gunbc/runner/microvm_controller_app_key_converge.dag +++ b/dag/gunbc/runner/microvm_controller_app_key_converge.dag @@ -11,7 +11,7 @@ import product.placement_supply { HostIdentity } import gunbc.clock_read { clock_now_probed_at, probed_at_word } import gunbc.actions_run_binding { actions_variable_read, ActionsVariablePresent, ActionsVariableAbsent, fleet_converge_expected_host_env_name } import gunbc.fleet_ssh_locus { prepare_fleet_ssh_agent_context, FleetSshContextReady, FleetSshContextRefused } -import gunbc.fleet_known_hosts_anchor { FleetSshExecutionContext } +import gunbc.fleet_known_hosts_anchor { FleetSshExecutionContext, SshTarget } import gunbc.file_access { FileTreeScope, path_within_file_tree_scope } import gunbc.auth.github_apps { gunbai_ci_app_pem_secret } import gunbc.auth.access_token_source { WorkloadIdentityToken } @@ -45,11 +45,11 @@ import gunbc.typed_remote_file_write { remote_file_privileged_argv, converge_typed_remote_file, } +import gunbc.runner_host_deploy { runner_host_spec_for, RunnerHostSpecFound, RunnerHostSpecAbsent } +import gunbc.runner_host_grants { executor_bootstrap_principal, bootstrap_principal_is_not_the_job_user } +import gunbc.fleet_reach_endpoint { fleet_probe_endpoint_for } +import gunbc.live_deploy.member_observe { path_parent, path_basename } import gunbc.runner_host_file_converge { - RunnerHostFileSubject, - RunnerHostFileSubjectAdmitted, - RunnerHostFileSubjectRefused, - runner_host_file_subject, RunnerHostFileStanding, HostFileIdentical, HostFileDiffers, @@ -240,20 +240,37 @@ fn key_dir_metadata_wire(m: KeyDirMetadata) -> String { } } -// The staging sibling's presence: `test -e` answers 0 (present) or 1 (absent); anything else means the -// test did not run, which is neither answer. +// THE STAGING SIBLING'S ABSENCE IS ESTABLISHED BY A SUCCESSFUL LISTING OF ITS PARENT, never by a +// failed read of the child. This was `test -e`, whose exit 1 was read here as StagingAbsent -- and +// GNU `test -e` is stat(path) == 0, so ENOENT, EACCES on an ancestor, ELOOP, ENOTDIR and EIO all +// answer 1 with an empty stderr. "The staging file is gone" and "I could not look" arrived as one +// value, and this one feeds ControllerAppKeyHeld: a metadata failure would have been reported as +// custody held with no residue. A successful preceding `rm -f` is not proof of the later +// observation, because the two are different reads of a host that can change between them. +// +// THE RULE IS gunbc.live_deploy.member_observe's, APPLIED OVER AN ELEVATED LEG, and the departure +// is stated rather than silent (DESIGN §3b). entry_presence is the landed authority for +// establishing absence from a parent listing over a transport, but it reaches the far side as the +// bootstrap principal, and this parent is the key directory: root:root 0700. An unelevated listing +// of it can only ever refuse, so entry_presence would answer Indeterminate for every host whether +// or not the residue exists -- fail-closed and empty of information. So the listing runs through +// this module's own elevated leg and the membership question is the same one. type StagingResidue = StagingAbsent | StagingResiduePresent { path: String } | StagingUnobservable { reason: String } -fn classify_staging_residue(path: String, exit_code: Int, stderr: String) -> StagingResidue { - if exit_code == 1 { - StagingAbsent - } else if exit_code == 0 { +fn staging_parent_listing_argv(dir: String) -> List { + ["ls", "-1", "-A", "--", dir] +} + +// PURE, over a listing that SUCCEEDED. The caller reaches this only on a successful leg, so every +// arm here is a reading of what the parent contains -- there is no exit code to misread. +fn classify_staging_residue(path: String, name: String, stdout: String) -> StagingResidue { + if any(map(split(s: stdout, delimiter: "\n"), l => trim(s: l)), l => l == name) { StagingResiduePresent { path: path } } else { - StagingUnobservable { reason: join(["staging presence test exit=", to_string(exit_code), " ", trim(s: stderr)], "") } + StagingAbsent } } @@ -386,8 +403,62 @@ type ElevatedLeg // Every leg is elevated: the directory is root-only, so an unprivileged find or test inside it would // report the permission boundary as an answer. +// THE SUBJECT OF A CUSTODY CONVERGE IS A HOST, NOT A SLOT POPULATION. This resolved through +// gunbc.runner_host_file_converge runner_host_file_subject, which requires an admitted +// RunnerHostDeploy -- a spec plus an admitted WIDTH -- and refuses a host whose width is +// unresolved. srv2 has no deploy row for that reason, so the mode terminated on srv2 while +// describing itself as covering srv1 and srv2. But the App key's location, its administrator +// target and its custody do not depend on how many runner slots a host admits: the key is root's, +// in root's directory, outside every slot and jail root. runner_host_spec_for names srv2's address +// and principals independently of width, so custody is resolved from the SPEC. +// +// THE PRIVILEGE LAW IS NOT DROPPED WITH THE DEPLOY ROW. The writer may not be the account CI jobs +// run as, and that comparison keeps its one authority in gunbc.runner_host_grants -- asked here +// over the spec's job_user rather than re-spelled (DESIGN §3). +// +// WHAT IS DELIBERATELY NOT CARRIED: desired and retired unit populations. This module verifies no +// teardown and names no unit, so a subject carrying empty unit lists would be a value whose fields +// lie about what was established. +type ControllerKeyHost { + host: HostIdentity + target: SshTarget +} + +type ControllerKeyHostAdmission + = ControllerKeyHostAdmitted { subject: ControllerKeyHost } + | ControllerKeyHostRefused { cause: String } + +fn controller_key_host(host: HostIdentity) -> ControllerKeyHostAdmission { + match runner_host_spec_for(host: host) { + RunnerHostSpecAbsent { host: h } => + ControllerKeyHostRefused { + cause: join(["microvm_controller_app_key_converge: ", h as String, " has no runner host spec, so it is not a runner host"], ""), + } + RunnerHostSpecFound { spec: spec } => + if !bootstrap_principal_is_not_the_job_user(bootstrap: executor_bootstrap_principal, job_user: spec.job_user) { + ControllerKeyHostRefused { + cause: join([ + "microvm_controller_app_key_converge: the administrator principal ", executor_bootstrap_principal.login as String, + " is the job user on ", host as String, + ", so the account that places a root-only key would be the one CI jobs run as", + ], ""), + } + } else { + ControllerKeyHostAdmitted { + subject: ControllerKeyHost { + host: host, + target: SshTarget { + endpoint: fleet_probe_endpoint_for(host: host as String) as NonEmptyStr, + principal: executor_bootstrap_principal.login, + }, + }, + } + } + } +} + fn run_elevated_leg( - subject: RunnerHostFileSubject, + subject: ControllerKeyHost, context: FleetSshExecutionContext, argv: List, stdin_payload: String, @@ -417,7 +488,7 @@ fn classify_find_answer(path: String, exit_code: Int, stdout: String, stderr: St } fn find_answer( - subject: RunnerHostFileSubject, + subject: ControllerKeyHost, context: FleetSshExecutionContext, path: String, kind: String, @@ -445,7 +516,7 @@ type KeyPathObservation | KeyPathUnobservable { reason: String } fn observe_key_path( - subject: RunnerHostFileSubject, + subject: ControllerKeyHost, context: FleetSshExecutionContext, path: String, kind: String, @@ -484,7 +555,7 @@ fn observe_key_path( } } -fn observe_key_file(subject: RunnerHostFileSubject, context: FleetSshExecutionContext, path: String) -> KeyFileMetadata +fn observe_key_file(subject: ControllerKeyHost, context: FleetSshExecutionContext, path: String) -> KeyFileMetadata uses net: Network { match observe_key_path(subject: subject, context: context, path: path, kind: "f") { @@ -494,7 +565,7 @@ fn observe_key_file(subject: RunnerHostFileSubject, context: FleetSshExecutionCo } } -fn observe_key_dir(subject: RunnerHostFileSubject, context: FleetSshExecutionContext, path: String) -> KeyDirMetadata +fn observe_key_dir(subject: ControllerKeyHost, context: FleetSshExecutionContext, path: String) -> KeyDirMetadata uses net: Network { match observe_key_path(subject: subject, context: context, path: path, kind: "d") { @@ -504,7 +575,7 @@ fn observe_key_dir(subject: RunnerHostFileSubject, context: FleetSshExecutionCon } } -fn observe_upper_ancestors(subject: RunnerHostFileSubject, context: FleetSshExecutionContext, paths: List) -> RunnerHostPathMetadata +fn observe_upper_ancestors(subject: ControllerKeyHost, context: FleetSshExecutionContext, paths: List) -> RunnerHostPathMetadata uses net: Network { match run_elevated_leg(subject: subject, context: context, argv: runner_host_root_only_find_argv(paths: paths, kind: "d"), stdin_payload: "") { @@ -515,7 +586,7 @@ fn observe_upper_ancestors(subject: RunnerHostFileSubject, context: FleetSshExec // The same far-side `cmp -s -` judgment converge_typed_remote_file mints from, run elevated with the // fetched version's bytes on stdin, so observation and apply cannot disagree about "identical". -fn observe_key_content(subject: RunnerHostFileSubject, context: FleetSshExecutionContext, write: TypedRemoteFileWrite) -> RunnerHostFileStanding +fn observe_key_content(subject: ControllerKeyHost, context: FleetSshExecutionContext, write: TypedRemoteFileWrite) -> RunnerHostFileStanding uses net: Network { match run_elevated_leg(subject: subject, context: context, argv: ["test", "-e", write.path as String], stdin_payload: "") { @@ -538,7 +609,13 @@ fn observe_key_content(subject: RunnerHostFileSubject, context: FleetSshExecutio // REMOVE, THEN READ THE ABSENCE BACK. `rm -f` exits 0 on an absent path, so its exit alone cannot // distinguish "removed" from "never there" -- which is fine -- nor "there and still there", which is // not; the presence test is what answers that. -fn clear_staging(subject: RunnerHostFileSubject, context: FleetSshExecutionContext, staging: String) -> StagingResidue +fn clear_staging( + subject: ControllerKeyHost, + context: FleetSshExecutionContext, + staging: String, + staging_parent: String, + staging_name: String, +) -> StagingResidue uses net: Network { match run_elevated_leg(subject: subject, context: context, argv: staging_remove_argv(staging: staging), stdin_payload: "") { @@ -547,9 +624,14 @@ fn clear_staging(subject: RunnerHostFileSubject, context: FleetSshExecutionConte if rc != 0 { StagingUnobservable { reason: join(["staging removal exit=", to_string(rc), " ", trim(s: re)], "") } } else { - match run_elevated_leg(subject: subject, context: context, argv: ["test", "-e", staging], stdin_payload: "") { - ElevatedLegRefused { reason: r } => StagingUnobservable { reason: r } - ElevatedLegRan { exit_code: c, stdout: _, stderr: e } => classify_staging_residue(path: staging, exit_code: c, stderr: e) + match run_elevated_leg(subject: subject, context: context, argv: staging_parent_listing_argv(dir: staging_parent), stdin_payload: "") { + ElevatedLegRefused { reason: r } => StagingUnobservable { reason: concat("staging parent not listed: ", r) } + ElevatedLegRan { exit_code: c, stdout: o, stderr: e } => + if c != 0 { + StagingUnobservable { reason: join(["staging parent listing exit=", to_string(c), " ", trim(s: e)], "") } + } else { + classify_staging_residue(path: staging, name: staging_name, stdout: o) + } } } } @@ -566,7 +648,7 @@ type ControllerAppKeyRun { readback: ControllerAppKeyReadback } -fn ensure_key_dir(subject: RunnerHostFileSubject, context: FleetSshExecutionContext, dir: String) -> KeyDirMetadata +fn ensure_key_dir(subject: ControllerKeyHost, context: FleetSshExecutionContext, dir: String) -> KeyDirMetadata uses net: Network { match observe_key_dir(subject: subject, context: context, path: dir) { @@ -585,8 +667,21 @@ fn ensure_key_dir(subject: RunnerHostFileSubject, context: FleetSshExecutionCont } } +// THE ANCESTORS ARE OBSERVED BEFORE ANY MUTATION, and that ordering is the point rather than a +// style. ensure_key_dir CREATES (install -d) and then observes, so calling it first ran a host +// mutation ahead of the observation entitled to refuse the whole converge -- on a host whose /etc +// or /etc/gunbc is group-writable the directory was created and only then was the ancestor read. +// No key was ever written, because controller_app_key_action decides after every observation, so +// the residue was an empty root-owned directory rather than a custody hole. But the module claimed +// observe -> decide -> mutate and did not implement it, and the witnesses over the pure decision +// could not see the difference: that is a comment and an evidence population asserting a property +// the production route did not have. +// +// So the create is now gated on the ancestor reading. On the refusing arm the directory is only +// OBSERVED, which is a read, and the same pure controller_app_key_action still decides -- the +// decision keeps its single authority and only the order of the effects changed. fn converge_controller_app_key( - subject: RunnerHostFileSubject, + subject: ControllerKeyHost, context: FleetSshExecutionContext, placed_path: NonEmptyStr, key_dir: NonEmptyStr, @@ -597,8 +692,11 @@ fn converge_controller_app_key( uses net: Network { let staging = typed_remote_file_staging_path(write: write) - let dir_before = ensure_key_dir(subject: subject, context: context, dir: key_dir as String) let ancestors_before = observe_upper_ancestors(subject: subject, context: context, paths: upper_ancestors) + let dir_before = match ancestors_before { + PathsRootOnly => ensure_key_dir(subject: subject, context: context, dir: key_dir as String) + _ => observe_key_dir(subject: subject, context: context, path: key_dir as String) + } let content_before = observe_key_content(subject: subject, context: context, write: write) let file_before = observe_key_file(subject: subject, context: context, path: placed_path as String) let action = controller_app_key_action(dir: dir_before, upper_ancestors: ancestors_before, content: content_before, file: file_before) @@ -616,7 +714,13 @@ fn converge_controller_app_key( } _ => none } - let staging_after = clear_staging(subject: subject, context: context, staging: staging) + let staging_after = clear_staging( + subject: subject, + context: context, + staging: staging, + staging_parent: path_parent(path: staging), + staging_name: path_basename(path: staging), + ) ControllerAppKeyRun { host: subject.host, key_path: placed_path, @@ -693,10 +797,9 @@ fn write_receipt_then_exit(body: String, ok: Bool) -> ProcessExit { } // ONE HOST PER RUN, NAMED BY THE DISPATCH, exactly as gunbc.runner_password_session_tool_converge: -// the fleet-converge job is pinned to a runner on the named host, and the subject (the administrator -// target, refusing a host with no runner deploy row or whose administrator is the job user) is -// gunbc.runner_host_file_converge runner_host_file_subject rather than a second resolution. The -// receipt is written on the failing path too. +// the fleet-converge job is pinned to a runner on the named host, and the subject -- the +// administrator target, refusing a host with no runner host spec or whose administrator is the job +// user -- is controller_key_host above. The receipt is written on the failing path too. fn microvm_controller_app_key_converge_ci_wet() -> ProcessExit uses net: Network { @@ -705,9 +808,9 @@ fn microvm_controller_app_key_converge_ci_wet() -> ProcessExit ActionsVariableAbsent { variable: v, detail: d } => write_receipt_then_exit(body: join(["microvm_controller_app_key_converge: ", v, " ", d, "; one host per run, named by the dispatch\n"], ""), ok: false) ActionsVariablePresent { value: raw_host } => - match runner_host_file_subject(host: raw_host as HostIdentity) { - RunnerHostFileSubjectRefused { cause: c } => write_receipt_then_exit(body: concat(c, "\n"), ok: false) - RunnerHostFileSubjectAdmitted { subject: subject } => + match controller_key_host(host: raw_host as HostIdentity) { + ControllerKeyHostRefused { cause: c } => write_receipt_then_exit(body: concat(c, "\n"), ok: false) + ControllerKeyHostAdmitted { subject: subject } => match controller_app_key_placement(key_path: signing_key_file_path(key: lifecycle_controller_app_key)) { ControllerAppKeyPlacementRefused { cause: c } => write_receipt_then_exit(body: concat(c as String, "\n"), ok: false) ControllerAppKeyPlaced { key_path: kp, key_dir: kd, upper_ancestors: ua } => diff --git a/dag/gunbc/runner/runner_host_grants.dag b/dag/gunbc/runner/runner_host_grants.dag index 3ecf9f18489..9cb1a7cb64c 100644 --- a/dag/gunbc/runner/runner_host_grants.dag +++ b/dag/gunbc/runner/runner_host_grants.dag @@ -455,5 +455,17 @@ fn bootstrap_principal_is_not_the_grantee( bootstrap: ExecutorBootstrapPrincipal, deploy: RunnerHostDeploy, ) -> Bool { - bootstrap.login != deploy.job_user + bootstrap_principal_is_not_the_job_user(bootstrap: bootstrap, job_user: deploy.job_user) +} + +// THE SAME LAW OVER THE JOB USER ALONE. A deploy row is a spec plus an ADMITTED WIDTH, and the +// privilege law does not depend on the width: whether the writer is the account CI jobs run as is a +// fact about the two principals, not about how many slots a host admits. A custody converge that +// resolves its host from runner_host_spec_for asks this directly rather than re-spelling the +// comparison, so the law has one authority and the deploy arm above is one caller of it. +fn bootstrap_principal_is_not_the_job_user( + bootstrap: ExecutorBootstrapPrincipal, + job_user: NonEmptyStr, +) -> Bool { + bootstrap.login != job_user } diff --git a/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag b/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag index de01bc4e46b..cbcea5103ed 100644 --- a/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag +++ b/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag @@ -9,8 +9,17 @@ import gunbc.runner_host_file_converge { HostFileDiffers, PathsRootOnly, PathsNotRootOnly, + runner_host_file_subject, + RunnerHostFileSubjectAdmitted, + RunnerHostFileSubjectRefused, } +import product.placement_supply { HostIdentity } +import gunbc.fleet_intent_network { operator_host_srv2 } import gunbc.microvm_controller_app_key_converge { + controller_key_host, + ControllerKeyHostAdmitted, + ControllerKeyHostRefused, + StagingResidue, ControllerAppKeyPlaced, ControllerAppKeyPlacementRefused, controller_app_key_placement, @@ -53,13 +62,23 @@ data held_file: KeyPathFindReading = KeyPathFindReading { root_owned: true, grou data held_dir: KeyPathFindReading = KeyPathFindReading { root_owned: true, group_or_other_bits: false, exactly_owner_read: false } -fn readback_with(file: KeyPathFindReading, staging_exit: Int, content_identical: Bool) -> ControllerAppKeyReadback { +data staging_path: String = "/etc/gunbc/microvm-controller/app.pem.gunbc-staging" +data staging_name: String = "app.pem.gunbc-staging" + +// THE STAGING READING IS SUPPLIED AS THE VALUE IT IS, not as an exit code. classify_staging_residue +// is now pure over a listing that SUCCEEDED, so StagingUnobservable has no constructor inside it -- +// that arm belongs to the leg, and the claim that needs it supplies it directly. +fn staging_from_listing(listing: String) -> StagingResidue { + classify_staging_residue(path: staging_path, name: staging_name, stdout: listing) +} + +fn readback_with(file: KeyPathFindReading, staging: StagingResidue, content_identical: Bool) -> ControllerAppKeyReadback { ControllerAppKeyReadback { file: classify_key_file_metadata(reading: file), dir: classify_key_dir_metadata(reading: held_dir), upper_ancestors: PathsRootOnly, content: if content_identical { HostFileIdentical } else { HostFileDiffers }, - staging: classify_staging_residue(path: "/etc/gunbc/microvm-controller/app.pem.gunbc-staging", exit_code: staging_exit, stderr: ""), + staging: staging, } } @@ -73,13 +92,13 @@ fn is_held(r: ControllerAppKeyReadback) -> Bool { // ── positive control ──────────────────────────────────────────────────────────────────────────── test fn a_root_owned_0400_identical_key_with_no_staging_is_held() -> Bool { - is_held(r: readback_with(file: held_file, staging_exit: 1, content_identical: true)) + is_held(r: readback_with(file: held_file, staging: staging_from_listing(listing: "other-file\napp.pem"), content_identical: true)) } // ── discriminating reds, each changing ONE input from the control and asserting the REASON ────── test fn a_runner_owned_key_is_not_held_and_is_named_wrong_owner() -> Bool { - let r = readback_with(file: KeyPathFindReading { root_owned: false, group_or_other_bits: false, exactly_owner_read: true }, staging_exit: 1, content_identical: true) + let r = readback_with(file: KeyPathFindReading { root_owned: false, group_or_other_bits: false, exactly_owner_read: true }, staging: staging_from_listing(listing: "other-file\napp.pem"), content_identical: true) !is_held(r: r) && match r.file { KeyFileWrongOwner => true _ => false @@ -87,7 +106,7 @@ test fn a_runner_owned_key_is_not_held_and_is_named_wrong_owner() -> Bool { } test fn a_group_readable_key_is_not_held_and_is_named_group_or_other_access() -> Bool { - let r = readback_with(file: KeyPathFindReading { root_owned: true, group_or_other_bits: true, exactly_owner_read: false }, staging_exit: 1, content_identical: true) + let r = readback_with(file: KeyPathFindReading { root_owned: true, group_or_other_bits: true, exactly_owner_read: false }, staging: staging_from_listing(listing: "other-file\napp.pem"), content_identical: true) !is_held(r: r) && match r.file { KeyFileGroupOrOtherAccess => true _ => false @@ -95,7 +114,7 @@ test fn a_group_readable_key_is_not_held_and_is_named_group_or_other_access() -> } test fn an_owner_writable_key_is_not_held_and_is_named_mode_not_0400() -> Bool { - let r = readback_with(file: KeyPathFindReading { root_owned: true, group_or_other_bits: false, exactly_owner_read: false }, staging_exit: 1, content_identical: true) + let r = readback_with(file: KeyPathFindReading { root_owned: true, group_or_other_bits: false, exactly_owner_read: false }, staging: staging_from_listing(listing: "other-file\napp.pem"), content_identical: true) !is_held(r: r) && match r.file { KeyFileModeNotOwnerReadOnly => true _ => false @@ -103,19 +122,22 @@ test fn an_owner_writable_key_is_not_held_and_is_named_mode_not_0400() -> Bool { } test fn a_key_whose_bytes_differ_from_the_sm_version_is_not_held() -> Bool { - !is_held(r: readback_with(file: held_file, staging_exit: 1, content_identical: false)) + !is_held(r: readback_with(file: held_file, staging: staging_from_listing(listing: "other-file\napp.pem"), content_identical: false)) } test fn a_surviving_staging_sibling_is_not_held_and_is_named_residue() -> Bool { - let r = readback_with(file: held_file, staging_exit: 0, content_identical: true) + let r = readback_with(file: held_file, staging: staging_from_listing(listing: "app.pem\napp.pem.gunbc-staging"), content_identical: true) !is_held(r: r) && match r.staging { StagingResiduePresent { path: _ } => true _ => false } } -test fn an_unrunnable_staging_test_is_unobservable_not_absent() -> Bool { - let r = readback_with(file: held_file, staging_exit: 2, content_identical: true) +// THE NAME SAYS WHAT IT ESTABLISHES: a leg that did not run is not absence. The probe this +// replaced was `test -e`, whose exit 1 collapsed "gone" with "could not look" -- and the absent +// arm is the one that lets ControllerAppKeyHeld be minted. +test fn an_unrunnable_staging_listing_is_unobservable_not_absent() -> Bool { + let r = readback_with(file: held_file, staging: StagingUnobservable { reason: "staging parent listing exit=2 ls: cannot open directory" }, content_identical: true) !is_held(r: r) && match r.staging { StagingUnobservable { reason: _ } => true _ => false @@ -152,14 +174,22 @@ test fn a_held_key_is_left_in_place() -> Bool { } } -test fn an_unsafe_directory_refuses_before_any_write() -> Bool { +// WHAT THESE TWO ESTABLISH, STATED IN THEIR NAMES. They call the pure controller_app_key_action +// with SUPPLIED observations; they do not execute the converge, so they cannot establish that no +// host mutation preceded the decision. What they do establish is that neither an unsafe key +// directory nor a writable ancestor reaches the arm that writes KEY CONTENT. Their previous names +// said "before any write", which advertised a property of the production route that the route did +// not have: converge_controller_app_key ran ensure_key_dir (install -d) before the ancestors were +// observed. That ordering is now repaired -- the create is gated on the ancestor reading -- but the +// names stay scoped to what a claim over a pure function can reach. +test fn an_unsafe_directory_refuses_before_any_key_content_write() -> Bool { match controller_app_key_action(dir: KeyDirGroupOrOtherAccess, upper_ancestors: PathsRootOnly, content: HostFileDiffers, file: KeyFileAbsent) { AppKeyActionRefused { reason: _ } => true _ => false } } -test fn a_writable_ancestor_refuses_before_any_write() -> Bool { +test fn a_writable_ancestor_refuses_before_any_key_content_write() -> Bool { match controller_app_key_action(dir: KeyDirRootOnly, upper_ancestors: PathsNotRootOnly { paths: ["/etc/gunbc"], detail: "" }, content: HostFileDiffers, file: KeyFileAbsent) { AppKeyActionRefused { reason: _ } => true _ => false @@ -189,3 +219,59 @@ test fn the_mode_leg_asks_for_exactly_0400() -> Bool { key_path_find_argv(path: "/p", kind: "f", clause: key_path_exactly_owner_read_clause) == ["find", "/p", "-maxdepth", "0", "-type", "f", "-perm", "0400"] } + + +// ── the custody subject is independent of slot width ──────────────────────────────────────────── + +// THE DISCRIMINATING PAIR, and the reason this repair exists. srv2's runner width is unresolved, so +// it has no admitted RunnerHostDeploy and runner_host_file_subject refuses it -- while the mode +// described itself as covering srv1 and srv2. The App key's location, administrator target and +// custody do not depend on how many slots a host admits, so controller_key_host resolves the same +// host from its SPEC and admits it. If a future edit re-couples custody to the deploy row, the +// first of these goes red. +test fn srv2_resolves_a_custody_subject_although_its_slot_width_is_unresolved() -> Bool { + match controller_key_host(host: operator_host_srv2) { + ControllerKeyHostAdmitted { subject: s } => (s.host as String) == (operator_host_srv2 as String) + ControllerKeyHostRefused { cause: _ } => false + } +} + +test fn the_deploy_route_still_refuses_srv2_which_is_what_made_the_mode_terminate() -> Bool { + match runner_host_file_subject(host: operator_host_srv2) { + RunnerHostFileSubjectRefused { cause: _ } => true + RunnerHostFileSubjectAdmitted { subject: _ } => false + } +} + +test fn a_host_with_no_runner_spec_is_refused_as_a_custody_subject() -> Bool { + match controller_key_host(host: "not-a-fleet-host" as HostIdentity) { + ControllerKeyHostRefused { cause: c } => string_contains(s: c, pattern: "no runner host spec") + ControllerKeyHostAdmitted { subject: _ } => false + } +} + +// ── staging absence comes from the parent listing ─────────────────────────────────────────────── + +test fn a_parent_listing_without_the_staging_name_establishes_absence() -> Bool { + match staging_from_listing(listing: "app.pem\nother") { + StagingAbsent => true + _ => false + } +} + +test fn a_parent_listing_carrying_the_staging_name_is_residue() -> Bool { + match staging_from_listing(listing: "app.pem\napp.pem.gunbc-staging") { + StagingResiduePresent { path: p } => p == staging_path + _ => false + } +} + +// AN EMPTY LISTING IS ABSENCE, and that is the one case worth stating apart: the parent was read and +// held nothing, which is a reading. It is NOT the same as a listing that never ran, which cannot +// reach this function at all. +test fn an_empty_parent_listing_is_absence_because_the_parent_was_read() -> Bool { + match staging_from_listing(listing: "") { + StagingAbsent => true + _ => false + } +} From 954ff01f9c55592cce604986b3eece35fad2a61e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 20 Sep 2026 20:44:24 +0000 Subject: [PATCH 2/6] Consume the listing and the SSH target rather than re-minting them (review 69368) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both findings are the same class, both are right, and the sharper point is that this diff applied the correct standard one line earlier -- the privilege predicate was deliberately extracted to keep one authority -- and then broke it twice in the same file. 1. The staging listing argv and the membership read were re-spellings of gunbc.live_deploy.member_observe entry_presence_in_parent. The stated §3b departure argues only that the TRANSPORT must be this module's elevated leg; it does not reach the argv or the predicate, which are the same facts whichever principal runs them. And the copies had ALREADY drifted in the commit that created them: mine trimmed each line, the original does not -- two sources that can answer one question differently, which is the fork §3 forbids and the drift §2 predicts. member_observe now exports the two pure halves, parent_listing_argv and listing_contains_entry, and BOTH entry_presence_in_parent and this module consume them. The elevated transport stays here, because that is the only part that actually differs. 2. The administrator SSH target was re-spelled from runner_host_file_subject_over_obligation. gunbc.runner_host_file_converge now exports administrator_ssh_target -- the endpoint from the fleet reach authority, the principal from the declared administrator, neither depending on the deploy row -- and both subjects consume it. Executed: 21/21 microvm_controller_app_key_converge witnesses still pass, and member_observe's own consumers (member_identity_witness_test) stay green after the extraction. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/live_deploy/member_observe.dag | 18 +++++++++++-- .../microvm_controller_app_key_converge.dag | 26 +++++++------------ .../runner/runner_host_file_converge.dag | 17 +++++++++--- 3 files changed, 39 insertions(+), 22 deletions(-) diff --git a/dag/gunbc/live_deploy/member_observe.dag b/dag/gunbc/live_deploy/member_observe.dag index ea944e6cb1f..7a2629d15d6 100644 --- a/dag/gunbc/live_deploy/member_observe.dag +++ b/dag/gunbc/live_deploy/member_observe.dag @@ -121,6 +121,20 @@ fn path_basename(path: String) -> String { fold(split(s: path, delimiter: "/"), init: "", f: (acc, seg) => if seg == "" { acc } else { seg }) } +// THE TWO PURE HALVES OF A TRANSPORT LISTING, named so a caller that must supply its OWN transport +// consumes them rather than re-minting them. The elevated arms of the fleet converges cannot use +// entry_presence itself -- it reaches the far side as the bootstrap principal, and a root:root 0700 +// parent refuses that listing -- but the argv and the membership read are the same facts whichever +// principal runs them, and two copies of a membership predicate can drift into two answers about +// one question (DESIGN §2: net concepts must not grow by re-invention). +fn parent_listing_argv(parent: String) -> List { + ["ls", "-1", "-A", "--", parent] +} + +fn listing_contains_entry(stdout: String, name: String) -> Bool { + any(split(s: stdout, delimiter: "\n"), entry => entry == name) +} + fn entry_presence_in_parent(arm: ObservationArm, parent: String, name: String) -> EntryPresence { match arm { OnTheHostItself => { @@ -135,9 +149,9 @@ fn entry_presence_in_parent(arm: ObservationArm, parent: String, name: String) - FilesystemEntrySubjectRefused { directory: _, name: _, cause } => EntryPresenceIndeterminate { cause: cause } } } - OverTransport { transport } => match remote_leg(transport: transport, argv: ["ls", "-1", "-A", "--", parent], leg: join(["listing ", parent], "")) { + OverTransport { transport } => match remote_leg(transport: transport, argv: parent_listing_argv(parent: parent), leg: join(["listing ", parent], "")) { LegRefused { cause } => EntryPresenceIndeterminate { cause: cause } - LegOut { stdout } => if any(split(s: stdout, delimiter: "\n"), entry => entry == name) { EntryPresent } else { EntryAbsent } + LegOut { stdout } => if listing_contains_entry(stdout: stdout, name: name) { EntryPresent } else { EntryAbsent } } } } diff --git a/dag/gunbc/runner/microvm_controller_app_key_converge.dag b/dag/gunbc/runner/microvm_controller_app_key_converge.dag index 103f9e99f74..4ec1317e153 100644 --- a/dag/gunbc/runner/microvm_controller_app_key_converge.dag +++ b/dag/gunbc/runner/microvm_controller_app_key_converge.dag @@ -47,9 +47,9 @@ import gunbc.typed_remote_file_write { } import gunbc.runner_host_deploy { runner_host_spec_for, RunnerHostSpecFound, RunnerHostSpecAbsent } import gunbc.runner_host_grants { executor_bootstrap_principal, bootstrap_principal_is_not_the_job_user } -import gunbc.fleet_reach_endpoint { fleet_probe_endpoint_for } -import gunbc.live_deploy.member_observe { path_parent, path_basename } +import gunbc.live_deploy.member_observe { path_parent, path_basename, parent_listing_argv, listing_contains_entry } import gunbc.runner_host_file_converge { + administrator_ssh_target, RunnerHostFileStanding, HostFileIdentical, HostFileDiffers, @@ -260,14 +260,14 @@ type StagingResidue | StagingResiduePresent { path: String } | StagingUnobservable { reason: String } -fn staging_parent_listing_argv(dir: String) -> List { - ["ls", "-1", "-A", "--", dir] -} - // PURE, over a listing that SUCCEEDED. The caller reaches this only on a successful leg, so every -// arm here is a reading of what the parent contains -- there is no exit code to misread. +// arm here is a reading of what the parent contains -- there is no exit code to misread. The argv +// and the membership read are member_observe's (parent_listing_argv, listing_contains_entry): only +// the TRANSPORT differs here, so only the transport is this module's. An earlier revision spelled +// both again and the copies had already drifted -- this one trimmed each line and the original did +// not, which is two sources answering one question differently (DESIGN §2). fn classify_staging_residue(path: String, name: String, stdout: String) -> StagingResidue { - if any(map(split(s: stdout, delimiter: "\n"), l => trim(s: l)), l => l == name) { + if listing_contains_entry(stdout: stdout, name: name) { StagingResiduePresent { path: path } } else { StagingAbsent @@ -445,13 +445,7 @@ fn controller_key_host(host: HostIdentity) -> ControllerKeyHostAdmission { } } else { ControllerKeyHostAdmitted { - subject: ControllerKeyHost { - host: host, - target: SshTarget { - endpoint: fleet_probe_endpoint_for(host: host as String) as NonEmptyStr, - principal: executor_bootstrap_principal.login, - }, - }, + subject: ControllerKeyHost { host: host, target: administrator_ssh_target(host: host) }, } } } @@ -624,7 +618,7 @@ fn clear_staging( if rc != 0 { StagingUnobservable { reason: join(["staging removal exit=", to_string(rc), " ", trim(s: re)], "") } } else { - match run_elevated_leg(subject: subject, context: context, argv: staging_parent_listing_argv(dir: staging_parent), stdin_payload: "") { + match run_elevated_leg(subject: subject, context: context, argv: parent_listing_argv(parent: staging_parent), stdin_payload: "") { ElevatedLegRefused { reason: r } => StagingUnobservable { reason: concat("staging parent not listed: ", r) } ElevatedLegRan { exit_code: c, stdout: o, stderr: e } => if c != 0 { diff --git a/dag/gunbc/runner/runner_host_file_converge.dag b/dag/gunbc/runner/runner_host_file_converge.dag index 8b5d469a525..21c7f032092 100644 --- a/dag/gunbc/runner/runner_host_file_converge.dag +++ b/dag/gunbc/runner/runner_host_file_converge.dag @@ -337,6 +337,18 @@ fn runner_host_file_subject(host: HostIdentity) -> RunnerHostFileSubjectAdmissio // this change removes everywhere else, surviving in the one module that decides teardown. The // refusal arm already exists here, so the obligation joins the other two conditions this // constructor refuses on. +// WHO WE REACH A RUNNER HOST AS, in one place. The endpoint comes from the fleet reach authority and +// the principal is the declared administrator; neither depends on the deploy row, so a converge that +// resolves its subject some other way -- gunbc.microvm_controller_app_key_converge resolves custody +// from the host SPEC, because the App key does not depend on slot width -- consumes this rather than +// spelling the pair again (DESIGN §3). +fn administrator_ssh_target(host: HostIdentity) -> SshTarget { + SshTarget { + endpoint: fleet_probe_endpoint_for(host: host as String) as NonEmptyStr, + principal: executor_bootstrap_principal.login, + } +} + fn runner_host_file_subject_over_obligation( host: HostIdentity, units: List, @@ -355,10 +367,7 @@ fn runner_host_file_subject_over_obligation( RunnerHostFileSubjectAdmitted { subject: RunnerHostFileSubject { host: host, - target: SshTarget { - endpoint: fleet_probe_endpoint_for(host: host as String) as NonEmptyStr, - principal: executor_bootstrap_principal.login, - }, + target: administrator_ssh_target(host: host), desired_units: units, retired_units: retired, }, From d4e77bca6f700071a54d175c63ff5d29810d5836 Mon Sep 17 00:00:00 2001 From: "gunbai-bot[bot]" <289086189+gunbai-bot[bot]@users.noreply.github.com> Date: Sun, 20 Sep 2026 21:30:09 +0000 Subject: [PATCH 3/6] chore: regenerate drifted generated artifacts (ci auto-heal) Ledger-Repair-Judged: docs/design-rung-drops.md Heal-Candidate-Run: 35536516170 --- ROADMAP.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index 348c9538632..9e9de4dd75f 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -10,7 +10,7 @@ Parked context (non-dispatchable): [compiler algorithm survey](docs/plans/compil The graph has sixteen lanes: SCM compatibility · namespace · P-derive · observation · placement · compute · CI cost · CI control · generated artefacts · v1 exit (four finish lines: compiler fixed point, interpreter deleted, products v1-free, zero hand-maintained Rust) · shell · roadmap runtime · fleet/hygiene · judgment · hermetic toolchain · compiler-guarantee (the DESIGN §4b ladder climbs; rung STATE lives in the guarantee claims carrier and is emitted, never restated in tickets — [gap analysis](docs/plans/compiler-guarantee-recovery-gap-analysis.md)). The three independent SCM R0 models, the separate P−1 evidence carrier, R1 compatibility-shape extraction, and P0 user-contract/landing spine are accepted; the operator-authored P1 proof-kernel node is active and fail-closed pending its first discriminating closing validation, while P2 and later product lanes remain parked. The toolchain pin model is an independent root. The P-derive receipt feeds the emitter fixed point, so the v1 chain nests under it. Compute owns the one contract everything else asks for work through — an exact subject in, a typed ending and the outputs it promised back out — and it sits ABOVE CI rather than inside it, because owning CI, converging the fleet, serving models and eventually judging changes are four consumers of one fabric, not four execution systems. It grounds on the signed realization spine rather than minting a second scheduler beside it. CI control owns who starts, queues and hands out required work and how its result reaches GitHub; CI cost owns how much computation that work performs. Fleet owns whether a merge to main becomes applied machine state and whether that question has one answer. Node fields define boundary, first slice, RED control, exclusions, owner, and handback. -**Focused view — the compute fabric + the infrastructure stabilisation lanes + fleet convergence from main + the harness, roadmap workflow and dashboard lanes.** 136 active deliverable(s) in other lanes are declared in the authority and hidden here; nothing is deleted or parked by focusing. Clear `roadmap_focus_selection` in `dag/gunbc/roadmap/roadmap_authority.dag` to restore the full page. 11 of the rows below are NOT lane deliverables — they are prerequisites pulled in from other lanes because lane work is blocked on them: commit-writer-admission, shell-gate-migration, shell-effectplan-to-bash, shell-typed-invocation, placement-compile-pool-envelope, placement-live-roster-preflight, observation-scoped-run-consumer, observation-scoped-run-seed-growth-justification, observation-scoped-run-seed-growth-justification-closing-contract, fleet-spark-host-enrollment, confidence-semantic-impact-query. Hidden lanes remain readable through their carriers: [docs/plans/namespace-cut-replacement-plan.md](docs/plans/namespace-cut-replacement-plan.md) · [docs/plans/dag-scm-design.md](docs/plans/dag-scm-design.md) · [docs/plans/native-scm-cas-fit-and-consumer-cut.md](docs/plans/native-scm-cas-fit-and-consumer-cut.md) · [docs/plans/namespace-unique-on-chain-operational-plan.md](docs/plans/namespace-unique-on-chain-operational-plan.md) · [docs/plans/v2-self-hosting.md](docs/plans/v2-self-hosting.md) · [src/v2/compiler/05_emit.dag](src/v2/compiler/05_emit.dag) · [docs/plans/progress-observation-design.md](docs/plans/progress-observation-design.md) · [src/v2/compiler/self_host/candidate_generation.dag](src/v2/compiler/self_host/candidate_generation.dag) · [src/v2/compiler/self_host/stage0_production_target.dag](src/v2/compiler/self_host/stage0_production_target.dag) · [src/v2/compiler/self_host/wet_receipt_enrollment.dag](src/v2/compiler/self_host/wet_receipt_enrollment.dag) · [src/v2/workflow/rust_crate_partition.dag](src/v2/workflow/rust_crate_partition.dag) · [src/v2/compiler/self_host/v2_emitter_direct_rust_door_contract.dag](src/v2/compiler/self_host/v2_emitter_direct_rust_door_contract.dag) · [dag/gunbc/v1/v1_deletion_plan.dag](dag/gunbc/v1/v1_deletion_plan.dag) · [dag/gunbc/stage0/stage0_rust_host_observation.dag](dag/gunbc/stage0/stage0_rust_host_observation.dag) · [docs/plans/witness-realization-plan.md](docs/plans/witness-realization-plan.md) · [src/v1/05_emit_rust.dag](src/v1/05_emit_rust.dag) · [dag/gunbc/v1/v1_interpreter_primitive_surface.dag](dag/gunbc/v1/v1_interpreter_primitive_surface.dag) · [docs/plans/shell-to-dag-residual-census-and-arc-completion.md](docs/plans/shell-to-dag-residual-census-and-arc-completion.md) · [docs/plans/roadmap-workspace-ux-plan.md](docs/plans/roadmap-workspace-ux-plan.md) · [docs/plans/hermetic-tool-provisioning-design.md](docs/plans/hermetic-tool-provisioning-design.md) · [dag/gunbc/capability_binding.dag](dag/gunbc/capability_binding.dag) · [dag/gunbc/roadmap/roadmap_component.dag](dag/gunbc/roadmap/roadmap_component.dag) · [dag/gunbc/design_document.dag](dag/gunbc/design_document.dag) · [docs/plans/compiler-guarantee-recovery-gap-analysis.md](docs/plans/compiler-guarantee-recovery-gap-analysis.md) · [docs/plans/cardinality-refinement.md](docs/plans/cardinality-refinement.md) · [docs/plans/typed-module-cross-run-materialization.md](docs/plans/typed-module-cross-run-materialization.md) · [dag/gunbc/roadmap/roadmap_authority.dag](dag/gunbc/roadmap/roadmap_authority.dag) · [dag/test/claim/closing/namespace_reference_derived_producer_bounded_closing_contract_witness_test.dag](dag/test/claim/closing/namespace_reference_derived_producer_bounded_closing_contract_witness_test.dag) · [dag/test/claim/closing/2_scm_native_write_spine_acceptance_closing_contract_witness_test.dag](dag/test/claim/closing/2_scm_native_write_spine_acceptance_closing_contract_witness_test.dag) · [dag/test/claim/closing/2_scm_native_authority_program_closing_contract_witness_test.dag](dag/test/claim/closing/2_scm_native_authority_program_closing_contract_witness_test.dag) · [dag/test/claim/closing/namespace_cross_file_provenance_closing_contract_witness_test.dag](dag/test/claim/closing/namespace_cross_file_provenance_closing_contract_witness_test.dag) · [dag/test/claim/closing/v1_materialization_kernel_closing_contract_witness_test.dag](dag/test/claim/closing/v1_materialization_kernel_closing_contract_witness_test.dag) · [dag/test/claim/closing/gate_refusal_reason_survives_wrapper_closing_contract_witness_test.dag](dag/test/claim/closing/gate_refusal_reason_survives_wrapper_closing_contract_witness_test.dag) · [dag/test/claim/closing/toolchain_pin_model_closing_contract_witness_test.dag](dag/test/claim/closing/toolchain_pin_model_closing_contract_witness_test.dag) · [dag/test/claim/closing/instrument_motion_physical_qualification_closing_contract_witness_test.dag](dag/test/claim/closing/instrument_motion_physical_qualification_closing_contract_witness_test.dag) · [dag/test/claim/closing/instrument_rendered_control_coverage_closing_contract_witness_test.dag](dag/test/claim/closing/instrument_rendered_control_coverage_closing_contract_witness_test.dag) · [dag/test/claim/closing/discarded_bool_result_wall_closing_contract_witness_test.dag](dag/test/claim/closing/discarded_bool_result_wall_closing_contract_witness_test.dag) · [dag/test/claim/closing/ladder_probe_corpus_closing_contract_witness_test.dag](dag/test/claim/closing/ladder_probe_corpus_closing_contract_witness_test.dag) · [dag/test/claim/closing/method_established_surface_wall_closing_contract_witness_test.dag](dag/test/claim/closing/method_established_surface_wall_closing_contract_witness_test.dag) · [dag/test/claim/closing/call_label_and_surplus_wall_closing_contract_witness_test.dag](dag/test/claim/closing/call_label_and_surplus_wall_closing_contract_witness_test.dag) · [dag/test/claim/closing/declared_conformance_ground_fragment_closing_contract_witness_test.dag](dag/test/claim/closing/declared_conformance_ground_fragment_closing_contract_witness_test.dag) · [dag/test/claim/closing/v2_self_grounding_frontier_closing_contract_witness_test.dag](dag/test/claim/closing/v2_self_grounding_frontier_closing_contract_witness_test.dag) · [dag/test/claim/closing/interpreter_primitive_roster_closing_contract_witness_test.dag](dag/test/claim/closing/interpreter_primitive_roster_closing_contract_witness_test.dag) · [dag/test/claim/closing/unforgeable_construction_capability_closing_contract_witness_test.dag](dag/test/claim/closing/unforgeable_construction_capability_closing_contract_witness_test.dag) · [dag/test/claim/closing/typed_store_cold_warm_measurement_closing_contract_witness_test.dag](dag/test/claim/closing/typed_store_cold_warm_measurement_closing_contract_witness_test.dag) · [dag/test/claim/closing/compiler_identity_invariant_under_corpus_commit_closing_contract_witness_test.dag](dag/test/claim/closing/compiler_identity_invariant_under_corpus_commit_closing_contract_witness_test.dag). +**Focused view — the compute fabric + the infrastructure stabilisation lanes + fleet convergence from main + the harness, roadmap workflow and dashboard lanes.** 143 active deliverable(s) in other lanes are declared in the authority and hidden here; nothing is deleted or parked by focusing. Clear `roadmap_focus_selection` in `dag/gunbc/roadmap/roadmap_authority.dag` to restore the full page. 11 of the rows below are NOT lane deliverables — they are prerequisites pulled in from other lanes because lane work is blocked on them: commit-writer-admission, shell-gate-migration, shell-effectplan-to-bash, shell-typed-invocation, placement-compile-pool-envelope, placement-live-roster-preflight, observation-scoped-run-consumer, observation-scoped-run-seed-growth-justification, observation-scoped-run-seed-growth-justification-closing-contract, fleet-spark-host-enrollment, confidence-semantic-impact-query. Hidden lanes remain readable through their carriers: [docs/plans/namespace-cut-replacement-plan.md](docs/plans/namespace-cut-replacement-plan.md) · [docs/plans/dag-scm-design.md](docs/plans/dag-scm-design.md) · [docs/plans/native-scm-cas-fit-and-consumer-cut.md](docs/plans/native-scm-cas-fit-and-consumer-cut.md) · [docs/plans/namespace-unique-on-chain-operational-plan.md](docs/plans/namespace-unique-on-chain-operational-plan.md) · [docs/plans/v2-self-hosting.md](docs/plans/v2-self-hosting.md) · [src/v2/compiler/05_emit.dag](src/v2/compiler/05_emit.dag) · [docs/plans/progress-observation-design.md](docs/plans/progress-observation-design.md) · [src/v2/compiler/self_host/candidate_generation.dag](src/v2/compiler/self_host/candidate_generation.dag) · [src/v2/compiler/self_host/stage0_production_target.dag](src/v2/compiler/self_host/stage0_production_target.dag) · [src/v2/compiler/self_host/wet_receipt_enrollment.dag](src/v2/compiler/self_host/wet_receipt_enrollment.dag) · [src/v2/workflow/rust_crate_partition.dag](src/v2/workflow/rust_crate_partition.dag) · [src/v2/compiler/self_host/v2_emitter_direct_rust_door_contract.dag](src/v2/compiler/self_host/v2_emitter_direct_rust_door_contract.dag) · [dag/gunbc/v1/v1_deletion_plan.dag](dag/gunbc/v1/v1_deletion_plan.dag) · [dag/gunbc/stage0/stage0_rust_host_observation.dag](dag/gunbc/stage0/stage0_rust_host_observation.dag) · [docs/plans/witness-realization-plan.md](docs/plans/witness-realization-plan.md) · [src/v1/05_emit_rust.dag](src/v1/05_emit_rust.dag) · [dag/gunbc/v1/v1_interpreter_primitive_surface.dag](dag/gunbc/v1/v1_interpreter_primitive_surface.dag) · [docs/plans/shell-to-dag-residual-census-and-arc-completion.md](docs/plans/shell-to-dag-residual-census-and-arc-completion.md) · [docs/plans/roadmap-workspace-ux-plan.md](docs/plans/roadmap-workspace-ux-plan.md) · [docs/plans/hermetic-tool-provisioning-design.md](docs/plans/hermetic-tool-provisioning-design.md) · [dag/gunbc/capability_binding.dag](dag/gunbc/capability_binding.dag) · [dag/gunbc/roadmap/roadmap_component.dag](dag/gunbc/roadmap/roadmap_component.dag) · [dag/gunbc/design_document.dag](dag/gunbc/design_document.dag) · [docs/plans/compiler-guarantee-recovery-gap-analysis.md](docs/plans/compiler-guarantee-recovery-gap-analysis.md) · [docs/plans/cardinality-refinement.md](docs/plans/cardinality-refinement.md) · [docs/plans/typed-module-cross-run-materialization.md](docs/plans/typed-module-cross-run-materialization.md) · [dag/gunbc/roadmap/roadmap_authority.dag](dag/gunbc/roadmap/roadmap_authority.dag) · [dag/test/claim/closing/namespace_reference_derived_producer_bounded_closing_contract_witness_test.dag](dag/test/claim/closing/namespace_reference_derived_producer_bounded_closing_contract_witness_test.dag) · [dag/test/claim/closing/2_scm_native_write_spine_acceptance_closing_contract_witness_test.dag](dag/test/claim/closing/2_scm_native_write_spine_acceptance_closing_contract_witness_test.dag) · [dag/test/claim/closing/2_scm_native_authority_program_closing_contract_witness_test.dag](dag/test/claim/closing/2_scm_native_authority_program_closing_contract_witness_test.dag) · [dag/test/claim/closing/namespace_cross_file_provenance_closing_contract_witness_test.dag](dag/test/claim/closing/namespace_cross_file_provenance_closing_contract_witness_test.dag) · [dag/test/claim/closing/v1_materialization_kernel_closing_contract_witness_test.dag](dag/test/claim/closing/v1_materialization_kernel_closing_contract_witness_test.dag) · [dag/test/claim/closing/gate_refusal_reason_survives_wrapper_closing_contract_witness_test.dag](dag/test/claim/closing/gate_refusal_reason_survives_wrapper_closing_contract_witness_test.dag) · [dag/test/claim/closing/toolchain_pin_model_closing_contract_witness_test.dag](dag/test/claim/closing/toolchain_pin_model_closing_contract_witness_test.dag) · [dag/test/claim/closing/instrument_motion_physical_qualification_closing_contract_witness_test.dag](dag/test/claim/closing/instrument_motion_physical_qualification_closing_contract_witness_test.dag) · [dag/test/claim/closing/instrument_rendered_control_coverage_closing_contract_witness_test.dag](dag/test/claim/closing/instrument_rendered_control_coverage_closing_contract_witness_test.dag) · [dag/test/claim/closing/discarded_bool_result_wall_closing_contract_witness_test.dag](dag/test/claim/closing/discarded_bool_result_wall_closing_contract_witness_test.dag) · [dag/test/claim/closing/ladder_probe_corpus_closing_contract_witness_test.dag](dag/test/claim/closing/ladder_probe_corpus_closing_contract_witness_test.dag) · [dag/test/claim/closing/method_established_surface_wall_closing_contract_witness_test.dag](dag/test/claim/closing/method_established_surface_wall_closing_contract_witness_test.dag) · [dag/test/claim/closing/call_label_and_surplus_wall_closing_contract_witness_test.dag](dag/test/claim/closing/call_label_and_surplus_wall_closing_contract_witness_test.dag) · [dag/test/claim/closing/declared_conformance_ground_fragment_closing_contract_witness_test.dag](dag/test/claim/closing/declared_conformance_ground_fragment_closing_contract_witness_test.dag) · [dag/test/claim/closing/v2_self_grounding_frontier_closing_contract_witness_test.dag](dag/test/claim/closing/v2_self_grounding_frontier_closing_contract_witness_test.dag) · [dag/test/claim/closing/interpreter_primitive_roster_closing_contract_witness_test.dag](dag/test/claim/closing/interpreter_primitive_roster_closing_contract_witness_test.dag) · [dag/test/claim/closing/unforgeable_construction_capability_closing_contract_witness_test.dag](dag/test/claim/closing/unforgeable_construction_capability_closing_contract_witness_test.dag) · [dag/test/claim/closing/typed_store_cold_warm_measurement_closing_contract_witness_test.dag](dag/test/claim/closing/typed_store_cold_warm_measurement_closing_contract_witness_test.dag) · [dag/test/claim/closing/compiler_identity_invariant_under_corpus_commit_closing_contract_witness_test.dag](dag/test/claim/closing/compiler_identity_invariant_under_corpus_commit_closing_contract_witness_test.dag). - [x] **Run the worker on DeepSeek V4 Flash with thinking on, straight at the engines, from briefs it can finish** — The harness posts to the Spark vLLM engines directly on the chat-completions shape with Think Max as the request switch, decodes inline reasoning client-side, replays it, and derives its deadline from the engine's own decode rate. A write brief names files small enough to hold whole and the decisions already made. Why: A day of runs with 0 files changed: briefs naming one file when the change spans its importers, a co-tenanted router killing every long step, a deadline that could not cover max_tokens, and agents deliberating modeling decisions a brief should have made. [authority](dag/gunbc/harness/harness_cli.dag) — ✓ signed off: operator curation 2026-09-06 (session 019iXPtAqzPaNBZbaaM5rxrY) - [x] **The roadmap commits, verifies, and opens the pull request itself once verification passes** — After the provider completes, the belt commits the attempt worktree, verifies the committed head in a detached checkout, admits publication only on a ValidationPassed receipt for that exact head, and the token-holding helper pushes the branch and opens the pull request, then answers with what GitHub shows. Why: Verification was checking out an uncommitted worktree's head, publication never consulted the verdict, and no operation existed to push or create a pull request, so every attempt stalled in the Agent segment and a human harvested by hand. [authority](dag/gunbc/roadmap/roadmap_publish_admission.dag) — ✓ signed off: operator curation 2026-09-06 (session 019iXPtAqzPaNBZbaaM5rxrY) From 933b25d8dcac2349d4355781aa86e453fb4d8e2b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 21 Sep 2026 01:01:19 +0000 Subject: [PATCH 4/6] Staging cleanup is a root mutation, so it carries the same path authority the write does The ordering repair stopped `install -d` beneath an untrusted ancestor, but converge_controller_app_key still evaluated clear_staging unconditionally, and clear_staging BEGINS with an elevated leg: run_elevated_leg(staging_remove_argv) = sudo rm -f -- . The non-write arms of the preceding match produce `none`; they did not skip cleanup. So this execution was representable: /etc/gunbc group- or other-writable -> PathsNotRootOnly -> directory only OBSERVED -> controller_app_key_action refuses -> no key content written -> ELEVATED rm STILL EXECUTES BENEATH THE REFUSED ANCESTOR. The consequence is not residue. A non-root principal who can write an upper ancestor can replace an intermediate path component -- a directory or a symlink -- between the observation and the leg, so the route performs a ROOT MUTATION THROUGH THE EXACT PATH WHOSE CONTAINMENT IT JUST DECLINED TO TRUST. The module note said staging is removed "after every run whether or not a write was attempted" and the code implemented that literally. The correct boundary is narrower and the note now states it: after every attempt WHOSE ANCESTOR AND PARENT-DIRECTORY AUTHORITY HAS BEEN ESTABLISHED. The gate is PATH AUTHORITY and deliberately not the whole action: a content or file-metadata observation may be unobservable while the path is safely root-contained, and cleanup is still desirable there. StagingCleanupAuthorization is sole_constructor, so the bad state is UNWRITABLE rather than merely unreached (DESIGN 4b rung 4) -- admit_staging_cleanup is the only mint, joining upper ancestors = PathsRootOnly, directory = KeyDirRootOnly, and staging's parent being that admitted directory. clear_staging now accepts the sealed authorization instead of a bare subject and a bare path, so a cleanup leg over an unadmitted path has no spelling. The withheld arm carries StagingUnobservable, which controller_app_key_custody already counts as not-held. WHY THE PREVIOUS 21 COULD NOT SEE IT: the ordering controls invoke only the pure decision with supplied values and never execute clear_staging, so a control proving controller_app_key_action refuses was already green while the cleanup mutation ran. Five controls added over the admission fold, which is the whole gate: writable upper ancestor -> withheld; unsafe key directory -> withheld; UNREADABLE key directory -> withheld (blind is not safe); staging path outside the admitted directory -> withheld (the join, not merely the two readings); and root-only ancestors + root-only directory -> an authorization naming the exact parent and staging path. The four withheld arms and the positive control discriminate each other. 26/26 witnesses PASS in one claim_batch over the module. Co-Authored-By: Claude Opus 5 (1M context) --- .../microvm_controller_app_key_converge.dag | 89 ++++++++++++-- ...ntroller_app_key_converge_witness_test.dag | 115 ++++++++++++++++++ 2 files changed, 194 insertions(+), 10 deletions(-) diff --git a/dag/gunbc/runner/microvm_controller_app_key_converge.dag b/dag/gunbc/runner/microvm_controller_app_key_converge.dag index 4ec1317e153..d9dbd248cb5 100644 --- a/dag/gunbc/runner/microvm_controller_app_key_converge.dag +++ b/dag/gunbc/runner/microvm_controller_app_key_converge.dag @@ -115,9 +115,12 @@ import gunbc.runner_host_file_converge { // PLAINTEXT STAGING. The only staging is the far-side sibling .gunbc-staging that // converge_typed_remote_file writes, modes and renames. It lives inside the root-only directory, // which is verified BEFORE the stage leg runs, so even the moment between `dd` and `chmod 400` is not -// observable by a non-root uid. It is removed after every run whether or not a write was attempted, -// and its absence is READ BACK; a failed removal or a surviving sibling refuses the run (the -// cleanup-is-part-of-the-mint rule of gunbc.secret_provision_actuator). +// observable by a non-root uid. It is removed after every attempt WHOSE ANCESTOR AND +// PARENT-DIRECTORY AUTHORITY HAS BEEN ESTABLISHED -- whether or not a write was attempted, but never +// beneath a path the route declined to trust, because `rm` is a root mutation through that same path +// (see StagingCleanupAuthorization). Its absence is READ BACK; a failed removal, a surviving sibling, +// or a withheld cleanup refuses the run (the cleanup-is-part-of-the-mint rule of +// gunbc.secret_provision_actuator). // ── Placement (pure) ───────────────────────────────────────────────────────────────────────────── @@ -260,6 +263,66 @@ type StagingResidue | StagingResiduePresent { path: String } | StagingUnobservable { reason: String } +// CLEANUP IS A ROOT MUTATION, so it is entitled to the same path authority the WRITE is. The +// earlier revision ran `rm -f --` beneath the very ancestors controller_app_key_action had just +// declined to trust: the non-write arms of that match produced `none` and then fell through to an +// unconditional clear_staging. A group- or other-writable upper ancestor made this representable -- +// PathsNotRootOnly, directory only observed, action refused, no key content written, and an +// ELEVATED rm still executing through a path component a non-root principal can replace with a +// directory or a symlink between the observation and the leg. That is not residue; it is a root +// mutation through the exact containment the route declined to trust. +// +// The gate is PATH AUTHORITY and deliberately not the whole action: a content or file-metadata +// observation may be unobservable while the path is safely root-contained, and cleanup is still +// desirable there. So the seal joins three facts and nothing else -- upper ancestors PathsRootOnly, +// the key directory KeyDirRootOnly, and the staging path's parent being that admitted directory. +// sole_constructor makes the bad state UNWRITABLE rather than merely unreached (DESIGN §4b rung 4): +// clear_staging accepts the sealed authorization, so there is no way to spell a cleanup leg over a +// subject and a bare path that no admission fold produced. +type StagingCleanupAuthorization sole_constructor { + subject: ControllerKeyHost + parent: String + staging: String +} + +type StagingCleanupAdmission + = StagingCleanupAuthorized { authorization: StagingCleanupAuthorization } + | StagingCleanupWithheld { reason: String } + +// THE ONLY MINT. PURE, over readings the caller already has: no leg runs here. +fn admit_staging_cleanup( + subject: ControllerKeyHost, + upper_ancestors: RunnerHostPathMetadata, + dir: KeyDirMetadata, + key_dir: String, + staging: String, +) -> StagingCleanupAdmission { + match upper_ancestors { + PathsRootOnly => + match dir { + KeyDirRootOnly => + if path_parent(path: staging) != key_dir { + StagingCleanupWithheld { reason: join(["staging parent ", path_parent(path: staging), " is not the admitted key directory ", key_dir], "") } + } else { + StagingCleanupAuthorized { + authorization: StagingCleanupAuthorization { subject: subject, parent: key_dir, staging: staging }, + } + } + _ => StagingCleanupWithheld { reason: concat("key directory is not root-only: ", key_dir_metadata_wire(m: dir)) } + } + _ => StagingCleanupWithheld { reason: concat("an ancestor directory is not root-only: ", runner_host_path_metadata_wire(m: upper_ancestors)) } + } +} + +data staging_cleanup_withheld_reason: String = "staging cleanup withheld because root-only path authority was not established" + +fn staging_cleanup_admission_wire(a: StagingCleanupAdmission) -> String { + match a { + StagingCleanupAuthorized { authorization: z } => concat("authorized ", z.staging) + StagingCleanupWithheld { reason: r } => concat("WITHHELD ", r) + } +} + // PURE, over a listing that SUCCEEDED. The caller reaches this only on a successful leg, so every // arm here is a reading of what the parent contains -- there is no exit code to misread. The argv // and the membership read are member_observe's (parent_listing_argv, listing_contains_entry): only @@ -604,14 +667,15 @@ fn observe_key_content(subject: ControllerKeyHost, context: FleetSshExecutionCon // distinguish "removed" from "never there" -- which is fine -- nor "there and still there", which is // not; the presence test is what answers that. fn clear_staging( - subject: ControllerKeyHost, + authorization: StagingCleanupAuthorization, context: FleetSshExecutionContext, - staging: String, - staging_parent: String, staging_name: String, ) -> StagingResidue uses net: Network { + let subject = authorization.subject + let staging = authorization.staging + let staging_parent = authorization.parent match run_elevated_leg(subject: subject, context: context, argv: staging_remove_argv(staging: staging), stdin_payload: "") { ElevatedLegRefused { reason: r } => StagingUnobservable { reason: concat("staging removal not run: ", r) } ElevatedLegRan { exit_code: rc, stdout: _, stderr: re } => @@ -708,13 +772,18 @@ fn converge_controller_app_key( } _ => none } - let staging_after = clear_staging( + let cleanup_admission = admit_staging_cleanup( subject: subject, - context: context, + upper_ancestors: ancestors_before, + dir: dir_before, + key_dir: key_dir as String, staging: staging, - staging_parent: path_parent(path: staging), - staging_name: path_basename(path: staging), ) + let staging_after = match cleanup_admission { + StagingCleanupAuthorized { authorization: z } => + clear_staging(authorization: z, context: context, staging_name: path_basename(path: staging)) + StagingCleanupWithheld { reason: _ } => StagingUnobservable { reason: staging_cleanup_withheld_reason } + } ControllerAppKeyRun { host: subject.host, key_path: placed_path, diff --git a/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag b/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag index cbcea5103ed..d216e165569 100644 --- a/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag +++ b/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag @@ -48,6 +48,10 @@ import gunbc.microvm_controller_app_key_converge { controller_app_key_action, key_path_find_argv, key_path_exactly_owner_read_clause, + KeyDirMetadataUnobservable, + admit_staging_cleanup, + StagingCleanupAuthorized, + StagingCleanupWithheld, } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -63,6 +67,8 @@ data held_file: KeyPathFindReading = KeyPathFindReading { root_owned: true, grou data held_dir: KeyPathFindReading = KeyPathFindReading { root_owned: true, group_or_other_bits: false, exactly_owner_read: false } data staging_path: String = "/etc/gunbc/microvm-controller/app.pem.gunbc-staging" + +data cleanup_key_dir: String = "/etc/gunbc/microvm-controller" data staging_name: String = "app.pem.gunbc-staging" // THE STAGING READING IS SUPPLIED AS THE VALUE IT IS, not as an exit code. classify_staging_residue @@ -275,3 +281,112 @@ test fn an_empty_parent_listing_is_absence_because_the_parent_was_read() -> Bool _ => false } } + + +// ── cleanup is a root mutation, so it carries the same path authority the write does ──────────── + +// THE FOURTH FINDING IN THIS FAMILY, one step further down the same route. The ordering repair +// stopped `install -d` beneath an untrusted ancestor, but clear_staging still ran UNCONDITIONALLY +// after the action refused, and it BEGINS with `sudo rm -f -- `. On a host whose /etc or +// /etc/gunbc is group- or other-writable the route refused the write and then performed a root +// mutation through the very path component it had declined to trust -- a component a non-root +// principal can replace with a directory or a symlink between the observation and the leg. +// +// These controls run the PURE admission, which is the whole gate: sole_constructor means +// StagingCleanupAuthorization exists nowhere else, so an unauthorized arm has no value to pass to +// clear_staging and the rm has no way to be spelled. The previous 21 could not see the defect +// because they invoked only controller_app_key_action and never reached the cleanup leg. + +test fn a_writable_upper_ancestor_withholds_the_staging_cleanup() -> Bool { + match controller_key_host(host: operator_host_srv2) { + ControllerKeyHostRefused { cause: _ } => false + ControllerKeyHostAdmitted { subject: s } => + match admit_staging_cleanup( + subject: s, + upper_ancestors: PathsNotRootOnly { paths: ["/etc/gunbc"], detail: "" }, + dir: KeyDirRootOnly, + key_dir: cleanup_key_dir, + staging: staging_path, + ) { + StagingCleanupWithheld { reason: r } => string_contains(s: r, pattern: "ancestor") + StagingCleanupAuthorized { authorization: _ } => false + } + } +} + +test fn an_unsafe_key_directory_withholds_the_staging_cleanup() -> Bool { + match controller_key_host(host: operator_host_srv2) { + ControllerKeyHostRefused { cause: _ } => false + ControllerKeyHostAdmitted { subject: s } => + match admit_staging_cleanup( + subject: s, + upper_ancestors: PathsRootOnly, + dir: KeyDirGroupOrOtherAccess, + key_dir: cleanup_key_dir, + staging: staging_path, + ) { + StagingCleanupWithheld { reason: r } => string_contains(s: r, pattern: "not root-only") + StagingCleanupAuthorized { authorization: _ } => false + } + } +} + +// UNREADABLE IS NOT SAFE. A directory whose metadata could not be read is exactly the state where a +// cleanup leg would be running blind, so it withholds for the same reason an unsafe one does. +test fn an_unreadable_key_directory_withholds_the_staging_cleanup() -> Bool { + match controller_key_host(host: operator_host_srv2) { + ControllerKeyHostRefused { cause: _ } => false + ControllerKeyHostAdmitted { subject: s } => + match admit_staging_cleanup( + subject: s, + upper_ancestors: PathsRootOnly, + dir: KeyDirMetadataUnobservable { reason: "find leg exit=1" }, + key_dir: cleanup_key_dir, + staging: staging_path, + ) { + StagingCleanupWithheld { reason: _ } => true + StagingCleanupAuthorized { authorization: _ } => false + } + } +} + +// THE JOIN, not merely the two readings: a staging path whose parent is NOT the directory that was +// admitted is unauthorized even when both readings are root-only, because the authority established +// is over that directory and nothing else. +test fn a_staging_path_outside_the_admitted_directory_is_withheld() -> Bool { + match controller_key_host(host: operator_host_srv2) { + ControllerKeyHostRefused { cause: _ } => false + ControllerKeyHostAdmitted { subject: s } => + match admit_staging_cleanup( + subject: s, + upper_ancestors: PathsRootOnly, + dir: KeyDirRootOnly, + key_dir: cleanup_key_dir, + staging: "/tmp/app.pem.gunbc-staging", + ) { + StagingCleanupWithheld { reason: r } => string_contains(s: r, pattern: "admitted key directory") + StagingCleanupAuthorized { authorization: _ } => false + } + } +} + +// THE POSITIVE CONTROL. Root-only ancestors and a root-only directory containing the staging path +// authorize exactly one cleanup, and the seal names the exact parent and staging path the leg will +// run over -- not the subject's idea of them. +test fn root_only_ancestors_and_directory_authorize_the_exact_staging_path() -> Bool { + match controller_key_host(host: operator_host_srv2) { + ControllerKeyHostRefused { cause: _ } => false + ControllerKeyHostAdmitted { subject: s } => + match admit_staging_cleanup( + subject: s, + upper_ancestors: PathsRootOnly, + dir: KeyDirRootOnly, + key_dir: cleanup_key_dir, + staging: staging_path, + ) { + StagingCleanupAuthorized { authorization: z } => + z.staging == staging_path && z.parent == cleanup_key_dir && (z.subject.host as String) == (operator_host_srv2 as String) + StagingCleanupWithheld { reason: _ } => false + } + } +} From 5ac6ab2a09ec45ddb79f669fa1d6b9212753e7bf Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 21 Sep 2026 01:36:01 +0000 Subject: [PATCH 5/6] Derive the residue predicate's key from the seal: the rung was claimed, not constructed review 69444, raised as REQUEST_CHANGES against the cleanup-authorization repair. The module note at the sole_constructor claim says clear_staging accepts the sealed authorization "so there is no way to spell a cleanup leg over a subject and a bare path that no admission fold produced". That was true of the subject, the parent and the path -- and NOT of staging_name, which clear_staging still took as an unsealed parameter beside the seal, and which is precisely the value classify_staging_residue KEYS ON. A name that does not match authorization.staging reads a parent listing CONTAINING the residue as StagingAbsent, and that absence feeds ControllerAppKeyHeld: the same false-absence class the parent-listing repair in this PR exists to close. The defect is not a live one -- the single production caller passed path_basename(path: staging) over the same value -- so this is not a behaviour fix. It is a RUNG HONESTY fix (DESIGN 4b meta-obligation 1: the reported rung must equal the rung established by executed evidence). A comment asserting a seal covers a value the seal does not reach is an overclaim, and shipping one inside the PR whose subject is overclaims is the defect in a new place. So staging_name is DERIVED inside clear_staging from authorization.staging and the parameter is deleted, which makes the comment true rather than making the comment softer -- construction over restatement (DESIGN 5). Every value the leg uses now comes from the seal: subject, parent, path, and the residue predicate's key. The note is corrected to say exactly that. 26/26 witnesses PASS in one claim_batch at this source head. Co-Authored-By: Claude Opus 5 (1M context) --- .../microvm_controller_app_key_converge.dag | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/runner/microvm_controller_app_key_converge.dag b/dag/gunbc/runner/microvm_controller_app_key_converge.dag index d9dbd248cb5..64b2448835e 100644 --- a/dag/gunbc/runner/microvm_controller_app_key_converge.dag +++ b/dag/gunbc/runner/microvm_controller_app_key_converge.dag @@ -277,8 +277,9 @@ type StagingResidue // desirable there. So the seal joins three facts and nothing else -- upper ancestors PathsRootOnly, // the key directory KeyDirRootOnly, and the staging path's parent being that admitted directory. // sole_constructor makes the bad state UNWRITABLE rather than merely unreached (DESIGN §4b rung 4): -// clear_staging accepts the sealed authorization, so there is no way to spell a cleanup leg over a -// subject and a bare path that no admission fold produced. +// clear_staging accepts the sealed authorization and DERIVES every value the leg uses from it -- +// subject, parent, path and the residue predicate's key -- so there is no way to spell a cleanup leg, +// or a residue reading over one, that no admission fold produced. type StagingCleanupAuthorization sole_constructor { subject: ControllerKeyHost parent: String @@ -669,13 +670,20 @@ fn observe_key_content(subject: ControllerKeyHost, context: FleetSshExecutionCon fn clear_staging( authorization: StagingCleanupAuthorization, context: FleetSshExecutionContext, - staging_name: String, ) -> StagingResidue uses net: Network { let subject = authorization.subject let staging = authorization.staging let staging_parent = authorization.parent + // THE RESIDUE PREDICATE'S KEY IS DERIVED FROM THE SEAL, never supplied beside it. As a parameter + // it was the one value of the three a caller could still spell freely, and it is exactly what + // classify_staging_residue keys on: a name that does not match authorization.staging reads a + // listing CONTAINING the residue as StagingAbsent, and that absence feeds ControllerAppKeyHeld -- + // the same false-absence class the parent-listing repair above exists to close. Deriving it here + // is what makes the sole_constructor claim true of every input the leg uses rather than of two of + // the three (DESIGN 4b meta-obligation 1; 5, construction over validation). + let staging_name = path_basename(path: staging) match run_elevated_leg(subject: subject, context: context, argv: staging_remove_argv(staging: staging), stdin_payload: "") { ElevatedLegRefused { reason: r } => StagingUnobservable { reason: concat("staging removal not run: ", r) } ElevatedLegRan { exit_code: rc, stdout: _, stderr: re } => @@ -781,7 +789,7 @@ fn converge_controller_app_key( ) let staging_after = match cleanup_admission { StagingCleanupAuthorized { authorization: z } => - clear_staging(authorization: z, context: context, staging_name: path_basename(path: staging)) + clear_staging(authorization: z, context: context) StagingCleanupWithheld { reason: _ } => StagingUnobservable { reason: staging_cleanup_withheld_reason } } ControllerAppKeyRun { From 37e759fbaf9d85fd14f56bdcead5af41aac75799 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 21 Sep 2026 02:14:24 +0000 Subject: [PATCH 6/6] The withheld arm threw away the located cause, and the wire meant to carry it was dangling review 69456. Both halves are one defect and one edit fixes both. staging_cleanup_admission_wire was added for symmetry with the other *_wire functions in this module and never given a consumer: git grep returned its own definition and nothing else. DESIGN 3c -- a declaration with no call site in the closure is dangling, and dangling is red regardless of how well modeled it is. The consumer it should have had was one line away. The withheld arm at the converge call site matched StagingCleanupWithheld { reason: _ } and substituted the constant staging_cleanup_withheld_reason, so the receipt said "root-only path authority was not established" without saying WHICH of the three joined facts failed -- while admit_staging_cleanup had just computed exactly that string. An operator reading that receipt cannot tell whether to fix an ancestor, fix the directory, or fix a staging path pointing outside it. That is a typed diagnostic that is not a LOCATED one (DESIGN 5), and it is the flattening this PR exists to remove, reintroduced one layer down in the repair itself. So the cause is threaded through and the constant is demoted to a PREFIX, which is what it always was; the dangling wire is deleted rather than given a ceremonial call, because the located string is what the receipt needs and the wire added nothing over it. A 27th control asserts the three withheld causes are PAIRWISE DISTINCT and non-empty. That is what makes "located" a property rather than a claim: it reddens if the causes are ever flattened back onto one constant, which is precisely the defect 69456 caught. 38/38 witnesses PASS in one claim_batch from the composed head -- 27 App-key converge plus the 11 member_identity. Co-Authored-By: Claude Opus 5 (1M context) --- .../microvm_controller_app_key_converge.dag | 14 +++++----- ...ntroller_app_key_converge_witness_test.dag | 26 +++++++++++++++++++ 2 files changed, 32 insertions(+), 8 deletions(-) diff --git a/dag/gunbc/runner/microvm_controller_app_key_converge.dag b/dag/gunbc/runner/microvm_controller_app_key_converge.dag index 64b2448835e..61b9dc3f2d8 100644 --- a/dag/gunbc/runner/microvm_controller_app_key_converge.dag +++ b/dag/gunbc/runner/microvm_controller_app_key_converge.dag @@ -315,15 +315,13 @@ fn admit_staging_cleanup( } } +// THE PREFIX, not the whole reason. admit_staging_cleanup has already computed WHICH of the three +// joined facts failed, and the withheld arm carries that cause through rather than flattening it: +// a receipt saying only "authority was not established" cannot tell an operator whether to fix an +// ancestor, the directory, or a staging path pointing outside it (DESIGN 5 -- a typed, LOCATED +// diagnostic). data staging_cleanup_withheld_reason: String = "staging cleanup withheld because root-only path authority was not established" -fn staging_cleanup_admission_wire(a: StagingCleanupAdmission) -> String { - match a { - StagingCleanupAuthorized { authorization: z } => concat("authorized ", z.staging) - StagingCleanupWithheld { reason: r } => concat("WITHHELD ", r) - } -} - // PURE, over a listing that SUCCEEDED. The caller reaches this only on a successful leg, so every // arm here is a reading of what the parent contains -- there is no exit code to misread. The argv // and the membership read are member_observe's (parent_listing_argv, listing_contains_entry): only @@ -790,7 +788,7 @@ fn converge_controller_app_key( let staging_after = match cleanup_admission { StagingCleanupAuthorized { authorization: z } => clear_staging(authorization: z, context: context) - StagingCleanupWithheld { reason: _ } => StagingUnobservable { reason: staging_cleanup_withheld_reason } + StagingCleanupWithheld { reason: r } => StagingUnobservable { reason: join([staging_cleanup_withheld_reason, ": ", r], "") } } ControllerAppKeyRun { host: subject.host, diff --git a/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag b/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag index d216e165569..c69b9773ba6 100644 --- a/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag +++ b/dag/test/claim/runner/microvm_controller_app_key_converge_witness_test.dag @@ -390,3 +390,29 @@ test fn root_only_ancestors_and_directory_authorize_the_exact_staging_path() -> } } } + +// THE THREE WITHHELD CAUSES ARE DISTINCT, which is what makes the diagnostic LOCATED rather than +// merely typed. An earlier revision discarded admit_staging_cleanup's computed cause at the call +// site and substituted one constant, so a receipt said "root-only path authority was not +// established" without saying whether an operator should fix an ancestor, the directory, or a +// staging path pointing outside it. This reddens if the three are ever flattened back together. +test fn the_three_withheld_causes_name_which_fact_failed() -> Bool { + match controller_key_host(host: operator_host_srv2) { + ControllerKeyHostRefused { cause: _ } => false + ControllerKeyHostAdmitted { subject: s } => { + let ancestor_cause = match admit_staging_cleanup(subject: s, upper_ancestors: PathsNotRootOnly { paths: ["/etc/gunbc"], detail: "" }, dir: KeyDirRootOnly, key_dir: cleanup_key_dir, staging: staging_path) { + StagingCleanupWithheld { reason: r } => r + StagingCleanupAuthorized { authorization: _ } => "" + } + let dir_cause = match admit_staging_cleanup(subject: s, upper_ancestors: PathsRootOnly, dir: KeyDirGroupOrOtherAccess, key_dir: cleanup_key_dir, staging: staging_path) { + StagingCleanupWithheld { reason: r } => r + StagingCleanupAuthorized { authorization: _ } => "" + } + let path_cause = match admit_staging_cleanup(subject: s, upper_ancestors: PathsRootOnly, dir: KeyDirRootOnly, key_dir: cleanup_key_dir, staging: "/tmp/app.pem.gunbc-staging") { + StagingCleanupWithheld { reason: r } => r + StagingCleanupAuthorized { authorization: _ } => "" + } + ancestor_cause != "" && ancestor_cause != dir_cause && dir_cause != path_cause && ancestor_cause != path_cause + } + } +}