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 <noreply@anthropic.com>

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`
+  current_executing_entry`). IS/DEFER@ (`StarForth_Defer_Words.thy`) are
-  tracking (no vm_state field, so `:` stops just short of full closure);
+  also now modelled end to end, with the FIND-family name-resolution gap
-  DEFER's own runtime (dispatch reassignment via a stored pointer — a
+  sidestepped via an explicit `target_wid_opt :: nat option` +
-  fundamentally different DF usage, still gap (c)); IS/DEFER@ (need the
+  `is_defer_word :: bool` pair, the same technique
-  FIND-family name-resolution gap first); and the pin-shadow name-scan
+  `physics_freeze_words.c`'s FREEZE-WORD/etc. already established. Still
-  guard everywhere (sidestepped via an explicit `pinned_conflict :: bool`
+  open: `:`'s `vm->compiling_word` tracking (no vm_state field, so `:`
-  parameter, same technique as the XT-pop gap elsewhere in this suite).
+  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/

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
-  \<comment> \<open>Beyond the underflow guard: name parse (unmodelled TIB dependency),
+  \<comment> \<open>Superseded by forth_is_full below (name parse and DF store are now
-     vm_find_word (FIND-family gap), the `func != defer_runtime` identity
+     modelled; only the FIND lookup and identity check are sidestepped,
-     check (unmodellable -- word_table has no per-entry function-identity
+     not left as a blank "not modelled"). Kept for its accurate
-     query in this model), and the DF store (gap b). See file header.\<close>
+     description of the OLD state, not deleted.\<close>
   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 \<Rightarrow> nat option \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> 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\<lparr>data_stack := tl (data_stack vm)\<rparr>;
+           (nm, vm2) = forth_parse_word max_len vm1
+       in if nm = ''''
+          then set_error vm2
+          else case target_wid_opt of
+                 None \<Rightarrow> set_error vm2
+               | Some wid \<Rightarrow>
+                   if \<not> 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 \<noteq> []"
+  assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
+  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\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
+    by fastforce
+  hence "nm \<noteq> ''''" 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 \<noteq> []"
+  assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
+  assumes "target_wid_opt = Some wid" "\<not> 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\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
+    by fastforce
+  hence "nm \<noteq> ''''" 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 \<noteq> []"
+  assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
+  assumes "target_wid_opt = Some wid" "is_defer_word"
+  assumes "dictionary (snd (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>))) wid = Some e"
+  shows "dictionary (forth_is_full max_len target_wid_opt is_defer_word vm) wid = Some (e\<lparr>de_df := hd (data_stack vm)\<rparr>)"
+proof -
+  obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
+    by fastforce
+  hence "nm \<noteq> ''''" 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 \<comment> \<open>defer_runtime: DF read (gap b) + call-through (gap c).\<close>
+lemma defer_runtime_not_modelled: True \<comment> \<open>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.\<close>
   by simp
-lemma defer_fetch_not_modelled: True   \<comment> \<open>DEFER@: FIND (name-resolution gap) + DF read (gap b).\<close>
+lemma defer_fetch_not_modelled: True   \<comment> \<open>Superseded by forth_defer_fetch_full below, same as is_guard_rest_not_modelled above.\<close>
   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 \<Rightarrow> nat option \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> 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 \<Rightarrow> set_error vm1
+             | Some wid \<Rightarrow>
+                 if \<not> is_defer_word
+                 then set_error vm1
+                 else case dictionary vm1 wid of
+                        None \<Rightarrow> set_error vm1
+                      | Some e \<Rightarrow>
+                          if ds_full vm1
+                          then set_error vm1
+                          else vm1\<lparr>data_stack := de_df e # data_stack vm1\<rparr>)"
+
+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) \<noteq> ''''"
+  assumes "target_wid_opt = Some wid" "is_defer_word"
+  assumes "dictionary (snd (forth_parse_word max_len vm)) wid = Some e"
+  assumes "\<not> 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 \<noteq> ''''" 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