diff --git a/proof/COVERAGE.md b/proof/COVERAGE.md index 4f5f381..93d0f29 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 (`:`/`;`) + 4 entry-creation-half (`:`/CREATE/VARIABLE/CONSTANT, added 2026-08-14) | +| `defining_words.c` | `StarForth_Defining_Words.thy` | 4/19 full + `;` guard-only + `:`/CREATE/VARIABLE/CONSTANT full up to the DF write (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 | @@ -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` | live (see FINDINGS.md §3 correction); DEFER's entry-creation half modelled (added 2026-08-14) | +| `defer_words.c` | `StarForth_Defer_Words.thy` | live (see FINDINGS.md §3 correction); DEFER full up to the DF write (added 2026-08-14/15) | | `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 | @@ -95,34 +95,37 @@ effort on the scale of what's already here: - **The disk-backed block-window cache** (`block_subsystem.h` + `blk_vm_lbn`/`blk_vm_cbuf`/`blk_vm_dirty`/`blk_vm_next`) — blocks `block_words.c` and `editor_words.c` almost entirely. -- **The TIB / interactive input subsystem — partially closed 2026-08-14.** +- **The TIB / interactive input subsystem — partially closed 2026-08-14/15.** `input_buffer`/`input_length`/`input_pos` turned out to be plain per-VM array/scalar fields, not host pointers, and `vm_parse_word` (the whitespace-delimited name-parse every CREATE/VARIABLE/CONSTANT/`:`/ DEFER-family word depends on) is a pure scan — now modelled as - `forth_parse_word` in `StarForth_Base.thy`, composed with - `dict_insert_entry` for CONSTANT in `StarForth_Defining_Words.thy` as a - worked example. Still blocked: words needing a *different* scan shape - over the same buffer — `(`/`\` comment (skip-to-delimiter, not - whitespace-delimited), `KEY` (single raw character, not a parsed - token), `."`/`S"` (delimiter-terminated string literal), `ABORT"`'s - compile-time half, `SEE` (raw pointer walk) — each would need its own - scan function modelled against the same fields, not automatically - unlocked by `forth_parse_word`. + `forth_parse_word` in `StarForth_Base.thy`, composed end-to-end with + `dict_insert_entry` for all five name-parsing/entry-creating words + (`forth_colon_full`/`forth_create_full`/`forth_variable_full`/ + `forth_constant_full`/`forth_defer_full`). Still blocked: words needing + a *different* scan shape over the same buffer — `(`/`\` comment + (skip-to-delimiter, not whitespace-delimited), `KEY` (single raw + character, not a parsed token), `."`/`S"` (delimiter-terminated string + literal), `ABORT"`'s compile-time half, `SEE` (raw pointer walk) — each + would need its own scan function modelled against the same fields, not + automatically unlocked by `forth_parse_word`. - **Real stdio/file I/O** — `SAVE-SYSTEM`, parts of `string_words.c`. - **Raw C-string/strtol-backed words** — the rest of `string_words.c`. - **Raw-pointer DictEntry navigation** (`>BODY`/`>NAME`/CFA-style words) — 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) — **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, which take the parsed - name as a caller-supplied parameter. `forth_constant_full` composes - `forth_parse_word` (the TIB gap above) in directly for CONSTANT, as a - worked example not yet repeated for the other four. Still not modelled - for any of the five: `vm->compiling_word` tracking (no vm_state field), + CONSTANT, DEFER) — **partially closed 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. All five + words now have a `forth_*_full` definition composing the real parse, + any word-specific guard (CONSTANT's stack-underflow check, `:`'s + nested-definition check), any align/allot step (CREATE's `vm_align`, + VARIABLE's `vm_align` + a new `forth_vm_allot_raw` modelling the raw + `vm_allot` C helper), and the entry insertion itself, all the way up + to — but not including — the data-field write. Still not modelled for + any of the five: `vm->compiling_word` tracking (no vm_state field), the data-field (DF) write each word 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 diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 5a88792..838ad09 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -730,6 +730,18 @@ lemma forth_parse_word_preserves_data_stack: "data_stack (snd (forth_parse_word max_len vm)) = data_stack vm" by (simp add: forth_parse_word_def Let_def) +lemma forth_parse_word_preserves_vm_mode: + "vm_mode (snd (forth_parse_word max_len vm)) = vm_mode vm" + by (simp add: forth_parse_word_def Let_def) + +lemma forth_parse_word_preserves_dictionary: + "dictionary (snd (forth_parse_word max_len vm)) = dictionary vm" + by (simp add: forth_parse_word_def Let_def) + +lemma forth_parse_word_preserves_word_id_next: + "word_id_next (snd (forth_parse_word max_len vm)) = word_id_next vm" + by (simp add: forth_parse_word_def Let_def) + lemma forth_parse_word_never_sets_error: True \ \vm_parse_word's own C body never touches vm->error -- callers check the returned length themselves and set it. Faithfully NOT set here diff --git a/proof/StarForth_Defer_Words.thy b/proof/StarForth_Defer_Words.thy index 094dd16..28bca34 100644 --- a/proof/StarForth_Defer_Words.thy +++ b/proof/StarForth_Defer_Words.thy @@ -87,8 +87,48 @@ lemma defer_entry_half_pinned_conflict_errors: shows "vm_error (forth_defer_entry_half name 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.\ +lemma defer_not_modelled: True \ \DEFER beyond the entry-creation half: DF zero-init (gap b). See forth_defer_full below for the parse composition.\ by simp + +(* ── DEFER, full composition, gap (a)+parse CLOSED 2026-08-15 ──────────── + `word_defer` (defer_words.c:73-101): parse name -> vm_create_word. No + align/allot, no stack guard -- the simplest full composition in this + suite. Same pattern as StarForth_Defining_Words.thy's forth_create_full/ + forth_constant_full/forth_variable_full. *) + +definition forth_defer_full :: "nat \ bool \ vm_state \ vm_state" where + "forth_defer_full max_len pinned_conflict vm = + (let (nm, vm1) = forth_parse_word max_len vm + in if nm = '''' + then set_error vm1 + else dict_insert_entry nm 0 pinned_conflict vm1)" + +lemma defer_full_empty_parse_errors: + assumes "fst (forth_parse_word max_len vm) = ''''" + shows "vm_error (forth_defer_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_defer_full_def set_error_def) +qed + +lemma defer_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_defer_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) + have "forth_defer_full max_len pinned_conflict vm = dict_insert_entry nm 0 pinned_conflict vm1" + using parse_eq nm_nonempty by (simp add: forth_defer_full_def) + moreover have "\e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) (word_id_next vm1) = Some e + \ de_name e = nm \ de_flags e = 0" + using assms(3) by (simp add: dict_insert_entry_def Let_def) + ultimately show ?thesis using nm_nonempty by auto +qed lemma defer_runtime_not_modelled: True \ \defer_runtime: DF read (gap b) + call-through (gap c).\ by simp lemma defer_fetch_not_modelled: True \ \DEFER@: FIND (name-resolution gap) + DF read (gap b).\ diff --git a/proof/StarForth_Defining_Words.thy b/proof/StarForth_Defining_Words.thy index b38b6cd..2b66f9d 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 ACL_Pin_Monotone + imports StarForth_Base StarForth_Memory_Words ACL_Pin_Monotone StarForth_Dictionary_Words begin (* ========================================================================= @@ -402,13 +402,70 @@ lemma colon_entry_half_still_compile_mode: 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_constant_full - below for the one word in this file where parse IS composed in), - vm->compiling_word tracking (no vm_state field), vm_align+HERE + 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.\ by simp +(* ── `:`, full composition, gap (a)+parse 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). *) + +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 + (* ── ; ( -- ) : 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, @@ -550,6 +607,125 @@ proof - ultimately show ?thesis using nm_nonempty by auto qed +(* ── CREATE, full composition, gap (a)+parse CLOSED for this word + 2026-08-15 ───────────────────────────────────────────────────────────── + CREATE's real C order: parse name -> vm_create_word -> vm_align(vm) -> + capture dfa = here (fed to the still-unmodelled DF write, gap b). 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. Composed unconditionally + over `dict_insert_entry`'s result the same way `forth_colon_entry_half` + already does: when `pinned_conflict` holds, the real C returns before + ever calling vm_align, so `forth_align` running anyway on the + already-errored state 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 forth_align (dict_insert_entry nm 0 pinned_conflict vm1))" + +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) + have "forth_create_full max_len pinned_conflict vm + = forth_align (dict_insert_entry nm 0 pinned_conflict vm1)" + using parse_eq nm_nonempty by (simp add: forth_create_full_def) + moreover have "\e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) (word_id_next vm1) = Some e + \ de_name e = nm \ de_flags e = 0" + using assms(3) by (simp add: dict_insert_entry_def Let_def) + moreover have "dictionary (forth_align vm2) = dictionary vm2" for vm2 + by (simp add: forth_align_def set_error_def Let_def) + ultimately show ?thesis using nm_nonempty by metis +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) + +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 dict_insert_entry nm 0 pinned_conflict + (forth_vm_allot_raw CELL_BYTES (forth_align vm1)))" + +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)" + have "forth_variable_full max_len pinned_conflict vm + = dict_insert_entry nm 0 pinned_conflict ?vm3" + using parse_eq nm_nonempty by (simp add: forth_variable_full_def) + moreover have "\e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) (word_id_next ?vm3) = Some e + \ de_name e = nm \ de_flags e = 0" + using assms(3) by (simp add: dict_insert_entry_def Let_def) + ultimately show ?thesis using nm_nonempty by auto +qed + 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).\