theory StarForth_Defining_Words
  imports StarForth_Base StarForth_Memory_Words ACL_Pin_Monotone
begin

(* =========================================================================
   Mirrors: src/word_source/defining_words.c
   Registers: : ; CREATE VARIABLE CONSTANT IMMEDIATE STATE [ ] FORGET
              COMPILE [COMPILE] LIT LITERAL does_rt DOES> DEFER IS DEFER@

   ── Duplicate-registration finding (corrects a StarForth_Dictionary_
      Manipulation_Words.thy note) ────────────────────────────────────────
   `src/word_registry.c` registers dictionary_manipulation_words.c's `[`,
   `]`, `STATE` (Module 13, line 122) BEFORE defining_words.c's `[`, `]`,
   `STATE` (Module 17, line 126). FORTH dictionary lookup finds the MOST
   RECENT definition of a name first, so defining_words.c's versions are
   the only ones ever reachable -- dictionary_manipulation_words.c's `[`/
   `]`/`STATE` are permanently shadowed, dead code from the moment boot
   registration completes. CORRECTED 2026-08-14: `INTERPRET` is NOT part of
   this shadow -- defining_words.c never registers a word named INTERPRET
   at all (confirmed by grep), so dictionary_manipulation_words.c's
   INTERPRET is the only registration that exists and is live, not dead.
   The earlier version of this note (and proof/FINDINGS.md) incorrectly
   folded it into the shadowed group.

   This also CORRECTS that file's finding, not just supersedes it: its
   `[`/`]`/`STATE` write/read a dead file-scope `static cell_t
   state_variable`, cross-VM-shared and never the real per-VM STATE. The
   LIVE versions here (defining_word_left_bracket/right_bracket/state) use
   `vm->state_addr` (include/vm.h:452) -- a genuine per-VM VM-memory
   address, correctly written via `vm_store_cell`. The dead-static bug is
   real IN THE SHADOWED CODE, but does not reach runtime: no VM instance's
   `[`/`]`/`STATE` actually touches that static. Added `state_addr :: nat`
   to vm_state (StarForth_Base.thy) to model this correctly.

   ── Scope of this file ──────────────────────────────────────────────────
   Split three ways:
   1. Mode/flag/address words ([, ], STATE, IMMEDIATE) -- fully modelled,
      provable against `vm_mode`/`state_addr`/`memory`/`dictionary`/
      `latest_id`.
   2. `:` / `;` -- guard conditions modelled; `:`'s STATE/mode-setting half
      of `vm_enter_compile_mode` is modelled (identical shape to `]`), AND
      (added 2026-08-14, see `dict_insert_entry` below) its dictionary-
      entry-creation half is now PARTIALLY modelled too
      (`forth_colon_entry_half`: fresh word_id, WORD_SMUDGED flag, ACL
      defaults) -- what remains unmodelled is named at that definition's
      site. `;`'s entire effect beyond the guard (`vm_exit_compile_mode`:
      find/compile EXIT, clear WORD_SMUDGED, set WORD_COMPILED, evict
      hot-words cache) is still NOT modelled, for the same reason plus
      dependence on the hot-words cache, itself never modelled in this
      suite.
   3. Everything else (CREATE, VARIABLE, CONSTANT partially modelled as of
      2026-08-14, see below; FORGET, COMPILE, [COMPILE], LIT, LITERAL,
      does_rt, DOES>, DEFER, IS, DEFER@, and the three defining-runtime
      functions CREATE/VARIABLE/CONSTANT install still NOT modelled) --
      each hits one or more of the same three model gaps, named once here
      rather than repeated per word:

      (a) DICTIONARY-ENTRY CREATION, PARTIALLY CLOSED 2026-08-14. Was not
          modelled anywhere in this proof suite: `dictionary :: nat \<Rightarrow>
          dict_entry option` (StarForth_Base.thy:498) was treated as a
          fixed, pre-populated table by every theory so far -- FIND/
          TRAVERSE/etc. in StarForth_Dictionary_Manipulation_Words.thy
          only READ it. This was the first file in the sweep whose primary
          job IS insertion (`:`, CREATE, VARIABLE, CONSTANT, DEFER all
          call `vm_create_word`). `dict_insert_entry` (defined below) now
          models the word_id-assignment/dictionary-table/latest_id/
          `word_id_next`-counter portion of `vm_create_word`, reusing the
          `word_id_next :: nat` field already declared in StarForth_
          Base.thy but never previously written by any theory. What
          remains unmodelled per word: `vm_create_word` itself parses no
          input (name arrives pre-parsed, but the parse producing that
          name is the TIB/input-subsystem gap, present throughout this
          suite), does not capture the entry into any per-VM
          `vm->compiling_word`-style tracking field (none exists in
          vm_state), and callers still mutate the returned `DictEntry*`
          directly afterward for flags beyond what `dict_insert_entry`'s
          `init_flags` parameter already captures. This is still a
          materially bigger gap than the raw-pointer-navigation gap
          already flagged in dictionary_manipulation_words.c (which only
          reads), even partially closed -- the single largest finding of
          this file remains real, just smaller than before.

      (b) DATA-FIELD (DF) ADDRESSING: `dict_entry` (StarForth_Base.thy:293)
          has no field corresponding to a DictEntry's data-field cell (the
          storage `vm_dictionary_get_data_field` returns a pointer into).
          CREATE/VARIABLE/CONSTANT's runtimes, DODOES, and does_rt all
          read or write this cell -- the exact gap already named for
          `>BODY` in StarForth_Dictionary_Manipulation_Words.thy
          (`to_body_not_modelled`). Same root cause, different words.

      (c) MUTABLE PER-ENTRY DISPATCH: `word_table` (StarForth_Base.thy:626)
          is a fixed, uninterpreted global constant -- by design (see that
          section's comment), not a per-VM-instance mutable field. DEFER's
          `IS` reassigns an entry's *effective* dispatch target at runtime
          (stored in the DF cell and read by `defining_runtime_defer`); a
          fixed `word_table` cannot express this at all, independent of
          gap (b).

      LIT additionally treats the top return-stack cell as a raw C
      `cell_t*` threaded-code instruction pointer, advanced with C pointer
      arithmetic (`rip++`) and dereferenced directly -- NOT as a VM address
      resolved through `vm_ptr`/`vm_addr_ok` the way control_words.c's
      return-stack-held IP values were (see StarForth_Control_Words.thy's
      resume note: that gap turned out to already be covered by `mem_read`
      on VM-address-valued return-stack entries). LIT's IP is a genuinely
      different, raw-host-pointer usage of the same field; the list-based
      `return_stack :: cell list` model has no way to hold or advance a
      host pointer.
   ======================================================================== *)

