diff --git a/FABRIC-3.5.md b/FABRIC-3.5.md index f000aaf8..806b9eea 100644 --- a/FABRIC-3.5.md +++ b/FABRIC-3.5.md @@ -4103,3 +4103,123 @@ The obstacle was never decay itself; it was decay being applied to the wrong fie - ⬜ **Item 40, NEW** — rule on §XXXVIII.4: separate reservation from age, or keep the forfeit and document it as a designed sink. - Items 32–35, 37 unchanged. + +--- + +## XXXIX. Item 39 SETTLED: the two accountings are not coupled — and §XXXIV.6's tripwire watches the wrong one + +§XXXVIII.3 declined to claim the message-reap leak was visible to `VM-CONSERVED?`, and filed +this to settle before §XXXIV.6's tripwire was relied on. **Settled: they are entirely separate +systems, and the tripwire as written would have stayed green through exactly the failure it was +meant to catch.** + +### XXXIX.1 — The trace: no coupling, in either direction + +| Check | Result | +|---|---| +| `capsule_vm_physics.c` references to `stadium` | **0** — and it does not include `stadium.h` (only `starforth_config.h`, for the unrelated `STADIUM_CAPACITY_TICK`) | +| `capsule_vm_physics.c` references to `reservoir` | **0** | +| `stadium.c` references to `vm_physics` | **1 — a comment**, not code | +| `stadium_words.c` references to `vm_physics` | **0** | + +**`vm_physics_fleet_heat_sum()` sums `n->physics.execution_heat_q48`** over the physics node +list. Every writer of that field is internal: initialise (`is_root ? Q48_ONE : 0`), transfer +between two VMs, redistribute on death. **Nothing reads or writes a Stadium reservoir or patron +cell.** Message allocation cannot move it. + +### XXXIX.2 — They are not even the same *shape* of invariant + +`StadiumVMQuota.reservoir`'s own doc comment (`stadium.c:105-109`): + +> "Invariant: **Σ(resident patron heat) + reservoir == `Q48_ONE`**, checked the same way +> `vm_physics_conserved()` checks the fleet sum." + +…and `stadium.h:484` confirms "**conservation is per-VM**." + +| | Scope | Quantity | Target | +|---|---|---|---| +| **Stadium** | **Per-VM** | patron-cell heat + that VM's reservoir | `Q48_ONE` **each** | +| **VM-physics ("K")** | **Fleet-wide** | Σ `execution_heat_q48` over live VMs | `Q48_ONE` **total** | + +Two invariants, two scopes, two disjoint data sets — sharing only the Q48.16 format, the +constant `Q48_ONE`, and the word "heat." **That shared vocabulary is what made them look like +one system**, and is why §XV.4 and §XXXIV.6 conflated them. + +### XXXIX.3 — Only one of them has a checker + +**`vm_physics_conserved()` is the only `*_conserved()` function in the kernel.** Confirmed by +exhaustive grep: the sole other match is `mama_word_vm_conserved()`, its FORTH wrapper. + +The Stadium side has: +- a **documented** invariant (the comment above), +- a **diagnostic print** — `stadium_words.c:328`, `"Stadium conservation: resident_sum="` — a + human-readable dump, not a boolean, +- `MSG-K` (`messaging.4th:364`), a FORTH word covering only the messaging slice, which someone + must call. + +**There is no automated, continuous verification of Stadium conservation anywhere.** Which +means §XXXVIII's leak — `Q.SLOT` destroyed per reaped message — **is invisible to every +automated check in the system.** It is not that the checks disagree; it is that nothing is +looking. + +### XXXIX.4 — CORRECTION to §XXXIV.6: the tripwire monitors a quantity the failure cannot move + +§XXXIV.6 states: *"Stage B fails — `fleet_conserved` will not hold across a bare alloc/free +cycle under the new allocator."* + +**That is wrong, and wrong in the dangerous direction.** `fleet_conserved` reports +`vm_physics_conserved()`, which sums `execution_heat_q48`. **Message allocation never touches +that field.** A kernel-Hermes allocator that leaked every reservation it took would leave +`fleet_conserved` reporting a serene `1`. + +**This is precisely §XXXV.0's signature** — a check that passes while the thing it is supposed +to guard is broken — and I built one into the plan. **Item 39 existed to catch it before it +mattered, and did.** + +**Corrected tripwire for Stage B:** + +> Stage B verifies **(a)** kernel-Hermes's own ledger (§XXXVII.3, epsilon zero) and **(b)** the +> **Stadium per-VM invariant** for the sending VM — Σ(resident patron heat) + reservoir == +> `Q48_ONE` — **before and after** the alloc/free cycle. **`fleet_conserved` is not evidence for +> this stage** and should not be cited as such. + +Since §XXXIX.3 shows no boolean Stadium checker exists, Stage B either calls `MSG-K`, or reads +`stadium_words.c:328`'s dump, or — better, and cheap — **adds the missing `stadium_conserved()` +as its first act.** That function is a five-line analogue of `vm_physics_conserved()` and the +system has wanted one since the invariant was written down. + +### XXXIX.5 — Consequences for two earlier rulings + +**§XV.4 ("nothing survives except K") needs its K qualified.** The heat a dying arbiter holds +is **Stadium** heat. The K that `FABRIC-3.md` §XVIII verified live, and that §XV.4 cited, is +**VM-physics** K. **The arbiter's heat was never in the verified quantity.** The ruling's +substance stands — a dying arbiter must return what it holds — but it must say *Stadium +conservation*, not K. + +**§XXXVI/§XXXVII's self-audit is promoted from safety net to sole instrument.** With no +continuous Stadium checker, kernel-Hermes auditing its own ledger would be **the only automated +guard on the messaging pool's conservation.** That raises the value of §XXXVII.3's zero epsilon +considerably — and argues for §XXXIX.4's `stadium_conserved()` as a second, independent check +rather than relying on the arbiter to police itself alone. + +### XXXIX.6 — A naming hazard worth fixing in the sweep + +Two conserved quantities, both Q48.16, both targeting `Q48_ONE`, both called "heat," differing +only in scope — and the FABRIC series calls one of them "K" without qualification. **Every +future reader will conflate them exactly as §XV.4 and §XXXIV.6 did.** + +**Added to item 13's documentation sweep:** wherever "K" or "conservation" appears, say which — +**fleet K** (`vm_physics`) or **quota conservation** (Stadium, per-VM). + +### XXXIX.7 — Punch list + +- ✅ **Item 39 — SETTLED** (§XXXIX): **not coupled.** Disjoint data, disjoint code, different + invariant scopes. +- ✅ **§XXXIV.6 corrected** (§XXXIX.4): Stage B verifies the ledger and Stadium per-VM + conservation; `fleet_conserved` is not evidence for it. +- ⬜ **Item 41, NEW** — add `stadium_conserved()`, the missing boolean analogue of + `vm_physics_conserved()`. Cheap, and the invariant has been documented-but-unverified since it + was written. +- ⬜ **Item 42, NEW** — qualify "K"/"conservation" throughout the docs (§XXXIX.6). Folds into + item 13. +- ⬜ **Item 40** unchanged — separate reservation from age (§XXXVIII.4).