diff --git a/FABRIC-3.5.md b/FABRIC-3.5.md index 4d6bbeaa..50ba1f7f 100644 --- a/FABRIC-3.5.md +++ b/FABRIC-3.5.md @@ -619,8 +619,9 @@ build-time check.** teardown path must reach `STADIUM-EVICT`, verifiable via `fleet_conserved`. - ~~**Item 17**~~ — **SETTLED 2026-09-19 by §XXIV**: a separate word; `BYE` left alone. The reshuffle therefore changes zero live registered words. -- **Item 18 (§XVI.7)** — if Hera is already dead, nobody performs the halt. Proposed shape (an - empty floor as a kernel-observable condition) is **analysis, not a ruling.** +- ~~**Item 18**~~ — **SETTLED 2026-09-19 by §XXVII**: the empty floor is unreachable (Hera is + pinned, unkillable, and every path by which she can cease already halts or reboots the + machine). Build nothing; §XVI.7's proposed shape is withdrawn. §XIII.5's proposed Hestia resolution shape remains **analysis, not a ruling.** §XIV.4's and §XIV.5's proposals were both superseded by §XV.4 and §XV.3 respectively. @@ -2556,7 +2557,7 @@ execution. | 6 | Kernel-Hermes; the sinking latch; `SOS` type 10 | §III, §XXI, §XXIII | | 7 | `BIRTH` generalization + ACL/DNA inheritance | §VI, §XV.1 | | 8 | The Hera-only suicide word (`SCUTTLE` recommended); pin beside `BIRTH` | §XXIV | -| 9 | **⬜ DECIDE: item 18** — the empty-floor halt when Hera is already gone | §XVI.7 | +| 9 | ~~item 18~~ — **CLOSED §XXVII**: empty floor unreachable, build nothing | §XXVII | | 10 | Teardown paths reach `STADIUM-EVICT`; verify via `fleet_conserved` | §XV.4 | | 11 | Category B strips, each as coding proves the item dead | §XXII.4 | | 12 | Isabelle/HOL pass — deliverable is the restated boundary | §XXV | @@ -2568,3 +2569,97 @@ execution. **No code is authorized by this document.** Per Captain Bob's Law, nothing on this list starts without an explicit instruction. + +--- + +## XXVII. Item 18 SETTLED: the empty floor is unreachable — build nothing + +§XVI.7 raised it and §XVI.7's own proposed shape (the kernel observing an empty floor and +halting) was offered as analysis. **Tested against the code 2026-09-19, the premise is false: +the state cannot occur.** The ruling is therefore to build nothing, and the value of the item +is the invariants it surfaced. + +### XXVII.1 — The premise, tested + +**An empty Stadium floor requires Hera to be gone.** Every other VM is her descendant, and +`capsule_vm_kill_all_nonmama()` spares her by construction. So item 18 reduces to: *can Hera +cease to exist while the machine keeps running?* + +Five paths, all traced: + +| Path | Result | Evidence | +|---|---|---| +| **Compudynamic death** (heat decay / `COOL`) | **Impossible** — she is pinned | `stadium.c:453` `if (header->flags & STADIUM_FLAG_PIN) return -1;`; `:559` `if (h->flags & STADIUM_FLAG_PIN) continue;`. Hera is pinned via `session_set_pinned()` (§H.10/§H.12 step 4) | +| **`KILL`** | **Impossible** — refused | `mama_word_kill()`'s own doc: "Destroy a named VM unconditionally. **Hera cannot be killed.**" | +| **Reaped with the children** | **Impossible** — spared by name | `capsule_vm_kill_all_nonmama()` | +| **`BYE`** | Machine **reboots** | `arch_cold_reset()` (§XXIV.2) — not a lingering state | +| **Scuttle** (§XXIV) / **panic** | Machine **halts** | Both end in a permanent `arch_halt()` loop | + +**Every path by which Hera can cease already terminates the machine.** There is no route to a +live kernel over an empty floor. + +**Note the pinning result generalises:** all three Tripod legs are pinned by the same +`is_fleet_foundation` line (§XIII.3), so **no Tripod leg can die a compudynamic death.** §XV.2's +compudynamic death applies to the unpinned population — identity VMs, agent VMs — which is +exactly where it was always aimed. + +### XXVII.2 — RULING: build nothing + +`.claude/CLAUDE.md` is direct about this class: *"Don't add error handling, fallbacks, or +validation for scenarios that can't happen."* An empty-floor halt would be precisely that — +defensive code for an unreachable state, carrying its own maintenance and its own risk of +firing wrongly. **§XVI.7's proposed shape is withdrawn, not adopted.** + +A supporting argument, recorded but *not* load-bearing (the ruling stands on §XXVII.1 alone): +even were the state reachable it would be provably terminal rather than a judgement call, since +`BIRTH` is a word a VM must call — **zero VMs means zero possible births**, so nothing could +ever run again. That is a dead end, not a decision. But it is moot. + +### XXVII.3 — The panic path already is the empty-floor halt + +`sk_hal_panic()` (`hal/hal.c:490-506`) prints `System halted.` and executes: + +```c +while (1) { + arch_halt(); +} +``` + +**That is character-for-character the idiom §XXIV.2 specified for Hera's suicide word.** The +two converge on the same terminal state by different triggers, which is a pleasing consistency +rather than a duplication: **a scuttle is a panic Hera chose.** Whatever kills her involuntarily +already routes here; what she does deliberately looks the same from outside. Nothing new is +needed at either end. + +### XXVII.4 — What this ruling depends on: three invariants to defend + +The ruling is conditional on facts that a future change could break silently. **State them as +invariants, since that is the durable part of this item:** + +1. **Hera stays pinned.** If she is ever admitted unpinned, or the `is_fleet_foundation` triple + (`capsule_birth.c:793-796`) stops covering her, she becomes evictable and the empty floor + becomes reachable. **Note this triple is edited by this very reshuffle** (§XIX.6, Hermes out, + Hestia in) — so the change most likely to break this is one already on the punch list. +2. **`KILL` keeps refusing Hera**, and any new teardown path spares her the way + `capsule_vm_kill_all_nonmama()` does. §XXVIII's already-confirmed unguarded-kill UAF shows + this area has been got wrong before. +3. **Every involuntary-death path ends at `sk_hal_panic()` or an equivalent permanent halt** — + never at a `return` that leaves the kernel looping over nothing. + +**If all three hold, the empty floor cannot occur and no code is needed. If any is broken, this +ruling must be revisited rather than patched around.** + +### XXVII.5 — Design phase complete + +**Every design question this document opened is now ruled.** Item 18 was the last, and it +closes by dissolution — the fourth to do so, after §XIV.2's four, §XV.2's two and §XX's one. + +That pattern is worth naming as the document closes its design phase: **of the questions that +dissolved rather than resolved, every one turned out to rest on a premise the code did not +support** — a supervisor that was not needed, a declarer that could not exist, a suffix that was +never load-bearing, a state that cannot occur. The design got simpler each time it was checked +against the tree rather than reasoned about in the abstract. That is the single most useful +habit to carry into the build. + +**Punch list (§XXVI.6) stands as written, with item 9 now closed and one decision outstanding: +the version number (§XXVI.3).** No code is authorized.