diff --git a/proof/COVERAGE.md b/proof/COVERAGE.md index 9f32bb8..a9df1e6 100644 --- a/proof/COVERAGE.md +++ b/proof/COVERAGE.md @@ -70,7 +70,7 @@ library itself is separately covered by `StarForth_Q48_16.thy`). | `format_words.c` | `StarForth_Format_Words.thy` | 17/19 (`#`/`#S` multi-precision division deferred) | | `system_words.c` | `StarForth_System_Words.thy` | 10/16 + `(ABORT")` helper | | `vocabulary_words.c` | `StarForth_Vocabulary_Words.thy` | 1/7 partial (entire subsystem is file-scope statics, see FINDINGS.md §1) | -| `defining_words.c` | `StarForth_Defining_Words.thy` | 4/19 full + 2 guard-only (`:`/`;`) | +| `defining_words.c` | `StarForth_Defining_Words.thy` | 4/19 full + 2 guard-only (`:`/`;`) + 4 entry-creation-half (`:`/CREATE/VARIABLE/CONSTANT, added 2026-08-14) | | `acl_words.c` | `StarForth_ACL_Words.thy` | 7/12 (5 already covered by the pre-existing `ACL_*.thy` policy theories) | | `dictionary_heat_diagnostic_words.c` | `StarForth_Dictionary_Heat_Diagnostic_Words.thy` | 4/6 full + 1 partial | | `physics_freeze_words.c` | `StarForth_Physics_Freeze_Words.thy` | 6/9 | @@ -81,7 +81,7 @@ library itself is separately covered by `StarForth_Q48_16.thy`). | `framebuffer_words.c`, `keyboard_words.c` | `StarForth_Framebuffer_Words.thy`, `StarForth_Keyboard_Words.thy` | hosted-build fallback branches fully modelled | | `scroll_words.c`, `ttf_words.c` | `StarForth_Scroll_Words.thy`, `StarForth_TTF_Words.thy` | sentinel-only — words don't exist on hosted builds at all | | `lifecycle_words_hosted.c` | `StarForth_Lifecycle_Words_Hosted.thy` | 100% — zero deferred remainder | -| `defer_words.c` | `StarForth_Defer_Words.thy` | modelled, but words are dead (shadowed, see FINDINGS.md §3) | +| `defer_words.c` | `StarForth_Defer_Words.thy` | live (see FINDINGS.md §3 correction); DEFER's entry-creation half modelled (added 2026-08-14) | | `log_words.c` | `StarForth_Log_Words.thy` | 100% | | `q48_words.c` | `StarForth_Q48_Words.thy` | 17/23 | | `inference_words.c` | `StarForth_Inference_Words.thy` | 5 accessors full; rest guard/shape | @@ -103,8 +103,16 @@ effort on the scale of what's already here: the abstract `dict_entry` model is word-id-indexed, not addressed; no independent `dsp` register exists to model `SP@`/`SP!` against either. - **Dictionary insertion** (`vm_create_word`, used by `:`, CREATE, VARIABLE, - CONSTANT, DEFER) — every other file only ever *reads* the abstract - dictionary table; no insertion operation has ever been modelled. + CONSTANT, DEFER) — **partially closed 2026-08-14.** `dict_insert_entry` + (`StarForth_Defining_Words.thy`) now models the word_id-assignment/ + dictionary-table/`latest_id`/`word_id_next`-counter portion, reused by + all five words' `forth_*_entry_half` definitions. Still not modelled: + the name parse (TIB gap, same as everywhere else in this suite), + `vm->compiling_word` tracking (no vm_state field), the data-field (DF) + write each of the five words does afterward (still gap (b) below), and + the pin-shadow name-scan guard (sidestepped via an explicit + `pinned_conflict :: bool` parameter, same technique as the XT-pop gap + elsewhere in this suite). - **The vocabulary chain mechanics** (VOCABULARY/DEFINITIONS/CONTEXT/CURRENT/ FORTH) — file-scope statics, see FINDINGS.md §1, instance #5. - **The hot-words cache** (`physics_benchmark_words.c`) and **the bucket/ diff --git a/proof/StarForth_Defer_Words.thy b/proof/StarForth_Defer_Words.thy index 727b484..dcaac88 100644 --- a/proof/StarForth_Defer_Words.thy +++ b/proof/StarForth_Defer_Words.thy @@ -1,5 +1,5 @@ theory StarForth_Defer_Words - imports StarForth_Base + imports StarForth_Base StarForth_Defining_Words begin (* ========================================================================= @@ -66,7 +66,28 @@ lemma is_guard_rest_not_modelled: True query in this model), and the DF store (gap b). See file header.\ by simp -lemma defer_not_modelled: True \ \DEFER: vm_create_word (gap a) + DF zero-init (gap b).\ +(* ── DEFER: entry-creation half, gap (a) PARTIALLY CLOSED 2026-08-14 ───── + `word_defer` (src/word_source/defer_words.c:73-101) calls + `vm_create_word(vm, name, len, defer_runtime)` with no extra flags set + afterward -- same shape as StarForth_Defining_Words.thy's CREATE/ + VARIABLE/CONSTANT, reusing `dict_insert_entry 0` directly. NOT modelled: + the name parse (TIB gap), and the DF zero-init that follows (gap b). *) + +definition forth_defer_entry_half :: "bool \ vm_state \ vm_state" where + "forth_defer_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" + +lemma defer_entry_half_populates_dictionary: + assumes "\ pinned_conflict" + shows "\e. dictionary (forth_defer_entry_half pinned_conflict vm) (word_id_next vm) = Some e + \ de_flags e = 0" + using assms by (simp add: forth_defer_entry_half_def dict_insert_entry_def Let_def) + +lemma defer_entry_half_pinned_conflict_errors: + assumes "pinned_conflict" + shows "vm_error (forth_defer_entry_half pinned_conflict vm)" + using assms by (simp add: forth_defer_entry_half_def dict_insert_entry_def set_error_def) + +lemma defer_not_modelled: True \ \DEFER beyond the entry-creation half: name parse (TIB gap) + DF zero-init (gap b). See forth_defer_entry_half above for what IS now modelled.\ by simp lemma defer_runtime_not_modelled: True \ \defer_runtime: DF read (gap b) + call-through (gap c).\ by simp diff --git a/proof/StarForth_Defining_Words.thy b/proof/StarForth_Defining_Words.thy index 58d9240..11ebedd 100644 --- a/proof/StarForth_Defining_Words.thy +++ b/proof/StarForth_Defining_Words.thy @@ -1,5 +1,5 @@ theory StarForth_Defining_Words - imports StarForth_Base StarForth_Memory_Words + imports StarForth_Base StarForth_Memory_Words ACL_Pin_Monotone begin (* ========================================================================= @@ -38,35 +38,47 @@ begin 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: + 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 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. + (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), does not capture the entry into any per-VM + `vm->compiling_word`-style tracking field (none exists in + vm_state), 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 @@ -97,6 +109,88 @@ begin ======================================================================== *) 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 :: "nat \ bool \ vm_state \ vm_state" where + "dict_insert_entry init_flags pinned_conflict vm = + (if pinned_conflict + then set_error vm + else + let wid = word_id_next vm; + e = \de_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\ + 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 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 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 init_flags pinned_conflict vm) (word_id_next vm) = Some e + \ de_word_id e = word_id_next vm \ 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" + 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 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 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 (* ── [ ( -- ) : interpret mode, LIVE version (see file header) ──────────── *) (* C: vm_store_cell(vm, vm->state_addr, 0); vm->mode = MODE_INTERPRET. *) @@ -273,6 +367,44 @@ lemma colon_guard_not_full_colon: True file header finding (a)/(b). Named so the omission is greppable.\ by simp +(* ── : entry-creation half, gap (a) PARTIALLY CLOSED 2026-08-14 ────────── + `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). Still + NOT modelled beyond this: name parse, `vm->compiling_word` tracking + (no vm_state counterpart -- would need a new field, not attempted + here), vm_align+HERE capture, and the DF write of the threaded-body + start address (gap b). *) + +definition forth_colon_entry_half :: "bool \ vm_state \ vm_state" where + "forth_colon_entry_half pinned_conflict vm = + dict_insert_entry WORD_SMUDGED pinned_conflict (forth_colon_guard vm)" + +lemma colon_entry_half_requires_guard_to_pass: + assumes "vm_mode vm \ ModeCompile" "\ pinned_conflict" + shows "\e. dictionary (forth_colon_entry_half pinned_conflict vm) (word_id_next (forth_colon_guard vm)) = Some e + \ 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 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_not_full_colon: True + \ \Still NOT modelled: name parse, vm->compiling_word tracking (no + vm_state field), vm_align+HERE capture, DF write of the threaded-body + start address (gap b). See section header.\ + 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, @@ -295,18 +427,70 @@ lemma semicolon_guard_not_full_semicolon: True 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. *) +(* ── 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 `:`. *) -lemma create_not_modelled: True \ \CREATE: vm_create_word (gap a) + DF write of captured DFA (gap b).\ +definition forth_create_entry_half :: "bool \ vm_state \ vm_state" where + "forth_create_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" + +definition forth_variable_entry_half :: "bool \ vm_state \ vm_state" where + "forth_variable_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" + +definition forth_constant_entry_half :: "bool \ vm_state \ vm_state" where + "forth_constant_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" + +lemma create_entry_half_populates_dictionary: + assumes "\ pinned_conflict" + shows "\e. dictionary (forth_create_entry_half pinned_conflict vm) (word_id_next vm) = Some e + \ 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 pinned_conflict vm) (word_id_next vm) = Some e + \ 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 pinned_conflict vm) (word_id_next vm) = Some e + \ 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 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 parse, vm_align+HERE + capture, and the DF write of the DFA (gap b). See section header.\ by simp -lemma variable_not_modelled: True \ \VARIABLE: vm_allot + vm_create_word (gap a) + DF write of the cell's address (gap b).\ +lemma variable_entry_half_not_full_variable: True + \ \Still NOT modelled beyond entry creation: name parse, 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_not_modelled: True \ \CONSTANT: vm_create_word (gap a) + DF write of the popped value (gap b).\ +lemma constant_entry_half_not_full_constant: True + \ \Still NOT modelled beyond entry creation: name parse, the value pop + (this word's one real vm_state-only guard, `vm->dsp < 0`, is itself + also unmodelled here since it gates the parse that must happen + before vm_create_word), and the DF write of the popped value + (gap b). See section header.\ 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).\