proof/: close the data-field (DF) gap for CREATE/VARIABLE/CONSTANT

Adds de_df :: cell to dict_entry (StarForth_Base.thy) -- the DF cell
modelled as a plain value, closing gap (b) for every word that only
reads/writes it through its OWNING entry. Confirmed by grep this record
has exactly one construction site in the whole 52-theory suite
(dict_insert_entry), so the field addition's blast radius is contained
to StarForth_Defining_Words.thy alone -- full suite still verifies
unchanged elsewhere.

dict_write_df writes an existing entry's DF by word_id. forth_create_full/
forth_variable_full/forth_constant_full now compose the DF write in,
making CREATE/VARIABLE/CONSTANT the first three FULLY modelled words in
this file (guard through parse through insertion through the DF write --
nothing left unmodelled per word except the pin-shadow name-scan guard,
sidestepped the same way as everywhere else in this suite).

Their runtime companions (defining_runtime_create/_variable/_constant --
confirmed byte-identical C bodies) share one new definition,
forth_runtime_read_df, gated on ds_full matching vm_push's real internal
check. Required adding current_executing_word_id to vm_state (mirrors
vm->current_executing_entry, word-id-indexed like latest_id).

DEFER and : remain at their previous closure level: DEFER's DF write was
already implicitly closed (de_df=0 at creation matches its explicit
*df=0), but its own runtime is a fundamentally different DF usage
(dispatch reassignment via a stored pointer, gap c, not a plain value);
: has no vm_state field for vm->compiling_word tracking.

Full suite (54 theories) verifies green.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

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 + `;` guard-only + `:`/CREATE/VARIABLE/CONSTANT full up to the DF write (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 + `:` full except `compiling_word` tracking (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,20 +116,30 @@ 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) — **partially closed 2026-08-14/15.** `dict_insert_entry`
+  CONSTANT, DEFER) — **closed end-to-end for CREATE/VARIABLE/CONSTANT,
-  (`StarForth_Defining_Words.thy`) models the word_id-assignment/
+  2026-08-14/15**, `:`/DEFER closed up to `vm->compiling_word` tracking.
-  dictionary-table/`latest_id`/`word_id_next`-counter portion. All five
+  `dict_insert_entry` (`StarForth_Defining_Words.thy`) models the
-  words now have a `forth_*_full` definition composing the real parse,
+  word_id-assignment/dictionary-table/`latest_id`/`word_id_next`-counter
-  any word-specific guard (CONSTANT's stack-underflow check, `:`'s
+  portion; `de_df :: cell` (added to `dict_entry` in `StarForth_Base.thy`)
-  nested-definition check), any align/allot step (CREATE's `vm_align`,
+  and `dict_write_df` close the data-field (DF) write gap (b) for every
-  VARIABLE's `vm_align` + a new `forth_vm_allot_raw` modelling the raw
+  word that treats DF as a plain value. Each of the five words' `forth_
-  `vm_allot` C helper), and the entry insertion itself, all the way up
+  *_full` definition now composes the real parse, any word-specific guard
-  to — but not including — the data-field write. Still not modelled for
+  (CONSTANT's stack-underflow check, `:`'s nested-definition check), any
-  any of the five: `vm->compiling_word` tracking (no vm_state field),
+  align/allot step (CREATE's `vm_align`; VARIABLE's `vm_align` +
-  the data-field (DF) write each word does afterward (still gap (b)
+  `forth_vm_allot_raw`, modelling the raw `vm_allot` C helper distinctly
-  below), and the pin-shadow name-scan guard (sidestepped via an explicit
+  from the FORTH word ALLOT), the entry insertion, AND the DF write —
-  `pinned_conflict :: bool` parameter, same technique as the XT-pop gap
+  CREATE/VARIABLE/CONSTANT are now fully modelled words, the first three
-  elsewhere in this suite).
+  in this entire file. Their runtime companions (`defining_runtime_
+  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).
 - **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_Base.thy