definition WORD_IMMEDIATE :: nat where "WORD_IMMEDIATE = 0x80"
definition WORD_SMUDGED   :: nat where "WORD_SMUDGED   = 0x20"

(* ── Dictionary-entry insertion (gap (a), PARTIALLY CLOSED 2026-08-14) ────
   `word_id_next` (StarForth_Base.thy, declared but never written by any
   theory before this one -- confirmed by grep) is exactly C's
   `vm->next_word_id`/`vm_dictionary_acquire_word_id` mechanism
   (src/dictionary_management.c:87-92,94-110): a monotonically increasing
   counter, one per fresh word, capped at DICTIONARY_SIZE. `vm_create_word`
   itself (dictionary_management.c:379-470) does three things this
   definition models and one it does not:
     1. Pin-shadow guard: scans vm->latest's linked list for a same-name
        PINNED entry; refuses (vm->error=1) if found. Sidestepped the same
        way StarForth_ACL_Words.thy/StarForth_Physics_Freeze_Words.thy
        sidestep the equivalent FIND-shaped dependency: parameterised over
        an explicit `pinned_conflict :: bool`, standing in for "whatever a
        real name-scan would have found."
     2. Allocates a `word_id` via the counter and installs the new entry
        into the word-id-indexed table (`vm->word_id_map` / this model's
        `dictionary`) -- modelled exactly, both are word_id-indexed.
     3. Prepends to `vm->latest`'s linked list, which is also what backs
        `latest_id` in this model.
   NOT modelled: the real `entry->func` (word_table -- a fixed,
   uninterpreted global per StarForth_Base.thy's design, cannot express a
   NEW word's dispatch target, which is gap (c)), the physics-metadata
   seed (`physics_metadata_init`/`apply_seed` -- modelled as all-zero
   `dict_physics`, not the real seeding logic), and the DF cell (gap (b),
   unchanged). ACL fields are modelled exactly from the C's literal
   initializers (acl_ttl=0, acl_allow=True, acl_mode=ACL_MODE_TTL=0,
   acl_pinned=False) -- src/dictionary_management.c:427-430. *)

definition dict_insert_entry :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "dict_insert_entry init_flags pinned_conflict vm =
    (if pinned_conflict
     then set_error vm
     else
       let wid = word_id_next vm;
           e = \<lparr>de_name = '''', de_flags = init_flags, de_heat = 0,
                de_word_id = wid,
                de_physics = \<lparr>dp_temperature_q8 = 0, dp_last_active_ns = 0,
                               dp_last_decay_ns = 0, dp_mass_bytes = 0,
                               dp_avg_latency_ns = 0, dp_state_flags = 0\<rparr>,
                de_acl_ttl = 0, de_acl_allow = True, de_acl_mode = ACL_MODE_TTL,
                de_acl_pinned = False\<rparr>
       in vm\<lparr>dictionary := (dictionary vm)(wid := Some e),
             latest_id := Some wid,
             word_id_next := wid + 1\<rparr>)"

lemma dict_insert_entry_pinned_conflict_errors:
  assumes "pinned_conflict"
  shows "vm_error (dict_insert_entry init_flags pinned_conflict vm)"
  by (simp add: dict_insert_entry_def set_error_def assms)

lemma dict_insert_entry_assigns_fresh_word_id:
  assumes "\<not> pinned_conflict"
  shows "latest_id (dict_insert_entry init_flags pinned_conflict vm) = Some (word_id_next vm)"
  using assms by (simp add: dict_insert_entry_def Let_def)

lemma dict_insert_entry_populates_dictionary:
  assumes "\<not> pinned_conflict"
  shows "\<exists>e. dictionary (dict_insert_entry init_flags pinned_conflict vm) (word_id_next vm) = Some e
             \<and> de_word_id e = word_id_next vm \<and> de_flags e = init_flags \<and> de_heat e = 0
             \<and> de_acl_ttl e = 0 \<and> de_acl_allow e \<and> de_acl_mode e = ACL_MODE_TTL \<and> \<not> de_acl_pinned e"
  using assms by (simp add: dict_insert_entry_def Let_def)

lemma dict_insert_entry_advances_counter:
  assumes "\<not> pinned_conflict"
  shows "word_id_next (dict_insert_entry init_flags pinned_conflict vm) = word_id_next vm + 1"
  using assms by (simp add: dict_insert_entry_def Let_def)

lemma dict_insert_entry_data_stack_unchanged:
  "data_stack (dict_insert_entry init_flags pinned_conflict vm) = data_stack vm"
  by (simp add: dict_insert_entry_def set_error_def Let_def)

lemma dict_insert_entry_not_full_word_id_next_bound: True
  \<comment> \<open>NOT modelled: the C's `word_id_next >= DICTIONARY_SIZE` exhaustion
     branch (dictionary_management.c:87-91,102), which returns
     WORD_ID_INVALID and skips the `word_id_map` write while the linked-
     list prepend to vm->latest still happens unconditionally regardless.
     This model always succeeds at installing into `dictionary` once past
     the pin guard -- a real, uncovered edge case (a VM that defines more
     than DICTIONARY_SIZE words), not claimed to be handled.\<close>
  by simp

(* ── [ ( -- ) : interpret mode, LIVE version (see file header) ──────────── *)
(* C: vm_store_cell(vm, vm->state_addr, 0); vm->mode = MODE_INTERPRET. *)

definition forth_d_left_bracket :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_left_bracket vm =
     vm\<lparr>memory  := mem_write (memory vm) (state_addr vm) 0,
        vm_mode := ModeInterpret\<rparr>"

lemma d_left_bracket_sets_interpret:
  "vm_mode (forth_d_left_bracket vm) = ModeInterpret"
  by (simp add: forth_d_left_bracket_def)

lemma d_left_bracket_writes_state_cell:
  "mem_read (memory (forth_d_left_bracket vm)) (state_addr vm) = 0"
  by (simp add: forth_d_left_bracket_def mem_read_def mem_write_def)

lemma d_left_bracket_data_stack_unchanged:
  "data_stack (forth_d_left_bracket vm) = data_stack vm"
  by (simp add: forth_d_left_bracket_def)

lemma d_left_bracket_never_errors:
  "vm_error (forth_d_left_bracket vm) = vm_error vm"
  by (simp add: forth_d_left_bracket_def)

(* ── ] ( -- ) : compile mode, LIVE version ───────────────────────────────── *)
(* C: vm_store_cell(vm, vm->state_addr, (cell_t)-1); vm->mode = MODE_COMPILE. *)

definition forth_d_right_bracket :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_right_bracket vm =
     vm\<lparr>memory  := mem_write (memory vm) (state_addr vm) (-1),
        vm_mode := ModeCompile\<rparr>"

lemma d_right_bracket_sets_compile:
  "vm_mode (forth_d_right_bracket vm) = ModeCompile"
  by (simp add: forth_d_right_bracket_def)

lemma d_right_bracket_writes_state_cell:
  "mem_read (memory (forth_d_right_bracket vm)) (state_addr vm) = -1"
  by (simp add: forth_d_right_bracket_def mem_read_def mem_write_def)

lemma d_right_bracket_data_stack_unchanged:
  "data_stack (forth_d_right_bracket vm) = data_stack vm"
  by (simp add: forth_d_right_bracket_def)

lemma d_right_bracket_never_errors:
  "vm_error (forth_d_right_bracket vm) = vm_error vm"
  by (simp add: forth_d_right_bracket_def)

lemma d_bracket_right_then_left:
  "vm_mode (forth_d_left_bracket (forth_d_right_bracket vm)) = ModeInterpret"
  by (simp add: forth_d_left_bracket_def)

lemma d_bracket_left_then_right:
  "vm_mode (forth_d_right_bracket (forth_d_left_bracket vm)) = ModeCompile"
  by (simp add: forth_d_right_bracket_def)

(* ── STATE ( -- addr ) : LIVE version, pushes a real VM address ─────────── *)
(* C: vm_push(vm, (cell_t)vm->state_addr). Unlike the shadowed dictionary_
   manipulation_words.c version (which pushed the address of a dead host
   static, and was left unmodelled), this pushes `state_addr` -- a genuine
   per-VM field, so this word IS modellable. *)

definition forth_d_state :: "vm_state \<Rightarrow> vm_state" where
  "forth_d_state vm =
    (if ds_full vm
     then set_error vm
     else vm\<lparr>data_stack := word_of_nat (state_addr vm) # data_stack vm\<rparr>)"

lemma d_state_normal:
  assumes "\<not> ds_full vm"
  shows "data_stack (forth_d_state vm) = word_of_nat (state_addr vm) # data_stack vm"
  by (simp add: forth_d_state_def assms)

lemma d_state_overflow:
  assumes "ds_full vm"
  shows "vm_error (forth_d_state vm)"
  by (simp add: forth_d_state_def set_error_def assms)

lemma d_state_preserves_state_addr:
  "state_addr (forth_d_state vm) = state_addr vm"
  by (simp add: forth_d_state_def set_error_def)

(* ── IMMEDIATE ( -- ) : mark latest word immediate, no mode guard ───────── *)
(* C: error if vm->latest is NULL; else vm->latest->flags |= WORD_IMMEDIATE.
   Unlike HIDDEN (dictionary_manipulation_words.c), there is no compile-mode
   guard at all. *)

definition forth_immediate :: "vm_state \<Rightarrow> vm_state" where
  "forth_immediate vm =
    (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_IMMEDIATE\<rparr>))\<rparr>))"

lemma immediate_requires_latest:
  assumes "latest_id vm = None"
  shows "vm_error (forth_immediate vm)"
  by (simp add: forth_immediate_def set_error_def assms)

lemma immediate_requires_latest_present_in_dict:
  assumes "latest_id vm = Some wid"
  assumes "dictionary vm wid = None"
  shows "vm_error (forth_immediate vm)"
  by (simp add: forth_immediate_def set_error_def assms)

lemma immediate_sets_flag:
  assumes "latest_id vm = Some wid"
  assumes "dictionary vm wid = Some e"
  shows "\<exists>e'. dictionary (forth_immediate vm) wid = Some e' \<and>
              de_flags e' = de_flags e OR WORD_IMMEDIATE"
  using assms by (simp add: forth_immediate_def)

lemma immediate_data_stack_unchanged:
  "data_stack (forth_immediate vm) = data_stack vm"
  by (auto simp: forth_immediate_def set_error_def split: option.split)

lemma immediate_no_mode_guard:
  \<comment> \<open>Unlike HIDDEN, IMMEDIATE has no `vm_mode vm \<noteq> ModeCompile` check at
     all -- when the latest-word guards above are satisfied, its error
     status is exactly whatever it was on entry (no NEW error is raised by
     a compile-mode check, since there is none). Stated explicitly since
     every other flag-setting word in this sweep (SMUDGE, HIDDEN) DOES gate
     on compile mode.\<close>
  assumes "latest_id vm = Some wid" "dictionary vm wid = Some e"
  shows "vm_error (forth_immediate vm) = vm_error vm"
  using assms by (simp add: forth_immediate_def)

(* ── : ( "name" -- ) : nested-guard + mode/STATE half only ──────────────── *)
(* C (defining_word_colon + vm_enter_compile_mode): error if already in
   MODE_COMPILE (nested ':' is illegal per FORTH-79); else vm->mode =
   MODE_COMPILE, vm->state_var = -1, vm_store_cell(vm, vm->state_addr, -1),
   THEN vm_create_word(...) -- the entry-creation half, see file header
   finding (a), is NOT modelled. Modelled here: guard + the mode/state_var/
   state_addr-cell effect, which is state-only and has the identical shape
   to `]` plus the extra `state_var` write `]` itself does not do. *)

definition forth_colon_guard :: "vm_state \<Rightarrow> vm_state" where
  "forth_colon_guard vm =
    (if vm_mode vm = ModeCompile
     then set_error vm
     else vm\<lparr>vm_mode := ModeCompile,
              state_var := -1,
              memory := mem_write (memory vm) (state_addr vm) (-1)\<rparr>)"

lemma colon_nested_errors:
  assumes "vm_mode vm = ModeCompile"
  shows "vm_error (forth_colon_guard vm)"
  by (simp add: forth_colon_guard_def set_error_def assms)

lemma colon_sets_compile_mode:
  assumes "vm_mode vm \<noteq> ModeCompile"
  shows "vm_mode (forth_colon_guard vm) = ModeCompile"
  by (simp add: forth_colon_guard_def assms)

lemma colon_sets_state_var:
  assumes "vm_mode vm \<noteq> ModeCompile"
  shows "state_var (forth_colon_guard vm) = -1"
  by (simp add: forth_colon_guard_def assms)

lemma colon_writes_state_cell:
  assumes "vm_mode vm \<noteq> ModeCompile"
  shows "mem_read (memory (forth_colon_guard vm)) (state_addr vm) = -1"
  by (simp add: forth_colon_guard_def mem_read_def mem_write_def assms)

lemma colon_guard_not_full_colon: True
  \<comment> \<open>forth_colon_guard is NOT a full model of `:` -- it omits the
     dictionary-entry-creation half (`vm_create_word`, `vm->compiling_word`,
     WORD_SMUDGED, the DF write of the threaded-body start address). See
     file header finding (a)/(b). Named so the omission is greppable.\<close>
  by simp

(* ── : entry-creation half, gap (a) PARTIALLY CLOSED 2026-08-14 ──────────
   `vm_enter_compile_mode` (src/vm.c:232-264) does forth_colon_guard's
   mode/state effect FIRST, then `vm_create_word(...)`, then
   `de->flags |= WORD_SMUDGED` on the fresh entry (vm.c:251) -- unlike
   CREATE/VARIABLE/CONSTANT, `:` sets a real flag at creation time, so
   this reuses `dict_insert_entry WORD_SMUDGED` rather than
   `dict_insert_entry 0`. Composed after forth_colon_guard: only valid
   when the nested-`:` guard did not already error (real C: vm_create_word
   is never reached if `defining_word_colon`'s own nested check fired,
   since that returns before calling vm_enter_compile_mode at all). Still
   NOT modelled beyond this: name parse, `vm->compiling_word` tracking
   (no vm_state counterpart -- would need a new field, not attempted
   here), vm_align+HERE capture, and the DF write of the threaded-body
   start address (gap b). *)

definition forth_colon_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_colon_entry_half pinned_conflict vm =
    dict_insert_entry WORD_SMUDGED pinned_conflict (forth_colon_guard vm)"

lemma colon_entry_half_requires_guard_to_pass:
  assumes "vm_mode vm \<noteq> ModeCompile" "\<not> pinned_conflict"
  shows "\<exists>e. dictionary (forth_colon_entry_half pinned_conflict vm) (word_id_next (forth_colon_guard vm)) = Some e
             \<and> de_flags e = WORD_SMUDGED"
  using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def
                            dict_insert_entry_def Let_def)

lemma colon_entry_half_still_compile_mode:
  assumes "vm_mode vm \<noteq> ModeCompile" "\<not> pinned_conflict"
  shows "vm_mode (forth_colon_entry_half pinned_conflict vm) = ModeCompile"
  using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def
                            dict_insert_entry_def Let_def)

lemma colon_entry_half_not_full_colon: True
  \<comment> \<open>Still NOT modelled: name parse, vm->compiling_word tracking (no
     vm_state field), vm_align+HERE capture, DF write of the threaded-body
     start address (gap b). See section header.\<close>
  by simp

(* ── ; ( -- ) : compile-mode guard only ──────────────────────────────────── *)
(* C: error unless vm->mode == MODE_COMPILE; else calls vm_exit_compile_mode,
   entirely unmodelled (finds/compiles EXIT, flips WORD_SMUDGED/WORD_COMPILED,
   evicts hot-words cache -- none modelled in this suite). *)

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

lemma semicolon_requires_compile_mode:
  assumes "vm_mode vm \<noteq> ModeCompile"
  shows "vm_error (forth_semicolon_guard vm)"
  by (simp add: forth_semicolon_guard_def set_error_def assms)

lemma semicolon_guard_not_full_semicolon: True
  \<comment> \<open>forth_semicolon_guard covers only the guard raised directly in
     defining_word_semicolon. vm_exit_compile_mode's own effects (EXIT
     lookup+compile, WORD_SMUDGED/WORD_COMPILED flag flip, hot-words cache
     eviction) are entirely unmodelled -- none of EXIT-lookup, per-entry
     mutable flags via a live pointer, or the hot-words cache have any
     counterpart in this suite's abstract model.\<close>
  by simp

(* ── CREATE / VARIABLE / CONSTANT: entry-creation half only, gap (a)
   PARTIALLY CLOSED 2026-08-14 ─────────────────────────────────────────────
   All three call `vm_create_word(vm, namebuf, nlen, <their own runtime>)`
   with no extra flags set afterward (`entry->flags = 0` inside
   vm_create_word is the final value) -- so their entry-creation half is
   exactly `dict_insert_entry 0`, reused verbatim from the definition
   above. NOT modelled, same as before: the name parse that produces
   `namebuf`/`nlen` (TIB/input-subsystem gap, present in every word in
   this suite that parses a name), CREATE's/VARIABLE's `vm_align`+HERE
   capture, VARIABLE's `vm_allot` of one cell, and all three words' DF
   write of their respective captured/popped value (gap (b), unchanged).
   These are named `forth_<word>_entry_half` deliberately, not
   `forth_<word>`, to keep the omission visible at the call site the way
   `forth_colon_guard` already does for `:`. *)

definition forth_create_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_create_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm"

definition forth_variable_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_variable_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm"

definition forth_constant_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
  "forth_constant_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm"

lemma create_entry_half_populates_dictionary:
  assumes "\<not> pinned_conflict"
  shows "\<exists>e. dictionary (forth_create_entry_half pinned_conflict vm) (word_id_next vm) = Some e
             \<and> de_flags e = 0"
  using assms by (simp add: forth_create_entry_half_def dict_insert_entry_def Let_def)

lemma variable_entry_half_populates_dictionary:
  assumes "\<not> pinned_conflict"
  shows "\<exists>e. dictionary (forth_variable_entry_half pinned_conflict vm) (word_id_next vm) = Some e
             \<and> de_flags e = 0"
  using assms by (simp add: forth_variable_entry_half_def dict_insert_entry_def Let_def)

lemma constant_entry_half_populates_dictionary:
  assumes "\<not> pinned_conflict"
  shows "\<exists>e. dictionary (forth_constant_entry_half pinned_conflict vm) (word_id_next vm) = Some e
             \<and> de_flags e = 0"
  using assms by (simp add: forth_constant_entry_half_def dict_insert_entry_def Let_def)

lemma create_entry_half_pinned_conflict_errors:
  assumes "pinned_conflict"
  shows "vm_error (forth_create_entry_half pinned_conflict vm)"
  using assms by (simp add: forth_create_entry_half_def dict_insert_entry_def set_error_def)

lemma create_entry_half_not_full_create: True
  \<comment> \<open>Still NOT modelled beyond entry creation: name parse, vm_align+HERE
     capture, and the DF write of the DFA (gap b). See section header.\<close>
  by simp
lemma variable_entry_half_not_full_variable: True
  \<comment> \<open>Still NOT modelled beyond entry creation: name parse, vm_align+HERE
     capture, vm_allot of one cell, and the DF write of that cell's
     address (gap b). See section header.\<close>
  by simp
lemma constant_entry_half_not_full_constant: True
  \<comment> \<open>Still NOT modelled beyond entry creation: name parse, the value pop
     (this word's one real vm_state-only guard, `vm->dsp < 0`, is itself
     also unmodelled here since it gates the parse that must happen
     before vm_create_word), and the DF write of the popped value
     (gap b). See section header.\<close>
  by simp

lemma create_runtime_not_modelled: True   \<comment> \<open>defining_runtime_create: reads current_executing_entry's DF cell (gap b).\<close>
  by simp
lemma variable_runtime_not_modelled: True \<comment> \<open>defining_runtime_variable: reads current_executing_entry's DF cell (gap b).\<close>
  by simp
lemma constant_runtime_not_modelled: True \<comment> \<open>defining_runtime_constant: reads current_executing_entry's DF cell (gap b).\<close>
  by simp
lemma lit_not_modelled: True           \<comment> \<open>LIT: reads/advances the return-stack top as a raw C cell_t* threaded-code IP -- see file header, distinct from control_words.c's already-resolved IP-as-vaddr usage.\<close>
  by simp
lemma literal_not_modelled: True       \<comment> \<open>LITERAL: compiles a literal into threaded code via vm_compile_literal -- depends on the same unmodelled compile-target machinery as `:`/COMPILE.\<close>
  by simp
lemma dodoes_not_modelled: True        \<comment> \<open>defining_runtime_dodoes: DF/PFA layout (gap b) + runs a raw threaded-code interpreter loop over cell_t* IPs (gap c-adjacent, distinct mechanism from vm_ip).\<close>
  by simp
lemma does_rt_not_modelled: True       \<comment> \<open>defining_runtime_does_rt: patches vm->latest's DF (gap b) and reassigns its func pointer to defining_runtime_dodoes (gap c).\<close>
  by simp
lemma does_greater_not_modelled: True  \<comment> \<open>DOES>: compiles does_rt + EXIT into the defining word's body -- same unmodelled compile-target machinery as `:`.\<close>
  by simp
lemma compile_not_modelled: True       \<comment> \<open>COMPILE: vm_find_word (parse+lookup, same class as FIND, already flagged not-modelled) + vm_compile_word.\<close>
  by simp
lemma bracket_compile_not_modelled: True \<comment> \<open>[COMPILE]: identical body to COMPILE (defining_word_bracket_compile IS defining_word_compile).\<close>
  by simp
lemma forget_not_modelled: True        \<comment> \<open>FORGET: walks vm->latest's raw linked chain by name, frees C structs, and rewinds `here` from a DF read (gap a/b combined) -- categorically the same class of gap as `block_words.c`'s cache-subsystem deferrals: a whole-subsystem project, not a one-word extension.\<close>
  by simp
lemma defer_not_modelled: True         \<comment> \<open>DEFER: vm_create_word (gap a) with a zeroed DF slot (gap b). CORRECTION (added when src/word_source/defer_words.c was later swept, see StarForth_Defer_Words.thy): word_registry.c registers defer_words.c's DEFER/IS/DEFER@ AFTER this file's (Module 27 vs 17), unconditionally in both builds -- this DEFER is dead, shadowed code, never reachable. The gap analysis below is still accurate as a description of what this dead code would hit, and the live version hits the same gaps anyway, so nothing here needed retracting.\<close>
  by simp
lemma defer_runtime_not_modelled: True \<comment> \<open>defining_runtime_defer: reads a DictEntry* out of the DF cell (gap b) and calls through it (gap c). Also shadowed/dead -- see defer_not_modelled correction above.\<close>
  by simp
lemma is_not_modelled: True            \<comment> \<open>IS: vm_find_word (parse+lookup) + writes an XT into the target's DF cell (gap b) -- the mutable-dispatch mechanism of gap (c). Also shadowed/dead -- see defer_not_modelled correction above.\<close>
  by simp
lemma defer_fetch_not_modelled: True   \<comment> \<open>DEFER@: vm_find_word + reads the DF cell (gap b). Also shadowed/dead -- see defer_not_modelled correction above.\<close>
  by simp

end
