Stage B proof: add per-VM consumed term to stadium_conserved -- FABRIC-3.6.md task 2.7

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

FABRIC-3.6.md

@@ -683,10 +683,35 @@ Hestia; headless policy intact.
       Limit, stated: the corruption proof exercises the predicate, not the wiring of the live
       audit's failure branch (that branch never executed). Task 2.8's scan cross-check is the
       independent check on the counters themselves.
-- [ ] **2.7** — **Stage B proof** (§XXXIV.3 as corrected by §XXXIX.4): alloc/free cycle
+- [x] **2.7** — **Stage B proof** (§XXXIV.3 as corrected by §XXXIX.4): alloc/free cycle
       verifying **(a)** the ledger and **(b)** `stadium_conserved()` before and after.
       *Check:* both true, all three arches. **`fleet_conserved` is not evidence here** — it
       cannot see Stadium heat (§XXXIX.1).
+      2026-09-20 · `logs/20260920-212209/amd64/`, `logs/20260920-212522/aarch64/`,
+      `logs/20260920-212845/riscv64/` — all print `Stage B (ledger + stadium_conserved): PASS`,
+      `audit_failures=0`, `vm_consumed=693`; zero `UNKNOWN WORD`; `dict_hash` triple unmoved and
+      identical across ISAs; reach `[zuse@Hera] ok>`.
+
+      **Prerequisite built here, as §XL.4 directs:** `stadium_conserved()` gains its `consumed`
+      term. New per-VM `consumed` field in `StadiumVMQuota` (zeroed at both quota-creation
+      sites), `stadium_consumed_record()`/`stadium_consumed_peek()`, and
+      `stadium_conserved()` now checks `resident + reservoir + consumed == Q48_ONE`, epsilon
+      zero. `SkHermesMessage` gained an `owner` VMUuid so decay charges the funding VM;
+      `sk_hermes_decay()` records into it. Other VMs are unaffected (consumed stays 0).
+
+      Stage B checks `stadium_conserved()` at four points — before, mid-hold, after decay,
+      after release — plus the ledger audit, and requires the old **two-term form to FAIL after
+      decay** while the four-term form holds (non-vacuity: the consumed term is load-bearing).
+      `fleet_conserved` is not consulted.
+
+      **First attempt FAILED on all three ISAs** (`logs/20260920-211204/`, `-211517/`,
+      `-211840/`, kept as audit artifacts). Cause was a bug in the test, not the code: it
+      expected 32 allocations, but the preceding decay cycle had consumed 352 from that VM's
+      reservoir so only 31 fit. Fixed by deriving the expected count from the current reservoir.
+      Vm_consumed=693 is 352 (32×11, first cycle) + 341 (31×11, Stage B).
+
+      **Phase 2 gate: passed** (2.7 holds on all three arches). Remaining Phase 2 work is 2.8
+      (diagnostic scan cross-check).
 - [ ] **2.8** — Scan-based cross-check of the counters, diagnostics only, off the hot path
       (§XXXVII.4). *Check:* scan agrees with counters.
 

include/starkernel/vm/kernel_hermes.h

@@ -132,6 +132,7 @@ typedef struct {
     uint32_t channel;
     uint32_t orig_type;
     int      in_use;
+    VMUuid   owner; /* VM whose reservoir funded this message (task 2.7) */
 } SkHermesMessage;
 
 /*

include/starkernel/vm/stadium.h

@@ -375,12 +375,13 @@ uint64_t stadium_resident_sum(VMUuid vm_id);
  *
  *   stadium_resident_sum(vm_id) + stadium_reservoir_peek(vm_id) == Q48_ONE
  *
- * FABRIC-3.5.md §XL.4 rules that the full invariant also adds a `consumed`
- * term once kernel-Hermes exists and ledgers what its allocator consumes
- * (Phase 2) -- until then nothing draws on a VM's Stadium quota, so the
- * two-term form above is exact, not an approximation of the eventual one.
- * A future caller adding the `consumed` term does so here, not by working
- * around this function.
+ * FABRIC-3.5.md §XL.4: the full invariant also has a per-VM `consumed`
+ * term (task 2.7), recorded by kernel-Hermes when its messages decay:
+ *
+ *   stadium_resident_sum + stadium_reservoir_peek + stadium_consumed_peek
+ *     == Q48_ONE
+ *
+ * The two-term form above is the special case consumed == 0.
  *
  * Returns 0 (not conserved) for an unknown vm_id, same convention as
  * stadium_reservoir_peek()/stadium_resident_sum() returning 0 for one.
@@ -390,6 +391,17 @@ uint64_t stadium_resident_sum(VMUuid vm_id);
  */
 int stadium_conserved(VMUuid vm_id);
 