@@ -300,6 +300,19 @@ record dict_entry =
   de_acl_allow   :: bool    \<comment> \<open>acl_allow: cached decision (True=allow, False=deny)\<close>
   de_acl_mode    :: nat     \<comment> \<open>acl_mode: 0=TTL, 1=STRICT\<close>
   de_acl_pinned  :: bool    \<comment> \<open>acl_pinned: one-way ratchet; True = immutable\<close>
+  (* ○ CODE-MUST-MATCH, added 2026-08-15: the entry's data-field (DF) cell
+     -- the storage C's `vm_dictionary_get_data_field(entry)` returns a
+     pointer into (a single cell_t immediately following the entry's name
+     in the arena, per vm_create_word's layout, dictionary_management.c:
+     406-410). Modelled here as a plain VALUE (`cell`), not an address --
+     this closes gap (b) for every word that only ever reads/writes the DF
+     as a value through its OWNING entry (CREATE/VARIABLE/CONSTANT/DEFER
+     and their runtimes). It does NOT close >BODY/>NAME-style words in
+     StarForth_Dictionary_Manipulation_Words.thy, which need the DF's
+     ADDRESS (so a later, unrelated `@`/`!` could target it generically)
+     -- this model has no notion of a dict_entry's own address, only its
+     word_id, so that remains a distinct, still-open gap. *)
+  de_df          :: cell
 
 (* ── Word transition metrics ─────────────────────────────────────────────── *)
 (* ○ CODE-MUST-MATCH: struct WordTransitionMetrics in include/physics_pipelining_metrics.h
@@ -501,6 +514,13 @@ record vm_state =
   dict_fence    :: "nat option"                   \<comment> \<open>FENCE word_id for FORGET\<close>
   dict_lock     :: lock_state
   word_id_next  :: nat
+  (* ○ CODE-MUST-MATCH, added 2026-08-15: C `DictEntry* vm->
+     current_executing_entry` (include/vm.h:434) -- the entry currently
+     executing, read by runtime helpers like `defining_runtime_create`/
+     `_variable`/`_constant` via `vm->current_executing_entry` rather than
+     a fresh lookup. Modelled word-id-indexed (`nat option`), matching
+     `latest_id`'s convention, rather than as a raw pointer. *)
+  current_executing_word_id :: "nat option"
 
   (* ── Execution state ──────────────────────────────────────────────────── *)
   vm_mode       :: vm_mode

proof/StarForth_Defining_Words.thy

@@ -151,7 +151,7 @@ definition dict_insert_entry :: "string \<Rightarrow> nat \<Rightarrow> bool \<R
                                dp_last_decay_ns = 0, dp_mass_bytes = 0,
                                dp_avg_latency_ns = 0, dp_state_flags = 0\<rparr>,
                 de_acl_ttl = 0, de_acl_allow = True, de_acl_mode = ACL_MODE_TTL,
-                de_acl_pinned = False\<rparr>
+                de_acl_pinned = False, de_df = 0\<rparr>
        in vm\<lparr>dictionary := (dictionary vm)(wid := Some e),
              latest_id := Some wid,
              word_id_next := wid + 1\<rparr>)"
@@ -171,7 +171,7 @@ lemma dict_insert_entry_populates_dictionary:
   shows "\<exists>e. dictionary (dict_insert_entry name init_flags pinned_conflict vm) (word_id_next vm) = Some e
              \<and> de_word_id e = word_id_next vm \<and> de_name e = name \<and> de_flags e = init_flags
              \<and> de_heat e = 0 \<and> de_acl_ttl e = 0 \<and> de_acl_allow e \<and> de_acl_mode e = ACL_MODE_TTL
-             \<and> \<not> de_acl_pinned e"
+             \<and> \<not> de_acl_pinned e \<and> de_df e = 0"
   using assms by (simp add: dict_insert_entry_def Let_def)
 
 lemma dict_insert_entry_advances_counter:
@@ -193,6 +193,36 @@ lemma dict_insert_entry_not_full_word_id_next_bound: True
      than DICTIONARY_SIZE words), not claimed to be handled.\<close>
   by simp
 
