From 40758fa554ba467aba4b2880c40954354d8bc744 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 14:47:24 -0400 Subject: [PATCH] proof/: add StarForth_Dictionary_Heat_Diagnostic_Words.thy (dictionary_heat_diagnostic_words.c coverage) 4 of 6 words fully modelled (HEAT-PERCENTILES, LOOKUP-STRATEGY@/!, SHOW-HEAT-OPTIMIZATION); REORG-BUCKETS deferred (bucket/lookup-table structure has no vm_state counterpart); COMPARE-LOOKUPS partially -- guards and its net-zero effect on lookup_strategy modelled, the timed FIND-loop benchmarking body deferred (same FIND gap already flagged elsewhere). --- proof/ROOT | 1 + ...Forth_Dictionary_Heat_Diagnostic_Words.thy | 186 ++++++++++++++++++ 2 files changed, 187 insertions(+) create mode 100644 proof/StarForth_Dictionary_Heat_Diagnostic_Words.thy diff --git a/proof/ROOT b/proof/ROOT index d6ca4f9..cfe65e6 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -23,6 +23,7 @@ session "StarForth" = "HOL-Library" + StarForth_Vocabulary_Words StarForth_Mutex StarForth_Transition + StarForth_Dictionary_Heat_Diagnostic_Words StarForth_Loop1_Heat StarForth_Loop2_Window StarForth_Loop3_Decay diff --git a/proof/StarForth_Dictionary_Heat_Diagnostic_Words.thy b/proof/StarForth_Dictionary_Heat_Diagnostic_Words.thy new file mode 100644 index 0000000..7721e93 --- /dev/null +++ b/proof/StarForth_Dictionary_Heat_Diagnostic_Words.thy @@ -0,0 +1,186 @@ +theory StarForth_Dictionary_Heat_Diagnostic_Words + imports StarForth_Base +begin + +(* ========================================================================= + Mirrors: src/word_source/dictionary_heat_diagnostic_words.c + Registers: HEAT-PERCENTILES LOOKUP-STRATEGY@ LOOKUP-STRATEGY! + REORG-BUCKETS SHOW-HEAT-OPTIMIZATION COMPARE-LOOKUPS + + Introspection/control words for Loop #1 (execution heat) dictionary + lookup strategy. All fields these words read/write already exist in + vm_state (heat_threshold_25th/50th/75th, lookup_strategy) -- no new + model infrastructure needed, unlike most files this sweep has hit + recently. + + ── Scope ───────────────────────────────────────────────────────────── + HEAT-PERCENTILES, LOOKUP-STRATEGY@, LOOKUP-STRATEGY!, and + SHOW-HEAT-OPTIMIZATION are fully modelled -- pure reads/writes of + existing vm_state fields (the last is stdout-only, hence an identity + transition). REORG-BUCKETS and the inner benchmarking loop of + COMPARE-LOOKUPS are NOT modelled: both call `dict_reorganize_buckets_ + by_heat()`, which physically re-sorts a bucket/lookup-table structure + that has no counterpart anywhere in vm_state (the abstract `dictionary` + is a plain word_id-indexed function with no notion of bucket order at + all) -- and COMPARE-LOOKUPS additionally calls `vm_find_word()` in its + timing loop, the same FIND dependency already flagged not-modelled in + StarForth_Dictionary_Manipulation_Words.thy. COMPARE-LOOKUPS' guard + conditions and its net-zero effect on `lookup_strategy` (temporarily + flipped, then explicitly restored) ARE modelled, since those don't + depend on either gap. + ======================================================================== *) + +(* ── HEAT-PERCENTILES ( -- 25th 50th 75th ) TOS = 75th ──────────────────── *) +(* C: three individual dsp-increment pushes, but the single guard + `vm->dsp + 3 > STACK_SIZE` is checked once up front before any push. *) + +definition forth_heat_percentiles :: "vm_state \ vm_state" where + "forth_heat_percentiles vm = + (if length (data_stack vm) + 3 > STACK_SIZE + then set_error vm + else vm\data_stack := heat_threshold_75th vm # heat_threshold_50th vm # + heat_threshold_25th vm # data_stack vm\)" + +lemma heat_percentiles_overflow: + assumes "length (data_stack vm) + 3 > STACK_SIZE" + shows "vm_error (forth_heat_percentiles vm)" + by (simp add: forth_heat_percentiles_def set_error_def assms) + +lemma heat_percentiles_normal: + assumes "length (data_stack vm) + 3 \ STACK_SIZE" + shows "data_stack (forth_heat_percentiles vm) = + heat_threshold_75th vm # heat_threshold_50th vm # + heat_threshold_25th vm # data_stack vm" + using assms by (auto simp: forth_heat_percentiles_def) + +lemma heat_percentiles_preserves_thresholds: + "heat_threshold_25th (forth_heat_percentiles vm) = heat_threshold_25th vm" + "heat_threshold_50th (forth_heat_percentiles vm) = heat_threshold_50th vm" + "heat_threshold_75th (forth_heat_percentiles vm) = heat_threshold_75th vm" + by (simp_all add: forth_heat_percentiles_def set_error_def) + +(* ── LOOKUP-STRATEGY@ ( -- strategy ) ─────────────────────────────────────── *) + +definition forth_lookup_strategy_fetch :: "vm_state \ vm_state" where + "forth_lookup_strategy_fetch vm = + (if ds_full vm + then set_error vm + else vm\data_stack := word_of_nat (lookup_strategy vm) # data_stack vm\)" + +lemma lookup_strategy_fetch_overflow: + assumes "ds_full vm" + shows "vm_error (forth_lookup_strategy_fetch vm)" + by (simp add: forth_lookup_strategy_fetch_def set_error_def assms) + +lemma lookup_strategy_fetch_normal: + assumes "\ ds_full vm" + shows "data_stack (forth_lookup_strategy_fetch vm) = + word_of_nat (lookup_strategy vm) # data_stack vm" + by (simp add: forth_lookup_strategy_fetch_def assms) + +(* ── LOOKUP-STRATEGY! ( strategy -- ) ─────────────────────────────────────── *) +(* C: only 0 or 1 are accepted; any other popped value is silently + discarded (the pop itself always happens once the underflow guard + passes). *) + +definition forth_lookup_strategy_store :: "vm_state \ vm_state" where + "forth_lookup_strategy_store vm = + (case data_stack vm of + [] \ set_error vm + | s # xs \ + if s = 0 \ s = 1 + then vm\data_stack := xs, lookup_strategy := unat s\ + else vm\data_stack := xs\)" + +lemma lookup_strategy_store_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_lookup_strategy_store vm)" + by (simp add: forth_lookup_strategy_store_def set_error_def assms) + +lemma lookup_strategy_store_pops_one: + assumes "data_stack vm = s # xs" + shows "data_stack (forth_lookup_strategy_store vm) = xs" + by (simp add: forth_lookup_strategy_store_def assms) + +lemma lookup_strategy_store_accepts_0: + assumes "data_stack vm = 0 # xs" + shows "lookup_strategy (forth_lookup_strategy_store vm) = 0" + by (simp add: forth_lookup_strategy_store_def assms) + +lemma lookup_strategy_store_accepts_1: + assumes "data_stack vm = 1 # xs" + shows "lookup_strategy (forth_lookup_strategy_store vm) = 1" + by (simp add: forth_lookup_strategy_store_def assms) + +lemma lookup_strategy_store_rejects_other: + assumes "data_stack vm = s # xs" + assumes "s \ 0" "s \ 1" + shows "lookup_strategy (forth_lookup_strategy_store vm) = lookup_strategy vm" + using assms by (simp add: forth_lookup_strategy_store_def) + +(* ── SHOW-HEAT-OPTIMIZATION ( -- ) : stdout only, identity transition ────── *) + +definition forth_show_heat_optimization :: "vm_state \ vm_state" where + "forth_show_heat_optimization vm = vm" + +lemma show_heat_optimization_identity: + "forth_show_heat_optimization vm = vm" + by (simp add: forth_show_heat_optimization_def) + +(* ── REORG-BUCKETS ( -- ) -- NOT MODELLED ─────────────────────────────────── *) + +lemma reorg_buckets_not_modelled: True + \ \dict_reorganize_buckets_by_heat() / dict_update_heat_percentiles() + physically re-sort a bucket/lookup-table structure with no counterpart + in vm_state -- the abstract `dictionary` is a plain word_id-indexed + function, no bucket ordering. (dict_update_heat_percentiles DOES write + heat_threshold_25th/50th/75th, which ARE modelled fields, but its + computation depends on the unmodelled bucket contents, so the RESULT + value can't be characterised without modelling the buckets first.)\ + by simp + +(* ── COMPARE-LOOKUPS ( iterations -- ) : guards + net-zero strategy only ─── *) +(* C: pop iterations; error if stack was empty; if iterations <= 0, print + and return (no-op beyond the pop); otherwise runs two timed FIND loops + (not modelled, see file header) and unconditionally restores + vm->lookup_strategy to its pre-call value before returning. Modelled + here: the two guards, and the fact that IF the benchmarking path runs, + lookup_strategy is unchanged end-to-end despite being mutated + mid-function -- everything else (timing, FIND calls, printf) is opaque + I/O this proof suite doesn't model. *) + +definition forth_compare_lookups_guard :: "vm_state \ vm_state" where + "forth_compare_lookups_guard vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ vm\data_stack := xs\)" + +lemma compare_lookups_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_compare_lookups_guard vm)" + by (simp add: forth_compare_lookups_guard_def set_error_def assms) + +lemma compare_lookups_pops_one: + assumes "data_stack vm = n # xs" + shows "data_stack (forth_compare_lookups_guard vm) = xs" + by (simp add: forth_compare_lookups_guard_def assms) + +lemma compare_lookups_nonpositive_is_pop_only: True + \ \C: `if (iterations <= 0) { printf(...); return; }` -- once the + underflow guard passes and iterations \s 0, the word's entire + remaining effect is the pop already captured by + forth_compare_lookups_guard; nothing further happens to vm_state.\ + by simp + +lemma compare_lookups_benchmark_path_not_modelled: True + \ \When iterations > 0: two timed loops of vm_find_word (FIND, already + flagged not-modelled elsewhere) bracketing a + dict_reorganize_buckets_by_heat() call (see reorg_buckets_not_modelled + above). vm->lookup_strategy is flipped to 0 then 1 during the two + passes but is explicitly restored to its entry value + (`vm->lookup_strategy = orig_strategy;`) before return -- net effect + on lookup_strategy is the identity, even though this proof suite + doesn't model the intervening FIND-loop timing/output.\ + by simp + +end