+/*
+ * stadium_consumed_record - Add amount to vm_id's per-VM consumed total
+ * (heat destroyed by decay; FABRIC-3.5.md §XL.4). No-op if vm_id has no
+ * quota. Caller (kernel-Hermes decay) must have removed the same amount
+ * from a resident patron's heat.
+ */
+void stadium_consumed_record(VMUuid vm_id, uint64_t amount);
+
+/* stadium_consumed_peek - vm_id's consumed total, 0 for an unknown vm_id. */
+uint64_t stadium_consumed_peek(VMUuid vm_id);
+
 /*
  * stadium_evict - Reap the patron header at cell_index (FABRIC-0.md §17.2:
  * "reap means leaves the floor, not destroyed"). Dispatches its behaviour

src/starkernel/kernel_main.c

@@ -951,6 +951,43 @@ static void kernel_main_deep(BootInfo *boot_info) {
             if (held4 != pulled4 - returned4 - consumed4) ok = 0;
             if (stadium_reservoir_peek(alloc_test_id) != reservoir0 - decay_expected) ok = 0;
 
+            /* Task 2.7, Stage B proof (SXXXIV.3 as corrected by SXXXIX.4):
+             * a fresh alloc/decay/free cycle on this VM, checking BOTH the
+             * ledger and stadium_conserved() at every stage. fleet_conserved
+             * is deliberately not consulted (cannot see Stadium heat). The
+             * four-term form must hold before, mid-hold, after decay, and
+             * after release; and after decay the old two-term form must
+             * FAIL while the four-term one holds -- proving the consumed
+             * term is load-bearing, not vacuous. */
+            {
+                uint64_t nb = 0, h, p_, r, c;
+                /* Derived from the CURRENT reservoir: the earlier decay
+                 * cycle consumed heat, so fewer than expected_n fit now. */
+                uint64_t expected_b = stadium_reservoir_peek(alloc_test_id) / SK_HERMES_Q_SLOT;
+                int sb = 1;
+                if (!stadium_conserved(alloc_test_id)) sb = 0;               /* before */
+                while (nb < SK_HERMES_MSG_MAX && sk_hermes_alloc(alloc_test_id, &msg) == 0) {
+                    msgs[nb++] = msg;
+                }
+                if (nb != expected_b || nb == 0) sb = 0;
+                if (!stadium_conserved(alloc_test_id)) sb = 0;               /* mid-hold */
+                for (i = 0; i < nb; i++) if (sk_hermes_decay(msgs[i]) != 0) sb = 0;
+                if (!stadium_conserved(alloc_test_id)) sb = 0;               /* after decay */
+                if (stadium_consumed_peek(alloc_test_id) == 0) sb = 0;
+                if (stadium_resident_sum(alloc_test_id) + stadium_reservoir_peek(alloc_test_id)
+                        == (uint64_t)Q48_ONE) sb = 0;                        /* two-term must fail */
+                sk_hermes_ledger(&h, &p_, &r, &c);
+                if (!sk_hermes_audit_values(h, p_, r, c)) sb = 0;
+                for (i = 0; i < nb; i++) if (sk_hermes_release(msgs[i]) != 0) sb = 0;
+                if (!stadium_conserved(alloc_test_id)) sb = 0;               /* after release */
+                sk_hermes_ledger(&h, &p_, &r, &c);
+                if (h != held0 || !sk_hermes_audit_values(h, p_, r, c)) sb = 0;
+                console_puts("Stage B (ledger + stadium_conserved): ");
+                console_println(sb ? "PASS" : "FAIL");
+                print_uint("  vm_consumed=", stadium_consumed_peek(alloc_test_id));
+                if (!sb) ok = 0;
+            }
+
             /* Task 2.6: the live audit never fired across both cycles,
              * and a ONE-unit corruption of each counter in turn (on a
              * copy -- live state untouched) is caught by the pure

src/starkernel/vm/kernel_hermes.c

@@ -151,6 +151,7 @@ int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg) {
     memset(&sk_hermes_msgs[slot], 0, sizeof(SkHermesMessage));
     sk_hermes_msgs[slot].in_use      = 1;
     sk_hermes_msgs[slot].stadium_cell = (int32_t)cell;
+    sk_hermes_msgs[slot].owner        = vm_id;
     *out_msg = &sk_hermes_msgs[slot];
 
     /* Task 2.4: the one site where held/pulled increment -- only reached
@@ -222,6 +223,7 @@ int sk_hermes_decay(SkHermesMessage *msg) {
      * pays for it). SXXXVII.3: decay's delta is exact and in hand here. */
     sk_hermes_consumed += before - after;
     sk_hermes_held     -= before - after;