+(* ── Data-field (DF) write, gap (b) PARTIALLY CLOSED 2026-08-15 ──────────
+   `de_df` (StarForth_Base.thy) models the DF cell as a plain value.
+   `dict_write_df` writes it into an EXISTING entry by word_id -- the
+   shared mechanism CREATE/VARIABLE/CONSTANT's own DF write (after
+   `vm_create_word` already returned) all reduce to. No-op if the word_id
+   doesn't resolve (mirrors a defensive NULL check that never actually
+   fires on any real caller in this suite, all of which write DF
+   immediately after a successful `dict_insert_entry` at a word_id they
+   just observed being created). *)
+
+definition dict_write_df :: "nat \<Rightarrow> cell \<Rightarrow> vm_state \<Rightarrow> vm_state" where
+  "dict_write_df wid v vm =
+    (case dictionary vm wid of
+       None \<Rightarrow> vm
+     | Some e \<Rightarrow> vm\<lparr>dictionary := (dictionary vm)(wid := Some (e\<lparr>de_df := v\<rparr>))\<rparr>)"
+
+lemma dict_write_df_present:
+  assumes "dictionary vm wid = Some e"
+  shows "dictionary (dict_write_df wid v vm) wid = Some (e\<lparr>de_df := v\<rparr>)"
+  using assms by (simp add: dict_write_df_def)
+
+lemma dict_write_df_absent_noop:
+  assumes "dictionary vm wid = None"
+  shows "dict_write_df wid v vm = vm"
+  using assms by (simp add: dict_write_df_def)
+
+lemma dict_write_df_data_stack_unchanged:
+  "data_stack (dict_write_df wid v vm) = data_stack vm"
+  by (simp add: dict_write_df_def split: option.split)
+
 (* ── [ ( -- ) : interpret mode, LIVE version (see file header) ──────────── *)
 (* C: vm_store_cell(vm, vm->state_addr, 0); vm->mode = MODE_INTERPRET. *)
 
@@ -553,30 +583,25 @@ lemma constant_entry_half_not_full_constant: True
      popped value (gap b). See section header.\<close>
   by simp
 
-(* ── CONSTANT, full composition, gap (a)+parse CLOSED for this one word
+(* ── CONSTANT, full composition, gap (a)+parse+DF CLOSED 2026-08-14/15 ───
-   2026-08-14 ─────────────────────────────────────────────────────────────
+   CONSTANT's real C order: guard (dsp<0) -> pop value -> parse name ->
-   Demonstrates end-to-end what StarForth_Base.thy's `forth_parse_word`
+   vm_create_word -> DF write of the popped value. Now modelled completely
-   (added this session, closing the TIB/name-parse gap named as an
+   -- the first fully-closed word in this file, and the flagship
-   unmodelled precondition throughout this suite) unlocks when composed
+   composition of `forth_parse_word` (TIB), `dict_insert_entry` (gap a),
-   with `dict_insert_entry`: CONSTANT's real C order is guard (dsp<0) ->
+   and `dict_write_df` (gap b), all added this session. *)
-   pop value -> parse name -> vm_create_word. Modelled here exactly in
-   that order, chosen as the flagship composition because it is this
-   file's simplest word with a real stack guard (unlike CREATE/VARIABLE,
-   which have no stack precondition at all). Still NOT modelled: the DF
-   write of the popped value into the new entry (gap b) -- `value` is
-   computed and discarded here, faithfully matching everything up to
-   that point but no further. *)
 
 definition forth_constant_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
   "forth_constant_full max_len pinned_conflict vm =
     (if data_stack vm = []
      then set_error vm
      else
-       let vm1        = vm\<lparr>data_stack := tl (data_stack vm)\<rparr>;
+       let value      = 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 dict_insert_entry nm 0 pinned_conflict vm2)"
+          else let wid = word_id_next vm2
+               in dict_write_df wid value (dict_insert_entry nm 0 pinned_conflict vm2))"
 
 lemma constant_full_underflow:
   assumes "data_stack vm = []"
