microVM lifecycle controller decisions + host-local CellReadiness store; admission consumes cell readiness

dag/gunbc/product/fabric/sanitation.dag

@@ -47,26 +47,49 @@ type SanitationFact
   | CgroupEmpty
   | MountsRemoved
   | NetworkNamespaceRemoved
+  | SlotNetworkQuiescent
   | WritableLayersDeleted
   | SecretsRemoved
 
+// THE NETWORK FACT DEPENDS ON WHO OWNS THE NETWORK, AND THE TWO OWNERS OWE DIFFERENT FACTS.
+//
+// A sandbox whose network namespace is created per attempt owes its REMOVAL: a namespace that
+// survives can hold the previous tenant's listening socket. A sandbox attached to network state the
+// SLOT owns across attempts -- a microVM's tap and nft rules, converged per slot -- owes no removal,
+// because that state exists by design between attempts. What it owes instead is QUIESCENCE: nothing
+// holds the slot's interface, no connection-tracking state for the reused guest address survives,
+// and the ruleset is the converged one. These are different contracts, so they are different facts
+// rather than one name read two ways; and the scope is declared on the readback, so which one is
+// required is decided here rather than by whichever consumer maps its observation onto a name.
+type SandboxNetworkScope
+  = AttemptScopedNetwork
+  | SlotScopedNetwork
+
 fn sanitation_fact_label(fact: SanitationFact) -> String {
   match fact {
     NoSurvivingProcesses => "no-surviving-processes"
     CgroupEmpty => "cgroup-empty"
     MountsRemoved => "mounts-removed"
     NetworkNamespaceRemoved => "network-namespace-removed"
+    SlotNetworkQuiescent => "slot-network-quiescent"
     WritableLayersDeleted => "writable-layers-deleted"
     SecretsRemoved => "secrets-removed"
   }
 }
 
