LithosAnanake/proof/StarForth_Dictionary_Manipulation_Words.thy

theory StarForth_Dictionary_Manipulation_Words
  imports StarForth_Base
begin

(* =========================================================================
   POST-07: Dictionary Manipulation Words
   Mirrors: src/word_source/dictionary_manipulation_words.c

   This file splits sharply into two classes:

   1. Mode/flag words ([, ], SMUDGE, HIDDEN, INTERPRET) -- provable against
      the existing vm_mode / dictionary / latest_id fields.

   2. Raw-pointer dictionary-navigation words (>BODY, >NAME, NAME>, >LINK,
      LINK>, CFA, LFA, NFA, PFA, TRAVERSE, FIND, ') -- NOT modelled. Every
      one of these casts a cell_t directly to/from a C `DictEntry*` and
      walks struct fields (name_len, link, the byte after the header) that
      have no counterpart in the abstract `dict_entry` record (StarForth_
      Base.thy:293), which is indexed abstractly by word_id, not by a raw
      memory address at all. This is the same class of gap already flagged
      for control_words.c's vm_ip/return-stack-as-raw-pointers (see that
      file's resume-point note) -- formalizing it would mean re-deriving
      the C struct layout (header size, name_len byte, link pointer
      arithmetic, body alignment) as a second, address-based dictionary
      model living alongside the existing word_id-based one. Out of scope
      for this pass; flagged per-word below as documented gaps, not lemmas.

      Per CLAUDE.md: `dictionary_m_word_find` (registered as "FIND") is the
      real, tested, non-standard FIND word ("parses from input stream").
      This file only *reads* it for modelling purposes here -- consistent
      with "never modify FIND", since nothing in proof/ touches the C
      source.

   ── Genuine findings, not fixed ──────────────────────────────────────────
   1. `[`, `]`, `STATE`, and `INTERPRET` all read/write a `static cell_t
      state_variable` at FILE SCOPE (line 49) -- NOT `vm->state_var`
      (include/vm.h:431, the real per-VM STATE field actively used by
      vm.c/vm_core.c/vm_bootstrap.c/capsule_loader.c on both hosted and
      kernel builds). This static is a single process-wide variable, not
      even per-VM: in the Tripod multi-VM fleet, EVERY VM's `[`/`]`/
      `INTERPRET` mutates the SAME shared cell, and `STATE` pushes ITS
      address (a bare host pointer, not a VM address) -- identical across
      every VM instance. `vm->state_var` itself is correctly toggled
      elsewhere in the real interpreter loop, so the dictionary-space
      compile/interpret bookkeeping isn't broken, but these four FORTH
      words are effectively wired to a dead, cross-VM-shared shadow
      variable instead of the VM's own state. Modelled below using only
      `vm_mode` (which `[`/`]` DO correctly set) -- the dead static write
      has no vm_state counterpart and is simply omitted, not "fixed".
   2. `dictionary_m_word_hidden`'s `#else` fallback branch (taken only if
      `WORD_HIDDEN` is undefined -- it is always defined per include/vm.h:
      181, so this branch is dead in every build configuration seen) calls
      `dictionary_word_smudge`, which does not exist: the real function in
      this file is `static void dictionary_m_word_smudge` (note the `_m_`
      and `static` -- not externally callable even if the name were right).
      Latent compile-time bug, unreachable under current WORD_HIDDEN
      always-defined builds. Not modelled (dead branch), not fixed.
   ======================================================================== *)

(* ── [ ( -- ) : enter interpretation mode ─────────────────────────────── *)
(* C: vm->mode = MODE_INTERPRET; state_variable = 0 (dead static, see above). *)

definition forth_left_bracket :: "vm_state \<Rightarrow> vm_state" where
  "forth_left_bracket vm = vm\<lparr>vm_mode := ModeInterpret\<rparr>"

lemma left_bracket_sets_interpret:
  "vm_mode (forth_left_bracket vm) = ModeInterpret"
  by (simp add: forth_left_bracket_def)

lemma left_bracket_data_stack_unchanged:
  "data_stack (forth_left_bracket vm) = data_stack vm"
  by (simp add: forth_left_bracket_def)

lemma left_bracket_never_errors:
  "vm_error (forth_left_bracket vm) = vm_error vm"
  by (simp add: forth_left_bracket_def)

(* ── ] ( -- ) : enter compilation mode ─────────────────────────────────── *)
(* C: vm->mode = MODE_COMPILE; state_variable = -1 (dead static, see above). *)

definition forth_right_bracket :: "vm_state \<Rightarrow> vm_state" where
  "forth_right_bracket vm = vm\<lparr>vm_mode := ModeCompile\<rparr>"

lemma right_bracket_sets_compile:
  "vm_mode (forth_right_bracket vm) = ModeCompile"
  by (simp add: forth_right_bracket_def)

lemma right_bracket_data_stack_unchanged:
  "data_stack (forth_right_bracket vm) = data_stack vm"
  by (simp add: forth_right_bracket_def)

lemma right_bracket_never_errors:
  "vm_error (forth_right_bracket vm) = vm_error vm"
  by (simp add: forth_right_bracket_def)

(* ── [ then ] / ] then [ : mode is exactly what was set last ─────────────── *)

lemma bracket_right_then_left:
  "vm_mode (forth_left_bracket (forth_right_bracket vm)) = ModeInterpret"
  by (simp add: forth_left_bracket_def)

lemma bracket_left_then_right:
  "vm_mode (forth_right_bracket (forth_left_bracket vm)) = ModeCompile"
  by (simp add: forth_right_bracket_def)

(* ── STATE ( -- addr ) -- NOT MODELLED ────────────────────────────────── *)

lemma state_not_modelled: True
  \<comment> \<open>STATE pushes `(cell_t)(uintptr_t)&state_variable` -- the address of a
     bare host C static, not a VM address and not `vm->state_addr`/
     `vm->state_var` (which DO exist in the abstract model and ARE the real
     per-VM state, see the file-level finding above). There is nothing in
     vm_state for this word to legitimately push; modelling it would mean
     inventing a fake address for a variable outside the VM's own address
     space entirely. Left undocumented as a lemma, gap only.\<close>
  by simp

(* ── SMUDGE ( -- ) : compile-only guard, empty body ──────────────────────── *)
(* C: error unless vm->mode == MODE_COMPILE; the "existing body that toggles
   the smudge bit" is literally absent (comment placeholder only, no code).
   So the word's entire effect, when it doesn't error, is: nothing. *)

definition forth_smudge :: "vm_state \<Rightarrow> vm_state" where
  "forth_smudge vm = (if vm_mode vm \<noteq> ModeCompile then set_error vm else vm)"

lemma smudge_requires_compile_mode:
  assumes "vm_mode vm \<noteq> ModeCompile"
  shows "vm_error (forth_smudge vm)"
  by (simp add: forth_smudge_def set_error_def assms)

lemma smudge_in_compile_mode_is_noop:
  assumes "vm_mode vm = ModeCompile"
  shows "forth_smudge vm = vm"
  by (simp add: forth_smudge_def assms)

(* ── HIDDEN ( -- ) : set WORD_HIDDEN (0x40) on the latest word ──────────── *)
(* C: error unless vm->mode == MODE_COMPILE; error if vm->latest is NULL;
   else e->flags |= WORD_HIDDEN (the #else dead-branch, see file note #2,
   is unreachable and not modelled). *)

definition WORD_HIDDEN :: nat where "WORD_HIDDEN = 0x40"

definition forth_hidden :: "vm_state \<Rightarrow> vm_state" where
  "forth_hidden vm =
    (if vm_mode vm \<noteq> ModeCompile
     then set_error vm
     else case latest_id vm of
            None \<Rightarrow> set_error vm
          | Some wid \<Rightarrow>
              (case dictionary vm wid of
                 None \<Rightarrow> set_error vm
               | Some e \<Rightarrow>
                   vm\<lparr>dictionary := (dictionary vm)
                        (wid := Some (e\<lparr>de_flags := de_flags e OR WORD_HIDDEN\<rparr>))\<rparr>))"

lemma hidden_requires_compile_mode:
  assumes "vm_mode vm \<noteq> ModeCompile"
  shows "vm_error (forth_hidden vm)"
  by (simp add: forth_hidden_def set_error_def assms)

lemma hidden_requires_latest:
  assumes "vm_mode vm = ModeCompile"
  assumes "latest_id vm = None"
  shows "vm_error (forth_hidden vm)"
  by (simp add: forth_hidden_def set_error_def assms)

