Commit Graph
8 Commits
Author SHA1 Message Date
Robert Allan JamesandClaude Sonnet 5 feace42397 Add diagnostic scan cross-check of the Hermes counters -- FABRIC-3.6.md task 2.8
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-09-21 08:46:07 -04:00
Robert Allan JamesandClaude Sonnet 5 2a2bf6eb35 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>
2026-09-20 21:31:45 -04:00
Robert Allan JamesandClaude Sonnet 5 313ffc89e6 Add exact-equality Hermes ledger self-audit -- FABRIC-3.6.md task 2.6
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-09-20 21:02:27 -04:00
Robert Allan JamesandClaude Sonnet 5 d11eb2e5db Add sk_hermes_decay(), ledgering decay into consumed -- FABRIC-3.6.md task 2.5
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-09-20 18:48:46 -04:00
Robert Allan JamesandClaude Sonnet 5 493d410028 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>
2026-09-20 05:59:09 -04:00
Robert Allan JamesandClaude Sonnet 5 2c1dc1753a Correct sk_hermes_alloc() to admit a real Stadium patron; add sk_hermes_release() -- FABRIC-3.6.md tasks 2.2 (amended) + 2.3
Real finding, caught before building release on a foundation that
couldn't support it: task 2.2's first cut of sk_hermes_alloc() pulled
reservoir heat but never admitted a real Stadium-floor patron -- just a
local in_use flag. FABRIC-3.5.md SXXXIII.4 item 1 says MSG-FREE-NODE
returns heat "via STADIUM-EVICT", which only means something if
allocation admitted something. SXL.4's own invariant, Sigma(resident
patron heat) + reservoir + consumed == Q48_ONE, cannot balance if held
heat is invisible to every term while held. Flagged to Captain Bob
before proceeding; authorized to correct 2.2 in the same pass as
building 2.3 on top of the fix.

sk_hermes_alloc() now calls stadium_admit() with heat = the pulled
amount, behaviour = STADIUM_BEHAVIOUR_DELIVER (matching messaging.4th's
own SB-DELIVER STADIUM-ADMIT exactly), and identity = the message's own
slot index (matching the FORTH precedent -- caught live in the first
boot of this fix that omitting this made stadium_dispatch()'s existing
DELIVER diagnostic print msg_idx=0 for every message instead of a
distinct value). The returned cell index is stored in the message's
own stadium_cell field. Stadium-floor refusal (independent of reservoir
affordability) rolls back the pull the same way the other refusal
paths already do.

sk_hermes_release() -- the function task 2.3 actually asks for -- calls
stadium_evict() on that cell, which itself returns the departing
patron's remaining heat to its owning VM's reservoir, matching
MSG-FREE-NODE's exact shape. Release does not touch the reservoir
directly.

Self-test (kernel_main.c) extended: keeps every allocated message's
pointer, allocates to exhaustion as before, releases all of them, and
checks the reservoir returns to precisely its starting value.
"Undecayed" is true by construction (no decay/TTL logic exists yet,
task 2.5) -- exact restoration, not approximate.

Three-arch boot clean: amd64/aarch64/riscv64 all reach [zuse@Hera] ok>,
zero UNKNOWN WORD, dict_hash unmoved from task 2.2. All three print
identical PASS arithmetic: reservoir0=65536, reservoir_after_alloc=0,
reservoir_final=65536. No compiler warnings.

stadium_dispatch()'s DELIVER-case console output (one line per
eviction) is pre-existing instrumentation, not new -- confirmed real
and load-bearing per stadium.c's own comment, verbose but expected.

