Commit Graph
2 Commits
Author SHA1 Message Date
Robert Allan JamesandClaude Sonnet 5 dfdabcc2d7 word_source: repair DECAY-RATE@ overflow guard and remove dead shadowed registrations
DECAY-RATE@ (physics_freeze_words.c) pushed to the data stack with no
capacity check and no prior pop to make room, unlike its neighbors in
the same file -- the one live, unconditional missing-guard bug the
Isabelle sweep's ~15 candidate findings reduced to once checked against
vm_push()'s real internal bounds check (see proof/FINDINGS.md SS2).

Removed dictionary_manipulation_words.c's [ ] STATE and defining_words.c's
DEFER IS DEFER@ (plus the now-orphaned defining_runtime_defer helper) --
all confirmed permanently shadowed by later dictionary registrations
(defining_words.c and defer_words.c respectively), per FORTH's
newest-first lookup. No behavior change: the removed code was already
unreachable.

Verified: hosted `make` builds clean under -Wall -Werror; the hosted
self-test suite passes 965/965 implemented tests with no regressions.
Three-architecture QEMU acceptance boot, all clean to ok> with an
identical dict_hash=0x24b4279f0670aa3a across amd64/aarch64/riscv64 and
identical 1003/965/0/0 test totals -- logs attached.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-08-14 21:33:17 -04:00
Robert Allan JamesandClaude Sonnet 5 77d8f0606a proof/: add StarForth_Dictionary_Manipulation_Words.thy ([/]/STATE/SMUDGE/HIDDEN/INTERPRET)
Covers the mode/flag half of dictionary_manipulation_words.c that's provable
against the existing vm_mode/dictionary/latest_id model. The raw-pointer
DictEntry navigation half (>BODY/>NAME/NAME>/>LINK/LINK>/CFA/LFA/NFA/PFA/
TRAVERSE/FIND/') is left unmodelled -- same class of gap as control_words.c's
deferred vm_ip/return-stack-as-raw-pointers issue, since the abstract
dict_entry record is word_id-indexed, not addressed, and has no counterpart
for struct-relative pointer arithmetic (name_len, link, body offset).

Genuine findings recorded in comments, not fixed:
- [, ], STATE, and INTERPRET all read/write a file-scope `static cell_t
  state_variable` -- NOT vm->state_var, the real per-VM STATE field used
  everywhere else in the interpreter. In the Tripod multi-VM fleet this
  static is shared across every VM instance, not per-VM.
- dictionary_m_word_hidden's dead #else branch (unreachable since
  WORD_HIDDEN is always defined) calls a function that doesn't exist
  (dictionary_word_smudge vs. the real static dictionary_m_word_smudge).

27 theory files verify with zero errors.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2026-08-13 19:33:42 -04:00