proof/: add physics diagnostic/benchmark/pipelining coverage

StarForth_Physics_Diagnostic_Words.thy (physics_diagnostic_words.c):
3 of 4 words are pure-printf identity transitions; PHYSICS-BURN's guard
modelled, its arbitrary dynamically-selected func-pointer execution loop
is a new class of gap (not reducible to any prior one).

StarForth_Physics_Benchmark_Words.thy (physics_benchmark_words.c):
hot-words cache is a whole unmodelled subsystem. PHYSICS-RESET-STATS's
pipeline_metrics half (3 real vm_state fields) modelled; everything else
in the file deferred.

StarForth_Physics_Pipelining_Diagnostic_Words.thy
(physics_pipelining_diagnostic_words.c): root-cause finding --
`word_transition_metrics` has been a declared record type in
StarForth_Base.thy since early in the sweep but was never wired into
`dict_entry` as a field, so every word in this file touches state with
zero abstract representation. Three no-arg words modelled as identity
(with an explicit caveat that this reflects the model's blind spot, not
a no-op claim about the C); the three lookup words get only their
simplest empty-stack underflow case.

Suite now 43 theories, green.

proof/ROOT

@@ -25,6 +25,9 @@ session "StarForth" = "HOL-Library" +
     StarForth_Transition
     StarForth_Dictionary_Heat_Diagnostic_Words
     StarForth_Physics_Freeze_Words
+    StarForth_Physics_Diagnostic_Words
+    StarForth_Physics_Benchmark_Words
+    StarForth_Physics_Pipelining_Diagnostic_Words
     StarForth_Loop1_Heat
     StarForth_Loop2_Window
     StarForth_Loop3_Decay

proof/StarForth_Physics_Benchmark_Words.thy

