From c742e3f549e0720a901ad4b8e28c93011adf95a5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 02:49:37 +0000 Subject: [PATCH 01/15] WIP permit scope --- dag/gunbc/compile_permit_scope.dag | 49 ++++++++ dag/gunbc/runner/runner_unit_file.dag | 107 +++++++++++++----- dag/gunbc/witness/witness_floor_workflow.dag | 28 ++++- .../claim/run_disposition_witness_test.dag | 49 ++++++++ .../runner/runner_unit_file_witness_test.dag | 60 +++++++++- 5 files changed, 263 insertions(+), 30 deletions(-) create mode 100644 dag/gunbc/compile_permit_scope.dag diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag new file mode 100644 index 00000000000..7f8323b99ea --- /dev/null +++ b/dag/gunbc/compile_permit_scope.dag @@ -0,0 +1,49 @@ +module gunbc.compile_permit_scope + +import std.types { String, NonEmptyStr, Bool } +import std.measure { HardwareThreadCount } +import gunbc.host_converge { gunbc_runner_jobserver_default_fifo, gunbc_runner_jobserver_service } + +// WHETHER A COMPILE PERMIT OUTLIVES THE PROCESS THAT BORROWED IT. That single fact is what makes +// killing a running build either cheap or permanently expensive, and until now it was not written +// down anywhere -- it was implied by the runner unit always rendering a shared FIFO, which made the +// alternative unrepresentable rather than merely unchosen. +// +// The fleet's builds are bounded by a host-persistent GNU jobserver whose permits are returned +// COOPERATIVELY. A SIGKILLed cargo returns nothing, so every permit that process held is lost for +// the lifetime of the daemon; there is no reaper, and a host at zero permits still accepts jobs, +// which is why the symptom is a slow queue rather than a failure. gunbc#9789 contained the CAUSE by +// declaring NeverSupersedeRunning, and declared a DESIGN 4b(3) drop whose dissolve-on is this +// capability: no client of the required floor holds a host-persistent cooperative permit -- either +// the host FIFO is gone and compile parallelism is invocation-local to cargo, or the pool is +// server-owned with admission that survives client death. +// +// This module makes that capability a MODELLED FACT rather than a sentence in an annotation, so the +// containment retires by construction when the fleet changes rather than by someone remembering the +// row exists. The two arms below are the two the trigger names as sufficient; a third arm belongs +// here the day someone builds a server-owned pool, and not before -- an arm with no realization is +// vocabulary invented ahead of its consumer. +type CompilePermitScope + = HostPersistentPermitPool { fifo_path: String, daemon_service: NonEmptyStr } + | InvocationLocalParallelism { jobs_per_slot: HardwareThreadCount } + +// THE DECIDABLE QUESTION THE DISSOLVE-ON ASKS, answered by construction rather than by inspection. +// A borrower that cannot outlive its own permit cannot leak one, so the invalid state has no +// constructor under the second arm -- DESIGN 4b rung 4 for this class, reached by deleting the +// shared resource rather than by watching it. +fn permit_outlives_borrower(scope: CompilePermitScope) -> Bool { + match scope { + HostPersistentPermitPool { fifo_path: _, daemon_service: _ } => true + InvocationLocalParallelism { jobs_per_slot: _ } => false + } +} + +// WHAT THE FLEET RUNS TODAY. Flipping this row is the cutover, and because both the runner unit's +// environment and the required floor's supersession policy are DERIVED from it, the flip cannot +// move one without the other -- which is the disagreement DESIGN section 3 forbids and the specific +// way this containment could have gone stale: the fleet retires the FIFO, and CI keeps refusing to +// supersede for a reason that stopped being true. +data fleet_compile_permit_scope: CompilePermitScope = HostPersistentPermitPool { + fifo_path: gunbc_runner_jobserver_default_fifo, + daemon_service: gunbc_runner_jobserver_service as NonEmptyStr, +} diff --git a/dag/gunbc/runner/runner_unit_file.dag b/dag/gunbc/runner/runner_unit_file.dag index 8ae60561c86..d5e43e03676 100644 --- a/dag/gunbc/runner/runner_unit_file.dag +++ b/dag/gunbc/runner/runner_unit_file.dag @@ -1,11 +1,18 @@ module gunbc.runner_unit_file -import std.types { String, NonEmptyStr, List, Bool } +import std.types { String, NonEmptyStr, List, Bool, Int } +import std.measure { hardware_thread_count_value } import std.disposition { Disposition, SingleAuthority } import extdeps.github.actions { RunnerSpec, SelfHosted, HostedRunner, RunsOnExpression } import extdeps.github.actions_runner { actions_runner_base_dir } import extdeps.languages.json.emit { json_string, json_array, serialize_json } import extdeps.jobserver { jobserver_makeflags_fifo_auth } +import gunbc.compile_permit_scope { + CompilePermitScope, + HostPersistentPermitPool, + InvocationLocalParallelism, + fleet_compile_permit_scope +} import extdeps.systemd.unit_file { SystemdUnitFile, ServiceUnitFile, @@ -167,14 +174,52 @@ fn runner_unit_app_environment(app: GithubAppRunnerConfig) -> List List { - [ - runner_unit_environment(name: "CTRL_JOBSERVER_FIFO", value: fifo_path), - runner_unit_environment( - name: "MAKEFLAGS", - value: jobserver_makeflags_fifo_auth(fifo_path: fifo_path), - ), - ] +fn runner_unit_jobserver_environment(scope: CompilePermitScope) -> List { + match scope { + HostPersistentPermitPool { fifo_path: p, daemon_service: _ } => + [ + runner_unit_environment(name: "CTRL_JOBSERVER_FIFO", value: p), + runner_unit_environment( + name: "MAKEFLAGS", + value: jobserver_makeflags_fifo_auth(fifo_path: p), + ), + ] + // NO MAKEFLAGS, AND THAT ABSENCE IS THE POINT. Under invocation-local parallelism there is no + // shared pool to advertise, so handing cargo an auth clause would point it at a FIFO nobody + // serves. The bound moves to CARGO_BUILD_JOBS, which cargo applies per invocation and which + // therefore cannot survive the process that read it. + InvocationLocalParallelism { jobs_per_slot: j } => + [ + runner_unit_environment( + name: "CARGO_BUILD_JOBS", + value: to_string(hardware_thread_count_value(t: j) as Int), + ), + ] + } +} + +// THE ORDERING DEPENDENCY IS PART OF THE SAME FACT, not a constant beside it. Under the host- +// persistent arm a runner that starts before the daemon gets a job whose first cargo invocation +// fails on an unserved FIFO -- the pair was found ABSENT from the live srv1 unit on 2026-08-26. +// Under the invocation-local arm the service does not exist, and a unit ordering itself After a +// unit systemd cannot resolve is a fresh failure introduced by the cutover. So the dependency +// arrives and departs WITH the environment that needs it. +// Two accessors rather than one pair, because the emitted unit interleaves them -- After=network, +// After=daemon, Wants=network, Wants=daemon -- and a single function returning the pair would have +// reordered the file. The bytes are the artifact here (gunbc.generated_artifact_boundary), so a +// refactor that changes them is a change, not a cleanup. +fn runner_unit_jobserver_after(scope: CompilePermitScope) -> List { + match scope { + HostPersistentPermitPool { fifo_path: _, daemon_service: svc } => [After { target: svc }] + InvocationLocalParallelism { jobs_per_slot: _ } => [] + } +} + +fn runner_unit_jobserver_wants(scope: CompilePermitScope) -> List { + match scope { + HostPersistentPermitPool { fifo_path: _, daemon_service: svc } => [Wants { target: svc }] + InvocationLocalParallelism { jobs_per_slot: _ } => [] + } } // THE TEARDOWN PAIR IS THE WHOLE POINT OF THIS MODULE, AND IT IS A PARAMETER RATHER THAN A CONSTANT. @@ -198,7 +243,7 @@ type RunnerUnitFileRendering fn runner_unit_file( deploy: RunnerHostDeploy, spec: RunnerSpec, - jobserver_fifo: String, + permit_scope: CompilePermitScope, intent: RunnerUnitLifecycleIntent, ) -> RunnerUnitFileRendering { match runner_unit_labels_json(spec: spec) { @@ -217,20 +262,28 @@ fn runner_unit_file( RunnerUnitLabels { json_text: labels_json } => RunnerUnitFileRendered { file: ServiceUnitFile { - unit: [ - Description { - text: join([ - "Ephemeral GitHub Actions Runner (", - systemd_instance_name_specifier, - ")", - ], "") as NonEmptyStr, - }, - After { target: "network-online.target" as NonEmptyStr }, - After { target: gunbc_runner_jobserver_service as NonEmptyStr }, - Wants { target: "network-online.target" as NonEmptyStr }, - Wants { target: gunbc_runner_jobserver_service as NonEmptyStr }, - StartLimitIntervalSec { duration: "0" as NonEmptyStr }, - ], + unit: concat( + [ + Description { + text: join([ + "Ephemeral GitHub Actions Runner (", + systemd_instance_name_specifier, + ")", + ], "") as NonEmptyStr, + }, + After { target: "network-online.target" as NonEmptyStr }, + ], + concat( + runner_unit_jobserver_after(scope: permit_scope), + concat( + [Wants { target: "network-online.target" as NonEmptyStr }], + concat( + runner_unit_jobserver_wants(scope: permit_scope), + [StartLimitIntervalSec { duration: "0" as NonEmptyStr }], + ), + ), + ), + ), service: concat( concat( [ @@ -248,7 +301,7 @@ fn runner_unit_file( ), ), concat( - runner_unit_jobserver_environment(fifo_path: jobserver_fifo), + runner_unit_jobserver_environment(scope: permit_scope), concat( [ ExecStart { command: runner_lifecycle_jit_wrapper_path as NonEmptyStr }, @@ -272,12 +325,12 @@ fn runner_unit_file( fn gunbc_runner_unit_file( deploy: RunnerHostDeploy, spec: RunnerSpec, - jobserver_fifo: String, + permit_scope: CompilePermitScope, ) -> RunnerUnitFileRendering { runner_unit_file( deploy: deploy, spec: spec, - jobserver_fifo: jobserver_fifo, + permit_scope: permit_scope, intent: gunbc_runner_lifecycle_intent, ) } diff --git a/dag/gunbc/witness/witness_floor_workflow.dag b/dag/gunbc/witness/witness_floor_workflow.dag index ad75c9f9906..2159aa6ecbb 100644 --- a/dag/gunbc/witness/witness_floor_workflow.dag +++ b/dag/gunbc/witness/witness_floor_workflow.dag @@ -30,6 +30,12 @@ import gunbc.toolchain_workflow_steps { toolchain_home_isolation_step, toolchain_pin_rustup_default_step, } +import gunbc.compile_permit_scope { + CompilePermitScope, + HostPersistentPermitPool, + InvocationLocalParallelism, + fleet_compile_permit_scope +} import extdeps.github.actions { Workflow, Job, Step, RunStep, UsesStep, upload_artifact_action, @@ -273,9 +279,29 @@ type WitnessFloorConcurrencyPolicy { running: RunningSupersessionPolicy } +// THE RUNNING AXIS IS DERIVED FROM THE PERMIT SCOPE, not authored beside it. +// +// gunbc#9789 declared NeverSupersedeRunning and a DESIGN 4b(3) drop whose dissolve-on is a +// capability: no client of the required floor holds a host-persistent cooperative permit. Written as +// a literal, that row survives its own reason -- the fleet retires the FIFO and CI goes on refusing +// to supersede, the drop stays standing, and nothing refuses because nothing joins the two facts. +// DESIGN section 4b(3) says a drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, so the trigger is +// the whole check; making it a function of gunbc.compile_permit_scope is what turns that sentence +// into something the compiler evaluates rather than something a reviewer remembers. +// +// Restoring supersession while a permit still outlives its borrower restores the leak, which is why +// this reads the scope rather than a date, a flag, or a hand-flipped row. +fn running_supersession_for_permit_scope(scope: CompilePermitScope) -> RunningSupersessionPolicy { + match scope { + HostPersistentPermitPool { fifo_path: _, daemon_service: _ } => NeverSupersedeRunning + InvocationLocalParallelism { jobs_per_slot: _ } => + SupersedeRunningForEvent { event: "pull_request" } + } +} + data witness_floor_concurrency_policy: WitnessFloorConcurrencyPolicy = WitnessFloorConcurrencyPolicy { pending: ReplaceExistingPending, - running: NeverSupersedeRunning + running: running_supersession_for_permit_scope(scope: fleet_compile_permit_scope) } data witness_floor_running_supersession_policy: RunningSupersessionPolicy = witness_floor_concurrency_policy.running diff --git a/dag/test/claim/run_disposition_witness_test.dag b/dag/test/claim/run_disposition_witness_test.dag index 712fbd2af94..47cab280f64 100644 --- a/dag/test/claim/run_disposition_witness_test.dag +++ b/dag/test/claim/run_disposition_witness_test.dag @@ -1,6 +1,7 @@ module test.claim.run_disposition_witness_test import std.types { Bool } +import std.measure { hardware_thread_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.github.actions_runs { WorkflowRunRecord, @@ -9,7 +10,14 @@ import extdeps.github.actions_runs { run_conclusion_wire, run_settled } +import gunbc.compile_permit_scope { + CompilePermitScope, + HostPersistentPermitPool, + InvocationLocalParallelism, + fleet_compile_permit_scope +} import gunbc.witness_floor_workflow { + running_supersession_for_permit_scope, WitnessFloorConcurrencyPolicy, PendingReplacementPolicy, ReplaceExistingPending, @@ -563,3 +571,44 @@ test fn w_the_running_axis_crosses_into_the_queue_max_vocabulary() -> Bool { } live_holds && retaining_holds && superseding_holds } + + +// ── The drop retires by construction, not by remembering ──────────────────────────────────────── + +// THE CONTAINMENT IS A FUNCTION OF ITS OWN REASON. gunbc#9789's declared DESIGN 4b(3) drop names a +// capability as its dissolve-on -- no client of the required floor holds a host-persistent +// cooperative permit. Authored as a literal, NeverSupersedeRunning would outlive that condition +// silently: the fleet retires the FIFO, the leak stops, and CI keeps paying the latency of not +// superseding because nothing joins the two facts. These two arms are that join executing. +test fn w_a_leaking_permit_scope_refuses_to_supersede_a_running_run() -> Bool { + match running_supersession_for_permit_scope( + scope: HostPersistentPermitPool { + fifo_path: "/var/lib/ctrl/jobserver/host.fifo", + daemon_service: "ctrl-jobserver.service" as NonEmptyStr, + }, + ) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} + +// AND THE CUTOVER RESTORES SUPERSESSION WITHOUT ANYONE EDITING THIS POLICY. This is the arm that +// makes the pair discriminating: a derivation that ignored its argument and answered +// NeverSupersedeRunning for everything would pass the witness above and fail here. +test fn w_a_non_leaking_permit_scope_restores_supersession() -> Bool { + match running_supersession_for_permit_scope( + scope: InvocationLocalParallelism { jobs_per_slot: hardware_thread_count(count: 8) }, + ) { + SupersedeRunningForEvent { event: e } => e == "pull_request" + NeverSupersedeRunning => false + } +} + +// THE LIVE ROW STILL PROJECTS WHAT CI ACTUALLY RUNS, so the derivation cannot quietly change the +// emitted workflow while the two arms above stay green on fixtures. +test fn w_the_live_policy_still_refuses_running_supersession() -> Bool { + match running_supersession_for_permit_scope(scope: fleet_compile_permit_scope) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index aa9374de5d0..0fb2b656578 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -12,6 +12,14 @@ import gunbc.runner_unit { } import gunbc.runner_host_deploy { srv1_runner_host_deploy } import gunbc.host_converge { gunbc_runner_jobserver_default_fifo } +import gunbc.compile_permit_scope { + CompilePermitScope, + HostPersistentPermitPool, + InvocationLocalParallelism, + fleet_compile_permit_scope, + permit_outlives_borrower +} +import std.measure { hardware_thread_count } import gunbc.runner_unit_file { RunnerUnitFileRendered, RunnerUnitFileRefused, @@ -40,7 +48,7 @@ fn rendered_text(intent: RunnerUnitLifecycleIntent) -> String { rendering: runner_unit_file( deploy: srv1_runner_host_deploy, spec: srv1_spec(), - jobserver_fifo: gunbc_runner_jobserver_default_fifo, + permit_scope: fleet_compile_permit_scope, intent: intent, ), ) { @@ -178,7 +186,7 @@ fn refusal_reason(spec: RunnerSpec) -> String { match gunbc_runner_unit_file( deploy: srv1_runner_host_deploy, spec: spec, - jobserver_fifo: gunbc_runner_jobserver_default_fifo, + permit_scope: fleet_compile_permit_scope, ) { RunnerUnitFileRefused { reason: r } => r as String RunnerUnitFileRendered { file: _ } => "" @@ -197,3 +205,51 @@ test fn an_unresolved_runs_on_expression_refuses_as_unknown_not_as_absent() -> B && string_contains(s: reason, pattern: "matrix.runner") && reason != refusal_reason(spec: HostedRunner { label: UbuntuLatest }) } + + +// ── The permit scope, which is the fact both the unit and the required floor now read ─────────── + +// THE CUTOVER ARM RENDERS A DIFFERENT UNIT, and this is the discriminating red for the whole +// construction: if runner_unit_jobserver_environment ignored its scope and kept emitting the FIFO +// pair, every witness above would stay green because they all render the live arm. +fn invocation_local_text() -> String { + match runner_unit_text( + rendering: runner_unit_file( + deploy: srv1_runner_host_deploy, + spec: srv1_spec(), + permit_scope: InvocationLocalParallelism { jobs_per_slot: hardware_thread_count(count: 8) }, + intent: gunbc_runner_lifecycle_intent, + ), + ) { + RunnerUnitText { text: t } => t + RunnerUnitTextRefused { reason: _ } => "" + } +} + +test fn w_the_live_scope_lets_a_permit_outlive_its_borrower() -> Bool { + permit_outlives_borrower(scope: fleet_compile_permit_scope) == true +} + +test fn w_invocation_local_parallelism_cannot_leak_a_permit() -> Bool { + permit_outlives_borrower( + scope: InvocationLocalParallelism { jobs_per_slot: hardware_thread_count(count: 8) }, + ) == false +} + +// THE MAKEFLAGS CLAUSE IS GONE UNDER THE CUTOVER ARM, not merely repointed. Handing cargo an auth +// clause for a FIFO nobody serves is the silent-misconfig boundary extdeps.jobserver warns about: +// cargo does not refuse an unrecognised clause, it builds unbounded. +test fn w_the_cutover_arm_advertises_no_shared_pool() -> Bool { + let text = invocation_local_text() + !string_contains(s: text, pattern: "MAKEFLAGS") + && !string_contains(s: text, pattern: "CTRL_JOBSERVER_FIFO") + && string_contains(s: text, pattern: "\nEnvironment=CARGO_BUILD_JOBS=8\n") +} + +// AND THE ORDERING DEPENDENCY LEAVES WITH IT. A unit ordering itself After a service the cutover +// deleted is a fresh failure introduced by the fix, so the pair departs with the environment that +// needed it -- while the live arm above still asserts both lines are present. +test fn w_the_cutover_arm_drops_the_daemon_ordering() -> Bool { + let text = invocation_local_text() + !string_contains(s: text, pattern: "ctrl-jobserver.service") +} From 1e635c735e401dbf640dc48ab605c75ea9017613 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 03:32:42 +0000 Subject: [PATCH 02/15] Bind the containment to its own dissolve-on: derive both consumers from one permit-scope row gunbc#9789 stopped the cause of the jobserver permit leak by declaring NeverSupersedeRunning, and declared a DESIGN 4b(3) drop whose dissolve-on names a CAPABILITY: no client of the required floor holds a host-persistent cooperative permit -- either the ctrl host FIFO is gone and compile parallelism is invocation-local to cargo, or the pool is server-owned with admission that survives client death. That capability was a sentence in an annotation and the policy was an authored literal, so the containment could outlive its own reason: the fleet retires the FIFO, the leak stops, and CI goes on refusing to supersede because nothing joins the two facts. DESIGN 4b(3) says a drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, which makes the trigger the whole check -- and a check nothing evaluates is diligence, not a check. gunbc.compile_permit_scope declares CompilePermitScope with the two arms the trigger names as sufficient, permit_outlives_borrower as the decidable question it asks, and one row for what the fleet runs today. Both consumers derive from that row: the runner unit's environment and its After/Wants on ctrl-jobserver.service, and the required floor's running supersession axis. The ordering dependency departs WITH the environment that needed it, because a unit ordering itself After a service the cutover deleted is a fresh failure introduced by the fix. No arm for a server-owned pool: an arm with no realization is vocabulary invented ahead of its consumer. It belongs here the day someone builds one. Nothing actuates. fleet_compile_permit_scope still carries HostPersistentPermitPool, so the emitted workflow and the rendered unit are unchanged; flipping the row is the cutover and is an operator act. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/runner/runner_unit_file.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/runner/runner_unit_file.dag b/dag/gunbc/runner/runner_unit_file.dag index d5e43e03676..b6ab1aeda41 100644 --- a/dag/gunbc/runner/runner_unit_file.dag +++ b/dag/gunbc/runner/runner_unit_file.dag @@ -1,6 +1,6 @@ module gunbc.runner_unit_file -import std.types { String, NonEmptyStr, List, Bool, Int } +import std.types { String, NonEmptyStr, List, Bool } import std.measure { hardware_thread_count_value } import std.disposition { Disposition, SingleAuthority } import extdeps.github.actions { RunnerSpec, SelfHosted, HostedRunner, RunsOnExpression } @@ -192,7 +192,7 @@ fn runner_unit_jobserver_environment(scope: CompilePermitScope) -> List Date: Wed, 2 Sep 2026 03:43:23 +0000 Subject: [PATCH 03/15] Policy reads an OBSERVED fleet standing, not a desired realization row Side-chat review of the first draft found a fail-open I authored, and it is the kind DESIGN section 5 names rather than a rough edge: a generated artifact can make a rendered unit and a rendered workflow agree, but it cannot make host deployment and GitHub workflow activation atomic. Deriving the running axis straight from the desired realization row would have restored cancellation the moment the workflow reached main, while every host that had not yet received and restarted onto the new unit went on losing a permit per kill. My commit message claimed flipping one row moves the unit and retires the containment together; operationally that was not true. Three layers now, because they are three facts. CompileParallelismRealization is what a host runs. BorrowerDeathCapacityDisposition is what that implies for capacity under kill, and it is what business policy is allowed to see -- a workflow that matched realization variants would have to learn FIFO paths and systemd service names, and would need a new business branch per realization. HostCompileCancellationStanding and its fleet fold are what has been OBSERVED, with the safe arm carrying its readback rather than asserting itself. The fleet standing today is NotSafe over an empty roster, so the policy stays NeverSupersedeRunning BY REFUSAL. Unobserved is on the refusing side, one unsafe or unread host holds the containment, and a safe readback carrying a losing disposition joins the unsafe side rather than being believed. CapacityPreservedByServerReclamation exists with no concrete realization, reversing my earlier call. It is one of the two arms the dissolve-on names as sufficient and it has an immediate consumer in the policy fold, so omitting it narrowed the trigger to one arm -- the 4b(3) failure where a trigger naming less than the capability is satisfied while the capability stays dead. What stays absent is a concrete server realization with guessed fields. Renamed off HostPersistentPermitPool: persistence is not the defect, since a server-owned pool may be host-persistent and still reclaim safely. The unsafe arm names what is load-bearing -- borrower-held, cooperative, unreclaimed. The unit witnesses now render from a fixture realization carrying /fixture/other.fifo and fixture-other.service rather than the production constants, because the old fixture used exactly the values the renderer previously hardcoded: an implementation ignoring the arm's payload passed every witness. Both arms also assert their exact unit-section directive sequence, which substring witnesses could not see after the list was restructured. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 188 ++++++++++++++---- dag/gunbc/runner/runner_unit_file.dag | 29 ++- dag/gunbc/witness/witness_floor_workflow.dag | 45 +++-- .../claim/run_disposition_witness_test.dag | 139 ++++++++++--- .../runner/runner_unit_file_witness_test.dag | 99 ++++++--- 5 files changed, 371 insertions(+), 129 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index 7f8323b99ea..ea4a21f5c57 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -1,49 +1,159 @@ module gunbc.compile_permit_scope -import std.types { String, NonEmptyStr, Bool } +import std.types { String, NonEmptyStr, List, Bool } import std.measure { HardwareThreadCount } -import gunbc.host_converge { gunbc_runner_jobserver_default_fifo, gunbc_runner_jobserver_service } -// WHETHER A COMPILE PERMIT OUTLIVES THE PROCESS THAT BORROWED IT. That single fact is what makes -// killing a running build either cheap or permanently expensive, and until now it was not written -// down anywhere -- it was implied by the runner unit always rendering a shared FIFO, which made the -// alternative unrepresentable rather than merely unchosen. +// WHAT A BORROWER'S DEATH DOES TO FUTURE COMPILE CAPACITY. That is the fact gunbc#9789's declared +// DESIGN 4b(3) drop turns on, and until now it existed only as a sentence in an annotation while the +// policy it governs was an authored literal -- so the containment could outlive its own reason. // -// The fleet's builds are bounded by a host-persistent GNU jobserver whose permits are returned -// COOPERATIVELY. A SIGKILLed cargo returns nothing, so every permit that process held is lost for -// the lifetime of the daemon; there is no reaper, and a host at zero permits still accepts jobs, -// which is why the symptom is a slow queue rather than a failure. gunbc#9789 contained the CAUSE by -// declaring NeverSupersedeRunning, and declared a DESIGN 4b(3) drop whose dissolve-on is this -// capability: no client of the required floor holds a host-persistent cooperative permit -- either -// the host FIFO is gone and compile parallelism is invocation-local to cargo, or the pool is -// server-owned with admission that survives client death. +// The fleet's builds are bounded by a GNU jobserver whose permits are returned COOPERATIVELY. A +// SIGKILLed cargo returns nothing and no owner reclaims it, so the permit is not so much outliving +// its borrower as being ABANDONED: capacity is lost for the daemon's lifetime, there is no reaper, +// and a host at zero permits still accepts jobs. That is why the symptom is a slow queue and not a +// failure, and why the drop was declared rather than the leak simply fixed. // -// This module makes that capability a MODELLED FACT rather than a sentence in an annotation, so the -// containment retires by construction when the fleet changes rather than by someone remembering the -// row exists. The two arms below are the two the trigger names as sufficient; a third arm belongs -// here the day someone builds a server-owned pool, and not before -- an arm with no realization is -// vocabulary invented ahead of its consumer. -type CompilePermitScope - = HostPersistentPermitPool { fifo_path: String, daemon_service: NonEmptyStr } - | InvocationLocalParallelism { jobs_per_slot: HardwareThreadCount } - -// THE DECIDABLE QUESTION THE DISSOLVE-ON ASKS, answered by construction rather than by inspection. -// A borrower that cannot outlive its own permit cannot leak one, so the invalid state has no -// constructor under the second arm -- DESIGN 4b rung 4 for this class, reached by deleting the -// shared resource rather than by watching it. -fn permit_outlives_borrower(scope: CompilePermitScope) -> Bool { - match scope { - HostPersistentPermitPool { fifo_path: _, daemon_service: _ } => true - InvocationLocalParallelism { jobs_per_slot: _ } => false +// THREE LAYERS, BECAUSE THEY ARE THREE FACTS. A concrete realization is what a host runs; a +// disposition is what that realization implies for capacity under kill; a standing is what has been +// OBSERVED to be true of the running fleet. Collapsing the first into the third is what lets a +// desired-state row authorize a policy the hosts have not yet earned. +type CompileParallelismRealization + = BorrowerHeldCooperativeHostFifo { fifo_path: String, daemon_service: NonEmptyStr } + | InvocationLocalCargo { jobs_per_slot: HardwareThreadCount } + +// THE SEMANTIC OUTCOME, WHICH IS WHAT POLICY IS ALLOWED TO SEE. Business policy that matched +// realization variants would have to learn FIFO paths and systemd service names, and would need a +// new business branch every time a realization appeared -- the layer inversion DESIGN section 3 +// names. It reads this instead. +// +// CapacityPreservedByServerReclamation HAS NO CONCRETE REALIZATION TODAY, and it belongs here +// anyway: it is one of the two arms the controlling dissolve-on names as SUFFICIENT, it has an +// immediate consumer in the policy fold below, and it is fixture-authorable. Omitting it would +// narrow the trigger to one of its two arms -- the failure DESIGN 4b(3) warns about, where a trigger +// naming less than the capability is satisfied while the capability stays dead. What would be +// vocabulary ahead of its consumer is a concrete server realization with guessed fields, and that is +// deliberately absent until someone builds one. +type BorrowerDeathCapacityDisposition + = CapacityLostUntilPoolRestart + | CapacityPreservedByInvocationLifetime + | CapacityPreservedByServerReclamation + +// ONE DECISION PROCEDURE OVER THIS FACT, not two. An earlier draft declared a Boolean +// `permit_outlives_borrower` as "the decidable question" and then had the policy fold independently +// re-match the same realization type -- two procedures over one fact, which is what DESIGN section 2 +// removes. A Boolean was also the wrong shape: unsafe, safe-by-local-lifetime and +// safe-by-server-reclamation are materially different states, and a fourth -- unobserved -- is not a +// property of the realization at all but of our knowledge of the fleet, which is why it lives on the +// standing below rather than here. +fn borrower_death_capacity_disposition( + realization: CompileParallelismRealization, +) -> BorrowerDeathCapacityDisposition { + match realization { + BorrowerHeldCooperativeHostFifo { fifo_path: _, daemon_service: _ } => CapacityLostUntilPoolRestart + InvocationLocalCargo { jobs_per_slot: _ } => CapacityPreservedByInvocationLifetime } } -// WHAT THE FLEET RUNS TODAY. Flipping this row is the cutover, and because both the runner unit's -// environment and the required floor's supersession policy are DERIVED from it, the flip cannot -// move one without the other -- which is the disagreement DESIGN section 3 forbids and the specific -// way this containment could have gone stale: the fleet retires the FIFO, and CI keeps refusing to -// supersede for a reason that stopped being true. -data fleet_compile_permit_scope: CompilePermitScope = HostPersistentPermitPool { - fifo_path: gunbc_runner_jobserver_default_fifo, - daemon_service: gunbc_runner_jobserver_service as NonEmptyStr, +fn disposition_preserves_capacity(disposition: BorrowerDeathCapacityDisposition) -> Bool { + match disposition { + CapacityLostUntilPoolRestart => false + CapacityPreservedByInvocationLifetime => true + CapacityPreservedByServerReclamation => true + } } + +// WHAT A HOST HAS BEEN OBSERVED TO BE RUNNING, which is not what a row desires it to run. +// +// This is the boundary the first draft of this module got wrong, and the error was a fail-open of +// exactly the kind DESIGN section 5 forbids. Deriving the workflow policy straight from a desired +// realization row would restore cancellation the moment the workflow change reached main, whether or +// not any host had received and restarted onto the new unit -- so between merge and convergence, CI +// would supersede running builds on hosts still leaking a permit for every kill. A generated +// artifact can make a rendered unit and a rendered workflow agree; it cannot make host deployment +// and GitHub workflow activation atomic. +// +// So the safe arm carries its READBACK rather than asserting itself: what the active unit says, not +// what the model wishes it said. +type HostCompileCancellationStanding + = HostCancellationSafe { + host: NonEmptyStr, + disposition: BorrowerDeathCapacityDisposition, + active_unit_readback: NonEmptyStr, + } + | HostCancellationUnsafe { host: NonEmptyStr, cause: NonEmptyStr } + | HostCancellationUnobserved { host: NonEmptyStr, cause: NonEmptyStr } + +type FleetCompileCancellationStanding + = FleetCancellationSafe { hosts: List } + | FleetCancellationNotSafe { unsafe_hosts: List, unobserved_hosts: List } + +type FleetCancellationFoldAcc { + unsafe_hosts: List + unobserved_hosts: List + safe_hosts: List +} + +// ONE UNSAFE, MIXED OR UNREAD HOST KEEPS THE CONTAINMENT IN FORCE, and an EMPTY observation set is +// not safe either -- it is the empty-observation narrowing this repository has a named failure mode +// for. A fleet nobody has looked at is unobserved, and unobserved is on the refusing side. +// +// The caller supplies the eligible-host denominator, so a host that satisfies the workflow's runner +// selector and produced no observation arrives here as HostCancellationUnobserved rather than being +// silently absent from the fold. A fold that ranged only over the observations it happened to +// receive would answer SAFE for a fleet it had never asked about. +fn fleet_cancellation_standing( + observations: List, +) -> FleetCompileCancellationStanding { + let acc = fold( + observations, + init: FleetCancellationFoldAcc { unsafe_hosts: [], unobserved_hosts: [], safe_hosts: [] }, + f: (a, o) => match o { + HostCancellationSafe { host: h, disposition: d, active_unit_readback: _ } => + match disposition_preserves_capacity(disposition: d) { + true => FleetCancellationFoldAcc { + unsafe_hosts: a.unsafe_hosts, + unobserved_hosts: a.unobserved_hosts, + safe_hosts: concat(a.safe_hosts, [h]), + } + // A readback that says SAFE while carrying a disposition that loses capacity is a + // contradiction in the observation, not a safe host. It joins the unsafe side. + false => FleetCancellationFoldAcc { + unsafe_hosts: concat(a.unsafe_hosts, [h]), + unobserved_hosts: a.unobserved_hosts, + safe_hosts: a.safe_hosts, + } + } + HostCancellationUnsafe { host: h, cause: _ } => FleetCancellationFoldAcc { + unsafe_hosts: concat(a.unsafe_hosts, [h]), + unobserved_hosts: a.unobserved_hosts, + safe_hosts: a.safe_hosts, + } + HostCancellationUnobserved { host: h, cause: _ } => FleetCancellationFoldAcc { + unsafe_hosts: a.unsafe_hosts, + unobserved_hosts: concat(a.unobserved_hosts, [h]), + safe_hosts: a.safe_hosts, + } + }, + ) + match acc.safe_hosts { + [] => FleetCancellationNotSafe { + unsafe_hosts: acc.unsafe_hosts, + unobserved_hosts: acc.unobserved_hosts, + } + _ => match concat(acc.unsafe_hosts, acc.unobserved_hosts) { + [] => FleetCancellationSafe { hosts: acc.safe_hosts } + _ => FleetCancellationNotSafe { + unsafe_hosts: acc.unsafe_hosts, + unobserved_hosts: acc.unobserved_hosts, + } + } + } +} + +// THE FLEET AS OBSERVED TODAY: nothing. No host readback exists yet, so the standing is NotSafe with +// an empty roster on both sides, and the policy below stays NeverSupersedeRunning BY REFUSAL rather +// than by a literal someone has to remember to keep. Publishing real observations is what moves it, +// and that is the second stage of the cutover -- deploy and restart the safe realization on every +// eligible host, read the active units back, bind the receipts, and only then does the policy move. +data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = + fleet_cancellation_standing(observations: []) diff --git a/dag/gunbc/runner/runner_unit_file.dag b/dag/gunbc/runner/runner_unit_file.dag index b6ab1aeda41..f576534b9a8 100644 --- a/dag/gunbc/runner/runner_unit_file.dag +++ b/dag/gunbc/runner/runner_unit_file.dag @@ -8,10 +8,9 @@ import extdeps.github.actions_runner { actions_runner_base_dir } import extdeps.languages.json.emit { json_string, json_array, serialize_json } import extdeps.jobserver { jobserver_makeflags_fifo_auth } import gunbc.compile_permit_scope { - CompilePermitScope, - HostPersistentPermitPool, - InvocationLocalParallelism, - fleet_compile_permit_scope + CompileParallelismRealization, + BorrowerHeldCooperativeHostFifo, + InvocationLocalCargo } import extdeps.systemd.unit_file { SystemdUnitFile, @@ -174,9 +173,9 @@ fn runner_unit_app_environment(app: GithubAppRunnerConfig) -> List List { +fn runner_unit_jobserver_environment(scope: CompileParallelismRealization) -> List { match scope { - HostPersistentPermitPool { fifo_path: p, daemon_service: _ } => + BorrowerHeldCooperativeHostFifo { fifo_path: p, daemon_service: _ } => [ runner_unit_environment(name: "CTRL_JOBSERVER_FIFO", value: p), runner_unit_environment( @@ -188,7 +187,7 @@ fn runner_unit_jobserver_environment(scope: CompilePermitScope) -> List + InvocationLocalCargo { jobs_per_slot: j } => [ runner_unit_environment( name: "CARGO_BUILD_JOBS", @@ -208,17 +207,17 @@ fn runner_unit_jobserver_environment(scope: CompilePermitScope) -> List List { +fn runner_unit_jobserver_after(scope: CompileParallelismRealization) -> List { match scope { - HostPersistentPermitPool { fifo_path: _, daemon_service: svc } => [After { target: svc }] - InvocationLocalParallelism { jobs_per_slot: _ } => [] + BorrowerHeldCooperativeHostFifo { fifo_path: _, daemon_service: svc } => [After { target: svc }] + InvocationLocalCargo { jobs_per_slot: _ } => [] } } -fn runner_unit_jobserver_wants(scope: CompilePermitScope) -> List { +fn runner_unit_jobserver_wants(scope: CompileParallelismRealization) -> List { match scope { - HostPersistentPermitPool { fifo_path: _, daemon_service: svc } => [Wants { target: svc }] - InvocationLocalParallelism { jobs_per_slot: _ } => [] + BorrowerHeldCooperativeHostFifo { fifo_path: _, daemon_service: svc } => [Wants { target: svc }] + InvocationLocalCargo { jobs_per_slot: _ } => [] } } @@ -243,7 +242,7 @@ type RunnerUnitFileRendering fn runner_unit_file( deploy: RunnerHostDeploy, spec: RunnerSpec, - permit_scope: CompilePermitScope, + permit_scope: CompileParallelismRealization, intent: RunnerUnitLifecycleIntent, ) -> RunnerUnitFileRendering { match runner_unit_labels_json(spec: spec) { @@ -325,7 +324,7 @@ fn runner_unit_file( fn gunbc_runner_unit_file( deploy: RunnerHostDeploy, spec: RunnerSpec, - permit_scope: CompilePermitScope, + permit_scope: CompileParallelismRealization, ) -> RunnerUnitFileRendering { runner_unit_file( deploy: deploy, diff --git a/dag/gunbc/witness/witness_floor_workflow.dag b/dag/gunbc/witness/witness_floor_workflow.dag index 2159aa6ecbb..7fb298dae91 100644 --- a/dag/gunbc/witness/witness_floor_workflow.dag +++ b/dag/gunbc/witness/witness_floor_workflow.dag @@ -31,10 +31,10 @@ import gunbc.toolchain_workflow_steps { toolchain_pin_rustup_default_step, } import gunbc.compile_permit_scope { - CompilePermitScope, - HostPersistentPermitPool, - InvocationLocalParallelism, - fleet_compile_permit_scope + FleetCompileCancellationStanding, + FleetCancellationSafe, + FleetCancellationNotSafe, + fleet_compile_cancellation_standing } import extdeps.github.actions { Workflow, Job, Step, RunStep, UsesStep, @@ -279,29 +279,34 @@ type WitnessFloorConcurrencyPolicy { running: RunningSupersessionPolicy } -// THE RUNNING AXIS IS DERIVED FROM THE PERMIT SCOPE, not authored beside it. +// THE RUNNING AXIS IS DERIVED FROM THE OBSERVED FLEET STANDING, not authored beside it and not read +// off a desired-state row. // // gunbc#9789 declared NeverSupersedeRunning and a DESIGN 4b(3) drop whose dissolve-on is a -// capability: no client of the required floor holds a host-persistent cooperative permit. Written as -// a literal, that row survives its own reason -- the fleet retires the FIFO and CI goes on refusing -// to supersede, the drop stays standing, and nothing refuses because nothing joins the two facts. -// DESIGN section 4b(3) says a drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, so the trigger is -// the whole check; making it a function of gunbc.compile_permit_scope is what turns that sentence -// into something the compiler evaluates rather than something a reviewer remembers. -// -// Restoring supersession while a permit still outlives its borrower restores the leak, which is why -// this reads the scope rather than a date, a flag, or a hand-flipped row. -fn running_supersession_for_permit_scope(scope: CompilePermitScope) -> RunningSupersessionPolicy { - match scope { - HostPersistentPermitPool { fifo_path: _, daemon_service: _ } => NeverSupersedeRunning - InvocationLocalParallelism { jobs_per_slot: _ } => - SupersedeRunningForEvent { event: "pull_request" } +// capability: no client of the required floor holds a permit whose abandonment costs future compile +// capacity. Written as a literal, that row survives its own reason -- the fleet stops leaking and CI +// goes on refusing to supersede, the drop stays standing, and nothing refuses because nothing joins +// the two facts. Section 4b(3) says a drop is retired BY ITS TRIGGER AND BY NOTHING ELSE, so the +// trigger is the whole check, and a check nothing evaluates is diligence rather than a check. +// +// IT READS THE STANDING AND NOT THE REALIZATION, for a reason that is a safety property rather than +// a taste: a desired realization row and the live hosts are two independently actuated systems, and +// a generated artifact cannot make them transition together. Deriving from the row would restore +// cancellation the moment this workflow reached main, while hosts that had not yet restarted onto +// the new unit went on losing a permit per kill. The unobserved fleet is on the refusing side, so +// that interval is unwritable rather than merely unlikely. +fn running_supersession_for_fleet_standing( + standing: FleetCompileCancellationStanding, +) -> RunningSupersessionPolicy { + match standing { + FleetCancellationNotSafe { unsafe_hosts: _, unobserved_hosts: _ } => NeverSupersedeRunning + FleetCancellationSafe { hosts: _ } => SupersedeRunningForEvent { event: "pull_request" } } } data witness_floor_concurrency_policy: WitnessFloorConcurrencyPolicy = WitnessFloorConcurrencyPolicy { pending: ReplaceExistingPending, - running: running_supersession_for_permit_scope(scope: fleet_compile_permit_scope) + running: running_supersession_for_fleet_standing(standing: fleet_compile_cancellation_standing) } data witness_floor_running_supersession_policy: RunningSupersessionPolicy = witness_floor_concurrency_policy.running diff --git a/dag/test/claim/run_disposition_witness_test.dag b/dag/test/claim/run_disposition_witness_test.dag index 47cab280f64..9f6428553b1 100644 --- a/dag/test/claim/run_disposition_witness_test.dag +++ b/dag/test/claim/run_disposition_witness_test.dag @@ -1,7 +1,6 @@ module test.claim.run_disposition_witness_test -import std.types { Bool } -import std.measure { hardware_thread_count } +import std.types { Bool, String, NonEmptyStr } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.github.actions_runs { WorkflowRunRecord, @@ -11,13 +10,21 @@ import extdeps.github.actions_runs { run_settled } import gunbc.compile_permit_scope { - CompilePermitScope, - HostPersistentPermitPool, - InvocationLocalParallelism, - fleet_compile_permit_scope + FleetCompileCancellationStanding, + FleetCancellationSafe, + FleetCancellationNotSafe, + HostCompileCancellationStanding, + HostCancellationSafe, + HostCancellationUnsafe, + HostCancellationUnobserved, + CapacityPreservedByInvocationLifetime, + CapacityPreservedByServerReclamation, + CapacityLostUntilPoolRestart, + fleet_cancellation_standing, + fleet_compile_cancellation_standing } import gunbc.witness_floor_workflow { - running_supersession_for_permit_scope, + running_supersession_for_fleet_standing, WitnessFloorConcurrencyPolicy, PendingReplacementPolicy, ReplaceExistingPending, @@ -573,41 +580,117 @@ test fn w_the_running_axis_crosses_into_the_queue_max_vocabulary() -> Bool { } -// ── The drop retires by construction, not by remembering ──────────────────────────────────────── +// ── The drop retires by construction, and only on observed convergence ───────────────────────── -// THE CONTAINMENT IS A FUNCTION OF ITS OWN REASON. gunbc#9789's declared DESIGN 4b(3) drop names a -// capability as its dissolve-on -- no client of the required floor holds a host-persistent -// cooperative permit. Authored as a literal, NeverSupersedeRunning would outlive that condition -// silently: the fleet retires the FIFO, the leak stops, and CI keeps paying the latency of not -// superseding because nothing joins the two facts. These two arms are that join executing. -test fn w_a_leaking_permit_scope_refuses_to_supersede_a_running_run() -> Bool { - match running_supersession_for_permit_scope( - scope: HostPersistentPermitPool { - fifo_path: "/var/lib/ctrl/jobserver/host.fifo", - daemon_service: "ctrl-jobserver.service" as NonEmptyStr, - }, +fn safe_host(name: String) -> HostCompileCancellationStanding { + HostCancellationSafe { + host: name as NonEmptyStr, + disposition: CapacityPreservedByInvocationLifetime, + active_unit_readback: "Environment=CARGO_BUILD_JOBS=8" as NonEmptyStr, + } +} + +// THE CONTAINMENT IS A FUNCTION OF ITS OWN REASON, AND OF WHAT THE HOSTS ACTUALLY RUN. +// +// Authored as a literal, NeverSupersedeRunning outlives the condition that required it. Derived from +// a DESIRED realization row it does something worse: it restores cancellation the moment the +// workflow reaches main, while hosts that have not restarted onto the new unit keep losing a permit +// per kill. So the policy reads an OBSERVED fleet standing, and the arms below are that join. +test fn w_an_unobserved_fleet_refuses_to_supersede_a_running_run() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing(observations: []), ) { NeverSupersedeRunning => true SupersedeRunningForEvent { event: _ } => false } } -// AND THE CUTOVER RESTORES SUPERSESSION WITHOUT ANYONE EDITING THIS POLICY. This is the arm that +// ONE UNREAD HOST IS ENOUGH. A fold that answered on the hosts it happened to receive would report +// the fleet safe while an eligible host nobody asked about went on leaking. +test fn w_a_single_unobserved_host_holds_the_containment() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing(observations: [ + safe_host(name: "srv1"), + safe_host(name: "srv2"), + HostCancellationUnobserved { + host: "srv3" as NonEmptyStr, + cause: "no active unit readback" as NonEmptyStr, + }, + ]), + ) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} + +test fn w_a_single_unsafe_host_holds_the_containment() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing(observations: [ + safe_host(name: "srv1"), + HostCancellationUnsafe { + host: "srv4" as NonEmptyStr, + cause: "active unit still names the host FIFO" as NonEmptyStr, + }, + ]), + ) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} + +// A READBACK THAT CLAIMS SAFE WHILE CARRYING A LOSING DISPOSITION IS A CONTRADICTION, and joins the +// unsafe side rather than being believed. Without this arm the safe constructor is self-certifying. +test fn w_a_safe_readback_carrying_a_losing_disposition_is_not_safe() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing(observations: [ + HostCancellationSafe { + host: "srv1" as NonEmptyStr, + disposition: CapacityLostUntilPoolRestart, + active_unit_readback: "Environment=MAKEFLAGS=--jobserver-auth=fifo:/var/lib/ctrl/jobserver/host.fifo" as NonEmptyStr, + }, + ]), + ) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} + +// AND A FULLY OBSERVED SAFE FLEET RESTORES SUPERSESSION WITH NO EDIT TO THIS POLICY. This is what // makes the pair discriminating: a derivation that ignored its argument and answered -// NeverSupersedeRunning for everything would pass the witness above and fail here. -test fn w_a_non_leaking_permit_scope_restores_supersession() -> Bool { - match running_supersession_for_permit_scope( - scope: InvocationLocalParallelism { jobs_per_slot: hardware_thread_count(count: 8) }, +// NeverSupersedeRunning for everything would pass every witness above and fail here. +test fn w_a_fully_observed_safe_fleet_restores_supersession() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing(observations: [ + safe_host(name: "srv1"), + safe_host(name: "srv2"), + ]), + ) { + SupersedeRunningForEvent { event: e } => e == "pull_request" + NeverSupersedeRunning => false + } +} + +// SERVER RECLAMATION IS THE OTHER SUFFICIENT ARM the dissolve-on names, and the policy already knows +// what it means -- so the day a server-owned pool exists it needs no new business branch here. +test fn w_server_reclamation_is_a_sufficient_arm_for_the_policy() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing(observations: [ + HostCancellationSafe { + host: "srv1" as NonEmptyStr, + disposition: CapacityPreservedByServerReclamation, + active_unit_readback: "server-owned pool with death reclamation" as NonEmptyStr, + }, + ]), ) { SupersedeRunningForEvent { event: e } => e == "pull_request" NeverSupersedeRunning => false } } -// THE LIVE ROW STILL PROJECTS WHAT CI ACTUALLY RUNS, so the derivation cannot quietly change the -// emitted workflow while the two arms above stay green on fixtures. -test fn w_the_live_policy_still_refuses_running_supersession() -> Bool { - match running_supersession_for_permit_scope(scope: fleet_compile_permit_scope) { +// THE LIVE ROW STILL PROJECTS WHAT CI ACTUALLY RUNS, so the fixtures above cannot go green while the +// emitted workflow quietly moves. +test fn w_the_live_fleet_standing_still_refuses_running_supersession() -> Bool { + match running_supersession_for_fleet_standing(standing: fleet_compile_cancellation_standing) { NeverSupersedeRunning => true SupersedeRunningForEvent { event: _ } => false } diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index 0fb2b656578..d11fa5ba94f 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -11,13 +11,15 @@ import gunbc.runner_unit { lifecycle_intent_cannot_orphan, } import gunbc.runner_host_deploy { srv1_runner_host_deploy } -import gunbc.host_converge { gunbc_runner_jobserver_default_fifo } import gunbc.compile_permit_scope { - CompilePermitScope, - HostPersistentPermitPool, - InvocationLocalParallelism, - fleet_compile_permit_scope, - permit_outlives_borrower + CompileParallelismRealization, + BorrowerHeldCooperativeHostFifo, + InvocationLocalCargo, + BorrowerDeathCapacityDisposition, + CapacityLostUntilPoolRestart, + CapacityPreservedByInvocationLifetime, + CapacityPreservedByServerReclamation, + borrower_death_capacity_disposition } import std.measure { hardware_thread_count } import gunbc.runner_unit_file { @@ -48,7 +50,7 @@ fn rendered_text(intent: RunnerUnitLifecycleIntent) -> String { rendering: runner_unit_file( deploy: srv1_runner_host_deploy, spec: srv1_spec(), - permit_scope: fleet_compile_permit_scope, + permit_scope: live_realization(), intent: intent, ), ) { @@ -101,8 +103,8 @@ test fn the_rendered_intent_is_the_one_that_cannot_orphan() -> Bool { // fail against a FIFO nobody is serving. test fn the_jobserver_ordering_dependency_survives_the_redesign() -> Bool { let text = rendered_text(intent: gunbc_runner_lifecycle_intent) - string_contains(s: text, pattern: "\nAfter=ctrl-jobserver.service\n") - && string_contains(s: text, pattern: "\nWants=ctrl-jobserver.service\n") + string_contains(s: text, pattern: "\nAfter=fixture-other.service\n") + && string_contains(s: text, pattern: "\nWants=fixture-other.service\n") && string_contains(s: text, pattern: "\nAfter=network-online.target\n") } @@ -117,8 +119,8 @@ test fn the_start_rate_limiter_is_disabled_for_a_restart_per_job_unit() -> Bool // about again. test fn both_jobserver_lines_name_the_same_fifo() -> Bool { let text = rendered_text(intent: gunbc_runner_lifecycle_intent) - string_contains(s: text, pattern: "\nEnvironment=CTRL_JOBSERVER_FIFO=/var/lib/ctrl/jobserver/host.fifo\n") - && string_contains(s: text, pattern: "\nEnvironment=MAKEFLAGS=--jobserver-auth=fifo:/var/lib/ctrl/jobserver/host.fifo\n") + string_contains(s: text, pattern: "\nEnvironment=CTRL_JOBSERVER_FIFO=/fixture/other.fifo\n") + && string_contains(s: text, pattern: "\nEnvironment=MAKEFLAGS=--jobserver-auth=fifo:/fixture/other.fifo\n") } // THE per-slot TASK CEILING IS NOT HERE, AND ITS ABSENCE IS THE CLAIM. gunbc.host_converge converges @@ -186,7 +188,7 @@ fn refusal_reason(spec: RunnerSpec) -> String { match gunbc_runner_unit_file( deploy: srv1_runner_host_deploy, spec: spec, - permit_scope: fleet_compile_permit_scope, + permit_scope: live_realization(), ) { RunnerUnitFileRefused { reason: r } => r as String RunnerUnitFileRendered { file: _ } => "" @@ -207,17 +209,25 @@ test fn an_unresolved_runs_on_expression_refuses_as_unknown_not_as_absent() -> B } -// ── The permit scope, which is the fact both the unit and the required floor now read ─────────── +// ── The permit realization, and whether the render actually reads its payload ─────────────────── + +// THE LIVE-SHAPED FIXTURE CARRIES FIXTURE VALUES, NOT THE PRODUCTION CONSTANTS. An earlier draft +// passed the fleet row itself, whose FIFO path and service name are exactly what the renderer used +// to hardcode -- so a renderer that ignored its argument entirely would have passed every witness +// here. Distinct values are what make the field occupancy discriminating. +fn live_realization() -> CompileParallelismRealization { + BorrowerHeldCooperativeHostFifo { + fifo_path: "/fixture/other.fifo", + daemon_service: "fixture-other.service" as NonEmptyStr, + } +} -// THE CUTOVER ARM RENDERS A DIFFERENT UNIT, and this is the discriminating red for the whole -// construction: if runner_unit_jobserver_environment ignored its scope and kept emitting the FIFO -// pair, every witness above would stay green because they all render the live arm. fn invocation_local_text() -> String { match runner_unit_text( rendering: runner_unit_file( deploy: srv1_runner_host_deploy, spec: srv1_spec(), - permit_scope: InvocationLocalParallelism { jobs_per_slot: hardware_thread_count(count: 8) }, + permit_scope: InvocationLocalCargo { jobs_per_slot: hardware_thread_count(count: 8) }, intent: gunbc_runner_lifecycle_intent, ), ) { @@ -226,14 +236,51 @@ fn invocation_local_text() -> String { } } -test fn w_the_live_scope_lets_a_permit_outlive_its_borrower() -> Bool { - permit_outlives_borrower(scope: fleet_compile_permit_scope) == true +// EVERY FIELD OF THE ARM REACHES THE FOUR PLACES THAT NAME IT. Four separate assertions rather than +// one, because a renderer that dropped the daemon service from the ordering while keeping it in the +// environment would otherwise still pass. +test fn w_the_realization_payload_reaches_every_directive_that_names_it() -> Bool { + let text = rendered_text(intent: gunbc_runner_lifecycle_intent) + string_contains(s: text, pattern: "\nEnvironment=CTRL_JOBSERVER_FIFO=/fixture/other.fifo\n") + && string_contains(s: text, pattern: "\nEnvironment=MAKEFLAGS=--jobserver-auth=fifo:/fixture/other.fifo\n") + && string_contains(s: text, pattern: "\nAfter=fixture-other.service\n") + && string_contains(s: text, pattern: "\nWants=fixture-other.service\n") } -test fn w_invocation_local_parallelism_cannot_leak_a_permit() -> Bool { - permit_outlives_borrower( - scope: InvocationLocalParallelism { jobs_per_slot: hardware_thread_count(count: 8) }, - ) == false +// THE EXACT UNIT-SECTION SEQUENCE FOR BOTH ARMS, because the directive list was restructured to +// interleave the optional pair and substring witnesses cannot see order, duplication, or a stray +// blank line. This is the shape oracle the restructure owes. +test fn w_the_live_arm_unit_section_is_exactly_ordered() -> Bool { + let text = rendered_text(intent: gunbc_runner_lifecycle_intent) + string_contains( + s: text, + pattern: "\nAfter=network-online.target\nAfter=fixture-other.service\nWants=network-online.target\nWants=fixture-other.service\nStartLimitIntervalSec=0\n", + ) +} + +test fn w_the_cutover_arm_unit_section_is_exactly_ordered() -> Bool { + string_contains( + s: invocation_local_text(), + pattern: "\nAfter=network-online.target\nWants=network-online.target\nStartLimitIntervalSec=0\n", + ) +} + +test fn w_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies() -> Bool { + match borrower_death_capacity_disposition(realization: live_realization()) { + CapacityLostUntilPoolRestart => true + CapacityPreservedByInvocationLifetime => false + CapacityPreservedByServerReclamation => false + } +} + +test fn w_invocation_local_parallelism_preserves_capacity_by_lifetime() -> Bool { + match borrower_death_capacity_disposition( + realization: InvocationLocalCargo { jobs_per_slot: hardware_thread_count(count: 8) }, + ) { + CapacityPreservedByInvocationLifetime => true + CapacityLostUntilPoolRestart => false + CapacityPreservedByServerReclamation => false + } } // THE MAKEFLAGS CLAUSE IS GONE UNDER THE CUTOVER ARM, not merely repointed. Handing cargo an auth @@ -247,9 +294,7 @@ test fn w_the_cutover_arm_advertises_no_shared_pool() -> Bool { } // AND THE ORDERING DEPENDENCY LEAVES WITH IT. A unit ordering itself After a service the cutover -// deleted is a fresh failure introduced by the fix, so the pair departs with the environment that -// needed it -- while the live arm above still asserts both lines are present. +// deleted is a fresh failure introduced by the fix. test fn w_the_cutover_arm_drops_the_daemon_ordering() -> Bool { - let text = invocation_local_text() - !string_contains(s: text, pattern: "ctrl-jobserver.service") + !string_contains(s: invocation_local_text(), pattern: "fixture-other.service") } From 0eba901270615eccdd3c7632d96ddb85c881ff80 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 04:12:04 +0000 Subject: [PATCH 04/15] Parse fix: list_length instead of empty-list patterns The build lane refused with 'module index refused: 1 unparseable .dag source(s)'. The empty-list pattern I used to test the rosters -- [] => ... / _ => ... -- has no precedent anywhere in the corpus, which was the tell I should have read before pushing rather than after: a construct nothing else in 4471 modules uses is a construct the grammar probably does not have. list_length is what std.types already provides, and the conjunction is bound to a name before the match rather than matched as a parenthesised expression, which is likewise unprecedented here. The refusal shape is unchanged and still deliberate: SAFE requires a non-empty safe roster AND an empty blocking one, so an empty observation set stays on the refusing side. Testing only the blocking roster would report SAFE for silence, which is the empty-observation narrowing this repository has a named failure mode for. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index ea4a21f5c57..2f06594af10 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -1,6 +1,6 @@ module gunbc.compile_permit_scope -import std.types { String, NonEmptyStr, List, Bool } +import std.types { String, NonEmptyStr, List, Bool, list_length } import std.measure { HardwareThreadCount } // WHAT A BORROWER'S DEATH DOES TO FUTURE COMPILE CAPACITY. That is the fact gunbc#9789's declared @@ -135,18 +135,18 @@ fn fleet_cancellation_standing( } }, ) - match acc.safe_hosts { - [] => FleetCancellationNotSafe { + // SAFE REQUIRES BOTH a non-empty safe roster AND an empty not-safe one. The first conjunct is what + // keeps an empty observation set on the refusing side: a fleet nobody looked at has no unsafe and + // no unobserved host either, so testing only the second would report SAFE for silence. + let blocking = list_length(items: concat(acc.unsafe_hosts, acc.unobserved_hosts)) + let observed_safe = list_length(items: acc.safe_hosts) + let fleet_is_safe = (blocking == 0) && (observed_safe > 0) + match fleet_is_safe { + true => FleetCancellationSafe { hosts: acc.safe_hosts } + false => FleetCancellationNotSafe { unsafe_hosts: acc.unsafe_hosts, unobserved_hosts: acc.unobserved_hosts, } - _ => match concat(acc.unsafe_hosts, acc.unobserved_hosts) { - [] => FleetCancellationSafe { hosts: acc.safe_hosts } - _ => FleetCancellationNotSafe { - unsafe_hosts: acc.unsafe_hosts, - unobserved_hosts: acc.unobserved_hosts, - } - } } } From 3177b99a9816f17259ac3f4c45ad2850283bc957 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 04:31:46 +0000 Subject: [PATCH 05/15] Parse fix: the data initializer goes on the declaration's own line The real parse error was compile_permit_scope.dag:158:77 'expected expression, found Newline' -- a data declaration whose initializer I wrapped onto the following line. Every other diagnostic in that run was the cascade: forty 'source annotation names no subject' lines, which is what the annotation channel reports once the item after it fails to parse. I read the cascade first and guessed at the empty-list patterns; those were unprecedented and worth replacing anyway, but they were not the failure. Also takes review 58445's non-blocking point, which is right: fifo_path was String while its sibling daemon_service was NonEmptyStr, so an empty path would have rendered Environment=CTRL_JOBSERVER_FIFO= and --jobserver-auth=fifo: with nothing after the colon. cargo does not refuse an unrecognised auth clause, it builds unbounded -- the same silent boundary extdeps.jobserver already warns about, which is what makes the weaker type worth closing now rather than when a caller finally supplies one. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 5 ++--- dag/gunbc/runner/runner_unit_file.dag | 4 ++-- dag/test/claim/runner/runner_unit_file_witness_test.dag | 2 +- 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index 2f06594af10..c0b233b9a5d 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -18,7 +18,7 @@ import std.measure { HardwareThreadCount } // OBSERVED to be true of the running fleet. Collapsing the first into the third is what lets a // desired-state row authorize a policy the hosts have not yet earned. type CompileParallelismRealization - = BorrowerHeldCooperativeHostFifo { fifo_path: String, daemon_service: NonEmptyStr } + = BorrowerHeldCooperativeHostFifo { fifo_path: NonEmptyStr, daemon_service: NonEmptyStr } | InvocationLocalCargo { jobs_per_slot: HardwareThreadCount } // THE SEMANTIC OUTCOME, WHICH IS WHAT POLICY IS ALLOWED TO SEE. Business policy that matched @@ -155,5 +155,4 @@ fn fleet_cancellation_standing( // than by a literal someone has to remember to keep. Publishing real observations is what moves it, // and that is the second stage of the cutover -- deploy and restart the safe realization on every // eligible host, read the active units back, bind the receipts, and only then does the policy move. -data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = - fleet_cancellation_standing(observations: []) +data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_cancellation_standing(observations: []) diff --git a/dag/gunbc/runner/runner_unit_file.dag b/dag/gunbc/runner/runner_unit_file.dag index f576534b9a8..77e76d616ef 100644 --- a/dag/gunbc/runner/runner_unit_file.dag +++ b/dag/gunbc/runner/runner_unit_file.dag @@ -177,10 +177,10 @@ fn runner_unit_jobserver_environment(scope: CompileParallelismRealization) -> Li match scope { BorrowerHeldCooperativeHostFifo { fifo_path: p, daemon_service: _ } => [ - runner_unit_environment(name: "CTRL_JOBSERVER_FIFO", value: p), + runner_unit_environment(name: "CTRL_JOBSERVER_FIFO", value: p as String), runner_unit_environment( name: "MAKEFLAGS", - value: jobserver_makeflags_fifo_auth(fifo_path: p), + value: jobserver_makeflags_fifo_auth(fifo_path: p as String), ), ] // NO MAKEFLAGS, AND THAT ABSENCE IS THE POINT. Under invocation-local parallelism there is no diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index d11fa5ba94f..75224872f26 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -217,7 +217,7 @@ test fn an_unresolved_runs_on_expression_refuses_as_unknown_not_as_absent() -> B // here. Distinct values are what make the field occupancy discriminating. fn live_realization() -> CompileParallelismRealization { BorrowerHeldCooperativeHostFifo { - fifo_path: "/fixture/other.fifo", + fifo_path: "/fixture/other.fifo" as NonEmptyStr, daemon_service: "fixture-other.service" as NonEmptyStr, } } From 7168b005454d58f1debe6ee3014059e84399e750 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 04:59:15 +0000 Subject: [PATCH 06/15] Annotations belong at module-item grain, not inside a declaration body DESIGN section 4c states it plainly and it is in the design document loaded on every turn: the .dag realization admits only standalone leading // blocks attached to module-scope declarations, and body forms refuse until separately modeled. I put rationale inside match arms and a let sequence in two modules, so the parse refused nine times. The rationale is not deleted -- it is hoisted into the leading block of the declaration it was describing, which is where a reader looking for why the fold refuses an empty roster or why the cutover arm emits no MAKEFLAGS will now find it. That is the grain the annotation channel models, and the constraint is the reason section 4c gives: an annotation is captured authored-source data disjoint from semantic occurrence allocation, so admitting it at arbitrary depth is a separate modeling job nobody has done. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 14 +++++++++----- dag/gunbc/runner/runner_unit_file.dag | 9 +++++---- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index c0b233b9a5d..f22e4e72d3a 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -101,6 +101,15 @@ type FleetCancellationFoldAcc { // selector and produced no observation arrives here as HostCancellationUnobserved rather than being // silently absent from the fold. A fold that ranged only over the observations it happened to // receive would answer SAFE for a fleet it had never asked about. +// +// SAFE THEREFORE REQUIRES BOTH a non-empty safe roster and an empty blocking one. The first +// conjunct is what keeps an empty observation set on the refusing side: a fleet nobody looked at +// has no unsafe and no unobserved host either, so testing only the blocking roster would report +// SAFE for silence. +// +// And a HostCancellationSafe carrying a disposition that loses capacity is a contradiction in the +// observation rather than a safe host, so it joins the unsafe side -- without that arm the safe +// constructor would be self-certifying. fn fleet_cancellation_standing( observations: List, ) -> FleetCompileCancellationStanding { @@ -115,8 +124,6 @@ fn fleet_cancellation_standing( unobserved_hosts: a.unobserved_hosts, safe_hosts: concat(a.safe_hosts, [h]), } - // A readback that says SAFE while carrying a disposition that loses capacity is a - // contradiction in the observation, not a safe host. It joins the unsafe side. false => FleetCancellationFoldAcc { unsafe_hosts: concat(a.unsafe_hosts, [h]), unobserved_hosts: a.unobserved_hosts, @@ -135,9 +142,6 @@ fn fleet_cancellation_standing( } }, ) - // SAFE REQUIRES BOTH a non-empty safe roster AND an empty not-safe one. The first conjunct is what - // keeps an empty observation set on the refusing side: a fleet nobody looked at has no unsafe and - // no unobserved host either, so testing only the second would report SAFE for silence. let blocking = list_length(items: concat(acc.unsafe_hosts, acc.unobserved_hosts)) let observed_safe = list_length(items: acc.safe_hosts) let fleet_is_safe = (blocking == 0) && (observed_safe > 0) diff --git a/dag/gunbc/runner/runner_unit_file.dag b/dag/gunbc/runner/runner_unit_file.dag index 77e76d616ef..1d30bec4db6 100644 --- a/dag/gunbc/runner/runner_unit_file.dag +++ b/dag/gunbc/runner/runner_unit_file.dag @@ -173,6 +173,11 @@ fn runner_unit_app_environment(app: GithubAppRunnerConfig) -> List List { match scope { BorrowerHeldCooperativeHostFifo { fifo_path: p, daemon_service: _ } => @@ -183,10 +188,6 @@ fn runner_unit_jobserver_environment(scope: CompileParallelismRealization) -> Li value: jobserver_makeflags_fifo_auth(fifo_path: p as String), ), ] - // NO MAKEFLAGS, AND THAT ABSENCE IS THE POINT. Under invocation-local parallelism there is no - // shared pool to advertise, so handing cargo an auth clause would point it at a FIFO nobody - // serves. The bound moves to CARGO_BUILD_JOBS, which cargo applies per invocation and which - // therefore cannot survive the process that read it. InvocationLocalCargo { jobs_per_slot: j } => [ runner_unit_environment( From 58a70c55e4291c1ee451ffcda5e98d717a71858a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 05:26:59 +0000 Subject: [PATCH 07/15] No observation asserts its own safety, and the Boolean predicate goes with it Review 58469, both findings, and both are right. HostCancellationSafe carried an authored disposition beside an active_unit_readback string, and the fold read only the disposition -- so the readback was decorative and arbitrary prose could label a host capacity-preserving and, through the policy fold, authorize superseding running builds. My own server-reclamation fixture demonstrated exactly that with a sentence of prose. A carrier that looks like evidence and is never consumed is worse than no carrier, because it will be cited as coverage. The observation now carries only WHAT WAS READ -- the realization -- and the fold DERIVES the disposition from it. There is no longer a constructor for a safe host at all, so the self-certifying state is unwritable rather than merely unwitnessed. HostCancellationUnsafe became HostCancellationUnreadable, which is the honest residual: a readback obtained but not interpretable, distinct from no readback at all, and both on the refusing side. disposition_preserves_capacity is deleted. It matched a substrate coproduct's variants only to collapse them into true/false, which is the predicate-dissolution trigger; the fold now matches the three arms directly, so a fourth disposition refuses to compile here instead of silently falling to one side. What this costs, stated rather than hidden: no realization produces CapacityPreservedByServerReclamation, so that arm now has no producer and its sufficiency is modeled and consumed but not exercised. That is the honest state -- the semantic outcome exists because the dissolve-on names it, and it becomes reachable when someone builds the realization. Binding real host readbacks to realizations is the stage-2 consumer this PR does not claim to have; until it exists the fleet standing has no observations and the policy refuses. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 49 ++++++++++--------- .../claim/run_disposition_witness_test.dag | 48 ++++++------------ 2 files changed, 41 insertions(+), 56 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index f22e4e72d3a..10a5677a022 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -54,14 +54,6 @@ fn borrower_death_capacity_disposition( } } -fn disposition_preserves_capacity(disposition: BorrowerDeathCapacityDisposition) -> Bool { - match disposition { - CapacityLostUntilPoolRestart => false - CapacityPreservedByInvocationLifetime => true - CapacityPreservedByServerReclamation => true - } -} - // WHAT A HOST HAS BEEN OBSERVED TO BE RUNNING, which is not what a row desires it to run. // // This is the boundary the first draft of this module got wrong, and the error was a fail-open of @@ -75,12 +67,8 @@ fn disposition_preserves_capacity(disposition: BorrowerDeathCapacityDisposition) // So the safe arm carries its READBACK rather than asserting itself: what the active unit says, not // what the model wishes it said. type HostCompileCancellationStanding - = HostCancellationSafe { - host: NonEmptyStr, - disposition: BorrowerDeathCapacityDisposition, - active_unit_readback: NonEmptyStr, - } - | HostCancellationUnsafe { host: NonEmptyStr, cause: NonEmptyStr } + = HostCancellationObserved { host: NonEmptyStr, realization: CompileParallelismRealization } + | HostCancellationUnreadable { host: NonEmptyStr, cause: NonEmptyStr } | HostCancellationUnobserved { host: NonEmptyStr, cause: NonEmptyStr } type FleetCompileCancellationStanding @@ -107,9 +95,17 @@ type FleetCancellationFoldAcc { // has no unsafe and no unobserved host either, so testing only the blocking roster would report // SAFE for silence. // -// And a HostCancellationSafe carrying a disposition that loses capacity is a contradiction in the -// observation rather than a safe host, so it joins the unsafe side -- without that arm the safe -// constructor would be self-certifying. +// NO OBSERVATION ASSERTS ITS OWN SAFETY. An earlier draft had HostCancellationSafe carry both an +// authored disposition and an active_unit_readback string, and the fold read only the disposition -- +// so the readback was decorative and arbitrary prose could label a host capacity-preserving, which +// is the self-certifying carrier review 58469 named. The observation now carries only WHAT WAS READ +// -- the realization -- and safety is DERIVED from it here, so there is no constructor for "safe" +// at all. +// +// The Boolean predicate that used to sit between them is gone with it. It matched the disposition +// coproduct's variants only to collapse them to true/false, which is the predicate-dissolution +// trigger; the fold matches the three arms directly, and a fourth disposition would refuse to +// compile here rather than silently falling to one side. fn fleet_cancellation_standing( observations: List, ) -> FleetCompileCancellationStanding { @@ -117,20 +113,25 @@ fn fleet_cancellation_standing( observations, init: FleetCancellationFoldAcc { unsafe_hosts: [], unobserved_hosts: [], safe_hosts: [] }, f: (a, o) => match o { - HostCancellationSafe { host: h, disposition: d, active_unit_readback: _ } => - match disposition_preserves_capacity(disposition: d) { - true => FleetCancellationFoldAcc { + HostCancellationObserved { host: h, realization: r } => + match borrower_death_capacity_disposition(realization: r) { + CapacityLostUntilPoolRestart => FleetCancellationFoldAcc { + unsafe_hosts: concat(a.unsafe_hosts, [h]), + unobserved_hosts: a.unobserved_hosts, + safe_hosts: a.safe_hosts, + } + CapacityPreservedByInvocationLifetime => FleetCancellationFoldAcc { unsafe_hosts: a.unsafe_hosts, unobserved_hosts: a.unobserved_hosts, safe_hosts: concat(a.safe_hosts, [h]), } - false => FleetCancellationFoldAcc { - unsafe_hosts: concat(a.unsafe_hosts, [h]), + CapacityPreservedByServerReclamation => FleetCancellationFoldAcc { + unsafe_hosts: a.unsafe_hosts, unobserved_hosts: a.unobserved_hosts, - safe_hosts: a.safe_hosts, + safe_hosts: concat(a.safe_hosts, [h]), } } - HostCancellationUnsafe { host: h, cause: _ } => FleetCancellationFoldAcc { + HostCancellationUnreadable { host: h, cause: _ } => FleetCancellationFoldAcc { unsafe_hosts: concat(a.unsafe_hosts, [h]), unobserved_hosts: a.unobserved_hosts, safe_hosts: a.safe_hosts, diff --git a/dag/test/claim/run_disposition_witness_test.dag b/dag/test/claim/run_disposition_witness_test.dag index 9f6428553b1..7f27ec346f8 100644 --- a/dag/test/claim/run_disposition_witness_test.dag +++ b/dag/test/claim/run_disposition_witness_test.dag @@ -1,6 +1,7 @@ module test.claim.run_disposition_witness_test import std.types { Bool, String, NonEmptyStr } +import std.measure { hardware_thread_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.github.actions_runs { WorkflowRunRecord, @@ -14,12 +15,11 @@ import gunbc.compile_permit_scope { FleetCancellationSafe, FleetCancellationNotSafe, HostCompileCancellationStanding, - HostCancellationSafe, - HostCancellationUnsafe, + HostCancellationObserved, + HostCancellationUnreadable, HostCancellationUnobserved, - CapacityPreservedByInvocationLifetime, - CapacityPreservedByServerReclamation, - CapacityLostUntilPoolRestart, + BorrowerHeldCooperativeHostFifo, + InvocationLocalCargo, fleet_cancellation_standing, fleet_compile_cancellation_standing } @@ -583,10 +583,9 @@ test fn w_the_running_axis_crosses_into_the_queue_max_vocabulary() -> Bool { // ── The drop retires by construction, and only on observed convergence ───────────────────────── fn safe_host(name: String) -> HostCompileCancellationStanding { - HostCancellationSafe { + HostCancellationObserved { host: name as NonEmptyStr, - disposition: CapacityPreservedByInvocationLifetime, - active_unit_readback: "Environment=CARGO_BUILD_JOBS=8" as NonEmptyStr, + realization: InvocationLocalCargo { jobs_per_slot: hardware_thread_count(count: 8) }, } } @@ -623,13 +622,13 @@ test fn w_a_single_unobserved_host_holds_the_containment() -> Bool { } } -test fn w_a_single_unsafe_host_holds_the_containment() -> Bool { +test fn w_a_single_unreadable_host_holds_the_containment() -> Bool { match running_supersession_for_fleet_standing( standing: fleet_cancellation_standing(observations: [ safe_host(name: "srv1"), - HostCancellationUnsafe { + HostCancellationUnreadable { host: "srv4" as NonEmptyStr, - cause: "active unit still names the host FIFO" as NonEmptyStr, + cause: "systemctl show returned no Environment property" as NonEmptyStr, }, ]), ) { @@ -640,13 +639,15 @@ test fn w_a_single_unsafe_host_holds_the_containment() -> Bool { // A READBACK THAT CLAIMS SAFE WHILE CARRYING A LOSING DISPOSITION IS A CONTRADICTION, and joins the // unsafe side rather than being believed. Without this arm the safe constructor is self-certifying. -test fn w_a_safe_readback_carrying_a_losing_disposition_is_not_safe() -> Bool { +test fn w_a_host_still_running_the_cooperative_fifo_is_derived_unsafe() -> Bool { match running_supersession_for_fleet_standing( standing: fleet_cancellation_standing(observations: [ - HostCancellationSafe { + HostCancellationObserved { host: "srv1" as NonEmptyStr, - disposition: CapacityLostUntilPoolRestart, - active_unit_readback: "Environment=MAKEFLAGS=--jobserver-auth=fifo:/var/lib/ctrl/jobserver/host.fifo" as NonEmptyStr, + realization: BorrowerHeldCooperativeHostFifo { + fifo_path: "/var/lib/ctrl/jobserver/host.fifo" as NonEmptyStr, + daemon_service: "ctrl-jobserver.service" as NonEmptyStr, + }, }, ]), ) { @@ -670,23 +671,6 @@ test fn w_a_fully_observed_safe_fleet_restores_supersession() -> Bool { } } -// SERVER RECLAMATION IS THE OTHER SUFFICIENT ARM the dissolve-on names, and the policy already knows -// what it means -- so the day a server-owned pool exists it needs no new business branch here. -test fn w_server_reclamation_is_a_sufficient_arm_for_the_policy() -> Bool { - match running_supersession_for_fleet_standing( - standing: fleet_cancellation_standing(observations: [ - HostCancellationSafe { - host: "srv1" as NonEmptyStr, - disposition: CapacityPreservedByServerReclamation, - active_unit_readback: "server-owned pool with death reclamation" as NonEmptyStr, - }, - ]), - ) { - SupersedeRunningForEvent { event: e } => e == "pull_request" - NeverSupersedeRunning => false - } -} - // THE LIVE ROW STILL PROJECTS WHAT CI ACTUALLY RUNS, so the fixtures above cannot go green while the // emitted workflow quietly moves. test fn w_the_live_fleet_standing_still_refuses_running_supersession() -> Bool { From 84b7b3dfad296a1013856838a11d154b9a39f745 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 05:42:50 +0000 Subject: [PATCH 08/15] The eligible-host denominator is a parameter, not a sentence in an annotation Side-chat review of the pushed head found that my annotation claimed the caller supplies the eligible-host roster while fleet_cancellation_standing took only observations. So [safe_host("srv1")] answered SAFE with srv2, srv3 and srv4 eligible and never asked -- the unsafe interval this whole construction exists to close, still writable, described as closed. An annotation cannot authorize; only executable structure can. The roster is now an argument, and SAFE is an identity join over it rather than a count equality: every eligible host must appear among the safe observations, no observation may name a host outside the roster, and the counts must agree so a duplicate cannot stand in for an absentee. Missing hosts are reported in unobserved_hosts rather than vanishing. An empty roster refuses outright -- a fleet with no eligible hosts is an unasked question, not a safe fleet. Two witnesses for the arms the parameter exists for: a partially observed fleet is not safe, and an observation for a host outside the roster does not complete it. The second is what makes the join two-directional rather than a size comparison. Still open from the same review and not addressed here: the two exact-order unit witnesses are contiguous substring checks, which prove one expected fragment occurs but not that it is the complete [Unit] list with no duplicate or extra directive. A complete-equality oracle against a production-equivalent baseline is the accepted substitute for the parent-versus-candidate differential, and it is the next commit rather than this one. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 51 ++++++++++++++----- .../claim/run_disposition_witness_test.dag | 51 +++++++++++++++---- 2 files changed, 81 insertions(+), 21 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index 10a5677a022..4ab119f86b9 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -1,6 +1,7 @@ module gunbc.compile_permit_scope import std.types { String, NonEmptyStr, List, Bool, list_length } +import std.materialization_ladder { string_list_contains } import std.measure { HardwareThreadCount } // WHAT A BORROWER'S DEATH DOES TO FUTURE COMPILE CAPACITY. That is the fact gunbc#9789's declared @@ -85,15 +86,16 @@ type FleetCancellationFoldAcc { // not safe either -- it is the empty-observation narrowing this repository has a named failure mode // for. A fleet nobody has looked at is unobserved, and unobserved is on the refusing side. // -// The caller supplies the eligible-host denominator, so a host that satisfies the workflow's runner -// selector and produced no observation arrives here as HostCancellationUnobserved rather than being -// silently absent from the fold. A fold that ranged only over the observations it happened to -// receive would answer SAFE for a fleet it had never asked about. +// THE DENOMINATOR IS A PARAMETER, NOT A SENTENCE. An earlier draft's annotation said the caller +// supplied the eligible-host roster while the signature took only observations, so one safe +// observation carried the whole fleet: [safe_host("srv1")] answered SAFE while srv2, srv3 and srv4 +// were eligible and unobserved. An annotation cannot authorize; only executable structure can, and +// that is what review 58469's companion finding names. // -// SAFE THEREFORE REQUIRES BOTH a non-empty safe roster and an empty blocking one. The first -// conjunct is what keeps an empty observation set on the refusing side: a fleet nobody looked at -// has no unsafe and no unobserved host either, so testing only the blocking roster would report -// SAFE for silence. +// SAFE IS AN IDENTITY JOIN over that roster, not a count equality -- every eligible host must appear +// among the safe observations (missing), no observation may name a host outside it (unexpected), and +// the counts must agree so a duplicate cannot stand in for an absentee. An empty roster is refused +// outright: a fleet with no eligible hosts is not a safe fleet, it is an unasked question. // // NO OBSERVATION ASSERTS ITS OWN SAFETY. An earlier draft had HostCancellationSafe carry both an // authored disposition and an active_unit_readback string, and the fold read only the disposition -- @@ -107,6 +109,7 @@ type FleetCancellationFoldAcc { // trigger; the fold matches the three arms directly, and a fourth disposition would refuse to // compile here rather than silently falling to one side. fn fleet_cancellation_standing( + eligible_hosts: List, observations: List, ) -> FleetCompileCancellationStanding { let acc = fold( @@ -143,21 +146,45 @@ fn fleet_cancellation_standing( } }, ) + let safe_names = map(acc.safe_hosts, h => h as String) + let missing = fold( + eligible_hosts, + init: [], + f: (m, e) => if string_list_contains(xs: safe_names, wanted: e as String) { m } else { concat(m, [e]) }, + ) + let unexpected = fold( + acc.safe_hosts, + init: [], + f: (u, h) => if string_list_contains(xs: map(eligible_hosts, e => e as String), wanted: h as String) { u } else { concat(u, [h]) }, + ) let blocking = list_length(items: concat(acc.unsafe_hosts, acc.unobserved_hosts)) - let observed_safe = list_length(items: acc.safe_hosts) - let fleet_is_safe = (blocking == 0) && (observed_safe > 0) + let eligible_count = list_length(items: eligible_hosts) + let safe_count = list_length(items: acc.safe_hosts) + let joined = (list_length(items: missing) == 0) && (list_length(items: unexpected) == 0) + let no_duplicates = safe_count == eligible_count + let fleet_is_safe = (blocking == 0) && (eligible_count > 0) && joined && no_duplicates match fleet_is_safe { true => FleetCancellationSafe { hosts: acc.safe_hosts } false => FleetCancellationNotSafe { unsafe_hosts: acc.unsafe_hosts, - unobserved_hosts: acc.unobserved_hosts, + unobserved_hosts: concat(acc.unobserved_hosts, missing), } } } +// THE HOSTS THE REQUIRED FLOOR CAN ROUTE TO, which is the denominator the join above ranges over. +// Every one of them must be observed safe before a kill stops costing capacity, because a single +// unconverged host still leaks a permit for every superseded build that lands on it. +data fleet_cancellation_eligible_hosts: List = [ + "srv1" as NonEmptyStr, + "srv2" as NonEmptyStr, + "srv3" as NonEmptyStr, + "srv4" as NonEmptyStr, +] + // THE FLEET AS OBSERVED TODAY: nothing. No host readback exists yet, so the standing is NotSafe with // an empty roster on both sides, and the policy below stays NeverSupersedeRunning BY REFUSAL rather // than by a literal someone has to remember to keep. Publishing real observations is what moves it, // and that is the second stage of the cutover -- deploy and restart the safe realization on every // eligible host, read the active units back, bind the receipts, and only then does the policy move. -data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_cancellation_standing(observations: []) +data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_cancellation_standing(eligible_hosts: fleet_cancellation_eligible_hosts, observations: []) diff --git a/dag/test/claim/run_disposition_witness_test.dag b/dag/test/claim/run_disposition_witness_test.dag index 7f27ec346f8..f4c0a812f80 100644 --- a/dag/test/claim/run_disposition_witness_test.dag +++ b/dag/test/claim/run_disposition_witness_test.dag @@ -1,6 +1,6 @@ module test.claim.run_disposition_witness_test -import std.types { Bool, String, NonEmptyStr } +import std.types { Bool, String, NonEmptyStr, List } import std.measure { hardware_thread_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.github.actions_runs { @@ -582,6 +582,10 @@ test fn w_the_running_axis_crosses_into_the_queue_max_vocabulary() -> Bool { // ── The drop retires by construction, and only on observed convergence ───────────────────────── +fn two_host_fleet() -> List { + ["srv1" as NonEmptyStr, "srv2" as NonEmptyStr] +} + fn safe_host(name: String) -> HostCompileCancellationStanding { HostCancellationObserved { host: name as NonEmptyStr, @@ -597,7 +601,7 @@ fn safe_host(name: String) -> HostCompileCancellationStanding { // per kill. So the policy reads an OBSERVED fleet standing, and the arms below are that join. test fn w_an_unobserved_fleet_refuses_to_supersede_a_running_run() -> Bool { match running_supersession_for_fleet_standing( - standing: fleet_cancellation_standing(observations: []), + standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: []), ) { NeverSupersedeRunning => true SupersedeRunningForEvent { event: _ } => false @@ -608,11 +612,10 @@ test fn w_an_unobserved_fleet_refuses_to_supersede_a_running_run() -> Bool { // the fleet safe while an eligible host nobody asked about went on leaking. test fn w_a_single_unobserved_host_holds_the_containment() -> Bool { match running_supersession_for_fleet_standing( - standing: fleet_cancellation_standing(observations: [ + standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: [ safe_host(name: "srv1"), - safe_host(name: "srv2"), HostCancellationUnobserved { - host: "srv3" as NonEmptyStr, + host: "srv2" as NonEmptyStr, cause: "no active unit readback" as NonEmptyStr, }, ]), @@ -624,10 +627,10 @@ test fn w_a_single_unobserved_host_holds_the_containment() -> Bool { test fn w_a_single_unreadable_host_holds_the_containment() -> Bool { match running_supersession_for_fleet_standing( - standing: fleet_cancellation_standing(observations: [ + standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: [ safe_host(name: "srv1"), HostCancellationUnreadable { - host: "srv4" as NonEmptyStr, + host: "srv2" as NonEmptyStr, cause: "systemctl show returned no Environment property" as NonEmptyStr, }, ]), @@ -641,7 +644,7 @@ test fn w_a_single_unreadable_host_holds_the_containment() -> Bool { // unsafe side rather than being believed. Without this arm the safe constructor is self-certifying. test fn w_a_host_still_running_the_cooperative_fifo_is_derived_unsafe() -> Bool { match running_supersession_for_fleet_standing( - standing: fleet_cancellation_standing(observations: [ + standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: [ HostCancellationObserved { host: "srv1" as NonEmptyStr, realization: BorrowerHeldCooperativeHostFifo { @@ -661,7 +664,7 @@ test fn w_a_host_still_running_the_cooperative_fifo_is_derived_unsafe() -> Bool // NeverSupersedeRunning for everything would pass every witness above and fail here. test fn w_a_fully_observed_safe_fleet_restores_supersession() -> Bool { match running_supersession_for_fleet_standing( - standing: fleet_cancellation_standing(observations: [ + standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: [ safe_host(name: "srv1"), safe_host(name: "srv2"), ]), @@ -679,3 +682,33 @@ test fn w_the_live_fleet_standing_still_refuses_running_supersession() -> Bool { SupersedeRunningForEvent { event: _ } => false } } + + +// A SAFE OBSERVATION FOR PART OF THE FLEET IS NOT A SAFE FLEET. This is the arm the denominator +// exists for: before it was a parameter, one safe host answered SAFE while every other eligible host +// went unasked, and the unsafe interval stayed writable. +test fn w_a_partially_observed_fleet_is_not_safe() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing( + eligible_hosts: two_host_fleet(), + observations: [safe_host(name: "srv1")], + ), + ) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} + +// AND AN OBSERVATION FOR A HOST OUTSIDE THE ROSTER CANNOT STAND IN FOR ONE INSIDE IT, which is why +// the join runs in both directions rather than comparing two counts. +test fn w_an_observation_outside_the_roster_does_not_complete_it() -> Bool { + match running_supersession_for_fleet_standing( + standing: fleet_cancellation_standing( + eligible_hosts: two_host_fleet(), + observations: [safe_host(name: "srv1"), safe_host(name: "srv9")], + ), + ) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} From d611dd42310ecf58dfb35e7293ff66f3afd8b1d7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 05:59:15 +0000 Subject: [PATCH 09/15] Pin the complete [Unit] section header-to-header, on the production values The last open item from the side-chat differential ruling. The two exact-order witnesses were contiguous string_contains checks: they prove an expected run of directives occurs, which fixes order WITHIN that run and says nothing about what surrounds it. A duplicated After=, an extra Wants=, or a stray blank line outside the fragment left them green, so they could not answer the question the restructure actually raised -- did interleaving the optional pair change any byte that was not meant to change. Sections are emitted header-first and separated by one empty line, so pinning from [Unit] through to [Service] is the entire section and nothing can hide inside it. That is the complete-equality oracle offered as the accepted substitute for a two-compiler parent-versus-candidate differential, without standing machinery that builds two compilers on every run. It renders the PRODUCTION realization -- the fleet's own FIFO path and daemon service -- beside the distinct-value fixture rather than instead of it, because they answer different questions. The fixture proves the renderer consumes its argument's payload; this proves the live arm serializes to exactly what the fleet's realization produces. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- .../runner/runner_unit_file_witness_test.dag | 48 +++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index 75224872f26..0ba27b9c2db 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -11,6 +11,7 @@ import gunbc.runner_unit { lifecycle_intent_cannot_orphan, } import gunbc.runner_host_deploy { srv1_runner_host_deploy } +import gunbc.host_converge { gunbc_runner_jobserver_default_fifo, gunbc_runner_jobserver_service } import gunbc.compile_permit_scope { CompileParallelismRealization, BorrowerHeldCooperativeHostFifo, @@ -298,3 +299,50 @@ test fn w_the_cutover_arm_advertises_no_shared_pool() -> Bool { test fn w_the_cutover_arm_drops_the_daemon_ordering() -> Bool { !string_contains(s: invocation_local_text(), pattern: "fixture-other.service") } + + +// ── The complete [Unit] section, pinned header to header ──────────────────────────────────────── + +// A CONTIGUOUS FRAGMENT IS NOT A COMPLETE SECTION. The two witnesses above assert that an expected +// run of directives occurs, which proves order WITHIN that run and nothing about what surrounds it: +// a duplicated After=, an extra Wants=, or a stray blank line outside the fragment leaves them +// green. Since sections are emitted header-first and separated by one empty line, pinning from +// "[Unit]" through to "[Service]" is the whole section -- nothing can hide inside it. +// +// AND IT RENDERS THE PRODUCTION VALUES, beside the distinct-value fixture rather than instead of it. +// They answer different questions: the fixture proves the renderer consumes its argument's payload, +// this proves the live arm's serialization is exactly what the fleet's own realization produces. +fn production_realization() -> CompileParallelismRealization { + BorrowerHeldCooperativeHostFifo { + fifo_path: gunbc_runner_jobserver_default_fifo as NonEmptyStr, + daemon_service: gunbc_runner_jobserver_service as NonEmptyStr, + } +} + +fn production_unit_text() -> String { + match runner_unit_text( + rendering: runner_unit_file( + deploy: srv1_runner_host_deploy, + spec: srv1_spec(), + permit_scope: production_realization(), + intent: gunbc_runner_lifecycle_intent, + ), + ) { + RunnerUnitText { text: t } => t + RunnerUnitTextRefused { reason: _ } => "" + } +} + +test fn w_the_production_arm_unit_section_is_complete_and_exact() -> Bool { + string_contains( + s: production_unit_text(), + pattern: "[Unit]\nDescription=Ephemeral GitHub Actions Runner (%i)\nAfter=network-online.target\nAfter=ctrl-jobserver.service\nWants=network-online.target\nWants=ctrl-jobserver.service\nStartLimitIntervalSec=0\n\n[Service]", + ) +} + +test fn w_the_cutover_arm_unit_section_is_complete_and_exact() -> Bool { + string_contains( + s: invocation_local_text(), + pattern: "[Unit]\nDescription=Ephemeral GitHub Actions Runner (%i)\nAfter=network-online.target\nWants=network-online.target\nStartLimitIntervalSec=0\n\n[Service]", + ) +} From b34471ceaba23f740676c6fe0abe1d900b7f882f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 06:14:20 +0000 Subject: [PATCH 10/15] The denominator is the fleet's own roster, not a second one Review 58495, and it is right in a way that matters more than the ordinary parallel-authority case: the re-minted list would have defeated the very join it fed. fleet_cancellation_eligible_hosts hardcoded four names beside gunbc.fleet_runner_connectivity fleet_hosts, which already owns that fact and has several consumers. Add a fifth host to the real roster and my copy answers SAFE on a 4/4 observation set while the new host leaks a permit for every superseded build -- the exact denominator failure the parameter was added to prevent, reintroduced one layer up. The roster is gone and the standing reads fleet_hosts(). Hosts are typed HostIdentity throughout rather than bare NonEmptyStr, which is what the fleet authority already returns, so the join compares the same branded identity the rest of the corpus uses instead of casting through a second spelling. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 39 +++++++++---------- .../claim/run_disposition_witness_test.dag | 13 ++++--- 2 files changed, 26 insertions(+), 26 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index 4ab119f86b9..f042fa515ba 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -2,6 +2,8 @@ module gunbc.compile_permit_scope import std.types { String, NonEmptyStr, List, Bool, list_length } import std.materialization_ladder { string_list_contains } +import product.placement_supply { HostIdentity } +import gunbc.fleet_runner_connectivity { fleet_hosts } import std.measure { HardwareThreadCount } // WHAT A BORROWER'S DEATH DOES TO FUTURE COMPILE CAPACITY. That is the fact gunbc#9789's declared @@ -68,18 +70,18 @@ fn borrower_death_capacity_disposition( // So the safe arm carries its READBACK rather than asserting itself: what the active unit says, not // what the model wishes it said. type HostCompileCancellationStanding - = HostCancellationObserved { host: NonEmptyStr, realization: CompileParallelismRealization } - | HostCancellationUnreadable { host: NonEmptyStr, cause: NonEmptyStr } - | HostCancellationUnobserved { host: NonEmptyStr, cause: NonEmptyStr } + = HostCancellationObserved { host: HostIdentity, realization: CompileParallelismRealization } + | HostCancellationUnreadable { host: HostIdentity, cause: NonEmptyStr } + | HostCancellationUnobserved { host: HostIdentity, cause: NonEmptyStr } type FleetCompileCancellationStanding - = FleetCancellationSafe { hosts: List } - | FleetCancellationNotSafe { unsafe_hosts: List, unobserved_hosts: List } + = FleetCancellationSafe { hosts: List } + | FleetCancellationNotSafe { unsafe_hosts: List, unobserved_hosts: List } type FleetCancellationFoldAcc { - unsafe_hosts: List - unobserved_hosts: List - safe_hosts: List + unsafe_hosts: List + unobserved_hosts: List + safe_hosts: List } // ONE UNSAFE, MIXED OR UNREAD HOST KEEPS THE CONTAINMENT IN FORCE, and an EMPTY observation set is @@ -109,7 +111,7 @@ type FleetCancellationFoldAcc { // trigger; the fold matches the three arms directly, and a fourth disposition would refuse to // compile here rather than silently falling to one side. fn fleet_cancellation_standing( - eligible_hosts: List, + eligible_hosts: List, observations: List, ) -> FleetCompileCancellationStanding { let acc = fold( @@ -172,19 +174,16 @@ fn fleet_cancellation_standing( } } -// THE HOSTS THE REQUIRED FLOOR CAN ROUTE TO, which is the denominator the join above ranges over. -// Every one of them must be observed safe before a kill stops costing capacity, because a single -// unconverged host still leaks a permit for every superseded build that lands on it. -data fleet_cancellation_eligible_hosts: List = [ - "srv1" as NonEmptyStr, - "srv2" as NonEmptyStr, - "srv3" as NonEmptyStr, - "srv4" as NonEmptyStr, -] - +// THE DENOMINATOR IS THE FLEET'S OWN ROSTER, read from gunbc.fleet_runner_connectivity fleet_hosts +// rather than re-minted here. Review 58495 caught the second authoring, and its concrete +// consequence is that this construction would have defeated itself: a fifth host joining the fleet +// leaves a hand-written four-name list answering SAFE on a 4/4 observation set while the new host +// leaks a permit per kill -- the exact denominator failure the parameter was added to prevent, +// reintroduced one layer up. +// // THE FLEET AS OBSERVED TODAY: nothing. No host readback exists yet, so the standing is NotSafe with // an empty roster on both sides, and the policy below stays NeverSupersedeRunning BY REFUSAL rather // than by a literal someone has to remember to keep. Publishing real observations is what moves it, // and that is the second stage of the cutover -- deploy and restart the safe realization on every // eligible host, read the active units back, bind the receipts, and only then does the policy move. -data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_cancellation_standing(eligible_hosts: fleet_cancellation_eligible_hosts, observations: []) +data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_cancellation_standing(eligible_hosts: fleet_hosts(), observations: []) diff --git a/dag/test/claim/run_disposition_witness_test.dag b/dag/test/claim/run_disposition_witness_test.dag index f4c0a812f80..3d7afc666c0 100644 --- a/dag/test/claim/run_disposition_witness_test.dag +++ b/dag/test/claim/run_disposition_witness_test.dag @@ -1,6 +1,7 @@ module test.claim.run_disposition_witness_test import std.types { Bool, String, NonEmptyStr, List } +import product.placement_supply { HostIdentity } import std.measure { hardware_thread_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.github.actions_runs { @@ -582,13 +583,13 @@ test fn w_the_running_axis_crosses_into_the_queue_max_vocabulary() -> Bool { // ── The drop retires by construction, and only on observed convergence ───────────────────────── -fn two_host_fleet() -> List { - ["srv1" as NonEmptyStr, "srv2" as NonEmptyStr] +fn two_host_fleet() -> List { + ["srv1" as HostIdentity, "srv2" as HostIdentity] } fn safe_host(name: String) -> HostCompileCancellationStanding { HostCancellationObserved { - host: name as NonEmptyStr, + host: name as HostIdentity, realization: InvocationLocalCargo { jobs_per_slot: hardware_thread_count(count: 8) }, } } @@ -615,7 +616,7 @@ test fn w_a_single_unobserved_host_holds_the_containment() -> Bool { standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: [ safe_host(name: "srv1"), HostCancellationUnobserved { - host: "srv2" as NonEmptyStr, + host: "srv2" as HostIdentity, cause: "no active unit readback" as NonEmptyStr, }, ]), @@ -630,7 +631,7 @@ test fn w_a_single_unreadable_host_holds_the_containment() -> Bool { standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: [ safe_host(name: "srv1"), HostCancellationUnreadable { - host: "srv2" as NonEmptyStr, + host: "srv2" as HostIdentity, cause: "systemctl show returned no Environment property" as NonEmptyStr, }, ]), @@ -646,7 +647,7 @@ test fn w_a_host_still_running_the_cooperative_fifo_is_derived_unsafe() -> Bool match running_supersession_for_fleet_standing( standing: fleet_cancellation_standing(eligible_hosts: two_host_fleet(), observations: [ HostCancellationObserved { - host: "srv1" as NonEmptyStr, + host: "srv1" as HostIdentity, realization: BorrowerHeldCooperativeHostFifo { fifo_path: "/var/lib/ctrl/jobserver/host.fifo" as NonEmptyStr, daemon_service: "ctrl-jobserver.service" as NonEmptyStr, From 26d5625edd03781ae33d2ee8eb53973a32c35e41 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 06:43:45 +0000 Subject: [PATCH 11/15] Complete-file equality against an independently enumerated parent shape The differential finding, discharged rather than deferred a second time. Every previous version of this evidence was string_contains -- contiguous fragments, then the whole [Unit] section header-to-header -- and none of them is the byte claim the restructure owes. A substring says nothing about what surrounds it: a duplicated directive in [Service], an extra blank line, a dropped Install directive all leave it green. Three complete-equality witnesses now compare the serialized render against an expected SystemdUnitFile enumerated here. The expected side does not call runner_unit_file, runner_unit_jobserver_after, runner_unit_jobserver_wants or runner_unit_jobserver_environment -- the four places the restructure moved -- because an oracle built from the code under test agrees with it by construction. It does reuse runner_unit_app_environment and the shared serializer, which are not what changed. One expected constructor serves two orthogonal propositions, executed twice. Against the production FIFO and service it establishes that the live arm's complete bytes are unchanged from parent d61f8c9bc4d341ce0576799e97aac1bbf055ce32. Against /fixture/other.fifo and fixture-other.service it establishes that the renderer consumes its argument -- a renderer hardcoding today's constants passes the first perfectly and fails the second, since the expected object places the fixture path twice and the fixture service twice. The cutover arm gets its own constructor rather than an expected-side match, so the oracle never reproduces the candidate's arm dispatch. rendered_or_refused replaces the helper that collapsed a refusal to the empty string. For a substring probe that was harmless; for an equality oracle it is fatal, because a renderer that refused everything would satisfy "" == "". A refusal now renders its reason and fails the comparison. The three witnesses these subsume are deleted rather than left beside them, since a weaker assertion over the same subject is a second representation that can only go green when the stronger one already has. This is a TRANSITION oracle, not a claim the unit may never change. When it legitimately moves, the expected shape moves with it and the parent anchor becomes the previous transition. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- .../runner/runner_unit_file_witness_test.dag | 238 +++++++++++++----- 1 file changed, 174 insertions(+), 64 deletions(-) diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index 0ba27b9c2db..198b7986388 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -3,7 +3,30 @@ module test.claim.runner_unit_file_witness_test import std.types { Bool, String, NonEmptyStr } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.github.actions { RunnerSpec, SelfHosted, HostedRunner, RunsOnExpression, UbuntuLatest } -import extdeps.systemd.unit_file { ExitTypeMain, KillModeProcess } +import extdeps.systemd.unit_file { + ExitTypeMain, + KillModeProcess, + SystemdUnitFile, + ServiceUnitFile, + Description, + After, + Wants, + StartLimitIntervalSec, + ServiceType, + ServiceUser, + WorkingDirectory, + ExecStart, + Restart, + RestartSec, + ServiceExitType, + ServiceKillMode, + TimeoutStopSec, + Installable, + WantedBy, + serialize_systemd_unit_file, +} +import extdeps.languages.json.emit { json_string, json_array, serialize_json } +import gunbc.runner_lifecycle { runner_lifecycle_jit_wrapper_path } import gunbc.runner_unit { RunnerUnitLifecycleIntent, gunbc_runner_lifecycle_intent, @@ -32,6 +55,10 @@ import gunbc.runner_unit_file { gunbc_runner_unit_file, runner_unit_text, runner_unit_system_path, + runner_unit_environment, + runner_unit_quoted_environment, + runner_unit_app_environment, + runner_slot_instance_directory, } // Every claim here is a function of declared substrate rows -- a render and its serialization -- so @@ -235,38 +262,7 @@ fn invocation_local_text() -> String { RunnerUnitText { text: t } => t RunnerUnitTextRefused { reason: _ } => "" } -} - -// EVERY FIELD OF THE ARM REACHES THE FOUR PLACES THAT NAME IT. Four separate assertions rather than -// one, because a renderer that dropped the daemon service from the ordering while keeping it in the -// environment would otherwise still pass. -test fn w_the_realization_payload_reaches_every_directive_that_names_it() -> Bool { - let text = rendered_text(intent: gunbc_runner_lifecycle_intent) - string_contains(s: text, pattern: "\nEnvironment=CTRL_JOBSERVER_FIFO=/fixture/other.fifo\n") - && string_contains(s: text, pattern: "\nEnvironment=MAKEFLAGS=--jobserver-auth=fifo:/fixture/other.fifo\n") - && string_contains(s: text, pattern: "\nAfter=fixture-other.service\n") - && string_contains(s: text, pattern: "\nWants=fixture-other.service\n") -} - -// THE EXACT UNIT-SECTION SEQUENCE FOR BOTH ARMS, because the directive list was restructured to -// interleave the optional pair and substring witnesses cannot see order, duplication, or a stray -// blank line. This is the shape oracle the restructure owes. -test fn w_the_live_arm_unit_section_is_exactly_ordered() -> Bool { - let text = rendered_text(intent: gunbc_runner_lifecycle_intent) - string_contains( - s: text, - pattern: "\nAfter=network-online.target\nAfter=fixture-other.service\nWants=network-online.target\nWants=fixture-other.service\nStartLimitIntervalSec=0\n", - ) -} - -test fn w_the_cutover_arm_unit_section_is_exactly_ordered() -> Bool { - string_contains( - s: invocation_local_text(), - pattern: "\nAfter=network-online.target\nWants=network-online.target\nStartLimitIntervalSec=0\n", - ) -} - -test fn w_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies() -> Bool { +}test fn w_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies() -> Bool { match borrower_death_capacity_disposition(realization: live_realization()) { CapacityLostUntilPoolRestart => true CapacityPreservedByInvocationLifetime => false @@ -301,17 +297,90 @@ test fn w_the_cutover_arm_drops_the_daemon_ordering() -> Bool { } -// ── The complete [Unit] section, pinned header to header ──────────────────────────────────────── +// ── Complete-file equality against an independently enumerated parent shape ──────────────────── -// A CONTIGUOUS FRAGMENT IS NOT A COMPLETE SECTION. The two witnesses above assert that an expected -// run of directives occurs, which proves order WITHIN that run and nothing about what surrounds it: -// a duplicated After=, an extra Wants=, or a stray blank line outside the fragment leaves them -// green. Since sections are emitted header-first and separated by one empty line, pinning from -// "[Unit]" through to "[Service]" is the whole section -- nothing can hide inside it. +// THE TRANSITION ORACLE FOR THE RESTRUCTURE, anchored at parent d61f8c9bc4d341ce0576799e97aac1bbf055ce32. +// +// Every earlier witness here was string_contains: contiguous fragments, then the whole [Unit] +// section header-to-header. Each is stronger than the last and none of them is the byte claim the +// restructure owes, because a substring says nothing about what surrounds it -- a duplicated +// directive in [Service], an extra blank line, a dropped Install directive all leave them green. +// The proposition this witness carries is narrower and harder: interleaving the optional After and +// Wants pair changed NO byte of the live arm. // -// AND IT RENDERS THE PRODUCTION VALUES, beside the distinct-value fixture rather than instead of it. -// They answer different questions: the fixture proves the renderer consumes its argument's payload, -// this proves the live arm's serialization is exactly what the fleet's own realization produces. +// The expected side enumerates the complete file itself. It does not call runner_unit_file, +// runner_unit_jobserver_after, runner_unit_jobserver_wants or runner_unit_jobserver_environment -- +// the four places the restructure moved -- because an oracle built from the code under test agrees +// with it by construction and would make the same mistake twice. It does reuse the untouched +// runner_unit_app_environment and the shared serializer, which are not what changed. +// +// It is a TRANSITION oracle, not a claim that this unit may never intentionally change. When the +// unit legitimately moves, this expected shape moves with it and the parent anchor above becomes the +// previous transition rather than a permanent baseline. +fn expected_live_unit_file(fifo_path: String, daemon_service: NonEmptyStr) -> SystemdUnitFile { + ServiceUnitFile { + unit: [ + Description { text: "Ephemeral GitHub Actions Runner (%i)" as NonEmptyStr }, + After { target: "network-online.target" as NonEmptyStr }, + After { target: daemon_service }, + Wants { target: "network-online.target" as NonEmptyStr }, + Wants { target: daemon_service }, + StartLimitIntervalSec { duration: "0" as NonEmptyStr }, + ], + service: concat( + [ + ServiceType { mode: "simple" as NonEmptyStr }, + ServiceUser { name: srv1_runner_host_deploy.runner_user }, + WorkingDirectory { path: runner_slot_instance_directory() as NonEmptyStr }, + ], + concat( + runner_unit_app_environment(app: srv1_runner_host_deploy.app), + [ + runner_unit_environment(name: "RUNNER_DIR", value: runner_slot_instance_directory()), + runner_unit_environment(name: "RUNNER_NAME_PREFIX", value: "%i"), + runner_unit_quoted_environment(name: "LABELS_JSON", value: expected_labels_json()), + runner_unit_environment(name: "CTRL_JOBSERVER_FIFO", value: fifo_path), + runner_unit_environment( + name: "MAKEFLAGS", + value: join(["--jobserver-auth=fifo:", fifo_path], ""), + ), + ExecStart { command: runner_lifecycle_jit_wrapper_path as NonEmptyStr }, + Restart { policy: "always" as NonEmptyStr }, + RestartSec { duration: "5" as NonEmptyStr }, + ServiceExitType { exit_type: gunbc_runner_lifecycle_intent.exit_type }, + ServiceKillMode { mode: gunbc_runner_lifecycle_intent.kill_mode }, + TimeoutStopSec { duration: "5min" as NonEmptyStr }, + ], + ), + ), + install: Installable { directives: [WantedBy { target: "multi-user.target" as NonEmptyStr }] }, + } +} + +fn expected_labels_json() -> String { + serialize_json(value: json_array(items: [ + json_string(value: "self-hosted"), + json_string(value: "linux"), + json_string(value: "arm64"), + json_string(value: "srv1"), + ])) +} + +// REFUSAL MAKES THE WITNESS FALSE rather than comparing two empty strings. rendered_text collapses a +// refusal to "", which is fine for a substring probe and fatal for an equality oracle: a renderer +// that refused everything would satisfy "" == "" if the expected side collapsed the same way. +fn rendered_or_refused(realization: CompileParallelismRealization) -> String { + match runner_unit_file( + deploy: srv1_runner_host_deploy, + spec: srv1_spec(), + permit_scope: realization, + intent: gunbc_runner_lifecycle_intent, + ) { + RunnerUnitFileRendered { file: f } => serialize_systemd_unit_file(file: f) + RunnerUnitFileRefused { reason: r } => join(["REFUSED: ", r as String], "") + } +} + fn production_realization() -> CompileParallelismRealization { BorrowerHeldCooperativeHostFifo { fifo_path: gunbc_runner_jobserver_default_fifo as NonEmptyStr, @@ -319,30 +388,71 @@ fn production_realization() -> CompileParallelismRealization { } } -fn production_unit_text() -> String { - match runner_unit_text( - rendering: runner_unit_file( - deploy: srv1_runner_host_deploy, - spec: srv1_spec(), - permit_scope: production_realization(), - intent: gunbc_runner_lifecycle_intent, - ), - ) { - RunnerUnitText { text: t } => t - RunnerUnitTextRefused { reason: _ } => "" - } +test fn w_the_production_live_arm_is_byte_identical_to_the_parent_shape() -> Bool { + rendered_or_refused(realization: production_realization()) + == serialize_systemd_unit_file( + file: expected_live_unit_file( + fifo_path: gunbc_runner_jobserver_default_fifo, + daemon_service: gunbc_runner_jobserver_service as NonEmptyStr, + ), + ) } -test fn w_the_production_arm_unit_section_is_complete_and_exact() -> Bool { - string_contains( - s: production_unit_text(), - pattern: "[Unit]\nDescription=Ephemeral GitHub Actions Runner (%i)\nAfter=network-online.target\nAfter=ctrl-jobserver.service\nWants=network-online.target\nWants=ctrl-jobserver.service\nStartLimitIntervalSec=0\n\n[Service]", - ) +// THE SAME EXPECTED SHAPE, EXECUTED ON DISTINCT VALUES. A renderer that ignored its argument and +// hardcoded today's production FIFO and service would pass the witness above perfectly; the expected +// object here places the fixture path twice and the fixture service twice, so a hardcoded or dropped +// occurrence fails equality. One independently authored shape, two orthogonal propositions. +test fn w_the_live_arm_renders_its_argument_rather_than_the_production_constants() -> Bool { + rendered_or_refused(realization: live_realization()) + == serialize_systemd_unit_file( + file: expected_live_unit_file( + fifo_path: "/fixture/other.fifo", + daemon_service: "fixture-other.service" as NonEmptyStr, + ), + ) } -test fn w_the_cutover_arm_unit_section_is_complete_and_exact() -> Bool { - string_contains( - s: invocation_local_text(), - pattern: "[Unit]\nDescription=Ephemeral GitHub Actions Runner (%i)\nAfter=network-online.target\nWants=network-online.target\nStartLimitIntervalSec=0\n\n[Service]", - ) + +// AND THE CUTOVER ARM HAS EXACTLY ITS INTENDED COMPLETE SHAPE -- a separate expected constructor +// rather than an expected-side match over the realization, so the oracle does not reproduce the +// candidate's own arm dispatch. The daemon ordering is absent here because the service the cutover +// deletes cannot be ordered against, and CARGO_BUILD_JOBS replaces the pool advertisement. +fn expected_invocation_local_unit_file(jobs: String) -> SystemdUnitFile { + ServiceUnitFile { + unit: [ + Description { text: "Ephemeral GitHub Actions Runner (%i)" as NonEmptyStr }, + After { target: "network-online.target" as NonEmptyStr }, + Wants { target: "network-online.target" as NonEmptyStr }, + StartLimitIntervalSec { duration: "0" as NonEmptyStr }, + ], + service: concat( + [ + ServiceType { mode: "simple" as NonEmptyStr }, + ServiceUser { name: srv1_runner_host_deploy.runner_user }, + WorkingDirectory { path: runner_slot_instance_directory() as NonEmptyStr }, + ], + concat( + runner_unit_app_environment(app: srv1_runner_host_deploy.app), + [ + runner_unit_environment(name: "RUNNER_DIR", value: runner_slot_instance_directory()), + runner_unit_environment(name: "RUNNER_NAME_PREFIX", value: "%i"), + runner_unit_quoted_environment(name: "LABELS_JSON", value: expected_labels_json()), + runner_unit_environment(name: "CARGO_BUILD_JOBS", value: jobs), + ExecStart { command: runner_lifecycle_jit_wrapper_path as NonEmptyStr }, + Restart { policy: "always" as NonEmptyStr }, + RestartSec { duration: "5" as NonEmptyStr }, + ServiceExitType { exit_type: gunbc_runner_lifecycle_intent.exit_type }, + ServiceKillMode { mode: gunbc_runner_lifecycle_intent.kill_mode }, + TimeoutStopSec { duration: "5min" as NonEmptyStr }, + ], + ), + ), + install: Installable { directives: [WantedBy { target: "multi-user.target" as NonEmptyStr }] }, + } +} + +test fn w_the_cutover_arm_has_exactly_its_intended_complete_shape() -> Bool { + rendered_or_refused( + realization: InvocationLocalCargo { jobs_per_slot: hardware_thread_count(count: 8) }, + ) == serialize_systemd_unit_file(file: expected_invocation_local_unit_file(jobs: "8")) } From 90741a1f5c75c5ddf4119ddae5f0b523141bea91 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 06:59:49 +0000 Subject: [PATCH 12/15] Production reaches the standing through a producer, not an authored list Review 58515 is right, and it names the thing my own previous commit message admitted: HostCancellationObserved carries a realization an author supplies, so while the live standing was a data row of observations, inserting InvocationLocalCargo constructors would have enabled supersession with no host having converged. That is satisfiable by editing the declaration while the realization lies -- the validation tell DESIGN section 5 names. No in-repo type can stop a fixture constructing an observation, and it must not: section 4b requires the discriminating RED to be authorable as source handed to the compiler by a fixture, which is what every witness on this fold is. What the model can do is refuse to let PRODUCTION reach the safe arm through authorship. ActiveUnitReadbackSource is that boundary: its live row is ReadbackProducerAbsent, every eligible host is unobserved because nothing reads them, and there is no list an author can extend to change the answer -- reaching SAFE now requires implementing ReadbackObservations, which means writing the host read. The boundary is declared rather than implied by an empty observation list, because an empty list reads as 'we looked and found nothing' when the truth is 'nothing has looked'. That is the column DESIGN 4b keeps deliberately off the ladder: external reality, observed or refused at a declared boundary, never fabricated. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 49 ++++++++++++++++++++++++++---- 1 file changed, 43 insertions(+), 6 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index f042fa515ba..f08daf1602f 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -181,9 +181,46 @@ fn fleet_cancellation_standing( // leaks a permit per kill -- the exact denominator failure the parameter was added to prevent, // reintroduced one layer up. // -// THE FLEET AS OBSERVED TODAY: nothing. No host readback exists yet, so the standing is NotSafe with -// an empty roster on both sides, and the policy below stays NeverSupersedeRunning BY REFUSAL rather -// than by a literal someone has to remember to keep. Publishing real observations is what moves it, -// and that is the second stage of the cutover -- deploy and restart the safe realization on every -// eligible host, read the active units back, bind the receipts, and only then does the policy move. -data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_cancellation_standing(eligible_hosts: fleet_hosts(), observations: []) +// PRODUCTION READS A PRODUCER, NOT AN AUTHORED LIST, and that distinction is the whole of review +// 58515's finding. HostCancellationObserved carries a realization an author supplies, so if the live +// standing were a data row of observations then inserting InvocationLocalCargo constructors would +// enable supersession with no host having converged -- satisfiable by editing the declaration while +// the realization lies, which is exactly the validation tell DESIGN section 5 names. +// +// No in-repo type can stop a fixture constructing an observation, and it must not: section 4b +// requires the discriminating RED to be authorable as source handed to the compiler by a fixture, +// which is what every witness on this fold is. What the model CAN do is refuse to let production +// reach the safe arm through authorship, and that is what the boundary below does. The eligible +// hosts are unobserved because no producer reads them, and there is no data row an author can +// extend to change that answer -- reaching SAFE requires implementing ReadbackObservations, which +// means writing the host read. The cause is carried on the source row rather than in the refusal, +// because FleetCancellationNotSafe reports rosters; a reader asking WHY every host is unobserved is +// one hop away, at fleet_active_unit_readback. +// +// This is the column DESIGN 4b keeps deliberately OFF the ladder: external reality, observed or +// refused at a declared boundary, never fabricated. The boundary is declared here rather than +// implied by an empty list, because an empty list reads as "we looked and found nothing" while the +// truth is "nothing has looked". +type ActiveUnitReadbackSource + = ReadbackProducerAbsent { cause: NonEmptyStr } + | ReadbackObservations { observations: List } + +data fleet_active_unit_readback: ActiveUnitReadbackSource = ReadbackProducerAbsent { + cause: "no producer reads a host's active runner unit: the cutover's stage two is to deploy and restart the safe realization on every eligible host, read the active units back, and bind each receipt to the host it was read from" as NonEmptyStr, +} + +fn fleet_standing_from_readback( + source: ActiveUnitReadbackSource, + eligible_hosts: List, +) -> FleetCompileCancellationStanding { + match source { + ReadbackProducerAbsent { cause: _ } => FleetCancellationNotSafe { + unsafe_hosts: [], + unobserved_hosts: eligible_hosts, + } + ReadbackObservations { observations: o } => + fleet_cancellation_standing(eligible_hosts: eligible_hosts, observations: o) + } +} + +data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_standing_from_readback(source: fleet_active_unit_readback, eligible_hosts: fleet_hosts()) From 86c1f16f68d7f6b9a4bc4ba117f2e228e717c799 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 07:26:03 +0000 Subject: [PATCH 13/15] Call the JSON emitter by its declared parameter names The floor caught three call-shape errors in the expected-labels helper I wrote for the complete-file oracle: json_array takes elements not items, json_string takes s not value, and serialize_json takes v not value. I invented those names instead of reading the declaration, and the one place in the corpus that already calls all three -- runner_unit_labels_json, twenty lines from the code I was mirroring -- spells them correctly. Worth stating because it is the same shape as the parse errors earlier in this PR: every one was a construct I assumed rather than checked, in a language whose corpus was open in front of me. I have now verified the remaining fifteen constructors and four helpers in that oracle against their declarations rather than pushing and finding out. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- .../claim/runner/runner_unit_file_witness_test.dag | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index 198b7986388..4582bcb10c2 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -358,11 +358,11 @@ fn expected_live_unit_file(fifo_path: String, daemon_service: NonEmptyStr) -> Sy } fn expected_labels_json() -> String { - serialize_json(value: json_array(items: [ - json_string(value: "self-hosted"), - json_string(value: "linux"), - json_string(value: "arm64"), - json_string(value: "srv1"), + serialize_json(v: json_array(elements: [ + json_string(s: "self-hosted"), + json_string(s: "linux"), + json_string(s: "arm64"), + json_string(s: "srv1"), ])) } From a92f2259e64037ddfb6ef41b18ff58851b734188 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 08:30:13 +0000 Subject: [PATCH 14/15] Take production's route to SAFE away entirely, and hoist the reclamation arm to where its RED is authorable MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two merge blockers from the side chat's read of #9994, both fail-open in the same direction — a claim the code did not have. The producer boundary was an authored row. ActiveUnitReadbackSource wrapped the observation list in two arms and its live row was ReadbackProducerAbsent, with an annotation saying reaching SAFE would require implementing the observed arm. False: ReadbackObservations was an ordinary constructor, so a source edit could supply a roster-covering observation list and the fold would answer SAFE with no host read, no command, no captured output and no receipt. Wrapping an author-constructible value in a coproduct does not change its provenance. The live binding now calls producer_absent_standing, a function with NO safe arm. Fixtures keep the full fold, because 4b requires the discriminating RED and its positive control to be authorable as source handed to the compiler by a fixture. CapacityPreservedByServerReclamation was unexecuted vocabulary. Review 58515 mutated only that arm to classify its host UNSAFE and every witness still passed: no realization maps to that disposition, so the ordinary path never produces one, and the arm sat inside the fold's lambda where no fixture could address it. It is half of the drop's dissolve-on and must not be deleted, so the classification and the identity join become the production helpers accumulate_observed_disposition and finalize_fleet_standing, and two witnesses drive that arm through those same procedures — a positive control reaching restored supersession, and a losing-host red so the positive one cannot be satisfied by a helper that calls everything safe. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/gunbc/compile_permit_scope.dag | 160 ++++++++++-------- .../claim/run_disposition_witness_test.dag | 62 ++++++- 2 files changed, 146 insertions(+), 76 deletions(-) diff --git a/dag/gunbc/compile_permit_scope.dag b/dag/gunbc/compile_permit_scope.dag index f08daf1602f..586826a39d7 100644 --- a/dag/gunbc/compile_permit_scope.dag +++ b/dag/gunbc/compile_permit_scope.dag @@ -110,44 +110,46 @@ type FleetCancellationFoldAcc { // coproduct's variants only to collapse them to true/false, which is the predicate-dissolution // trigger; the fold matches the three arms directly, and a fourth disposition would refuse to // compile here rather than silently falling to one side. -fn fleet_cancellation_standing( +// THE THREE-ARM CLASSIFICATION IS A PRODUCTION HELPER, so a fixture can drive an arm the ordinary +// path cannot yet reach. Review 58515 mutated only the CapacityPreservedByServerReclamation arm to +// classify its host as UNSAFE and every witness still passed: no realization maps to that +// disposition, so borrower_death_capacity_disposition never produces it and the arm was unexecuted +// vocabulary sitting inside the fold's lambda where no test could address it. An arm whose +// discriminating RED is unauthorable is a decoration, and DESIGN 4b says to ask that question before +// writing the check -- so the arm is not deleted (it is half of the drop's dissolve-on) but hoisted +// to where the RED is authorable, which is the same repair the ladder names. +fn accumulate_observed_disposition( + acc: FleetCancellationFoldAcc, + host: HostIdentity, + disposition: BorrowerDeathCapacityDisposition, +) -> FleetCancellationFoldAcc { + match disposition { + CapacityLostUntilPoolRestart => FleetCancellationFoldAcc { + unsafe_hosts: concat(acc.unsafe_hosts, [host]), + unobserved_hosts: acc.unobserved_hosts, + safe_hosts: acc.safe_hosts, + } + CapacityPreservedByInvocationLifetime => FleetCancellationFoldAcc { + unsafe_hosts: acc.unsafe_hosts, + unobserved_hosts: acc.unobserved_hosts, + safe_hosts: concat(acc.safe_hosts, [host]), + } + CapacityPreservedByServerReclamation => FleetCancellationFoldAcc { + unsafe_hosts: acc.unsafe_hosts, + unobserved_hosts: acc.unobserved_hosts, + safe_hosts: concat(acc.safe_hosts, [host]), + } + } +} + +// THE IDENTITY JOIN IS ALSO REACHABLE ON ITS OWN, for the same reason: a fixture that drives a +// disposition through the helper above must be able to carry it all the way to a fleet standing and +// then to the workflow's running axis, or it has established a classification and not a consequence. +// Both callers below run this same procedure -- there is no second finalization. +fn finalize_fleet_standing( + acc: FleetCancellationFoldAcc, eligible_hosts: List, - observations: List, ) -> FleetCompileCancellationStanding { - let acc = fold( - observations, - init: FleetCancellationFoldAcc { unsafe_hosts: [], unobserved_hosts: [], safe_hosts: [] }, - f: (a, o) => match o { - HostCancellationObserved { host: h, realization: r } => - match borrower_death_capacity_disposition(realization: r) { - CapacityLostUntilPoolRestart => FleetCancellationFoldAcc { - unsafe_hosts: concat(a.unsafe_hosts, [h]), - unobserved_hosts: a.unobserved_hosts, - safe_hosts: a.safe_hosts, - } - CapacityPreservedByInvocationLifetime => FleetCancellationFoldAcc { - unsafe_hosts: a.unsafe_hosts, - unobserved_hosts: a.unobserved_hosts, - safe_hosts: concat(a.safe_hosts, [h]), - } - CapacityPreservedByServerReclamation => FleetCancellationFoldAcc { - unsafe_hosts: a.unsafe_hosts, - unobserved_hosts: a.unobserved_hosts, - safe_hosts: concat(a.safe_hosts, [h]), - } - } - HostCancellationUnreadable { host: h, cause: _ } => FleetCancellationFoldAcc { - unsafe_hosts: concat(a.unsafe_hosts, [h]), - unobserved_hosts: a.unobserved_hosts, - safe_hosts: a.safe_hosts, - } - HostCancellationUnobserved { host: h, cause: _ } => FleetCancellationFoldAcc { - unsafe_hosts: a.unsafe_hosts, - unobserved_hosts: concat(a.unobserved_hosts, [h]), - safe_hosts: a.safe_hosts, - } - }, - ) let safe_names = map(acc.safe_hosts, h => h as String) let missing = fold( eligible_hosts, @@ -174,6 +176,31 @@ fn fleet_cancellation_standing( } } +fn fleet_cancellation_standing( + eligible_hosts: List, + observations: List, +) -> FleetCompileCancellationStanding { + let acc = fold( + observations, + init: FleetCancellationFoldAcc { unsafe_hosts: [], unobserved_hosts: [], safe_hosts: [] }, + f: (a, o) => match o { + HostCancellationObserved { host: h, realization: r } => + accumulate_observed_disposition(acc: a, host: h, disposition: borrower_death_capacity_disposition(realization: r)) + HostCancellationUnreadable { host: h, cause: _ } => FleetCancellationFoldAcc { + unsafe_hosts: concat(a.unsafe_hosts, [h]), + unobserved_hosts: a.unobserved_hosts, + safe_hosts: a.safe_hosts, + } + HostCancellationUnobserved { host: h, cause: _ } => FleetCancellationFoldAcc { + unsafe_hosts: a.unsafe_hosts, + unobserved_hosts: concat(a.unobserved_hosts, [h]), + safe_hosts: a.safe_hosts, + } + }, + ) + finalize_fleet_standing(acc: acc, eligible_hosts: eligible_hosts) +} + // THE DENOMINATOR IS THE FLEET'S OWN ROSTER, read from gunbc.fleet_runner_connectivity fleet_hosts // rather than re-minted here. Review 58495 caught the second authoring, and its concrete // consequence is that this construction would have defeated itself: a fifth host joining the fleet @@ -181,46 +208,29 @@ fn fleet_cancellation_standing( // leaks a permit per kill -- the exact denominator failure the parameter was added to prevent, // reintroduced one layer up. // -// PRODUCTION READS A PRODUCER, NOT AN AUTHORED LIST, and that distinction is the whole of review -// 58515's finding. HostCancellationObserved carries a realization an author supplies, so if the live -// standing were a data row of observations then inserting InvocationLocalCargo constructors would -// enable supersession with no host having converged -- satisfiable by editing the declaration while -// the realization lies, which is exactly the validation tell DESIGN section 5 names. +// PRODUCTION HAS NO ROUTE TO SAFE AT ALL, which is stronger than routing one through a named arm. // -// No in-repo type can stop a fixture constructing an observation, and it must not: section 4b -// requires the discriminating RED to be authorable as source handed to the compiler by a fixture, -// which is what every witness on this fold is. What the model CAN do is refuse to let production -// reach the safe arm through authorship, and that is what the boundary below does. The eligible -// hosts are unobserved because no producer reads them, and there is no data row an author can -// extend to change that answer -- reaching SAFE requires implementing ReadbackObservations, which -// means writing the host read. The cause is carried on the source row rather than in the refusal, -// because FleetCancellationNotSafe reports rosters; a reader asking WHY every host is unobserved is -// one hop away, at fleet_active_unit_readback. +// An earlier revision wrapped the observation list in an ActiveUnitReadbackSource coproduct whose +// live row was ReadbackProducerAbsent, and annotated that reaching SAFE would require implementing +// the observed arm. That annotation was false: ReadbackObservations was an ordinary constructor, so +// a source edit could supply an authored observation list covering fleet_hosts() and the fold would +// return SAFE with no host read, no command, no captured output and no receipt. Wrapping an +// author-constructible value in a two-arm source does not change its provenance, and the type's name +// establishes nothing -- the third time in this PR that an annotation claimed a property the code +// did not have. // -// This is the column DESIGN 4b keeps deliberately OFF the ladder: external reality, observed or -// refused at a declared boundary, never fabricated. The boundary is declared here rather than -// implied by an empty list, because an empty list reads as "we looked and found nothing" while the -// truth is "nothing has looked". -type ActiveUnitReadbackSource - = ReadbackProducerAbsent { cause: NonEmptyStr } - | ReadbackObservations { observations: List } - -data fleet_active_unit_readback: ActiveUnitReadbackSource = ReadbackProducerAbsent { - cause: "no producer reads a host's active runner unit: the cutover's stage two is to deploy and restart the safe realization on every eligible host, read the active units back, and bind each receipt to the host it was read from" as NonEmptyStr, -} - -fn fleet_standing_from_readback( - source: ActiveUnitReadbackSource, - eligible_hosts: List, -) -> FleetCompileCancellationStanding { - match source { - ReadbackProducerAbsent { cause: _ } => FleetCancellationNotSafe { - unsafe_hosts: [], - unobserved_hosts: eligible_hosts, - } - ReadbackObservations { observations: o } => - fleet_cancellation_standing(eligible_hosts: eligible_hosts, observations: o) - } +// So the production binding calls a function with no safe arm. Fixtures keep the full fold, because +// section 4b requires the discriminating RED and its positive control to be authorable as source +// handed to the compiler by a fixture; the restriction belongs on the production path alone. The +// stage-two PR that adds a real observer adds it together with its observed output, in the shape +// gunbc.host_hygiene_reaper_observe already uses for typed systemctl and filesystem reads. +// +// A note the eventual boundary owes: an active-unit readback alone cannot establish server +// reclamation, because reclaim-on-client-death is a property of the pool's behaviour rather than of +// the runner unit's environment. The observation boundary is borrower-death capacity evidence, of +// which unit text is one source. +fn producer_absent_standing(eligible_hosts: List) -> FleetCompileCancellationStanding { + FleetCancellationNotSafe { unsafe_hosts: [], unobserved_hosts: eligible_hosts } } -data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = fleet_standing_from_readback(source: fleet_active_unit_readback, eligible_hosts: fleet_hosts()) +data fleet_compile_cancellation_standing: FleetCompileCancellationStanding = producer_absent_standing(eligible_hosts: fleet_hosts()) diff --git a/dag/test/claim/run_disposition_witness_test.dag b/dag/test/claim/run_disposition_witness_test.dag index 3d7afc666c0..44c7c028283 100644 --- a/dag/test/claim/run_disposition_witness_test.dag +++ b/dag/test/claim/run_disposition_witness_test.dag @@ -22,7 +22,12 @@ import gunbc.compile_permit_scope { BorrowerHeldCooperativeHostFifo, InvocationLocalCargo, fleet_cancellation_standing, - fleet_compile_cancellation_standing + fleet_compile_cancellation_standing, + FleetCancellationFoldAcc, + CapacityPreservedByServerReclamation, + CapacityLostUntilPoolRestart, + accumulate_observed_disposition, + finalize_fleet_standing } import gunbc.witness_floor_workflow { running_supersession_for_fleet_standing, @@ -713,3 +718,58 @@ test fn w_an_observation_outside_the_roster_does_not_complete_it() -> Bool { SupersedeRunningForEvent { event: _ } => false } } + + +// ── The reclamation arm, reached where its RED is authorable ──────────────────────────────────── + +// EVERY WITNESS ABOVE PASSES IF THE RECLAMATION ARM IS MUTATED TO CLASSIFY ITS HOST AS UNSAFE. +// Review 58515 ran exactly that mutation and nothing went red, because no realization maps to +// CapacityPreservedByServerReclamation, so the ordinary path never produces one and the arm sat +// inside the fold's lambda where no fixture could address it. The arm is half of the drop's +// dissolve-on and must not be deleted; what has to change is the production shape, so the two +// witnesses here call the SAME production procedures the fold calls -- there is no second +// classification and no second finalization for a fixture to agree with vacuously. +fn reclaiming_fleet_acc() -> FleetCancellationFoldAcc { + accumulate_observed_disposition( + acc: accumulate_observed_disposition( + acc: FleetCancellationFoldAcc { unsafe_hosts: [], unobserved_hosts: [], safe_hosts: [] }, + host: "srv1" as HostIdentity, + disposition: CapacityPreservedByServerReclamation, + ), + host: "srv2" as HostIdentity, + disposition: CapacityPreservedByServerReclamation, + ) +} + +// THE POSITIVE CONTROL: a fleet whose every host preserves capacity by SERVER RECLAMATION carries +// all the way to restored supersession. Flip that arm to the unsafe side and this goes red. +test fn w_a_server_reclaiming_fleet_restores_supersession() -> Bool { + match running_supersession_for_fleet_standing( + standing: finalize_fleet_standing(acc: reclaiming_fleet_acc(), eligible_hosts: two_host_fleet()), + ) { + SupersedeRunningForEvent { event: e } => e == "pull_request" + NeverSupersedeRunning => false + } +} + +// AND THE DISCRIMINATING RED FOR THE SAME HELPER: one losing host among reclaiming ones holds the +// containment, so the witness above cannot be satisfied by a helper that classifies everything safe. +test fn w_one_losing_host_among_reclaiming_hosts_holds_the_containment() -> Bool { + match running_supersession_for_fleet_standing( + standing: finalize_fleet_standing( + acc: accumulate_observed_disposition( + acc: accumulate_observed_disposition( + acc: FleetCancellationFoldAcc { unsafe_hosts: [], unobserved_hosts: [], safe_hosts: [] }, + host: "srv1" as HostIdentity, + disposition: CapacityPreservedByServerReclamation, + ), + host: "srv2" as HostIdentity, + disposition: CapacityLostUntilPoolRestart, + ), + eligible_hosts: two_host_fleet(), + ), + ) { + NeverSupersedeRunning => true + SupersedeRunningForEvent { event: _ } => false + } +} From 2456e92aa17a4d72c6b0a51920ae864f0989cd51 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 2 Sep 2026 11:52:12 +0000 Subject: [PATCH 15/15] Separate a run-on closing brace from the test fn that followed it Review 58660, cosmetic. invocation_local_text's closing brace and the next test fn shared a line. It tokenizes, but nothing else in the file is written that way. Worth recording how the finding was cited: it named runner_unit_file_witness_test.dag:827-828 in a 458-line file. The position was wrong and the symbols -- invocation_local_text and w_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies -- were right, which is the positional-citation decay DESIGN section 3 names, arriving inside a review of a PR about exactly this kind of authority drift. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01UE62aajYJsXgn4udvrJAVh --- dag/test/claim/runner/runner_unit_file_witness_test.dag | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/dag/test/claim/runner/runner_unit_file_witness_test.dag b/dag/test/claim/runner/runner_unit_file_witness_test.dag index 4582bcb10c2..9701756c988 100644 --- a/dag/test/claim/runner/runner_unit_file_witness_test.dag +++ b/dag/test/claim/runner/runner_unit_file_witness_test.dag @@ -262,7 +262,9 @@ fn invocation_local_text() -> String { RunnerUnitText { text: t } => t RunnerUnitTextRefused { reason: _ } => "" } -}test fn w_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies() -> Bool { +} + +test fn w_a_cooperative_host_fifo_loses_capacity_when_its_borrower_dies() -> Bool { match borrower_death_capacity_disposition(realization: live_realization()) { CapacityLostUntilPoolRestart => true CapacityPreservedByInvocationLifetime => false