-fn required_sanitation_facts() -> List<SanitationFact> {
+fn network_sanitation_fact(scope: SandboxNetworkScope) -> SanitationFact {
+  match scope {
+    AttemptScopedNetwork => NetworkNamespaceRemoved
+    SlotScopedNetwork => SlotNetworkQuiescent
+  }
+}
+
+fn required_sanitation_facts(scope: SandboxNetworkScope) -> List<SanitationFact> {
   [
     NoSurvivingProcesses,
     CgroupEmpty,
     MountsRemoved,
-    NetworkNamespaceRemoved,
+    network_sanitation_fact(scope: scope),
     WritableLayersDeleted,
     SecretsRemoved,
   ]
@@ -105,6 +128,7 @@ fn observation_confirms(observation: SanitationObservation) -> Bool {
 type SanitationReadback {
   cell: CellId
   sandbox: SandboxId
+  network_scope: SandboxNetworkScope
   observations: List<SanitationObservation>
 }
 
@@ -153,7 +177,7 @@ fn unproven_for_required(
 }
 
 fn unproven_facts(readback: SanitationReadback) -> List<UnprovenFact> {
-  fold(required_sanitation_facts(), init: [], f: (acc, required) =>
+  fold(required_sanitation_facts(scope: readback.network_scope), init: [], f: (acc, required) =>
     concat(acc, unproven_for_required(readback: readback, required: required)))
 }
 
@@ -203,10 +227,11 @@ fn cell_readiness_line(readiness: CellReadiness) -> String {
 // a missing report as nothing-to-clean. That is the same narrow one level out: no observation
 // becomes no problem. An absent readback yields every required fact unobserved, so the cell
 // quarantines with a full list rather than returning to supply.
-fn readiness_without_readback(cell: CellId, sandbox: SandboxId) -> CellReadiness {
+fn readiness_without_readback(cell: CellId, sandbox: SandboxId, network_scope: SandboxNetworkScope) -> CellReadiness {
   cell_readiness_after(readback: SanitationReadback {
     cell: cell,
     sandbox: sandbox,
+    network_scope: network_scope,
     observations: [],
   })
 }

dag/gunbc/runner/runner_microvm.dag

@@ -46,6 +46,11 @@ import gunbc.runner_unit {
   lifecycle_intent_stops_finished_incarnation,
   gunbc_runner_main_exits_when_incarnation_ends,
 }
+import product.fabric.sanitation { CellId }
+import gunbc.runner_microvm_cell_readiness {
+  CellIncarnationAdmission, CellIncarnationAdmitted, CellRecoveryRequired, CellWithdrawn,
+  HostWithdrawn, HostWithdrawal, CellWithdrawal, CellBoundAttempt,
+}
 import extdeps.github.actions_runner {
   ActionsRunnerRelease, actions_runner_release_2_337_0, actions_runner_jitconfig_env_name,
 }
@@ -815,15 +820,22 @@ type VmmProcessTopology = VmmIsMainProcess | VmmUnderLifecycleController
 // re-deriving it. Stating the dependency in prose would have left it satisfiable by an author who
 // never read the paragraph.
 //
-// THIS IS A NECESSARY GATE, NOT A SUFFICIENT ONE, and the gap is a declared frontier. The predicate
-// is static: it says a finished incarnation makes systemd issue a stop that reaches the cgroup. It
-// cannot say the VMM is gone afterwards -- a task in uninterruptible sleep survives SIGKILL, and a
-// main process that outlives its incarnation issues no stop at all -- nor that the cell is safe to
-// reuse. That is gunbc.product.fabric.sanitation's CellReadiness, established by a terminalizer's
-// readback, which this admission will consume once the terminalizer lands. Until then an Admitted
-// verdict here is not sufficient grounds to run customer work.
+// THE TOPOLOGY GATE IS NECESSARY, NOT SUFFICIENT, and the cell's readiness is the other half. The
+// predicate is static: it says a finished incarnation makes systemd issue a stop that reaches the
+// cgroup. It cannot say the VMM is gone afterwards -- a task in uninterruptible sleep survives
+// SIGKILL -- nor that the cell is safe to reuse. That is gunbc.product.fabric.sanitation's
+// CellReadiness as held across incarnations by gunbc.runner_microvm_cell_readiness, whose admission
+// joins the allocation generation to the readiness recorded at the previous one. It is consumed
+// FIRST, before any static gate: a cell that is withdrawn is withdrawn whatever the VM looks like,
+// and reporting a malformed VM for a quarantined cell would send the operator to the wrong fact.
+// Its three non-admitting arms stay three arms here, because their remedies differ: host grain (fix
+// the store; no cell on the host may start), cell grain (this cell's readback), and recovery required
+// (not a refusal to act but the instruction to run the lost attempt's teardown first).
 type RunnerMicroVmAdmission
   = RunnerMicroVmAdmitted
+  | RunnerMicroVmRefusedHostWithdrawn { withdrawal: HostWithdrawal }
+  | RunnerMicroVmRefusedCellWithdrawn { cell: CellId, withdrawal: CellWithdrawal }
+  | RunnerMicroVmRecoveryRequired { bound: CellBoundAttempt }
   | RunnerMicroVmRefusedOrphanableUnit { reason: String }
   | RunnerMicroVmRefusedSharedCredential { reason: String }
   | RunnerMicroVmRefusedMalformedVm { reason: String }
@@ -843,6 +855,31 @@ type RunnerMicroVmAdmission
 // instead of writing it. Collapsing them into one cause is the state-space conflation DESIGN names,
 // and it would send an operator to the wrong module.
 fn runner_microvm_admission(
+  cell: CellIncarnationAdmission,
+  topology: VmmProcessTopology,
+  intent: RunnerUnitLifecycleIntent,
+  main_exits_when_incarnation_ends: Bool,
+  transport: JitCredentialTransport,
+  config: FirecrackerVmConfig,
+  reserve: RealizationReserve,
+) -> RunnerMicroVmAdmission {
+  match cell {
+    HostWithdrawn { withdrawal: w } => RunnerMicroVmRefusedHostWithdrawn { withdrawal: w }
+    CellWithdrawn { cell: c, withdrawal: w } => RunnerMicroVmRefusedCellWithdrawn { cell: c, withdrawal: w }
+    CellRecoveryRequired { bound: b } => RunnerMicroVmRecoveryRequired { bound: b }
+    CellIncarnationAdmitted { cell: _, generation: _ } =>
+      runner_microvm_admission_after_cell(
+        topology: topology,
+        intent: intent,
+        main_exits_when_incarnation_ends: main_exits_when_incarnation_ends,
+        transport: transport,
+        config: config,
+        reserve: reserve,
+      )
+  }
+}
+
+fn runner_microvm_admission_after_cell(
   topology: VmmProcessTopology,
   intent: RunnerUnitLifecycleIntent,
   main_exits_when_incarnation_ends: Bool,
@@ -1026,10 +1063,12 @@ fn attach_workspace_drive(config: FirecrackerVmConfig, path: FilePath) -> Firecr
 // gunbc_runner_lifecycle_intent rather than by an author's assertion. It moves the day that intent
 // is deployed, and not before.
 fn gunbc_runner_microvm_admission(
+  cell: CellIncarnationAdmission,
   topology: VmmProcessTopology,
   config: FirecrackerVmConfig,
 ) -> RunnerMicroVmAdmission {
   runner_microvm_admission(
+    cell: cell,
     topology: topology,
     intent: gunbc_runner_lifecycle_intent,
     main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends,

dag/gunbc/runner/runner_microvm_attempt.dag

@@ -32,7 +32,10 @@ data runner_microvm_attempt_disposition: Disposition = SingleAuthority
 //   BOUNDARY  the VMM runs in the cell's slice, so the guest's CPU, memory and task consumption is
 //             accounted to the cell that was reserved -- a VM outside the slice is invisible to
 //             every limit the cell carries and to every observation that reads them.
-//   LIFETIME  the cell is not releasable until teardown is PROVEN, not attempted.
+//   LIFETIME  the cell is not releasable until teardown is PROVEN, not attempted. That verdict is
+//             gunbc.product.fabric.sanitation's CellReadiness, derived from host readbacks by
+//             gunbc.runner_microvm_lifecycle and held across incarnations by
+//             gunbc.runner_microvm_cell_readiness; this module owns no second release verdict.
 //
 // A guest missing any one of these is refused rather than downgraded, because each failure is
 // silent in production: unbound storage looks like a working VM until two attempts collide,
@@ -242,36 +245,3 @@ fn bind_owned_attempt(attempt: MicroVmAttempt, owned: Bool) -> MicroVmCellBindin
     }
   }
 }
-
-// TEARDOWN IS PROVEN, NOT ATTEMPTED, AND THE CELL IS NOT RELEASABLE WITHOUT THE PROOF.
-//
-// The arms are separate because they are different events with different remedies. A VMM that
-// exited but left its attempt directory populated is a cleanup bug; a VMM still running is a
-// LEAK, and releasing the cell under it would hand a reserved boundary to a second guest while the
-// first still executes in it. There is deliberately no arm meaning "probably fine".
-type MicroVmTeardownVerdict
-  = TeardownProven
-  | TeardownVmmStillRunning { unit: NonEmptyStr }
-  | TeardownResidueRemains { path: String }
-  | TeardownNotObserved { cause: String }
-
-fn microvm_cell_releasable(verdict: MicroVmTeardownVerdict) -> Bool {
-  match verdict {
-    TeardownProven => true
-    TeardownVmmStillRunning { unit: _ } => false
-    TeardownResidueRemains { path: _ } => false
-    TeardownNotObserved { cause: _ } => false
-  }
-}
-
-fn microvm_teardown_verdict_text(v: MicroVmTeardownVerdict) -> String {
-  match v {
-    TeardownProven => "teardown=proven"
-    TeardownVmmStillRunning { unit: u } =>
-      join(["teardown=REFUSED vmm still running (", u as String, "); releasing the cell would hand a live boundary to a second guest"], "")
-    TeardownResidueRemains { path: p } =>
-      join(["teardown=REFUSED residue remains at ", p], "")
-    TeardownNotObserved { cause: c } =>
-      join(["teardown=REFUSED not observed (", c, "); an unobserved teardown is not a completed one"], "")
-  }
-}