@@ -589,7 +614,7 @@ lemma constant_full_success_populates_dictionary:
   assumes "max_len \<ge> 2"
   assumes "\<not> pinned_conflict"
   shows "\<exists>e wid. dictionary (forth_constant_full max_len pinned_conflict vm) wid = Some e
-                \<and> de_name e \<noteq> '''' \<and> de_flags e = 0"
+                \<and> de_name e \<noteq> '''' \<and> de_flags e = 0 \<and> de_df e = hd (data_stack vm)"
 proof -
   let ?vm1 = "vm\<lparr>data_stack := tl (data_stack vm)\<rparr>"
   obtain nm vm2 where parse_eq: "forth_parse_word max_len ?vm1 = (nm, vm2)" by fastforce
@@ -598,26 +623,31 @@ proof -
   hence nm_nonempty: "nm \<noteq> ''''"
     using forth_parse_word_success_nonempty[OF input_pos_unaffected assms(3)] parse_eq
     by (metis fstI)
-  have "forth_constant_full max_len pinned_conflict vm
+  let ?wid = "word_id_next vm2"
-          = dict_insert_entry nm 0 pinned_conflict vm2"
+  let ?vm3 = "dict_insert_entry nm 0 pinned_conflict vm2"
+  have full_eq: "forth_constant_full max_len pinned_conflict vm = dict_write_df ?wid (hd (data_stack vm)) ?vm3"
     using assms(1) parse_eq nm_nonempty by (simp add: forth_constant_full_def)
-  moreover have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict vm2) (word_id_next vm2) = Some e
+  have "\<exists>e. dictionary ?vm3 ?wid = Some e \<and> de_name e = nm \<and> de_flags e = 0"
-                     \<and> de_name e = nm \<and> de_flags e = 0"
     using assms(4) by (simp add: dict_insert_entry_def Let_def)
-  ultimately show ?thesis using nm_nonempty by auto
+  then obtain e where e_eq: "dictionary ?vm3 ?wid = Some e" "de_name e = nm" "de_flags e = 0" by blast
+  have "dictionary (dict_write_df ?wid (hd (data_stack vm)) ?vm3) ?wid = Some (e\<lparr>de_df := hd (data_stack vm)\<rparr>)"
+    using dict_write_df_present[OF e_eq(1)] by simp
+  thus ?thesis using full_eq e_eq nm_nonempty by auto
 qed
 
-(* ── CREATE, full composition, gap (a)+parse CLOSED for this word
+(* ── CREATE, full composition, gap (a)+parse+DF CLOSED 2026-08-15 ────────
-   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
+   capture dfa = here -> DF write of dfa. No stack precondition at all
-   stack precondition at all (unlike CONSTANT). `forth_align`
+   (unlike CONSTANT). `forth_align` (StarForth_Dictionary_Words.thy) is
-   (StarForth_Dictionary_Words.thy) is reused directly -- it is exactly
+   reused directly -- it is exactly what `vm_align` already models,
-   what `vm_align` already models, word-for-word. Composed unconditionally
+   word-for-word. The word_id is captured BEFORE `dict_insert_entry`
-   over `dict_insert_entry`'s result the same way `forth_colon_entry_half`
+   advances `word_id_next`, then used to target the DF write after
-   already does: when `pinned_conflict` holds, the real C returns before
+   `forth_align` has run (align only touches `here`, never `dictionary`,
-   ever calling vm_align, so `forth_align` running anyway on the
+   so this ordering is safe regardless of which happens first). When
-   already-errored state is a known, minor divergence, not claimed
+   `pinned_conflict` holds, the real C returns before ever calling
+   vm_align; `forth_align`/`dict_write_df` running anyway on the
+   already-errored state (a no-op for dict_write_df, since no entry
+   exists at that word_id) is a known, minor divergence, not claimed
    otherwise -- see forth_colon_entry_half's identical precedent. *)
 
 definition forth_create_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
@@ -625,7 +655,10 @@ definition forth_create_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \
     (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))"
+        else
+          let wid = word_id_next vm1;
+              vm2 = forth_align (dict_insert_entry nm 0 pinned_conflict vm1)
+          in dict_write_df wid (word_of_nat (here vm2)) vm2)"
 
 lemma create_full_empty_parse_errors:
   assumes "fst (forth_parse_word max_len vm) = ''''"
@@ -646,15 +679,20 @@ proof -
   obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce
   hence nm_nonempty: "nm \<noteq> ''''"
     using forth_parse_word_success_nonempty[OF assms(1) assms(2)] by (metis fstI)
-  have "forth_create_full max_len pinned_conflict vm
+  let ?wid = "word_id_next vm1"
-          = forth_align (dict_insert_entry nm 0 pinned_conflict vm1)"
+  let ?vm2 = "forth_align (dict_insert_entry nm 0 pinned_conflict vm1)"
-    using parse_eq nm_nonempty by (simp add: forth_create_full_def)
+  have full_eq: "forth_create_full max_len pinned_conflict vm = dict_write_df ?wid (word_of_nat (here ?vm2)) ?vm2"
-  moreover have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) (word_id_next vm1) = Some e
+    using parse_eq nm_nonempty by (simp add: forth_create_full_def Let_def)
-                     \<and> de_name e = nm \<and> de_flags e = 0"
+  have dict_eq: "dictionary ?vm2 = dictionary (dict_insert_entry nm 0 pinned_conflict vm1)"
-    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
+  have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) ?wid = Some e
+           \<and> de_name e = nm \<and> de_flags e = 0"
+    using assms(3) by (simp add: dict_insert_entry_def Let_def)
+  then obtain e where e_eq: "dictionary ?vm2 ?wid = Some e" "de_name e = nm" "de_flags e = 0"
+    using dict_eq by auto
+  have "dictionary (forth_create_full max_len pinned_conflict vm) ?wid = Some (e\<lparr>de_df := word_of_nat (here ?vm2)\<rparr>)"
+    using full_eq dict_write_df_present[OF e_eq(1)] by simp
+  thus ?thesis using e_eq(2) e_eq(3) nm_nonempty by fastforce
 qed
 
 (* ── VARIABLE, full composition, gap (a)+parse CLOSED for this word
@@ -689,13 +727,21 @@ 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)
 
+(* Real C order: parse -> vm_align -> capture addr=here -> vm_allot(cell)
+   -> vm_create_word -> DF write of addr. `addr` is captured right after
+   align, BEFORE allot advances `here` again -- gap (b) now closed too. *)
+
 definition forth_variable_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> 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
+        else
-               (forth_vm_allot_raw CELL_BYTES (forth_align vm1)))"
+          let vm2  = forth_align vm1;
+              addr = here vm2;
+              vm3  = forth_vm_allot_raw CELL_BYTES vm2;
+              wid  = word_id_next vm3
+          in dict_write_df wid (word_of_nat addr) (dict_insert_entry nm 0 pinned_conflict vm3))"
 
 lemma variable_full_empty_parse_errors:
   assumes "fst (forth_parse_word max_len vm) = ''''"
@@ -717,20 +763,71 @@ proof -
   hence nm_nonempty: "nm \<noteq> ''''"
     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
+  let ?wid = "word_id_next ?vm3"
-          = dict_insert_entry nm 0 pinned_conflict ?vm3"
+  have full_eq: "forth_variable_full max_len pinned_conflict vm
-    using parse_eq nm_nonempty by (simp add: forth_variable_full_def)
+          = dict_write_df ?wid (word_of_nat (here (forth_align vm1))) (dict_insert_entry nm 0 pinned_conflict ?vm3)"
-  moreover have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) (word_id_next ?vm3) = Some e
+    using parse_eq nm_nonempty by (simp add: forth_variable_full_def Let_def)
-                     \<and> de_name e = nm \<and> de_flags e = 0"
+  have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) ?wid = Some e
+           \<and> de_name e = nm \<and> de_flags e = 0"
     using assms(3) by (simp add: dict_insert_entry_def Let_def)