+    stadium_consumed_record(msg->owner, before - after);
     sk_hermes_audit();
 
     return 0;

src/starkernel/vm/stadium.c

@@ -107,6 +107,10 @@ typedef struct {
                           * Invariant: Σ(resident patron heat) + reservoir ==
                           * Q48_ONE, checked the same way vm_physics_conserved()
                           * checks the fleet sum. */
+    uint64_t consumed;  /* FABRIC-3.5.md §XL.4 -- Q48.16, heat this VM's messages
+                          * have decayed away (recorded by kernel-Hermes,
+                          * FABRIC-3.6.md task 2.7). Full invariant:
+                          * Σ(resident) + reservoir + consumed == Q48_ONE. */
 } StadiumVMQuota;
 
 /* kmalloc'd at stadium_boot_init() to stadium_max_vm_count_val entries,
@@ -275,6 +279,7 @@ int stadium_boot_init(void) {
             quotas[i].free_count    = 0;
             quotas[i].resident_head = STADIUM_CELL_NONE;
             quotas[i].reservoir     = 0;
+            quotas[i].consumed      = 0;
         }
     }
     quotas[0].vm_id     = vm_uuid_hera();
@@ -642,6 +647,7 @@ int stadium_grant_quota(VMUuid new_vm_id, VMUuid from_vm_id) {
     stadium_quotas[new_slot].free_count    = half;
     stadium_quotas[new_slot].resident_head = STADIUM_CELL_NONE;
     stadium_quotas[new_slot].reservoir     = Q48_ONE;
+    stadium_quotas[new_slot].consumed      = 0;
 
     return 0;
 }
@@ -764,8 +770,23 @@ uint64_t stadium_resident_sum(VMUuid vm_id) {
     return sum;
 }
 
+void stadium_consumed_record(VMUuid vm_id, uint64_t amount) {
+    int slot = quota_slot_for_vm(vm_id);
+
+    if (slot < 0) return;
+    stadium_quotas[slot].consumed += amount;
+}
+
+uint64_t stadium_consumed_peek(VMUuid vm_id) {
+    int slot = quota_slot_for_vm(vm_id);
+
+    if (slot < 0) return 0;
+    return stadium_quotas[slot].consumed;
+}
+
 int stadium_conserved(VMUuid vm_id) {
-    return (stadium_resident_sum(vm_id) + stadium_reservoir_peek(vm_id)) == (uint64_t)Q48_ONE;
+    return (stadium_resident_sum(vm_id) + stadium_reservoir_peek(vm_id) +
+            stadium_consumed_peek(vm_id)) == (uint64_t)Q48_ONE;
 }
 
 /*