proof/FINDINGS.md's Isabelle/HOL word-source sweep (§4) flagged five real
defects; this fixes all five and records resolution in that doc:
- EXECUTE (system_words.c): cast a popped cell straight to a DictEntry*
and called through it with only a null check. Now validates via a new
shared vm_dict_entry_ok(), promoted out of starforth_words.c's
ENTROPY@/ENTROPY! guard (dictionary_management.c) so EXECUTE gets the
same live-entry check.
- ? and DUMP (format_words.c): dereferenced the popped cell as a raw host
pointer, bypassing vm_addr_ok entirely (out-of-VM-bounds read). Both now
go through VM_ADDR/vm_addr_ok/vm_load_cell/vm_ptr like every other
memory word (@, `,`, editor_words.c).
- TYPE (io_words.c): bounds check computed addr+count in signed 64-bit
arithmetic, which can overflow and bypass the check on large operands.
Replaced with vm_addr_ok(), which is written to avoid that overflow.
- DECIMAL/HEX/OCTAL (format_words.c): wrote only the BASE memory cell,
never vm->base, the host-mirror field number-output words actually read
via current_base() -- so these words silently affected number parsing
but never printing. Now call the existing vm_set_base() (previously
only used at boot init), which updates both. vm_get_base/vm_set_base
promoted to public declarations in include/vm.h.
- ALIGN vs ALLOT/,/C,/2, (dictionary_words.c): disagreed on dictionary
growth ceiling (2MB vs 5MB). Investigated which was correct rather than
blindly widening: vm_get_block_addr() maps block N to
vm->memory + N*BLOCK_SIZE across the full 5MB arena, and
USER_BLOCKS_START (block 2048) lines up exactly with
DICTIONARY_MEMORY_SIZE -- so ALLOT/,/C,/2, letting `here` grow past 2MB
could silently corrupt live block/user data sharing that memory.
Tightened ALLOT/,/C,/2, to DICTIONARY_MEMORY_SIZE to match ALIGN.
Verified: hosted (amd64) and kernel (amd64, __STARKERNEL__) both build
clean with -Wall -Werror; hosted POST suite 1012/1012 passing (0
regressions); manually exercised EXECUTE, ?/DUMP, TYPE, HEX/DECIMAL/OCTAL,
and large-ALLOT rejection in the REPL.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014Qf6YcnHgaEtEygq3knx19
Migrates Hermes's message/channel lifecycle onto the Stadium's unified
heat/capacity economy: MSG-ALLOC/FREE-NODE and CH-ALLOC/FREE-NODE now
route entirely through stadium_admit()/stadium_evict(), replacing the
old local free-list + independent heat-field mechanism. Eight
kernel-only STADIUM-* FORTH primitives (ADMIT, EVICT, RES@, RES-PULL,
RES-PUSH, HEAT@, HEAT!, WORD-HEAT), VM.stadium_vm_id threaded through
all three vm_core.c dispatch sites (replacing item 4.1's hardcoded
vm_uuid_hera()), and the stadium_owner[idx] fix so evict-credit lands
in the VM that actually admitted a patron, not whoever owned cell 0.
This session's own contribution, on top of that pre-existing
implementation: found and fixed two bugs blocking the item's own K≡1.0
conservation self-check (HERMES-K was reading 0, not 65536):
- Q.SLOT admission-heat fix (capsules/hermes/init.4th): MSG-SEND/
CH-ACCEPT admitted with Q.1 (the entire fleet-wide "1.0" unit) per
item, a leftover from before the Stadium migration when each
message/channel had its own unconstrained heat field. Instantly
drained the shared, finite reservoir.
- Reservoir floor for word-execution admission (stadium_words.c):
stadium_word_dispatch() (item 4.1) pulls STADIUM_WORD_HEAT_QUANTUM on
every word dispatch, not just first admission -- exhausts a VM's
entire reservoir in ~32 dispatches, starving any application-level
economy sharing that VM's reservoir before it gets a chance to pull
anything. word_dispatch_pull() now clamps word-execution's own pulls
to leave a Q48_ONE/3 floor (same fair-share figure COMMON-CH's own
floor already uses); application-level pulls are unaffected.
- STADIUM-WORD-HEAT primitive + stadium_words_resident_heat(): the
floor deliberately leaves word-execution residents holding real
heat, invisible to HERMES-K's original formula (MSG+CH+reservoir,
no term for word patrons). Adding this term closes K to exactly
65536 on all three architectures.
Also rules on two open scope questions in FABRIC.md: MBR-ALLOC/
MBR-FREE-NODE stay off the Stadium (membership records have no heat
field, never did -- the acceptance bullet's inclusion of them was a
completeness gesture predating a check of the actual layout), and
records the effort number (12 implementation files, +759/-120 lines).
Verified: all three architectures boot clean, full self-test passes,
Stadium conservation closes exactly (resident_sum + reservoir =
Q48_ONE) at both the C/Stadium level and the FORTH-level HERMES-K
check.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Punch list §25 item 4.1 complete.
Replaces the round-robin hotwords cache with Stadium density-ranked
admission/eviction on the kernel side, via the §17.7 reservoir mechanism and a
kernel-side word_id -> cell_index map (no DictEntry change, dict_hash
untouched). Adds stadium_birth_hera() to close the cell-0 panic hazard,
STADIUM_WORD_HEAT_QUANTUM/STADIUM_WORD_COOL_RATE_Q48 Kconfig knobs (flagged
untuned), and a stadium_word_forget() FORGET coherence hook to close a
recycled-word_id aliasing gap.
Verified: all five hotwords_cache_* call sites in dictionary_management.c
bypassed under __STARKERNEL__; word dispatch feeds the Stadium at all three
vm_core.c physics_execution_heat_increment() sites; hosted make unaffected;
all three architectures booted to ok> with matching dict_hash
(0x3d4e1daf289da94f) and matching conservation stats (promotions=354
evictions=0, resident_sum=65536 reservoir=0 sum=65536).
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude