theory StarForth_Defining_Words imports StarForth_Base StarForth_Memory_Words ACL_Pin_Monotone StarForth_Dictionary_Words begin (* ========================================================================= Mirrors: src/word_source/defining_words.c Registers: : ; CREATE VARIABLE CONSTANT IMMEDIATE STATE [ ] FORGET COMPILE [COMPILE] LIT LITERAL does_rt DOES> DEFER IS DEFER@ ── Duplicate-registration finding (corrects a StarForth_Dictionary_ Manipulation_Words.thy note) ──────────────────────────────────────── `src/word_registry.c` registers dictionary_manipulation_words.c's `[`, `]`, `STATE` (Module 13, line 122) BEFORE defining_words.c's `[`, `]`, `STATE` (Module 17, line 126). FORTH dictionary lookup finds the MOST RECENT definition of a name first, so defining_words.c's versions are the only ones ever reachable -- dictionary_manipulation_words.c's `[`/ `]`/`STATE` are permanently shadowed, dead code from the moment boot registration completes. CORRECTED 2026-08-14: `INTERPRET` is NOT part of this shadow -- defining_words.c never registers a word named INTERPRET at all (confirmed by grep), so dictionary_manipulation_words.c's INTERPRET is the only registration that exists and is live, not dead. The earlier version of this note (and proof/FINDINGS.md) incorrectly folded it into the shadowed group. This also CORRECTS that file's finding, not just supersedes it: its `[`/`]`/`STATE` write/read a dead file-scope `static cell_t state_variable`, cross-VM-shared and never the real per-VM STATE. The LIVE versions here (defining_word_left_bracket/right_bracket/state) use `vm->state_addr` (include/vm.h:452) -- a genuine per-VM VM-memory address, correctly written via `vm_store_cell`. The dead-static bug is real IN THE SHADOWED CODE, but does not reach runtime: no VM instance's `[`/`]`/`STATE` actually touches that static. Added `state_addr :: nat` to vm_state (StarForth_Base.thy) to model this correctly. ── Scope of this file ────────────────────────────────────────────────── Split three ways: 1. Mode/flag/address words ([, ], STATE, IMMEDIATE) -- fully modelled, provable against `vm_mode`/`state_addr`/`memory`/`dictionary`/ `latest_id`. 2. `:` / `;` -- guard conditions modelled; `:`'s STATE/mode-setting half of `vm_enter_compile_mode` is modelled (identical shape to `]`), AND (added 2026-08-14, see `dict_insert_entry` below) its dictionary- entry-creation half is now PARTIALLY modelled too (`forth_colon_entry_half`: fresh word_id, WORD_SMUDGED flag, ACL defaults) -- what remains unmodelled is named at that definition's site. `;`'s entire effect beyond the guard (`vm_exit_compile_mode`: find/compile EXIT, clear WORD_SMUDGED, set WORD_COMPILED, evict hot-words cache) is still NOT modelled, for the same reason plus dependence on the hot-words cache, itself never modelled in this suite. 3. Everything else (CREATE, VARIABLE, CONSTANT partially modelled as of 2026-08-14, see below; FORGET, COMPILE, [COMPILE], LIT, LITERAL, does_rt, DOES>, DEFER, IS, DEFER@, and the three defining-runtime functions CREATE/VARIABLE/CONSTANT install still NOT modelled) -- each hits one or more of the same three model gaps, named once here rather than repeated per word: (a) DICTIONARY-ENTRY CREATION, PARTIALLY CLOSED 2026-08-14. Was not modelled anywhere in this proof suite: `dictionary :: nat \ dict_entry option` (StarForth_Base.thy:498) was treated as a fixed, pre-populated table by every theory so far -- FIND/ TRAVERSE/etc. in StarForth_Dictionary_Manipulation_Words.thy only READ it. This was the first file in the sweep whose primary job IS insertion (`:`, CREATE, VARIABLE, CONSTANT, DEFER all call `vm_create_word`). `dict_insert_entry` (defined below) now models the word_id-assignment/dictionary-table/latest_id/ `word_id_next`-counter portion of `vm_create_word`, reusing the `word_id_next :: nat` field already declared in StarForth_ Base.thy but never previously written by any theory. What remains unmodelled per word: `vm_create_word` itself parses no input (name arrives pre-parsed, but the parse producing that name is the TIB/input-subsystem gap, present throughout this suite; `:` alone captures the entry into `compiling_word_id`, CLOSED 2026-08-15, see `forth_colon_entry_half` below), and callers still mutate the returned `DictEntry*` directly afterward for flags beyond what `dict_insert_entry`'s `init_flags` parameter already captures. This is still a materially bigger gap than the raw-pointer-navigation gap already flagged in dictionary_manipulation_words.c (which only reads), even partially closed -- the single largest finding of this file remains real, just smaller than before. (b) DATA-FIELD (DF) ADDRESSING: `dict_entry` (StarForth_Base.thy:293) has no field corresponding to a DictEntry's data-field cell (the storage `vm_dictionary_get_data_field` returns a pointer into). CREATE/VARIABLE/CONSTANT's runtimes, DODOES, and does_rt all read or write this cell -- the exact gap already named for `>BODY` in StarForth_Dictionary_Manipulation_Words.thy (`to_body_not_modelled`). Same root cause, different words. (c) MUTABLE PER-ENTRY DISPATCH: `word_table` (StarForth_Base.thy:626) is a fixed, uninterpreted global constant -- by design (see that section's comment), not a per-VM-instance mutable field. DEFER's `IS` reassigns an entry's *effective* dispatch target at runtime (stored in the DF cell and read by `defining_runtime_defer`); a fixed `word_table` cannot express this at all, independent of gap (b). LIT additionally treats the top return-stack cell as a raw C `cell_t*` threaded-code instruction pointer, advanced with C pointer arithmetic (`rip++`) and dereferenced directly -- NOT as a VM address resolved through `vm_ptr`/`vm_addr_ok` the way control_words.c's return-stack-held IP values were (see StarForth_Control_Words.thy's resume note: that gap turned out to already be covered by `mem_read` on VM-address-valued return-stack entries). LIT's IP is a genuinely different, raw-host-pointer usage of the same field; the list-based `return_stack :: cell list` model has no way to hold or advance a host pointer. ======================================================================== *) definition WORD_IMMEDIATE :: nat where "WORD_IMMEDIATE = 0x80" definition WORD_SMUDGED :: nat where "WORD_SMUDGED = 0x20" (* ── Dictionary-entry insertion (gap (a), PARTIALLY CLOSED 2026-08-14) ──── `word_id_next` (StarForth_Base.thy, declared but never written by any theory before this one -- confirmed by grep) is exactly C's `vm->next_word_id`/`vm_dictionary_acquire_word_id` mechanism (src/dictionary_management.c:87-92,94-110): a monotonically increasing counter, one per fresh word, capped at DICTIONARY_SIZE. `vm_create_word` itself (dictionary_management.c:379-470) does three things this definition models and one it does not: 1. Pin-shadow guard: scans vm->latest's linked list for a same-name PINNED entry; refuses (vm->error=1) if found. Sidestepped the same way StarForth_ACL_Words.thy/StarForth_Physics_Freeze_Words.thy sidestep the equivalent FIND-shaped dependency: parameterised over an explicit `pinned_conflict :: bool`, standing in for "whatever a real name-scan would have found." 2. Allocates a `word_id` via the counter and installs the new entry into the word-id-indexed table (`vm->word_id_map` / this model's `dictionary`) -- modelled exactly, both are word_id-indexed. 3. Prepends to `vm->latest`'s linked list, which is also what backs `latest_id` in this model. NOT modelled: the real `entry->func` (word_table -- a fixed, uninterpreted global per StarForth_Base.thy's design, cannot express a NEW word's dispatch target, which is gap (c)), the physics-metadata seed (`physics_metadata_init`/`apply_seed` -- modelled as all-zero `dict_physics`, not the real seeding logic), and the DF cell (gap (b), unchanged). ACL fields are modelled exactly from the C's literal initializers (acl_ttl=0, acl_allow=True, acl_mode=ACL_MODE_TTL=0, acl_pinned=False) -- src/dictionary_management.c:427-430. *) definition dict_insert_entry :: "string \ nat \ bool \ vm_state \ vm_state" where "dict_insert_entry name init_flags pinned_conflict vm = (if pinned_conflict then set_error vm else let wid = word_id_next vm; e = \de_name = name, de_flags = init_flags, de_heat = 0, de_word_id = wid, de_physics = \dp_temperature_q8 = 0, dp_last_active_ns = 0, dp_last_decay_ns = 0, dp_mass_bytes = 0, dp_avg_latency_ns = 0, dp_state_flags = 0\, de_acl_ttl = 0, de_acl_allow = True, de_acl_mode = ACL_MODE_TTL, de_acl_pinned = False, de_df = 0\ in vm\dictionary := (dictionary vm)(wid := Some e), latest_id := Some wid, word_id_next := wid + 1\)" lemma dict_insert_entry_pinned_conflict_errors: assumes "pinned_conflict" shows "vm_error (dict_insert_entry name init_flags pinned_conflict vm)" by (simp add: dict_insert_entry_def set_error_def assms) lemma dict_insert_entry_assigns_fresh_word_id: assumes "\ pinned_conflict" shows "latest_id (dict_insert_entry name init_flags pinned_conflict vm) = Some (word_id_next vm)" using assms by (simp add: dict_insert_entry_def Let_def) lemma dict_insert_entry_populates_dictionary: assumes "\ pinned_conflict" shows "\e. dictionary (dict_insert_entry name init_flags pinned_conflict vm) (word_id_next vm) = Some e \ de_word_id e = word_id_next vm \ de_name e = name \ de_flags e = init_flags \ de_heat e = 0 \ de_acl_ttl e = 0 \ de_acl_allow e \ de_acl_mode e = ACL_MODE_TTL \ \ de_acl_pinned e \ de_df e = 0" using assms by (simp add: dict_insert_entry_def Let_def) lemma dict_insert_entry_advances_counter: assumes "\ pinned_conflict" shows "word_id_next (dict_insert_entry name init_flags pinned_conflict vm) = word_id_next vm + 1" using assms by (simp add: dict_insert_entry_def Let_def) lemma dict_insert_entry_data_stack_unchanged: "data_stack (dict_insert_entry name init_flags pinned_conflict vm) = data_stack vm" by (simp add: dict_insert_entry_def set_error_def Let_def) lemma dict_insert_entry_not_full_word_id_next_bound: True \ \NOT modelled: the C's `word_id_next >= DICTIONARY_SIZE` exhaustion branch (dictionary_management.c:87-91,102), which returns WORD_ID_INVALID and skips the `word_id_map` write while the linked- list prepend to vm->latest still happens unconditionally regardless. This model always succeeds at installing into `dictionary` once past the pin guard -- a real, uncovered edge case (a VM that defines more than DICTIONARY_SIZE words), not claimed to be handled.\ by simp (* ── Data-field (DF) write, gap (b) PARTIALLY CLOSED 2026-08-15 ────────── `de_df` (StarForth_Base.thy) models the DF cell as a plain value. `dict_write_df` writes it into an EXISTING entry by word_id -- the shared mechanism CREATE/VARIABLE/CONSTANT's own DF write (after `vm_create_word` already returned) all reduce to. No-op if the word_id doesn't resolve (mirrors a defensive NULL check that never actually fires on any real caller in this suite, all of which write DF immediately after a successful `dict_insert_entry` at a word_id they just observed being created). *) definition dict_write_df :: "nat \ cell \ vm_state \ vm_state" where "dict_write_df wid v vm = (case dictionary vm wid of None \ vm | Some e \ vm\dictionary := (dictionary vm)(wid := Some (e\de_df := v\))\)" lemma dict_write_df_present: assumes "dictionary vm wid = Some e" shows "dictionary (dict_write_df wid v vm) wid = Some (e\de_df := v\)" using assms by (simp add: dict_write_df_def) lemma dict_write_df_absent_noop: assumes "dictionary vm wid = None" shows "dict_write_df wid v vm = vm" using assms by (simp add: dict_write_df_def) lemma dict_write_df_data_stack_unchanged: "data_stack (dict_write_df wid v vm) = data_stack vm" by (simp add: dict_write_df_def split: option.split) (* ── [ ( -- ) : interpret mode, LIVE version (see file header) ──────────── *) (* C: vm_store_cell(vm, vm->state_addr, 0); vm->mode = MODE_INTERPRET. *) definition forth_d_left_bracket :: "vm_state \ vm_state" where "forth_d_left_bracket vm = vm\memory := mem_write (memory vm) (state_addr vm) 0, vm_mode := ModeInterpret\" lemma d_left_bracket_sets_interpret: "vm_mode (forth_d_left_bracket vm) = ModeInterpret" by (simp add: forth_d_left_bracket_def) lemma d_left_bracket_writes_state_cell: "mem_read (memory (forth_d_left_bracket vm)) (state_addr vm) = 0" by (simp add: forth_d_left_bracket_def mem_read_def mem_write_def) lemma d_left_bracket_data_stack_unchanged: "data_stack (forth_d_left_bracket vm) = data_stack vm" by (simp add: forth_d_left_bracket_def) lemma d_left_bracket_never_errors: "vm_error (forth_d_left_bracket vm) = vm_error vm" by (simp add: forth_d_left_bracket_def) (* ── ] ( -- ) : compile mode, LIVE version ───────────────────────────────── *) (* C: vm_store_cell(vm, vm->state_addr, (cell_t)-1); vm->mode = MODE_COMPILE. *) definition forth_d_right_bracket :: "vm_state \ vm_state" where "forth_d_right_bracket vm = vm\memory := mem_write (memory vm) (state_addr vm) (-1), vm_mode := ModeCompile\" lemma d_right_bracket_sets_compile: "vm_mode (forth_d_right_bracket vm) = ModeCompile" by (simp add: forth_d_right_bracket_def) lemma d_right_bracket_writes_state_cell: "mem_read (memory (forth_d_right_bracket vm)) (state_addr vm) = -1" by (simp add: forth_d_right_bracket_def mem_read_def mem_write_def) lemma d_right_bracket_data_stack_unchanged: "data_stack (forth_d_right_bracket vm) = data_stack vm" by (simp add: forth_d_right_bracket_def) lemma d_right_bracket_never_errors: "vm_error (forth_d_right_bracket vm) = vm_error vm" by (simp add: forth_d_right_bracket_def) lemma d_bracket_right_then_left: "vm_mode (forth_d_left_bracket (forth_d_right_bracket vm)) = ModeInterpret" by (simp add: forth_d_left_bracket_def) lemma d_bracket_left_then_right: "vm_mode (forth_d_right_bracket (forth_d_left_bracket vm)) = ModeCompile" by (simp add: forth_d_right_bracket_def) (* ── STATE ( -- addr ) : LIVE version, pushes a real VM address ─────────── *) (* C: vm_push(vm, (cell_t)vm->state_addr). Unlike the shadowed dictionary_ manipulation_words.c version (which pushed the address of a dead host static, and was left unmodelled), this pushes `state_addr` -- a genuine per-VM field, so this word IS modellable. *) definition forth_d_state :: "vm_state \ vm_state" where "forth_d_state vm = (if ds_full vm then set_error vm else vm\data_stack := word_of_nat (state_addr vm) # data_stack vm\)" lemma d_state_normal: assumes "\ ds_full vm" shows "data_stack (forth_d_state vm) = word_of_nat (state_addr vm) # data_stack vm" by (simp add: forth_d_state_def assms) lemma d_state_overflow: assumes "ds_full vm" shows "vm_error (forth_d_state vm)" by (simp add: forth_d_state_def set_error_def assms) lemma d_state_preserves_state_addr: "state_addr (forth_d_state vm) = state_addr vm" by (simp add: forth_d_state_def set_error_def) (* ── IMMEDIATE ( -- ) : mark latest word immediate, no mode guard ───────── *) (* C: error if vm->latest is NULL; else vm->latest->flags |= WORD_IMMEDIATE. Unlike HIDDEN (dictionary_manipulation_words.c), there is no compile-mode guard at all. *) definition forth_immediate :: "vm_state \ vm_state" where "forth_immediate vm = (case latest_id vm of None \ set_error vm | Some wid \ (case dictionary vm wid of None \ set_error vm | Some e \ vm\dictionary := (dictionary vm) (wid := Some (e\de_flags := de_flags e OR WORD_IMMEDIATE\))\))" lemma immediate_requires_latest: assumes "latest_id vm = None" shows "vm_error (forth_immediate vm)" by (simp add: forth_immediate_def set_error_def assms) lemma immediate_requires_latest_present_in_dict: assumes "latest_id vm = Some wid" assumes "dictionary vm wid = None" shows "vm_error (forth_immediate vm)" by (simp add: forth_immediate_def set_error_def assms) lemma immediate_sets_flag: assumes "latest_id vm = Some wid" assumes "dictionary vm wid = Some e" shows "\e'. dictionary (forth_immediate vm) wid = Some e' \ de_flags e' = de_flags e OR WORD_IMMEDIATE" using assms by (simp add: forth_immediate_def) lemma immediate_data_stack_unchanged: "data_stack (forth_immediate vm) = data_stack vm" by (auto simp: forth_immediate_def set_error_def split: option.split) lemma immediate_no_mode_guard: \ \Unlike HIDDEN, IMMEDIATE has no `vm_mode vm \ ModeCompile` check at all -- when the latest-word guards above are satisfied, its error status is exactly whatever it was on entry (no NEW error is raised by a compile-mode check, since there is none). Stated explicitly since every other flag-setting word in this sweep (SMUDGE, HIDDEN) DOES gate on compile mode.\ assumes "latest_id vm = Some wid" "dictionary vm wid = Some e" shows "vm_error (forth_immediate vm) = vm_error vm" using assms by (simp add: forth_immediate_def) (* ── : ( "name" -- ) : nested-guard + mode/STATE half only ──────────────── *) (* C (defining_word_colon + vm_enter_compile_mode): error if already in MODE_COMPILE (nested ':' is illegal per FORTH-79); else vm->mode = MODE_COMPILE, vm->state_var = -1, vm_store_cell(vm, vm->state_addr, -1), THEN vm_create_word(...) -- the entry-creation half, see file header finding (a), is NOT modelled. Modelled here: guard + the mode/state_var/ state_addr-cell effect, which is state-only and has the identical shape to `]` plus the extra `state_var` write `]` itself does not do. *) definition forth_colon_guard :: "vm_state \ vm_state" where "forth_colon_guard vm = (if vm_mode vm = ModeCompile then set_error vm else vm\vm_mode := ModeCompile, state_var := -1, memory := mem_write (memory vm) (state_addr vm) (-1)\)" lemma colon_nested_errors: assumes "vm_mode vm = ModeCompile" shows "vm_error (forth_colon_guard vm)" by (simp add: forth_colon_guard_def set_error_def assms) lemma colon_sets_compile_mode: assumes "vm_mode vm \ ModeCompile" shows "vm_mode (forth_colon_guard vm) = ModeCompile" by (simp add: forth_colon_guard_def assms) lemma colon_sets_state_var: assumes "vm_mode vm \ ModeCompile" shows "state_var (forth_colon_guard vm) = -1" by (simp add: forth_colon_guard_def assms) lemma colon_writes_state_cell: assumes "vm_mode vm \ ModeCompile" shows "mem_read (memory (forth_colon_guard vm)) (state_addr vm) = -1" by (simp add: forth_colon_guard_def mem_read_def mem_write_def assms) lemma colon_guard_not_full_colon: True \ \forth_colon_guard is NOT a full model of `:` -- it omits the dictionary-entry-creation half (`vm_create_word`, `vm->compiling_word`, WORD_SMUDGED, the DF write of the threaded-body start address). See file header finding (a)/(b). Named so the omission is greppable.\ by simp (* ── : entry-creation half, gap (a) CLOSED 2026-08-15 ───────────────────── `vm_enter_compile_mode` (src/vm.c:232-264) does forth_colon_guard's mode/state effect FIRST, then `vm_create_word(...)`, then `de->flags |= WORD_SMUDGED` on the fresh entry (vm.c:251) -- unlike CREATE/VARIABLE/CONSTANT, `:` sets a real flag at creation time, so this reuses `dict_insert_entry WORD_SMUDGED` rather than `dict_insert_entry 0`. Composed after forth_colon_guard: only valid when the nested-`:` guard did not already error (real C: vm_create_word is never reached if `defining_word_colon`'s own nested check fired, since that returns before calling vm_enter_compile_mode at all). `vm->compiling_word = de;` (vm.c:245) is unconditional -- it runs BEFORE the `if (!de) { vm->error = 1; return; }` check right after it, so compiling_word is set to the fresh entry on success and to NULL (mirrored here as `None`) on failure, in both cases. Modelled via `compiling_word_id` (StarForth_Base.thy), set from `latest_id vm1` after `dict_insert_entry` (which sets `latest_id := Some wid` only on the non-pinned-conflict path and leaves it untouched on the error path) -- explicitly forced to `None` on the pinned_conflict branch so a stale `latest_id` from an earlier successful definition can never leak through as a false "compiling_word" on this failure. Still NOT modelled: vm_align+HERE capture, and the DF write of the threaded-body start address (gap b). *) definition forth_colon_entry_half :: "string \ bool \ vm_state \ vm_state" where "forth_colon_entry_half name pinned_conflict vm = (let vm1 = dict_insert_entry name WORD_SMUDGED pinned_conflict (forth_colon_guard vm) in vm1\compiling_word_id := (if pinned_conflict then None else latest_id vm1)\)" lemma colon_entry_half_requires_guard_to_pass: assumes "vm_mode vm \ ModeCompile" "\ pinned_conflict" shows "\e. dictionary (forth_colon_entry_half name pinned_conflict vm) (word_id_next (forth_colon_guard vm)) = Some e \ de_name e = name \ de_flags e = WORD_SMUDGED" using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def dict_insert_entry_def Let_def) lemma colon_entry_half_still_compile_mode: assumes "vm_mode vm \ ModeCompile" "\ pinned_conflict" shows "vm_mode (forth_colon_entry_half name pinned_conflict vm) = ModeCompile" using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def dict_insert_entry_def Let_def) lemma colon_entry_half_sets_compiling_word: assumes "\ pinned_conflict" shows "compiling_word_id (forth_colon_entry_half name pinned_conflict vm) = Some (word_id_next (forth_colon_guard vm))" using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def dict_insert_entry_def Let_def) lemma colon_entry_half_conflict_clears_compiling_word: assumes "pinned_conflict" shows "compiling_word_id (forth_colon_entry_half name pinned_conflict vm) = None" using assms by (simp add: forth_colon_entry_half_def) lemma colon_entry_half_not_full_colon: True \ \Still NOT modelled: name parse (`name` is a caller-supplied parameter here, not derived from `forth_parse_word` -- see forth_colon_full below), vm_align+HERE capture, DF write of the threaded-body start address (gap b). See section header.\ by simp (* ── `:`, full composition, gap (a)+parse+compiling_word CLOSED 2026-08-15 `defining_word_colon` (defining_words.c:407-426): nested-`:` guard FIRST (checked before any parse -- real C order), THEN parse name, THEN `vm_enter_compile_mode` (mode/state effect + WORD_SMUDGED entry creation + compiling_word_id, already `forth_colon_entry_half`). `forth_parse_word` never touches `vm_mode`, so checking the guard before parsing and reusing `forth_colon_entry_half` (which re-derives the same guard internally via `forth_colon_guard`) afterward is sound -- the mode it observes is unchanged by the intervening parse. Still NOT modelled: vm_align+HERE capture, DF write of the threaded-body start address (gap b) -- this is the last remaining gap for `:`. *) definition forth_colon_full :: "nat \ bool \ vm_state \ vm_state" where "forth_colon_full max_len pinned_conflict vm = (if vm_mode vm = ModeCompile then set_error vm else let (nm, vm1) = forth_parse_word max_len vm in if nm = '''' then set_error vm1 else forth_colon_entry_half nm pinned_conflict vm1)" lemma colon_full_nested_errors: assumes "vm_mode vm = ModeCompile" shows "vm_error (forth_colon_full max_len pinned_conflict vm)" by (simp add: forth_colon_full_def set_error_def assms) lemma colon_full_empty_parse_errors: assumes "vm_mode vm \ ModeCompile" assumes "fst (forth_parse_word max_len vm) = ''''" shows "vm_error (forth_colon_full max_len pinned_conflict vm)" proof - obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce hence "nm = ''''" using assms(2) by simp thus ?thesis using parse_eq assms(1) by (simp add: forth_colon_full_def set_error_def) qed lemma colon_full_success_populates_dictionary: assumes "vm_mode vm \ ModeCompile" assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \ []" (is "?s1 \ []") assumes "max_len \ 2" assumes "\ pinned_conflict" shows "\e wid. dictionary (forth_colon_full max_len pinned_conflict vm) wid = Some e \ de_name e \ '''' \ de_flags e = WORD_SMUDGED" proof - obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce hence nm_nonempty: "nm \ ''''" using forth_parse_word_success_nonempty[OF assms(2) assms(3)] by (metis fstI) have vm_mode_vm1: "vm_mode vm1 = vm_mode vm" using parse_eq forth_parse_word_preserves_vm_mode[of max_len vm] by simp have "forth_colon_full max_len pinned_conflict vm = forth_colon_entry_half nm pinned_conflict vm1" using parse_eq nm_nonempty assms(1) by (simp add: forth_colon_full_def) moreover have "\e. dictionary (forth_colon_entry_half nm pinned_conflict vm1) (word_id_next (forth_colon_guard vm1)) = Some e \ de_name e = nm \ de_flags e = WORD_SMUDGED" using assms(1) assms(4) vm_mode_vm1 by (simp add: forth_colon_entry_half_def forth_colon_guard_def dict_insert_entry_def Let_def) ultimately show ?thesis using nm_nonempty by auto qed lemma colon_full_success_sets_compiling_word: assumes "vm_mode vm \ ModeCompile" assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \ []" assumes "max_len \ 2" assumes "\ pinned_conflict" shows "compiling_word_id (forth_colon_full max_len pinned_conflict vm) \ None" proof - obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce hence nm_nonempty: "nm \ ''''" using forth_parse_word_success_nonempty[OF assms(2) assms(3)] by (metis fstI) have "forth_colon_full max_len pinned_conflict vm = forth_colon_entry_half nm pinned_conflict vm1" using parse_eq nm_nonempty assms(1) by (simp add: forth_colon_full_def) thus ?thesis using colon_entry_half_sets_compiling_word[OF assms(4), of nm vm1] by simp qed (* ── ; ( -- ) : compile-mode guard only ──────────────────────────────────── *) (* C: error unless vm->mode == MODE_COMPILE; else calls vm_exit_compile_mode, entirely unmodelled (finds/compiles EXIT, flips WORD_SMUDGED/WORD_COMPILED, evicts hot-words cache -- none modelled in this suite). *) definition forth_semicolon_guard :: "vm_state \ vm_state" where "forth_semicolon_guard vm = (if vm_mode vm \ ModeCompile then set_error vm else vm)" lemma semicolon_requires_compile_mode: assumes "vm_mode vm \ ModeCompile" shows "vm_error (forth_semicolon_guard vm)" by (simp add: forth_semicolon_guard_def set_error_def assms) lemma semicolon_guard_not_full_semicolon: True \ \forth_semicolon_guard covers only the guard raised directly in defining_word_semicolon. vm_exit_compile_mode's own effects (EXIT lookup+compile, WORD_SMUDGED/WORD_COMPILED flag flip, hot-words cache eviction) are entirely unmodelled -- none of EXIT-lookup, per-entry mutable flags via a live pointer, or the hot-words cache have any counterpart in this suite's abstract model.\ by simp (* ── CREATE / VARIABLE / CONSTANT: entry-creation half only, gap (a) PARTIALLY CLOSED 2026-08-14 ───────────────────────────────────────────── All three call `vm_create_word(vm, namebuf, nlen, )` with no extra flags set afterward (`entry->flags = 0` inside vm_create_word is the final value) -- so their entry-creation half is exactly `dict_insert_entry 0`, reused verbatim from the definition above. NOT modelled, same as before: the name parse that produces `namebuf`/`nlen` (TIB/input-subsystem gap, present in every word in this suite that parses a name), CREATE's/VARIABLE's `vm_align`+HERE capture, VARIABLE's `vm_allot` of one cell, and all three words' DF write of their respective captured/popped value (gap (b), unchanged). These are named `forth__entry_half` deliberately, not `forth_`, to keep the omission visible at the call site the way `forth_colon_guard` already does for `:`. *) definition forth_create_entry_half :: "string \ bool \ vm_state \ vm_state" where "forth_create_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm" definition forth_variable_entry_half :: "string \ bool \ vm_state \ vm_state" where "forth_variable_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm" definition forth_constant_entry_half :: "string \ bool \ vm_state \ vm_state" where "forth_constant_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm" lemma create_entry_half_populates_dictionary: assumes "\ pinned_conflict" shows "\e. dictionary (forth_create_entry_half name pinned_conflict vm) (word_id_next vm) = Some e \ de_name e = name \ de_flags e = 0" using assms by (simp add: forth_create_entry_half_def dict_insert_entry_def Let_def) lemma variable_entry_half_populates_dictionary: assumes "\ pinned_conflict" shows "\e. dictionary (forth_variable_entry_half name pinned_conflict vm) (word_id_next vm) = Some e \ de_name e = name \ de_flags e = 0" using assms by (simp add: forth_variable_entry_half_def dict_insert_entry_def Let_def) lemma constant_entry_half_populates_dictionary: assumes "\ pinned_conflict" shows "\e. dictionary (forth_constant_entry_half name pinned_conflict vm) (word_id_next vm) = Some e \ de_name e = name \ de_flags e = 0" using assms by (simp add: forth_constant_entry_half_def dict_insert_entry_def Let_def) lemma create_entry_half_pinned_conflict_errors: assumes "pinned_conflict" shows "vm_error (forth_create_entry_half name pinned_conflict vm)" using assms by (simp add: forth_create_entry_half_def dict_insert_entry_def set_error_def) lemma create_entry_half_not_full_create: True \ \Still NOT modelled beyond entry creation: `name` here is a caller- supplied parameter, not derived from `forth_parse_word` (see forth_constant_full below for that composition); also vm_align+HERE capture and the DF write of the DFA (gap b). See section header.\ by simp lemma variable_entry_half_not_full_variable: True \ \Still NOT modelled beyond entry creation: name parse (see note above), vm_align+HERE capture, vm_allot of one cell, and the DF write of that cell's address (gap b). See section header.\ by simp lemma constant_entry_half_not_full_constant: True \ \Still NOT modelled beyond entry creation: name parse (see note above -- though see forth_constant_full below, which DOES compose the parse and the value-pop guard together) and the DF write of the popped value (gap b). See section header.\ by simp (* ── CONSTANT, full composition, gap (a)+parse+DF CLOSED 2026-08-14/15 ─── CONSTANT's real C order: guard (dsp<0) -> pop value -> parse name -> vm_create_word -> DF write of the popped value. Now modelled completely -- the first fully-closed word in this file, and the flagship composition of `forth_parse_word` (TIB), `dict_insert_entry` (gap a), and `dict_write_df` (gap b), all added this session. *) definition forth_constant_full :: "nat \ bool \ vm_state \ vm_state" where "forth_constant_full max_len pinned_conflict vm = (if data_stack vm = [] then set_error vm else let value = hd (data_stack vm); vm1 = vm\data_stack := tl (data_stack vm)\; (nm, vm2) = forth_parse_word max_len vm1 in if nm = '''' then set_error vm2 else let wid = word_id_next vm2 in dict_write_df wid value (dict_insert_entry nm 0 pinned_conflict vm2))" lemma constant_full_underflow: assumes "data_stack vm = []" shows "vm_error (forth_constant_full max_len pinned_conflict vm)" by (simp add: forth_constant_full_def set_error_def assms) lemma constant_full_success_populates_dictionary: assumes "data_stack vm \ []" assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \ []" (is "?s1 \ []") assumes "max_len \ 2" assumes "\ pinned_conflict" shows "\e wid. dictionary (forth_constant_full max_len pinned_conflict vm) wid = Some e \ de_name e \ '''' \ de_flags e = 0 \ de_df e = hd (data_stack vm)" proof - let ?vm1 = "vm\data_stack := tl (data_stack vm)\" obtain nm vm2 where parse_eq: "forth_parse_word max_len ?vm1 = (nm, vm2)" by fastforce have input_pos_unaffected: "dropWhile is_ws (drop (input_pos ?vm1) (input_buffer ?vm1)) \ []" using assms(2) by simp hence nm_nonempty: "nm \ ''''" using forth_parse_word_success_nonempty[OF input_pos_unaffected assms(3)] parse_eq by (metis fstI) let ?wid = "word_id_next vm2" let ?vm3 = "dict_insert_entry nm 0 pinned_conflict vm2" have full_eq: "forth_constant_full max_len pinned_conflict vm = dict_write_df ?wid (hd (data_stack vm)) ?vm3" using assms(1) parse_eq nm_nonempty by (simp add: forth_constant_full_def) have "\e. dictionary ?vm3 ?wid = Some e \ de_name e = nm \ de_flags e = 0" using assms(4) by (simp add: dict_insert_entry_def Let_def) then obtain e where e_eq: "dictionary ?vm3 ?wid = Some e" "de_name e = nm" "de_flags e = 0" by blast have "dictionary (dict_write_df ?wid (hd (data_stack vm)) ?vm3) ?wid = Some (e\de_df := hd (data_stack vm)\)" using dict_write_df_present[OF e_eq(1)] by simp thus ?thesis using full_eq e_eq nm_nonempty by auto qed (* ── CREATE, full composition, gap (a)+parse+DF CLOSED 2026-08-15 ──────── CREATE's real C order: parse name -> vm_create_word -> vm_align(vm) -> capture dfa = here -> DF write of dfa. No stack precondition at all (unlike CONSTANT). `forth_align` (StarForth_Dictionary_Words.thy) is reused directly -- it is exactly what `vm_align` already models, word-for-word. The word_id is captured BEFORE `dict_insert_entry` advances `word_id_next`, then used to target the DF write after `forth_align` has run (align only touches `here`, never `dictionary`, so this ordering is safe regardless of which happens first). When `pinned_conflict` holds, the real C returns before ever calling vm_align; `forth_align`/`dict_write_df` running anyway on the already-errored state (a no-op for dict_write_df, since no entry exists at that word_id) is a known, minor divergence, not claimed otherwise -- see forth_colon_entry_half's identical precedent. *) definition forth_create_full :: "nat \ bool \ vm_state \ vm_state" where "forth_create_full max_len pinned_conflict vm = (let (nm, vm1) = forth_parse_word max_len vm in if nm = '''' then set_error vm1 else let wid = word_id_next vm1; vm2 = forth_align (dict_insert_entry nm 0 pinned_conflict vm1) in dict_write_df wid (word_of_nat (here vm2)) vm2)" lemma create_full_empty_parse_errors: assumes "fst (forth_parse_word max_len vm) = ''''" shows "vm_error (forth_create_full max_len pinned_conflict vm)" proof - obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce hence "nm = ''''" using assms by simp thus ?thesis using parse_eq by (simp add: forth_create_full_def set_error_def) qed lemma create_full_success_populates_dictionary: assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \ []" (is "?s1 \ []") assumes "max_len \ 2" assumes "\ pinned_conflict" shows "\e wid. dictionary (forth_create_full max_len pinned_conflict vm) wid = Some e \ de_name e \ '''' \ de_flags e = 0" proof - obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce hence nm_nonempty: "nm \ ''''" using forth_parse_word_success_nonempty[OF assms(1) assms(2)] by (metis fstI) let ?wid = "word_id_next vm1" let ?vm2 = "forth_align (dict_insert_entry nm 0 pinned_conflict vm1)" have full_eq: "forth_create_full max_len pinned_conflict vm = dict_write_df ?wid (word_of_nat (here ?vm2)) ?vm2" using parse_eq nm_nonempty by (simp add: forth_create_full_def Let_def) have dict_eq: "dictionary ?vm2 = dictionary (dict_insert_entry nm 0 pinned_conflict vm1)" by (simp add: forth_align_def set_error_def Let_def) have "\e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) ?wid = Some e \ de_name e = nm \ de_flags e = 0" using assms(3) by (simp add: dict_insert_entry_def Let_def) then obtain e where e_eq: "dictionary ?vm2 ?wid = Some e" "de_name e = nm" "de_flags e = 0" using dict_eq by auto have "dictionary (forth_create_full max_len pinned_conflict vm) ?wid = Some (e\de_df := word_of_nat (here ?vm2)\)" using full_eq dict_write_df_present[OF e_eq(1)] by simp thus ?thesis using e_eq(2) e_eq(3) nm_nonempty by fastforce qed (* ── VARIABLE, full composition, gap (a)+parse CLOSED for this word 2026-08-15 ───────────────────────────────────────────────────────────── VARIABLE's real C order: parse name -> vm_align(vm) -> capture addr = here (fed to the still-unmodelled DF write, gap b) -> vm_allot(vm, sizeof(cell_t)) [the RAW C helper, bounds-checked against DICTIONARY_MEMORY_SIZE exactly like vm_align -- NOT the FORTH word ALLOT, which pops a stack argument and checks VM_MEMORY_SIZE instead, see StarForth_Dictionary_Words.thy's forth_allot header] -> vm_create_word. `forth_vm_allot_raw` below models that raw helper; `addr` itself is not tracked since only the still-unmodelled DF write consumes it. *) definition forth_vm_allot_raw :: "nat \ vm_state \ vm_state" where "forth_vm_allot_raw bytes vm = (if here vm + bytes \ DICTIONARY_MEMORY_SIZE then set_error vm else vm\here := here vm + bytes\)" lemma vm_allot_raw_advances_here: assumes "here vm + bytes < DICTIONARY_MEMORY_SIZE" shows "here (forth_vm_allot_raw bytes vm) = here vm + bytes" using assms by (simp add: forth_vm_allot_raw_def) lemma vm_allot_raw_overflow: assumes "here vm + bytes \ DICTIONARY_MEMORY_SIZE" shows "vm_error (forth_vm_allot_raw bytes vm)" using assms by (simp add: forth_vm_allot_raw_def set_error_def) lemma vm_allot_raw_dictionary_unchanged: "dictionary (forth_vm_allot_raw bytes vm) = dictionary vm" by (simp add: forth_vm_allot_raw_def set_error_def) (* Real C order: parse -> vm_align -> capture addr=here -> vm_allot(cell) -> vm_create_word -> DF write of addr. `addr` is captured right after align, BEFORE allot advances `here` again -- gap (b) now closed too. *) definition forth_variable_full :: "nat \ bool \ vm_state \ vm_state" where "forth_variable_full max_len pinned_conflict vm = (let (nm, vm1) = forth_parse_word max_len vm in if nm = '''' then set_error vm1 else let vm2 = forth_align vm1; addr = here vm2; vm3 = forth_vm_allot_raw CELL_BYTES vm2; wid = word_id_next vm3 in dict_write_df wid (word_of_nat addr) (dict_insert_entry nm 0 pinned_conflict vm3))" lemma variable_full_empty_parse_errors: assumes "fst (forth_parse_word max_len vm) = ''''" shows "vm_error (forth_variable_full max_len pinned_conflict vm)" proof - obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce hence "nm = ''''" using assms by simp thus ?thesis using parse_eq by (simp add: forth_variable_full_def set_error_def) qed lemma variable_full_success_populates_dictionary: assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \ []" (is "?s1 \ []") assumes "max_len \ 2" assumes "\ pinned_conflict" shows "\e wid. dictionary (forth_variable_full max_len pinned_conflict vm) wid = Some e \ de_name e \ '''' \ de_flags e = 0" proof - obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce hence nm_nonempty: "nm \ ''''" using forth_parse_word_success_nonempty[OF assms(1) assms(2)] by (metis fstI) let ?vm3 = "forth_vm_allot_raw CELL_BYTES (forth_align vm1)" let ?wid = "word_id_next ?vm3" have full_eq: "forth_variable_full max_len pinned_conflict vm = dict_write_df ?wid (word_of_nat (here (forth_align vm1))) (dict_insert_entry nm 0 pinned_conflict ?vm3)" using parse_eq nm_nonempty by (simp add: forth_variable_full_def Let_def) have "\e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) ?wid = Some e \ de_name e = nm \ de_flags e = 0" using assms(3) by (simp add: dict_insert_entry_def Let_def) then obtain e where e_eq: "dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) ?wid = Some e" "de_name e = nm" "de_flags e = 0" by blast have "dictionary (forth_variable_full max_len pinned_conflict vm) ?wid = Some (e\de_df := word_of_nat (here (forth_align vm1))\)" using full_eq dict_write_df_present[OF e_eq(1)] by simp thus ?thesis using e_eq(2) e_eq(3) nm_nonempty by fastforce qed (* ── defining_runtime_create / _variable / _constant: gap (b) CLOSED 2026-08-15 ─────────────────────────────────────────────────────────── All three C bodies are byte-identical in shape (defining_words.c:91-160): guard `current_executing_entry` present, guard its DF cell present, push the DF value. One shared definition suffices; the real C's distinction is only which name gets logged, with no vm_state-visible difference. `current_executing_word_id` (StarForth_Base.thy) models `vm->current_executing_entry`; the second guard (DF cell present) is always true here since a live word_id always has an entry with a `de_df` field in this model -- included anyway via the `None` dictionary case for defensive symmetry with the C's own two-guard shape, even though it is unreachable from any real entry point in this suite. A `ds_full` check is added before the push, matching every other guarded-push word in this suite that goes through `vm_push`. *) definition forth_runtime_read_df :: "vm_state \ vm_state" where "forth_runtime_read_df vm = (case current_executing_word_id vm of None \ set_error vm | Some wid \ (case dictionary vm wid of None \ set_error vm | Some e \ if ds_full vm then set_error vm else vm\data_stack := de_df e # data_stack vm\))" lemma runtime_read_df_no_executing_entry: assumes "current_executing_word_id vm = None" shows "vm_error (forth_runtime_read_df vm)" using assms by (simp add: forth_runtime_read_df_def set_error_def) lemma runtime_read_df_pushes_value: assumes "current_executing_word_id vm = Some wid" assumes "dictionary vm wid = Some e" assumes "\ ds_full vm" shows "data_stack (forth_runtime_read_df vm) = de_df e # data_stack vm" using assms by (simp add: forth_runtime_read_df_def) lemma runtime_read_df_overflow: assumes "current_executing_word_id vm = Some wid" assumes "dictionary vm wid = Some e" assumes "ds_full vm" shows "vm_error (forth_runtime_read_df vm)" using assms by (simp add: forth_runtime_read_df_def set_error_def) lemma create_runtime_is_read_df: True \ \defining_runtime_create IS forth_runtime_read_df -- see definition above.\ by simp lemma variable_runtime_is_read_df: True \ \defining_runtime_variable IS forth_runtime_read_df -- see definition above.\ by simp lemma constant_runtime_is_read_df: True \ \defining_runtime_constant IS forth_runtime_read_df -- see definition above.\ by simp lemma lit_not_modelled: True \ \LIT: reads/advances the return-stack top as a raw C cell_t* threaded-code IP -- see file header, distinct from control_words.c's already-resolved IP-as-vaddr usage.\ by simp lemma literal_not_modelled: True \ \LITERAL: compiles a literal into threaded code via vm_compile_literal -- depends on the same unmodelled compile-target machinery as `:`/COMPILE.\ by simp lemma dodoes_not_modelled: True \ \defining_runtime_dodoes: DF/PFA layout (gap b) + runs a raw threaded-code interpreter loop over cell_t* IPs (gap c-adjacent, distinct mechanism from vm_ip).\ by simp lemma does_rt_not_modelled: True \ \defining_runtime_does_rt: patches vm->latest's DF (gap b) and reassigns its func pointer to defining_runtime_dodoes (gap c).\ by simp lemma does_greater_not_modelled: True \ \DOES>: compiles does_rt + EXIT into the defining word's body -- same unmodelled compile-target machinery as `:`.\ by simp lemma compile_not_modelled: True \ \COMPILE: vm_find_word (parse+lookup, same class as FIND, already flagged not-modelled) + vm_compile_word.\ by simp lemma bracket_compile_not_modelled: True \ \[COMPILE]: identical body to COMPILE (defining_word_bracket_compile IS defining_word_compile).\ by simp lemma forget_not_modelled: True \ \FORGET: walks vm->latest's raw linked chain by name, frees C structs, and rewinds `here` from a DF read (gap a/b combined) -- categorically the same class of gap as `block_words.c`'s cache-subsystem deferrals: a whole-subsystem project, not a one-word extension.\ by simp lemma defer_not_modelled: True \ \DEFER: vm_create_word (gap a) with a zeroed DF slot (gap b). CORRECTION (added when src/word_source/defer_words.c was later swept, see StarForth_Defer_Words.thy): word_registry.c registers defer_words.c's DEFER/IS/DEFER@ AFTER this file's (Module 27 vs 17), unconditionally in both builds -- this DEFER is dead, shadowed code, never reachable. The gap analysis below is still accurate as a description of what this dead code would hit, and the live version hits the same gaps anyway, so nothing here needed retracting.\ by simp lemma defer_runtime_not_modelled: True \ \defining_runtime_defer: reads a DictEntry* out of the DF cell (gap b) and calls through it (gap c). Also shadowed/dead -- see defer_not_modelled correction above.\ by simp lemma is_not_modelled: True \ \IS: vm_find_word (parse+lookup) + writes an XT into the target's DF cell (gap b) -- the mutable-dispatch mechanism of gap (c). Also shadowed/dead -- see defer_not_modelled correction above.\ by simp lemma defer_fetch_not_modelled: True \ \DEFER@: vm_find_word + reads the DF cell (gap b). Also shadowed/dead -- see defer_not_modelled correction above.\ by simp end