@@ -0,0 +1,109 @@
+theory StarForth_Physics_Benchmark_Words
+  imports StarForth_Base
+begin
+
+(* =========================================================================
+   Mirrors: src/word_source/physics_benchmark_words.c
+   Registers: BENCH-DICT-LOOKUP PHYSICS-CACHE-STATS PHYSICS-TOGGLE-CACHE
+              PHYSICS-RESET-STATS PHYSICS-BUILD-INFO PHYSICS-BAYESIAN-REPORT
+
+   ── Hot-words cache -- a whole unmodelled subsystem ─────────────────────
+   Every word in this file reads or writes `vm->hotwords_cache` (a
+   `HotwordsCache*`) and/or its nested `HotwordsStats` -- neither has any
+   counterpart in vm_state. This is the same class of gap as the block-
+   window cache StarForth_Block_Words.thy/StarForth_Editor_Words.thy
+   already deferred (own subsystem-modelling project, not a one-word
+   extension), just for a different cache.
+
+   ── Scope ─────────────────────────────────────────────────────────────
+   PHYSICS-RESET-STATS is the one partial exception: alongside its
+   unmodelled `hotwords_stats_reset` call, it ALSO resets three
+   `pipeline_metrics` fields that ARE in vm_state
+   (`pm_prefetch_attempts`/`pm_prefetch_hits`/`pm_tuning_checks`). Modelled
+   assuming the (unmodelled) cache-initialized guard is reached -- i.e.
+   this states the word's effect on `pipeline_metrics` conditional on
+   control reaching that point, not the guard itself.
+
+   BENCH-DICT-LOOKUP's guard/pop shape is modelled (same pattern as
+   COMPARE-LOOKUPS/PHYSICS-BURN); its benchmark body is not (timed
+   `vm_find_word` loop, same FIND-family gap, PLUS the hot-words cache
+   gap above).
+
+   PHYSICS-CACHE-STATS, PHYSICS-TOGGLE-CACHE, PHYSICS-BUILD-INFO, and
+   PHYSICS-BAYESIAN-REPORT are entirely reads/writes of the unmodelled
+   cache subsystem (or pure stdout using only compile-time constants) --
+   not modelled at all.
+   ======================================================================== *)
+
+(* ── BENCH-DICT-LOOKUP ( iterations -- ) : guard/pop only ────────────────── *)
+
+definition forth_bench_dict_lookup_guard :: "vm_state \<Rightarrow> vm_state" where
+  "forth_bench_dict_lookup_guard vm =
+    (case data_stack vm of
+       []     \<Rightarrow> set_error vm
+     | n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
+
+lemma bench_dict_lookup_underflow:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_bench_dict_lookup_guard vm)"
+  by (simp add: forth_bench_dict_lookup_guard_def set_error_def assms)
+
+lemma bench_dict_lookup_pops_one:
+  assumes "data_stack vm = n # xs"
+  shows "data_stack (forth_bench_dict_lookup_guard vm) = xs"
+  by (simp add: forth_bench_dict_lookup_guard_def assms)
+
+lemma bench_dict_lookup_body_not_modelled: True
+  \<comment> \<open>iterations \<ge> 1: timed vm_find_word loop over the hot-words cache --
+     both the FIND-family gap and the cache-subsystem gap above.\<close>
+  by simp
+
+(* ── PHYSICS-RESET-STATS ( -- ) : pipeline_metrics half only ─────────────── *)
+(* C: guarded by `if (!vm->hotwords_cache) { ...; return; }` (unmodelled);
+   once past that guard: hotwords_stats_reset(...) (unmodelled, cache
+   subsystem) THEN three real vm_state field writes:
+     vm->pipeline_metrics.prefetch_hits = 0
+     vm->pipeline_metrics.prefetch_attempts = 0
+     vm->pipeline_metrics.window_tuning_checks = 0
+   Modelled as the pipeline_metrics update alone, conditional on the guard
+   having been reached (not itself expressed, since "cache initialized"
+   has no vm_state predicate). *)
+
+definition forth_physics_reset_stats_metrics :: "vm_state \<Rightarrow> vm_state" where
+  "forth_physics_reset_stats_metrics vm =
+     vm\<lparr>pipeline_metrics := (pipeline_metrics vm)
+          \<lparr>pm_prefetch_hits := 0, pm_prefetch_attempts := 0, pm_tuning_checks := 0\<rparr>\<rparr>"
+
+lemma physics_reset_stats_clears_pipeline_counters:
+  "pm_prefetch_hits     (pipeline_metrics (forth_physics_reset_stats_metrics vm)) = 0"
+  "pm_prefetch_attempts (pipeline_metrics (forth_physics_reset_stats_metrics vm)) = 0"
+  "pm_tuning_checks     (pipeline_metrics (forth_physics_reset_stats_metrics vm)) = 0"
+  by (simp_all add: forth_physics_reset_stats_metrics_def)
+
+lemma physics_reset_stats_preserves_other_pipeline_fields:
+  "pm_last_window_size    (pipeline_metrics (forth_physics_reset_stats_metrics vm))
+     = pm_last_window_size    (pipeline_metrics vm)"
+  "pm_last_accuracy_num   (pipeline_metrics (forth_physics_reset_stats_metrics vm))
+     = pm_last_accuracy_num   (pipeline_metrics vm)"
+  "pm_last_accuracy_den   (pipeline_metrics (forth_physics_reset_stats_metrics vm))
+     = pm_last_accuracy_den   (pipeline_metrics vm)"
+  "pm_suggested_next_size (pipeline_metrics (forth_physics_reset_stats_metrics vm))
+     = pm_suggested_next_size (pipeline_metrics vm)"
+  by (simp_all add: forth_physics_reset_stats_metrics_def)
+
+lemma physics_reset_stats_data_stack_unchanged:
+  "data_stack (forth_physics_reset_stats_metrics vm) = data_stack vm"
+  by (simp add: forth_physics_reset_stats_metrics_def)
+
+(* ── Everything else -- NOT MODELLED ──────────────────────────────────── *)
+
+lemma cache_stats_not_modelled: True       \<comment> \<open>PHYSICS-CACHE-STATS: reads hotwords_cache subsystem, stdout only.\<close>
+  by simp
+lemma toggle_cache_not_modelled: True      \<comment> \<open>PHYSICS-TOGGLE-CACHE: flips hotwords_cache->enabled -- outside vm_state.\<close>
+  by simp
+lemma build_info_not_modelled: True        \<comment> \<open>PHYSICS-BUILD-INFO: stdout of compile-time constants + hotwords_cache read.\<close>
+  by simp
+lemma bayesian_report_not_modelled: True   \<comment> \<open>PHYSICS-BAYESIAN-REPORT: reads/synthesizes HotwordsStats, stdout only.\<close>
+  by simp
+
+end

proof/StarForth_Physics_Diagnostic_Words.thy

