theory StarForth_System_Words
  imports StarForth_Base
begin

(* =========================================================================
   POST-14: System Words
   Mirrors: src/word_source/system_words.c (16 registered words, plus the
            internal (ABORT") runtime helper)

   ── Genuine finding, not fixed: two MORE file-scope C statics doing
      per-VM-shaped work (5th and 6th occurrence of this pattern) ─────────
   `system_running` (written by every COLD/WARM via `reset_vm_state`) and
   `forth_79_standard` (read by `79-STANDARD`) are both `static int` at
   file scope in system_words.c -- not `struct VM` fields. Same bug class
   already found in control_words.c's `cf_stack`, dictionary_manipulation_
   words.c's `state_variable`, and string_words.c's `word_scratch_addr`
   (StarForth_Control_Words.thy, StarForth_Dictionary_Manipulation_Words.thy,
   StarForth_String_Words.thy) -- in the Tripod multi-VM fleet, one VM's
   COLD silently resets every other VM's "is the system running" flag, and
   79-STANDARD reports one shared compliance flag for all VMs regardless
   of which one asked. Five occurrences now; still worth the aggregated
   write-up the earlier files' notes flagged. Neither is modeled below
   (not per-VM state, nothing in vm_state corresponds to it) --
   `forth_79_standard` is instead threaded through as an explicit
   parameter, see `forth_79_standard_word` below.

   ── Genuine finding, not fixed: EXECUTE dereferences a raw host pointer
      from an attacker-controlled FORTH cell -- the most consequential
      instance of this sweep's raw-pointer-cast pattern ─────────────────
   `system_word_execute` casts the popped cell straight to a `DictEntry`
   host pointer (a C-style pointer cast, same shape as format_words.c's
   `?`/`DUMP`) then calls `entry->func(vm)` -- an indirect function-pointer
   CALL through
   a pointer built directly from a popped FORTH cell, gated only by a null
   check. This is the same category as format_words.c's `?`/`DUMP`
   (StarForth_Format_Words.thy) and this file's own `SEE`/`system_word_see`
   (which walks compiled threaded-code the same way), but strictly worse:
   `?`/`DUMP` are diagnostic corner words; EXECUTE is a core, ubiquitous
   FORTH-79 primitive (used by `'`/`DEFER`/every indirect-call idiom). Any
   FORTH code that computes, corrupts, or is tricked into supplying a bad
   "xt" value gets an unchecked indirect call through it -- not just an
   out-of-bounds read (the format_words.c findings) but arbitrary-code-
   execution shaped. Worth flagging to Bob as the highest-severity finding
   this sweep has produced so far. Also a plumbing/model mismatch: this
   suite's `word_table :: nat \<Rightarrow> vm_state \<Rightarrow> vm_state` (StarForth_Base.thy)
   models dispatch as word_id-indexed, but EXECUTE's real dispatch is via
   raw DictEntry pointers smuggled through cell_t values, not word_ids --
   the two dispatch pictures don't actually correspond for this word.

   MODELED (10 words): COLD, WARM, BYE, WORDS, VLIST, PAGE, NOP, QUIT,
   ABORT, EXECUTE (guard shape only, not dispatch), plus the internal
   `(ABORT")` runtime helper.

   NOT MODELED (7 words), each for a documented reason:
   - `(` / `\` (comments): parse via `vm_parse_word`/`input_pos` -- the
     same TIB/input-subsystem dependency string_words.c already deferred.
   - `SAVE-SYSTEM`: real host filesystem I/O (`fopen`/`fwrite` to
     "forth_system.img") -- entirely outside vm_state.
   - `79-STANDARD`: reads the file-scope static, see finding above.
   - `ABORT"` (compile-time immediate half): TIB-dependent message parsing
     PLUS compile-time codegen (`vm_allot`/`vm_compile_literal`/
     `vm_compile_call`), the same category as control_words.c's deferred
     compile-time half. Its interpret-mode runtime companion, `(ABORT")`,
     IS modeled (it has no TIB dependency -- flag/addr/len already on the
     stack by the time it runs).
   - `SEE`: TIB-dependent name parsing PLUS a raw-pointer threaded-code
     walk (same hazard class as EXECUTE, see finding above).
   - `REBOOT`: guard clauses modeled (see `forth_reboot_guards_*` below);
     the effectful tail is platform-branching -- real UEFI NVRAM writes
     and `ResetSystem` on `__STARKERNEL__` (genuine hardware I/O, no
     vm_state analog at all), vs. `vm_halted := True` on the hosted build
     (modeled, see `reboot_hosted_success_halts`).
   ======================================================================== *)

(* ── reset_vm_state helper (shared by COLD/WARM/ABORT/(ABORT")) ─────────── *)

definition reset_vm_state :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "reset_vm_state cold_start vm =
    (let vm1 = vm\<lparr>data_stack := [], return_stack := [],
                  vm_error := False, vm_mode := ModeInterpret\<rparr>
     in if cold_start \<and> here vm1 > 1024 then vm1\<lparr>here := 1024\<rparr> else vm1)"

lemma reset_vm_state_clears_stacks:
  "data_stack (reset_vm_state c vm) = []"
  "return_stack (reset_vm_state c vm) = []"
  by (simp_all add: reset_vm_state_def Let_def)

lemma reset_vm_state_clears_error_and_interprets:
  "vm_error (reset_vm_state c vm) = False"
  "vm_mode (reset_vm_state c vm) = ModeInterpret"
  by (simp_all add: reset_vm_state_def Let_def)

lemma reset_vm_state_warm_preserves_here:
  "here (reset_vm_state False vm) = here vm"
  by (simp add: reset_vm_state_def Let_def)

lemma reset_vm_state_cold_clamps_here:
  assumes "here vm > 1024"
  shows "here (reset_vm_state True vm) = 1024"
  using assms by (simp add: reset_vm_state_def Let_def)

lemma reset_vm_state_cold_preserves_small_here:
  assumes "here vm \<le> 1024"
  shows "here (reset_vm_state True vm) = here vm"
  using assms by (simp add: reset_vm_state_def Let_def)

(* ── COLD / WARM ( -- ) ───────────────────────────────────────────────── *)

definition forth_cold :: "vm_state \<Rightarrow> vm_state" where
  "forth_cold vm = reset_vm_state True vm"

definition forth_warm :: "vm_state \<Rightarrow> vm_state" where
  "forth_warm vm = reset_vm_state False vm"

lemma cold_is_reset_true: "forth_cold vm = reset_vm_state True vm"
  by (simp add: forth_cold_def)
lemma warm_is_reset_false: "forth_warm vm = reset_vm_state False vm"
  by (simp add: forth_warm_def)

(* ── BYE ( -- ) ───────────────────────────────────────────────────────── *)

definition forth_bye :: "vm_state \<Rightarrow> vm_state" where
  "forth_bye vm = vm\<lparr>vm_halted := True\<rparr>"

lemma bye_halts: "vm_halted (forth_bye vm) = True"
  by (simp add: forth_bye_def)
lemma bye_preserves_stacks:
  "data_stack (forth_bye vm) = data_stack vm"
  "return_stack (forth_bye vm) = return_stack vm"
  by (simp_all add: forth_bye_def)

(* ── WORDS / VLIST / PAGE / NOP ( -- ) : pure I/O or true no-ops ────────── *)

definition forth_words :: "vm_state \<Rightarrow> vm_state" where "forth_words vm = vm"
definition forth_vlist :: "vm_state \<Rightarrow> vm_state" where "forth_vlist vm = vm"
definition forth_page  :: "vm_state \<Rightarrow> vm_state" where "forth_page  vm = vm"
definition forth_nop   :: "vm_state \<Rightarrow> vm_state" where "forth_nop   vm = vm"

lemma words_is_identity: "forth_words vm = vm" by (simp add: forth_words_def)
lemma vlist_is_identity: "forth_vlist vm = vm" by (simp add: forth_vlist_def)
lemma page_is_identity:  "forth_page vm = vm"  by (simp add: forth_page_def)
lemma nop_is_identity:   "forth_nop vm = vm"   by (simp add: forth_nop_def)

(* ── 79-STANDARD ( -- flag ) : reads a non-per-VM global, see finding ───── *)
(* Threaded through as an explicit parameter rather than pretending it's
   vm_state, since it genuinely is not (file-scope C static). *)

definition forth_79_standard_word :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_79_standard_word compliant vm =
    vm\<lparr>data_stack := (if compliant then forth_true else forth_false) # data_stack vm\<rparr>"

lemma standard_pushes_flag:
  "data_stack (forth_79_standard_word compliant vm) =
     (if compliant then forth_true else forth_false) # data_stack vm"
  by (simp add: forth_79_standard_word_def)

(* ── QUIT ( -- ) : IMMEDIATE, forbidden inside a compiling definition ───── *)

definition forth_quit :: "vm_state \<Rightarrow> vm_state" where
  "forth_quit vm =
    (if vm_mode vm = ModeCompile then set_error vm
     else vm\<lparr>return_stack := [], vm_mode := ModeInterpret, vm_error := False\<rparr>)"

lemma quit_in_compile_mode_errors:
  assumes "vm_mode vm = ModeCompile"
  shows "vm_error (forth_quit vm)"
  using assms by (simp add: forth_quit_def set_error_def)

lemma quit_in_interpret_mode_resets:
  assumes "vm_mode vm = ModeInterpret"
  shows "return_stack (forth_quit vm) = []"
    and "vm_mode (forth_quit vm) = ModeInterpret"
    and "vm_error (forth_quit vm) = False"
  using assms by (simp_all add: forth_quit_def)

lemma quit_preserves_data_stack:
  "data_stack (forth_quit vm) = data_stack vm"
  by (simp add: forth_quit_def set_error_def)

(* ── ABORT ( -- ) : full reset + abort_req flag, NOT an error ───────────── *)

definition forth_abort :: "vm_state \<Rightarrow> vm_state" where
  "forth_abort vm = (reset_vm_state False vm)\<lparr>abort_req := True\<rparr>"

lemma abort_sets_abort_req:
  "abort_req (forth_abort vm) = True"
  by (simp add: forth_abort_def)
lemma abort_clears_error:
  "vm_error (forth_abort vm) = False"
  by (simp add: forth_abort_def reset_vm_state_def Let_def)
lemma abort_clears_stacks:
  "data_stack (forth_abort vm) = []"
  "return_stack (forth_abort vm) = []"
  by (simp_all add: forth_abort_def reset_vm_state_def Let_def)

(* ── (ABORT") runtime ( flag addr len -- ) : interpret-only stack helper ── *)
(* Address/length bounds check inlined the same way StarForth_IO_Words.thy's
   TYPE does (concrete VM_MEMORY_SIZE comparison), not the Memory_Words.thy
   `valid_addr` placeholder (which is unconditionally True and would make
   the bounds-fail branch unreachable in this model). *)

definition forth_runtime_abortq :: "vm_state \<Rightarrow> vm_state" where
  "forth_runtime_abortq vm =
    (case data_stack vm of
       len # addr # flag # rest \<Rightarrow>
         if flag = 0 then vm\<lparr>data_stack := rest\<rparr>
         else if addr <s 0 \<or> len <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + len)
         then set_error (vm\<lparr>data_stack := rest\<rparr>)
         else (reset_vm_state False (vm\<lparr>data_stack := rest\<rparr>))
     | _ \<Rightarrow> set_error vm)"

lemma runtime_abortq_underflow:
  assumes "length (data_stack vm) < 3"
  shows "vm_error (forth_runtime_abortq vm)"
  using assms
  by (auto simp add: forth_runtime_abortq_def set_error_def split: list.split)

lemma runtime_abortq_false_flag_is_noop_pop:
  assumes "data_stack vm = len # addr # 0 # rest"
  shows "data_stack (forth_runtime_abortq vm) = rest"
    and "vm_error (forth_runtime_abortq vm) = vm_error vm"
  using assms by (simp_all add: forth_runtime_abortq_def)

lemma runtime_abortq_bounds_fail_errors:
  assumes "data_stack vm = len # addr # flag # rest" "flag \<noteq> 0"
  assumes "addr <s 0 \<or> len <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + len)"
  shows "vm_error (forth_runtime_abortq vm)"
  using assms by (simp add: forth_runtime_abortq_def set_error_def)

lemma runtime_abortq_success_resets_everything:
  assumes "data_stack vm = len # addr # flag # rest" "flag \<noteq> 0"
  assumes "\<not> (addr <s 0 \<or> len <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + len))"
  shows "data_stack (forth_runtime_abortq vm) = []"
    and "return_stack (forth_runtime_abortq vm) = []"
    and "vm_error (forth_runtime_abortq vm) = False"
    and "vm_mode (forth_runtime_abortq vm) = ModeInterpret"
  using assms by (simp_all add: forth_runtime_abortq_def reset_vm_state_def Let_def)

(* ── EXECUTE ( xt -- ) : guard shape only, dispatch is the finding above ── *)

definition forth_execute :: "vm_state \<Rightarrow> vm_state" where
  "forth_execute vm =
    (case data_stack vm of
       []       \<Rightarrow> set_error vm
     | xt # rest \<Rightarrow>
         if xt = 0 then set_error (vm\<lparr>data_stack := rest\<rparr>)
         else vm\<lparr>data_stack := rest\<rparr>)  \<comment> \<open>indirect call via raw pointer, unmodelled -- see finding\<close>"

lemma execute_underflow: "data_stack vm = [] \<Longrightarrow> vm_error (forth_execute vm)"
  by (simp add: forth_execute_def set_error_def)
lemma execute_null_xt_errors:
  "data_stack vm = 0 # rest \<Longrightarrow> vm_error (forth_execute vm) \<and> data_stack (forth_execute vm) = rest"
  by (simp add: forth_execute_def set_error_def)
lemma execute_pops_one:
  "data_stack vm = xt # rest \<Longrightarrow> data_stack (forth_execute vm) = rest"
  by (simp add: forth_execute_def)

(* ── REBOOT ( addr len -- ) : guards modeled; hosted success tail modeled ─ *)

definition KERNEL_ARGS_CMDLINE_MAX :: nat where "KERNEL_ARGS_CMDLINE_MAX = 512"
  \<comment> \<open>○ CODE-MUST-MATCH: #define KERNEL_ARGS_CMDLINE_MAX 512 in
     include/starkernel/kernel_args.h\<close>

definition forth_reboot_guards_ok :: "vm_state \<Rightarrow> bool" where
  "forth_reboot_guards_ok vm =
    (vm_mode vm \<noteq> ModeCompile \<and> length (data_stack vm) \<ge> 2 \<and>
     (case data_stack vm of len # addr # _ \<Rightarrow>
        0 <s len \<and> len <s word_of_nat KERNEL_ARGS_CMDLINE_MAX \<and>
        \<not> (addr <s 0 \<or> len <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + len))
      | _ \<Rightarrow> False))"

(* No single total `forth_reboot` is defined -- only the guard predicate
   and the two named error/success facts below -- since the effectful tail
   genuinely branches on a compile-time #ifdef that has no single vm_state
   transition to name. The four REBOOT guard-failure facts, each
   independent of the others: *)

lemma reboot_guard_compile_mode:
  "vm_mode vm = ModeCompile \<Longrightarrow> \<not> forth_reboot_guards_ok vm"
  by (simp add: forth_reboot_guards_ok_def)

lemma reboot_guard_underflow:
  "length (data_stack vm) < 2 \<Longrightarrow> \<not> forth_reboot_guards_ok vm"
  by (simp add: forth_reboot_guards_ok_def)

lemma reboot_guard_len_range:
  assumes "data_stack vm = len # addr # rest"
  assumes "\<not> (0 <s len \<and> len <s word_of_nat KERNEL_ARGS_CMDLINE_MAX)"
  shows "\<not> forth_reboot_guards_ok vm"
  using assms by (auto simp add: forth_reboot_guards_ok_def)

lemma reboot_guard_addr_bounds:
  assumes "data_stack vm = len # addr # rest"
  assumes "addr <s 0 \<or> len <s 0 \<or> word_of_nat VM_MEMORY_SIZE <s (addr + len)"
  shows "\<not> forth_reboot_guards_ok vm"
  using assms by (auto simp add: forth_reboot_guards_ok_def)

(* Hosted-build success tail (the `#else` branch of the C `#ifdef
   __STARKERNEL__`): prints a stub message, then halts. The kernel-build
   branch (EFI NVRAM write + ResetSystem) has no vm_state analog and is
   not modeled at all. *)

definition forth_reboot_hosted_tail :: "vm_state \<Rightarrow> vm_state" where
  "forth_reboot_hosted_tail vm = vm\<lparr>data_stack := drop 2 (data_stack vm), vm_halted := True\<rparr>"

lemma reboot_hosted_success_halts:
  assumes "forth_reboot_guards_ok vm"
  shows "vm_halted (forth_reboot_hosted_tail vm) = True"
  using assms by (simp add: forth_reboot_hosted_tail_def)

end