theory StarForth_Physics_Pipelining_Diagnostic_Words
  imports StarForth_Base
begin

(* =========================================================================
   Mirrors: src/word_source/physics_pipelining_diagnostic_words.c
   Registers (via vm_create_word directly, NOT register_word -- a
   different registration style from every other file in this sweep, note
   in case it ever matters for ACL/hot-words-cache interaction):
   PIPELINING-SHOW-STATS PIPELINING-SHOW-TOP-TRANSITIONS
   PIPELINING-RESET-ALL PIPELINING-ENABLE PIPELINING-STATS
   PIPELINING-ANALYZE-WORD

   ── Root gap: `transition_metrics` was never wired into `dict_entry` ────
   Every word in this file reads or writes `entry->transition_metrics`, a
   `WordTransitionMetrics*` -- StarForth_Base.thy already declares a
   `word_transition_metrics` RECORD TYPE (Section 3, "Word transition
   metrics") matching the C struct field-for-field, but `dict_entry`
   (Section 3, "Dictionary entry") has no field of that type. This looks
   like an intentional scope decision when `dict_entry` was designed (the
   comment there only documents omitting a `func` pointer, not
   transition_metrics), not an oversight noticed until now -- this is the
   first file in the sweep that actually needs it. Consequence: NOTHING
   any of these six words reads or writes has a counterpart in the
   abstract model. This is a materially different situation from every
   other "not modelled" gap so far (raw pointers, parsing, name lookup) --
   the underlying DATA doesn't exist in dict_entry at all, only its type
   declaration does.

   ── Scope ─────────────────────────────────────────────────────────────
   PIPELINING-RESET-ALL / -ENABLE / -STATS take no stack arguments and
   touch nothing that exists in vm_state (dictionary traversal via ->link
   is read-only and only reaches the unmodelled transition_metrics field;
   -ENABLE reads only a compile-time #if). Modelled as identity
   transitions -- but see the caveat lemma below: this identity is a
   modelling artifact of the gap above, not a claim that the real C words
   are no-ops.

   PIPELINING-SHOW-STATS / -ANALYZE-WORD (pop addr, len) and
   PIPELINING-SHOW-TOP-TRANSITIONS (pop addr, len, top_count) resolve a
   word by (address, length) via `vm_ptr` + `vm_find_word` -- the same
   raw-pointer name-resolution gap as physics_freeze_words.c -- then read
   transition_metrics (root gap above). Only the simplest underflow case
   (stack already empty before any pop) is modelled; the C's actual
   guard shape does a real `vm_pop` per argument with an error check
   between each, 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 -- a genuine partial-pop-then-error path, noted but not
   mechanised per argument count here given how little of each word's
   downstream effect is modellable regardless.
   ======================================================================== *)

(* ── PIPELINING-RESET-ALL / -ENABLE / -STATS : identity (see caveat) ────── *)

definition forth_pipelining_reset_all :: "vm_state \<Rightarrow> vm_state" where
  "forth_pipelining_reset_all vm = vm"

definition forth_pipelining_enable :: "vm_state \<Rightarrow> vm_state" where
  "forth_pipelining_enable vm = vm"

definition forth_pipelining_stats :: "vm_state \<Rightarrow> vm_state" where
  "forth_pipelining_stats vm = vm"

lemma pipelining_reset_all_identity: "forth_pipelining_reset_all vm = vm"
  by (simp add: forth_pipelining_reset_all_def)

lemma pipelining_enable_identity: "forth_pipelining_enable vm = vm"
  by (simp add: forth_pipelining_enable_def)

lemma pipelining_stats_identity: "forth_pipelining_stats vm = vm"
  by (simp add: forth_pipelining_stats_def)

lemma pipelining_identity_is_a_modelling_artifact: True
  \<comment> \<open>The three identities above hold ONLY because transition_metrics has
     no vm_state representation (see file header) -- PIPELINING-RESET-ALL
     genuinely mutates real C heap state (transition_metrics_reset on
     every instrumented word); this proof suite simply cannot see it.
     Not evidence of a no-op C implementation.\<close>
  by simp

(* ── PIPELINING-SHOW-STATS / -ANALYZE-WORD ( addr len -- ) : empty-stack
   underflow only ─────────────────────────────────────────────────────── *)

definition forth_pipelining_show_stats_empty_guard :: "vm_state \<Rightarrow> vm_state" where
  "forth_pipelining_show_stats_empty_guard vm =
    (if data_stack vm = [] then set_error vm else vm)"

lemma pipelining_show_stats_empty_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_pipelining_show_stats_empty_guard vm)"
  by (simp add: forth_pipelining_show_stats_empty_guard_def set_error_def assms)

definition forth_pipelining_analyze_word_empty_guard :: "vm_state \<Rightarrow> vm_state" where
  "forth_pipelining_analyze_word_empty_guard vm =
    (if data_stack vm = [] then set_error vm else vm)"

lemma pipelining_analyze_word_empty_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_pipelining_analyze_word_empty_guard vm)"
  by (simp add: forth_pipelining_analyze_word_empty_guard_def set_error_def assms)

(* ── PIPELINING-SHOW-TOP-TRANSITIONS ( addr len top_count -- ) : empty-
   stack underflow only ───────────────────────────────────────────────── *)

definition forth_pipelining_show_top_transitions_empty_guard :: "vm_state \<Rightarrow> vm_state" where
  "forth_pipelining_show_top_transitions_empty_guard vm =
    (if data_stack vm = [] then set_error vm else vm)"

lemma pipelining_show_top_transitions_empty_underflow:
  assumes "data_stack vm = []"
  shows "vm_error (forth_pipelining_show_top_transitions_empty_guard vm)"
  by (simp add: forth_pipelining_show_top_transitions_empty_guard_def set_error_def assms)

lemma pipelining_lookup_words_rest_not_modelled: True
  \<comment> \<open>Beyond the empty-stack case: partial-pop-then-error on a too-short
     nonempty stack (see file header), vm_ptr/vm_find_word name resolution
     (physics_freeze_words.c-class gap), and all transition_metrics reads
     (root gap) -- none modelled.\<close>
  by simp

end
