LithosAnanake/proof/StarForth_Defer_Words.thy

theory StarForth_Defer_Words
  imports StarForth_Base StarForth_Defining_Words
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

(* ── DEFER: entry-creation half, gap (a) PARTIALLY CLOSED 2026-08-14 ─────
   `word_defer` (src/word_source/defer_words.c:73-101) calls
   `vm_create_word(vm, name, len, defer_runtime)` with no extra flags set
   afterward -- same shape as StarForth_Defining_Words.thy's CREATE/
   VARIABLE/CONSTANT, reusing `dict_insert_entry 0` directly. NOT modelled:
   the name parse (TIB gap), and the DF zero-init that follows (gap b). *)

definition forth_defer_entry_half :: "string \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_defer_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm"

lemma defer_entry_half_populates_dictionary:
  assumes "\<not> pinned_conflict"
  shows "\<exists>e. dictionary (forth_defer_entry_half name pinned_conflict vm) (word_id_next vm) = Some e
             \<and> de_name e = name \<and> de_flags e = 0"
  using assms by (simp add: forth_defer_entry_half_def dict_insert_entry_def Let_def)

lemma defer_entry_half_pinned_conflict_errors:
  assumes "pinned_conflict"
  shows "vm_error (forth_defer_entry_half name pinned_conflict vm)"
  using assms by (simp add: forth_defer_entry_half_def dict_insert_entry_def set_error_def)

lemma defer_not_modelled: True         \<comment> \<open>DEFER beyond the entry-creation half: DF zero-init (gap b). See forth_defer_full below for the parse composition.\<close>
  by simp

(* ── DEFER, full composition, gap (a)+parse CLOSED 2026-08-15 ────────────
   `word_defer` (defer_words.c:73-101): parse name -> vm_create_word. No
   align/allot, no stack guard -- the simplest full composition in this
   suite. Same pattern as StarForth_Defining_Words.thy's forth_create_full/
   forth_constant_full/forth_variable_full. *)

definition forth_defer_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_defer_full max_len pinned_conflict vm =
    (let (nm, vm1) = forth_parse_word max_len vm
     in if nm = ''''
        then set_error vm1
        else dict_insert_entry nm 0 pinned_conflict vm1)"

lemma defer_full_empty_parse_errors:
  assumes "fst (forth_parse_word max_len vm) = ''''"
  shows "vm_error (forth_defer_full max_len pinned_conflict vm)"
proof -
  obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce
  hence "nm = ''''" using assms by simp
  thus ?thesis using parse_eq by (simp add: forth_defer_full_def set_error_def)
qed

lemma defer_full_success_populates_dictionary:
  assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \<noteq> []" (is "?s1 \<noteq> []")
  assumes "max_len \<ge> 2"
  assumes "\<not> pinned_conflict"
  shows "\<exists>e wid. dictionary (forth_defer_full max_len pinned_conflict vm) wid = Some e
                \<and> de_name e \<noteq> '''' \<and> de_flags e = 0"
proof -
  obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce
  hence nm_nonempty: "nm \<noteq> ''''"
    using forth_parse_word_success_nonempty[OF assms(1) assms(2)] by (metis fstI)
  have "forth_defer_full max_len pinned_conflict vm = dict_insert_entry nm 0 pinned_conflict vm1"
    using parse_eq nm_nonempty by (simp add: forth_defer_full_def)
  moreover have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) (word_id_next vm1) = Some e
                     \<and> de_name e = nm \<and> de_flags e = 0"
    using assms(3) by (simp add: dict_insert_entry_def Let_def)
  ultimately show ?thesis using nm_nonempty by auto
qed
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