Record the microVM, floor and per-VM-memory state at wind-down

docs/plans/microvm-and-floor-wind-down-state.md

@@ -0,0 +1,251 @@
+# microVM and floor: wind-down state, 2026-09-21
+
+Written on operator instruction to wind down and record remaining items, so that v1
+performance and v2 migration can be prioritised. **This is a state record, not a plan**: it
+says what is true on `origin/main`, what is owed, and what is blocked, so that resuming any
+lane does not begin by re-deriving it.
+
+Every claim below was verified against `origin/main` at `7a145ef9ca` or read from the lane
+that produced it. Where a claim is **contested**, it is marked, and neither version is
+asserted — DESIGN §4d: a bet is typed as a bet, and the reader who consumes it as a fact is
+the defect.
+
+**Consumer, and a declared frontier (DESIGN §3c).** This page is cited by path from the two
+re-entry briefs that govern the parked programs, which is where a resuming session reads it.
+It is **not** linked from `DESIGN.md`, and it deliberately does not add a
+`gunbc.design_document` row to become so: it is a dated state record rather than a doctrine
+a DESIGN section governs, and editing that authority is not a wind-down act. It therefore
+joins the orphan population already rostered as `gunbc.guarantee_stall`
+`doc_graph_orphan_population_stall` (`current: OutsideTheLadder`), and this paragraph is the
+admission rather than a silent addition. **Trigger for the frontier:** whichever funded lane
+resumes a program named here either links this page from the section that governs its work,
+or supersedes it and deletes it. A wind-down record that outlives the wind-down is debt.
+
+**On the numbers below.** Where a figure is load-bearing it is stated with the producer that
+re-derives it (DESIGN §6: name the instrument, never transcribe its output). Where a figure
+is a lane's reported reading rather than a re-derivable instrument, it is attributed to that
+lane and marked as such — those are receipts of a past run, not facts a reader may refresh,
+and they are written so that staleness is visible rather than plausible.
+
+---
+
+## 1. The floor reports SUCCESS over its own refusal — the highest-value open item
+
+`.github/workflows/witnesses.yml:67`:
+
+```
+if [ "$GUNBC_FLOOR_CLASS" = structural ] && [ "$GUNBC_FLOOR_EXIT" -eq 0 ]; then GUNBC_FLOOR_CLASS='none'
+```
+
+`claim_executor` **exits 0 over its own typed refusal**, so the class is downgraded to `none`
+and the job concludes success. A job can therefore report SUCCESS over a run that executed
+**zero witnesses**, with its own log saying `phases_failed=1`.
+
+**This is not merely a hidden defect — it admitted a new one.** #11731 landed a file that
+could not parse *because* the floor was refusing and reporting success. The hollow gate is
+upstream of the breakage, not downstream of it (§5: a failure arm must refuse, never widen;
+the downgrade is an absorbing fallback executed in YAML).
+
+**Current standing.** The parse class is **closed**: the indented-annotation census is 0
+corpus-wide and the floor selects and executes its full planned set, with `not_attempted=0`
+and `claims_failed=0`, where previously **zero** witnesses were selected. Closed by #11896,
+#11897, #11880, #11920, #11842. **Re-derive rather than trust this sentence:** the producer
+is the required floor itself — `claim_executor --required-ci --source-root dag
+--source-root src/v2 --required-lane witnesses` — whose run prints its own
+`planned/executed/not_attempted/terminal/passed` summary line. The counts move with every
+landed witness, so a number copied here would rot within a day.
+
+**CONTESTED — do not propagate either reading.** Whether the downgrade swallows failures
+*per phase* is disputed by two lanes:
+
+| reading | source | consequence if true |
+|---|---|---|
+| per-phase: parse reds the job honestly, declarations passes | `nimble-swift-273` | once parse cleared, a **declarations defect is invisible** |
+| no such ordering | four run observations | the discriminator is unknown |
+
+The four observations: main `0de0b6137c7` 13 parse FAILs → **SUCCESS**; #11803 `70faed05501`
+340 → **SUCCESS**; #11842 343 → **FAILURE**; #11884 317 → **FAILURE**. No ordering by count,
+and parse failures did **not** always red the job. `eager-swift-412` independently reports
+the discriminator as **cannot-tell from the logs**.
+
+**The discriminating test nobody has run**, and it is cheap: read `$GUNBC_FLOOR_LOG` — a
+**file** the floor writes, *not* the job log, where every `class=` line is echoed script — or
+the classifier itself, on **one PASS and one FAIL of the same phase shape**. Counting
+signature strings in the GHA job log is **not** discriminating: a fired signature sets an env
+var rather than printing, so identical counts appear whether the hypothesis holds or not.
+
+**#11836 and #11829 are competing repairs. Only one should land.** Neither is owned.
+
+## 2. microVM: the part that decides is built; the part that acts is not
+
+`gunbc.runner_microvm_lifecycle_realize` **landed** (#11803) and has executed against real
+processes on srv1: the lane reported every claim group green at its landing head, including
+the wet receipt under `--wet` and the argv-binding wall. That is a **lane receipt of a past
+run**, not a standing fact — re-derive it with `claim_batch` over the module's witness
+modules at the current head before relying on it. #11677 closed both launch frontiers, so
+the JIT credential mint and jail staging are realized.
+
+**Five declared frontiers, all live in that one landed module.** Read them from the file,
+not from here.
+
+| # | frontier | status | what is missing |
+|---|---|---|---|
+| 1 | `controller_main_pid_consumer_frontier` | **dispatchable, start here** | **nothing calls `run_controller`.** Until a slot unit execs it as MainPID the module is a library, not a controller. Every other frontier is worth less until this clears. |
+| 2 | `attempt_cleanup_realization_frontier` | dispatchable | no unmount, no delete of credential device / workspace / attempt root, no flush. The **only** host mutation in teardown is the `cgroup.kill` write. |
+| 3 | `guest_bring_up_channel_frontier` | dispatchable, spans host+guest | no guest→host readiness channel above `VmmStarted`. Decides only whether a slot is SERVING, never whether a cell is CLEAN. |
+| 4 | `slot_network_readings_producer_frontier` | **BLOCKED — security** | no converged slot network on any host; every reading is `Unreadable`, which quarantines. |
+| 5 | `workflow_effect_sequencing_frontier` | **not a lane — a design question** | `std` carries **no** effect-sequencing authority. Bigger than microVM: every effect sequence in the corpus rests on the answer. |
+
+**The consequence that governs planning:** the module states it itself — *"no cell settles
+CellReady through this module today."* **A first full run quarantines by construction, and
+that is not a bug in the readbacks.** A warm pool is impossible until (4) clears.
+
+> Do not let anyone "fix" (4) by omitting `SlotNetworkQuiescent` from the required facts.
+> That is the empty-observation narrow `product.fabric.sanitation` exists to refuse.
+
+### Why (4) is blocked, stated so the reason survives
+
+**The converge principal IS the job principal.** Granting it install+restart over files it
+also *stages* is granting root: `install <grantee-writable-source> /etc/systemd/system/…`
+followed by `systemctl restart` is root-equivalence, however narrowly spelled. So
+`microvm_network_granted_operations` deliberately carries **readbacks only**.
+
+To unblock, an administrator principal must (1) own the staged source so the job user cannot
+write what root will install and execute; (2) install the nft loader unit and ruleset and
+`daemon-reload` + restart it; (3) set `ip_forward` and create the bridge; (4) create and
+destroy per-attempt taps — and be **unimpersonable by the job user**. That last is the whole
+point, and is why the frontier trigger names a *capability* rather than an artifact (§4b(3)).
+
+#11751 (`microvm_network_observe`) is in the merge queue at `cd2041cc69a`. It **installs
+nothing**, reads every fact with its own UNREAD arm, and mints `ConvergedNetwork` only when
+every fact was actually read. On every host today it will **refuse**, because nothing has
+installed a tap or the table — that is honest, not a failure.
+
+### The floor's own job does not fit a cell
+
+`runner_microvm_floor_fit_stall` remains rostered: the floor's measured held-set peak exceeds
+`gunbc.runner_slot_allocation` `gunbc_runner_slot_memory_max_bytes` less the realization
+reserve. Both sides are derivable rather than transcribed — the cap is that declaration, and
+the demand is produced by `gunbc.floor_memory_demand`, whose qualification against readable
+limits is what the stall cites. The stall row itself carries the figures it was written
+against; read them there, where they sit beside the reading that produced them.
+
+**Grounding it is an operator decision with a fleet cost**, not an engineering task: raise
+per-slot `MemoryMax` to ~28 GiB, which **lowers each host's memory-admitted width**, or
+reduce floor demand. The stall explicitly rules out deleting the allowance, reserve or
+receipt, and rules out using a fixture cell.
+
+### The milestone that would settle the cutover question
+
+**One cell settling `CellReady` once, on one host, after one real job.** Nothing before that
+is evidence. If that cannot be reached, the remaining work is unbounded.
+
+## 3. Dynamic per-VM memory — two compiling, unreconciled implementations
+
+Design ruled and approved by the side chat; **build parked**. Six items; item 1 is built
+**twice, independently, blind to each other**.
+
+**Neither branch is uncompiled.** The uncompiled attempts are the two *closed* PRs, #11849
+and #11850.
+
+| branch | sha | evidence | carries uniquely |
+|---|---|---|---|
+| `session/bright-ram-63` | `125659f70df` | lane-reported: all claims green under `claim_batch`, plus five mutation controls, tree restored green after each | the **executed** authority-token wall |
+| `session/royal-moth-544` | `80ec5065822` | lane-reported: all claims green under `claim_batch`, two mutation controls executed | `std.measure round_up_to_grain` (resolves the unowned rounder fork), ceiling-as-parameter, permit-in-provenance |
+
+The same three file paths exist on both with different contents, so **merging them is a
+textual conflict on every file, not a union.** Pick one base and port the other's evidence.
+
+**Both PRs (#11883, #11885) were found NON-DRAFT on 2026-09-21, although both lanes believed
+they had left them draft** — so a parked program was consuming CI and reviewer attention on
+every push. Both were converted back to draft at wind-down. Keep them draft while parked:
+ready buys coverage that was never approved. *The lesson is the gap itself* — "I left it
+draft" is a belief about a past action, and the dashboard opens PRs on a lane's behalf, so
+it must be re-read rather than remembered.
+
+**The defect, stated correctly** (it is a bypass, not an absence). All three verified against
+`origin/main`:
+
+- `CellReserved` holds exactly four fields — offer, slot_key, generation, account. **No
+  requirement, no grant, no envelope.**
+- `admit_executor_capacity` takes a whole `ExecutionRequirements` and reads exactly **one**
+  field, `requirements.capacity_class`. **Cell admission does not consider memory.**
+- `unmet_memory_axis` returns `[]` when `needed.envelope.memory` is `Absent`, so **unstated
+  memory is admitted** by the supply screen rather than refused.
+
+So memory *is* screened before reservation and the runner *does* read the requirement; what
+is missing is that memory is never converted into a **grant**, never **atomically reserved**
+against live host use, and never **carried on `CellReservation`**.
+
+`MemoryGrant` and `HostMemoryLedger` return **zero matches anywhere on main**, so items 3-6
+have no landed symbols to integrate against. The coordination hazard for item 4 (#11625,
+static-vs-dynamic `MemoryHigh`/`MemorySwapMax`) is still **open**, but its head has moved to
+`8e75da2aa48` — re-read it before item 4 rather than trusting any recorded sha.
+
+**Topology precondition, a gate rather than an item:** exact per-Work sizing is valid only
+where Work is bound **before** the VM boots. A generic prebooted GitHub runner does not know
+its eventual job. Do not let a guest discover its Work after boot and call that dynamic
+allocation.
+
+**Amendment worth not re-litigating:** a per-host **CAS-linearized** ledger is required.
+Per-cell records cannot conserve a host-wide sum — A and B each read 60 of 100 free, each
+reserve 30, both succeed, 120 committed. One CAS commits cell occupancy and memory claim
+together.
+
+## 4. Owed evidence
+
+**#11845's discriminating RED was never executed.** The repair is real and approved, and it
+lands on a green that is hollow for the two reasons in §1. Branch
+`verify/11845-red-mutation` (`2499194f4b2`) is pushed and is exactly one hunk off the merge
+head: the `test -e` defect put back inside the new classifier. **Both of its blockers have
+since cleared**, so the pair is now runnable — expect green at the merge head, red at
+`2499194f4b2` on `an_unread_path_reaches_unobservable_and_never_absent`. **If the mutation
+passes, the control does not discriminate and the repair needs a better one.** Delete that
+branch afterwards; `verify/11845-red-control` is plain main and can go now.
+
+**Two unowned repairs**, both one-liners, both real:
+
+- `v2.lens.reference_derived_residency_reading` has zero occurrences of
+  `construction_justification`, while its siblings import it from `v2.lens.common`.
+- `dag/test/claim/machine_intake/jade_first_contact_model_witness_test.dag:3` imports `Nat`
+  from `std.types`; `Nat` is declared in `dag/std/nat.dag`.
+
+**`required_gate_prefixes` has no `dag/test/claim/runner/` row**, so that file is never
+resolved by CI unless a diff touches it — a symbol deletion can strand it silently, as
+#11762 did. Likewise no row matches `test.claim.fabric.`, so the dynamic-memory witnesses are
+discovered and declined.
+
+## 5. The P0 that opened this session is contained but not closed
+
+srv2 still carries `ExitType=cgroup` in
+`/etc/systemd/system/actions-runner@.service.d/70-fleet-teardown.conf` — the configuration
+that left PID 56295 orphaned holding 16 GB for 2.7 days. srv1 and srv3 are converged to
+`ExitType=main`.
+
+**Residual risk, precisely.** srv2-01..05 are **masked**, so the P0 cannot recur on them
+today. But the drop-in lives in the **template** directory and the template is *not* masked,
+so any **new** instance (`actions-runner@srv2-06`) inherits `ExitType=cgroup`. The remedy is
+to run the modelled fleet converge on srv2; it has simply never run there.
+
+srv4 is off the reach chain (container → srv1 → srv2-lan → srv3) and `gunbc.fleet_reach`
+carries no row for it.
+
+## 6. Method findings worth keeping
+
+- **A suite of controls that invoke a pure decision with supplied values is blind to
+  everything after the decision** — the cleanup leg, the receipt the withheld arm writes —
+  and stays blind however many are added. Two post-sign-off findings on #11902 both lived in
+  that one gap. **38/38 is not route coverage.**
+- **A repair of a fail-open is a prime site for the same class one layer down.** #11902's
+  own (d) repair discarded the located cause on its withheld arm and wrote a constant. Grep
+  every declaration your repair *adds* for a call site before pushing, and re-read every new
+  refusal arm for whether it names which fact failed.
+- **At any power-of-two grain, a checked-add rounder and a subtraction rounder refuse the
+  same set**, because 2^63 is a multiple of the grain. A gibibyte-grain mutation control
+  stayed green under the mutation. Use a non-power-of-two grain (1000). Two authors asserted
+  the opposite from reasoning alone; both were wrong.
+- **A refusal-arm claim tests that the arm fires, not that the right inputs reach it.** That
+  is how two lanes and a reviewer converged on bounding by the maximum instead of by
+  representability.
+- **`claim_batch` exits 0 over its own refusal.** A `*Refused` line is a **non-answer** —
+  neither pass nor fail — and exit status must never be read as the verdict.