Robert Allan James
40758fa554
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).
187 lines
9.0 KiB
Plaintext
187 lines
9.0 KiB
Plaintext
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 \<Rightarrow> vm_state" where
|
|
"forth_heat_percentiles vm =
|
|
(if length (data_stack vm) + 3 > STACK_SIZE
|
|
then set_error vm
|
|
else vm\<lparr>data_stack := heat_threshold_75th vm # heat_threshold_50th vm #
|
|
heat_threshold_25th vm # data_stack vm\<rparr>)"
|
|
|
|
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 \<le> 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 \<Rightarrow> vm_state" where
|
|
"forth_lookup_strategy_fetch vm =
|
|
(if ds_full vm
|
|
then set_error vm
|
|
else vm\<lparr>data_stack := word_of_nat (lookup_strategy vm) # data_stack vm\<rparr>)"
|
|
|
|
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 "\<not> 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 \<Rightarrow> vm_state" where
|
|
"forth_lookup_strategy_store vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| s # xs \<Rightarrow>
|
|
if s = 0 \<or> s = 1
|
|
then vm\<lparr>data_stack := xs, lookup_strategy := unat s\<rparr>
|
|
else vm\<lparr>data_stack := xs\<rparr>)"
|
|
|
|
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 \<noteq> 0" "s \<noteq> 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 \<Rightarrow> 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
|
|
\<comment> \<open>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.)\<close>
|
|
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 \<Rightarrow> vm_state" where
|
|
"forth_compare_lookups_guard vm =
|
|
(case data_stack vm of
|
|
[] \<Rightarrow> set_error vm
|
|
| n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
|
|
|
|
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
|
|
\<comment> \<open>C: `if (iterations <= 0) { printf(...); return; }` -- once the
|
|
underflow guard passes and iterations \<le>s 0, the word's entire
|
|
remaining effect is the pop already captured by
|
|
forth_compare_lookups_guard; nothing further happens to vm_state.\<close>
|
|
by simp
|
|
|
|
lemma compare_lookups_benchmark_path_not_modelled: True
|
|
\<comment> \<open>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.\<close>
|
|
by simp
|
|
|
|
end
|