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>Superseded by forth_is_full below (name parse and DF store are now
     modelled; only the FIND lookup and identity check are sidestepped,
     not left as a blank "not modelled"). Kept for its accurate
     description of the OLD state, not deleted.\<close>
  by simp

(* ── IS, full composition (FIND sidestepped), gap (a)+(b) CLOSED where
   reachable, 2026-08-15 ───────────────────────────────────────────────────
   `word_is` (defer_words.c:112-154): underflow guard -> pop xt -> parse
   name -> vm_find_word -> `de->func != defer_runtime` identity check ->
   DF store. `vm_find_word` and the identity check are both unmodellable
   in this suite (FIND-family name-resolution gap; `word_table` exposes
   no per-entry function-identity query) -- sidestepped the same way
   `physics_freeze_words.c`'s FREEZE-WORD/UNFREEZE-WORD/etc. already
   sidestep the identical shape: parameterised over an explicit
   `target_wid_opt :: nat option` (standing in for whatever vm_find_word
   would have resolved) and `is_defer_word :: bool` (standing in for the
   identity check's result). Given both, the DF store itself is fully
   modelled via `dict_write_df`. *)

definition forth_is_full :: "nat \<Rightarrow> nat option \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_is_full max_len target_wid_opt is_defer_word vm =
    (if data_stack vm = []
     then set_error vm
     else
       let xt        = hd (data_stack vm);
           vm1       = vm\<lparr>data_stack := tl (data_stack vm)\<rparr>;
           (nm, vm2) = forth_parse_word max_len vm1
       in if nm = ''''
          then set_error vm2
          else case target_wid_opt of
                 None \<Rightarrow> set_error vm2
               | Some wid \<Rightarrow>
                   if \<not> is_defer_word
                   then set_error vm2
                   else dict_write_df wid xt vm2)"

lemma is_full_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)"
  by (simp add: forth_is_full_def set_error_def assms)

lemma is_full_not_found_errors:
  assumes "data_stack vm \<noteq> []"
  assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
  assumes "target_wid_opt = None"
  shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)"
proof -
  obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
    by fastforce
  hence "nm \<noteq> ''''" using assms(2) by simp
  thus ?thesis using assms(1) assms(3) parse_eq by (simp add: forth_is_full_def set_error_def)
qed

lemma is_full_not_defer_word_errors:
  assumes "data_stack vm \<noteq> []"
  assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
  assumes "target_wid_opt = Some wid" "\<not> is_defer_word"
  shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)"
proof -
  obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
    by fastforce
  hence "nm \<noteq> ''''" using assms(2) by simp
  thus ?thesis using assms(1) assms(3) assms(4) parse_eq by (simp add: forth_is_full_def set_error_def)
qed

lemma is_full_success_writes_df:
  assumes "data_stack vm \<noteq> []"
  assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
  assumes "target_wid_opt = Some wid" "is_defer_word"
  assumes "dictionary (snd (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>))) wid = Some e"
  shows "dictionary (forth_is_full max_len target_wid_opt is_defer_word vm) wid = Some (e\<lparr>de_df := hd (data_stack vm)\<rparr>)"
proof -
  obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
    by fastforce
  hence "nm \<noteq> ''''" using assms(2) by simp
  moreover have "dictionary vm2 wid = Some e" using assms(5) parse_eq by simp
  ultimately show ?thesis
    using assms(1) assms(3) assms(4) parse_eq dict_write_df_present
    by (simp add: forth_is_full_def)
qed

(* ── 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) -- structurally different from forth_runtime_read_df, since the DF value here is USED as a dispatch target, not just returned. Genuinely still not modelled, not superseded.\<close>
  by simp
lemma defer_fetch_not_modelled: True   \<comment> \<open>Superseded by forth_defer_fetch_full below, same as is_guard_rest_not_modelled above.\<close>
  by simp

(* ── DEFER@, full composition (FIND sidestepped), gap (a)+(b) CLOSED where
   reachable, 2026-08-15 ───────────────────────────────────────────────────
   `word_defer_fetch` (defer_words.c:161-198): parse name -> vm_find_word
   -> identity check -> DF read + push. Same sidestep as forth_is_full;
   the DF read itself is fully modelled via `de_df`, with the same
   `ds_full` guard `forth_runtime_read_df` already established for the
   equivalent vm_push() call. *)

definition forth_defer_fetch_full :: "nat \<Rightarrow> nat option \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_defer_fetch_full max_len target_wid_opt is_defer_word vm =
    (let (nm, vm1) = forth_parse_word max_len vm
     in if nm = ''''
        then set_error vm1
        else case target_wid_opt of
               None \<Rightarrow> set_error vm1
             | Some wid \<Rightarrow>
                 if \<not> is_defer_word
                 then set_error vm1
                 else case dictionary vm1 wid of
                        None \<Rightarrow> set_error vm1
                      | Some e \<Rightarrow>
                          if ds_full vm1
                          then set_error vm1
                          else vm1\<lparr>data_stack := de_df e # data_stack vm1\<rparr>)"

lemma defer_fetch_full_empty_parse_errors:
  assumes "fst (forth_parse_word max_len vm) = ''''"
  shows "vm_error (forth_defer_fetch_full max_len target_wid_opt is_defer_word 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_fetch_full_def set_error_def)
qed

lemma defer_fetch_full_success_pushes_df:
  assumes "fst (forth_parse_word max_len vm) \<noteq> ''''"
  assumes "target_wid_opt = Some wid" "is_defer_word"
  assumes "dictionary (snd (forth_parse_word max_len vm)) wid = Some e"
  assumes "\<not> ds_full (snd (forth_parse_word max_len vm))"
  shows "data_stack (forth_defer_fetch_full max_len target_wid_opt is_defer_word vm)
           = de_df e # data_stack (snd (forth_parse_word max_len vm))"
proof -
  obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce
  hence nm_nonempty: "nm \<noteq> ''''" using assms(1) by simp
  have "dictionary vm1 wid = Some e" using assms(4) parse_eq by simp
  thus ?thesis
    using parse_eq nm_nonempty assms(2) assms(3) assms(5)
    by (simp add: forth_defer_fetch_full_def)
qed

end