Robert Allan James
81b1083100
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.
103 lines
4.9 KiB
Plaintext
103 lines
4.9 KiB
Plaintext
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
|