FABRIC-3.5.md §XXXIX: item 39 settled -- the accountings are not coupled, and §XXXIV.6 watched the wrong one
Traced both directions. capsule_vm_physics.c has zero references to stadium and does not include its header; it has zero references to reservoir. stadium.c's single vm_physics mention is a comment. vm_physics_fleet_heat_sum() sums execution_heat_q48, whose only writers are initialise, transfer between two VMs, and redistribute on death. Message allocation cannot move it. They are not even the same shape of invariant. StadiumVMQuota.reservoir's own comment states Stadium conservation is per-VM -- resident patron heat plus that VM's reservoir equals Q48_ONE each -- while vm-physics K is fleet-wide across all VMs. Two scopes, two disjoint data sets, sharing only the Q48.16 format, the constant, and the word heat. That shared vocabulary is what made them look like one system. Only one has a checker. vm_physics_conserved() is the sole *_conserved() function in the kernel; the Stadium side has a documented invariant, a human-readable diagnostic print, and MSG-K covering just the messaging slice. So §XXXVIII's leak is invisible to every automated check -- not because checks disagree, but because nothing is looking. Corrects §XXXIV.6 in the dangerous direction: it made fleet_conserved the tripwire for Stage B, but a kernel-Hermes allocator leaking every reservation would leave it reporting a serene 1. That is §XXXV.0's signature exactly, built into the plan, and item 39 existed to catch it before it mattered. Stage B instead verifies kernel-Hermes's own ledger and the Stadium per-VM invariant, and should add the missing stadium_conserved() as its first act. Two earlier rulings need consequent care. §XV.4's K must be qualified, since the heat a dying arbiter holds is Stadium heat rather than the verified fleet K -- substance stands, citation was wrong. And the self-audit is promoted from safety net to sole instrument, which argues for an independent Stadium checker rather than the arbiter policing itself alone. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VkM1zHGvBerLF6aqkHPweP
This commit is contained in:
+120
@@ -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).
|
||||
|
||||
Reference in New Issue
Block a user