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
Aggregates the sweep's cross-cutting architectural findings (file-scope
statics standing in for per-VM state, missing overflow guards, duplicate
word registration/shadowing) and gives an executive-summary coverage
index across all 34 src/word_source/*.c files, per Bob's original framing
for this initiative.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude