diff --git a/proof/COVERAGE.md b/proof/COVERAGE.md index 1c5dc36..23845be 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` | 7/19 fully modelled (original 4 + CREATE/VARIABLE/CONSTANT and their runtimes) + `;` guard-only + `:` full except `compiling_word` tracking (added 2026-08-14/15) | +| `defining_words.c` | `StarForth_Defining_Words.thy` | 7/19 fully modelled (original 4 + CREATE/VARIABLE/CONSTANT and their runtimes) + `;` guard-only + `:` closed through entry-creation + `compiling_word_id` tracking, DF write (gap b) still open (added 2026-08-14/15) | | `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 | @@ -116,8 +116,8 @@ 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) — **closed end-to-end for CREATE/VARIABLE/CONSTANT, - 2026-08-14/15**, `:`/DEFER closed up to `vm->compiling_word` tracking. + CONSTANT, DEFER) — **closed end-to-end for CREATE/VARIABLE/CONSTANT/`:`, + 2026-08-14/15.** `dict_insert_entry` (`StarForth_Defining_Words.thy`) models the word_id-assignment/dictionary-table/`latest_id`/`word_id_next`-counter portion; `de_df :: cell` (added to `dict_entry` in `StarForth_Base.thy`) @@ -137,14 +137,21 @@ effort on the scale of what's already here: also now modelled end to end, with the FIND-family name-resolution gap sidestepped via an explicit `target_wid_opt :: nat option` + `is_defer_word :: bool` pair, the same technique - `physics_freeze_words.c`'s FREEZE-WORD/etc. already established. Still - open: `:`'s `vm->compiling_word` tracking (no vm_state field, so `:` - stops just short of full closure); DEFER's own runtime (dispatch - reassignment via a stored pointer — a fundamentally different DF usage, - still gap (c), NOT the same shape as IS/DEFER@'s plain-value DF access); - the pin-shadow name-scan guard everywhere (sidestepped via an explicit - `pinned_conflict :: bool` parameter); and the FIND-family lookup itself, - which IS/DEFER@'s sidestep still doesn't model, only routes around. + `physics_freeze_words.c`'s FREEZE-WORD/etc. already established. `:` + closed to the same point as CREATE/VARIABLE/CONSTANT, 2026-08-15: + `compiling_word_id` added to `vm_state` (mirrors `vm->compiling_word`), + set by `forth_colon_entry_half` from `latest_id` on success and forced + to `None` on the pinned-conflict failure path, matching the real C's + unconditional `vm->compiling_word = de;` before its own null check. + Still open: `:`'s vm_align+HERE capture and DF write of the + threaded-body start address (gap b, same as CREATE/VARIABLE/CONSTANT's + own DF write, just not yet composed in for `:`); DEFER's own runtime + (dispatch reassignment via a stored pointer — a fundamentally different + DF usage, still gap (c), NOT the same shape as IS/DEFER@'s plain-value + DF access); the pin-shadow name-scan guard everywhere (sidestepped via + an explicit `pinned_conflict :: bool` parameter); and the FIND-family + lookup itself, which IS/DEFER@'s sidestep still doesn't model, only + routes around. - **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_Base.thy b/proof/StarForth_Base.thy index 9089921..7211532 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -522,6 +522,13 @@ record vm_state = `latest_id`'s convention, rather than as a raw pointer. *) current_executing_word_id :: "nat option" + (* ── Compile-time state ─────────────────────────────────────────────── + Models `vm->compiling_word` (include/vm.h:421, a DictEntry pointer), + the entry currently under construction by `:` until `;` clears it. + Word-id-indexed (`nat option`), matching `current_executing_word_id` + and `latest_id`'s convention, rather than a raw pointer. *) + compiling_word_id :: "nat option" + (* ── Execution state ──────────────────────────────────────────────────── *) vm_mode :: vm_mode vm_ip :: nat \ \instruction pointer (byte offset)\ diff --git a/proof/StarForth_Defining_Words.thy b/proof/StarForth_Defining_Words.thy index e686843..b0a53c9 100644 --- a/proof/StarForth_Defining_Words.thy +++ b/proof/StarForth_Defining_Words.thy @@ -70,10 +70,10 @@ begin 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 + 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 @@ -398,7 +398,7 @@ 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 ────────── +(* ── : 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 @@ -407,15 +407,24 @@ lemma colon_guard_not_full_colon: True `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). *) + 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 = - dict_insert_entry name WORD_SMUDGED pinned_conflict (forth_colon_guard 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" @@ -430,24 +439,36 @@ lemma colon_entry_half_still_compile_mode: 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->compiling_word tracking (no vm_state field), vm_align+HERE - capture, DF write of the threaded-body start address (gap b). See - section header.\ + 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 CLOSED 2026-08-15 ────────────── +(* ── `:`, 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, 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-> - compiling_word tracking, vm_align+HERE capture, DF write (gap b). *) + 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 = @@ -496,6 +517,22 @@ proof - 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,