From 873c537e203fe7c596b3ec20b205b394d59e953e Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 14:54:00 -0400 Subject: [PATCH] proof/: add StarForth_Physics_Freeze_Words.thy (physics_freeze_words.c coverage) 6 of 9 words fully modelled (FREEZE-WORD, UNFREEZE-WORD, FROZEN?, HEAT!, HEAT@, DECAY-RATE@), parameterised over an explicit word_id-resolution input to sidestep the same raw-pointer name-lookup gap already flagged for FIND -- these words are an even rawer variant (caddr is an already-computed VM address cast straight to a host pointer, not a parsed input-stream token). SHOW-HEAT/ALL-HEATS (stdout diagnostics) and FREEZE-CRITICAL (21-name batch of the same FREEZE-WORD op) deferred. Finding: DECAY-RATE@ is the only push-only word in this file (and one of few in the whole sweep) with no data-stack-full guard before the raw push -- a genuine overflow hazard, modelled faithfully. --- proof/ROOT | 1 + proof/StarForth_Physics_Freeze_Words.thy | 325 +++++++++++++++++++++++ 2 files changed, 326 insertions(+) create mode 100644 proof/StarForth_Physics_Freeze_Words.thy diff --git a/proof/ROOT b/proof/ROOT index cfe65e6..b6b7bf4 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -24,6 +24,7 @@ session "StarForth" = "HOL-Library" + StarForth_Mutex StarForth_Transition StarForth_Dictionary_Heat_Diagnostic_Words + StarForth_Physics_Freeze_Words StarForth_Loop1_Heat StarForth_Loop2_Window StarForth_Loop3_Decay diff --git a/proof/StarForth_Physics_Freeze_Words.thy b/proof/StarForth_Physics_Freeze_Words.thy new file mode 100644 index 0000000..b07fbd1 --- /dev/null +++ b/proof/StarForth_Physics_Freeze_Words.thy @@ -0,0 +1,325 @@ +theory StarForth_Physics_Freeze_Words + imports StarForth_Base +begin + +(* ========================================================================= + Mirrors: src/word_source/physics_freeze_words.c + Registers: FREEZE-WORD UNFREEZE-WORD FROZEN? HEAT! HEAT@ SHOW-HEAT + ALL-HEATS DECAY-RATE@ FREEZE-CRITICAL + + ── Name-resolution gap, same class as FIND ───────────────────────────── + Every lookup word here (FREEZE-WORD, UNFREEZE-WORD, FROZEN?, HEAT!, + HEAT@) pops a (caddr, len) pair straight off the data stack and calls + vm_find_word with caddr reinterpreted as a raw C string pointer -- an + even more raw variant of the `find_not_modelled` gap already flagged in + StarForth_Dictionary_Manipulation_Words.thy (FIND there at least parses + from the input stream; here caddr is an arbitrary already-computed VM + address cast straight to a host pointer). Following the same convention + ACL_Pin_Monotone/StarForth_ACL_Words.thy use for the XT-pop gap, each + word below is parameterised over an explicit `wid_opt :: nat option` + argument standing in for "whatever `vm_find_word` would have resolved + this call's (caddr, len) to" -- modelling the word's contract given a + resolution result, not the resolution mechanism itself (which stays + unmodelled, same as FIND). + + All five lookup words share the same lenient contract: invalid length, + unresolved name (`wid_opt = None`), or a `wid_opt` that doesn't resolve + in `dictionary` all fall through to "no-op beyond the stack pop(s)" -- + never an error. Only stack underflow before the pop raises `vm_error`. + + ── Scope ───────────────────────────────────────────────────────────── + FREEZE-WORD, UNFREEZE-WORD, FROZEN?, HEAT!, HEAT@, and DECAY-RATE@ are + fully modelled (the first five up to the name-resolution parameter + above; DECAY-RATE@ needs no such parameter, it is a bare constant push). + SHOW-HEAT and ALL-HEATS are stdout-only diagnostics (SHOW-HEAT also + depends on the same name-resolution gap) -- not modelled, following the + `forth_show_heat_optimization`-style precedent of treating pure-I/O + words as out of scope rather than trivial identities cluttering the + file with restated boilerplate. FREEZE-CRITICAL resolves 21 hard-coded + names via the same gap and is a batch application of the FREEZE-WORD + flag-set operation -- not modelled as a whole (would need a length-21 + list of `nat option` resolutions as a parameter, disproportionate to + the word's diagnostic-only purpose), but its per-word effect is exactly + `freeze_flag_set`, already proved by `freeze_word_found`. + ======================================================================== *) + +definition WORD_NAME_MAX :: nat where "WORD_NAME_MAX = 31" +definition WORD_FROZEN :: nat where "WORD_FROZEN = 0x04" +definition WORD_PINNED :: nat where "WORD_PINNED = 0x08" +(* Clears bit 2 (WORD_FROZEN) only. Safe as a fixed AND-mask because every + flag bit this suite's model ever sets (WORD_FROZEN/WORD_PINNED/ + WORD_COMPILED/WORD_SMUDGED/WORD_HIDDEN/WORD_IMMEDIATE = 0x04..0x80) fits + inside one byte -- see StarForth_Defining_Words.thy / StarForth_ + Dictionary_Manipulation_Words.thy for the others. *) +definition WORD_FROZEN_CLEAR_MASK :: nat where "WORD_FROZEN_CLEAR_MASK = 0xFB" + +definition resolve_len_ok :: "cell \ bool" where + "resolve_len_ok len \ 0 unat len \ WORD_NAME_MAX" + +(* Shared "apply this transform to the resolved entry, or no-op" pattern. *) +definition apply_at_resolved :: "nat option \ (dict_entry \ dict_entry) \ + (nat \ dict_entry option) \ (nat \ dict_entry option)" where + "apply_at_resolved wid_opt f dict = + (case wid_opt of + None \ dict + | Some wid \ (case dict wid of + None \ dict + | Some e \ dict (wid := Some (f e))))" + +(* ── FREEZE-WORD ( caddr u -- ) ───────────────────────────────────────── *) + +definition forth_freeze_word :: "nat option \ vm_state \ vm_state" where + "forth_freeze_word wid_opt vm = + (case data_stack vm of + len # caddr # xs \ + (if \ resolve_len_ok len then vm\data_stack := xs\ + else vm\data_stack := xs, + dictionary := apply_at_resolved wid_opt + (\e. e\de_flags := de_flags e OR WORD_FROZEN\) (dictionary vm)\) + | _ \ set_error vm)" + +lemma freeze_word_underflow_nil: + assumes "data_stack vm = []" + shows "vm_error (forth_freeze_word wid_opt vm)" + by (simp add: forth_freeze_word_def set_error_def assms) + +lemma freeze_word_underflow_one: + assumes "data_stack vm = [x]" + shows "vm_error (forth_freeze_word wid_opt vm)" + by (simp add: forth_freeze_word_def set_error_def assms) + +lemma freeze_word_bad_length_noop: + assumes "data_stack vm = len # caddr # xs" + assumes "\ resolve_len_ok len" + shows "forth_freeze_word wid_opt vm = vm\data_stack := xs\" + using assms by (simp add: forth_freeze_word_def) + +lemma freeze_word_not_found_noop: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = None" + shows "dictionary (forth_freeze_word wid_opt vm) = dictionary vm" + using assms by (simp add: forth_freeze_word_def apply_at_resolved_def) + +lemma freeze_word_found: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = Some wid" + assumes "dictionary vm wid = Some e" + shows "data_stack (forth_freeze_word wid_opt vm) = xs" + and "dictionary (forth_freeze_word wid_opt vm) wid = + Some (e\de_flags := de_flags e OR WORD_FROZEN\)" + using assms by (simp_all add: forth_freeze_word_def apply_at_resolved_def) + +(* ── UNFREEZE-WORD ( caddr u -- ) ─────────────────────────────────────── *) + +definition forth_unfreeze_word :: "nat option \ vm_state \ vm_state" where + "forth_unfreeze_word wid_opt vm = + (case data_stack vm of + len # caddr # xs \ + (if \ resolve_len_ok len then vm\data_stack := xs\ + else vm\data_stack := xs, + dictionary := apply_at_resolved wid_opt + (\e. e\de_flags := de_flags e AND WORD_FROZEN_CLEAR_MASK\) (dictionary vm)\) + | _ \ set_error vm)" + +lemma unfreeze_word_underflow_nil: + assumes "data_stack vm = []" + shows "vm_error (forth_unfreeze_word wid_opt vm)" + by (simp add: forth_unfreeze_word_def set_error_def assms) + +lemma unfreeze_word_found: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = Some wid" + assumes "dictionary vm wid = Some e" + shows "dictionary (forth_unfreeze_word wid_opt vm) wid = + Some (e\de_flags := de_flags e AND WORD_FROZEN_CLEAR_MASK\)" + using assms by (simp add: forth_unfreeze_word_def apply_at_resolved_def) + +(* ── FROZEN? ( caddr u -- flag ) ───────────────────────────────────────── *) + +definition forth_frozen_query :: "nat option \ vm_state \ vm_state" where + "forth_frozen_query wid_opt vm = + (case data_stack vm of + len # caddr # xs \ + (if \ resolve_len_ok len then vm\data_stack := to_forth_bool False # xs\ + else case wid_opt of + None \ vm\data_stack := to_forth_bool False # xs\ + | Some wid \ + (case dictionary vm wid of + None \ vm\data_stack := to_forth_bool False # xs\ + | Some e \ vm\data_stack := + to_forth_bool (de_flags e AND WORD_FROZEN \ 0) # xs\)) + | _ \ set_error vm)" + +lemma frozen_query_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_frozen_query wid_opt vm)" + by (simp add: forth_frozen_query_def set_error_def assms) + +lemma frozen_query_bad_length: + assumes "data_stack vm = len # caddr # xs" + assumes "\ resolve_len_ok len" + shows "data_stack (forth_frozen_query wid_opt vm) = -1 # xs \ + data_stack (forth_frozen_query wid_opt vm) = 0 # xs" + using assms by (simp add: forth_frozen_query_def to_forth_bool_eq) + +lemma frozen_query_not_found: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = None" + shows "data_stack (forth_frozen_query wid_opt vm) = 0 # xs" + using assms by (simp add: forth_frozen_query_def) + +lemma frozen_query_found_true: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = Some wid" + assumes "dictionary vm wid = Some e" + assumes "de_flags e AND WORD_FROZEN \ 0" + shows "data_stack (forth_frozen_query wid_opt vm) = -1 # xs" + using assms by (simp add: forth_frozen_query_def) + +lemma frozen_query_found_false: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = Some wid" + assumes "dictionary vm wid = Some e" + assumes "de_flags e AND WORD_FROZEN = 0" + shows "data_stack (forth_frozen_query wid_opt vm) = 0 # xs" + using assms by (simp add: forth_frozen_query_def) + +(* ── HEAT! ( heat caddr u -- ) ─────────────────────────────────────────── *) + +definition forth_heat_store :: "nat option \ vm_state \ vm_state" where + "forth_heat_store wid_opt vm = + (case data_stack vm of + len # caddr # heat # xs \ + (if \ resolve_len_ok len then vm\data_stack := xs\ + else vm\data_stack := xs, + dictionary := apply_at_resolved wid_opt + (\e. e\de_heat := heat\) (dictionary vm)\) + | _ \ set_error vm)" + +lemma heat_store_underflow_nil: + assumes "data_stack vm = []" + shows "vm_error (forth_heat_store wid_opt vm)" + by (simp add: forth_heat_store_def set_error_def assms) + +lemma heat_store_underflow_one: + assumes "data_stack vm = [x]" + shows "vm_error (forth_heat_store wid_opt vm)" + by (simp add: forth_heat_store_def set_error_def assms) + +lemma heat_store_underflow_two: + assumes "data_stack vm = [x, y]" + shows "vm_error (forth_heat_store wid_opt vm)" + by (simp add: forth_heat_store_def set_error_def assms) + +lemma heat_store_found: + assumes "data_stack vm = len # caddr # heat # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = Some wid" + assumes "dictionary vm wid = Some e" + shows "data_stack (forth_heat_store wid_opt vm) = xs" + and "dictionary (forth_heat_store wid_opt vm) wid = Some (e\de_heat := heat\)" + using assms by (simp_all add: forth_heat_store_def apply_at_resolved_def) + +lemma heat_store_not_found_noop: + assumes "data_stack vm = len # caddr # heat # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = None" + shows "dictionary (forth_heat_store wid_opt vm) = dictionary vm" + using assms by (simp add: forth_heat_store_def apply_at_resolved_def) + +(* ── HEAT@ ( caddr u -- heat ) ─────────────────────────────────────────── *) + +definition forth_heat_fetch :: "nat option \ vm_state \ vm_state" where + "forth_heat_fetch wid_opt vm = + (case data_stack vm of + len # caddr # xs \ + (if \ resolve_len_ok len then vm\data_stack := 0 # xs\ + else case wid_opt of + None \ vm\data_stack := 0 # xs\ + | Some wid \ + (case dictionary vm wid of + None \ vm\data_stack := 0 # xs\ + | Some e \ vm\data_stack := de_heat e # xs\)) + | _ \ set_error vm)" + +lemma heat_fetch_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_heat_fetch wid_opt vm)" + by (simp add: forth_heat_fetch_def set_error_def assms) + +lemma heat_fetch_found: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = Some wid" + assumes "dictionary vm wid = Some e" + shows "data_stack (forth_heat_fetch wid_opt vm) = de_heat e # xs" + using assms by (simp add: forth_heat_fetch_def) + +lemma heat_fetch_not_found: + assumes "data_stack vm = len # caddr # xs" + assumes "resolve_len_ok len" + assumes "wid_opt = None" + shows "data_stack (forth_heat_fetch wid_opt vm) = 0 # xs" + using assms by (simp add: forth_heat_fetch_def) + +lemma heat_store_fetch_roundtrip: + assumes "dictionary vm wid = Some e" + shows "de_heat (the (apply_at_resolved (Some wid) (\e. e\de_heat := heat\) (dictionary vm) wid)) = heat" + using assms by (simp add: apply_at_resolved_def) + +(* ── DECAY-RATE@ ( -- rate ) ──────────────────────────────────────────── *) +(* C: pushes the compile-time (Kconfig-overridable) constant + DECAY_RATE_PER_US_Q16, default 1 (include/starforth_config.h). No + underflow/overflow guard in the C at all -- not even the usual ds_full + check other push-only words have. Modelled faithfully: unconditional. *) + +definition DECAY_RATE_PER_US_Q16_DEFAULT :: cell where "DECAY_RATE_PER_US_Q16_DEFAULT = 1" + +definition forth_decay_rate_fetch :: "vm_state \ vm_state" where + "forth_decay_rate_fetch vm = + vm\data_stack := DECAY_RATE_PER_US_Q16_DEFAULT # data_stack vm\" + +lemma decay_rate_fetch_pushes_constant: + "data_stack (forth_decay_rate_fetch vm) = DECAY_RATE_PER_US_Q16_DEFAULT # data_stack vm" + by (simp add: forth_decay_rate_fetch_def) + +lemma decay_rate_fetch_no_overflow_guard: True + \ \Genuine finding, not a bug per se: forth_DECAY_RATE_FETCH is the only + push-only word in this file (and one of very few in the whole sweep) + with NO `vm->dsp >= STACK_SIZE` guard before the raw + `vm->data_stack[vm->dsp++] = ...` write -- a full data stack makes + this a one-past-the-end write into `data_stack[STACK_SIZE]`, out of + bounds. Modelled faithfully (unconditional push, no error path) since + that IS the C behaviour; flagged here as a real overflow hazard.\ + by simp + +(* ── SHOW-HEAT, ALL-HEATS -- NOT MODELLED ─────────────────────────────── *) + +lemma show_heat_not_modelled: True + \ \SHOW-HEAT: name-resolution gap (see file header) plus stdout-only + output -- no vm_state effect to characterise beyond the same pop/guard + shape as FROZEN?/HEAT@, not worth restating as a separate word.\ + by simp + +lemma all_heats_not_modelled: True + \ \ALL-HEATS: walks vm->latest's raw ->link chain (same class of gap as + FORGET/TRAVERSE), collects into a fixed 1024-entry C array, bubble-sorts + by heat, prints -- entirely I/O + raw-pointer traversal, no stack or + dictionary-content effect to model.\ + by simp + +(* ── FREEZE-CRITICAL ( -- ) -- NOT MODELLED AS A WHOLE ─────────────────── + Per-word effect is exactly `freeze_word_found`'s dictionary update + (silently skipping any of the 21 hard-coded names that don't resolve); + see file header for why the full 21-name batch isn't modelled here. *) + +lemma freeze_critical_per_word_effect_is_freeze_word: True + by simp + +end