Adds compiling_word_id :: nat option to vm_state, modelling vm->compiling_word
(include/vm.h:421). forth_colon_entry_half now sets it from latest_id on success
and forces it to None on the pinned-conflict failure path, matching the real C's
unconditional `vm->compiling_word = de;` before its own NULL check in
vm_enter_compile_mode (src/vm.c:232-264).
: is now closed through entry creation + compiling_word tracking, same point as
CREATE/VARIABLE/CONSTANT. Remaining gap for : is the same DF write (gap b,
vm_align+HERE capture) those three already closed but not yet composed in here.
All 52 theories verify clean (isabelle build -D proof/, ~48s).
Part of the pre-Artemis closeout pass (FABRIC-2.md 5.2). PROOFS included per
Captain Bob's 2026-08-14 instruction.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
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>
Adds de_df :: cell to dict_entry (StarForth_Base.thy) -- the DF cell
modelled as a plain value, closing gap (b) for every word that only
reads/writes it through its OWNING entry. Confirmed by grep this record
has exactly one construction site in the whole 52-theory suite
(dict_insert_entry), so the field addition's blast radius is contained
to StarForth_Defining_Words.thy alone -- full suite still verifies
unchanged elsewhere.
dict_write_df writes an existing entry's DF by word_id. forth_create_full/
forth_variable_full/forth_constant_full now compose the DF write in,
making CREATE/VARIABLE/CONSTANT the first three FULLY modelled words in
this file (guard through parse through insertion through the DF write --
nothing left unmodelled per word except the pin-shadow name-scan guard,
sidestepped the same way as everywhere else in this suite).
Their runtime companions (defining_runtime_create/_variable/_constant --
confirmed byte-identical C bodies) share one new definition,
forth_runtime_read_df, gated on ds_full matching vm_push's real internal
check. Required adding current_executing_word_id to vm_state (mirrors
vm->current_executing_entry, word-id-indexed like latest_id).
DEFER and : remain at their previous closure level: DEFER's DF write was
already implicitly closed (de_df=0 at creation matches its explicit
*df=0), but its own runtime is a fundamentally different DF usage
(dispatch reassignment via a stored pointer, gap c, not a plain value);
: has no vm_state field for vm->compiling_word tracking.
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>
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>
