Both words' real blockers are vm_find_word (name resolution, still
unmodelled everywhere in this suite) and a de->func != defer_runtime
identity check (unmodellable -- word_table exposes no per-entry function
identity). Sidestepped the same way physics_freeze_words.c's
FREEZE-WORD/UNFREEZE-WORD/etc. already do: parameterised over an
explicit target_wid_opt :: nat option (whatever vm_find_word would have
resolved) and is_defer_word :: bool (the identity check's result). Given
both, forth_is_full's DF write and forth_defer_fetch_full's DF read are
fully modelled via dict_write_df/de_df, including IS's own real
stack-underflow guard and both words' ds_full push guard.
defer_runtime itself remains unmodelled -- it's a structurally different
DF usage (the DF value is used as a dispatch target via word_table, gap
c, not just returned to the caller like the other DF-reading words).
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Extends the CONSTANT worked example from the previous commit to all five
name-parsing/entry-creating words. Each now has a forth_*_full definition
composing the real C order end to end, up to but not including the
data-field write (gap b, still open):
- forth_create_full: parse -> dict_insert_entry -> forth_align (reused
directly from StarForth_Dictionary_Words.thy's ALIGN model).
- forth_variable_full: parse -> forth_align -> forth_vm_allot_raw (new --
models the raw vm_allot() C helper VARIABLE calls directly, bounds-
checked against DICTIONARY_MEMORY_SIZE exactly like vm_align, distinct
from the FORTH word ALLOT's own VM_MEMORY_SIZE-bounded forth_allot) ->
dict_insert_entry.
- forth_colon_full: nested-':' guard (checked before the parse, matching
real C order) -> parse -> forth_colon_entry_half (mode-set + WORD_SMUDGED
insert). Added forth_parse_word_preserves_vm_mode/dictionary/
word_id_next to StarForth_Base.thy to support this composition cleanly.
- forth_defer_full: parse -> dict_insert_entry, the simplest of the five.
dict_insert_entry's callers (the four forth_*_entry_half definitions)
still take the parsed name as a caller parameter for standalone use.
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
input_buffer/input_length/input_pos (include/vm.h:415-417) turned out to
be plain per-VM array/scalar fields, not host pointers -- unlike almost
every other input-adjacent gap in this suite. vm_parse_word (src/vm.c:
137-160) is a pure whitespace-delimited scan over them, now modelled as
forth_parse_word in StarForth_Base.thy (is_ws + dropWhile/takeWhile,
faithful to the C's skip-then-copy-with-truncation loop, including that
input_pos only advances past a truncated token by what was actually
copied, matching the C's `len < max_len - 1` bound exactly).
dict_insert_entry (added last session) now takes the entry's name as a
parameter instead of hardcoding the empty string. forth_constant_full
composes forth_parse_word with dict_insert_entry end-to-end as a worked
example: CONSTANT's real order (stack-underflow guard -> pop value ->
parse name -> vm_create_word) is modelled in full up to the data-field
write, which remains the one still-open gap. The other four entry-half
definitions (:/CREATE/VARIABLE/DEFER) take the parsed name as a caller
parameter for now rather than repeating the same composition four more
times in one pass.
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Every prior file in the word-source sweep only ever read the abstract
dictionary table; none modelled insertion. dict_insert_entry now models
the word_id-assignment/dictionary-table/latest_id/word_id_next-counter
portion of vm_create_word (dictionary_management.c:379-470), reusing
word_id_next :: nat -- a field already declared in StarForth_Base.thy but
never previously written by any theory. Applied to :, CREATE, VARIABLE,
CONSTANT (StarForth_Defining_Words.thy) and DEFER (StarForth_Defer_Words.thy)
via forth_*_entry_half definitions, each named to keep visible what's
still not modelled: the TIB name-parse dependency, the DF (data-field)
write each word does afterward, and (for :) vm->compiling_word tracking,
none of which have a vm_state counterpart. Pin-shadow conflicts are
sidestepped via an explicit pinned_conflict :: bool parameter, the same
technique already used for the XT-pop gap elsewhere in this suite.
Full suite (54 theories) verifies green.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
StarForth_Lifecycle_Words_Hosted.thy: BIRTH/KILL/PAUSE/RESUME/USE are all
the SAME vm_state transition (pop u, pop caddr, log -- the C's own
"kernel build skips this file via Makefile glob" framing means this
covers only the hosted stand-ins; the real kernel capsule-birth-protocol
words live in src/starkernel/, out of this sweep's scope). First file in
the sweep where every registered word's full vm_state footprint is
captured with no deferred remainder -- name extraction is a pure memory
read, logging is pure I/O. Models the genuine partial-pop-before-error
case (C doesn't check vm->error between its two vm_pop calls).
StarForth_Defer_Words.thy: another duplicate-registration finding, same
class as defining_words.c vs dictionary_manipulation_words.c's [/]/STATE
-- word_registry.c registers this file's DEFER/IS/DEFER@ (Module 27)
AFTER defining_words.c's (Module 17), unconditionally in BOTH builds
(defer_words.c has no __STARKERNEL__ guard despite CLAUDE.md's "kernel-
only addition" framing; the hosted Makefile's SRC wildcard includes it
regardless). This makes StarForth_Defining_Words.thy's DEFER/IS/DEFER@
sentinels describe dead, shadowed code -- corrected in place with
cross-references. The live version hits the same three model gaps
anyway (dictionary-entry creation, data-field addressing, mutable
per-entry dispatch), so only IS's stack-underflow guard is new.
StarForth_Log_Words.thy: the five level-constant pushes, LOG-LEVEL!'s
guard+clamp, and all five LOG-*-STR words fully modelled (the STR words
share lifecycle_words_hosted.c's "pop2 + bounds-check, no vm_state write"
shape). LOG-LEVEL@, the (do-log-N) runtime words (raw threaded-code
pointer, same class as LIT), and the LOG-*" immediates (TIB + compile-
time dependencies) deferred. Finding: LOG-ERROR..DEBUG and LOG-LEVEL@
push with no overflow guard -- more instances of the pattern first found
at DECAY-RATE@.
Suite now 51 theories, green.