lemma hidden_requires_latest_present_in_dict:
  assumes "vm_mode vm = ModeCompile"
  assumes "latest_id vm = Some wid"
  assumes "dictionary vm wid = None"
  shows "vm_error (forth_hidden vm)"
  by (simp add: forth_hidden_def set_error_def assms)

lemma hidden_sets_flag:
  assumes "vm_mode vm = ModeCompile"
  assumes "latest_id vm = Some wid"
  assumes "dictionary vm wid = Some e"
  shows "\<exists>e'. dictionary (forth_hidden vm) wid = Some e' \<and>
              de_flags e' = de_flags e OR WORD_HIDDEN"
  using assms by (simp add: forth_hidden_def)

lemma hidden_data_stack_unchanged:
  "data_stack (forth_hidden vm) = data_stack vm"
  by (auto simp: forth_hidden_def set_error_def split: option.split)

(* ── INTERPRET ( -- ) ──────────────────────────────────────────────────── *)
(* C: vm->mode = MODE_INTERPRET; state_variable = 0 (dead static, see file
   note). Comment in the C source admits the word does not itself invoke
   the interpreter loop ("This word exists mainly for completeness and mode
   setting") -- so its real effect is identical to `[`. *)

definition forth_interpret :: "vm_state \<Rightarrow> vm_state" where
  "forth_interpret = forth_left_bracket"

lemma interpret_is_left_bracket:
  "forth_interpret vm = forth_left_bracket vm"
  by (simp add: forth_interpret_def)

lemma interpret_sets_interpret_mode:
  "vm_mode (forth_interpret vm) = ModeInterpret"
  by (simp add: forth_interpret_def forth_left_bracket_def)

(* ── Raw-pointer dictionary navigation -- NOT MODELLED ────────────────────
   See the file-level note at the top: >BODY, >NAME, NAME>, >LINK, LINK>,
   CFA, LFA, NFA, PFA, TRAVERSE, FIND, ' all cast cell_t <-> DictEntry* and
   walk struct-layout details (name_len, link, header-relative body offset)
   absent from the word_id-indexed abstract dict_entry model. Each gets a
   named sentinel lemma so the gap is greppable per word, matching the
   SP@/SP! convention in StarForth_Dictionary_Words.thy. *)

lemma to_body_not_modelled: True    \<comment> \<open>>BODY: xt -> DictEntry* -> data field addr (struct-relative pointer arithmetic).\<close>
  by simp
lemma to_name_not_modelled: True    \<comment> \<open>>NAME: xt -> DictEntry* -> &entry->name (struct field address).\<close>
  by simp
lemma name_to_not_modelled: True    \<comment> \<open>NAME>: linear scan of vm->latest chain by raw name-field pointer identity.\<close>
  by simp
lemma to_link_not_modelled: True    \<comment> \<open>>LINK (= LFA): addr -> DictEntry* -> &entry->link (struct field address).\<close>
  by simp
lemma link_from_not_modelled: True  \<comment> \<open>LINK>: dereferences a DictEntry** raw pointer.\<close>
  by simp
lemma cfa_not_modelled: True        \<comment> \<open>CFA: identity cast addr -> DictEntry* -> xt; no abstract counterpart needed but the cast itself is untyped.\<close>
  by simp
lemma nfa_not_modelled: True        \<comment> \<open>NFA: same struct-field address as >NAME.\<close>
  by simp
lemma pfa_not_modelled: True        \<comment> \<open>PFA: get_body_address -- header size + name_len + alignment arithmetic.\<close>
  by simp
lemma traverse_not_modelled: True   \<comment> \<open>TRAVERSE: raw byte-pointer arithmetic over a length-prefixed name field.\<close>
  by simp
lemma find_not_modelled: True       \<comment> \<open>FIND: parses input stream (vm_parse_word) + vm_find_word lookup, neither modelled anywhere in this suite yet. Per CLAUDE.md this is the real, tested, non-standard FIND -- read-only reference here, the C is untouched.\<close>
  by simp
lemma tick_not_modelled: True       \<comment> \<open>' (tick): identical parse+lookup dependency as FIND, plus a not-found error path FIND itself doesn't have.\<close>
  by simp

end