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