theory StarForth_Defer_Words
  imports StarForth_Base
begin

(* =========================================================================
   Mirrors: src/word_source/defer_words.c
   Registers: DEFER IS DEFER@

   ── Duplicate-registration finding, same class as `[`/`]`/STATE ─────────
   `word_registry.c` registers `defining_words.c`'s DEFER/IS/DEFER@ at
   Module 17 (line 126) and THIS file's DEFER/IS/DEFER@ at Module 27
   (line 137) -- unconditionally, with no `#ifdef __STARKERNEL__` guarding
   either call. Despite CLAUDE.md categorising `defer_words.c` as a
   "kernel-side-only addition," the hosted `Makefile`'s `SRC` is a bare
   `wildcard src/word_source/*.c` (line 443) with no exclusion for this
   file, and `defer_words.c` itself has no `#ifndef __STARKERNEL__` guard
   the way `lifecycle_words_hosted.c` does -- so it compiles and registers
   in BOTH builds. Registered later, this file's DEFER/IS/DEFER@ SHADOW
   `defining_words.c`'s and are the only reachable versions in either
   build. **This corrects StarForth_Defining_Words.thy's
   `defer_not_modelled`/`is_not_modelled`/`defer_fetch_not_modelled`
   sentinels: those describe dead, shadowed code, not the live
   implementation.** (Those sentinels are still accurate as descriptions
   of what that dead code WOULD do, and the underlying model gaps this
   file hits below are the same ones anyway, so nothing there needs to be
   retracted -- just understood as describing unreachable code.)

   ── Why this file isn't more tractable despite being the live version ──
   Every one of DEFER/IS/DEFER@'s real effects still hits the same three
   gaps StarForth_Defining_Words.thy's file header names: (a) dictionary-
   entry creation (`vm_create_word`, used by DEFER), (b) data-field
   addressing (`vm_dictionary_get_data_field` -- DEFER's initial zero-set,
   IS's xt store, DEFER@'s xt fetch, and `defer_runtime`'s own read all
   depend on it), (c) mutable per-entry dispatch (`defer_runtime` reads a
   `DictEntry*` out of the DF cell and calls through it -- `word_table` is
   a fixed global in this suite's model, see StarForth_Base.thy). IS and
   DEFER@ additionally depend on `vm_find_word` (the FIND-family name-
   resolution gap) and a raw `de->func != defer_runtime` function-pointer
   identity comparison, itself unmodellable since `word_table` doesn't
   expose per-entry function identity as a queryable value in this model.

   ── Scope ─────────────────────────────────────────────────────────────
   Only IS's stack-underflow guard is modelled (the one real vm_state
   condition that doesn't depend on any of the above). Everything else in
   all three words is not modelled.
   ======================================================================== *)

(* ── IS ( xt -- ) : underflow guard only ──────────────────────────────── *)
(* C: `if (vm->dsp < 0) { ...; vm->error = 1; return; }` before popping xt
   -- i.e. needs at least one element. Everything after the pop (name
   parse, FIND, defer_runtime identity check, DF store) is unmodelled. *)

definition forth_is_guard :: "vm_state \<Rightarrow> vm_state" where
  "forth_is_guard vm =
    (if data_stack vm = [] then set_error vm else vm)"

lemma is_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_is_guard vm)"
  by (simp add: forth_is_guard_def set_error_def assms)

lemma is_guard_rest_not_modelled: True
  \<comment> \<open>Beyond the underflow guard: name parse (unmodelled TIB dependency),
     vm_find_word (FIND-family gap), the `func != defer_runtime` identity
     check (unmodellable -- word_table has no per-entry function-identity
     query in this model), and the DF store (gap b). See file header.\<close>
  by simp

lemma defer_not_modelled: True         \<comment> \<open>DEFER: vm_create_word (gap a) + DF zero-init (gap b).\<close>
  by simp
lemma defer_runtime_not_modelled: True \<comment> \<open>defer_runtime: DF read (gap b) + call-through (gap c).\<close>
  by simp
lemma defer_fetch_not_modelled: True   \<comment> \<open>DEFER@: FIND (name-resolution gap) + DF read (gap b).\<close>
  by simp

end
