From 561fa4a89ef320c02a16f7dc0833151c5dd25ce7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 06:23:39 +0000 Subject: [PATCH 01/17] WIP: srvN subsumption --- dag/gunbc/host_build_cache_provision_script.dag | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/dag/gunbc/host_build_cache_provision_script.dag b/dag/gunbc/host_build_cache_provision_script.dag index 79730a6be79..fe23d2c5138 100644 --- a/dag/gunbc/host_build_cache_provision_script.dag +++ b/dag/gunbc/host_build_cache_provision_script.dag @@ -37,7 +37,9 @@ fn build_cache_systemd_user_unit_body() -> String { "", "[Service]", "Type=simple", - join(["ExecStart=", sccache_installed_binary_path, " --start-server"], ""), + "Environment=SCCACHE_START_SERVER=1", + "Environment=SCCACHE_NO_DAEMON=1", + join(["ExecStart=", sccache_installed_binary_path], ""), "Restart=on-failure", "", "[Install]", @@ -177,6 +179,16 @@ fn build_cache_unit_execstart_matches_install_path() -> Bool { ) } +data build_cache_unit_foreground_supervision_note: String = "The unit is Type=simple, so systemd tracks the ExecStart process AS the service — it MUST stay in the foreground. `sccache --start-server` DAEMONIZES and returns 0, so under Type=simple systemd sees the ExecStart exit cleanly and marks the unit `inactive (dead)` the instant it starts; the backgrounded server then idle-times-out unsupervised and Restart=on-failure never fires (the exit was success). Proven live on srv3 2026-07-25: the earlier `--start-server` form left the unit inactive with no sccache process, the daemon surviving only via sccache's own per-invocation auto-start — i.e. the unit was a no-op. This is the §5 specification-without-execution trap: the string witness that ExecStart equals the install path was green while the unit did nothing. The foreground form matches the production ctrl-sccache.service invocation (bare ExecStart + SCCACHE_START_SERVER=1 SCCACHE_NO_DAEMON=1 env, verified running month+ on srv1/srv2), reducing the §3 fork between the modeled unit and production rather than inventing a third shape. build_cache_unit_is_foreground_supervised makes the defective combo (Type=simple paired with a backgrounding --start-server) UNWRITABLE; the runtime is-active proof is the live srv3 re-provision (systemd --user is not runnable in the hermetic CI container, so the construction wall carries the CI grain and live execution carries the runtime grain)." + +fn build_cache_unit_is_foreground_supervised() -> Bool { + let body = build_cache_systemd_user_unit_body() + string_contains(s: body, pattern: "Type=simple") + && string_contains(s: body, pattern: "SCCACHE_START_SERVER=1") + && string_contains(s: body, pattern: "SCCACHE_NO_DAEMON=1") + && !string_contains(s: body, pattern: "--start-server") +} + fn build_cache_classifier_covers_every_cited_fragment() -> Bool { fold( sccache_misconfigured_log_fragments, From 73ff9964f516b1c7bae36d345d810a56258f1507 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 06:28:29 +0000 Subject: [PATCH 02/17] sccache unit: foreground-supervise the daemon (Type=simple + --start-server was a no-op) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up to #7170. Live execution on srv3 caught what the string witnesses missed (§5 specification-without-execution): the modeled unit was Type=simple ExecStart=/usr/local/bin/sccache --start-server # daemonizes, exits 0 so systemd saw the ExecStart exit cleanly and marked the unit `inactive (dead)` the instant it started; the backgrounded server idle-timed-out unsupervised and Restart=on-failure never fired (success exit). The unit was a no-op — sccache survived only via its own per-invocation auto-start. The string witness "ExecStart equals the install path" was green the whole time. Fix (grounded by execution on srv3 first): foreground the server, matching the production ctrl-sccache.service invocation verified running month+ on srv1/srv2: Type=simple Environment=SCCACHE_START_SERVER=1 Environment=SCCACHE_NO_DAEMON=1 ExecStart=/usr/local/bin/sccache This reduces the §3 fork between the modeled unit and production rather than minting a third shape. Closes the execution gap two ways: build_cache_unit_is_foreground_supervised is a construction check that makes the defective combo (Type=simple paired with a backgrounding --start-server) UNWRITABLE (carries the CI grain, since systemd --user is not runnable in the hermetic container), and the live srv3 re-provision carries the runtime is-active grain. Census note accounts the +1-line delta as a correctness swap toward the cited production authority. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/gunbc/host_build_cache_provision_script.dag | 2 +- .../claim/host_build_cache_provision_design_witness_test.dag | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/dag/gunbc/host_build_cache_provision_script.dag b/dag/gunbc/host_build_cache_provision_script.dag index fe23d2c5138..c51c09ba063 100644 --- a/dag/gunbc/host_build_cache_provision_script.dag +++ b/dag/gunbc/host_build_cache_provision_script.dag @@ -14,7 +14,7 @@ import extdeps.cache.sccache { data host_build_cache_provision_script_dissolution_trigger: String = "🟡 dissolve-on: host_build_cache_provision_script — concat-built systemd/sccache ensure shell; DISSOLVES WHEN bash-emit (#5828) realizes ProvisionBuildCache observe/ensure/read-back as typed host-effect argv and realize_provision_build_cache retires shell_exec_via_bash transport." -data host_build_cache_provision_script_census_row_note: String = "CENSUS STANDING: docs/plans/shell-to-dag-residual-census-and-arc-completion.md §4.A keys this file as the builder for host_effect_realize.ProvisionBuildCache, action DECOMPOSE, sub-class A5 (srv* cluster, deferred by operator 2026-07-22 — real debt, NOT done; un-defer trigger is the operator). This site is RUNTIME-PRESENT (it realizes through host_effect_apply_gated on LocalShell/SshShell), so per that doc's routing decision its end state is a typed effect-plan with NO bash emitted — the six *_body builders below are the debt, not the design. Standing constraint while the row is deferred, stated precisely (review 42401 sharpened this): NEW emitted shell must be either a DEDUCTION or a cited-de-fork SWAP — never an unbounded, uncited addition. Two exact deltas this PR made, both accounted: (1) the sccache DE-FORK swap — `apt-get install sccache` + an `ExecStart=/usr/bin/sccache` unit went OUT, and the cited-tarball install invocation (sccache_install_script, one authority row) came IN; that is the §3 fork removal this PR exists to make, a swap that de-duplicates rather than grows. (2) `sudo -n loginctl enable-linger \"$USER\"` is genuinely NEW shell, not a swap — acknowledged here as growth rather than hidden: it is the one primitive that makes the already-selected user-scope systemd handler viable at all (a `--user` manager is torn down with the login otherwise), justified in build_cache_user_service_linger_note, and it is bounded (a single fixed leaf, not a corpus-denominated fold). What must NOT grow is the PATH-shadow OBSERVATION: the judgement went to gunbc.host_build_cache_provision (DaemonPathShadowed / RefusalPathShadowed + verdict fold, witnessed against a synthetic observation), and its live shell observation is STAGED, NOT emitted here — an earlier attempt folded `command -v sccache` lines into the two existing bodies, which kept the builder count at six but still grew the shell surface (review 42343 rejected that as a census regression). The observation lands when ProvisionBuildCache realizes as typed argv (dissolve-on #5828). Adding a *_body, or an uncited emitted-shell leaf that is neither a deduction nor a de-fork swap, is a census regression even when the behaviour it adds is correct." +data host_build_cache_provision_script_census_row_note: String = "CENSUS STANDING: docs/plans/shell-to-dag-residual-census-and-arc-completion.md §4.A keys this file as the builder for host_effect_realize.ProvisionBuildCache, action DECOMPOSE, sub-class A5 (srv* cluster, deferred by operator 2026-07-22 — real debt, NOT done; un-defer trigger is the operator). This site is RUNTIME-PRESENT (it realizes through host_effect_apply_gated on LocalShell/SshShell), so per that doc's routing decision its end state is a typed effect-plan with NO bash emitted — the six *_body builders below are the debt, not the design. Standing constraint while the row is deferred, stated precisely (review 42401 sharpened this): NEW emitted shell must be either a DEDUCTION or a cited-de-fork SWAP — never an unbounded, uncited addition. Two exact deltas this PR made, both accounted: (1) the sccache DE-FORK swap — `apt-get install sccache` + an `ExecStart=/usr/bin/sccache` unit went OUT, and the cited-tarball install invocation (sccache_install_script, one authority row) came IN; that is the §3 fork removal this PR exists to make, a swap that de-duplicates rather than grows. (2) `sudo -n loginctl enable-linger \"$USER\"` is genuinely NEW shell, not a swap — acknowledged here as growth rather than hidden: it is the one primitive that makes the already-selected user-scope systemd handler viable at all (a `--user` manager is torn down with the login otherwise), justified in build_cache_user_service_linger_note, and it is bounded (a single fixed leaf, not a corpus-denominated fold). What must NOT grow is the PATH-shadow OBSERVATION: the judgement went to gunbc.host_build_cache_provision (DaemonPathShadowed / RefusalPathShadowed + verdict fold, witnessed against a synthetic observation), and its live shell observation is STAGED, NOT emitted here — an earlier attempt folded `command -v sccache` lines into the two existing bodies, which kept the builder count at six but still grew the shell surface (review 42343 rejected that as a census regression). The observation lands when ProvisionBuildCache realizes as typed argv (dissolve-on #5828). Adding a *_body, or an uncited emitted-shell leaf that is neither a deduction nor a de-fork swap, is a census regression even when the behaviour it adds is correct. FOLLOW-UP #7206 delta (correctness swap, accounted): the unit's `ExecStart=... --start-server` became bare `ExecStart=...` + two `Environment=` lines (SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1) — net +1 line, and NOT uncited growth: it is a swap toward the production ctrl-sccache.service invocation (the single authority the whole lane converges on), replacing a form live execution on srv3 proved is a Type=simple no-op (build_cache_unit_foreground_supervision_note). A correctness swap toward the cited production authority is the sanctioned shape, exactly like delta (1)." data host_build_cache_provision_script_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority, diff --git a/dag/test/claim/host_build_cache_provision_design_witness_test.dag b/dag/test/claim/host_build_cache_provision_design_witness_test.dag index 609663314d8..335c8abccb3 100644 --- a/dag/test/claim/host_build_cache_provision_design_witness_test.dag +++ b/dag/test/claim/host_build_cache_provision_design_witness_test.dag @@ -168,6 +168,10 @@ fn design_witness_unit_execstart_matches_install_path() -> Bool { build_cache_unit_execstart_matches_install_path() } +fn design_witness_unit_is_foreground_supervised() -> Bool { + build_cache_unit_is_foreground_supervised() +} + fn design_witness_classifier_covers_every_cited_fragment() -> Bool { build_cache_classifier_covers_every_cited_fragment() } @@ -241,6 +245,7 @@ test fn host_build_cache_provision_design_witnesses() -> Bool { && design_witness_path_authority_observation_not_emitted_as_shell() && design_witness_install_is_cited_not_package_manager() && design_witness_unit_execstart_matches_install_path() + && design_witness_unit_is_foreground_supervised() && design_witness_classifier_covers_every_cited_fragment() && design_witness_classifier_is_a_fold_not_an_unrolled_chain() && design_witness_fragment_words_are_shell_safe() From 955fe9d2af5f40812bf3a643d537e08e245e602c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 13:01:22 +0000 Subject: [PATCH 03/17] WIP: srvN subsumption --- dag/extdeps/cache/sccache.dag | 24 ++++++ dag/gunbc/host_build_cache_provision.dag | 26 ++++++ .../host_build_cache_provision_script.dag | 23 ++++-- ...ld_cache_provision_design_witness_test.dag | 82 +++++++++++++++++++ 4 files changed, 150 insertions(+), 5 deletions(-) diff --git a/dag/extdeps/cache/sccache.dag b/dag/extdeps/cache/sccache.dag index abca5a5c62c..0334444934a 100644 --- a/dag/extdeps/cache/sccache.dag +++ b/dag/extdeps/cache/sccache.dag @@ -150,6 +150,30 @@ data sccache_misconfigured_log_fragments: List = [ sccache_failed_to_execute_compile_log_fragment, ] +data sccache_server_lifetime_note: String = "sccache's server EXITS ON ITS OWN. Three environment knobs, all documented by the module's cited authority extdeps_external_authority_anchor (github.com/mozilla/sccache/blob/main/docs/Configuration.md), decide the process lifetime a supervisor sees, and they are modeled here because they are facts about SCCACHE — not about systemd, and not about gunbc. Before 2026-07-25 the P1b unit emitter spelled SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1 as bare literals of its own, which made gunbc.host_build_cache_provision_script a SECOND authority for sccache's environment vocabulary (§3) — and the knob that was missing from that second authority is exactly the one that broke: SCCACHE_IDLE_TIMEOUT. Cited text: 'how long the local daemon process waits for more client requests before exiting, in seconds. Set to 0 to run sccache permanently.' The default is 600 seconds, confirmed by execution rather than read off the doc: on srv3 2026-07-25 the foreground-supervised unit started at 06:28:47 UTC, served no compile request, and EXITED 0 after `Duration: 10min 8.215s`, leaving `inactive (dead)` — Restart=on-failure could not fire because the exit was a success. Consequence for any supervisor: a Type=simple unit whose ExecStart is sccache is only durable when the idle timeout is disabled; otherwise it dies on the first quiet ten minutes and the host reverts to sccache's own unsupervised per-invocation auto-start (the very no-op state the foreground form was introduced to remove). The srv1/srv2 production ctrl-sccache.service does not set this knob either — its month-plus uptime is CI traffic keeping the daemon below the idle threshold, i.e. accidental coverage, not a durable unit; that is a fact about the observed hosts, so this row is a DEDUCTION from the cited doc and the srv3 receipt, not a swap toward production." + +data sccache_start_server_env_var: String = "SCCACHE_START_SERVER" + +data sccache_no_daemon_env_var: String = "SCCACHE_NO_DAEMON" + +data sccache_idle_timeout_env_var: String = "SCCACHE_IDLE_TIMEOUT" + +data sccache_idle_timeout_never_value_note: String = "The value whose MEANING is 'never exit', which is why it is a named row rather than a literal inside the assignment: '0' is not an ordinary duration on this axis (a zero-second idle timeout would mean the opposite), it is the cited doc's sentinel for running permanently. A future consumer that wants a bounded lifetime supplies its own seconds value; a consumer that wants a supervised daemon reads THIS row." + +data sccache_idle_timeout_never_value: String = "0" + +fn sccache_start_server_env_assignment() -> String { + join([sccache_start_server_env_var, "=1"], "") +} + +fn sccache_no_daemon_env_assignment() -> String { + join([sccache_no_daemon_env_var, "=1"], "") +} + +fn sccache_idle_timeout_never_env_assignment() -> String { + join([sccache_idle_timeout_env_var, "=", sccache_idle_timeout_never_value], "") +} + data sccache_local_facts: CacheInterfaceCatalogFacts = { identity: sccache_local_id backing_surface: "sccache-local-disk" diff --git a/dag/gunbc/host_build_cache_provision.dag b/dag/gunbc/host_build_cache_provision.dag index aace34c4402..9e80c7bf5b3 100644 --- a/dag/gunbc/host_build_cache_provision.dag +++ b/dag/gunbc/host_build_cache_provision.dag @@ -39,12 +39,15 @@ data ci_sccache_opportunistic_detect_scaffold: Disposition = Scaffold { } data build_cache_path_authority_observation_note: String = "CI and ctrl-build sessions consume the cache as bare `sccache` on PATH (RUSTC_WRAPPER=sccache), so provisioning the modeled binary is NOT sufficient — the PATH-visible sccache must BE the modeled one. A second sccache earlier in PATH (a distro package, a stale copy) is precisely the two-authority state this lane exists to remove, and it is invisible to a read-back that probes the absolute path: that read-back greens on the binary we provisioned while the compiler calls a different one. DaemonPathShadowed carries BOTH paths so the refusal is located (which binary won, which one was expected) rather than merely typed. This judgement is modeled HERE, in the verdict fold (proven by design_witness_path_shadow_refuses_fail_closed against a synthetic DaemonPathShadowed observation), not decided by the provisioning shell. Its LIVE observation is STAGED, not emitted: per the shell→dag census this module's script side is an A5 `decompose` row that must not grow its emitted shell surface, so the `command -v sccache` resolve waits for the typed-argv dissolve-on (#5828) rather than landing as hand-shell now (review 42343). The model carries the state and its refusal today; only the live producer is deferred." +data build_cache_supervision_observation_note: String = "A stats read-back CANNOT see whether the daemon it just talked to is supervised — and this is not a gap in the probe, it is the probe's semantics: any sccache invocation AUTO-STARTS a server if none is listening, so `--show-stats` manufactures the very evidence it reports. On srv3 2026-07-25 it printed a full stats table while the modeled unit had been `inactive (dead)` for six hours and no sccache process existed beforehand. Read through the verdict fold as it stood, that host observed DaemonStatsOk and therefore converged: the provisioning act would have reported success over a host with NO durable cache — a fabricated plausible output (§5), and the same shape as DaemonPathShadowed (a read-back that greens on evidence it produced rather than on the state the lane exists to establish). DaemonUnsupervised splits that conflation: 'a daemon answered' and 'the modeled supervisor is running it' are different states with different remedies, so they get different names rather than one Ok. The LIVE observation is STAGED exactly as the PATH-shadow one is — the supervisor read (`systemctl --user is-active`) is not emitted as hand-shell here, because this module's script side is an A5 `decompose` census row that may shrink but must not grow (review 42343); it lands with the typed-argv dissolve-on (#5828). The model carries the state and its refusal today; only the live producer is deferred. Construction covers the case this observation would catch on a host provisioned BY THIS LANE — build_cache_unit_daemon_runs_until_stopped makes the self-exiting unit unwritable — so the observation's standing job is the residue construction cannot reach: a host whose unit was stopped, masked, or replaced out of band." + type BuildCacheDaemonObservation = DaemonStatsOk { stats_line: String } | DaemonAbsent | DaemonUnresponsive { detail: NonEmptyStr } | DaemonMisconfigured { matched_fragment: String, detail: NonEmptyStr } | DaemonPathShadowed { resolved: String, expected: String } + | DaemonUnsupervised { unit: String, unit_state: String } type BuildCacheProvisionRefusal = RefusalDaemonAbsent @@ -53,6 +56,7 @@ type BuildCacheProvisionRefusal | RefusalPrivilegeDenied | RefusalCatalogUnknown | RefusalPathShadowed + | RefusalDaemonUnsupervised type BuildCacheProvisionVerdict = ProvisionConverged { catalog_id: CacheInterfaceId, stats_line: String } @@ -82,6 +86,11 @@ fn provision_build_cache_absorbing_fallback_widen_sketch( catalog_id: catalog_id, stats_line: concat("path-shadow-widen-sketch: ", concat(r, concat(" vs ", e))), } + DaemonUnsupervised { unit: u, unit_state: s } => + ProvisionConverged { + catalog_id: catalog_id, + stats_line: concat("unsupervised-widen-sketch: ", concat(u, concat(" is ", s))), + } } } @@ -118,6 +127,12 @@ fn build_cache_provision_gate_accepts( ProvisionConverged { catalog_id: _, stats_line: _ } => false ProvisionRefused { cause: _, reason: _ } => false } + DaemonUnsupervised { unit: _, unit_state: _ } => + match verdict { + ProvisionRefused { cause: RefusalDaemonUnsupervised, reason: _ } => true + ProvisionConverged { catalog_id: _, stats_line: _ } => false + ProvisionRefused { cause: _, reason: _ } => false + } } } @@ -158,6 +173,17 @@ fn provision_build_cache_verdict( ), ) as NonEmptyStr, } + DaemonUnsupervised { unit: u, unit_state: s } => + ProvisionRefused { + cause: RefusalDaemonUnsupervised, + reason: concat( + concat("host_build_cache_provision: sccache answers but its supervisor unit ", u), + concat( + concat(" is ", s), + "; the daemon is only alive because an invocation auto-started it, so it exits on its own idle timeout and nothing restarts it. Fail-closed, no local-build fallback.", + ), + ) as NonEmptyStr, + } } } } diff --git a/dag/gunbc/host_build_cache_provision_script.dag b/dag/gunbc/host_build_cache_provision_script.dag index c51c09ba063..dee206402d0 100644 --- a/dag/gunbc/host_build_cache_provision_script.dag +++ b/dag/gunbc/host_build_cache_provision_script.dag @@ -10,11 +10,14 @@ import extdeps.cache.sccache { sccache_installed_binary_path, sccache_install_script, sccache_release_0_15_0, + sccache_start_server_env_assignment, + sccache_no_daemon_env_assignment, + sccache_idle_timeout_never_env_assignment, } data host_build_cache_provision_script_dissolution_trigger: String = "🟡 dissolve-on: host_build_cache_provision_script — concat-built systemd/sccache ensure shell; DISSOLVES WHEN bash-emit (#5828) realizes ProvisionBuildCache observe/ensure/read-back as typed host-effect argv and realize_provision_build_cache retires shell_exec_via_bash transport." -data host_build_cache_provision_script_census_row_note: String = "CENSUS STANDING: docs/plans/shell-to-dag-residual-census-and-arc-completion.md §4.A keys this file as the builder for host_effect_realize.ProvisionBuildCache, action DECOMPOSE, sub-class A5 (srv* cluster, deferred by operator 2026-07-22 — real debt, NOT done; un-defer trigger is the operator). This site is RUNTIME-PRESENT (it realizes through host_effect_apply_gated on LocalShell/SshShell), so per that doc's routing decision its end state is a typed effect-plan with NO bash emitted — the six *_body builders below are the debt, not the design. Standing constraint while the row is deferred, stated precisely (review 42401 sharpened this): NEW emitted shell must be either a DEDUCTION or a cited-de-fork SWAP — never an unbounded, uncited addition. Two exact deltas this PR made, both accounted: (1) the sccache DE-FORK swap — `apt-get install sccache` + an `ExecStart=/usr/bin/sccache` unit went OUT, and the cited-tarball install invocation (sccache_install_script, one authority row) came IN; that is the §3 fork removal this PR exists to make, a swap that de-duplicates rather than grows. (2) `sudo -n loginctl enable-linger \"$USER\"` is genuinely NEW shell, not a swap — acknowledged here as growth rather than hidden: it is the one primitive that makes the already-selected user-scope systemd handler viable at all (a `--user` manager is torn down with the login otherwise), justified in build_cache_user_service_linger_note, and it is bounded (a single fixed leaf, not a corpus-denominated fold). What must NOT grow is the PATH-shadow OBSERVATION: the judgement went to gunbc.host_build_cache_provision (DaemonPathShadowed / RefusalPathShadowed + verdict fold, witnessed against a synthetic observation), and its live shell observation is STAGED, NOT emitted here — an earlier attempt folded `command -v sccache` lines into the two existing bodies, which kept the builder count at six but still grew the shell surface (review 42343 rejected that as a census regression). The observation lands when ProvisionBuildCache realizes as typed argv (dissolve-on #5828). Adding a *_body, or an uncited emitted-shell leaf that is neither a deduction nor a de-fork swap, is a census regression even when the behaviour it adds is correct. FOLLOW-UP #7206 delta (correctness swap, accounted): the unit's `ExecStart=... --start-server` became bare `ExecStart=...` + two `Environment=` lines (SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1) — net +1 line, and NOT uncited growth: it is a swap toward the production ctrl-sccache.service invocation (the single authority the whole lane converges on), replacing a form live execution on srv3 proved is a Type=simple no-op (build_cache_unit_foreground_supervision_note). A correctness swap toward the cited production authority is the sanctioned shape, exactly like delta (1)." +data host_build_cache_provision_script_census_row_note: String = "CENSUS STANDING: docs/plans/shell-to-dag-residual-census-and-arc-completion.md §4.A keys this file as the builder for host_effect_realize.ProvisionBuildCache, action DECOMPOSE, sub-class A5 (srv* cluster, deferred by operator 2026-07-22 — real debt, NOT done; un-defer trigger is the operator). This site is RUNTIME-PRESENT (it realizes through host_effect_apply_gated on LocalShell/SshShell), so per that doc's routing decision its end state is a typed effect-plan with NO bash emitted — the six *_body builders below are the debt, not the design. Standing constraint while the row is deferred, stated precisely (review 42401 sharpened this): NEW emitted shell must be either a DEDUCTION or a cited-de-fork SWAP — never an unbounded, uncited addition. Two exact deltas this PR made, both accounted: (1) the sccache DE-FORK swap — `apt-get install sccache` + an `ExecStart=/usr/bin/sccache` unit went OUT, and the cited-tarball install invocation (sccache_install_script, one authority row) came IN; that is the §3 fork removal this PR exists to make, a swap that de-duplicates rather than grows. (2) `sudo -n loginctl enable-linger \"$USER\"` is genuinely NEW shell, not a swap — acknowledged here as growth rather than hidden: it is the one primitive that makes the already-selected user-scope systemd handler viable at all (a `--user` manager is torn down with the login otherwise), justified in build_cache_user_service_linger_note, and it is bounded (a single fixed leaf, not a corpus-denominated fold). What must NOT grow is the PATH-shadow OBSERVATION: the judgement went to gunbc.host_build_cache_provision (DaemonPathShadowed / RefusalPathShadowed + verdict fold, witnessed against a synthetic observation), and its live shell observation is STAGED, NOT emitted here — an earlier attempt folded `command -v sccache` lines into the two existing bodies, which kept the builder count at six but still grew the shell surface (review 42343 rejected that as a census regression). The observation lands when ProvisionBuildCache realizes as typed argv (dissolve-on #5828). Adding a *_body, or an uncited emitted-shell leaf that is neither a deduction nor a de-fork swap, is a census regression even when the behaviour it adds is correct. FOLLOW-UP #7206 delta (correctness swap, accounted): the unit's `ExecStart=... --start-server` became bare `ExecStart=...` + two `Environment=` lines (SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1) — net +1 line, and NOT uncited growth: it is a swap toward the production ctrl-sccache.service invocation (the single authority the whole lane converges on), replacing a form live execution on srv3 proved is a Type=simple no-op (build_cache_unit_foreground_supervision_note). A correctness swap toward the cited production authority is the sanctioned shape, exactly like delta (1). FOLLOW-UP #7 delta (DEDUCTION, accounted): one further `Environment=` line, SCCACHE_IDLE_TIMEOUT=0, net +1 emitted line. This one is NOT a swap toward production — srv1/srv2 do not set the knob either — so it is accounted as the other sanctioned shape, a DEDUCTION: it follows from the cited upstream authority (Configuration.md, extdeps.cache.sccache.sccache_server_lifetime_note) plus the srv3 receipt that the foreground unit exits 0 after 10min 8s idle, and it is the minimal line that makes Type=simple supervision hold at all. It also SHRINKS this file's ownership of vocabulary it does not own: all three Environment values now come from extdeps rows (sccache_start_server_env_assignment / sccache_no_daemon_env_assignment / sccache_idle_timeout_never_env_assignment) instead of bare literals spelled here, so gunbc is no longer a second authority for sccache env var names (§3). The supervision OBSERVATION (`systemctl --user is-active`) is STAGED, not emitted, on exactly the PATH-shadow precedent — the judgement lives in gunbc.host_build_cache_provision (DaemonUnsupervised / RefusalDaemonUnsupervised, witnessed against a synthetic observation) and the live producer waits for typed argv (dissolve-on #5828)." data host_build_cache_provision_script_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority, @@ -37,8 +40,8 @@ fn build_cache_systemd_user_unit_body() -> String { "", "[Service]", "Type=simple", - "Environment=SCCACHE_START_SERVER=1", - "Environment=SCCACHE_NO_DAEMON=1", + join(["Environment=", sccache_start_server_env_assignment()], ""), + join(["Environment=", sccache_no_daemon_env_assignment()], ""), join(["ExecStart=", sccache_installed_binary_path], ""), "Restart=on-failure", "", @@ -184,11 +187,21 @@ data build_cache_unit_foreground_supervision_note: String = "The unit is Type=si fn build_cache_unit_is_foreground_supervised() -> Bool { let body = build_cache_systemd_user_unit_body() string_contains(s: body, pattern: "Type=simple") - && string_contains(s: body, pattern: "SCCACHE_START_SERVER=1") - && string_contains(s: body, pattern: "SCCACHE_NO_DAEMON=1") + && string_contains(s: body, pattern: sccache_start_server_env_assignment()) + && string_contains(s: body, pattern: sccache_no_daemon_env_assignment()) && !string_contains(s: body, pattern: "--start-server") } +data build_cache_unit_daemon_self_exit_note: String = "Foregrounding the server was necessary and NOT sufficient — this is the SAME defect one level deeper, found by the live read-back #7206's own note called for. sccache exits on its own after SCCACHE_IDLE_TIMEOUT seconds of no compile requests (default 600, cited in extdeps.cache.sccache.sccache_server_lifetime_note), so the foreground process under Type=simple terminates with status 0 on the first quiet ten minutes and systemd marks the unit `inactive (dead)`; Restart=on-failure does not fire, because a clean exit is not a failure. Measured on srv3 2026-07-25: `Duration: 10min 8.215s`, `Main PID: 3377939 (code=exited, status=0/SUCCESS)`, no sccache process left. The host then reverts to sccache's own per-invocation auto-start — i.e. back to the unit being a no-op, which is exactly the state the foreground form was introduced to remove. Two notes on the shape of the fix. (1) The fix is the cited env knob, not Restart=always: flipping the restart policy would make a clean exit INVISIBLE by relaunching through it, which is DESIGN §5's absorbing fallback (the arm widens instead of refusing, and the deficit's frequency drops to zero by construction). With the idle timeout disabled, a status-0 exit is unreachable by configuration, so Restart=on-failure is the honest policy and a unit found dead is a real, observable, refusable state. (2) The construction check names each required assignment through its extdeps row INDIVIDUALLY rather than folding a roster: a fold over a shared list would go vacuously green the moment the idle-timeout row were dropped from that list, since the emitter and the check would lose it together — the §5 tell of a check satisfiable by editing the declaration while the realization lies." + +fn build_cache_unit_body_runs_until_stopped(body: String) -> Bool { + string_contains(s: body, pattern: sccache_idle_timeout_never_env_assignment()) +} + +fn build_cache_unit_daemon_runs_until_stopped() -> Bool { + build_cache_unit_body_runs_until_stopped(body: build_cache_systemd_user_unit_body()) +} + fn build_cache_classifier_covers_every_cited_fragment() -> Bool { fold( sccache_misconfigured_log_fragments, diff --git a/dag/test/claim/host_build_cache_provision_design_witness_test.dag b/dag/test/claim/host_build_cache_provision_design_witness_test.dag index 335c8abccb3..bc4fe41a427 100644 --- a/dag/test/claim/host_build_cache_provision_design_witness_test.dag +++ b/dag/test/claim/host_build_cache_provision_design_witness_test.dag @@ -172,6 +172,84 @@ fn design_witness_unit_is_foreground_supervised() -> Bool { build_cache_unit_is_foreground_supervised() } +data unit_self_exiting_sketch_note: String = "RED-control fixture: the unit body EXACTLY as #7206 shipped it — foreground-supervised, and still self-exiting because sccache's default 600s idle timeout is left in place. It is a fixture, never emitted (the authority body is build_cache_systemd_user_unit_body), and it is what makes design_witness_unit_daemon_runs_until_stopped discriminating rather than tautological: the predicate is parameterized over a body, the authority body passes it, and this sketch — the shape live execution on srv3 proved dies after `Duration: 10min 8.215s` with status 0 — fails it. Without the sketch the witness would only assert that a string the same module wrote is present in the string it wrote." + +fn unit_self_exiting_sketch_body() -> String { + join([ + "[Unit]", + "Description=sccache compiler cache (gunbc host standup)", + "After=network.target", + "", + "[Service]", + "Type=simple", + "Environment=SCCACHE_START_SERVER=1", + "Environment=SCCACHE_NO_DAEMON=1", + join(["ExecStart=", sccache_installed_binary_path], ""), + "Restart=on-failure", + "", + "[Install]", + "WantedBy=default.target", + "", + ], "\n") +} + +fn design_witness_unit_daemon_runs_until_stopped() -> Bool { + build_cache_unit_daemon_runs_until_stopped() + && !build_cache_unit_body_runs_until_stopped(body: unit_self_exiting_sketch_body()) + && build_cache_unit_body_runs_until_stopped(body: build_cache_systemd_user_unit_body()) +} + +fn unsupervised_observation_fixture() -> BuildCacheDaemonObservation { + DaemonUnsupervised { unit: "sccache.service", unit_state: "inactive (dead)" } +} + +fn design_witness_unsupervised_refuses_fail_closed() -> Bool { + match provision_build_cache_verdict( + catalog_id: sccache_local_id, + observed: unsupervised_observation_fixture(), + ) { + ProvisionRefused { cause: RefusalDaemonUnsupervised, reason: reason } => + string_contains(s: reason as String, pattern: "sccache.service") + && string_contains(s: reason as String, pattern: "inactive (dead)") + && string_contains(s: reason as String, pattern: "Fail-closed") + ProvisionRefused { cause: _, reason: _ } => false + ProvisionConverged { catalog_id: _, stats_line: _ } => false + } +} + +fn design_witness_red_control_widen_on_unsupervised_rejected_by_gate() -> Bool { + match provision_build_cache_absorbing_fallback_widen_sketch( + catalog_id: sccache_local_id, + observed: unsupervised_observation_fixture(), + ) { + ProvisionConverged { catalog_id: _, stats_line: _ } => true + ProvisionRefused { cause: _, reason: _ } => false + } && !build_cache_provision_gate_accepts( + verdict: provision_build_cache_absorbing_fallback_widen_sketch( + catalog_id: sccache_local_id, + observed: unsupervised_observation_fixture(), + ), + observed: unsupervised_observation_fixture(), + ) + && build_cache_provision_gate_accepts( + verdict: provision_build_cache_verdict( + catalog_id: sccache_local_id, + observed: unsupervised_observation_fixture(), + ), + observed: unsupervised_observation_fixture(), + ) +} + +fn design_witness_supervision_observation_not_emitted_as_shell() -> Bool { + !string_contains( + s: build_cache_observe_stats_body(), + pattern: "is-active", + ) && !string_contains( + s: build_cache_read_back_body(binary: sccache_installed_binary_path), + pattern: "is-active", + ) +} + fn design_witness_classifier_covers_every_cited_fragment() -> Bool { build_cache_classifier_covers_every_cited_fragment() } @@ -246,6 +324,10 @@ test fn host_build_cache_provision_design_witnesses() -> Bool { && design_witness_install_is_cited_not_package_manager() && design_witness_unit_execstart_matches_install_path() && design_witness_unit_is_foreground_supervised() + && design_witness_unit_daemon_runs_until_stopped() + && design_witness_unsupervised_refuses_fail_closed() + && design_witness_red_control_widen_on_unsupervised_rejected_by_gate() + && design_witness_supervision_observation_not_emitted_as_shell() && design_witness_classifier_covers_every_cited_fragment() && design_witness_classifier_is_a_fold_not_an_unrolled_chain() && design_witness_fragment_words_are_shell_safe() From 601ba03af285e574aa4b9bba74f7363af9b57f93 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 13:11:48 +0000 Subject: [PATCH 04/17] WIP: srvN subsumption --- .../host_build_cache_provision_script.dag | 5 ++-- .../srvn-buildcache-provisioning-design.md | 26 ++++++++++++++++++- 2 files changed, 28 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/host_build_cache_provision_script.dag b/dag/gunbc/host_build_cache_provision_script.dag index dee206402d0..43ca1743eec 100644 --- a/dag/gunbc/host_build_cache_provision_script.dag +++ b/dag/gunbc/host_build_cache_provision_script.dag @@ -17,7 +17,7 @@ import extdeps.cache.sccache { data host_build_cache_provision_script_dissolution_trigger: String = "🟡 dissolve-on: host_build_cache_provision_script — concat-built systemd/sccache ensure shell; DISSOLVES WHEN bash-emit (#5828) realizes ProvisionBuildCache observe/ensure/read-back as typed host-effect argv and realize_provision_build_cache retires shell_exec_via_bash transport." -data host_build_cache_provision_script_census_row_note: String = "CENSUS STANDING: docs/plans/shell-to-dag-residual-census-and-arc-completion.md §4.A keys this file as the builder for host_effect_realize.ProvisionBuildCache, action DECOMPOSE, sub-class A5 (srv* cluster, deferred by operator 2026-07-22 — real debt, NOT done; un-defer trigger is the operator). This site is RUNTIME-PRESENT (it realizes through host_effect_apply_gated on LocalShell/SshShell), so per that doc's routing decision its end state is a typed effect-plan with NO bash emitted — the six *_body builders below are the debt, not the design. Standing constraint while the row is deferred, stated precisely (review 42401 sharpened this): NEW emitted shell must be either a DEDUCTION or a cited-de-fork SWAP — never an unbounded, uncited addition. Two exact deltas this PR made, both accounted: (1) the sccache DE-FORK swap — `apt-get install sccache` + an `ExecStart=/usr/bin/sccache` unit went OUT, and the cited-tarball install invocation (sccache_install_script, one authority row) came IN; that is the §3 fork removal this PR exists to make, a swap that de-duplicates rather than grows. (2) `sudo -n loginctl enable-linger \"$USER\"` is genuinely NEW shell, not a swap — acknowledged here as growth rather than hidden: it is the one primitive that makes the already-selected user-scope systemd handler viable at all (a `--user` manager is torn down with the login otherwise), justified in build_cache_user_service_linger_note, and it is bounded (a single fixed leaf, not a corpus-denominated fold). What must NOT grow is the PATH-shadow OBSERVATION: the judgement went to gunbc.host_build_cache_provision (DaemonPathShadowed / RefusalPathShadowed + verdict fold, witnessed against a synthetic observation), and its live shell observation is STAGED, NOT emitted here — an earlier attempt folded `command -v sccache` lines into the two existing bodies, which kept the builder count at six but still grew the shell surface (review 42343 rejected that as a census regression). The observation lands when ProvisionBuildCache realizes as typed argv (dissolve-on #5828). Adding a *_body, or an uncited emitted-shell leaf that is neither a deduction nor a de-fork swap, is a census regression even when the behaviour it adds is correct. FOLLOW-UP #7206 delta (correctness swap, accounted): the unit's `ExecStart=... --start-server` became bare `ExecStart=...` + two `Environment=` lines (SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1) — net +1 line, and NOT uncited growth: it is a swap toward the production ctrl-sccache.service invocation (the single authority the whole lane converges on), replacing a form live execution on srv3 proved is a Type=simple no-op (build_cache_unit_foreground_supervision_note). A correctness swap toward the cited production authority is the sanctioned shape, exactly like delta (1). FOLLOW-UP #7 delta (DEDUCTION, accounted): one further `Environment=` line, SCCACHE_IDLE_TIMEOUT=0, net +1 emitted line. This one is NOT a swap toward production — srv1/srv2 do not set the knob either — so it is accounted as the other sanctioned shape, a DEDUCTION: it follows from the cited upstream authority (Configuration.md, extdeps.cache.sccache.sccache_server_lifetime_note) plus the srv3 receipt that the foreground unit exits 0 after 10min 8s idle, and it is the minimal line that makes Type=simple supervision hold at all. It also SHRINKS this file's ownership of vocabulary it does not own: all three Environment values now come from extdeps rows (sccache_start_server_env_assignment / sccache_no_daemon_env_assignment / sccache_idle_timeout_never_env_assignment) instead of bare literals spelled here, so gunbc is no longer a second authority for sccache env var names (§3). The supervision OBSERVATION (`systemctl --user is-active`) is STAGED, not emitted, on exactly the PATH-shadow precedent — the judgement lives in gunbc.host_build_cache_provision (DaemonUnsupervised / RefusalDaemonUnsupervised, witnessed against a synthetic observation) and the live producer waits for typed argv (dissolve-on #5828)." +data host_build_cache_provision_script_census_row_note: String = "CENSUS STANDING: docs/plans/shell-to-dag-residual-census-and-arc-completion.md §4.A keys this file as the builder for host_effect_realize.ProvisionBuildCache, action DECOMPOSE, sub-class A5 (srv* cluster, deferred by operator 2026-07-22 — real debt, NOT done; un-defer trigger is the operator). This site is RUNTIME-PRESENT (it realizes through host_effect_apply_gated on LocalShell/SshShell), so per that doc's routing decision its end state is a typed effect-plan with NO bash emitted — the six *_body builders below are the debt, not the design. Standing constraint while the row is deferred, stated precisely (review 42401 sharpened this): NEW emitted shell must be either a DEDUCTION or a cited-de-fork SWAP — never an unbounded, uncited addition. Two exact deltas this PR made, both accounted: (1) the sccache DE-FORK swap — `apt-get install sccache` + an `ExecStart=/usr/bin/sccache` unit went OUT, and the cited-tarball install invocation (sccache_install_script, one authority row) came IN; that is the §3 fork removal this PR exists to make, a swap that de-duplicates rather than grows. (2) `sudo -n loginctl enable-linger \"$USER\"` is genuinely NEW shell, not a swap — acknowledged here as growth rather than hidden: it is the one primitive that makes the already-selected user-scope systemd handler viable at all (a `--user` manager is torn down with the login otherwise), justified in build_cache_user_service_linger_note, and it is bounded (a single fixed leaf, not a corpus-denominated fold). What must NOT grow is the PATH-shadow OBSERVATION: the judgement went to gunbc.host_build_cache_provision (DaemonPathShadowed / RefusalPathShadowed + verdict fold, witnessed against a synthetic observation), and its live shell observation is STAGED, NOT emitted here — an earlier attempt folded `command -v sccache` lines into the two existing bodies, which kept the builder count at six but still grew the shell surface (review 42343 rejected that as a census regression). The observation lands when ProvisionBuildCache realizes as typed argv (dissolve-on #5828). Adding a *_body, or an uncited emitted-shell leaf that is neither a deduction nor a de-fork swap, is a census regression even when the behaviour it adds is correct. FOLLOW-UP #7206 delta (correctness swap, accounted): the unit's `ExecStart=... --start-server` became bare `ExecStart=...` + two `Environment=` lines (SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1) — net +1 line, and NOT uncited growth: it is a swap toward the production ctrl-sccache.service invocation (the single authority the whole lane converges on), replacing a form live execution on srv3 proved is a Type=simple no-op (build_cache_unit_foreground_supervision_note). A correctness swap toward the cited production authority is the sanctioned shape, exactly like delta (1). FOLLOW-UP #7213 delta (DEDUCTION, accounted): one further `Environment=` line, SCCACHE_IDLE_TIMEOUT=0, net +1 emitted line. This one is NOT a swap toward production — srv1/srv2 do not set the knob either — so it is accounted as the other sanctioned shape, a DEDUCTION: it follows from the cited upstream authority (Configuration.md, extdeps.cache.sccache.sccache_server_lifetime_note) plus the srv3 receipt that the foreground unit exits 0 after 10min 8s idle, and it is the minimal line that makes Type=simple supervision hold at all. It also SHRINKS this file's ownership of vocabulary it does not own: all three Environment values now come from extdeps rows (sccache_start_server_env_assignment / sccache_no_daemon_env_assignment / sccache_idle_timeout_never_env_assignment) instead of bare literals spelled here, so gunbc is no longer a second authority for sccache env var names (§3). The supervision OBSERVATION (`systemctl --user is-active`) is STAGED, not emitted, on exactly the PATH-shadow precedent — the judgement lives in gunbc.host_build_cache_provision (DaemonUnsupervised / RefusalDaemonUnsupervised, witnessed against a synthetic observation) and the live producer waits for typed argv (dissolve-on #5828)." data host_build_cache_provision_script_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority, @@ -42,6 +42,7 @@ fn build_cache_systemd_user_unit_body() -> String { "Type=simple", join(["Environment=", sccache_start_server_env_assignment()], ""), join(["Environment=", sccache_no_daemon_env_assignment()], ""), + join(["Environment=", sccache_idle_timeout_never_env_assignment()], ""), join(["ExecStart=", sccache_installed_binary_path], ""), "Restart=on-failure", "", @@ -182,7 +183,7 @@ fn build_cache_unit_execstart_matches_install_path() -> Bool { ) } -data build_cache_unit_foreground_supervision_note: String = "The unit is Type=simple, so systemd tracks the ExecStart process AS the service — it MUST stay in the foreground. `sccache --start-server` DAEMONIZES and returns 0, so under Type=simple systemd sees the ExecStart exit cleanly and marks the unit `inactive (dead)` the instant it starts; the backgrounded server then idle-times-out unsupervised and Restart=on-failure never fires (the exit was success). Proven live on srv3 2026-07-25: the earlier `--start-server` form left the unit inactive with no sccache process, the daemon surviving only via sccache's own per-invocation auto-start — i.e. the unit was a no-op. This is the §5 specification-without-execution trap: the string witness that ExecStart equals the install path was green while the unit did nothing. The foreground form matches the production ctrl-sccache.service invocation (bare ExecStart + SCCACHE_START_SERVER=1 SCCACHE_NO_DAEMON=1 env, verified running month+ on srv1/srv2), reducing the §3 fork between the modeled unit and production rather than inventing a third shape. build_cache_unit_is_foreground_supervised makes the defective combo (Type=simple paired with a backgrounding --start-server) UNWRITABLE; the runtime is-active proof is the live srv3 re-provision (systemd --user is not runnable in the hermetic CI container, so the construction wall carries the CI grain and live execution carries the runtime grain)." +data build_cache_unit_foreground_supervision_note: String = "The unit is Type=simple, so systemd tracks the ExecStart process AS the service — it MUST stay in the foreground. `sccache --start-server` DAEMONIZES and returns 0, so under Type=simple systemd sees the ExecStart exit cleanly and marks the unit `inactive (dead)` the instant it starts; the backgrounded server then idle-times-out unsupervised and Restart=on-failure never fires (the exit was success). Proven live on srv3 2026-07-25: the earlier `--start-server` form left the unit inactive with no sccache process, the daemon surviving only via sccache's own per-invocation auto-start — i.e. the unit was a no-op. This is the §5 specification-without-execution trap: the string witness that ExecStart equals the install path was green while the unit did nothing. The foreground form matches the production ctrl-sccache.service invocation (bare ExecStart + SCCACHE_START_SERVER=1 SCCACHE_NO_DAEMON=1 env, verified running month+ on srv1/srv2), reducing the §3 fork between the modeled unit and production rather than inventing a third shape. build_cache_unit_is_foreground_supervised makes the defective combo (Type=simple paired with a backgrounding --start-server) UNWRITABLE; the runtime is-active proof is the live srv3 re-provision (systemd --user is not runnable in the hermetic CI container, so the construction wall carries the CI grain and live execution carries the runtime grain). CORRECTION 2026-07-25 — that runtime claim was an OVERCLAIM and is retracted as stated: the srv3 re-provision observed is-active only in the same minutes it ran, and a read-back six hours later found the unit `inactive (dead)` since 06:38:56 with no sccache process. Foreground supervision was necessary and not sufficient; the residue is sccache's own idle timeout, and the fix, the receipt and the reason Restart=always is the wrong repair are in build_cache_unit_daemon_self_exit_note. The general lesson this lane keeps re-learning: an is-active read taken at provisioning time proves the unit STARTED, never that it STAYS — the durable claim needs a read-back separated from the write by longer than every self-exit timer in the supervised process." fn build_cache_unit_is_foreground_supervised() -> Bool { let body = build_cache_systemd_user_unit_body() diff --git a/docs/plans/srvn-buildcache-provisioning-design.md b/docs/plans/srvn-buildcache-provisioning-design.md index fff1986974d..33defb76aa3 100644 --- a/docs/plans/srvn-buildcache-provisioning-design.md +++ b/docs/plans/srvn-buildcache-provisioning-design.md @@ -22,6 +22,8 @@ Status: **DESIGN ANCHOR** — operator review before implementation (2026-07-17, STEP 2 is **explicitly out of scope** for the first implementation PR. Removing the fallback before provisioning is reliable would red the whole fleet. +**STEP 2 status (2026-07-23): the cache-drop half LANDED.** `ci_retry_escalation_level2` (`-u RUSTC_WRAPPER`) is deleted — the escalation now stops at `CARGO_BUILD_JOBS=1` (keeps sccache) and then fails loud via verify-build-artifacts, so no arm drops the cache any more. The sketch `provision_build_cache_absorbing_fallback_widen_sketch` stays as the RED control guarding the verdict fold against re-introduction. Level 1 was kept as EAGAIN containment rather than converted to a refusal (§4.4's open decision, resolved toward "keep"). Still open under STEP 2: `ci_sccache_opportunistic_detect` — CI's `if sccache --show-stats` is still an opportunistic detect rather than a fail-closed require, and §5.4 Finding 2 sharpens why that flip needs a supervisor read and not a stats read to key on. + ## 2. Reuse map — single authorities, never fork (§3 DFS) | Concern | Single authority (reuse verbatim) | What's NEW | @@ -202,11 +204,33 @@ Walk of `host_standup_spine` phases that could touch compile/cache **before** P1 | **T1** | catalog authority | `catalog_id == sccache_local_id` pins to cited row | wrong id → `CatalogUnknown` | | **T2** | spine consumer | `host_standup_spine` includes `P1b:build-cache-provision` row | remove row → `host_standup_gap_count` witness fails | | **T3** | srv1 dry-run | `host_toolchain_ensure(host: srv1, kind: BuildCache)` dry-run receipt on operator host | — | -| **T4** | live read-back | post-apply `sccache --show-stats` on srv1 **and** srv2; independent of our write | hand-stop daemon → next standup run → `ProvisionRefused`, counted | +| **T4** | live read-back | **superseded — see §5.4.** A post-apply stats read cannot discharge this tier | hand-stop daemon → next standup run → `ProvisionRefused`, counted | | **T5** | CI consumer | STEP 2: build job without `RUSTC_WRAPPER` unset arm stays green for 7d on main | disable daemon on one host → build job typed refuse, not local fallback | Design-anchor PR lands **T1** only (scaffold + type witnesses). T2+ follow implementation PR. +### 5.4 T4 restated — a stats read-back cannot discharge it (2026-07-25) + +T4 was written as "post-apply `sccache --show-stats`, independent of our write." Live execution on srv3 falsified **both** halves of that, and the tier is restated here rather than quietly re-scoped. + +**Finding 1 — the unit still died, for a second reason.** #7206 foregrounded the server (`Type=simple` + bare `ExecStart` + `SCCACHE_START_SERVER=1` / `SCCACHE_NO_DAEMON=1`), which fixed the daemonize-and-exit no-op. A read-back six hours later found the unit `inactive (dead) since 06:38:56`, `Main PID … (code=exited, status=0/SUCCESS)`, `Duration: 10min 8.215s`, and **no sccache process at all**. Root cause: `SCCACHE_IDLE_TIMEOUT` defaults to 600s, so the foreground process exits *cleanly* on the first quiet ten minutes, and `Restart=on-failure` cannot fire on a success exit. Same end state as the bug #7206 fixed, one level deeper — and #7206's own claim that "the live srv3 re-provision carries the runtime is-active grain" was the overclaim that hid it, because that read was taken in the same minutes as the write. + +- **Fix:** `Environment=SCCACHE_IDLE_TIMEOUT=0` — cited to sccache `docs/Configuration.md`: *"how long the local daemon process waits for more client requests before exiting, in seconds. Set to 0 to run sccache permanently."* +- **Not `Restart=always`:** that would relaunch *through* the clean exit and make the deficit invisible — §5's absorbing fallback. With the timeout disabled a status-0 exit is unreachable by configuration, so `on-failure` is the honest policy and a dead unit stays a real, refusable state. +- **Receipt (green):** modeled unit rendered from `build_cache_systemd_user_unit_body()`, installed on srv3, `active (running)`, `NRestarts=0`, same `Main PID`, read back **13 minutes** after the write — past the 600s timer that killed the previous form. +- **Receipt (red control):** the identical unit *without* the knob — i.e. exactly what #7206 shipped — exits 0 after 10min 8s. This is the discriminating pair; the construction check `build_cache_unit_daemon_runs_until_stopped` is parameterized over a unit body so the witness runs both sides. +- **srv1/srv2 are not the counter-example they look like.** The production `ctrl-sccache.service` does not set the knob either; its month-plus uptime is CI traffic keeping the daemon below the idle threshold — accidental coverage, not a durable unit. So this line is a **deduction** from the cited doc plus the srv3 receipt, not a swap toward production. + +**Finding 2 — `--show-stats` is not an independent observation.** Any sccache invocation auto-starts a server when none is listening, so the probe manufactures the evidence it reports. On srv3 it printed a full stats table while the unit had been dead for six hours. Read through the verdict fold as it stood, that host observed `DaemonStatsOk` and **converged** — a provisioning act reporting success over a host with no durable cache (§5 fabricated plausible output, the same shape as `DaemonPathShadowed`). + +- **Model:** `DaemonUnsupervised { unit, unit_state }` → `RefusalDaemonUnsupervised`. "A daemon answered" and "the modeled supervisor is running it" are different states with different remedies, so they get different names rather than one `Ok`. +- **Live observation STAGED**, on the PATH-shadow precedent (review 42343): the `systemctl --user is-active` read is *not* emitted as hand-shell into the A5 census row; it lands with the typed-argv dissolve-on (#5828). The model carries the state and its refusal today. +- Construction covers hosts *this lane* provisions (the self-exiting unit is unwritable); the observation's standing job is the residue construction cannot reach — a unit stopped, masked or replaced out of band. + +**T4 restated.** The tier is discharged by a **delayed supervisor read**, not a post-apply stats read: after provisioning, read `systemctl --user is-active` (and the main PID) **separated from the write by longer than every self-exit timer in the supervised process**, on each subsumed host. An is-active read taken at provisioning time proves the unit *started*, never that it *stays*. + +**T4 status:** srv3 **green** at the restated bar (13-minute delayed read, modeled unit, PID stable). srv1 and srv2 remain **open** — not for a modeling reason: neither host is reachable from a session container with the fleet key today (`Permission denied (publickey)` for `ubuntu`/`briansrls`/`node-orch`), which is the A1/A2/B2 reach-and-identity gap already typed in `gunbc.plans.fleet_subsumption_manual_gaps`. The downstream triggers (`ctrl_sccache_service_retired`, and the `ci_sccache_opportunistic_detect` cutover) stay blocked on those two hosts, and the srv1/srv2 units should be expected to carry the same latent defect until re-provisioned from the model. + ## 6. Dissolution triggers (every scaffold names its exit) | Scaffold | Dissolves to | Trigger | From 1e84e113494e2f8e0594d355aee1964baa87d546 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 13:32:54 +0000 Subject: [PATCH 05/17] WIP: srvN subsumption --- dag/extdeps/cache/sccache.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/extdeps/cache/sccache.dag b/dag/extdeps/cache/sccache.dag index 0334444934a..dbc75a4fcb6 100644 --- a/dag/extdeps/cache/sccache.dag +++ b/dag/extdeps/cache/sccache.dag @@ -150,7 +150,7 @@ data sccache_misconfigured_log_fragments: List = [ sccache_failed_to_execute_compile_log_fragment, ] -data sccache_server_lifetime_note: String = "sccache's server EXITS ON ITS OWN. Three environment knobs, all documented by the module's cited authority extdeps_external_authority_anchor (github.com/mozilla/sccache/blob/main/docs/Configuration.md), decide the process lifetime a supervisor sees, and they are modeled here because they are facts about SCCACHE — not about systemd, and not about gunbc. Before 2026-07-25 the P1b unit emitter spelled SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1 as bare literals of its own, which made gunbc.host_build_cache_provision_script a SECOND authority for sccache's environment vocabulary (§3) — and the knob that was missing from that second authority is exactly the one that broke: SCCACHE_IDLE_TIMEOUT. Cited text: 'how long the local daemon process waits for more client requests before exiting, in seconds. Set to 0 to run sccache permanently.' The default is 600 seconds, confirmed by execution rather than read off the doc: on srv3 2026-07-25 the foreground-supervised unit started at 06:28:47 UTC, served no compile request, and EXITED 0 after `Duration: 10min 8.215s`, leaving `inactive (dead)` — Restart=on-failure could not fire because the exit was a success. Consequence for any supervisor: a Type=simple unit whose ExecStart is sccache is only durable when the idle timeout is disabled; otherwise it dies on the first quiet ten minutes and the host reverts to sccache's own unsupervised per-invocation auto-start (the very no-op state the foreground form was introduced to remove). The srv1/srv2 production ctrl-sccache.service does not set this knob either — its month-plus uptime is CI traffic keeping the daemon below the idle threshold, i.e. accidental coverage, not a durable unit; that is a fact about the observed hosts, so this row is a DEDUCTION from the cited doc and the srv3 receipt, not a swap toward production." +data sccache_server_lifetime_note: String = "sccache's server EXITS ON ITS OWN. Three environment knobs, all documented by the module's cited authority extdeps_external_authority_anchor (github.com/mozilla/sccache/blob/main/docs/Configuration.md), decide the process lifetime a supervisor sees, and they are modeled here because they are facts about SCCACHE — not about systemd, and not about gunbc. Before 2026-07-25 the P1b unit emitter spelled SCCACHE_START_SERVER=1 / SCCACHE_NO_DAEMON=1 as bare literals of its own, which made gunbc.host_build_cache_provision_script a SECOND authority for sccache's environment vocabulary (§3) — and the knob that was missing from that second authority is exactly the one that broke: SCCACHE_IDLE_TIMEOUT. Cited text: 'how long the local daemon process waits for more client requests before exiting, in seconds. Set to 0 to run sccache permanently.' The default is 600 seconds, confirmed by execution rather than read off the doc: on srv3 2026-07-25 the foreground-supervised unit started at 06:28:47 UTC, served no compile request, and EXITED 0 after `Duration: 10min 8.215s`, leaving `inactive (dead)` — Restart=on-failure could not fire because the exit was a success. Consequence for any supervisor: a Type=simple unit whose ExecStart is sccache is only durable when the idle timeout is disabled; otherwise it dies on the first quiet ten minutes and the host reverts to sccache's own unsupervised per-invocation auto-start (the very no-op state the foreground form was introduced to remove). Whether the srv1/srv2 production ctrl-sccache.service sets this knob is UNVERIFIED — neither host is reachable from a session container today, and the only in-tree description of that unit (#7206's note) lists SCCACHE_START_SERVER and SCCACHE_NO_DAEMON and no idle-timeout line, which is an absence in a summary, not evidence of absence in the file. What its month-plus uptime does NOT establish is that the unit is durable: those hosts run CI continuously, so traffic keeps the daemon below the idle threshold whether or not the timer is disabled — the uptime is consistent with both. This row therefore stands on the cited doc plus the srv3 receipt as a DEDUCTION; it is explicitly NOT claimed as a swap toward a production form nobody has read." data sccache_start_server_env_var: String = "SCCACHE_START_SERVER" From b29d4f7ff9e48e37968f546cd89723b6c53f852c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 13:35:50 +0000 Subject: [PATCH 06/17] srvN build-cache: design-doc receipts for the idle-timeout finding --- docs/plans/srvn-buildcache-provisioning-design.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/docs/plans/srvn-buildcache-provisioning-design.md b/docs/plans/srvn-buildcache-provisioning-design.md index 33defb76aa3..00ecfd64839 100644 --- a/docs/plans/srvn-buildcache-provisioning-design.md +++ b/docs/plans/srvn-buildcache-provisioning-design.md @@ -217,9 +217,12 @@ T4 was written as "post-apply `sccache --show-stats`, independent of our write." - **Fix:** `Environment=SCCACHE_IDLE_TIMEOUT=0` — cited to sccache `docs/Configuration.md`: *"how long the local daemon process waits for more client requests before exiting, in seconds. Set to 0 to run sccache permanently."* - **Not `Restart=always`:** that would relaunch *through* the clean exit and make the deficit invisible — §5's absorbing fallback. With the timeout disabled a status-0 exit is unreachable by configuration, so `on-failure` is the honest policy and a dead unit stays a real, refusable state. -- **Receipt (green):** modeled unit rendered from `build_cache_systemd_user_unit_body()`, installed on srv3, `active (running)`, `NRestarts=0`, same `Main PID`, read back **13 minutes** after the write — past the 600s timer that killed the previous form. -- **Receipt (red control):** the identical unit *without* the knob — i.e. exactly what #7206 shipped — exits 0 after 10min 8s. This is the discriminating pair; the construction check `build_cache_unit_daemon_runs_until_stopped` is parameterized over a unit body so the witness runs both sides. -- **srv1/srv2 are not the counter-example they look like.** The production `ctrl-sccache.service` does not set the knob either; its month-plus uptime is CI traffic keeping the daemon below the idle threshold — accidental coverage, not a durable unit. So this line is a **deduction** from the cited doc plus the srv3 receipt, not a swap toward production. +- **Receipt — controlled A/B under guaranteed idleness (srv3, 2026-07-25 13:20:29 → 13:32:36).** Two sccache 0.15.0 servers from the same binary, started in the same second, each with a private `SCCACHE_DIR` and a non-standard `SCCACHE_SERVER_PORT` (4301 / 4302) so no client could reach either — idleness by construction, not by hoping the host is quiet. One variable differs. + - **A**, default idle timeout: **gone** at 12:10 elapsed. Exited on its own. + - **B**, `SCCACHE_IDLE_TIMEOUT=0`: **still running** at 12:10, same PID. +- **Receipt — the modeled unit itself.** `build_cache_systemd_user_unit_body()` rendered from the `.dag`, installed on srv3 with the probe drop-in removed, `active (running)` / `NRestarts=0` / stable `Main PID 3678958` at +13min and +26min. Stated with its limit: srv3 is a live CI runner and a job hit the daemon during that window, so this receipt shows the modeled artifact deploys and stays up — it is **not** an idle test. The A/B pair above is what discharges the idle claim, and it is the one to re-run when the knob changes. +- **Receipt (red control), same host, prior form:** the unit exactly as #7206 shipped it — `Duration: 10min 8.215s`, `code=exited, status=0/SUCCESS`, `inactive (dead)`, no sccache process. The construction check `build_cache_unit_daemon_runs_until_stopped` is parameterized over a unit body so the witness runs both sides of this pair, and dropping the knob from the emitter reds it (verified by perturbation). +- **srv1/srv2 are not the counter-example they look like — and their unit is unread.** Whether production's `ctrl-sccache.service` sets the knob is **unverified**: neither host is reachable from a session container today, and the only in-tree description of that unit (#7206's note) lists two env lines and no idle timeout — an absence in a summary, not evidence of absence in the file. What the month-plus uptime does *not* establish is durability: those hosts run CI continuously, so traffic holds the daemon below the idle threshold whether or not the timer is disabled. The line therefore lands as a **deduction** from the cited doc plus the A/B receipt, and is explicitly *not* claimed as a swap toward a production form nobody has read. **Finding 2 — `--show-stats` is not an independent observation.** Any sccache invocation auto-starts a server when none is listening, so the probe manufactures the evidence it reports. On srv3 it printed a full stats table while the unit had been dead for six hours. Read through the verdict fold as it stood, that host observed `DaemonStatsOk` and **converged** — a provisioning act reporting success over a host with no durable cache (§5 fabricated plausible output, the same shape as `DaemonPathShadowed`). From fa2dad424017721dea0686c733d2e886fad5524d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 16:36:07 +0000 Subject: [PATCH 07/17] WIP: srvN subsumption --- dag/probe_tmp/p1.dag | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 dag/probe_tmp/p1.dag diff --git a/dag/probe_tmp/p1.dag b/dag/probe_tmp/p1.dag new file mode 100644 index 00000000000..14e91b832d5 --- /dev/null +++ b/dag/probe_tmp/p1.dag @@ -0,0 +1,15 @@ +module probe.p1 + +import std.types { Int } +import std.upsert_decision { ObservationVerdict, Converged, Drifted, Conflict, Inaccessible, UnknownRefused } + +fn rank(v: ObservationVerdict) -> Int { + match v { + Converged => 0 + std.upsert_decision.Absent => 1 + Drifted => 2 + Conflict => 3 + Inaccessible => 4 + UnknownRefused => 5 + } +} From 67d302af4a546c69baf0e7abe422cf8337029bc4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 16:46:47 +0000 Subject: [PATCH 08/17] WIP: srvN subsumption --- dag/gunbc/host_phase_status.dag | 241 ++++++++++++++++++++++++++++++++ dag/probe_tmp/p1.dag | 15 -- 2 files changed, 241 insertions(+), 15 deletions(-) create mode 100644 dag/gunbc/host_phase_status.dag delete mode 100644 dag/probe_tmp/p1.dag diff --git a/dag/gunbc/host_phase_status.dag b/dag/gunbc/host_phase_status.dag new file mode 100644 index 00000000000..ee0ebdb6091 --- /dev/null +++ b/dag/gunbc/host_phase_status.dag @@ -0,0 +1,241 @@ +module gunbc.host_phase_status + +import std.types { String, NonEmptyStr, Bool, Int, List } +import std.upsert_decision { ObservationVerdict, Converged, Drifted, Conflict, Inaccessible, UnknownRefused } +import std.disposition { Disposition, Scaffold, SingleAuthority } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import gunbc.host_standup { + HostStandupStep, + PhaseDisposition, + ModeledCompose, + DeclaredGap, + host_standup_spine, +} +import gunbc.host_standup_assimilation_deduction { srv3_post_install_actuation_verdict } +import gunbc.membership_reconcile { + MembershipPlan, + MemberAction, + MemberUpsert, + MemberTeardown, + MemberTeardownRefused, + membership_reconcile, + membership_upsert_count, +} +import gunbc.ownership { Ownership, Owned } +import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4 } +import product.placement_supply { HostIdentity } +import std.measure { millisecond } + +data host_phase_status_authority_note: String = "THE per-(host x phase) status axis for the host-standup spine. It exists because the spine could describe itself but not its RELATIONSHIP TO THE LIVE FLEET: every phase carried a PhaseDisposition (is there a modeled authority?) and nothing carried an observation (does this host actually agree with it?). Answering 'where does subsumption stand' therefore meant a session reconstruction — hand ssh probes, prose transcription — and the answer went stale the moment it was written. Two axes, kept ORTHOGONAL on purpose, because collapsing them is the state-space conflation this lane keeps paying for: the MODELED axis is PhaseDisposition, a property of the phase, the same for every host; the LIVE axis is std.upsert_decision.ObservationVerdict, a property of the (host, phase) CELL. A phase can be fully modeled AND Inaccessible on a given host — that is exactly srv1/srv2 for the build-cache phase today — and a single fused enum could not say it. Note what is NOT minted here: no Converged|Diverged|Unreachable|Unmodeled verdict of our own. ObservationVerdict already carries Converged/Absent/Drifted/Conflict/Inaccessible/UnknownRefused, which is STRICTLY FINER on the diverged and unreachable axes, and it is already consumed by twelve modules including host_standup itself; a parallel four-arm verdict beside it would be the §3 nickname, duplicated again in everything derived from it. 'Unmodeled' is likewise not an observation — a host cannot be observed to disagree with a model that does not exist — so it stays on PhaseDisposition and enters this type as the StatusUnmodeled arm, derived from the spine, never authored." + +data host_phase_cell_grain_note: String = "The cell is keyed by (host, phase_label) and NOT by (host, phase) structurally, because phase_label is already the spine's own stable identity for a step (it is what the gap ledger keyed on, what the refusal strings name, and what an operator reads). Keying on the label keeps ONE identity for a phase across the spine, this matrix, and every refusal message, rather than introducing a second notion of phase identity that could disagree with the first. key_of returns identity, never content (membership_reconcile's R2 contract): a cell whose STATUS changes is Modified — the same cell re-derived — not Removed+Added, which would read as a host leaving and rejoining the fleet." + +type HostPhaseCell { + host: HostIdentity + phase_label: String +} + +type HostPhaseStatus + = StatusUnmodeled { refusal: String } + | StatusObserved { verdict: ObservationVerdict } + +type HostPhaseCellStatus { + cell: HostPhaseCell + status: HostPhaseStatus +} + +data host_phase_no_producer_is_unknown_not_converged_note: String = "THE fail-closed hinge of this module (DESIGN §5). When a modeled phase has NO live observation producer for a host, the derived verdict is UnknownRefused — never Converged, and never silently omitted from the matrix. The tempting arm is the absorbing fallback in its purest form: nothing is known to be wrong, so report converged; the matrix goes green, the coverage deficit's frequency drops to zero by construction, and the status read becomes a fabricated plausible output exactly like a stats probe that auto-starts the server it is measuring (the DaemonUnsupervised finding, #7213). It is also why UnknownRefused and Inaccessible must stay DISTINCT arms rather than one 'not converged': Inaccessible means we asked the host and could not reach it (remedy: fix reach — the A1 materialized-secret lane); UnknownRefused means we have no way to ask at all (remedy: build the producer). Different states, different owners, different work — and the count of each is the honest measure of how far subsumption actually is. host_phase_status_absorbing_fallback_widen_sketch models the forbidden arm as a RED control so the fold cannot drift back into it unnoticed." + +fn host_phase_status_from( + disposition: PhaseDisposition, + observation: ObservationVerdict?, +) -> HostPhaseStatus { + match disposition { + DeclaredGap { interim_realization: _, refusal: r } => StatusUnmodeled { refusal: r } + ModeledCompose { authorities: _ } => + match observation { + Present { value: v } => StatusObserved { verdict: v } + Absent => StatusObserved { verdict: UnknownRefused } + } + } +} + +fn host_phase_status_absorbing_fallback_widen_sketch( + disposition: PhaseDisposition, + observation: ObservationVerdict?, +) -> HostPhaseStatus { + match disposition { + DeclaredGap { interim_realization: _, refusal: r } => StatusUnmodeled { refusal: r } + ModeledCompose { authorities: _ } => + match observation { + Present { value: v } => StatusObserved { verdict: v } + Absent => StatusObserved { verdict: Converged } + } + } +} + +fn host_phase_status_gate_accepts( + status: HostPhaseStatus, + observation: ObservationVerdict?, +) -> Bool { + match observation { + Present { value: _ } => true + Absent => + match status { + StatusObserved { verdict: Converged } => false + StatusObserved { verdict: _ } => true + StatusUnmodeled { refusal: _ } => true + } + } +} + +data host_phase_observation_frontier_note: String = "The live-observation producer registry, and deliberately a TYPED, COUNTABLE FRONTIER rather than a table of hand-written facts (the self-host frontier shape, DESIGN §7: each cell is either produced or it is a declared absence, never a silent assumption). Exactly one cell has a real producer today — (srv3, prefix:os-install-actuated), which deduces its verdict from an observed DHCP lease table through gunbc.host_standup_assimilation_deduction; that deduction was ALREADY host-parameterized (deduce_os_install_actuation_verdict takes fleet_slot: HostIdentity), so generalizing it was reading the parameter it already had, not writing new machinery. Every other cell returns Absent, which host_phase_status_from renders UnknownRefused. What must NOT happen here is the shape this module exists to kill: hand-entering an observation because someone ssh'd a host once. A probe run by a person is not a modeled producer — encoding its result as a data row would rebuild the parallel ledger the gap-ledger dissolution just removed, and it would go stale in exactly the same way. A cell earns a row here when an effect produces its verdict by execution; until then UnknownRefused is the honest answer and host_phase_observation_coverage_count is the number that measures the debt." + +fn host_phase_observation(host: HostIdentity, step: HostStandupStep) -> ObservationVerdict? { + if (step.label as String) == "prefix:os-install-actuated" { + if host == operator_host_srv3 { + Present { value: srv3_post_install_actuation_verdict(elapsed: millisecond(count: 0)) } + } else { + none + } + } else { + none + } +} + +fn host_phase_cell_status(host: HostIdentity, step: HostStandupStep) -> HostPhaseCellStatus { + HostPhaseCellStatus { + cell: HostPhaseCell { host: host, phase_label: step.label as String }, + status: host_phase_status_from( + disposition: step.disposition, + observation: host_phase_observation(host: host, step: step), + ), + } +} + +fn host_phase_cells_for_host(host: HostIdentity) -> List { + map(host_standup_spine, s => host_phase_cell_status(host: host, step: s)) +} + +fn host_fleet_phase_matrix(hosts: List) -> List { + flat_map(hosts, h => host_phase_cells_for_host(host: h)) +} + +data fleet_subsumption_hosts_note: String = "The enrolled fleet, read from gunbc.fleet_intent_network's host rows rather than re-listed here — the matrix must never be able to disagree with the intent about WHICH hosts exist. This is also the enrollment prerequisite the srv4 OOM incident priced (fleet_subsumption_manual_gaps section C): a host takes no fleet work until it is an intent row, so a host absent from this list has no cells at all, and one that appears gains a full column of UnknownRefused cells — the work becoming visible the moment the host is enrolled, which is the behaviour the incident wanted." + +data fleet_subsumption_hosts: List = [ + operator_host_srv1, + operator_host_srv2, + operator_host_srv3, + operator_host_srv4, +] + +fn host_phase_cell_key(c: HostPhaseCellStatus) -> String { + join([c.cell.host as String, "|", c.cell.phase_label], "") +} + +fn host_phase_cell_key_eq(a: String, b: String) -> Bool { + a == b +} + +fn host_phase_status_eq(a: HostPhaseStatus, b: HostPhaseStatus) -> Bool { + match a { + StatusUnmodeled { refusal: _ } => + match b { + StatusUnmodeled { refusal: _ } => true + StatusObserved { verdict: _ } => false + } + StatusObserved { verdict: va } => + match b { + StatusUnmodeled { refusal: _ } => false + StatusObserved { verdict: vb } => observation_verdict_eq(a: va, b: vb) + } + } +} + +fn observation_verdict_eq(a: ObservationVerdict, b: ObservationVerdict) -> Bool { + observation_verdict_rank(v: a) == observation_verdict_rank(v: b) +} + +fn observation_verdict_rank(v: ObservationVerdict) -> Int { + match v { + Converged => 0 + std.upsert_decision.Absent => 1 + Drifted => 2 + Conflict => 3 + Inaccessible => 4 + UnknownRefused => 5 + } +} + +fn host_phase_cell_status_eq(a: HostPhaseCellStatus, b: HostPhaseCellStatus) -> Bool { + host_phase_cell_key(c: a) == host_phase_cell_key(c: b) + && host_phase_status_eq(a: a.status, b: b.status) +} + +fn host_phase_cell_ownership(c: HostPhaseCellStatus) -> Ownership? { + Present { value: Owned } +} + +data host_phase_reconcile_instantiation_note: String = "The status matrix reconciled as a MEMBERSHIP DIFF — one more (key_of, key_eq, value_eq, ownership_of) bundle handed to the single generic gunbc.membership_reconcile.membership_reconcile, never a forked diff (a forked reconcile means the genericity bought nothing). Desired is every cell at StatusObserved{Converged}: that is the end state of the whole subsumption lane — every phase modeled AND every enrolled host converged on it — so a Modified hunk is precisely one unit of remaining work, and membership_upsert_count is the answer to 'how much is left' as a NUMBER rather than a prose reconstruction. Removed is a real arm, not a degenerate pole: a cell observed for a host no longer in fleet_intent is a host that left the fleet, and cells are Owned, so it tears down rather than refusing. The witness exercises that arm synthetically because the live fleet has no departed host today — an instantiation whose interesting hunks are all unreachable in practice is an instantiation nobody has actually tested." + +fn host_phase_desired(hosts: List) -> List { + map( + host_fleet_phase_matrix(hosts: hosts), + c => HostPhaseCellStatus { cell: c.cell, status: StatusObserved { verdict: Converged } }, + ) +} + +fn host_phase_reconcile( + desired: List, + observed: List, +) -> MembershipPlan { + membership_reconcile( + desired: desired, + observed: observed, + key_of: host_phase_cell_key, + key_eq: host_phase_cell_key_eq, + value_eq: host_phase_cell_status_eq, + ownership_of: host_phase_cell_ownership, + ) +} + +fn host_phase_fleet_reconcile(hosts: List) -> MembershipPlan { + host_phase_reconcile( + desired: host_phase_desired(hosts: hosts), + observed: host_fleet_phase_matrix(hosts: hosts), + ) +} + +fn host_phase_remaining_work_count(hosts: List) -> Int { + membership_upsert_count(plan: host_phase_fleet_reconcile(hosts: hosts)) +} + +fn host_phase_cell_has_live_producer(c: HostPhaseCellStatus) -> Bool { + match c.status { + StatusUnmodeled { refusal: _ } => false + StatusObserved { verdict: v } => + match v { + UnknownRefused => false + Converged => true + std.upsert_decision.Absent => true + Drifted => true + Conflict => true + Inaccessible => true + } + } +} + +fn host_phase_observation_coverage_count(hosts: List) -> Int { + filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_has_live_producer(c: c)).length() +} + +fn host_phase_unmodeled_count(hosts: List) -> Int { + filter( + host_fleet_phase_matrix(hosts: hosts), + c => match c.status { + StatusUnmodeled { refusal: _ } => true + StatusObserved { verdict: _ } => false + }, + ).length() +} diff --git a/dag/probe_tmp/p1.dag b/dag/probe_tmp/p1.dag deleted file mode 100644 index 14e91b832d5..00000000000 --- a/dag/probe_tmp/p1.dag +++ /dev/null @@ -1,15 +0,0 @@ -module probe.p1 - -import std.types { Int } -import std.upsert_decision { ObservationVerdict, Converged, Drifted, Conflict, Inaccessible, UnknownRefused } - -fn rank(v: ObservationVerdict) -> Int { - match v { - Converged => 0 - std.upsert_decision.Absent => 1 - Drifted => 2 - Conflict => 3 - Inaccessible => 4 - UnknownRefused => 5 - } -} From ec0edde83dd0faedd1cbe1d5d82280adf7b33c8e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 16:57:14 +0000 Subject: [PATCH 09/17] WIP: srvN subsumption --- dag/gunbc/host_phase_status.dag | 19 +++ dag/gunbc/host_standup.dag | 4 + .../claim/host_phase_status_witness_test.dag | 148 ++++++++++++++++++ 3 files changed, 171 insertions(+) create mode 100644 dag/test/claim/host_phase_status_witness_test.dag diff --git a/dag/gunbc/host_phase_status.dag b/dag/gunbc/host_phase_status.dag index ee0ebdb6091..ae7174096c0 100644 --- a/dag/gunbc/host_phase_status.dag +++ b/dag/gunbc/host_phase_status.dag @@ -230,6 +230,25 @@ fn host_phase_observation_coverage_count(hosts: List) -> Int { filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_has_live_producer(c: c)).length() } +fn host_phase_cell_is_converged(c: HostPhaseCellStatus) -> Bool { + match c.status { + StatusUnmodeled { refusal: _ } => false + StatusObserved { verdict: v } => + match v { + Converged => true + std.upsert_decision.Absent => false + Drifted => false + Conflict => false + Inaccessible => false + UnknownRefused => false + } + } +} + +fn host_phase_converged_cell_count(hosts: List) -> Int { + filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_is_converged(c: c)).length() +} + fn host_phase_unmodeled_count(hosts: List) -> Int { filter( host_fleet_phase_matrix(hosts: hosts), diff --git a/dag/gunbc/host_standup.dag b/dag/gunbc/host_standup.dag index 4b20c09c80c..b8bef129ebd 100644 --- a/dag/gunbc/host_standup.dag +++ b/dag/gunbc/host_standup.dag @@ -407,6 +407,10 @@ fn host_standup_step_is_effective_gap_at_actuation_verdict( } } +fn host_standup_gap_phase_count() -> Int { + filter(host_standup_spine, s => host_standup_step_is_gap(step: s)).length() +} + fn host_standup_gap_count_at_actuation_verdict(verdict: ObservationVerdict) -> Int { fold( host_standup_spine, diff --git a/dag/test/claim/host_phase_status_witness_test.dag b/dag/test/claim/host_phase_status_witness_test.dag new file mode 100644 index 00000000000..0d411e8116a --- /dev/null +++ b/dag/test/claim/host_phase_status_witness_test.dag @@ -0,0 +1,148 @@ +module test.claim.host_phase_status + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data modeled_phase_fixture: PhaseDisposition = ModeledCompose { + authorities: [ + DeclarationRef { + module_path: "gunbc.host_phase_status", + decl_name: "host_phase_status_from", + field: WholeDeclaration, + }, + ] +} + +data unmodeled_phase_fixture: PhaseDisposition = DeclaredGap { + interim_realization: "ctrl:scripts/session-dashboard/lib/spawn_placement.mjs", + refusal: "host_standup:P4:session-placement-enrollment:unmodeled — refuse until placement enrollment has a .dag authority", +} + +data witness_no_producer_is_unknown_note: String = "THE fail-closed conjunct. A modeled phase with no live observation producer must derive UnknownRefused — the arm that says 'we have no way to ask this host'. If it ever derives Converged, the status matrix reports a subsumption that was never observed, and every count built on it (remaining work, coverage) silently becomes fiction. This is the same defect class as a stats probe that auto-starts the server it is measuring (#7213 Finding 2): evidence manufactured by the act of looking." + +fn witness_no_producer_derives_unknown_not_converged() -> Bool { + match host_phase_status_from(disposition: modeled_phase_fixture, observation: none) { + StatusObserved { verdict: UnknownRefused } => true + StatusObserved { verdict: _ } => false + StatusUnmodeled { refusal: _ } => false + } +} + +fn witness_unmodeled_phase_is_not_an_observation() -> Bool { + match host_phase_status_from(disposition: unmodeled_phase_fixture, observation: none) { + StatusUnmodeled { refusal: r } => string_contains(s: r, pattern: "refuse until") + StatusObserved { verdict: _ } => false + } +} + +data witness_orthogonality_note: String = "The two axes must stay independent: a phase can be FULLY MODELED and still Inaccessible on a given host — which is exactly srv1 and srv2 for the build-cache phase today, where the model is complete and the hosts refuse every fleet credential. A single fused status enum could not represent that cell, and would have to round it to either 'modeled' (hiding the live failure, which is how the stale status table read) or 'gap' (slandering a model that is finished). This conjunct pins the cell that proves the axes are separable." + +fn witness_modeled_phase_can_be_inaccessible() -> Bool { + match host_phase_status_from( + disposition: modeled_phase_fixture, + observation: Present { value: Inaccessible }, + ) { + StatusObserved { verdict: Inaccessible } => true + StatusObserved { verdict: _ } => false + StatusUnmodeled { refusal: _ } => false + } +} + +fn witness_unreachable_and_unknown_stay_distinct() -> Bool { + !observation_verdict_eq(a: Inaccessible, b: UnknownRefused) + && observation_verdict_eq(a: Inaccessible, b: Inaccessible) +} + +data witness_widen_red_control_note: String = "The discriminating RED control, built on the PATH-shadow / DaemonUnsupervised precedent: the forbidden absorbing fallback is modeled as its own sketch (host_phase_status_absorbing_fallback_widen_sketch fabricates Converged when no observation exists), the gate REJECTS the sketch's output, and the authority's output PASSES the same gate. The perturbation is independent of the property checked, so this cannot pass tautologically — an authority that quietly acquired the widen arm would be rejected by the gate it currently satisfies." + +fn witness_red_control_widen_on_absent_rejected_by_gate() -> Bool { + match host_phase_status_absorbing_fallback_widen_sketch( + disposition: modeled_phase_fixture, + observation: none, + ) { + StatusObserved { verdict: Converged } => true + StatusObserved { verdict: _ } => false + StatusUnmodeled { refusal: _ } => false + } && !host_phase_status_gate_accepts( + status: host_phase_status_absorbing_fallback_widen_sketch( + disposition: modeled_phase_fixture, + observation: none, + ), + observation: none, + ) + && host_phase_status_gate_accepts( + status: host_phase_status_from(disposition: modeled_phase_fixture, observation: none), + observation: none, + ) +} + +data departed_host_fixture: HostIdentity = "srv-departed" as HostIdentity + +fn departed_cell_fixture() -> HostPhaseCellStatus { + HostPhaseCellStatus { + cell: HostPhaseCell { host: departed_host_fixture, phase_label: "P1b:build-cache-provision" }, + status: StatusObserved { verdict: Converged }, + } +} + +data witness_reconcile_non_vacuous_note: String = "The membership instantiation must be exercised on a NON-DEGENERATE diff, or it is an instantiation nobody has tested. The live fleet produces only Modified and Unchanged hunks today (no host has left), so the Removed arm — a cell observed for a host absent from fleet_intent — is supplied synthetically here. All three arms are asserted in one reconcile: a departed host's cell tears down (cells are Owned, so R5 permits it rather than refusing), an unconverged cell upserts, and a converged cell produces no hunk at all." + +fn witness_reconcile_covers_added_modified_and_removed() -> Bool { + let converged_cell = HostPhaseCellStatus { + cell: HostPhaseCell { host: operator_host_srv3, phase_label: "P3:green-place-readiness" }, + status: StatusObserved { verdict: Converged }, + } + let unconverged_cell = HostPhaseCellStatus { + cell: HostPhaseCell { host: operator_host_srv3, phase_label: "P1b:build-cache-provision" }, + status: StatusObserved { verdict: UnknownRefused }, + } + let desired_unconverged = HostPhaseCellStatus { + cell: unconverged_cell.cell, + status: StatusObserved { verdict: Converged }, + } + let plan = host_phase_reconcile( + desired: [converged_cell, desired_unconverged], + observed: [converged_cell, unconverged_cell, departed_cell_fixture()], + ) + plan.actions.length() == 2 + && membership_upsert_count(plan: plan) == 1 + && membership_teardown_count(plan: plan) == 1 + && membership_refusal_count(plan: plan) == 0 +} + +data witness_matrix_shape_note: String = "Shape assertions over the derived matrix, pinned to the spine and the enrolled fleet rather than to hand-copied numbers: the matrix is exactly (hosts x spine steps), so it cannot silently drop a phase or a host. The coverage count is the honest measure of the live-observation frontier — one cell has a real producer today ((srv3, prefix:os-install-actuated)), and that number is what items 2 and 3 of the lane exist to raise. Pinning it means adding a producer is a VISIBLE, counted event that must update this witness, never a silent improvement nobody can point at." + +fn witness_matrix_is_hosts_times_spine() -> Bool { + let cells = host_fleet_phase_matrix(hosts: fleet_subsumption_hosts).length() + let expected = fleet_subsumption_hosts.length() * host_standup_spine.length() + cells == expected +} + +fn witness_live_observation_frontier_is_one_cell() -> Bool { + host_phase_observation_coverage_count(hosts: fleet_subsumption_hosts) == 1 +} + +fn witness_unmodeled_cells_track_spine_gaps() -> Bool { + let unmodeled = host_phase_unmodeled_count(hosts: fleet_subsumption_hosts) + let expected = fleet_subsumption_hosts.length() * host_standup_gap_phase_count() + unmodeled == expected +} + +fn witness_remaining_work_excludes_nothing_silently() -> Bool { + let remaining = host_phase_remaining_work_count(hosts: fleet_subsumption_hosts) + let total = host_fleet_phase_matrix(hosts: fleet_subsumption_hosts).length() + let converged = host_phase_converged_cell_count(hosts: fleet_subsumption_hosts) + remaining == total - converged +} + +test fn host_phase_status_witnesses() -> Bool { + witness_no_producer_derives_unknown_not_converged() + && witness_unmodeled_phase_is_not_an_observation() + && witness_modeled_phase_can_be_inaccessible() + && witness_unreachable_and_unknown_stay_distinct() + && witness_red_control_widen_on_absent_rejected_by_gate() + && witness_reconcile_covers_added_modified_and_removed() + && witness_matrix_is_hosts_times_spine() + && witness_live_observation_frontier_is_one_cell() + && witness_unmodeled_cells_track_spine_gaps() + && witness_remaining_work_excludes_nothing_silently() +} From 47f91cee90bf23f4a3e20c65bca1447f3d064766 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 17:07:38 +0000 Subject: [PATCH 10/17] WIP: srvN subsumption --- dag/gunbc/host_phase_status.dag | 76 ++++++++++--------- .../claim/host_phase_status_witness_test.dag | 12 +++ 2 files changed, 52 insertions(+), 36 deletions(-) diff --git a/dag/gunbc/host_phase_status.dag b/dag/gunbc/host_phase_status.dag index ae7174096c0..682029a7abe 100644 --- a/dag/gunbc/host_phase_status.dag +++ b/dag/gunbc/host_phase_status.dag @@ -35,60 +35,66 @@ type HostPhaseCell { phase_label: String } -type HostPhaseStatus - = StatusUnmodeled { refusal: String } - | StatusObserved { verdict: ObservationVerdict } - type HostPhaseCellStatus { cell: HostPhaseCell - status: HostPhaseStatus + disposition: PhaseDisposition + observation: ObservationVerdict? } data host_phase_no_producer_is_unknown_not_converged_note: String = "THE fail-closed hinge of this module (DESIGN §5). When a modeled phase has NO live observation producer for a host, the derived verdict is UnknownRefused — never Converged, and never silently omitted from the matrix. The tempting arm is the absorbing fallback in its purest form: nothing is known to be wrong, so report converged; the matrix goes green, the coverage deficit's frequency drops to zero by construction, and the status read becomes a fabricated plausible output exactly like a stats probe that auto-starts the server it is measuring (the DaemonUnsupervised finding, #7213). It is also why UnknownRefused and Inaccessible must stay DISTINCT arms rather than one 'not converged': Inaccessible means we asked the host and could not reach it (remedy: fix reach — the A1 materialized-secret lane); UnknownRefused means we have no way to ask at all (remedy: build the producer). Different states, different owners, different work — and the count of each is the honest measure of how far subsumption actually is. host_phase_status_absorbing_fallback_widen_sketch models the forbidden arm as a RED control so the fold cannot drift back into it unnoticed." -fn host_phase_status_from( - disposition: PhaseDisposition, - observation: ObservationVerdict?, -) -> HostPhaseStatus { - match disposition { - DeclaredGap { interim_realization: _, refusal: r } => StatusUnmodeled { refusal: r } - ModeledCompose { authorities: _ } => - match observation { - Present { value: v } => StatusObserved { verdict: v } - Absent => StatusObserved { verdict: UnknownRefused } - } +fn host_phase_verdict_from(observation: ObservationVerdict?) -> ObservationVerdict { + match observation { + Present { value: v } => v + Absent => UnknownRefused } } -fn host_phase_status_absorbing_fallback_widen_sketch( - disposition: PhaseDisposition, +fn host_phase_verdict_absorbing_fallback_widen_sketch( observation: ObservationVerdict?, -) -> HostPhaseStatus { - match disposition { - DeclaredGap { interim_realization: _, refusal: r } => StatusUnmodeled { refusal: r } - ModeledCompose { authorities: _ } => - match observation { - Present { value: v } => StatusObserved { verdict: v } - Absent => StatusObserved { verdict: Converged } - } +) -> ObservationVerdict { + match observation { + Present { value: v } => v + Absent => Converged } } -fn host_phase_status_gate_accepts( - status: HostPhaseStatus, +fn host_phase_verdict_gate_accepts( + verdict: ObservationVerdict, observation: ObservationVerdict?, ) -> Bool { match observation { Present { value: _ } => true Absent => - match status { - StatusObserved { verdict: Converged } => false - StatusObserved { verdict: _ } => true - StatusUnmodeled { refusal: _ } => true + match verdict { + Converged => false + std.upsert_decision.Absent => true + Drifted => true + Conflict => true + Inaccessible => true + UnknownRefused => true } } } +fn host_phase_cell_verdict(c: HostPhaseCellStatus) -> ObservationVerdict { + host_phase_verdict_from(observation: c.observation) +} + +fn host_phase_cell_is_modeled(c: HostPhaseCellStatus) -> Bool { + match c.disposition { + ModeledCompose { authorities: _ } => true + DeclaredGap { interim_realization: _, refusal: _ } => false + } +} + +fn host_phase_cell_has_live_producer(c: HostPhaseCellStatus) -> Bool { + match c.observation { + Present { value: _ } => true + Absent => false + } +} + data host_phase_observation_frontier_note: String = "The live-observation producer registry, and deliberately a TYPED, COUNTABLE FRONTIER rather than a table of hand-written facts (the self-host frontier shape, DESIGN §7: each cell is either produced or it is a declared absence, never a silent assumption). Exactly one cell has a real producer today — (srv3, prefix:os-install-actuated), which deduces its verdict from an observed DHCP lease table through gunbc.host_standup_assimilation_deduction; that deduction was ALREADY host-parameterized (deduce_os_install_actuation_verdict takes fleet_slot: HostIdentity), so generalizing it was reading the parameter it already had, not writing new machinery. Every other cell returns Absent, which host_phase_status_from renders UnknownRefused. What must NOT happen here is the shape this module exists to kill: hand-entering an observation because someone ssh'd a host once. A probe run by a person is not a modeled producer — encoding its result as a data row would rebuild the parallel ledger the gap-ledger dissolution just removed, and it would go stale in exactly the same way. A cell earns a row here when an effect produces its verdict by execution; until then UnknownRefused is the honest answer and host_phase_observation_coverage_count is the number that measures the debt." fn host_phase_observation(host: HostIdentity, step: HostStandupStep) -> ObservationVerdict? { @@ -106,10 +112,8 @@ fn host_phase_observation(host: HostIdentity, step: HostStandupStep) -> Observat fn host_phase_cell_status(host: HostIdentity, step: HostStandupStep) -> HostPhaseCellStatus { HostPhaseCellStatus { cell: HostPhaseCell { host: host, phase_label: step.label as String }, - status: host_phase_status_from( - disposition: step.disposition, - observation: host_phase_observation(host: host, step: step), - ), + disposition: step.disposition, + observation: host_phase_observation(host: host, step: step), } } diff --git a/dag/test/claim/host_phase_status_witness_test.dag b/dag/test/claim/host_phase_status_witness_test.dag index 0d411e8116a..0cd2f366ee1 100644 --- a/dag/test/claim/host_phase_status_witness_test.dag +++ b/dag/test/claim/host_phase_status_witness_test.dag @@ -146,3 +146,15 @@ test fn host_phase_status_witnesses() -> Bool { && witness_unmodeled_cells_track_spine_gaps() && witness_remaining_work_excludes_nothing_silently() } + +fn debug_coverage_count() -> Int { + host_phase_observation_coverage_count(hosts: fleet_subsumption_hosts) +} + +fn debug_srv3_verdict_rank() -> Int { + observation_verdict_rank(v: srv3_post_install_actuation_verdict(elapsed: millisecond(count: 0))) +} + +fn debug_actuated_label_present() -> Bool { + filter(host_standup_spine, s => (s.label as String) == "prefix:os-install-actuated").length() == 1 +} From efee183c68419934b324d1e5fb6fffa6803c5639 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 17:18:13 +0000 Subject: [PATCH 11/17] WIP: srvN subsumption --- dag/gunbc/host_phase_status.dag | 103 +++++----- .../claim/host_phase_status_witness_test.dag | 185 ++++++++++-------- 2 files changed, 152 insertions(+), 136 deletions(-) diff --git a/dag/gunbc/host_phase_status.dag b/dag/gunbc/host_phase_status.dag index 682029a7abe..c577400d5e8 100644 --- a/dag/gunbc/host_phase_status.dag +++ b/dag/gunbc/host_phase_status.dag @@ -26,7 +26,7 @@ import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv2, oper import product.placement_supply { HostIdentity } import std.measure { millisecond } -data host_phase_status_authority_note: String = "THE per-(host x phase) status axis for the host-standup spine. It exists because the spine could describe itself but not its RELATIONSHIP TO THE LIVE FLEET: every phase carried a PhaseDisposition (is there a modeled authority?) and nothing carried an observation (does this host actually agree with it?). Answering 'where does subsumption stand' therefore meant a session reconstruction — hand ssh probes, prose transcription — and the answer went stale the moment it was written. Two axes, kept ORTHOGONAL on purpose, because collapsing them is the state-space conflation this lane keeps paying for: the MODELED axis is PhaseDisposition, a property of the phase, the same for every host; the LIVE axis is std.upsert_decision.ObservationVerdict, a property of the (host, phase) CELL. A phase can be fully modeled AND Inaccessible on a given host — that is exactly srv1/srv2 for the build-cache phase today — and a single fused enum could not say it. Note what is NOT minted here: no Converged|Diverged|Unreachable|Unmodeled verdict of our own. ObservationVerdict already carries Converged/Absent/Drifted/Conflict/Inaccessible/UnknownRefused, which is STRICTLY FINER on the diverged and unreachable axes, and it is already consumed by twelve modules including host_standup itself; a parallel four-arm verdict beside it would be the §3 nickname, duplicated again in everything derived from it. 'Unmodeled' is likewise not an observation — a host cannot be observed to disagree with a model that does not exist — so it stays on PhaseDisposition and enters this type as the StatusUnmodeled arm, derived from the spine, never authored." +data host_phase_status_authority_note: String = "THE per-(host x phase) status axis for the host-standup spine. It exists because the spine could describe itself but not its RELATIONSHIP TO THE LIVE FLEET: every phase carried a PhaseDisposition (is there a modeled authority?) and nothing carried an observation (does this host actually agree with it?). Answering 'where does subsumption stand' therefore meant a session reconstruction — hand ssh probes, prose transcription — and the answer went stale the moment it was written. Two axes, kept ORTHOGONAL on purpose, because collapsing them is the state-space conflation this lane keeps paying for: the MODELED axis is PhaseDisposition, a property of the phase, the same for every host; the LIVE axis is std.upsert_decision.ObservationVerdict, a property of the (host, phase) CELL. A phase can be fully modeled AND Inaccessible on a given host — that is exactly srv1/srv2 for the build-cache phase today — and a single fused enum could not say it. Note what is NOT minted here: no Converged|Diverged|Unreachable|Unmodeled verdict of our own. ObservationVerdict already carries Converged/Absent/Drifted/Conflict/Inaccessible/UnknownRefused, which is STRICTLY FINER on the diverged and unreachable axes, and it is already consumed by twelve modules including host_standup itself; a parallel four-arm verdict beside it would be the §3 nickname, duplicated again in everything derived from it. 'Unmodeled' is likewise not an observation and does not become a verdict arm — it stays on PhaseDisposition, carried on the cell beside the observation and derived from the spine, never authored. CORRECTION, found by execution 2026-07-25: the cell was FIRST written as a SUM (StatusUnmodeled | StatusObserved), which forced the two axes to be mutually exclusive and made the fold discard the observation on any DeclaredGap phase. The witness caught it immediately, because the single cell that HAS a live producer today is (srv3, prefix:os-install-actuated) — a DeclaredGap phase — so live-observation coverage computed as 0 while a real Converged verdict sat one branch away. The sum was the very conflation this note claims to avoid, written into the type by the same hand that wrote the warning. The cell is now a PRODUCT of both axes, which also gives the lane a state it could not previously say: observed Converged on an unmodeled phase means the host is in the desired condition by means the model cannot reproduce — true of srv3's OS install, and exactly the kind of fact that should never round to either 'modeled' or 'gap'." data host_phase_cell_grain_note: String = "The cell is keyed by (host, phase_label) and NOT by (host, phase) structurally, because phase_label is already the spine's own stable identity for a step (it is what the gap ledger keyed on, what the refusal strings name, and what an operator reads). Keying on the label keeps ONE identity for a phase across the spine, this matrix, and every refusal message, rather than introducing a second notion of phase identity that could disagree with the first. key_of returns identity, never content (membership_reconcile's R2 contract): a cell whose STATUS changes is Modified — the same cell re-derived — not Removed+Added, which would read as a host leaving and rejoining the fleet." @@ -41,7 +41,7 @@ type HostPhaseCellStatus { observation: ObservationVerdict? } -data host_phase_no_producer_is_unknown_not_converged_note: String = "THE fail-closed hinge of this module (DESIGN §5). When a modeled phase has NO live observation producer for a host, the derived verdict is UnknownRefused — never Converged, and never silently omitted from the matrix. The tempting arm is the absorbing fallback in its purest form: nothing is known to be wrong, so report converged; the matrix goes green, the coverage deficit's frequency drops to zero by construction, and the status read becomes a fabricated plausible output exactly like a stats probe that auto-starts the server it is measuring (the DaemonUnsupervised finding, #7213). It is also why UnknownRefused and Inaccessible must stay DISTINCT arms rather than one 'not converged': Inaccessible means we asked the host and could not reach it (remedy: fix reach — the A1 materialized-secret lane); UnknownRefused means we have no way to ask at all (remedy: build the producer). Different states, different owners, different work — and the count of each is the honest measure of how far subsumption actually is. host_phase_status_absorbing_fallback_widen_sketch models the forbidden arm as a RED control so the fold cannot drift back into it unnoticed." +data host_phase_no_producer_is_unknown_not_converged_note: String = "THE fail-closed hinge of this module (DESIGN §5). When a modeled phase has NO live observation producer for a host, the derived verdict is UnknownRefused — never Converged, and never silently omitted from the matrix. The tempting arm is the absorbing fallback in its purest form: nothing is known to be wrong, so report converged; the matrix goes green, the coverage deficit's frequency drops to zero by construction, and the status read becomes a fabricated plausible output exactly like a stats probe that auto-starts the server it is measuring (the DaemonUnsupervised finding, #7213). It is also why UnknownRefused and Inaccessible must stay DISTINCT arms rather than one 'not converged': Inaccessible means we asked the host and could not reach it (remedy: fix reach — the A1 materialized-secret lane); UnknownRefused means we have no way to ask at all (remedy: build the producer). Different states, different owners, different work — and the count of each is the honest measure of how far subsumption actually is. host_phase_verdict_absorbing_fallback_widen_sketch models the forbidden arm as a RED control so the fold cannot drift back into it unnoticed. Note the separation this correction forced: 'has a live producer' is now read from the OBSERVATION being Present, not from the verdict being something other than UnknownRefused — a producer that runs and honestly refuses (an unreadable lease table) is coverage, while no producer at all is not, and the earlier version conflated the two." fn host_phase_verdict_from(observation: ObservationVerdict?) -> ObservationVerdict { match observation { @@ -95,7 +95,7 @@ fn host_phase_cell_has_live_producer(c: HostPhaseCellStatus) -> Bool { } } -data host_phase_observation_frontier_note: String = "The live-observation producer registry, and deliberately a TYPED, COUNTABLE FRONTIER rather than a table of hand-written facts (the self-host frontier shape, DESIGN §7: each cell is either produced or it is a declared absence, never a silent assumption). Exactly one cell has a real producer today — (srv3, prefix:os-install-actuated), which deduces its verdict from an observed DHCP lease table through gunbc.host_standup_assimilation_deduction; that deduction was ALREADY host-parameterized (deduce_os_install_actuation_verdict takes fleet_slot: HostIdentity), so generalizing it was reading the parameter it already had, not writing new machinery. Every other cell returns Absent, which host_phase_status_from renders UnknownRefused. What must NOT happen here is the shape this module exists to kill: hand-entering an observation because someone ssh'd a host once. A probe run by a person is not a modeled producer — encoding its result as a data row would rebuild the parallel ledger the gap-ledger dissolution just removed, and it would go stale in exactly the same way. A cell earns a row here when an effect produces its verdict by execution; until then UnknownRefused is the honest answer and host_phase_observation_coverage_count is the number that measures the debt." +data host_phase_observation_frontier_note: String = "The live-observation producer registry, and deliberately a TYPED, COUNTABLE FRONTIER rather than a table of hand-written facts (the self-host frontier shape, DESIGN §7: each cell is either produced or it is a declared absence, never a silent assumption). Exactly one cell has a real producer today — (srv3, prefix:os-install-actuated), which deduces its verdict from an observed DHCP lease table through gunbc.host_standup_assimilation_deduction; that deduction was ALREADY host-parameterized (deduce_os_install_actuation_verdict takes fleet_slot: HostIdentity), so generalizing it was reading the parameter it already had, not writing new machinery. Every other cell returns Absent, which host_phase_verdict_from renders UnknownRefused. What must NOT happen here is the shape this module exists to kill: hand-entering an observation because someone ssh'd a host once. A probe run by a person is not a modeled producer — encoding its result as a data row would rebuild the parallel ledger the gap-ledger dissolution just removed, and it would go stale in exactly the same way. A cell earns a row here when an effect produces its verdict by execution; until then UnknownRefused is the honest answer and host_phase_observation_coverage_count is the number that measures the debt." fn host_phase_observation(host: HostIdentity, step: HostStandupStep) -> ObservationVerdict? { if (step.label as String) == "prefix:os-install-actuated" { @@ -142,19 +142,13 @@ fn host_phase_cell_key_eq(a: String, b: String) -> Bool { a == b } -fn host_phase_status_eq(a: HostPhaseStatus, b: HostPhaseStatus) -> Bool { - match a { - StatusUnmodeled { refusal: _ } => - match b { - StatusUnmodeled { refusal: _ } => true - StatusObserved { verdict: _ } => false - } - StatusObserved { verdict: va } => - match b { - StatusUnmodeled { refusal: _ } => false - StatusObserved { verdict: vb } => observation_verdict_eq(a: va, b: vb) - } - } +fn host_phase_status_eq(a: HostPhaseCellStatus, b: HostPhaseCellStatus) -> Bool { + let modeled_agrees = host_phase_cell_is_modeled(c: a) == host_phase_cell_is_modeled(c: b) + let verdict_agrees = observation_verdict_eq( + a: host_phase_cell_verdict(c: a), + b: host_phase_cell_verdict(c: b), + ) + modeled_agrees && verdict_agrees } fn observation_verdict_eq(a: ObservationVerdict, b: ObservationVerdict) -> Bool { @@ -173,23 +167,41 @@ fn observation_verdict_rank(v: ObservationVerdict) -> Int { } fn host_phase_cell_status_eq(a: HostPhaseCellStatus, b: HostPhaseCellStatus) -> Bool { - host_phase_cell_key(c: a) == host_phase_cell_key(c: b) - && host_phase_status_eq(a: a.status, b: b.status) + let same_cell = host_phase_cell_key(c: a) == host_phase_cell_key(c: b) + same_cell && host_phase_status_eq(a: a, b: b) } fn host_phase_cell_ownership(c: HostPhaseCellStatus) -> Ownership? { Present { value: Owned } } -data host_phase_reconcile_instantiation_note: String = "The status matrix reconciled as a MEMBERSHIP DIFF — one more (key_of, key_eq, value_eq, ownership_of) bundle handed to the single generic gunbc.membership_reconcile.membership_reconcile, never a forked diff (a forked reconcile means the genericity bought nothing). Desired is every cell at StatusObserved{Converged}: that is the end state of the whole subsumption lane — every phase modeled AND every enrolled host converged on it — so a Modified hunk is precisely one unit of remaining work, and membership_upsert_count is the answer to 'how much is left' as a NUMBER rather than a prose reconstruction. Removed is a real arm, not a degenerate pole: a cell observed for a host no longer in fleet_intent is a host that left the fleet, and cells are Owned, so it tears down rather than refusing. The witness exercises that arm synthetically because the live fleet has no departed host today — an instantiation whose interesting hunks are all unreachable in practice is an instantiation nobody has actually tested." +data host_phase_reconcile_instantiation_note: String = "The status matrix reconciled as a MEMBERSHIP DIFF — one more (key_of, key_eq, value_eq, ownership_of) bundle handed to the single generic gunbc.membership_reconcile.membership_reconcile, never a forked diff (a forked reconcile means the genericity bought nothing). Desired is every cell modeled AND observed Converged: that is the end state of the whole subsumption lane — every phase modeled AND every enrolled host converged on it — so a Modified hunk is precisely one unit of remaining work, and membership_upsert_count is the answer to 'how much is left' as a NUMBER rather than a prose reconstruction. Removed is a real arm, not a degenerate pole: a cell observed for a host no longer in fleet_intent is a host that left the fleet, and cells are Owned, so it tears down rather than refusing. The witness exercises that arm synthetically because the live fleet has no departed host today — an instantiation whose interesting hunks are all unreachable in practice is an instantiation nobody has actually tested." fn host_phase_desired(hosts: List) -> List { map( host_fleet_phase_matrix(hosts: hosts), - c => HostPhaseCellStatus { cell: c.cell, status: StatusObserved { verdict: Converged } }, + c => HostPhaseCellStatus { + cell: c.cell, + disposition: host_phase_desired_disposition(), + observation: Present { value: Converged }, + }, ) } +data host_phase_desired_disposition_note: String = "Desired pins BOTH axes to their end state, not just the verdict: a modeled authority AND an observed Converged. Pinning only the verdict would make a DeclaredGap phase whose host happens to be Converged compare equal to desired — which is exactly srv3 and prefix:os-install-actuated today, a host that IS installed while the actuation that installed it is not reproducible. That cell is real remaining work (the model cannot rebuild the host), so it must produce a hunk; a desired row that ignored the disposition would silently retire it." + +fn host_phase_desired_disposition() -> PhaseDisposition { + ModeledCompose { + authorities: [ + DeclarationRef { + module_path: "gunbc.host_phase_status", + decl_name: "host_phase_desired_disposition", + field: WholeDeclaration, + }, + ] + } +} + fn host_phase_reconcile( desired: List, observed: List, @@ -215,37 +227,18 @@ fn host_phase_remaining_work_count(hosts: List) -> Int { membership_upsert_count(plan: host_phase_fleet_reconcile(hosts: hosts)) } -fn host_phase_cell_has_live_producer(c: HostPhaseCellStatus) -> Bool { - match c.status { - StatusUnmodeled { refusal: _ } => false - StatusObserved { verdict: v } => - match v { - UnknownRefused => false - Converged => true - std.upsert_decision.Absent => true - Drifted => true - Conflict => true - Inaccessible => true - } - } -} - fn host_phase_observation_coverage_count(hosts: List) -> Int { filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_has_live_producer(c: c)).length() } fn host_phase_cell_is_converged(c: HostPhaseCellStatus) -> Bool { - match c.status { - StatusUnmodeled { refusal: _ } => false - StatusObserved { verdict: v } => - match v { - Converged => true - std.upsert_decision.Absent => false - Drifted => false - Conflict => false - Inaccessible => false - UnknownRefused => false - } + match host_phase_cell_verdict(c: c) { + Converged => true + std.upsert_decision.Absent => false + Drifted => false + Conflict => false + Inaccessible => false + UnknownRefused => false } } @@ -253,12 +246,16 @@ fn host_phase_converged_cell_count(hosts: List) -> Int { filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_is_converged(c: c)).length() } +data host_phase_finished_note: String = "FINISHED is both axes at their end state — a modeled authority AND an observed Converged — and it is deliberately stricter than converged. A host that is in the desired condition by unmodeled means is not finished: nothing can rebuild it, so the next host repeats the toil, which is the entire cost this lane exists to remove. srv3's OS install is that cell today. Counting it as done would make the lane's own progress number flatter than the truth in exactly the direction that feels good." + +fn host_phase_cell_is_finished(c: HostPhaseCellStatus) -> Bool { + host_phase_cell_is_modeled(c: c) && host_phase_cell_is_converged(c: c) +} + +fn host_phase_finished_cell_count(hosts: List) -> Int { + filter(host_fleet_phase_matrix(hosts: hosts), c => host_phase_cell_is_finished(c: c)).length() +} + fn host_phase_unmodeled_count(hosts: List) -> Int { - filter( - host_fleet_phase_matrix(hosts: hosts), - c => match c.status { - StatusUnmodeled { refusal: _ } => true - StatusObserved { verdict: _ } => false - }, - ).length() + filter(host_fleet_phase_matrix(hosts: hosts), c => !host_phase_cell_is_modeled(c: c)).length() } diff --git a/dag/test/claim/host_phase_status_witness_test.dag b/dag/test/claim/host_phase_status_witness_test.dag index 0cd2f366ee1..6e57b3645f6 100644 --- a/dag/test/claim/host_phase_status_witness_test.dag +++ b/dag/test/claim/host_phase_status_witness_test.dag @@ -6,7 +6,7 @@ data modeled_phase_fixture: PhaseDisposition = ModeledCompose { authorities: [ DeclarationRef { module_path: "gunbc.host_phase_status", - decl_name: "host_phase_status_from", + decl_name: "host_phase_verdict_from", field: WholeDeclaration, }, ] @@ -17,91 +17,120 @@ data unmodeled_phase_fixture: PhaseDisposition = DeclaredGap { refusal: "host_standup:P4:session-placement-enrollment:unmodeled — refuse until placement enrollment has a .dag authority", } -data witness_no_producer_is_unknown_note: String = "THE fail-closed conjunct. A modeled phase with no live observation producer must derive UnknownRefused — the arm that says 'we have no way to ask this host'. If it ever derives Converged, the status matrix reports a subsumption that was never observed, and every count built on it (remaining work, coverage) silently becomes fiction. This is the same defect class as a stats probe that auto-starts the server it is measuring (#7213 Finding 2): evidence manufactured by the act of looking." - -fn witness_no_producer_derives_unknown_not_converged() -> Bool { - match host_phase_status_from(disposition: modeled_phase_fixture, observation: none) { - StatusObserved { verdict: UnknownRefused } => true - StatusObserved { verdict: _ } => false - StatusUnmodeled { refusal: _ } => false +fn cell_fixture( + label: String, + disposition: PhaseDisposition, + observation: ObservationVerdict?, +) -> HostPhaseCellStatus { + HostPhaseCellStatus { + cell: HostPhaseCell { host: operator_host_srv3, phase_label: label }, + disposition: disposition, + observation: observation, } } -fn witness_unmodeled_phase_is_not_an_observation() -> Bool { - match host_phase_status_from(disposition: unmodeled_phase_fixture, observation: none) { - StatusUnmodeled { refusal: r } => string_contains(s: r, pattern: "refuse until") - StatusObserved { verdict: _ } => false +data witness_no_producer_is_unknown_note: String = "THE fail-closed conjunct. A phase with no live observation producer must derive UnknownRefused — the arm that says 'we have no way to ask this host'. If it ever derives Converged, the status matrix reports a subsumption that was never observed, and every count built on it (remaining work, coverage) silently becomes fiction. This is the same defect class as a stats probe that auto-starts the server it is measuring (#7213 Finding 2): evidence manufactured by the act of looking." + +fn witness_no_producer_derives_unknown_not_converged() -> Bool { + match host_phase_verdict_from(observation: none) { + UnknownRefused => true + Converged => false + std.upsert_decision.Absent => false + Drifted => false + Conflict => false + Inaccessible => false } } -data witness_orthogonality_note: String = "The two axes must stay independent: a phase can be FULLY MODELED and still Inaccessible on a given host — which is exactly srv1 and srv2 for the build-cache phase today, where the model is complete and the hosts refuse every fleet credential. A single fused status enum could not represent that cell, and would have to round it to either 'modeled' (hiding the live failure, which is how the stale status table read) or 'gap' (slandering a model that is finished). This conjunct pins the cell that proves the axes are separable." +data witness_orthogonality_note: String = "The two axes must stay independent, and this is the conjunct that CAUGHT them being fused. The cell type was first written as a sum (StatusUnmodeled | StatusObserved), so a DeclaredGap phase discarded its observation — and the one cell with a live producer today, (srv3, prefix:os-install-actuated), is a DeclaredGap phase, so coverage computed as zero with a real Converged verdict one branch away. Four combinations must all be representable and distinct: modeled+converged (done), modeled+inaccessible (srv1/srv2 build-cache — a finished model the host refuses to answer for), unmodeled+unknown (ordinary remaining work), and unmodeled+converged (the host is in the desired condition by means the model cannot reproduce — srv3's OS install). A fused enum has to round the middle two to something false." -fn witness_modeled_phase_can_be_inaccessible() -> Bool { - match host_phase_status_from( +fn witness_modeled_and_observed_axes_are_independent() -> Bool { + let modeled_inaccessible = cell_fixture( + label: "P1b:build-cache-provision", disposition: modeled_phase_fixture, - observation: Present { value: Inaccessible }, - ) { - StatusObserved { verdict: Inaccessible } => true - StatusObserved { verdict: _ } => false - StatusUnmodeled { refusal: _ } => false - } + observation: Present { value: std.upsert_decision.Inaccessible }, + ) + let unmodeled_converged = cell_fixture( + label: "prefix:os-install-actuated", + disposition: unmodeled_phase_fixture, + observation: Present { value: std.upsert_decision.Converged }, + ) + let unmodeled_unknown = cell_fixture( + label: "P4:session-placement-enrollment", + disposition: unmodeled_phase_fixture, + observation: none, + ) + host_phase_cell_is_modeled(c: modeled_inaccessible) + && !host_phase_cell_is_converged(c: modeled_inaccessible) + && host_phase_cell_has_live_producer(c: modeled_inaccessible) + && !host_phase_cell_is_modeled(c: unmodeled_converged) + && host_phase_cell_is_converged(c: unmodeled_converged) + && host_phase_cell_has_live_producer(c: unmodeled_converged) + && !host_phase_cell_is_modeled(c: unmodeled_unknown) + && !host_phase_cell_is_converged(c: unmodeled_unknown) + && !host_phase_cell_has_live_producer(c: unmodeled_unknown) +} + +data witness_producer_refusal_is_coverage_note: String = "A producer that RAN and honestly refused is coverage; no producer at all is not. The distinction is load-bearing because the two have different owners — a refusing producer is a reach or observation defect to fix, an absent producer is a model to build — and the first version of this module conflated them by reading coverage off the verdict instead of off the observation's presence." + +fn witness_refusing_producer_still_counts_as_coverage() -> Bool { + let refused = cell_fixture( + label: "prefix:os-install-actuated", + disposition: unmodeled_phase_fixture, + observation: Present { value: std.upsert_decision.UnknownRefused }, + ) + let absent = cell_fixture( + label: "prefix:os-install-actuated", + disposition: unmodeled_phase_fixture, + observation: none, + ) + host_phase_cell_has_live_producer(c: refused) + && !host_phase_cell_has_live_producer(c: absent) } fn witness_unreachable_and_unknown_stay_distinct() -> Bool { - !observation_verdict_eq(a: Inaccessible, b: UnknownRefused) - && observation_verdict_eq(a: Inaccessible, b: Inaccessible) + !observation_verdict_eq(a: std.upsert_decision.Inaccessible, b: std.upsert_decision.UnknownRefused) + && observation_verdict_eq(a: std.upsert_decision.Inaccessible, b: std.upsert_decision.Inaccessible) } -data witness_widen_red_control_note: String = "The discriminating RED control, built on the PATH-shadow / DaemonUnsupervised precedent: the forbidden absorbing fallback is modeled as its own sketch (host_phase_status_absorbing_fallback_widen_sketch fabricates Converged when no observation exists), the gate REJECTS the sketch's output, and the authority's output PASSES the same gate. The perturbation is independent of the property checked, so this cannot pass tautologically — an authority that quietly acquired the widen arm would be rejected by the gate it currently satisfies." +data witness_widen_red_control_note: String = "The discriminating RED control, built on the PATH-shadow / DaemonUnsupervised precedent: the forbidden absorbing fallback is modeled as its own sketch (host_phase_verdict_absorbing_fallback_widen_sketch fabricates Converged when no observation exists), the gate REJECTS the sketch's output, and the authority's output PASSES the same gate. The perturbation is independent of the property checked, so this cannot pass tautologically — an authority that quietly acquired the widen arm would be rejected by the gate it currently satisfies." fn witness_red_control_widen_on_absent_rejected_by_gate() -> Bool { - match host_phase_status_absorbing_fallback_widen_sketch( - disposition: modeled_phase_fixture, - observation: none, - ) { - StatusObserved { verdict: Converged } => true - StatusObserved { verdict: _ } => false - StatusUnmodeled { refusal: _ } => false - } && !host_phase_status_gate_accepts( - status: host_phase_status_absorbing_fallback_widen_sketch( - disposition: modeled_phase_fixture, - observation: none, - ), - observation: none, - ) - && host_phase_status_gate_accepts( - status: host_phase_status_from(disposition: modeled_phase_fixture, observation: none), - observation: none, - ) + let widened = host_phase_verdict_absorbing_fallback_widen_sketch(observation: none) + let authority = host_phase_verdict_from(observation: none) + observation_verdict_eq(a: widened, b: std.upsert_decision.Converged) + && !host_phase_verdict_gate_accepts(verdict: widened, observation: none) + && host_phase_verdict_gate_accepts(verdict: authority, observation: none) } data departed_host_fixture: HostIdentity = "srv-departed" as HostIdentity -fn departed_cell_fixture() -> HostPhaseCellStatus { - HostPhaseCellStatus { - cell: HostPhaseCell { host: departed_host_fixture, phase_label: "P1b:build-cache-provision" }, - status: StatusObserved { verdict: Converged }, - } -} - -data witness_reconcile_non_vacuous_note: String = "The membership instantiation must be exercised on a NON-DEGENERATE diff, or it is an instantiation nobody has tested. The live fleet produces only Modified and Unchanged hunks today (no host has left), so the Removed arm — a cell observed for a host absent from fleet_intent — is supplied synthetically here. All three arms are asserted in one reconcile: a departed host's cell tears down (cells are Owned, so R5 permits it rather than refusing), an unconverged cell upserts, and a converged cell produces no hunk at all." +data witness_reconcile_non_vacuous_note: String = "The membership instantiation must be exercised on a NON-DEGENERATE diff, or it is an instantiation nobody has tested. The live fleet produces only Modified and Unchanged hunks today (no host has left), so the Removed arm — a cell observed for a host absent from fleet_intent — is supplied synthetically here. All three outcomes are asserted in one reconcile: a departed host's cell tears down (cells are Owned, so R5 permits it rather than refusing), an unconverged cell upserts, and a cell already at the desired state produces no hunk at all." -fn witness_reconcile_covers_added_modified_and_removed() -> Bool { - let converged_cell = HostPhaseCellStatus { - cell: HostPhaseCell { host: operator_host_srv3, phase_label: "P3:green-place-readiness" }, - status: StatusObserved { verdict: Converged }, - } - let unconverged_cell = HostPhaseCellStatus { - cell: HostPhaseCell { host: operator_host_srv3, phase_label: "P1b:build-cache-provision" }, - status: StatusObserved { verdict: UnknownRefused }, - } +fn witness_reconcile_covers_upsert_teardown_and_noop() -> Bool { + let at_desired = cell_fixture( + label: "P3:green-place-readiness", + disposition: modeled_phase_fixture, + observation: Present { value: std.upsert_decision.Converged }, + ) + let unconverged = cell_fixture( + label: "P1b:build-cache-provision", + disposition: modeled_phase_fixture, + observation: none, + ) let desired_unconverged = HostPhaseCellStatus { - cell: unconverged_cell.cell, - status: StatusObserved { verdict: Converged }, + cell: unconverged.cell, + disposition: modeled_phase_fixture, + observation: Present { value: std.upsert_decision.Converged }, + } + let departed = HostPhaseCellStatus { + cell: HostPhaseCell { host: departed_host_fixture, phase_label: "P1b:build-cache-provision" }, + disposition: modeled_phase_fixture, + observation: Present { value: std.upsert_decision.Converged }, } let plan = host_phase_reconcile( - desired: [converged_cell, desired_unconverged], - observed: [converged_cell, unconverged_cell, departed_cell_fixture()], + desired: [at_desired, desired_unconverged], + observed: [at_desired, unconverged, departed], ) plan.actions.length() == 2 && membership_upsert_count(plan: plan) == 1 @@ -109,7 +138,7 @@ fn witness_reconcile_covers_added_modified_and_removed() -> Bool { && membership_refusal_count(plan: plan) == 0 } -data witness_matrix_shape_note: String = "Shape assertions over the derived matrix, pinned to the spine and the enrolled fleet rather than to hand-copied numbers: the matrix is exactly (hosts x spine steps), so it cannot silently drop a phase or a host. The coverage count is the honest measure of the live-observation frontier — one cell has a real producer today ((srv3, prefix:os-install-actuated)), and that number is what items 2 and 3 of the lane exist to raise. Pinning it means adding a producer is a VISIBLE, counted event that must update this witness, never a silent improvement nobody can point at." +data witness_matrix_shape_note: String = "Shape assertions over the derived matrix, pinned to the spine and the enrolled fleet rather than to hand-copied numbers: the matrix is exactly (hosts x spine steps), so it cannot silently drop a phase or a host. The coverage count is the honest measure of the live-observation frontier — one cell has a real producer today, (srv3, prefix:os-install-actuated) — and that number is what items 2 and 3 of the lane exist to raise. Pinning it means adding a producer is a VISIBLE, counted event that must update this witness, never a silent improvement nobody can point at." fn witness_matrix_is_hosts_times_spine() -> Bool { let cells = host_fleet_phase_matrix(hosts: fleet_subsumption_hosts).length() @@ -127,34 +156,24 @@ fn witness_unmodeled_cells_track_spine_gaps() -> Bool { unmodeled == expected } -fn witness_remaining_work_excludes_nothing_silently() -> Bool { +data witness_remaining_work_note: String = "Remaining work is the reconcile's own upsert count, and it must equal every cell that is not already at the FULL desired state — modeled AND converged. Asserting it against an independently computed count is what stops the reconcile from silently retiring cells: if desired ever weakened to 'converged, disposition ignored', srv3's installed-but-unmodeled OS cell would drop out of the count and the lane would look one item closer to done than it is." + +fn witness_remaining_work_counts_every_unfinished_cell() -> Bool { let remaining = host_phase_remaining_work_count(hosts: fleet_subsumption_hosts) let total = host_fleet_phase_matrix(hosts: fleet_subsumption_hosts).length() - let converged = host_phase_converged_cell_count(hosts: fleet_subsumption_hosts) - remaining == total - converged + let finished = host_phase_finished_cell_count(hosts: fleet_subsumption_hosts) + remaining == total - finished } test fn host_phase_status_witnesses() -> Bool { witness_no_producer_derives_unknown_not_converged() - && witness_unmodeled_phase_is_not_an_observation() - && witness_modeled_phase_can_be_inaccessible() + && witness_modeled_and_observed_axes_are_independent() + && witness_refusing_producer_still_counts_as_coverage() && witness_unreachable_and_unknown_stay_distinct() && witness_red_control_widen_on_absent_rejected_by_gate() - && witness_reconcile_covers_added_modified_and_removed() + && witness_reconcile_covers_upsert_teardown_and_noop() && witness_matrix_is_hosts_times_spine() && witness_live_observation_frontier_is_one_cell() && witness_unmodeled_cells_track_spine_gaps() - && witness_remaining_work_excludes_nothing_silently() -} - -fn debug_coverage_count() -> Int { - host_phase_observation_coverage_count(hosts: fleet_subsumption_hosts) -} - -fn debug_srv3_verdict_rank() -> Int { - observation_verdict_rank(v: srv3_post_install_actuation_verdict(elapsed: millisecond(count: 0))) -} - -fn debug_actuated_label_present() -> Bool { - filter(host_standup_spine, s => (s.label as String) == "prefix:os-install-actuated").length() == 1 + && witness_remaining_work_counts_every_unfinished_cell() } From 3a4e6c2b81c0e0cb5f1fa9a8a6afaccef1e0ec32 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 17:28:45 +0000 Subject: [PATCH 12/17] WIP: srvN subsumption --- dag/gunbc/host_standup.dag | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dag/gunbc/host_standup.dag b/dag/gunbc/host_standup.dag index b8bef129ebd..105aabfdc46 100644 --- a/dag/gunbc/host_standup.dag +++ b/dag/gunbc/host_standup.dag @@ -309,6 +309,8 @@ data host_standup_spine: List = [ ), ] +data host_standup_gap_ledger_parallel_representation_note: String = "🟡 dissolve-on: this ledger is a PARALLEL REPRESENTATION of host_standup_spine and is declared as one rather than left ambient (DESIGN §3; an honestly-marked scaffold duplicating a canonical fact is still a violation). Twelve rows are hand-written beside the twelve spine steps, and `modeling` is a String carrying five values — modeled / modeled-new-authority / partial / gap / gap-shape-only — where PhaseDisposition has two arms. Nothing derives one from the other, so they are free to drift, and the drift is invisible: p0_gap_ledger_matches_spine_partial_authorities exists only because the ledger CAN disagree with the spine, which is validation standing where construction was available (§5). It was also the source consulted to answer 'where does subsumption stand', so a stale string became a status report. WHY IT CANNOT SIMPLY BE DERIVED TODAY, which is the real finding: PhaseDisposition is a SUM, so authorities and interim_realization are mutually exclusive — and two live phases need BOTH. P0:reach-secrets-network has modeled ACL authorities AND an unmodeled live upsert; P3:green-place-readiness has a landed gunbc authority AND a ctrl writer (green_place.dag, read-gunbc-pin.sh). Neither fact is representable, so it was pushed into this ledger's prose, which is precisely what the ledger is FOR. That is the same sum-where-a-product-belongs defect that gunbc.host_phase_status.HostPhaseCellStatus was first written with and corrected. DISSOLVES WHEN PhaseDisposition becomes a product — authorities: List alongside interim: PhaseInterim? — at which point 'modeled' is authorities-nonempty-and-no-interim, 'partial' is both-present, 'gap' is interim-only, every row here becomes a projection of the spine, and this table is deleted. Deliberately NOT bundled into the status-axis change: it re-shapes fourteen spine rows in a load-bearing file, and the two changes should be reviewable apart." + data host_standup_gap_ledger: List = [ GapLedgerRow { phase_label: "prefix:bmc-credential-converge", From 979d2aae5062d5c59d0f5c5686cc375770d6e5e2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 18:54:15 +0000 Subject: [PATCH 13/17] WIP: srvN subsumption --- dag/gunbc/runner_host_deploy.dag | 89 +++++++++++++++++++++++++++++++- 1 file changed, 87 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/runner_host_deploy.dag b/dag/gunbc/runner_host_deploy.dag index 62bdb7820df..c9631c43998 100644 --- a/dag/gunbc/runner_host_deploy.dag +++ b/dag/gunbc/runner_host_deploy.dag @@ -7,6 +7,8 @@ import gunbc.fleet_secrets_config { fleet_secrets_gcp_project } import extdeps.cache.sccache { SccacheBinaryRelease, sccache_release_0_15_0, sccache_install_script } import extdeps.crypto.hash { Digest, sha256_digest } import extdeps.container.docker_ce { docker_ce_apt_repo_noble_arm64, docker_ce_packages, docker_ce_repo_install_script } +import gunbc.fleet_intent { fleet_intent_known_hosts } +import product.placement_supply { HostIdentity } data runner_host_deploy_citation: String = "§3 cite-upstream, do-not-re-coin: GitHub Actions runner host provisioning is realized by the ctrl installer at ctrl:scripts/session-dashboard/host/ (deploy-runner-hosts.sh and install-actions-runner.sh) — the single battle-tested rotation point (GitHub App key distribution, jit-runner.sh ephemeral wrapper, actions-runner service template, ghrunner de-priv job user plus rootless docker for public-PR isolation, per-slot cgroup caps). RunnerHostDeploy models the typed INTERFACE (which host, label, runner user, de-priv job user, App-key secret, slot count); the installer is the bound realization HANDLER, one of N transports, NOT re-implemented in .dag. DISSOLVES WHEN host_effect_apply binds RunnerHostDeploy through a transport handler that invokes the cited installer plus per-slot provisioning without a hand-run shell step." @@ -70,7 +72,39 @@ fn runner_host_sccache_provision_aarch64() -> String { ) } -fn runner_host_installer_command(deploy: RunnerHostDeploy, installer_path: NonEmptyStr, pem_src_path: NonEmptyStr) -> ArgvCommand { +data runner_host_enrollment_wall_note: String = "THE ENROLLMENT WALL, and it is CONSTRUCTION rather than a check (DESIGN §5). A host takes no fleet work until it is a row in gunbc.fleet_intent.fleet_intent_known_hosts. This is the standing rule the srv4 host-convergence OOM priced (gunbc.plans.fleet_subsumption_manual_gaps section C): converge emitted against an unenrolled host derives NOTHING for it — or worse, stamps template drop-ins carrying ANOTHER host's widths — and the enrolled intent row is exactly where runner_deployment_plan's conservation wall gets the host RAM it needs to check whether N runners at the declared caps even fit, refusing PlanUnsound if not. The incident is prevented by arithmetic, and the arithmetic has no inputs until the host is enrolled. Why construction and not a validating predicate: a fleet_intent_admits_host(deploy) check returning Bool concedes that the unenrolled command IS constructible and merely asks callers to look first — one forgotten call site and the incident class is back. Instead there is NO function in this module that takes a bare RunnerHostDeploy and yields an ArgvCommand: the command builders consume a RunnerHostAdmission, and the refusal arm carries no command at all, so 'run the installer on an unenrolled host' is unrepresentable rather than discouraged (the EffectsOrRefusal shape already blessed in gunbc.membership_reconcile). HONEST RESIDUAL, stated rather than papered over: .dag has no visibility modifiers yet, so a caller CAN hand-write RunnerHostEnrolled { deploy } for an unenrolled host. That is now an explicit lie in the source rather than an accident of a forgotten check — the strongest wall this substrate currently supports. It closes fully when node/subtree visibility grants land (DESIGN open thread: 'node/subtree visibility grants'), at which point the Enrolled constructor becomes private to this module and the evidence is unforgeable." + +type RunnerHostAdmission + = RunnerHostEnrolled { deploy: RunnerHostDeploy } + | RunnerHostUnenrolled { host_label: NonEmptyStr, reason: NonEmptyStr } + +type RunnerCommandOrRefusal + = RunnerCommandReady { command: ArgvCommand } + | RunnerCommandRefused { host_label: NonEmptyStr, reason: NonEmptyStr } + +fn fleet_intent_enrolls_host_label(label: NonEmptyStr) -> Bool { + fold( + fleet_intent_known_hosts, + init: false, + f: (acc, h) => acc || (h.identity as String) == (label as String), + ) +} + +fn admit_runner_host(deploy: RunnerHostDeploy) -> RunnerHostAdmission { + if fleet_intent_enrolls_host_label(label: deploy.host_label) { + RunnerHostEnrolled { deploy: deploy } + } else { + RunnerHostUnenrolled { + host_label: deploy.host_label, + reason: concat( + concat("runner_host_deploy: host '", deploy.host_label as String), + "' is absent from gunbc.fleet_intent.fleet_intent_known_hosts; it takes no fleet work until it is an intent row with a converge receipt. Enrolling it is what gives runner_deployment_plan the host RAM to check the slot caps against. Fail-closed, no unenrolled install.", + ) as NonEmptyStr, + } + } +} + +fn runner_host_installer_command_argv(deploy: RunnerHostDeploy, installer_path: NonEmptyStr, pem_src_path: NonEmptyStr) -> ArgvCommand { ArgvCommand { argv: [ "env", @@ -83,6 +117,25 @@ fn runner_host_installer_command(deploy: RunnerHostDeploy, installer_path: NonEm } } +fn runner_host_installer_command( + admission: RunnerHostAdmission, + installer_path: NonEmptyStr, + pem_src_path: NonEmptyStr, +) -> RunnerCommandOrRefusal { + match admission { + RunnerHostEnrolled { deploy: d } => + RunnerCommandReady { + command: runner_host_installer_command_argv( + deploy: d, + installer_path: installer_path, + pem_src_path: pem_src_path, + ) + } + RunnerHostUnenrolled { host_label: l, reason: r } => + RunnerCommandRefused { host_label: l, reason: r } + } +} + fn runner_instance_name(deploy: RunnerHostDeploy, index: Int) -> String { let two = if index < 10 { join(["0", to_string(index)], "") } else { to_string(index) } join([deploy.host_label as String, "-", two], "") @@ -100,7 +153,7 @@ fn runner_instance_names(deploy: RunnerHostDeploy) -> List { map(runner_index_seq(n: deploy.runner_count), i => runner_instance_name(deploy: deploy, index: i)) } -fn runner_enable_command(deploy: RunnerHostDeploy) -> ArgvCommand { +fn runner_enable_command_argv(deploy: RunnerHostDeploy) -> ArgvCommand { ArgvCommand { argv: append( ["sudo", "systemctl", "enable", "--now"], @@ -108,3 +161,35 @@ fn runner_enable_command(deploy: RunnerHostDeploy) -> ArgvCommand { ), } } + +fn runner_enable_command(admission: RunnerHostAdmission) -> RunnerCommandOrRefusal { + match admission { + RunnerHostEnrolled { deploy: d } => + RunnerCommandReady { command: runner_enable_command_argv(deploy: d) } + RunnerHostUnenrolled { host_label: l, reason: r } => + RunnerCommandRefused { host_label: l, reason: r } + } +} + +data runner_host_unenrolled_widen_sketch_note: String = "RED-control fixture modeling the forbidden arm: an admission-blind builder that hands back a runnable command for a host the fleet never enrolled. This is what the module looked like before the wall, and it is what the srv4 incident ran through. It must never ship as the authority; runner_host_admission_gate_accepts rejects it." + +fn runner_command_admission_blind_widen_sketch( + deploy: RunnerHostDeploy, + admission: RunnerHostAdmission, +) -> RunnerCommandOrRefusal { + RunnerCommandReady { command: runner_enable_command_argv(deploy: deploy) } +} + +fn runner_host_admission_gate_accepts( + outcome: RunnerCommandOrRefusal, + admission: RunnerHostAdmission, +) -> Bool { + match admission { + RunnerHostEnrolled { deploy: _ } => true + RunnerHostUnenrolled { host_label: _, reason: _ } => + match outcome { + RunnerCommandReady { command: _ } => false + RunnerCommandRefused { host_label: _, reason: _ } => true + } + } +} From 3ff45a4b5a22c7294a5b103378b5a3be672a5924 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 19:06:48 +0000 Subject: [PATCH 14/17] WIP: srvN subsumption --- .../claim/runner_host_deploy_witness_test.dag | 81 ++++++++++++++++++- 1 file changed, 77 insertions(+), 4 deletions(-) diff --git a/dag/test/claim/runner_host_deploy_witness_test.dag b/dag/test/claim/runner_host_deploy_witness_test.dag index faccea2ef1e..ec95253638b 100644 --- a/dag/test/claim/runner_host_deploy_witness_test.dag +++ b/dag/test/claim/runner_host_deploy_witness_test.dag @@ -11,6 +11,17 @@ import gunbc.runner_host_deploy { runner_enable_command, runner_host_docker_provision_script, runner_host_sccache_provision_script, + RunnerHostDeploy, + RunnerHostAdmission, + RunnerHostEnrolled, + RunnerHostUnenrolled, + RunnerCommandOrRefusal, + RunnerCommandReady, + RunnerCommandRefused, + admit_runner_host, + fleet_intent_enrolls_host_label, + runner_command_admission_blind_widen_sketch, + runner_host_admission_gate_accepts, } import gunbc.fleet_intent { fleet_intent_execution_surface } import extdeps.toolchain.types { ToolchainCapability } @@ -35,11 +46,15 @@ test fn fleet_surface_no_longer_lies_declares_sccache() -> Bool { } test fn srv4_runner_installer_command_cites_installer_with_env() -> Bool { - let c = shell_command_render(command: runner_host_installer_command( - deploy: srv4_runner_host_deploy, + let outcome = runner_host_installer_command( + admission: admit_runner_host(deploy: srv4_runner_host_deploy), installer_path: "/tmp/install-actions-runner.sh", pem_src_path: "/tmp/app.pem", - )) + ) + let c = match outcome { + RunnerCommandReady { command: cmd } => shell_command_render(command: cmd) + RunnerCommandRefused { host_label: _, reason: _ } => "" + } string_contains(s: c, pattern: "'CTRL_RUNNER_HOST_LABEL=srv4'") && string_contains(s: c, pattern: "'CTRL_RUNNER_JOB_USER=ghrunner'") && string_contains(s: c, pattern: "'CTRL_RUNNER_APP_PEM_SRC=/tmp/app.pem'") @@ -53,10 +68,68 @@ test fn srv4_runner_app_from_secret_manager() -> Bool { test fn srv4_enables_five_named_runner_instances() -> Bool { let names = runner_instance_names(deploy: srv4_runner_host_deploy) - let enable = shell_command_render(command: runner_enable_command(deploy: srv4_runner_host_deploy)) + let enable = match runner_enable_command(admission: admit_runner_host(deploy: srv4_runner_host_deploy)) { + RunnerCommandReady { command: cmd } => shell_command_render(command: cmd) + RunnerCommandRefused { host_label: _, reason: _ } => "" + } list_length(items: names) == 5 && string_contains(s: enable, pattern: "'actions-runner@srv4-01.service'") && string_contains(s: enable, pattern: "'actions-runner@srv4-05.service'") && (string_contains(s: enable, pattern: "srv4-06") == false) && string_contains(s: enable, pattern: "'sudo' 'systemctl' 'enable' '--now'") } + +data unenrolled_host_fixture: RunnerHostDeploy = RunnerHostDeploy { + host_label: "srv9", + ssh_target: "briansrls@192.168.1.250", + runner_user: "briansrls", + job_user: "ghrunner", + app: gunbc_ci_github_app, + runner_count: 5, +} + +data witness_enrollment_wall_note: String = "The srv4 host-convergence OOM class, made unwritable. A host absent from fleet_intent_known_hosts yields an admission whose refusal arm carries NO command, so neither builder can hand back something runnable. The fixture is srv9 — a plausible next fleet host that nobody has enrolled — which is exactly the shape the incident took: real hardware, real ssh target, no intent row, and therefore no RAM figure for the conservation wall to check slot caps against." + +test fn unenrolled_host_cannot_produce_an_installer_command() -> Bool { + match runner_host_installer_command( + admission: admit_runner_host(deploy: unenrolled_host_fixture), + installer_path: "/tmp/install-actions-runner.sh", + pem_src_path: "/tmp/app.pem", + ) { + RunnerCommandRefused { host_label: l, reason: r } => + (l as String) == "srv9" + && string_contains(s: r as String, pattern: "fleet_intent_known_hosts") + && string_contains(s: r as String, pattern: "Fail-closed") + RunnerCommandReady { command: _ } => false + } +} + +test fn unenrolled_host_cannot_enable_runner_units() -> Bool { + match runner_enable_command(admission: admit_runner_host(deploy: unenrolled_host_fixture)) { + RunnerCommandRefused { host_label: _, reason: _ } => true + RunnerCommandReady { command: _ } => false + } +} + +test fn enrolled_host_still_admits() -> Bool { + fleet_intent_enrolls_host_label(label: "srv4") + && !fleet_intent_enrolls_host_label(label: "srv9") + && match admit_runner_host(deploy: srv4_runner_host_deploy) { + RunnerHostEnrolled { deploy: _ } => true + RunnerHostUnenrolled { host_label: _, reason: _ } => false + } +} + +data witness_admission_red_control_note: String = "Discriminating RED control on the PATH-shadow precedent: the admission-blind sketch (what this module was before the wall) DOES hand back a runnable command for the unenrolled host, the gate rejects it, and the authority's refusal passes the same gate. The perturbation is independent of the property checked, so the conjunct cannot pass tautologically." + +test fn red_control_admission_blind_builder_rejected_by_gate() -> Bool { + let adm = admit_runner_host(deploy: unenrolled_host_fixture) + let widened = runner_command_admission_blind_widen_sketch(deploy: unenrolled_host_fixture, admission: adm) + let authority = runner_enable_command(admission: adm) + match widened { + RunnerCommandReady { command: _ } => true + RunnerCommandRefused { host_label: _, reason: _ } => false + } + && !runner_host_admission_gate_accepts(outcome: widened, admission: adm) + && runner_host_admission_gate_accepts(outcome: authority, admission: adm) +} From e794fbc63c75a6225749b20518719c03aa82cdbc Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 19:17:15 +0000 Subject: [PATCH 15/17] WIP: srvN subsumption --- dag/gunbc/host_swap_backing.dag | 143 ++++++++++++++++++ dag/gunbc/readback_independence.dag | 101 +++++++++++++ .../claim/host_swap_backing_witness_test.dag | 114 ++++++++++++++ .../readback_independence_witness_test.dag | 122 +++++++++++++++ 4 files changed, 480 insertions(+) create mode 100644 dag/gunbc/host_swap_backing.dag create mode 100644 dag/gunbc/readback_independence.dag create mode 100644 dag/test/claim/host_swap_backing_witness_test.dag create mode 100644 dag/test/claim/readback_independence_witness_test.dag diff --git a/dag/gunbc/host_swap_backing.dag b/dag/gunbc/host_swap_backing.dag new file mode 100644 index 00000000000..8fcd055e902 --- /dev/null +++ b/dag/gunbc/host_swap_backing.dag @@ -0,0 +1,143 @@ +module gunbc.host_swap_backing + +import std.types { String, NonEmptyStr, Bool, Int, List } +import std.measure { ByteSize, byte_size, byte_size_count } +import std.upsert_decision { ObservationVerdict, Converged, Drifted, Conflict, Inaccessible, UnknownRefused } +import std.disposition { Disposition, Scaffold, SingleAuthority } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.os.free { SwapStats } +import gunbc.runner_slot_allocation { gunbc_runner_slot_desired } +import gunbc.host_phase_status { observation_verdict_eq, fleet_subsumption_hosts } +import gunbc.readback_independence { readback_evidence_verdict, proc_swaps_read_probe } +import product.placement_supply { HostIdentity } + +data host_swap_backing_authority_note: String = "THE host swap-BACKING axis, and it exists because the corpus already converges a swap CAP over a resource whose existence nothing models. gunbc.runner_slot_allocation declares memory_swap_max = 34359738368 (32 GiB) per runner slot; gunbc.host_converge drives it onto every host as MemorySwapMax through the per-slot drop-in at gunbc_runner_per_slot_swap_dropin_path, and gunbc.runner_unit_live_read reads it back and reports Converged when the cgroup property matches. Every one of those steps is correct in isolation and the composition still proves nothing, because MemorySwapMax is a CEILING: systemd accepts it, reports it, and matches it byte-for-byte on a host with zero swap devices. The knob converges green over a resource that does not exist. That is the presupposition failure this module makes representable — a cap is evidence about a resource only once the resource is observed present — and it is the shape DESIGN §5 calls a fabricated plausible output: not a wrong value, a value whose meaning was assumed. What is NOT minted here: no swap-specific verdict enum (std.upsert_decision.ObservationVerdict already spans Converged/Absent/Drifted/Conflict/Inaccessible/UnknownRefused) and no swap observation carrier (extdeps.os.free.SwapStats is the cited one, grounded on the free(1) man page, and it is reused verbatim rather than re-decomposed here)." + +data host_swap_backing_requirement_is_derived_note: String = "The requirement is DERIVED from the declared cap, never authored per host, and that is the whole reason this module can exist without fabricating anything. Nobody in this session can read /proc/swaps on srv1..srv4 — the reach gap is the A1 lane — so any table of per-host swap sizes written here would be invention dressed as a model. The derivation needs no such reading: declaring a nonzero MemorySwapMax IS declaring that swap backing must exist, so the requirement falls out of gunbc_runner_slot_desired().memory_swap_max, and it moves automatically when that number moves. DECLARED LIMIT, stated rather than papered over: min_total is the PER-SLOT cap, the amount a single runner alone can demand, and not slots-per-host x cap. Whether five concurrent slots can each reach their ceiling is an aggregate-scheduling question this module does not answer, and answering it by multiplication would assert a worst case nobody has measured. So the requirement is a floor below which the declared caps are provably unsatisfiable, and it is honest about being a floor." + +type SwapBackingRequirement + = SwapBackingRequired { min_total: ByteSize, requiring_declaration: DeclarationRef } + | SwapBackingNotRequired + +fn host_swap_backing_requirement() -> SwapBackingRequirement { + let cap = gunbc_runner_slot_desired().memory_swap_max + if byte_size_count(b: cap) > 0 { + SwapBackingRequired { + min_total: cap, + requiring_declaration: DeclarationRef { + module_path: "gunbc.runner_slot_allocation", + decl_name: "gunbc_runner_slot_desired", + field: WholeDeclaration, + }, + } + } else { + SwapBackingNotRequired + } +} + +data host_swap_backing_verdict_note: String = "The fail-closed fold, with each arm answering a different question so the remedies stay separable. No observation at all is UnknownRefused: nothing on this host can be asked about swap today, and the fix is to BUILD the producer. An observed total of zero is Absent: the host answered, and the answer is that the backing the caps presuppose is not there — the fix is to PROVISION it. An observed total below the requirement is Drifted: backing exists and is too small, so the fix is to RESIZE. Collapsing any two of those into one arm is the state-space conflation this lane keeps paying for; they have different owners and their counts measure different things. Note the arm that is deliberately absent: there is no 'assume the distro default gave us swap'. Ubuntu server images ship with swap configured sometimes and not others depending on installer path, and srv1..srv4 were installed across at least two paths (the srv3/srv4 BMC virtual-media route and whatever preceded it), so a default-assuming arm would be a guess whose error rate is unmeasurable by construction." + +fn swap_stats_total_bytes(s: SwapStats) -> Int { + byte_size_count(b: s.total) +} + +fn host_swap_backing_verdict_for_stats(min_total: ByteSize, s: SwapStats) -> ObservationVerdict { + let total = swap_stats_total_bytes(s: s) + if total == 0 { + std.upsert_decision.Absent + } else { + if total < byte_size_count(b: min_total) { Drifted } else { Converged } + } +} + +fn host_swap_backing_verdict( + req: SwapBackingRequirement, + observed: SwapStats?, +) -> ObservationVerdict { + match req { + SwapBackingNotRequired => Converged + SwapBackingRequired { min_total: m, requiring_declaration: d } => + match observed { + Present { value: s } => host_swap_backing_verdict_for_stats(min_total: m, s: s) + Absent => UnknownRefused + } + } +} + +data host_swap_cap_qualification_note: String = "THE load-bearing conjunct of this module, and the reason it is not a free-floating swap model: it changes what an EXISTING converged knob is allowed to claim. gunbc.runner_unit_live_read already produces a verdict for the per-slot MemorySwapMax cap. That verdict is a fact about the cgroup property and is imported here unchanged; what this fold adds is the qualification that a cap verdict carries information only when its backing is observed Converged. Every other backing state DOMINATES the cap: unobserved backing yields UnknownRefused however green the property read was, absent backing yields Absent, undersized backing yields Drifted. This is not a min() over some verdict lattice and must not become one — it is a presupposition check, and the asymmetry is the point. A green cap over unknown backing is precisely the failure mode #7213 found in another dress: sccache --show-stats reported a healthy server because the probe auto-started the very thing it was measuring, and a MemorySwapMax read reports a healthy ceiling because systemd will happily store a ceiling for a resource the host does not have. Both manufacture their own evidence, and both must refuse instead." + +fn swap_cap_verdict_qualified_by_backing( + cap: ObservationVerdict, + backing: ObservationVerdict, +) -> ObservationVerdict { + cap +} + +data host_swap_cap_widen_red_control_note: String = "The forbidden arm, modeled as its own declaration so it can be executed against the gate rather than described in prose. Backing-blind qualification is what the corpus does TODAY — the cap verdict is reported as-is, with no backing term anywhere in the fold — so this sketch is not a hypothetical: it is the current behaviour written down and made falsifiable. The gate rejects it and accepts the authority on the same inputs, and the perturbation is independent of the property checked, so the pair cannot pass tautologically." + +fn swap_cap_verdict_backing_blind_widen_sketch( + cap: ObservationVerdict, + backing: ObservationVerdict, +) -> ObservationVerdict { + cap +} + +fn observation_verdict_is_converged(v: ObservationVerdict) -> Bool { + match v { + Converged => true + std.upsert_decision.Absent => false + Drifted => false + Conflict => false + Inaccessible => false + UnknownRefused => false + } +} + +fn swap_cap_verdict_gate_accepts( + verdict: ObservationVerdict, + backing: ObservationVerdict, +) -> Bool { + if observation_verdict_is_converged(v: backing) { + true + } else { + !observation_verdict_is_converged(v: verdict) + } +} + +data host_swap_backing_observation_frontier_note: String = "The live producer, and it returns none for every host on purpose. There is no /proc/swaps reader and no free(1) transport in the tree — extdeps.os.free carries the cited SHAPE and has zero live producers today — so the honest observation for all four hosts is absence, and the derived verdict for all four is UnknownRefused. Writing a fixture here and reading it back would be the specification-without-execution trap in its purest form (DESIGN §5): the matrix would go green against numbers this module itself authored. The count of unobserved hosts is exported instead, so the deficit is a NUMBER that must change when a producer lands, never a silence. Realization is blocked on one named thing and it is not swap-specific: the argv materializer binds a hardcoded five-parameter vocabulary (path, service, operation, package, bin, args, unit), so fallocate/mkswap/swapon/fstab and a /proc/swaps read cannot be expressed as typed host effects until that binding is generic. That materializer has no .dag declaration to bind a scaffold to — it is a v1 seed builtin, which is part of why it is the blocker — so the scaffold binds the transport type it materializes into. Declaring those operations before then would add rows to the shell-to-dag census that no consumer can reach, which is the parallel-representation debt the census exists to prevent." + +data host_swap_backing_realization_scaffold: Disposition = Scaffold { + dissolves_to: SingleAuthority, + bind: DeclarationRef { + module_path: "gunbc.host_effect", + decl_name: "HostEffectTransport", + field: WholeDeclaration, + } +} + +fn host_swap_backing_observation(host: HostIdentity) -> SwapStats? { + none +} + +data host_swap_backing_probe_independence_note: String = "The host verdict is routed through the read-back independence criterion rather than trusting the observation directly, and it is worth being precise about why, because /proc/swaps IS inert and the routing is therefore a no-op TODAY. The routing is what makes the classification load-bearing instead of decorative: the probe row travels with the verdict, so a future producer that swapped the transport for an ensure-shaped one — `swapon --show` after an activation attempt, an agent that mounts what it fails to find — would have to change proc_swaps_read_probe's classification to keep the same green, and changing it is a visible edit to a cited row rather than a silent change of meaning inside a transport. This is the same reason the swap CAP is qualified by its backing: a value is evidence only together with the conditions under which it was obtained." + +fn host_swap_backing_host_verdict(host: HostIdentity) -> ObservationVerdict { + readback_evidence_verdict( + p: proc_swaps_read_probe, + observed: host_swap_backing_verdict( + req: host_swap_backing_requirement(), + observed: host_swap_backing_observation(host: host), + ), + ) +} + +fn host_swap_backing_unobserved_count(hosts: List) -> Int { + filter( + hosts, + h => observation_verdict_eq(a: host_swap_backing_host_verdict(host: h), b: UnknownRefused), + ).length() +} + +fn host_swap_backing_fleet_unobserved_count() -> Int { + host_swap_backing_unobserved_count(hosts: fleet_subsumption_hosts) +} diff --git a/dag/gunbc/readback_independence.dag b/dag/gunbc/readback_independence.dag new file mode 100644 index 00000000000..a4e2d048dd1 --- /dev/null +++ b/dag/gunbc/readback_independence.dag @@ -0,0 +1,101 @@ +module gunbc.readback_independence + +import std.types { String, NonEmptyStr, Bool, Int, List } +import std.upsert_decision { ObservationVerdict, Converged, Drifted, Conflict, Inaccessible, UnknownRefused } +import std.decl_ref { DeclarationRef, WholeDeclaration } + +data readback_independence_authority_note: String = "THE standing criterion generalized out of #7213 Finding 2, which was found once, by hand, on one host: `sccache --show-stats` printed a healthy stats table over srv3 while the modeled unit had been inactive (dead) for six hours and no sccache process existed before the probe ran — because ANY sccache invocation auto-starts a server. The read did not observe the state, it CREATED it. That was written down as a note beside one verdict fold, which leaves the criterion as prose the next probe author has to happen to read. The criterion itself is general and has nothing to do with sccache: a read-back is evidence about a subject only if performing the read could not have established the subject. A probe that can establish what it reports is not measuring, it is asserting — the fabricated plausible output of DESIGN §5, arriving as a genuinely-executed command with genuinely-correct output. The class is not exotic and it is not rare. It is every probe whose transport shares a mechanism with the thing provisioned: a client that auto-starts its daemon, a mount check that triggers an automount, a token read that refreshes the token, a health endpoint that lazily initializes on first request, an ensure-shaped operation used as a query. The tell is always the same and it is a question about the TRANSPORT rather than the value: could running this have made the answer true?" + +data readback_independence_asymmetry_note: String = "The correction is deliberately ASYMMETRIC, and getting that right is what keeps the criterion from being a blunt instrument that discards good evidence. A self-establishing probe's NEGATIVE results stay trustworthy: if `--show-stats` had failed outright, that failure is real — the probe was willing and able to bring the subject into existence and still could not report it. Only the positive is poisoned, because that is the one outcome the probe's own side effect can manufacture. So the fold rewrites Converged and passes every other verdict through unchanged, and it rewrites Converged to UnknownRefused specifically — not to Absent, which would assert the subject is missing, and not to Conflict, which would assert two sources disagree. The honest statement is that this probe cannot answer this question, and UnknownRefused is exactly that statement. It is also the arm that keeps the deficit COUNTABLE: an UnknownRefused cell ranks for a producer to be built, while a silently-downgraded or silently-accepted one ranks for nothing." + +type ProbeEffectOnSubject + = ProbeInert + | ProbeMayEstablish { mechanism: NonEmptyStr } + | ProbeEffectUnknown { reason: NonEmptyStr } + +type ReadBackProbe { + label: NonEmptyStr + subject: NonEmptyStr + effect_on_subject: ProbeEffectOnSubject +} + +fn readback_probe_is_independent(p: ReadBackProbe) -> Bool { + match p.effect_on_subject { + ProbeInert => true + ProbeMayEstablish { mechanism: _ } => false + ProbeEffectUnknown { reason: _ } => false + } +} + +data readback_unknown_effect_is_not_inert_note: String = "An UNCLASSIFIED probe is treated exactly as a self-establishing one, and this is the fail-closed hinge. The tempting default is the other way — nobody has shown this probe has a side effect, so assume it does not — and that default is the absorbing fallback with the burden of proof reversed: it converts every un-audited transport into evidence, and the population of un-audited transports is the whole tree. Independence is a property that must be ESTABLISHED for a specific transport, so ProbeEffectUnknown carries a reason and yields the same correction as ProbeMayEstablish. The two stay distinct arms anyway, because their remedies differ: ProbeMayEstablish is a probe to REPLACE, ProbeEffectUnknown is a transport to AUDIT." + +fn readback_evidence_verdict(p: ReadBackProbe, observed: ObservationVerdict) -> ObservationVerdict { + observed +} + +data readback_trusting_widen_red_control_note: String = "The forbidden arm as an executable declaration: trust the probe's own answer whatever the transport can do to the subject. It is the corpus's behaviour everywhere the criterion has not yet been applied, so the sketch is a description of today rather than a hypothetical, and the gate rejects it on exactly the inputs #7213 hit live." + +fn readback_evidence_trusting_widen_sketch( + p: ReadBackProbe, + observed: ObservationVerdict, +) -> ObservationVerdict { + observed +} + +fn readback_verdict_is_converged(v: ObservationVerdict) -> Bool { + match v { + Converged => true + std.upsert_decision.Absent => false + Drifted => false + Conflict => false + Inaccessible => false + UnknownRefused => false + } +} + +fn readback_evidence_gate_accepts(p: ReadBackProbe, verdict: ObservationVerdict) -> Bool { + if readback_probe_is_independent(p: p) { + true + } else { + !readback_verdict_is_converged(v: verdict) + } +} + +data readback_probe_roster_note: String = "The lane's real probes, classified. This roster is a small honest inventory and not a claim of completeness — it covers the transports this lane has actually reasoned about, and a probe absent from it is unclassified, which the criterion already treats as non-independent. sccache_show_stats is the cited instance and the reason the module exists. systemd_show_property and systemd_is_active are the ones that make the criterion non-vacuous in the other direction: `systemctl show` and `systemctl is-active` read the manager's recorded state and start nothing, so they are genuinely inert and their Converged results survive — a criterion that refused every probe would be the absorbing fallback wearing a safety badge. proc_swaps_read is classified inert on the same reasoning: reading /proc/swaps enumerates active swap areas and cannot activate one, unlike `swapon` whose ensure shape would establish the very backing a query is supposed to find." + +data sccache_show_stats_probe: ReadBackProbe = ReadBackProbe { + label: "sccache --show-stats", + subject: "sccache daemon is running under the modeled unit", + effect_on_subject: ProbeMayEstablish { + mechanism: "any sccache client invocation auto-starts a server when none is listening, so the probe can create the daemon it reports on (#7213 Finding 2, observed live on srv3 2026-07-25)", + }, +} + +data systemd_show_property_probe: ReadBackProbe = ReadBackProbe { + label: "systemctl show -p ", + subject: "cgroup property value on a unit", + effect_on_subject: ProbeInert, +} + +data systemd_is_active_probe: ReadBackProbe = ReadBackProbe { + label: "systemctl --user is-active ", + subject: "unit is running under its supervisor", + effect_on_subject: ProbeInert, +} + +data proc_swaps_read_probe: ReadBackProbe = ReadBackProbe { + label: "read /proc/swaps", + subject: "host has swap backing active", + effect_on_subject: ProbeInert, +} + +data readback_probe_roster: List = [ + sccache_show_stats_probe, + systemd_show_property_probe, + systemd_is_active_probe, + proc_swaps_read_probe, +] + +fn readback_non_independent_probe_count() -> Int { + filter(readback_probe_roster, p => !readback_probe_is_independent(p: p)).length() +} diff --git a/dag/test/claim/host_swap_backing_witness_test.dag b/dag/test/claim/host_swap_backing_witness_test.dag new file mode 100644 index 00000000000..51d0a47c554 --- /dev/null +++ b/dag/test/claim/host_swap_backing_witness_test.dag @@ -0,0 +1,114 @@ +module test.claim.host_swap_backing + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn stats_fixture(total_bytes: Int) -> SwapStats { + SwapStats { + total: byte_size(total_bytes), + used: byte_size(0), + free: byte_size(total_bytes), + } +} + +data witness_requirement_derivation_note: String = "The requirement must come from the DECLARED cap, not from a number typed into this witness, or the module is asserting its own invention. So the assertion is a relationship: the derived min_total equals gunbc_runner_slot_desired().memory_swap_max exactly, which means editing that one declaration moves the requirement and this witness together, and a hand-written swap size anywhere would break it." + +fn witness_requirement_is_derived_from_the_declared_cap() -> Bool { + match host_swap_backing_requirement() { + SwapBackingRequired { min_total: m, requiring_declaration: d } => + byte_size_count(b: m) == byte_size_count(b: gunbc_runner_slot_desired().memory_swap_max) + && byte_size_count(b: m) > 0 + SwapBackingNotRequired => false + } +} + +data witness_verdict_arms_note: String = "The four backing states must stay distinct, because each names a different piece of work: no producer (build one), zero total (provision backing), undersized total (resize), sufficient total (done). A fold that collapsed any pair would make one of those disappear from every count derived from it. Absent is asserted specifically against zero rather than against small, because zero is the state the whole module exists for — a cap over nothing." + +fn witness_backing_verdict_separates_unknown_absent_drifted_converged() -> Bool { + let req = host_swap_backing_requirement() + let cap_bytes = byte_size_count(b: gunbc_runner_slot_desired().memory_swap_max) + let no_producer = host_swap_backing_verdict(req: req, observed: none) + let zero_backing = host_swap_backing_verdict( + req: req, + observed: Present { value: stats_fixture(total_bytes: 0) }, + ) + let undersized = host_swap_backing_verdict( + req: req, + observed: Present { value: stats_fixture(total_bytes: 1073741824) }, + ) + let sufficient = host_swap_backing_verdict( + req: req, + observed: Present { value: stats_fixture(total_bytes: cap_bytes) }, + ) + observation_verdict_eq(a: no_producer, b: std.upsert_decision.UnknownRefused) + && observation_verdict_eq(a: zero_backing, b: std.upsert_decision.Absent) + && observation_verdict_eq(a: undersized, b: std.upsert_decision.Drifted) + && observation_verdict_eq(a: sufficient, b: std.upsert_decision.Converged) +} + +data witness_cap_qualification_note: String = "THE conjunct the module exists for. A per-slot MemorySwapMax read that says Converged is the input on every line here; only the backing term varies. With backing observed Converged the cap verdict passes through unchanged — the non-vacuity control, without which a qualifier that refused everything would look correct. With backing zero, unobserved, or unreachable, the same green cap must NOT survive as Converged, and each case must keep its own arm rather than rounding to a single 'not converged': absent backing is provisioning work, unobserved backing is producer work, unreachable backing is the A1 reach lane." + +fn witness_green_cap_does_not_survive_missing_backing() -> Bool { + let green_cap = std.upsert_decision.Converged + let with_backing = swap_cap_verdict_qualified_by_backing(cap: green_cap, backing: std.upsert_decision.Converged) + let no_backing = swap_cap_verdict_qualified_by_backing( + cap: green_cap, + backing: std.upsert_decision.Absent, + ) + let unobserved = swap_cap_verdict_qualified_by_backing(cap: green_cap, backing: std.upsert_decision.UnknownRefused) + let unreachable = swap_cap_verdict_qualified_by_backing(cap: green_cap, backing: std.upsert_decision.Inaccessible) + observation_verdict_eq(a: with_backing, b: std.upsert_decision.Converged) + && observation_verdict_eq(a: no_backing, b: std.upsert_decision.Absent) + && observation_verdict_eq(a: unobserved, b: std.upsert_decision.UnknownRefused) + && observation_verdict_eq(a: unreachable, b: std.upsert_decision.Inaccessible) +} + +data witness_qualification_is_not_a_lattice_meet_note: String = "The qualification is a presupposition check and not a meet over some verdict ordering, and this conjunct pins the asymmetry so a later refactor cannot quietly turn it into one. A DRIFTED cap under CONVERGED backing stays Drifted — the backing does not repair the cap — while a CONVERGED cap under DRIFTED backing becomes Drifted. Under a symmetric meet those two would be the same value by construction and the direction of the check would be lost." + +fn witness_qualification_direction_is_asymmetric() -> Bool { + let drifted_cap_good_backing = swap_cap_verdict_qualified_by_backing( + cap: std.upsert_decision.Drifted, + backing: std.upsert_decision.Converged, + ) + let good_cap_drifted_backing = swap_cap_verdict_qualified_by_backing( + cap: std.upsert_decision.Converged, + backing: std.upsert_decision.Drifted, + ) + observation_verdict_eq(a: drifted_cap_good_backing, b: std.upsert_decision.Drifted) + && observation_verdict_eq(a: good_cap_drifted_backing, b: std.upsert_decision.Drifted) + && !observation_verdict_eq( + a: swap_cap_verdict_qualified_by_backing(cap: std.upsert_decision.Inaccessible, backing: std.upsert_decision.Converged), + b: std.upsert_decision.Converged, + ) +} + +data witness_red_control_note: String = "The discriminating RED control, and its perturbation is the corpus's CURRENT behaviour rather than an invented one: reporting the cap verdict with no backing term at all. The gate rejects the sketch and accepts the authority on identical inputs. Both halves are required — rejection alone would pass for a gate that rejects everything, acceptance alone for a gate that accepts everything — and the gate's own decision is computed from the backing argument, not from which function produced the verdict, so it cannot be satisfied by relabelling." + +fn witness_red_control_backing_blind_rejected_by_gate() -> Bool { + let backing = std.upsert_decision.UnknownRefused + let widened = swap_cap_verdict_backing_blind_widen_sketch(cap: std.upsert_decision.Converged, backing: backing) + let authority = swap_cap_verdict_qualified_by_backing(cap: std.upsert_decision.Converged, backing: backing) + observation_verdict_eq(a: widened, b: std.upsert_decision.Converged) + && !swap_cap_verdict_gate_accepts(verdict: widened, backing: backing) + && swap_cap_verdict_gate_accepts(verdict: authority, backing: backing) +} + +fn witness_gate_admits_a_green_cap_when_backing_is_present() -> Bool { + swap_cap_verdict_gate_accepts(verdict: std.upsert_decision.Converged, backing: std.upsert_decision.Converged) +} + +data witness_frontier_count_note: String = "The observation frontier is a counted number, not a silence. All four enrolled hosts derive UnknownRefused today because no /proc/swaps or free(1) producer exists in the tree, and pinning the count to the full fleet size means landing a producer is a VISIBLE event that must update this witness. It also fails in the right direction: if someone were to add a fabricated per-host fixture to make the matrix look greener, this count would drop and the witness would red." + +fn witness_every_enrolled_host_is_unobserved_today() -> Bool { + host_swap_backing_fleet_unobserved_count() == fleet_subsumption_hosts.length() + && fleet_subsumption_hosts.length() > 0 +} + +test fn host_swap_backing_witnesses() -> Bool { + witness_requirement_is_derived_from_the_declared_cap() + && witness_backing_verdict_separates_unknown_absent_drifted_converged() + && witness_green_cap_does_not_survive_missing_backing() + && witness_qualification_direction_is_asymmetric() + && witness_red_control_backing_blind_rejected_by_gate() + && witness_gate_admits_a_green_cap_when_backing_is_present() + && witness_every_enrolled_host_is_unobserved_today() +} diff --git a/dag/test/claim/readback_independence_witness_test.dag b/dag/test/claim/readback_independence_witness_test.dag new file mode 100644 index 00000000000..464877bdfa2 --- /dev/null +++ b/dag/test/claim/readback_independence_witness_test.dag @@ -0,0 +1,122 @@ +module test.claim.readback_independence + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data witness_cited_incident_note: String = "The conjunct is the incident itself, replayed through the criterion. On srv3 2026-07-25 `sccache --show-stats` returned a full stats table — a Converged read — over a host whose modeled unit had been dead for six hours. The criterion must turn that exact input into UnknownRefused, and it must do so because of what the PROBE can do, not because of anything about the value it returned." + +fn witness_self_establishing_probe_cannot_report_converged() -> Bool { + observation_verdict_eq( + a: readback_evidence_verdict( + p: sccache_show_stats_probe, + observed: std.upsert_decision.Converged, + ), + b: std.upsert_decision.UnknownRefused, + ) +} + +data witness_negatives_survive_note: String = "The asymmetry, and it is the conjunct that stops the criterion from being a blunt discard. A self-establishing probe that reports a NEGATIVE is still telling the truth: it had every opportunity to bring the subject into existence and still could not report it, so Absent stays Absent, Drifted stays Drifted, Inaccessible stays Inaccessible. Only the positive is rewritten. A fold that returned UnknownRefused for every verdict from a non-independent probe would pass the conjunct above and destroy real evidence here." + +fn witness_negative_results_from_a_tainted_probe_survive() -> Bool { + observation_verdict_eq( + a: readback_evidence_verdict(p: sccache_show_stats_probe, observed: std.upsert_decision.Absent), + b: std.upsert_decision.Absent, + ) + && observation_verdict_eq( + a: readback_evidence_verdict( + p: sccache_show_stats_probe, + observed: std.upsert_decision.Drifted, + ), + b: std.upsert_decision.Drifted, + ) + && observation_verdict_eq( + a: readback_evidence_verdict( + p: sccache_show_stats_probe, + observed: std.upsert_decision.Inaccessible, + ), + b: std.upsert_decision.Inaccessible, + ) +} + +data witness_inert_probe_note: String = "The non-vacuity control in the other direction. `systemctl show` and `systemctl --user is-active` read the manager's recorded state and start nothing, so their Converged results must survive untouched. Without this, a criterion that refused every probe would satisfy every other conjunct in this file while making read-back worthless — the absorbing fallback wearing a safety badge, which is precisely the failure this lane keeps catching." + +fn witness_inert_probes_keep_their_evidence() -> Bool { + observation_verdict_eq( + a: readback_evidence_verdict( + p: systemd_is_active_probe, + observed: std.upsert_decision.Converged, + ), + b: std.upsert_decision.Converged, + ) + && observation_verdict_eq( + a: readback_evidence_verdict( + p: systemd_show_property_probe, + observed: std.upsert_decision.Converged, + ), + b: std.upsert_decision.Converged, + ) + && readback_probe_is_independent(p: proc_swaps_read_probe) +} + +data witness_unknown_effect_note: String = "An unaudited transport must be treated as tainted, not as clean. This is the fail-closed default and it is where the criterion earns most of its value, because the classified probes are a handful and the unclassified ones are everything else." + +fn witness_unclassified_probe_is_treated_as_tainted() -> Bool { + let unaudited = ReadBackProbe { + label: "hypothetical unaudited transport", + subject: "some subject", + effect_on_subject: ProbeEffectUnknown { reason: "nobody has audited this transport yet" }, + } + !readback_probe_is_independent(p: unaudited) + && observation_verdict_eq( + a: readback_evidence_verdict(p: unaudited, observed: std.upsert_decision.Converged), + b: std.upsert_decision.UnknownRefused, + ) +} + +data witness_red_control_note: String = "The discriminating RED control. The perturbation is trusting the probe's own answer regardless of transport — the corpus's behaviour everywhere the criterion has not been applied — and the gate rejects it on the srv3 inputs while accepting the authority on the same inputs. Both directions are asserted so neither an always-reject nor an always-accept gate could pass." + +fn witness_red_control_trusting_probe_rejected_by_gate() -> Bool { + let p = sccache_show_stats_probe + let widened = readback_evidence_trusting_widen_sketch( + p: p, + observed: std.upsert_decision.Converged, + ) + let authority = readback_evidence_verdict(p: p, observed: std.upsert_decision.Converged) + observation_verdict_eq(a: widened, b: std.upsert_decision.Converged) + && !readback_evidence_gate_accepts(p: p, verdict: widened) + && readback_evidence_gate_accepts(p: p, verdict: authority) + && readback_evidence_gate_accepts(p: systemd_is_active_probe, verdict: std.upsert_decision.Converged) +} + +data witness_live_consumer_note: String = "The criterion has a live consumer, or it is an inert lens — a thing DESIGN §6 calls a lie in its own right. gunbc.host_swap_backing routes every host verdict through it. The routing is a no-op today because /proc/swaps is inert, so the conjunct proves it by SUBSTITUTION: the same swap verdict carried by the sccache probe instead would be refused. That is what makes the classification load-bearing rather than decorative — swapping the transport for an ensure-shaped one changes the answer." + +fn witness_swap_axis_consumes_the_criterion() -> Bool { + let inert_route = readback_evidence_verdict( + p: proc_swaps_read_probe, + observed: std.upsert_decision.Converged, + ) + let tainted_route = readback_evidence_verdict( + p: sccache_show_stats_probe, + observed: std.upsert_decision.Converged, + ) + observation_verdict_eq(a: inert_route, b: std.upsert_decision.Converged) + && observation_verdict_eq(a: tainted_route, b: std.upsert_decision.UnknownRefused) + && observation_verdict_eq( + a: host_swap_backing_host_verdict(host: operator_host_srv3), + b: std.upsert_decision.UnknownRefused, + ) +} + +fn witness_roster_names_the_cited_incident() -> Bool { + readback_non_independent_probe_count() == 1 + && readback_probe_roster.length() == 4 +} + +test fn readback_independence_witnesses() -> Bool { + witness_self_establishing_probe_cannot_report_converged() + && witness_negative_results_from_a_tainted_probe_survive() + && witness_inert_probes_keep_their_evidence() + && witness_unclassified_probe_is_treated_as_tainted() + && witness_red_control_trusting_probe_rejected_by_gate() + && witness_swap_axis_consumes_the_criterion() + && witness_roster_names_the_cited_incident() +} From 80ee799ef3fb9e64cb9293e6ce8b0a7776e8ad41 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 19:27:36 +0000 Subject: [PATCH 16/17] srvN quality sweep: enrollment wall, swap-backing axis, read-back independence criterion MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three quality items over the "modeled" middle of the host-standup spine, each landing with a discriminating RED control run by execution. 1. Enrollment construction wall (runner_host_deploy). No function takes a bare RunnerHostDeploy and yields an ArgvCommand any more: both command builders consume a RunnerHostAdmission and return RunnerCommandOrRefusal whose refusal arm carries no command, so a host absent from fleet_intent cannot produce installer or enable argv at all. Honest residual named in-code: .dag has no visibility modifiers, so RunnerHostEnrolled can be hand-forged — an explicit lie rather than an accident; closes when node/subtree visibility grants land. 2. Swap backing as a modeled axis (host_swap_backing). The corpus already converges MemorySwapMax = 32 GiB per slot over a resource whose existence nothing models — systemd stores and reports a ceiling byte-for-byte on a host with zero swap devices, so the knob greens over nothing. The requirement is DERIVED from the declared cap rather than authored per host (no fleet reach from a session container, so a per-host swap table would be invention); backing states stay separable (no producer / zero / undersized / sufficient, four different pieces of work); and a cap verdict is qualified by its backing, asymmetrically — a presupposition check, pinned by witness against becoming a lattice meet. The observation frontier is a counted number (4 of 4 hosts UnknownRefused today), so a fabricated fixture reds the witness instead of greening the matrix. Effect realization is blocked on the argv materializer's hardcoded five-parameter vocabulary and is declared, not stubbed. 3. Read-back independence as a standing criterion (readback_independence). #7213 Finding 2 generalized off one host: a read-back is evidence only if performing the read could not have established the subject. Asymmetric correction (tainted negatives survive; only Converged is rewritten, to UnknownRefused so the deficit stays countable), unclassified probes treated as tainted, and inert probes keep their evidence so the criterion is non-vacuous in both directions. Live consumer: host_swap_backing routes every host verdict through it; the witness proves the routing is load-bearing by substitution, since /proc/swaps is inert today. Witnesses: 7 swap conjuncts, 7 read-back conjuncts, 4 wall conjuncts — all PASS. RED controls: perturbing swap_cap_verdict_qualified_by_backing to be backing-blind and readback_evidence_verdict to trust the probe FAILs both witnesses; perturbing admit_runner_host to admit everything reds 3 of 4 wall conjuncts with enrolled_host_still_admits correctly staying green. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/host_swap_backing.dag | 9 ++++++- dag/gunbc/readback_independence.dag | 13 ++++++++- .../srvn-buildcache-provisioning-design.md | 27 +++++++++++++++++++ 3 files changed, 47 insertions(+), 2 deletions(-) diff --git a/dag/gunbc/host_swap_backing.dag b/dag/gunbc/host_swap_backing.dag index 8fcd055e902..69df1ecfea9 100644 --- a/dag/gunbc/host_swap_backing.dag +++ b/dag/gunbc/host_swap_backing.dag @@ -70,7 +70,14 @@ fn swap_cap_verdict_qualified_by_backing( cap: ObservationVerdict, backing: ObservationVerdict, ) -> ObservationVerdict { - cap + match backing { + Converged => cap + std.upsert_decision.Absent => std.upsert_decision.Absent + Drifted => Drifted + Conflict => Conflict + Inaccessible => Inaccessible + UnknownRefused => UnknownRefused + } } data host_swap_cap_widen_red_control_note: String = "The forbidden arm, modeled as its own declaration so it can be executed against the gate rather than described in prose. Backing-blind qualification is what the corpus does TODAY — the cap verdict is reported as-is, with no backing term anywhere in the fold — so this sketch is not a hypothetical: it is the current behaviour written down and made falsifiable. The gate rejects it and accepts the authority on the same inputs, and the perturbation is independent of the property checked, so the pair cannot pass tautologically." diff --git a/dag/gunbc/readback_independence.dag b/dag/gunbc/readback_independence.dag index a4e2d048dd1..dd2d10e4b6a 100644 --- a/dag/gunbc/readback_independence.dag +++ b/dag/gunbc/readback_independence.dag @@ -30,7 +30,18 @@ fn readback_probe_is_independent(p: ReadBackProbe) -> Bool { data readback_unknown_effect_is_not_inert_note: String = "An UNCLASSIFIED probe is treated exactly as a self-establishing one, and this is the fail-closed hinge. The tempting default is the other way — nobody has shown this probe has a side effect, so assume it does not — and that default is the absorbing fallback with the burden of proof reversed: it converts every un-audited transport into evidence, and the population of un-audited transports is the whole tree. Independence is a property that must be ESTABLISHED for a specific transport, so ProbeEffectUnknown carries a reason and yields the same correction as ProbeMayEstablish. The two stay distinct arms anyway, because their remedies differ: ProbeMayEstablish is a probe to REPLACE, ProbeEffectUnknown is a transport to AUDIT." fn readback_evidence_verdict(p: ReadBackProbe, observed: ObservationVerdict) -> ObservationVerdict { - observed + if readback_probe_is_independent(p: p) { + observed + } else { + match observed { + Converged => UnknownRefused + std.upsert_decision.Absent => std.upsert_decision.Absent + Drifted => Drifted + Conflict => Conflict + Inaccessible => Inaccessible + UnknownRefused => UnknownRefused + } + } } data readback_trusting_widen_red_control_note: String = "The forbidden arm as an executable declaration: trust the probe's own answer whatever the transport can do to the subject. It is the corpus's behaviour everywhere the criterion has not yet been applied, so the sketch is a description of today rather than a hypothetical, and the gate rejects it on exactly the inputs #7213 hit live." diff --git a/docs/plans/srvn-buildcache-provisioning-design.md b/docs/plans/srvn-buildcache-provisioning-design.md index 00ecfd64839..cefa0238d90 100644 --- a/docs/plans/srvn-buildcache-provisioning-design.md +++ b/docs/plans/srvn-buildcache-provisioning-design.md @@ -234,6 +234,33 @@ T4 was written as "post-apply `sccache --show-stats`, independent of our write." **T4 status:** srv3 **green** at the restated bar (13-minute delayed read, modeled unit, PID stable). srv1 and srv2 remain **open** — not for a modeling reason: neither host is reachable from a session container with the fleet key today (`Permission denied (publickey)` for `ubuntu`/`briansrls`/`node-orch`), which is the A1/A2/B2 reach-and-identity gap already typed in `gunbc.plans.fleet_subsumption_manual_gaps`. The downstream triggers (`ctrl_sccache_service_retired`, and the `ci_sccache_opportunistic_detect` cutover) stay blocked on those two hosts, and the srv1/srv2 units should be expected to carry the same latent defect until re-provisioned from the model. +### 5.5 Finding 2 generalized — read-back independence is a standing criterion (2026-07-25) + +Finding 2 was recorded as a note beside one verdict fold, which leaves it as prose the next probe author has to happen to read. The criterion is general and has nothing to do with sccache: **a read-back is evidence about a subject only if performing the read could not have established the subject.** A probe that can establish what it reports is not measuring, it is asserting — §5's fabricated plausible output arriving as a genuinely-executed command with genuinely-correct output. + +The class is not rare. It is every probe whose transport shares a mechanism with the thing provisioned: a client that auto-starts its daemon, a mount check that triggers an automount, a token read that refreshes the token, a health endpoint that lazily initializes on first request, an ensure-shaped operation used as a query. The tell is a question about the **transport**, never about the value: *could running this have made the answer true?* + +Landed as `gunbc.readback_independence` (`ProbeEffectOnSubject = ProbeInert | ProbeMayEstablish{mechanism} | ProbeEffectUnknown{reason}`), with three properties worth naming: + +- **Asymmetric correction.** A tainted probe's *negative* results survive — it had every opportunity to bring the subject into existence and still could not report it. Only `Converged` is rewritten, and to `UnknownRefused` (this probe cannot answer), never `Absent` (asserting the subject is missing) or `Conflict` (asserting two sources disagree). The `UnknownRefused` arm is what keeps the deficit countable. +- **Unclassified ⇒ tainted.** `ProbeEffectUnknown` gets the same correction as `ProbeMayEstablish`. The opposite default converts every un-audited transport into evidence, and the population of un-audited transports is the whole tree. The two arms stay distinct because the remedies differ: replace the probe vs audit the transport. +- **Non-vacuous in both directions.** `systemctl show` / `is-active` / a `/proc/swaps` read are classified `ProbeInert` and keep their `Converged` — a criterion that refused every probe would be the absorbing fallback wearing a safety badge. + +Live consumer: `gunbc.host_swap_backing` routes every host verdict through it. The routing is a no-op today (`/proc/swaps` is inert), so the witness proves it by **substitution** — the same verdict carried by the sccache probe is refused. That is what makes the classification load-bearing rather than decorative: swapping the transport for an ensure-shaped one changes the answer, and it does so by editing a cited row rather than silently inside a transport. + +### 5.6 The swap-cap presupposition — a converged knob over a resource nothing models (2026-07-25) + +Found while modeling swap as an axis, and it is the same shape as Finding 2 in different dress. `gunbc.runner_slot_allocation` declares `memory_swap_max = 34359738368` (32 GiB) per runner slot; `gunbc.host_converge` drives it onto every host as `MemorySwapMax` via the per-slot drop-in; `gunbc.runner_unit_live_read` reads it back and reports `Converged` when the property matches. Every step is correct in isolation and the composition still proves nothing, because `MemorySwapMax` is a **ceiling**: systemd accepts it, reports it, and matches it byte-for-byte on a host with zero swap devices. The knob converges green over a resource that may not exist — and nothing anywhere in the tree models whether it does (zero `mkswap`/`swapon`/`fallocate`/`/proc/swaps` occurrences; swap appears only as prose in `fleet_acceptance_criteria` and as the floor-timeout mechanism in `ci_budget_tree`). + +`gunbc.host_swap_backing` makes the presupposition representable: + +- **Requirement derived, never authored.** No one in this session can read `/proc/swaps` on srv1..srv4 (the A1 reach gap), so a per-host swap table here would be invention. Declaring a nonzero `MemorySwapMax` *is* declaring that backing must exist, so the requirement falls out of `gunbc_runner_slot_desired().memory_swap_max` and moves when it moves. **Declared limit:** `min_total` is the per-slot cap, not slots × cap — whether five concurrent slots can each reach their ceiling is an aggregate question nobody has measured, and multiplying would assert a worst case as fact. +- **Four separable states**, because each names different work: no producer → `UnknownRefused` (build one); zero total → `Absent` (provision backing); undersized → `Drifted` (resize); sufficient → `Converged`. There is deliberately **no** "assume the distro default gave us swap" arm — srv1..srv4 were installed across at least two paths, so its error rate would be unmeasurable by construction. +- **Cap qualified by backing.** A `MemorySwapMax` verdict carries information only when backing is observed `Converged`; every other backing state dominates. This is a presupposition check and explicitly *not* a lattice meet — a witness pins the asymmetry so a refactor cannot quietly symmetrize it. +- **Observation frontier counted, not silent.** All four enrolled hosts derive `UnknownRefused` today; the count is exported and pinned by witness, so landing a producer is a visible event and a fabricated fixture would *red* the witness rather than green the matrix. + +**Realization is blocked, and on nothing swap-specific:** the argv materializer binds a hardcoded five-parameter vocabulary (`path`, `service`, `operation`, `package`, `bin`, `args`, `unit`), so `fallocate`/`mkswap`/`swapon`/fstab and a `/proc/swaps` read cannot be expressed as typed host effects. Declaring them before that binding is generic would add census rows no consumer can reach — the parallel-representation debt the census exists to prevent. Scaffold binds `gunbc.host_effect.HostEffectTransport`; the materializer itself has no `.dag` declaration to bind to, which is part of why it is the blocker. + ## 6. Dissolution triggers (every scaffold names its exit) | Scaffold | Dissolves to | Trigger | From 736bc9e184ef77ca6afbd2793266d43218513eb9 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 19:54:43 +0000 Subject: [PATCH 17/17] WIP: srvN subsumption --- dag/gunbc/host_swap_backing.dag | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/host_swap_backing.dag b/dag/gunbc/host_swap_backing.dag index 69df1ecfea9..3dffd257cab 100644 --- a/dag/gunbc/host_swap_backing.dag +++ b/dag/gunbc/host_swap_backing.dag @@ -5,13 +5,13 @@ import std.measure { ByteSize, byte_size, byte_size_count } import std.upsert_decision { ObservationVerdict, Converged, Drifted, Conflict, Inaccessible, UnknownRefused } import std.disposition { Disposition, Scaffold, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } -import extdeps.os.free { SwapStats } +import extdeps.tools.free { SwapStats } import gunbc.runner_slot_allocation { gunbc_runner_slot_desired } import gunbc.host_phase_status { observation_verdict_eq, fleet_subsumption_hosts } import gunbc.readback_independence { readback_evidence_verdict, proc_swaps_read_probe } import product.placement_supply { HostIdentity } -data host_swap_backing_authority_note: String = "THE host swap-BACKING axis, and it exists because the corpus already converges a swap CAP over a resource whose existence nothing models. gunbc.runner_slot_allocation declares memory_swap_max = 34359738368 (32 GiB) per runner slot; gunbc.host_converge drives it onto every host as MemorySwapMax through the per-slot drop-in at gunbc_runner_per_slot_swap_dropin_path, and gunbc.runner_unit_live_read reads it back and reports Converged when the cgroup property matches. Every one of those steps is correct in isolation and the composition still proves nothing, because MemorySwapMax is a CEILING: systemd accepts it, reports it, and matches it byte-for-byte on a host with zero swap devices. The knob converges green over a resource that does not exist. That is the presupposition failure this module makes representable — a cap is evidence about a resource only once the resource is observed present — and it is the shape DESIGN §5 calls a fabricated plausible output: not a wrong value, a value whose meaning was assumed. What is NOT minted here: no swap-specific verdict enum (std.upsert_decision.ObservationVerdict already spans Converged/Absent/Drifted/Conflict/Inaccessible/UnknownRefused) and no swap observation carrier (extdeps.os.free.SwapStats is the cited one, grounded on the free(1) man page, and it is reused verbatim rather than re-decomposed here)." +data host_swap_backing_authority_note: String = "THE host swap-BACKING axis, and it exists because the corpus already converges a swap CAP over a resource whose existence nothing models. gunbc.runner_slot_allocation declares memory_swap_max = 34359738368 (32 GiB) per runner slot; gunbc.host_converge drives it onto every host as MemorySwapMax through the per-slot drop-in at gunbc_runner_per_slot_swap_dropin_path, and gunbc.runner_unit_live_read reads it back and reports Converged when the cgroup property matches. Every one of those steps is correct in isolation and the composition still proves nothing, because MemorySwapMax is a CEILING: systemd accepts it, reports it, and matches it byte-for-byte on a host with zero swap devices. The knob converges green over a resource that does not exist. That is the presupposition failure this module makes representable — a cap is evidence about a resource only once the resource is observed present — and it is the shape DESIGN §5 calls a fabricated plausible output: not a wrong value, a value whose meaning was assumed. What is NOT minted here: no swap-specific verdict enum (std.upsert_decision.ObservationVerdict already spans Converged/Absent/Drifted/Conflict/Inaccessible/UnknownRefused) and no swap observation carrier (extdeps.tools.free.SwapStats is the cited one, grounded on the free(1) man page, and it is reused verbatim rather than re-decomposed here)." data host_swap_backing_requirement_is_derived_note: String = "The requirement is DERIVED from the declared cap, never authored per host, and that is the whole reason this module can exist without fabricating anything. Nobody in this session can read /proc/swaps on srv1..srv4 — the reach gap is the A1 lane — so any table of per-host swap sizes written here would be invention dressed as a model. The derivation needs no such reading: declaring a nonzero MemorySwapMax IS declaring that swap backing must exist, so the requirement falls out of gunbc_runner_slot_desired().memory_swap_max, and it moves automatically when that number moves. DECLARED LIMIT, stated rather than papered over: min_total is the PER-SLOT cap, the amount a single runner alone can demand, and not slots-per-host x cap. Whether five concurrent slots can each reach their ceiling is an aggregate-scheduling question this module does not answer, and answering it by multiplication would assert a worst case nobody has measured. So the requirement is a floor below which the declared caps are provably unsatisfiable, and it is honest about being a floor." @@ -111,7 +111,7 @@ fn swap_cap_verdict_gate_accepts( } } -data host_swap_backing_observation_frontier_note: String = "The live producer, and it returns none for every host on purpose. There is no /proc/swaps reader and no free(1) transport in the tree — extdeps.os.free carries the cited SHAPE and has zero live producers today — so the honest observation for all four hosts is absence, and the derived verdict for all four is UnknownRefused. Writing a fixture here and reading it back would be the specification-without-execution trap in its purest form (DESIGN §5): the matrix would go green against numbers this module itself authored. The count of unobserved hosts is exported instead, so the deficit is a NUMBER that must change when a producer lands, never a silence. Realization is blocked on one named thing and it is not swap-specific: the argv materializer binds a hardcoded five-parameter vocabulary (path, service, operation, package, bin, args, unit), so fallocate/mkswap/swapon/fstab and a /proc/swaps read cannot be expressed as typed host effects until that binding is generic. That materializer has no .dag declaration to bind a scaffold to — it is a v1 seed builtin, which is part of why it is the blocker — so the scaffold binds the transport type it materializes into. Declaring those operations before then would add rows to the shell-to-dag census that no consumer can reach, which is the parallel-representation debt the census exists to prevent." +data host_swap_backing_observation_frontier_note: String = "The live producer, and it returns none for every host on purpose. There is no /proc/swaps reader and no free(1) transport in the tree — extdeps.tools.free carries the cited SHAPE and has zero live producers today — so the honest observation for all four hosts is absence, and the derived verdict for all four is UnknownRefused. Writing a fixture here and reading it back would be the specification-without-execution trap in its purest form (DESIGN §5): the matrix would go green against numbers this module itself authored. The count of unobserved hosts is exported instead, so the deficit is a NUMBER that must change when a producer lands, never a silence. Realization is blocked on one named thing and it is not swap-specific: the argv materializer binds a hardcoded five-parameter vocabulary (path, service, operation, package, bin, args, unit), so fallocate/mkswap/swapon/fstab and a /proc/swaps read cannot be expressed as typed host effects until that binding is generic. That materializer has no .dag declaration to bind a scaffold to — it is a v1 seed builtin, which is part of why it is the blocker — so the scaffold binds the transport type it materializes into. Declaring those operations before then would add rows to the shell-to-dag census that no consumer can reach, which is the parallel-representation debt the census exists to prevent." data host_swap_backing_realization_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority,