proof/: add StarForth_Defining_Words.thy (defining_words.c coverage)

4 of 19 words fully modelled ([, ], STATE, IMMEDIATE), 2 guard-only
partial (:, ;), rest deferred behind three named model gaps: dictionary-
entry creation (never modelled anywhere in this suite before now),
data-field addressing (same class as the existing >BODY gap), and
mutable per-entry dispatch (word_table is a fixed global, can't express
DEFER/IS).

Finding: defining_words.c's [/]/STATE are registered after (and thus
permanently shadow) dictionary_manipulation_words.c's versions of the
same names -- that file's prior "dead cross-VM-shared static" finding
only ever applied to the shadowed, unreachable code. The live versions
correctly use vm->state_addr, a real per-VM field, now added to
vm_state.

proof/StarForth_Base.thy

@@ -531,6 +531,15 @@ record vm_state =
   base_addr     :: nat
   hold_addr     :: nat
   hold_pos      :: nat
+  (* ○ CODE-MUST-MATCH: C: vaddr_t state_addr (include/vm.h:452) -- VM
+     address of the cell holding STATE (0=interp, -1=compile). Distinct from
+     `state_var` (above), which is the host-side mirror cell_t field. Added
+     for StarForth_Defining_Words.thy's `[`/`]`/STATE -- these are the LIVE,
+     reachable implementations (defining_words.c registers over
+     dictionary_manipulation_words.c's `[`/`]`/STATE, which are dead code
+     once shadowed; see that file for the shadowed versions and this file
+     for the correction). *)
+  state_addr    :: nat
 
   (* ── Physics Loop #1: Execution heat tracking ───────────────────────── *)
   (* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct.