Add the four ledger counters (held/pulled/returned/consumed) -- FABRIC-3.6.md task 2.4

FABRIC-3.5.md SXL.4's ledger: held == pulled - returned - consumed,
epsilon zero. Added sk_hermes_ledger() (an accessor, not a mutator)
plus four static counters in kernel_hermes.c.

Each counter has exactly one increment/decrement site: held/pulled
both move at sk_hermes_alloc()'s single success path, after every
refusal branch has already returned; held/returned both move at
sk_hermes_release()'s single success path. consumed is declared and
always reads 0 -- its one increment site doesn't exist yet, and won't
until task 2.5 gives decay something to record.

sk_hermes_release() now reads the Stadium cell's live header.heat
immediately before calling stadium_evict(), rather than assuming the
original pulled amount -- stadium_evict() zeroes the header as part of
freeing the cell and its own return value is a success code, not the
credited amount, so this is the only point the true remaining heat is
available. Today this always equals the original Q.SLOT pull; once
task 2.5's decay exists, this is what keeps returned correct without
touching this function again.

Self-test (kernel_main.c) extended: snapshots the ledger before
running so it checks its own deltas, verifies held/pulled grow by
exactly got_n * Q_SLOT on allocation with returned/consumed untouched,
then verifies held returns to its starting value and returned grows by
the same amount on release, and checks the audit invariant itself as a
bonus (task 2.6 formalizes this properly).

Three-arch boot clean: amd64/aarch64/riscv64 all reach [zuse@Hera] ok>,
zero UNKNOWN WORD, dict_hash unmoved. All three print PASS with
identical final ledger: held=0 pulled=65536 returned=65536 consumed=0.
No compiler warnings.

