From 4d025ab0f4e4a1f9505f889b5ac3388c492e38d3 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 14:33:29 -0400 Subject: [PATCH] proof/: add StarForth_Defining_Words.thy (defining_words.c coverage) 4 of 19 words fully modelled ([, ], STATE, IMMEDIATE), 2 guard-only partial (:, ;), rest deferred behind three named model gaps: dictionary- entry creation (never modelled anywhere in this suite before now), data-field addressing (same class as the existing >BODY gap), and mutable per-entry dispatch (word_table is a fixed global, can't express DEFER/IS). Finding: defining_words.c's [/]/STATE are registered after (and thus permanently shadow) dictionary_manipulation_words.c's versions of the same names -- that file's prior "dead cross-VM-shared static" finding only ever applied to the shadowed, unreachable code. The live versions correctly use vm->state_addr, a real per-VM field, now added to vm_state. --- proof/ROOT | 1 + proof/StarForth_Base.thy | 9 + proof/StarForth_Defining_Words.thy | 336 +++++++++++++++++++++++++++++ 3 files changed, 346 insertions(+) create mode 100644 proof/StarForth_Defining_Words.thy diff --git a/proof/ROOT b/proof/ROOT index d2859b1..6583b69 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -12,6 +12,7 @@ session "StarForth" = "HOL-Library" + StarForth_Memory_Words StarForth_Dictionary_Words StarForth_Dictionary_Manipulation_Words + StarForth_Defining_Words StarForth_Control_Words StarForth_String_Words StarForth_Block_Words diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 0e8b838..28b401d 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -531,6 +531,15 @@ record vm_state = base_addr :: nat hold_addr :: nat hold_pos :: nat + (* ○ CODE-MUST-MATCH: C: vaddr_t state_addr (include/vm.h:452) -- VM + address of the cell holding STATE (0=interp, -1=compile). Distinct from + `state_var` (above), which is the host-side mirror cell_t field. Added + for StarForth_Defining_Words.thy's `[`/`]`/STATE -- these are the LIVE, + reachable implementations (defining_words.c registers over + dictionary_manipulation_words.c's `[`/`]`/STATE, which are dead code + once shadowed; see that file for the shadowed versions and this file + for the correction). *) + state_addr :: nat (* ── Physics Loop #1: Execution heat tracking ───────────────────────── *) (* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct. diff --git a/proof/StarForth_Defining_Words.thy b/proof/StarForth_Defining_Words.thy new file mode 100644 index 0000000..f35db03 --- /dev/null +++ b/proof/StarForth_Defining_Words.thy @@ -0,0 +1,336 @@ +theory StarForth_Defining_Words + imports StarForth_Base StarForth_Memory_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`/`INTERPRET` are permanently shadowed, dead code from the + moment boot registration completes. + + 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 `]`), but + the dictionary-entry-creation half (`vm_create_word` -> a fresh + DictEntry with `vm->compiling_word` tracking it) is NOT modelled -- + see the finding below. `;`'s entire effect beyond the guard + (`vm_exit_compile_mode`: find/compile EXIT, clear WORD_SMUDGED, set + WORD_COMPILED, evict hot-words cache) is 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, FORGET, COMPILE, + [COMPILE], LIT, LITERAL, does_rt, DOES>, DEFER, IS, DEFER@, and the + three defining-runtime functions CREATE/VARIABLE/CONSTANT install) -- + 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 is not modelled anywhere in this proof + suite. `dictionary :: nat \ dict_entry option` (StarForth_ + Base.thy:498) is 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 is the first file in + the sweep whose primary job IS insertion (`:`, CREATE, VARIABLE, + CONSTANT, DEFER all call `vm_create_word`). `vm_create_word` + itself parses no input (name arrives pre-parsed) but allocates a + new DictEntry, links it into `vm->latest`, and returns a raw + `DictEntry*` the caller mutates directly (`entry->flags |= + WORD_SMUDGED`, etc.) -- none of which has a counterpart in the + word_id-indexed abstract model with no live pointer aliasing. + This is a materially bigger gap than the raw-pointer-navigation + gap already flagged in dictionary_manipulation_words.c (which + only reads), and is the single largest finding of this file. + + (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" + +(* ── [ ( -- ) : 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 + +(* ── ; ( -- ) : 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 + +(* ── Everything else in this file -- NOT MODELLED ───────────────────────── + See file header findings (a) dictionary-entry creation, (b) data-field + addressing, (c) mutable per-entry dispatch. One sentinel lemma per word/ + helper, matching the StarForth_Dictionary_Manipulation_Words.thy + convention. *) + +lemma create_not_modelled: True \ \CREATE: vm_create_word (gap a) + DF write of captured DFA (gap b).\ + by simp +lemma variable_not_modelled: True \ \VARIABLE: vm_allot + vm_create_word (gap a) + DF write of the cell's address (gap b).\ + by simp +lemma constant_not_modelled: True \ \CONSTANT: vm_create_word (gap a) + DF write of the popped value (gap b).\ + by simp +lemma create_runtime_not_modelled: True \ \defining_runtime_create: reads current_executing_entry's DF cell (gap b).\ + by simp +lemma variable_runtime_not_modelled: True \ \defining_runtime_variable: reads current_executing_entry's DF cell (gap b).\ + by simp +lemma constant_runtime_not_modelled: True \ \defining_runtime_constant: reads current_executing_entry's DF cell (gap b).\ + 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).\ + 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).\ + 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).\ + by simp +lemma defer_fetch_not_modelled: True \ \DEFER@: vm_find_word + reads the DF cell (gap b).\ + by simp + +end