-  ultimately show ?thesis using nm_nonempty by auto
+  then obtain e where e_eq: "dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) ?wid = Some e"
+                             "de_name e = nm" "de_flags e = 0" by blast
+  have "dictionary (forth_variable_full max_len pinned_conflict vm) ?wid = Some (e\<lparr>de_df := word_of_nat (here (forth_align vm1))\<rparr>)"
+    using full_eq dict_write_df_present[OF e_eq(1)] by simp
+  thus ?thesis using e_eq(2) e_eq(3) nm_nonempty by fastforce
 qed
 
-lemma create_runtime_not_modelled: True   \<comment> \<open>defining_runtime_create: reads current_executing_entry's DF cell (gap b).\<close>
+(* ── defining_runtime_create / _variable / _constant: gap (b) CLOSED
+   2026-08-15 ───────────────────────────────────────────────────────────
+   All three C bodies are byte-identical in shape (defining_words.c:91-160):
+   guard `current_executing_entry` present, guard its DF cell present,
+   push the DF value. One shared definition suffices; the real C's
+   distinction is only which name gets logged, with no vm_state-visible
+   difference. `current_executing_word_id` (StarForth_Base.thy) models
+   `vm->current_executing_entry`; the second guard (DF cell present) is
+   always true here since a live word_id always has an entry with a
+   `de_df` field in this model -- included anyway via the `None` dictionary
+   case for defensive symmetry with the C's own two-guard shape, even
+   though it is unreachable from any real entry point in this suite. A
+   `ds_full` check is added before the push, matching every other
+   guarded-push word in this suite that goes through `vm_push`. *)
+
+definition forth_runtime_read_df :: "vm_state \<Rightarrow> vm_state" where
+  "forth_runtime_read_df vm =
+    (case current_executing_word_id vm of
+       None \<Rightarrow> set_error vm
+     | Some wid \<Rightarrow>
+         (case dictionary vm wid of
+            None \<Rightarrow> set_error vm
+          | Some e \<Rightarrow>
+              if ds_full vm
+              then set_error vm
+              else vm\<lparr>data_stack := de_df e # data_stack vm\<rparr>))"
+
+lemma runtime_read_df_no_executing_entry:
+  assumes "current_executing_word_id vm = None"
+  shows "vm_error (forth_runtime_read_df vm)"
+  using assms by (simp add: forth_runtime_read_df_def set_error_def)
+
+lemma runtime_read_df_pushes_value:
+  assumes "current_executing_word_id vm = Some wid"
+  assumes "dictionary vm wid = Some e"
+  assumes "\<not> ds_full vm"
+  shows "data_stack (forth_runtime_read_df vm) = de_df e # data_stack vm"
+  using assms by (simp add: forth_runtime_read_df_def)
+
+lemma runtime_read_df_overflow:
+  assumes "current_executing_word_id vm = Some wid"
+  assumes "dictionary vm wid = Some e"
+  assumes "ds_full vm"
+  shows "vm_error (forth_runtime_read_df vm)"
+  using assms by (simp add: forth_runtime_read_df_def set_error_def)
+
+lemma create_runtime_is_read_df: True     \<comment> \<open>defining_runtime_create IS forth_runtime_read_df -- see definition above.\<close>
   by simp
-lemma variable_runtime_not_modelled: True \<comment> \<open>defining_runtime_variable: reads current_executing_entry's DF cell (gap b).\<close>
+lemma variable_runtime_is_read_df: True   \<comment> \<open>defining_runtime_variable IS forth_runtime_read_df -- see definition above.\<close>
   by simp
-lemma constant_runtime_not_modelled: True \<comment> \<open>defining_runtime_constant: reads current_executing_entry's DF cell (gap b).\<close>
+lemma constant_runtime_is_read_df: True   \<comment> \<open>defining_runtime_constant IS forth_runtime_read_df -- see definition above.\<close>
   by simp
 lemma lit_not_modelled: True           \<comment> \<open>LIT: reads/advances the return-stack top as a raw C cell_t* threaded-code IP -- see file header, distinct from control_words.c's already-resolved IP-as-vaddr usage.\<close>
   by simp