From 6f59e4f27c503e0acacf5ea69190cd3c4fe0cea6 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Sat, 15 Aug 2026 05:46:56 -0400 Subject: [PATCH] proof/: model IS and DEFER@ with the FIND-family gap sidestepped Both words' real blockers are vm_find_word (name resolution, still unmodelled everywhere in this suite) and a de->func != defer_runtime identity check (unmodellable -- word_table exposes no per-entry function identity). Sidestepped the same way physics_freeze_words.c's FREEZE-WORD/UNFREEZE-WORD/etc. already do: parameterised over an explicit target_wid_opt :: nat option (whatever vm_find_word would have resolved) and is_defer_word :: bool (the identity check's result). Given both, forth_is_full's DF write and forth_defer_fetch_full's DF read are fully modelled via dict_write_df/de_df, including IS's own real stack-underflow guard and both words' ds_full push guard. defer_runtime itself remains unmodelled -- it's a structurally different DF usage (the DF value is used as a dispatch target via word_table, gap c, not just returned to the caller like the other DF-reading words). Full suite (54 theories) verifies green. Co-Authored-By: Claude Sonnet 5 --- proof/COVERAGE.md | 21 +++-- proof/StarForth_Defer_Words.thy | 138 ++++++++++++++++++++++++++++++-- 2 files changed, 145 insertions(+), 14 deletions(-) diff --git a/proof/COVERAGE.md b/proof/COVERAGE.md index e8ebcc0..1c5dc36 100644 --- a/proof/COVERAGE.md +++ b/proof/COVERAGE.md @@ -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 full up to the DF write (added 2026-08-14/15) | +| `defer_words.c` | `StarForth_Defer_Words.thy` | live (see FINDINGS.md §3 correction); DEFER full up to the DF write, IS/DEFER@ full with FIND sidestepped, `defer_runtime` itself still gap (c) (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 | @@ -133,13 +133,18 @@ effort on the scale of what's already here: create`/`_variable`/`_constant` — byte-identical C bodies) share one new definition, `forth_runtime_read_df`, which also required adding `current_executing_word_id` to `vm_state` (mirrors `vm-> - current_executing_entry`). 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)); IS/DEFER@ (need the - FIND-family name-resolution gap first); and the pin-shadow name-scan - guard everywhere (sidestepped via an explicit `pinned_conflict :: bool` - parameter, same technique as the XT-pop gap elsewhere in this suite). + current_executing_entry`). IS/DEFER@ (`StarForth_Defer_Words.thy`) are + 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. - **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 28bca34..dfad3b9 100644 --- a/proof/StarForth_Defer_Words.thy +++ b/proof/StarForth_Defer_Words.thy @@ -60,12 +60,88 @@ lemma is_underflow: by (simp add: forth_is_guard_def set_error_def assms) lemma is_guard_rest_not_modelled: True - \ \Beyond the underflow guard: name parse (unmodelled TIB dependency), - vm_find_word (FIND-family gap), the `func != defer_runtime` identity - check (unmodellable -- word_table has no per-entry function-identity - query in this model), and the DF store (gap b). See file header.\ + \ \Superseded by forth_is_full below (name parse and DF store are now + modelled; only the FIND lookup and identity check are sidestepped, + not left as a blank "not modelled"). Kept for its accurate + description of the OLD state, not deleted.\ by simp +(* ── IS, full composition (FIND sidestepped), gap (a)+(b) CLOSED where + reachable, 2026-08-15 ─────────────────────────────────────────────────── + `word_is` (defer_words.c:112-154): underflow guard -> pop xt -> parse + name -> vm_find_word -> `de->func != defer_runtime` identity check -> + DF store. `vm_find_word` and the identity check are both unmodellable + in this suite (FIND-family name-resolution gap; `word_table` exposes + no per-entry function-identity query) -- sidestepped the same way + `physics_freeze_words.c`'s FREEZE-WORD/UNFREEZE-WORD/etc. already + sidestep the identical shape: parameterised over an explicit + `target_wid_opt :: nat option` (standing in for whatever vm_find_word + would have resolved) and `is_defer_word :: bool` (standing in for the + identity check's result). Given both, the DF store itself is fully + modelled via `dict_write_df`. *) + +definition forth_is_full :: "nat \ nat option \ bool \ vm_state \ vm_state" where + "forth_is_full max_len target_wid_opt is_defer_word vm = + (if data_stack vm = [] + then set_error vm + else + let xt = 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 case target_wid_opt of + None \ set_error vm2 + | Some wid \ + if \ is_defer_word + then set_error vm2 + else dict_write_df wid xt vm2)" + +lemma is_full_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)" + by (simp add: forth_is_full_def set_error_def assms) + +lemma is_full_not_found_errors: + assumes "data_stack vm \ []" + assumes "fst (forth_parse_word max_len (vm\data_stack := tl (data_stack vm)\)) \ ''''" + assumes "target_wid_opt = None" + shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)" +proof - + obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\data_stack := tl (data_stack vm)\) = (nm, vm2)" + by fastforce + hence "nm \ ''''" using assms(2) by simp + thus ?thesis using assms(1) assms(3) parse_eq by (simp add: forth_is_full_def set_error_def) +qed + +lemma is_full_not_defer_word_errors: + assumes "data_stack vm \ []" + assumes "fst (forth_parse_word max_len (vm\data_stack := tl (data_stack vm)\)) \ ''''" + assumes "target_wid_opt = Some wid" "\ is_defer_word" + shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)" +proof - + obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\data_stack := tl (data_stack vm)\) = (nm, vm2)" + by fastforce + hence "nm \ ''''" using assms(2) by simp + thus ?thesis using assms(1) assms(3) assms(4) parse_eq by (simp add: forth_is_full_def set_error_def) +qed + +lemma is_full_success_writes_df: + assumes "data_stack vm \ []" + assumes "fst (forth_parse_word max_len (vm\data_stack := tl (data_stack vm)\)) \ ''''" + assumes "target_wid_opt = Some wid" "is_defer_word" + assumes "dictionary (snd (forth_parse_word max_len (vm\data_stack := tl (data_stack vm)\))) wid = Some e" + shows "dictionary (forth_is_full max_len target_wid_opt is_defer_word vm) wid = Some (e\de_df := hd (data_stack vm)\)" +proof - + obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\data_stack := tl (data_stack vm)\) = (nm, vm2)" + by fastforce + hence "nm \ ''''" using assms(2) by simp + moreover have "dictionary vm2 wid = Some e" using assms(5) parse_eq by simp + ultimately show ?thesis + using assms(1) assms(3) assms(4) parse_eq dict_write_df_present + by (simp add: forth_is_full_def) +qed + (* ── 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 @@ -129,9 +205,59 @@ proof - 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).\ +lemma defer_runtime_not_modelled: True \ \defer_runtime: DF read (gap b) + call-through (gap c) -- structurally different from forth_runtime_read_df, since the DF value here is USED as a dispatch target, not just returned. Genuinely still not modelled, not superseded.\ by simp -lemma defer_fetch_not_modelled: True \ \DEFER@: FIND (name-resolution gap) + DF read (gap b).\ +lemma defer_fetch_not_modelled: True \ \Superseded by forth_defer_fetch_full below, same as is_guard_rest_not_modelled above.\ by simp +(* ── DEFER@, full composition (FIND sidestepped), gap (a)+(b) CLOSED where + reachable, 2026-08-15 ─────────────────────────────────────────────────── + `word_defer_fetch` (defer_words.c:161-198): parse name -> vm_find_word + -> identity check -> DF read + push. Same sidestep as forth_is_full; + the DF read itself is fully modelled via `de_df`, with the same + `ds_full` guard `forth_runtime_read_df` already established for the + equivalent vm_push() call. *) + +definition forth_defer_fetch_full :: "nat \ nat option \ bool \ vm_state \ vm_state" where + "forth_defer_fetch_full max_len target_wid_opt is_defer_word vm = + (let (nm, vm1) = forth_parse_word max_len vm + in if nm = '''' + then set_error vm1 + else case target_wid_opt of + None \ set_error vm1 + | Some wid \ + if \ is_defer_word + then set_error vm1 + else case dictionary vm1 wid of + None \ set_error vm1 + | Some e \ + if ds_full vm1 + then set_error vm1 + else vm1\data_stack := de_df e # data_stack vm1\)" + +lemma defer_fetch_full_empty_parse_errors: + assumes "fst (forth_parse_word max_len vm) = ''''" + shows "vm_error (forth_defer_fetch_full max_len target_wid_opt is_defer_word 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_fetch_full_def set_error_def) +qed + +lemma defer_fetch_full_success_pushes_df: + assumes "fst (forth_parse_word max_len vm) \ ''''" + assumes "target_wid_opt = Some wid" "is_defer_word" + assumes "dictionary (snd (forth_parse_word max_len vm)) wid = Some e" + assumes "\ ds_full (snd (forth_parse_word max_len vm))" + shows "data_stack (forth_defer_fetch_full max_len target_wid_opt is_defer_word vm) + = de_df e # data_stack (snd (forth_parse_word max_len vm))" +proof - + obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce + hence nm_nonempty: "nm \ ''''" using assms(1) by simp + have "dictionary vm1 wid = Some e" using assms(4) parse_eq by simp + thus ?thesis + using parse_eq nm_nonempty assms(2) assms(3) assms(5) + by (simp add: forth_defer_fetch_full_def) +qed + end