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 \ vm_state" where "forth_pipelining_reset_all vm = vm" definition forth_pipelining_enable :: "vm_state \ vm_state" where "forth_pipelining_enable vm = vm" definition forth_pipelining_stats :: "vm_state \ 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 \ \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.\ by simp (* ── PIPELINING-SHOW-STATS / -ANALYZE-WORD ( addr len -- ) : empty-stack underflow only ─────────────────────────────────────────────────────── *) definition forth_pipelining_show_stats_empty_guard :: "vm_state \ 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 \ 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 \ 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 \ \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.\ by simp end