From 81b10831009ebb63e0ccc67e16fda5d1be8c0dc4 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 15:43:48 -0400 Subject: [PATCH] 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 | 3 + proof/StarForth_Physics_Benchmark_Words.thy | 109 ++++++++++++++++ proof/StarForth_Physics_Diagnostic_Words.thy | 102 +++++++++++++++ ...th_Physics_Pipelining_Diagnostic_Words.thy | 121 ++++++++++++++++++ 4 files changed, 335 insertions(+) create mode 100644 proof/StarForth_Physics_Benchmark_Words.thy create mode 100644 proof/StarForth_Physics_Diagnostic_Words.thy create mode 100644 proof/StarForth_Physics_Pipelining_Diagnostic_Words.thy diff --git a/proof/ROOT b/proof/ROOT index b6b7bf4..2e8ab8a 100644 --- a/proof/ROOT +++ b/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 diff --git a/proof/StarForth_Physics_Benchmark_Words.thy b/proof/StarForth_Physics_Benchmark_Words.thy new file mode 100644 index 0000000..ffaf33c --- /dev/null +++ b/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 \ vm_state" where + "forth_bench_dict_lookup_guard vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ vm\data_stack := xs\)" + +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 + \ \iterations \ 1: timed vm_find_word loop over the hot-words cache -- + both the FIND-family gap and the cache-subsystem gap above.\ + 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 \ vm_state" where + "forth_physics_reset_stats_metrics vm = + vm\pipeline_metrics := (pipeline_metrics vm) + \pm_prefetch_hits := 0, pm_prefetch_attempts := 0, pm_tuning_checks := 0\\" + +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 \ \PHYSICS-CACHE-STATS: reads hotwords_cache subsystem, stdout only.\ + by simp +lemma toggle_cache_not_modelled: True \ \PHYSICS-TOGGLE-CACHE: flips hotwords_cache->enabled -- outside vm_state.\ + by simp +lemma build_info_not_modelled: True \ \PHYSICS-BUILD-INFO: stdout of compile-time constants + hotwords_cache read.\ + by simp +lemma bayesian_report_not_modelled: True \ \PHYSICS-BAYESIAN-REPORT: reads/synthesizes HotwordsStats, stdout only.\ + by simp + +end diff --git a/proof/StarForth_Physics_Diagnostic_Words.thy b/proof/StarForth_Physics_Diagnostic_Words.thy new file mode 100644 index 0000000..b6efc6b --- /dev/null +++ b/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 \ vm_state" where + "forth_physics_word_metrics vm = vm" + +definition forth_physics_calc_knobs :: "vm_state \ vm_state" where + "forth_physics_calc_knobs vm = vm" + +definition forth_physics_show_feedback :: "vm_state \ 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 \ vm_state" where + "forth_physics_burn_guard vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ vm\data_stack := xs\)" + +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 + \ \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.\ + by simp + +lemma physics_burn_loop_not_modelled: True + \ \burn_count \ 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.\ + by simp + +end diff --git a/proof/StarForth_Physics_Pipelining_Diagnostic_Words.thy b/proof/StarForth_Physics_Pipelining_Diagnostic_Words.thy new file mode 100644 index 0000000..ec4b6eb --- /dev/null +++ b/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 \ 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