srvN quality sweep: enrollment wall, swap-backing axis, read-back independence criterion

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<HostIdentity>) -> 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)
+}

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 <property>",
+  subject: "cgroup property value on a unit",
+  effect_on_subject: ProbeInert,
+}
+
+data systemd_is_active_probe: ReadBackProbe = ReadBackProbe {
+  label: "systemctl --user is-active <unit>",
+  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<ReadBackProbe> = [
+  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()
+}