Authorized by Captain Bob ("keep going with rhe 6.5 document").

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
2026-09-20 05:59:09 -04:00
co-authored by Claude Sonnet 5
parent 2c1dc1753a
commit 493d410028
11 changed files with 27655 additions and 5 deletions
+29 -1
View File
@@ -609,8 +609,36 @@ Hestia; headless policy intact.
real and load-bearing (`stadium.c`'s own comment: "has been real and live on every boot real and load-bearing (`stadium.c`'s own comment: "has been real and live on every boot
for weeks"), not something this task introduced. No compiler warnings on either edited for weeks"), not something this task introduced. No compiler warnings on either edited
file. file.
- [ ] **2.4** — The four counters: `held`, `pulled`, `returned`, `consumed` (§XL.4). *Check:* - [x] **2.4** — The four counters: `held`, `pulled`, `returned`, `consumed` (§XL.4). *Check:*
each increments at exactly one site. each increments at exactly one site.
2026-09-20 · `logs/20260920-055432/amd64/`, `logs/20260920-055549/aarch64/`,
`logs/20260920-055723/riscv64/` — all three reach `[zuse@Hera] ok>`, zero `UNKNOWN WORD`,
`dict_hash` triple unmoved. All three print `PASS` with **identical final ledger**:
`held=0 pulled=65536 returned=65536 consumed=0` — satisfying
`held == pulled − returned − consumed` (`0 == 65536 − 65536 − 0`) exactly.
Added `sk_hermes_ledger(uint64_t*, uint64_t*, uint64_t*, uint64_t*)` (an accessor, not a
mutator) plus four static counters in `src/starkernel/vm/kernel_hermes.c`. Each has exactly
one increment/decrement site: `held`/`pulled` both move at `sk_hermes_alloc()`'s single
success path (after every refusal branch has already returned); `held`/`returned` both
move at `sk_hermes_release()`'s single success path. `consumed` is declared and always
reads 0 — **its one increment site doesn't exist yet**, and won't until task 2.5 gives
decay something to record.
`sk_hermes_release()` reads the Stadium cell's **live** `header.heat` immediately before
calling `stadium_evict()`, rather than assuming the original pulled amount — `stadium_evict()`
zeroes the header as part of freeing the cell and its own return value is a success code,
not the credited amount, so this is the only point the true remaining heat is available.
Today (no decay yet) this always equals the original `Q.SLOT` pull; once task 2.5 exists,
this is what keeps `returned` correct without touching this function again.
Self-test (kernel_main.c) extended again: snapshots the ledger before running (so it
checks its own deltas, not an assumption that it's the only caller ever), verifies
`held`/`pulled` grow by exactly `got_n × Q_SLOT` on allocation with `returned`/`consumed`
untouched, then verifies `held` returns to its starting value and `returned` grows by the
same amount on release, with `consumed` still untouched, and checks the audit invariant
itself as a bonus (task 2.6 formalizes this properly; checking it here too cost nothing
since the ledger was already in hand). No compiler warnings on either edited file.
- [ ] **2.5** — Decay: apply, and **record the delta into `consumed`** (§XXXVII.3). *Check:* - [ ] **2.5** — Decay: apply, and **record the delta into `consumed`** (§XXXVII.3). *Check:*
`consumed` grows by exactly `heat_before − heat_after`. `consumed` grows by exactly `heat_before − heat_after`.
- [ ] **2.6** — Self-audit: `held == pulled − returned − consumed`, **epsilon zero**. *Check:* - [ ] **2.6** — Self-audit: `held == pulled − returned − consumed`, **epsilon zero**. *Check:*
+1 -1
View File
@@ -1,5 +1,5 @@
# Capsule Block Manifest — Auto-generated # Capsule Block Manifest — Auto-generated
<!-- Generated by mkcapsule --manifest 2026-09-20T08:17:49Z --> <!-- Generated by mkcapsule --manifest 2026-09-20T09:57:21Z -->
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. --> <!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
<!-- Hand-written justifications and immutability notes live --> <!-- Hand-written justifications and immutability notes live -->
<!-- in MANIFEST.md alongside this auto-generated index. --> <!-- in MANIFEST.md alongside this auto-generated index. -->
+28
View File
@@ -194,6 +194,34 @@ int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg);
*/ */
int sk_hermes_release(SkHermesMessage *msg); int sk_hermes_release(SkHermesMessage *msg);
/*
* sk_hermes_ledger - Task 2.4 (item 28), the four counters FABRIC-3.5.md
* SXXXVII.3/SXL.4 name: held, pulled, returned, consumed. Each is touched
* at exactly one call site:
*
* held += pulled amount -- sk_hermes_alloc(), on success only
* held -= returned amount -- sk_hermes_release(), on success only
* pulled += pulled amount -- sk_hermes_alloc(), same site as held's
* returned += returned amount -- sk_hermes_release(), same site as held's
* consumed += decay delta -- task 2.5, not yet wired; reads 0 until
* then
*
* The audit invariant this ledger exists to make checkable (task 2.6,
* epsilon zero): held == pulled - returned - consumed. All four are
* exact integers (SXXXVII.3: "Nothing here is a measurement. There is no
* noise to tolerate.") -- this accessor is how task 2.6's audit, task
* 2.7's Stage B proof, and task 2.8's scan cross-check all read the same
* four numbers, rather than each keeping its own copy.
*
* @param held Set to the current live total (may be NULL).
* @param pulled Set to the cumulative total ever pulled (may be NULL).
* @param returned Set to the cumulative total ever returned (may be
* NULL).
* @param consumed Set to the cumulative total ever consumed by decay
* (may be NULL) -- always 0 until task 2.5.
*/
void sk_hermes_ledger(uint64_t *held, uint64_t *pulled, uint64_t *returned, uint64_t *consumed);
#endif /* __STARKERNEL__ */ #endif /* __STARKERNEL__ */
#endif /* STARKERNEL_VM_KERNEL_HERMES_H */ #endif /* STARKERNEL_VM_KERNEL_HERMES_H */
File diff suppressed because it is too large Load Diff
File diff suppressed because it is too large Load Diff
File diff suppressed because it is too large Load Diff
+36
View File
@@ -855,6 +855,14 @@ static void kernel_main_deep(BootInfo *boot_info) {
SkHermesMessage *msg; SkHermesMessage *msg;
int ok = 1; int ok = 1;
size_t i; size_t i;
uint64_t held0, pulled0, returned0, consumed0;
uint64_t held1, pulled1, returned1, consumed1;
uint64_t held2, pulled2, returned2, consumed2;
/* Task 2.4: snapshot the ledger before touching it, so this
* test checks its own deltas rather than assuming it is the
* only thing that has ever called these functions. */
sk_hermes_ledger(&held0, &pulled0, &returned0, &consumed0);
while (got_n < SK_HERMES_MSG_MAX && sk_hermes_alloc(alloc_test_id, &msg) == 0) { while (got_n < SK_HERMES_MSG_MAX && sk_hermes_alloc(alloc_test_id, &msg) == 0) {
msgs[got_n] = msg; msgs[got_n] = msg;
@@ -869,6 +877,15 @@ static void kernel_main_deep(BootInfo *boot_info) {
if (stadium_reservoir_peek(alloc_test_id) != reservoir_after_alloc) ok = 0; if (stadium_reservoir_peek(alloc_test_id) != reservoir_after_alloc) ok = 0;
if (reservoir_after_alloc != reservoir0 - got_n * SK_HERMES_Q_SLOT) ok = 0; if (reservoir_after_alloc != reservoir0 - got_n * SK_HERMES_Q_SLOT) ok = 0;
/* Task 2.4: held/pulled must both have grown by exactly
* got_n * Q_SLOT; returned/consumed must be untouched by
* allocation alone. */
sk_hermes_ledger(&held1, &pulled1, &returned1, &consumed1);
if (held1 - held0 != got_n * SK_HERMES_Q_SLOT) ok = 0;
if (pulled1 - pulled0 != got_n * SK_HERMES_Q_SLOT) ok = 0;
if (returned1 != returned0) ok = 0;
if (consumed1 != consumed0) ok = 0;
/* Task 2.3: release every allocated message via the Stadium /* Task 2.3: release every allocated message via the Stadium
* eviction path and confirm the reservoir is restored * eviction path and confirm the reservoir is restored
* exactly -- "reservoir restored exactly for an undecayed * exactly -- "reservoir restored exactly for an undecayed
@@ -882,6 +899,21 @@ static void kernel_main_deep(BootInfo *boot_info) {
uint64_t reservoir_final = stadium_reservoir_peek(alloc_test_id); uint64_t reservoir_final = stadium_reservoir_peek(alloc_test_id);
if (reservoir_final != reservoir0) ok = 0; if (reservoir_final != reservoir0) ok = 0;
/* Task 2.4: held must fall back to held0 (every message this
* test allocated is now released); returned must have grown
* by exactly what held grew by; consumed still untouched
* (nothing decayed). This is the ledger side of "reservoir
* restored exactly." */
sk_hermes_ledger(&held2, &pulled2, &returned2, &consumed2);
if (held2 != held0) ok = 0;
if (pulled2 != pulled1) ok = 0; /* release never touches pulled */
if (returned2 - returned0 != got_n * SK_HERMES_Q_SLOT) ok = 0;
if (consumed2 != consumed0) ok = 0;
/* The audit invariant itself (task 2.6 formalizes this as its
* own check; verified here too since the ledger is already in
* hand): held == pulled - returned - consumed, at rest. */
if (held2 != pulled2 - returned2 - consumed2) ok = 0;
console_println(ok ? "PASS" : "FAIL"); console_println(ok ? "PASS" : "FAIL");
print_uint(" reservoir0=", reservoir0); print_uint(" reservoir0=", reservoir0);
print_uint(" Q_SLOT=", SK_HERMES_Q_SLOT); print_uint(" Q_SLOT=", SK_HERMES_Q_SLOT);
@@ -889,6 +921,10 @@ static void kernel_main_deep(BootInfo *boot_info) {
print_uint(" got_n=", got_n); print_uint(" got_n=", got_n);
print_uint(" reservoir_after_alloc=", reservoir_after_alloc); print_uint(" reservoir_after_alloc=", reservoir_after_alloc);
print_uint(" reservoir_final=", reservoir_final); print_uint(" reservoir_final=", reservoir_final);
print_uint(" held(final)=", held2);
print_uint(" pulled(final)=", pulled2);
print_uint(" returned(final)=", returned2);
print_uint(" consumed(final)=", consumed2);
} }
} }
+51 -3
View File
@@ -22,8 +22,9 @@
*/ */
/** /**
* kernel_hermes.c - Kernel-resident Hermes: the heat-coupled allocator * kernel_hermes.c - Kernel-resident Hermes: the heat-coupled allocator,
* and its release path (FABRIC-3.6.md tasks 2.2/2.3, item 28). * its release path, and the four-counter ledger (FABRIC-3.6.md tasks
* 2.2/2.3/2.4, item 28).
* *
* CORRECTION (task 2.3, found while starting it): task 2.2's first cut of * CORRECTION (task 2.3, found while starting it): task 2.2's first cut of
* sk_hermes_alloc() pulled reservoir heat but never admitted a real * sk_hermes_alloc() pulled reservoir heat but never admitted a real
@@ -49,6 +50,21 @@
static SkHermesMessage sk_hermes_msgs[SK_HERMES_MSG_MAX]; static SkHermesMessage sk_hermes_msgs[SK_HERMES_MSG_MAX];
/* Task 2.4 (item 28), FABRIC-3.5.md SXXXVII.3/SXL.4's four counters.
* `consumed` is declared now but touched nowhere yet -- task 2.5 adds
* its one increment site when decay exists to record a delta from. */
static uint64_t sk_hermes_held = 0;
static uint64_t sk_hermes_pulled = 0;
static uint64_t sk_hermes_returned = 0;
static uint64_t sk_hermes_consumed = 0;
void sk_hermes_ledger(uint64_t *held, uint64_t *pulled, uint64_t *returned, uint64_t *consumed) {
if (held) *held = sk_hermes_held;
if (pulled) *pulled = sk_hermes_pulled;
if (returned) *returned = sk_hermes_returned;
if (consumed) *consumed = sk_hermes_consumed;
}
static int sk_hermes_find_free_slot(void) { static int sk_hermes_find_free_slot(void) {
int i; int i;
for (i = 0; i < SK_HERMES_MSG_MAX; i++) { for (i = 0; i < SK_HERMES_MSG_MAX; i++) {
@@ -113,21 +129,53 @@ int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg) {
sk_hermes_msgs[slot].in_use = 1; sk_hermes_msgs[slot].in_use = 1;
sk_hermes_msgs[slot].stadium_cell = (int32_t)cell; sk_hermes_msgs[slot].stadium_cell = (int32_t)cell;
*out_msg = &sk_hermes_msgs[slot]; *out_msg = &sk_hermes_msgs[slot];
/* Task 2.4: the one site where held/pulled increment -- only reached
* once every refusal path above has already returned. */
sk_hermes_held += pulled;
sk_hermes_pulled += pulled;
return 0; return 0;
} }
int sk_hermes_release(SkHermesMessage *msg) { int sk_hermes_release(SkHermesMessage *msg) {
int rc; int rc;
uint64_t remaining;
if (!msg || !msg->in_use) return -1; if (!msg || !msg->in_use) return -1;
if (msg->stadium_cell < 0) {
memset(msg, 0, sizeof(*msg));
return -1;
}
/* Read the patron's current heat BEFORE eviction -- stadium_evict()
* zeroes the header as part of returning the cell to the free list,
* and its own return value is a success code, not the amount
* credited. Today (before task 2.5's decay exists) this always
* equals exactly what was pulled at allocation; once decay exists,
* this is the message's true remaining heat, which is what actually
* flows back to the reservoir -- reading it here rather than
* assuming the original pulled amount is what keeps this correct
* without changes once task 2.5 lands. */
remaining = stadium_cells()[msg->stadium_cell].header.heat;
/* stadium_evict() returns the departing patron's remaining heat to /* stadium_evict() returns the departing patron's remaining heat to
* its owner's reservoir itself (stadium.c: "the departing patron's * its owner's reservoir itself (stadium.c: "the departing patron's
* remaining heat must flow back to its owner's reservoir before the * remaining heat must flow back to its owner's reservoir before the
* cell returns to the free list") -- release does not touch the * cell returns to the free list") -- release does not touch the
* reservoir directly, the eviction path does it, matching * reservoir directly, the eviction path does it, matching
* MSG-FREE-NODE's own shape ("DUP 5 CELLS + @ STADIUM-EVICT DROP"). */ * MSG-FREE-NODE's own shape ("DUP 5 CELLS + @ STADIUM-EVICT DROP"). */
rc = (msg->stadium_cell >= 0) ? stadium_evict((size_t)msg->stadium_cell) : -1; rc = stadium_evict((size_t)msg->stadium_cell);
/* Task 2.4: the one site where held/returned change on release. Only
* on successful eviction -- a refused eviction leaves the patron
* (and its heat) exactly where it was, so the ledger must not move
* either. */
if (rc == 0) {
sk_hermes_held -= remaining;
sk_hermes_returned += remaining;
}
memset(msg, 0, sizeof(*msg)); memset(msg, 0, sizeof(*msg));
return rc; return rc;