theory StarForth_Lifecycle_Words_Hosted
  imports StarForth_Base
begin

(* =========================================================================
   Mirrors: src/word_source/lifecycle_words_hosted.c
   Registers (hosted build only -- see below): BIRTH KILL PAUSE RESUME USE

   ── Build-variant split, opposite of the console-fabric files ──────────
   The ENTIRE file is `#ifndef __STARKERNEL__` -- opposite of framebuffer_
   words.c/keyboard_words.c/scroll_words.c/ttf_words.c, which were kernel-
   only. Per the file's own header comment and CLAUDE.md's Hard Rules
   ("BIRTH, RUN, USE are primitives registered in C exactly like DUP...
   Never reach for FIND"), the KERNEL build's BIRTH/KILL/PAUSE/RESUME/USE
   live in `src/starkernel/capsule/lifecycle_words.c` -- a different file
   entirely, in `src/starkernel/` rather than `src/word_source/`, and per
   CLAUDE.md's scope note that tree is real/load-bearing kernel code, not
   this sweep's target (this sweep covers `src/word_source/*.c`, the
   vendored/shared word set). So this theory covers ONLY the hosted
   stand-ins; the real kernel capsule-birth-protocol words are out of
   scope for this file (and for this sweep generally).

   ── All five words are the SAME vm_state transition ─────────────────────
   Each body is: pop u, pop caddr (both via bare `vm_pop`, no upfront `dsp`
   guard -- deferring to `vm_pop`'s own internal underflow check, same
   convention scroll_words.c uses and explains), copy at most 63 bytes from
   `vm->memory[caddr..caddr+u)` into a local buffer (bounds-checked against
   `VM_MEMORY_SIZE`, silently truncated to empty if `caddr` is out of
   range), then `log_message` the extracted name. The five bodies differ
   ONLY in the literal string passed to `log_message` ("BIRTH %s (hosted)"
   vs "KILL %s (hosted)" etc.) -- everything with a vm_state footprint is
   byte-for-byte identical across all five. Modelled ONCE as
   `forth_lifecycle_pop2`, with each word's definition stated as literally
   equal to it.

   The C does NOT check `vm->error` between the two pops, so on a
   single-element stack the first pop succeeds (consuming it) before the
   second pop discovers the now-empty stack and sets the error -- the same
   partial-pop-then-error shape already seen in physics_pipelining_
   diagnostic_words.c, but here fully mechanised since (unlike that file)
   nothing downstream of the pops needs an unmodelled subsystem: the name
   extraction is a pure, bounds-checked memory READ with no vm_state
   write, and log_message is pure I/O. So this file's entire vm_state
   footprint is exactly captured by the two pops -- no deferred remainder
   at all, the only file in this sweep so far where that's true for every
   registered word. *)

definition forth_lifecycle_pop2 :: "vm_state \<Rightarrow> vm_state" where
  "forth_lifecycle_pop2 vm =
    (case data_stack vm of
       []            \<Rightarrow> set_error vm
     | [x]           \<Rightarrow> set_error (vm\<lparr>data_stack := []\<rparr>)
     | u # caddr # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"

lemma lifecycle_pop2_underflow_nil:
  assumes "data_stack vm = []"
  shows "vm_error (forth_lifecycle_pop2 vm)" and "data_stack (forth_lifecycle_pop2 vm) = []"
  by (simp_all add: forth_lifecycle_pop2_def set_error_def assms)

lemma lifecycle_pop2_underflow_one:
  \<comment> \<open>Partial pop: the single element IS consumed (it was popped
     successfully as `u`) before the second pop fails.\<close>
  assumes "data_stack vm = [x]"
  shows "vm_error (forth_lifecycle_pop2 vm)" and "data_stack (forth_lifecycle_pop2 vm) = []"
  by (simp_all add: forth_lifecycle_pop2_def set_error_def assms)

lemma lifecycle_pop2_normal:
  assumes "data_stack vm = u # caddr # xs"
  shows "data_stack (forth_lifecycle_pop2 vm) = xs"
    and "vm_error (forth_lifecycle_pop2 vm) = vm_error vm"
  by (simp_all add: forth_lifecycle_pop2_def assms)

(* ── The five registered words, each literally equal to forth_lifecycle_pop2 ── *)

definition forth_birth  :: "vm_state \<Rightarrow> vm_state" where "forth_birth  = forth_lifecycle_pop2"
definition forth_kill   :: "vm_state \<Rightarrow> vm_state" where "forth_kill   = forth_lifecycle_pop2"
definition forth_pause  :: "vm_state \<Rightarrow> vm_state" where "forth_pause  = forth_lifecycle_pop2"
definition forth_resume :: "vm_state \<Rightarrow> vm_state" where "forth_resume = forth_lifecycle_pop2"
definition forth_use    :: "vm_state \<Rightarrow> vm_state" where "forth_use    = forth_lifecycle_pop2"

lemma birth_is_pop2:  "forth_birth  vm = forth_lifecycle_pop2 vm" by (simp add: forth_birth_def)
lemma kill_is_pop2:   "forth_kill   vm = forth_lifecycle_pop2 vm" by (simp add: forth_kill_def)
lemma pause_is_pop2:  "forth_pause  vm = forth_lifecycle_pop2 vm" by (simp add: forth_pause_def)
lemma resume_is_pop2: "forth_resume vm = forth_lifecycle_pop2 vm" by (simp add: forth_resume_def)
lemma use_is_pop2:    "forth_use    vm = forth_lifecycle_pop2 vm" by (simp add: forth_use_def)

lemma lifecycle_words_preserve_dictionary:
  "dictionary (forth_lifecycle_pop2 vm) = dictionary vm"
  by (auto simp: forth_lifecycle_pop2_def set_error_def split: list.split)

lemma lifecycle_words_preserve_memory:
  "memory (forth_lifecycle_pop2 vm) = memory vm"
  by (auto simp: forth_lifecycle_pop2_def set_error_def split: list.split)

lemma lifecycle_name_extraction_and_log_not_modelled: True
  \<comment> \<open>extract_name's memcpy-from-vm-memory is a pure read (no vm_state
     write) and log_message is pure I/O -- neither has any vm_state effect
     to characterise beyond what forth_lifecycle_pop2 already captures.\<close>
  by simp

end