Authorized by Captain Bob ("yes").

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-09-20 04:20:14 -04:00
Robert Allan JamesandClaude Sonnet 5 9d129fdb1c Add sk_hermes_alloc(), the heat-coupled allocator -- FABRIC-3.6.md task 2.2, item 28
The piece FABRIC-3.5.md SXXXIII.6 calls "what remains genuinely hard,"
built and proven first per its own recommendation. Added
src/starkernel/vm/kernel_hermes.c (wired into Makefile.starkernel's
LOADER_EXTRA_SRCS -- this repo lists vm/*.c files explicitly, no glob)
and sk_hermes_alloc()'s declaration in kernel_hermes.h.

Checks stadium_reservoir_peek(vm_id) >= SK_HERMES_Q_SLOT before
touching the reservoir at all -- refusal this way needs no rollback,
since nothing was pulled -- with an explicit rollback path
(stadium_reservoir_push) kept defensively for the pull-then-short case,
though nothing in this single-core kernel is expected to reach it.

SK_HERMES_Q_SLOT = Q48_ONE / SK_HERMES_MSG_MAX (2048), deliberately
simpler than messaging.4th's own formula, which reserves a Q.1/3 floor
for COMMON-CH's own Stadium heat -- kernel-Hermes has no such object
(SXXXIII.4/SXXXIII.5's flat membership list carries no heat of its
own), so there is nothing left for that floor to protect.

Self-test in kernel_main.c, same diagnostic-only synthetic-VM pattern
as the existing Stadium quota grant self-test (lo=3, distinct from
that test's lo=1): reads back the actual granted reservoir rather than
assuming a number, derives expected_n from it, allocates to refusal,
and checks the refusal lands at exactly expected_n, the reservoir
doesn't move on the refused attempt (rollback proven, not assumed),
and the final reservoir is exactly reservoir0 minus got_n times
Q_SLOT.

Three-arch boot clean: amd64/aarch64/riscv64 all reach [zuse@Hera] ok>,
zero UNKNOWN WORD, dict_hash unmoved from task 2.1 (pure C, no FORTH
touched). All three print identical self-test arithmetic: reservoir0=
65536 Q_SLOT=2048 expected_n=32 got_n=32 reservoir_after=0. No compiler
warnings.

Noted, not fixed: Q_SLOT's divisor and SK_HERMES_MSG_MAX are the same
32, so reservoir and arena exhaustion land at exactly the same count by
construction -- this test can't distinguish which refusal reason
fired, only that refusal is correct and rolls back correctly.

Deliberately not evidence for stadium_conserved(): allocating alone
(no release yet, task 2.3) leaves pulled heat held off the Stadium
floor, so the two-term check would correctly read false right now if
run mid-hold. That's expected, not a bug -- Stage B (task 2.7) is
defined as "before and after the alloc/free cycle," not "continuously
during." This task's self-test checks reservoir arithmetic directly
instead.

Authorized by Captain Bob ("Yes continue").

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-09-19 21:00:20 -04:00
Robert Allan JamesandClaude Sonnet 5 f10fa7ae83 Add kernel-Hermes message/membership structures -- FABRIC-3.6.md task 2.1, Phase 2 begins
Phase 2, task 2.1 only: type definitions, wired to nothing, drawing no
heat -- no allocator, no protocol logic, no registration anywhere.
FABRIC-3.5.md SXXII.4: Phase 2 structures come first and prove nothing
until the allocator is built on top (task 2.2 onward, each its own
commit).

Added include/starkernel/vm/kernel_hermes.h:

SkHermesMessage -- field-for-field mirror of messaging.4th's live
9-cell MSG-* layout (type/from/to/payload addr+len/Stadium cell
index/seq/channel/orig-type), per SXXXIII.4 item 1 ("roughly half the
file is accessors that become struct fields"), plus an explicit
in_use flag for task 2.2's allocator. Deliberately no separate heat
field: per SXL.4, a message's heat IS the Stadium cell it occupies,
not a value copied alongside it -- one source of truth for the
conservation invariant stadium_conserved() (task 0.7) checks.

SkHermesMembership -- one flat broadcast membership list, SXXXIII.4/
SXXXIII.5's recommended replacement for messaging.4th's 28-word channel
abstraction (traced to exactly one live caller, CH-ADD-MBR). Item 27
(negotiation vs. broadcast, Phase 3 blocker B1) is not answered by this
structure and isn't meant to be -- a flat list is correct either way.

Genuinely wired to nothing: no .c file, no Makefile change, no include
from any compiled source. Syntax-checked standalone (gcc -std=c99
-Wall -Wextra -Werror -fsyntax-only) before touching the real build.

Boot byte-identical to task 1.9's baseline on amd64 (same dict_hash
triple, zero UNKNOWN WORD). Did not repeat aarch64/riscv64 -- the file
compiles into no object on any architecture, so there is no mechanism
by which it could diverge.

Authorized by Captain Bob ("yes").

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-09-19 20:48:24 -04:00