Add sk_hermes_decay(), ledgering decay into consumed -- FABRIC-3.6.md task 2.5

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
2026-09-20 18:48:46 -04:00
co-authored by Claude Sonnet 5
parent 493d410028
commit d11eb2e5db
7 changed files with 27737 additions and 4 deletions
+25 -1
View File
@@ -639,8 +639,32 @@ Hestia; headless policy intact.
same amount on release, with `consumed` still untouched, and checks the audit invariant 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 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. 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:* - [x] **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`.
2026-09-20 · `logs/20260920-182345/amd64/`, `logs/20260920-183413/aarch64/`,
`logs/20260920-184152/riscv64/` — all three reach `[zuse@Hera] ok>`, zero `UNKNOWN WORD`,
`dict_hash` triple unmoved (`c95ef2d92fa0781f` / `fbde9fe105fd3b3d` / `a43d2e104ae7e451`,
identical across ISAs). All three print `PASS` with **identical** `decay_consumed=352`.
Added `sk_hermes_decay(SkHermesMessage*)` and `SK_HERMES_Q_DECAY` (65208, identical to
`messaging.4th`'s `Q-DECAY`; §XL.4 preserves the economy exactly). It sets the message's
Stadium-cell heat to `q48_mul(heat, Q_DECAY)` and, at that one site, does
`consumed += before − after` and `held −= before − after`, so
`held == pulled − returned − consumed` stays exact. `consumed` now has its one increment
site.
Self-test: a second alloc-to-exhaustion cycle decays each message once. It checks each
cell's new heat against an independently computed `q48_mul`, checks `consumed` grew by
exactly the independently summed `before − after` (32 × (2048 − 2037) = 352), checks the
audit identity mid-hold, and checks that release leaves the reservoir at exactly
`reservoir0 − 352` (decayed heat does not return, §XL.4). A vacuity guard fails the test
if decay consumed nothing. The task 2.3 undecayed exact-restoration check is kept as the
first cycle.
Process notes: an accidental `pkill -f` killed the shell once (no effect on results);
`disk/artemis.img` and `disk/thumbdrives/zuse-thumb-ident.img` were restored via
`git checkout --` before each ISA per the task 0.0 finding. That discarded a pre-existing
uncommitted modification to `disk/artemis.img` that was present at session start.
- [ ] **2.6** — Self-audit: `held == pulled − returned − consumed`, **epsilon zero**. *Check:* - [ ] **2.6** — Self-audit: `held == pulled − returned − consumed`, **epsilon zero**. *Check:*
holds across the cycle; **deliberately corrupt a counter → audit fires on the first unit**. holds across the cycle; **deliberately corrupt a counter → audit fires on the first unit**.
- [ ] **2.7** — **Stage B proof** (§XXXIV.3 as corrected by §XXXIX.4): alloc/free cycle - [ ] **2.7** — **Stage B proof** (§XXXIV.3 as corrected by §XXXIX.4): alloc/free cycle
+25 -3
View File
@@ -203,8 +203,8 @@ int sk_hermes_release(SkHermesMessage *msg);
* held -= returned amount -- sk_hermes_release(), on success only * held -= returned amount -- sk_hermes_release(), on success only
* pulled += pulled amount -- sk_hermes_alloc(), same site as held's * pulled += pulled amount -- sk_hermes_alloc(), same site as held's
* returned += returned amount -- sk_hermes_release(), 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 * held -= decay delta -- sk_hermes_decay(), same site as consumed's
* then * consumed += decay delta -- sk_hermes_decay() (task 2.5)
* *
* The audit invariant this ledger exists to make checkable (task 2.6, * The audit invariant this ledger exists to make checkable (task 2.6,
* epsilon zero): held == pulled - returned - consumed. All four are * epsilon zero): held == pulled - returned - consumed. All four are
@@ -218,10 +218,32 @@ int sk_hermes_release(SkHermesMessage *msg);
* @param returned Set to the cumulative total ever returned (may be * @param returned Set to the cumulative total ever returned (may be
* NULL). * NULL).
* @param consumed Set to the cumulative total ever consumed by decay * @param consumed Set to the cumulative total ever consumed by decay
* (may be NULL) -- always 0 until task 2.5. * (may be NULL).
*/ */
void sk_hermes_ledger(uint64_t *held, uint64_t *pulled, uint64_t *returned, uint64_t *consumed); void sk_hermes_ledger(uint64_t *held, uint64_t *pulled, uint64_t *returned, uint64_t *consumed);
/*
* SK_HERMES_Q_DECAY - per-application decay factor, Q48.16. Identical to
* messaging.4th's `65208 CONSTANT Q-DECAY` (65208/65536 ~= 0.99499):
* FABRIC-3.5.md SXL.4 rules that the consumption economy is preserved
* exactly, not re-tuned.
*/
#define SK_HERMES_Q_DECAY ((uint64_t)65208)
/*
* sk_hermes_decay - Apply one decay step to a live message (task 2.5,
* item 28), mirroring MSG-COOL-ONE (`MSG-HEAT@ Q-DECAY Q.* MSG-HEAT!`):
* the message's Stadium-cell heat becomes q48_mul(heat, Q_DECAY). Unlike
* MSG-COOL-ONE, the destroyed difference is RECORDED (SXXXVII.3): the
* delta heat_before - heat_after is added to `consumed` and subtracted
* from `held`, so held == pulled - returned - consumed stays exact.
*
* @param msg A live slot from sk_hermes_alloc(). Refused (returns -1, no
* effect) if NULL, not in use, or holding no Stadium cell.
* @return 0 on success, -1 if refused.
*/
int sk_hermes_decay(SkHermesMessage *msg);
#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
+38
View File
@@ -914,7 +914,45 @@ static void kernel_main_deep(BootInfo *boot_info) {
* hand): held == pulled - returned - consumed, at rest. */ * hand): held == pulled - returned - consumed, at rest. */
if (held2 != pulled2 - returned2 - consumed2) ok = 0; if (held2 != pulled2 - returned2 - consumed2) ok = 0;
/* Task 2.5: second cycle, with decay. Allocate to exhaustion
* again, decay every message once, and check `consumed`
* grew by EXACTLY the sum of (heat_before - heat_after)
* measured independently from the Stadium cells, each
* message's new heat is q48_mul(before, Q_DECAY), and the
* audit invariant still holds mid-hold. Then release and
* confirm the reservoir returns reservoir0 minus exactly what
* was consumed (decayed heat does not return, SXL.4). */
uint64_t decay_expected = 0;
uint64_t held3, pulled3, returned3, consumed3;
uint64_t held4, pulled4, returned4, consumed4;
uint64_t n2 = 0;
while (n2 < SK_HERMES_MSG_MAX && sk_hermes_alloc(alloc_test_id, &msg) == 0) {
msgs[n2] = msg;
n2++;
}
if (n2 != expected_n) ok = 0;
for (i = 0; i < n2; i++) {
uint64_t before = stadium_cells()[msgs[i]->stadium_cell].header.heat;
uint64_t want = (uint64_t)q48_mul((q48_16_t)before, (q48_16_t)SK_HERMES_Q_DECAY);
if (sk_hermes_decay(msgs[i]) != 0) ok = 0;
if (stadium_cells()[msgs[i]->stadium_cell].header.heat != want) ok = 0;
decay_expected += before - want;
}
sk_hermes_ledger(&held3, &pulled3, &returned3, &consumed3);
if (decay_expected == 0) ok = 0; /* vacuity guard: decay must bite */
if (consumed3 - consumed2 != decay_expected) ok = 0;
if (held3 != pulled3 - returned3 - consumed3) ok = 0;
for (i = 0; i < n2; i++) {
if (sk_hermes_release(msgs[i]) != 0) ok = 0;
}
sk_hermes_ledger(&held4, &pulled4, &returned4, &consumed4);
if (held4 != held0) ok = 0;
if (consumed4 != consumed3) ok = 0;
if (held4 != pulled4 - returned4 - consumed4) ok = 0;
if (stadium_reservoir_peek(alloc_test_id) != reservoir0 - decay_expected) ok = 0;
console_println(ok ? "PASS" : "FAIL"); console_println(ok ? "PASS" : "FAIL");
print_uint(" decay_consumed=", decay_expected);
print_uint(" reservoir0=", reservoir0); print_uint(" reservoir0=", reservoir0);
print_uint(" Q_SLOT=", SK_HERMES_Q_SLOT); print_uint(" Q_SLOT=", SK_HERMES_Q_SLOT);
print_uint(" expected_n=", expected_n); print_uint(" expected_n=", expected_n);
+21
View File
@@ -47,6 +47,7 @@
#include <string.h> #include <string.h>
#include "starkernel/vm/kernel_hermes.h" #include "starkernel/vm/kernel_hermes.h"
#include "starkernel/vm/stadium.h" #include "starkernel/vm/stadium.h"
#include "starkernel/q48_16.h"
static SkHermesMessage sk_hermes_msgs[SK_HERMES_MSG_MAX]; static SkHermesMessage sk_hermes_msgs[SK_HERMES_MSG_MAX];
@@ -181,4 +182,24 @@ int sk_hermes_release(SkHermesMessage *msg) {
return rc; return rc;
} }
int sk_hermes_decay(SkHermesMessage *msg) {
uint64_t before, after;
StadiumCell *cell;
if (!msg || !msg->in_use || msg->stadium_cell < 0) return -1;
cell = &stadium_cells()[msg->stadium_cell];
before = cell->header.heat;
after = (uint64_t)q48_mul((q48_16_t)before, (q48_16_t)SK_HERMES_Q_DECAY);
cell->header.heat = after;
/* Task 2.5: the one site where consumed increments (and where held
* pays for it). SXXXVII.3: decay's delta is exact and in hand here. */
sk_hermes_consumed += before - after;
sk_hermes_held -= before - after;
return 0;
}
#endif /* __STARKERNEL__ */ #endif /* __STARKERNEL__ */