diff --git a/dag/gunbc/host_swap_backing.dag b/dag/gunbc/host_swap_backing.dag new file mode 100644 index 00000000000..3dffd257cab --- /dev/null +++ b/dag/gunbc/host_swap_backing.dag @@ -0,0 +1,150 @@ +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.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.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." + +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 { + 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." + +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.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, + 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..dd2d10e4b6a --- /dev/null +++ b/dag/gunbc/readback_independence.dag @@ -0,0 +1,112 @@ +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 { + 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." + +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/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 + } + } +} 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() +} 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) +} 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 |