@@ -0,0 +1,102 @@
+theory StarForth_Physics_Diagnostic_Words
+  imports StarForth_Base
+begin
+
+(* =========================================================================
+   Mirrors: src/word_source/physics_diagnostic_words.c
+   Registers: PHYSICS-WORD-METRICS PHYSICS-CALC-KNOBS PHYSICS-BURN
+              PHYSICS-SHOW-FEEDBACK
+
+   Interactive stdout demonstrations of the Loop #1 physics feedback loop,
+   built for REPL walkthroughs, not for programmatic use.
+
+   ── Scope ─────────────────────────────────────────────────────────────
+   PHYSICS-WORD-METRICS, PHYSICS-CALC-KNOBS, and PHYSICS-SHOW-FEEDBACK are
+   fully modelled: all three share the identical structure of "find the
+   dictionary entry with the largest `physics.last_active_ns` (a linked-
+   list scan via ->link, the same class of raw traversal already flagged
+   not-modelled for FORGET/ALL-HEATS -- but note this scan is READ-ONLY,
+   selecting which entry to print, with no consequence for what state
+   ends up being characterised), then printf a derived report from its
+   fields (`float` thermal-pressure math, purely for display -- not stored
+   anywhere)". None of the three writes to a SINGLE field of `vm_state` or
+   any `dict_entry` -- their entire observable contract, independent of
+   the (unmodelled) linked-list scan, is "no state change". Modelled as
+   identity transitions.
+
+   PHYSICS-BURN is different: its guard conditions are modelled, but its
+   core effect -- calling `target->func(vm)` in a loop, where `target` is
+   whichever word the same last-active-ns scan selects -- is NOT. This is
+   a genuinely new kind of gap for this sweep: every other file's
+   unmodelled dispatch has been either DEFER-style reassignment (function
+   pointer stored then later read) or a call embedded in a fixed
+   C-language control path (DODOES). PHYSICS-BURN calls an ARBITRARY,
+   data-dependent word's `func` directly from within a diagnostic
+   primitive -- there is no way to characterise its effect without first
+   knowing (a) which word gets selected (the unmodelled scan) and (b) what
+   that word's `func` does (the `word_table`/`word_physics_transparent`
+   abstraction StarForth_Transition.thy already provides IS the right tool
+   for word execution in general, but PHYSICS-BURN's selection is dynamic
+   and data-dependent in a way no other call site in this suite is).
+   ======================================================================== *)
+
+(* ── PHYSICS-WORD-METRICS / PHYSICS-CALC-KNOBS / PHYSICS-SHOW-FEEDBACK ────
+   All three: ( -- ), stdout-only, no vm_state field written. *)
+
+definition forth_physics_word_metrics :: "vm_state \<Rightarrow> vm_state" where
+  "forth_physics_word_metrics vm = vm"
+
+definition forth_physics_calc_knobs :: "vm_state \<Rightarrow> vm_state" where
+  "forth_physics_calc_knobs vm = vm"
+
+definition forth_physics_show_feedback :: "vm_state \<Rightarrow> vm_state" where
+  "forth_physics_show_feedback vm = vm"
+
+lemma physics_word_metrics_identity:
+  "forth_physics_word_metrics vm = vm"
+  by (simp add: forth_physics_word_metrics_def)
+
+lemma physics_calc_knobs_identity:
+  "forth_physics_calc_knobs vm = vm"
+  by (simp add: forth_physics_calc_knobs_def)
+
+lemma physics_show_feedback_identity:
+  "forth_physics_show_feedback vm = vm"
+  by (simp add: forth_physics_show_feedback_def)
+
+(* ── PHYSICS-BURN ( n -- ) : guards only ──────────────────────────────── *)
+(* C: error if stack empty; pop burn_count; if burn_count < 1, printf and
+   return (no-op beyond the pop); otherwise scans for a target word (same
+   unmodelled last-active-ns scan as the three words above) and calls its
+   func burn_count times -- NOT modelled, see file header. *)
+
+definition forth_physics_burn_guard :: "vm_state \<Rightarrow> vm_state" where
+  "forth_physics_burn_guard vm =
+    (case data_stack vm of
+       []     \<Rightarrow> set_error vm
+     | n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
+
+lemma physics_burn_underflow:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_physics_burn_guard vm)"
+  by (simp add: forth_physics_burn_guard_def set_error_def assms)
+
+lemma physics_burn_pops_one:
+  assumes "data_stack vm = n # xs"
+  shows "data_stack (forth_physics_burn_guard vm) = xs"
+  by (simp add: forth_physics_burn_guard_def assms)
+
+lemma physics_burn_nonpositive_count_is_pop_only: True
+  \<comment> \<open>C: `if (burn_count < 1) { printf(...); return; }` -- once the
+     underflow guard passes and burn_count < 1, the word's entire
+     remaining effect is the pop already captured by
+     forth_physics_burn_guard.\<close>
+  by simp
+
+lemma physics_burn_loop_not_modelled: True
+  \<comment> \<open>burn_count \<ge> 1: repeatedly calls an arbitrary, dynamically-selected
+     word's `func` pointer -- see file header for why this is a new class
+     of gap, not reducible to any single already-flagged one.\<close>
+  by simp
+
+end

proof/StarForth_Physics_Pipelining_Diagnostic_Words.thy

@@ -0,0 +1,121 @@
+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