FABRIC-3.5.md §XXVII: item 18 settled -- the empty floor is unreachable, build nothing
Tested §XVI.7's premise against the code rather than designing to it, and
the premise is false. An empty Stadium floor requires Hera to be gone,
and every path by which she can cease already terminates the machine.
She cannot starve: she is pinned via session_set_pinned(), and stadium.c
refuses pinned patrons at :453 and skips them at :559. She cannot be
killed: mama_word_kill()'s own doc says Hera cannot be killed, and
capsule_vm_kill_all_nonmama() spares her by construction. BYE reboots.
Scuttle and panic both halt. There is no route to a live kernel over an
empty floor.
So the ruling is to build nothing, and §XVI.7's proposed shape is
withdrawn. An empty-floor halt would be defensive code for a state that
cannot occur, which CLAUDE.md names directly as a thing not to add.
Notes that the pinning result generalises -- no Tripod leg can die a
compudynamic death, since all three are pinned by the same
is_fleet_foundation line, which puts §XV.2's compudynamic death exactly
where it was always aimed: the unpinned population.
Records that sk_hal_panic() already executes while(1){arch_halt();},
character for character the idiom §XXIV.2 specified for the suicide word.
The two converge on one terminal state by different triggers: a scuttle
is a panic Hera chose.
Closes by stating the three invariants the ruling depends on, since a
future change could break them silently -- Hera stays pinned, KILL keeps
refusing her, and involuntary death always ends at a permanent halt. The
first is edited by this very reshuffle when Hermes leaves the
is_fleet_foundation triple and Hestia enters it.
Design phase complete. Every question this document opened is ruled.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VkM1zHGvBerLF6aqkHPweP
This commit is contained in:
+98
-3
@@ -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.
|
||||
|
||||
Reference in New Issue
Block a user