diff --git a/proof/ROOT b/proof/ROOT
index 76f8cc3..7ae6dd5 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -12,6 +12,7 @@ session "StarForth" = "HOL-Library" +
     StarForth_Memory_Words
     StarForth_Dictionary_Words
     StarForth_Dictionary_Manipulation_Words
+    StarForth_Control_Words
     StarForth_Mutex
     StarForth_Transition
     StarForth_Loop1_Heat
diff --git a/proof/StarForth_Control_Words.thy b/proof/StarForth_Control_Words.thy
new file mode 100644
index 0000000..9f49e75
--- /dev/null
+++ b/proof/StarForth_Control_Words.thy
@@ -0,0 +1,525 @@
+theory StarForth_Control_Words
+  imports StarForth_Base StarForth_Dictionary_Words
+begin
+
+(* =========================================================================
+   POST-08: Control Flow Words
+   Mirrors: src/word_source/control_words.c
+
+   This file splits sharply into two classes, unlike any prior file in this
+   sweep:
+
+   1. RUNTIME words ((BRANCH), (0BRANCH), (?DO), (DO), (LOOP), (+LOOP),
+      (LEAVE), UNLOOP, I, J, EXIT) execute per-VM, inside `vm->return_stack`
+      -- which IS in the abstract model. The "vm_ip as raw pointer" gap
+      flagged at every earlier resume point turns out NOT to need a new
+      model extension: the top of `return_stack` holds a `cell` that is a
+      byte address into `vm->memory`, exactly like an `@`/`!` address taken
+      from the data stack. Reusing `mem_read`/`unat` from
+      StarForth_Memory_Words (imported transitively via
+      StarForth_Dictionary_Words) models it directly. Fully covered below.
+
+   2. COMPILE-TIME words (IF/ELSE/THEN, BEGIN/WHILE/REPEAT/AGAIN/UNTIL,
+      ?DO/DO/LOOP/+LOOP/LEAVE's compiling halves, CASE/OF/ENDOF/ENDCASE) are
+      NOT modelled -- not because the model is missing a piece, but because
+      of a genuine architectural finding (below) that makes modelling them
+      against `vm_state` actively misleading: their real state does not
+      live in the VM at all.
+
+   ── Headline finding, not fixed ──────────────────────────────────────────
+   EVERY compile-time control-flow word in this file operates on FILE-SCOPE
+   C statics, not `struct VM` fields: `cf_stack`/`cf_sp` (the IF/BEGIN/DO/
+   CASE/OF nesting stack), `cf_last_mode` (the mode-transition heuristic
+   `cf_epoch_sync` uses to decide when to reset `cf_stack`), `leave_addrs`/
+   `leave_sp`/`leave_mark_stack`/`leave_mark_sp` (LEAVE patch sites), and
+   `endof_addrs`/`endof_sp`/`endof_mark_stack`/`endof_mark_sp` (ENDOF patch
+   sites) -- all declared `static` at file scope (lines 115-183), shared by
+   every `VM*` in the process. There is no VM-id key anywhere in any of
+   them.
+
+   Concretely, in the Tripod multi-VM fleet this repo is built around: if
+   two VMs ever compile colon definitions containing control structures at
+   overlapping times, their IF/DO/CASE nesting corrupts across VMs, since
+   both write through the same `cf_stack`/`cf_sp`. Even without true
+   concurrency, if one VM's compilation aborts mid-structure (a syntax
+   error, an ACL denial, a capsule birth interrupted) leaving `cf_sp`/
+   `leave_sp`/`endof_sp` non-reset, that leftover state is silently
+   inherited by whichever VM compiles the next colon definition, in the
+   same process, regardless of which VM it is. The only guard,
+   `cf_epoch_sync` (lines 121-132), resets `cf_stack` when it observes a
+   *mode* transition -- but it compares against `cf_last_mode`, itself a
+   single global, not keyed per VM either: it can neither reliably detect
+   "this VM's mode changed" (another VM's mode flip can mask this one's)
+   nor avoid falsely resetting genuine in-progress nesting (this VM's own
+   legitimate COMPILE-mode session, interrupted by another VM's transition
+   observed first).
+
+   None of `cf_stack`, `leave_addrs`, `endof_addrs`, or their mark-stacks
+   and cursors have any representation in `vm_state` (StarForth_Base.thy) --
+   correctly so, since giving them one would misrepresent what the C code
+   actually does (global, not per-VM). Modelling the compile-time words
+   would therefore mean either (a) inventing a vm_state field the real
+   implementation doesn't have, silently "fixing" the bug in the proof
+   while the C stays broken, or (b) modelling a bare global outside
+   vm_state, which this proof suite has no precedent or plumbing for. Both
+   are out of scope; the words are left as documented gaps below.
+   ======================================================================== *)
+
+definition CELL_BYTES_W :: cell where "CELL_BYTES_W = word_of_nat CELL_BYTES"
+
+(* ── (BRANCH) ( -- ) : unconditional branch ───────────────────────────────
+   C: ip = return_stack[rsp] (TOS); rel = *ip; ip += rel (bytes); store back. *)
+
+definition forth_branch :: "vm_state \<Rightarrow> vm_state" where
+  "forth_branch vm =
+    (case return_stack vm of
+       []       \<Rightarrow> set_error vm
+     | ip # rst \<Rightarrow>
+         let rel = mem_read (memory vm) (unat ip)
+         in vm\<lparr>return_stack := (ip + rel) # rst\<rparr>)"
+
+lemma branch_underflow:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_branch vm)"
+  by (simp add: forth_branch_def set_error_def assms)
+
+lemma branch_normal:
+  assumes "return_stack vm = ip # rst"
+  shows "return_stack (forth_branch vm) = (ip + mem_read (memory vm) (unat ip)) # rst"
+  by (simp add: forth_branch_def assms)
+
+lemma branch_data_stack_unchanged:
+  "data_stack (forth_branch vm) = data_stack vm"
+  by (auto simp: forth_branch_def set_error_def Let_def split: list.split)
+
+(* ── (0BRANCH) ( f -- ) : conditional branch ──────────────────────────────
+   C: checks rsp<0 THEN dsp<0 (in that order); pops flag; if flag=0 take the
+   branch (ip+=rel), else fall through (ip+=1 cell, skipping the literal). *)
+
+definition forth_zero_branch :: "vm_state \<Rightarrow> vm_state" where
+  "forth_zero_branch vm =
+    (case return_stack vm of
+       []        \<Rightarrow> set_error vm
+     | ip # rst \<Rightarrow>
+         (case data_stack vm of
+            []          \<Rightarrow> set_error vm
+          | flag # drst \<Rightarrow>
+              let rel = mem_read (memory vm) (unat ip);
+                  new_ip = if flag = 0 then ip + rel else ip + CELL_BYTES_W
+              in vm\<lparr>data_stack := drst, return_stack := new_ip # rst\<rparr>))"
+
+lemma zero_branch_rsp_underflow:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_zero_branch vm)"
+  by (simp add: forth_zero_branch_def set_error_def assms)
+
+lemma zero_branch_dsp_underflow:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_zero_branch vm)"
+  by (simp add: forth_zero_branch_def set_error_def assms)
+
+lemma zero_branch_taken:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = 0 # drst"
+  shows "return_stack (forth_zero_branch vm) = (ip + mem_read (memory vm) (unat ip)) # rst"
+    and "data_stack (forth_zero_branch vm) = drst"
+  using assms by (simp_all add: forth_zero_branch_def)
+
+lemma zero_branch_not_taken:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = flag # drst"
+  assumes "flag \<noteq> 0"
+  shows "return_stack (forth_zero_branch vm) = (ip + CELL_BYTES_W) # rst"
+    and "data_stack (forth_zero_branch vm) = drst"
+  using assms by (simp_all add: forth_zero_branch_def)
+
+(* ── (?DO) ( limit index -- ) ──────────────────────────────────────────────
+   C: checks rsp<0 THEN dsp<1; pops index then limit. If index=limit, skips
+   the whole loop body (ip+=rel from the fwd-branch literal). Otherwise
+   enters: ip+=1 cell (skip literal), push (limit,index) under ip, checking
+   the same rsp+2>=STACK_SIZE overflow DO itself checks. *)
+
+definition forth_qdo_runtime :: "vm_state \<Rightarrow> vm_state" where
+  "forth_qdo_runtime vm =
+    (case return_stack vm of
+       []        \<Rightarrow> set_error vm
+     | ip # rst \<Rightarrow>
+         (case data_stack vm of
+            index # limit # drst \<Rightarrow>
+              let rel = mem_read (memory vm) (unat ip)
+              in if index = limit
+                 then vm\<lparr>data_stack := drst, return_stack := (ip + rel) # rst\<rparr>
+                 else if length rst + 2 \<ge> STACK_SIZE
+                      then set_error (vm\<lparr>data_stack := drst\<rparr>)
+                      else vm\<lparr>data_stack := drst,
+                               return_stack := (ip + CELL_BYTES_W) # index # limit # rst\<rparr>
+          | _ \<Rightarrow> set_error vm))"
+
+lemma qdo_rsp_underflow:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_qdo_runtime vm)"
+  by (simp add: forth_qdo_runtime_def set_error_def assms)
+
+lemma qdo_dsp_underflow_nil:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_qdo_runtime vm)"
+  by (simp add: forth_qdo_runtime_def set_error_def assms)
+
+lemma qdo_dsp_underflow_one:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = [x]"
+  shows "vm_error (forth_qdo_runtime vm)"
+  by (simp add: forth_qdo_runtime_def set_error_def assms)
+
+lemma qdo_empty_skips:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = n # n # drst"
+  shows "return_stack (forth_qdo_runtime vm) = (ip + mem_read (memory vm) (unat ip)) # rst"
+    and "data_stack (forth_qdo_runtime vm) = drst"
+  using assms by (simp_all add: forth_qdo_runtime_def)
+
+lemma qdo_enters:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = index # limit # drst"
+  assumes "index \<noteq> limit"
+  assumes "length rst + 2 < STACK_SIZE"
+  shows "return_stack (forth_qdo_runtime vm) = (ip + CELL_BYTES_W) # index # limit # rst"
+    and "data_stack (forth_qdo_runtime vm) = drst"
+  using assms by (simp_all add: forth_qdo_runtime_def)
+
+(* ── (DO) ( limit index -- ) ──────────────────────────────────────────────
+   C: checks rsp<0 THEN dsp<1; pops index then limit; unconditionally
+   inserts (limit,index) under the current ip (copied, never dereferenced --
+   no early-exit test, unlike (?DO)). Same overflow check as (?DO). *)
+
+definition forth_do_runtime :: "vm_state \<Rightarrow> vm_state" where
+  "forth_do_runtime vm =
+    (case return_stack vm of
+       []        \<Rightarrow> set_error vm
+     | ip # rst \<Rightarrow>
+         (case data_stack vm of
+            index # limit # drst \<Rightarrow>
+              if length rst + 2 \<ge> STACK_SIZE
+              then set_error (vm\<lparr>data_stack := drst\<rparr>)
+              else vm\<lparr>data_stack := drst, return_stack := ip # index # limit # rst\<rparr>
+          | _ \<Rightarrow> set_error vm))"
+
+lemma do_rsp_underflow:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_do_runtime vm)"
+  by (simp add: forth_do_runtime_def set_error_def assms)
+
+lemma do_normal:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = index # limit # drst"
+  assumes "length rst + 2 < STACK_SIZE"
+  shows "return_stack (forth_do_runtime vm) = ip # index # limit # rst"
+    and "data_stack (forth_do_runtime vm) = drst"
+  using assms by (simp_all add: forth_do_runtime_def)
+
+lemma do_overflow:
+  assumes "return_stack vm = ip # rst"
+  assumes "data_stack vm = index # limit # drst"
+  assumes "length rst + 2 \<ge> STACK_SIZE"
+  shows "vm_error (forth_do_runtime vm)"
+  using assms by (simp add: forth_do_runtime_def set_error_def)
+
+(* ── (LOOP) ( -- ) ─────────────────────────────────────────────────────── *)
+(* C: rsp<2 -> error. idx += 1; back = *ip; continue (signed idx<lim) ->
+   ip += back, keep frame; else drop (limit,index), ip += 1 cell. *)
+
+definition forth_loop_runtime :: "vm_state \<Rightarrow> vm_state" where
+  "forth_loop_runtime vm =
+    (case return_stack vm of
+       ip # idx # lim # rst \<Rightarrow>
+         let back = mem_read (memory vm) (unat ip);
+             new_idx = idx + 1
+         in if new_idx <s lim
+            then vm\<lparr>return_stack := (ip + back) # new_idx # lim # rst\<rparr>
+            else vm\<lparr>return_stack := (ip + CELL_BYTES_W) # rst\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma loop_underflow_nil:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_loop_runtime vm)"
+  by (simp add: forth_loop_runtime_def set_error_def assms)
+
+lemma loop_underflow_one:
+  assumes "return_stack vm = [ip]"
+  shows "vm_error (forth_loop_runtime vm)"
+  by (simp add: forth_loop_runtime_def set_error_def assms)
+
+lemma loop_underflow_two:
+  assumes "return_stack vm = [ip, idx]"
+  shows "vm_error (forth_loop_runtime vm)"
+  by (simp add: forth_loop_runtime_def set_error_def assms)
+
+lemma loop_continues:
+  assumes "return_stack vm = ip # idx # lim # rst"
+  assumes "idx + 1 <s lim"
+  shows "return_stack (forth_loop_runtime vm) =
+         (ip + mem_read (memory vm) (unat ip)) # (idx + 1) # lim # rst"
+  using assms by (simp add: forth_loop_runtime_def)
+
+lemma loop_exits:
+  assumes "return_stack vm = ip # idx # lim # rst"
+  assumes "\<not> (idx + 1 <s lim)"
+  shows "return_stack (forth_loop_runtime vm) = (ip + CELL_BYTES_W) # rst"
+  using assms by (simp add: forth_loop_runtime_def)
+
+lemma loop_data_stack_unchanged:
+  "data_stack (forth_loop_runtime vm) = data_stack vm"
+  by (auto simp: forth_loop_runtime_def set_error_def Let_def split: list.split)
+
+(* ── (+LOOP) ( n -- ) ──────────────────────────────────────────────────── *)
+(* C: checks dsp<0 THEN rsp<2, BOTH before popping n (unlike ALLOT's
+   pop-then-check -- here an rsp<2 failure leaves the data stack untouched).
+   newv = idx+n; continue test depends on sign of n (ascending vs
+   descending +LOOP). *)
+
+definition forth_plus_loop_runtime :: "vm_state \<Rightarrow> vm_state" where
+  "forth_plus_loop_runtime vm =
+    (case data_stack vm of
+       []          \<Rightarrow> set_error vm
+     | n # drst \<Rightarrow>
+         (case return_stack vm of
+            ip # idx # lim # rst \<Rightarrow>
+              let back = mem_read (memory vm) (unat ip);
+                  newv = idx + n;
+                  cont = if 0 \<le>s n then newv <s lim else lim \<le>s newv
+              in vm\<lparr>data_stack := drst,
+                     return_stack := (if cont then (ip + back) # newv # lim # rst
+                                       else (ip + CELL_BYTES_W) # rst)\<rparr>
+          | _ \<Rightarrow> set_error vm))"
+
+lemma plus_loop_dsp_underflow:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_plus_loop_runtime vm)"
+  by (simp add: forth_plus_loop_runtime_def set_error_def assms)
+
+lemma plus_loop_rsp_underflow_nil:
+  assumes "data_stack vm = n # drst"
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_plus_loop_runtime vm)"
+    and "data_stack (forth_plus_loop_runtime vm) = data_stack vm"
+  using assms by (simp_all add: forth_plus_loop_runtime_def set_error_def)
+
+lemma plus_loop_rsp_underflow_one:
+  assumes "data_stack vm = n # drst"
+  assumes "return_stack vm = [ip]"
+  shows "vm_error (forth_plus_loop_runtime vm)"
+    and "data_stack (forth_plus_loop_runtime vm) = data_stack vm"
+  using assms by (simp_all add: forth_plus_loop_runtime_def set_error_def)
+
+lemma plus_loop_rsp_underflow_two:
+  assumes "data_stack vm = n # drst"
+  assumes "return_stack vm = [ip, idx]"
+  shows "vm_error (forth_plus_loop_runtime vm)"
+    and "data_stack (forth_plus_loop_runtime vm) = data_stack vm"
+  using assms by (simp_all add: forth_plus_loop_runtime_def set_error_def)
+
+lemma plus_loop_ascending_continues:
+  assumes "data_stack vm = n # drst"
+  assumes "return_stack vm = ip # idx # lim # rst"
+  assumes "0 \<le>s n"
+  assumes "idx + n <s lim"
+  shows "return_stack (forth_plus_loop_runtime vm) =
+         (ip + mem_read (memory vm) (unat ip)) # (idx + n) # lim # rst"
+    and "data_stack (forth_plus_loop_runtime vm) = drst"
+  using assms by (simp_all add: forth_plus_loop_runtime_def)
+
+lemma plus_loop_descending_continues:
+  assumes "data_stack vm = n # drst"
+  assumes "return_stack vm = ip # idx # lim # rst"
+  assumes "\<not> 0 \<le>s n"
+  assumes "lim \<le>s (idx + n)"
+  shows "return_stack (forth_plus_loop_runtime vm) =
+         (ip + mem_read (memory vm) (unat ip)) # (idx + n) # lim # rst"
+  using assms by (simp add: forth_plus_loop_runtime_def)
+
+(* ── (LEAVE) ( -- ) : force the enclosing loop to exit at next LOOP/+LOOP ── *)
+(* C: rsp<2 -> error; else index := limit (loop-continue test becomes false
+   at the next (LOOP)/(+LOOP), since idx cannot exceed lim after this). *)
+
+definition forth_leave_runtime :: "vm_state \<Rightarrow> vm_state" where
+  "forth_leave_runtime vm =
+    (case return_stack vm of
+       ip # idx # lim # rst \<Rightarrow> vm\<lparr>return_stack := ip # lim # lim # rst\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma leave_runtime_underflow_nil:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_leave_runtime vm)"
+  by (simp add: forth_leave_runtime_def set_error_def assms)
+
+lemma leave_runtime_underflow_one:
+  assumes "return_stack vm = [ip]"
+  shows "vm_error (forth_leave_runtime vm)"
+  by (simp add: forth_leave_runtime_def set_error_def assms)
+
+lemma leave_runtime_underflow_two:
+  assumes "return_stack vm = [ip, idx]"
+  shows "vm_error (forth_leave_runtime vm)"
+  by (simp add: forth_leave_runtime_def set_error_def assms)
+
+lemma leave_runtime_normal:
+  assumes "return_stack vm = ip # idx # lim # rst"
+  shows "return_stack (forth_leave_runtime vm) = ip # lim # lim # rst"
+  by (simp add: forth_leave_runtime_def assms)
+
+(* ── UNLOOP ( -- ) : discard the innermost loop frame ─────────────────── *)
+(* C: rsp<2 -> error; else drop (limit,index), keep ip on top. *)
+
+definition forth_unloop :: "vm_state \<Rightarrow> vm_state" where
+  "forth_unloop vm =
+    (case return_stack vm of
+       ip # idx # lim # rst \<Rightarrow> vm\<lparr>return_stack := ip # rst\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma unloop_normal:
+  assumes "return_stack vm = ip # idx # lim # rst"
+  shows "return_stack (forth_unloop vm) = ip # rst"
+  by (simp add: forth_unloop_def assms)
+
+lemma unloop_data_stack_unchanged:
+  "data_stack (forth_unloop vm) = data_stack vm"
+  by (auto simp: forth_unloop_def set_error_def Let_def split: list.split)
+
+(* ── I ( -- i ) : innermost loop index ────────────────────────────────── *)
+
+definition forth_I :: "vm_state \<Rightarrow> vm_state" where
+  "forth_I vm =
+    (case return_stack vm of
+       ip # idx # lim # rst \<Rightarrow>
+         if ds_full vm then set_error vm else vm\<lparr>data_stack := idx # data_stack vm\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma I_normal:
+  assumes "return_stack vm = ip # idx # lim # rst"
+  assumes "\<not> ds_full vm"
+  shows "data_stack (forth_I vm) = idx # data_stack vm"
+  by (simp add: forth_I_def assms)
+
+lemma I_outside_loop_nil:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_I vm)"
+  by (simp add: forth_I_def set_error_def assms)
+
+lemma I_outside_loop_one:
+  assumes "return_stack vm = [ip]"
+  shows "vm_error (forth_I vm)"
+  by (simp add: forth_I_def set_error_def assms)
+
+lemma I_outside_loop_two:
+  assumes "return_stack vm = [ip, idx]"
+  shows "vm_error (forth_I vm)"
+  by (simp add: forth_I_def set_error_def assms)
+
+(* ── J ( -- j ) : next-outer loop index ───────────────────────────────── *)
+
+definition forth_J :: "vm_state \<Rightarrow> vm_state" where
+  "forth_J vm =
+    (case return_stack vm of
+       ip # idx # lim # outer_idx # outer_lim # rst \<Rightarrow>
+         if ds_full vm then set_error vm else vm\<lparr>data_stack := outer_idx # data_stack vm\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma J_normal:
+  assumes "return_stack vm = ip # idx # lim # outer_idx # outer_lim # rst"
+  assumes "\<not> ds_full vm"
+  shows "data_stack (forth_J vm) = outer_idx # data_stack vm"
+  by (simp add: forth_J_def assms)
+
+lemma J_needs_nested_loops_nil:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_J vm)"
+  by (simp add: forth_J_def set_error_def assms)
+
+lemma J_needs_nested_loops_one:
+  assumes "return_stack vm = [ip]"
+  shows "vm_error (forth_J vm)"
+  by (simp add: forth_J_def set_error_def assms)
+
+lemma J_needs_nested_loops_two:
+  assumes "return_stack vm = [ip, idx]"
+  shows "vm_error (forth_J vm)"
+  by (simp add: forth_J_def set_error_def assms)
+
+lemma J_needs_nested_loops_three:
+  assumes "return_stack vm = [ip, idx, lim]"
+  shows "vm_error (forth_J vm)"
+  by (simp add: forth_J_def set_error_def assms)
+
+lemma J_needs_nested_loops_four:
+  assumes "return_stack vm = [ip, idx, lim, outer_idx]"
+  shows "vm_error (forth_J vm)"
+  by (simp add: forth_J_def set_error_def assms)
+
+(* ── EXIT ( -- ) : one-shot return from the current colon definition ────── *)
+(* C: rsp<0 -> error; else vm->exit_colon = 1. The real interpreter loop
+   checks exit_colon after each word dispatch (per StarForth_Base.thy's
+   vm_state comment on exit_colon) -- this word only sets the flag. *)
+
+definition forth_exit :: "vm_state \<Rightarrow> vm_state" where
+  "forth_exit vm =
+    (case return_stack vm of
+       []  \<Rightarrow> set_error vm
+     | _   \<Rightarrow> vm\<lparr>exit_colon := True\<rparr>)"
+
+lemma exit_underflow:
+  assumes "return_stack vm = []"
+  shows "vm_error (forth_exit vm)"
+  by (simp add: forth_exit_def set_error_def assms)
+
+lemma exit_sets_flag:
+  assumes "return_stack vm \<noteq> []"
+  shows "exit_colon (forth_exit vm)"
+  using assms by (cases "return_stack vm") (auto simp: forth_exit_def)
+
+lemma exit_data_stack_unchanged:
+  "data_stack (forth_exit vm) = data_stack vm"
+  by (auto simp: forth_exit_def set_error_def Let_def split: list.split)
+
+(* ── Compile-time words -- NOT MODELLED, see the headline finding above ──
+   Named sentinels for greppability, matching the SP@/SP! and >BODY/etc.
+   conventions established in StarForth_Dictionary_Words.thy and
+   StarForth_Dictionary_Manipulation_Words.thy. *)
+
+lemma if_not_modelled: True        \<comment> \<open>IF: pushes a CF_IF marker onto the global cf_stack.\<close>
+  by simp
+lemma else_not_modelled: True      \<comment> \<open>ELSE: pops/pushes global cf_stack, patches vm->memory via vm->here.\<close>
+  by simp
+lemma then_not_modelled: True      \<comment> \<open>THEN: pops global cf_stack, patches vm->memory.\<close>
+  by simp
+lemma begin_not_modelled: True     \<comment> \<open>BEGIN: pushes a CF_BEGIN marker onto the global cf_stack.\<close>
+  by simp
+lemma while_not_modelled: True     \<comment> \<open>WHILE: peeks global cf_stack, pushes CF_WHILE.\<close>
+  by simp
+lemma repeat_not_modelled: True    \<comment> \<open>REPEAT: pops global cf_stack twice, patches vm->memory.\<close>
+  by simp
+lemma again_not_modelled: True     \<comment> \<open>AGAIN: pops global cf_stack, patches vm->memory.\<close>
+  by simp
+lemma until_not_modelled: True     \<comment> \<open>UNTIL: pops global cf_stack, patches vm->memory.\<close>
+  by simp
+lemma qdo_compile_not_modelled: True   \<comment> \<open>?DO (compiling half): pushes global cf_stack + leave_mark_stack.\<close>
+  by simp
+lemma do_compile_not_modelled: True    \<comment> \<open>DO (compiling half): pushes global cf_stack + leave_mark_stack.\<close>
+  by simp
+lemma leave_compile_not_modelled: True \<comment> \<open>LEAVE (compiling half): scans global cf_stack, pushes global leave_addrs.\<close>
+  by simp
+lemma loop_compile_not_modelled: True  \<comment> \<open>LOOP (compiling half): pops global cf_stack/leave_mark_stack, patches vm->memory.\<close>
+  by simp
+lemma plus_loop_compile_not_modelled: True \<comment> \<open>+LOOP (compiling half): same as LOOP's compiling half.\<close>
+  by simp
+lemma case_not_modelled: True      \<comment> \<open>CASE: pushes global cf_stack + endof_mark_stack.\<close>
+  by simp
+lemma of_not_modelled: True        \<comment> \<open>OF: scans global cf_stack, compiles calls to OVER/=/DROP by dictionary lookup.\<close>
+  by simp
+lemma endof_not_modelled: True     \<comment> \<open>ENDOF: pops global cf_stack, pushes global endof_addrs, patches vm->memory.\<close>
+  by simp
+lemma endcase_not_modelled: True   \<comment> \<open>ENDCASE: pops global cf_stack/endof_mark_stack, patches vm->memory.\<close>
+  by simp
+
+end