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.
This commit is contained in:
Robert Allan James
@@ -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
|
||||
|
||||
@@ -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 \<Rightarrow> bool" where
|
||||
"resolve_len_ok len \<longleftrightarrow> 0 <s len \<and> unat len \<le> WORD_NAME_MAX"
|
||||
|
||||
(* Shared "apply this transform to the resolved entry, or no-op" pattern. *)
|
||||
definition apply_at_resolved :: "nat option \<Rightarrow> (dict_entry \<Rightarrow> dict_entry) \<Rightarrow>
|
||||
(nat \<Rightarrow> dict_entry option) \<Rightarrow> (nat \<Rightarrow> dict_entry option)" where
|
||||
"apply_at_resolved wid_opt f dict =
|
||||
(case wid_opt of
|
||||
None \<Rightarrow> dict
|
||||
| Some wid \<Rightarrow> (case dict wid of
|
||||
None \<Rightarrow> dict
|
||||
| Some e \<Rightarrow> dict (wid := Some (f e))))"
|
||||
|
||||
(* ── FREEZE-WORD ( caddr u -- ) ───────────────────────────────────────── *)
|
||||
|
||||
definition forth_freeze_word :: "nat option \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_freeze_word wid_opt vm =
|
||||
(case data_stack vm of
|
||||
len # caddr # xs \<Rightarrow>
|
||||
(if \<not> resolve_len_ok len then vm\<lparr>data_stack := xs\<rparr>
|
||||
else vm\<lparr>data_stack := xs,
|
||||
dictionary := apply_at_resolved wid_opt
|
||||
(\<lambda>e. e\<lparr>de_flags := de_flags e OR WORD_FROZEN\<rparr>) (dictionary vm)\<rparr>)
|
||||
| _ \<Rightarrow> 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 "\<not> resolve_len_ok len"
|
||||
shows "forth_freeze_word wid_opt vm = vm\<lparr>data_stack := xs\<rparr>"
|
||||
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\<lparr>de_flags := de_flags e OR WORD_FROZEN\<rparr>)"
|
||||
using assms by (simp_all add: forth_freeze_word_def apply_at_resolved_def)
|
||||
|
||||
(* ── UNFREEZE-WORD ( caddr u -- ) ─────────────────────────────────────── *)
|
||||
|
||||
definition forth_unfreeze_word :: "nat option \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_unfreeze_word wid_opt vm =
|
||||
(case data_stack vm of
|
||||
len # caddr # xs \<Rightarrow>
|
||||
(if \<not> resolve_len_ok len then vm\<lparr>data_stack := xs\<rparr>
|
||||
else vm\<lparr>data_stack := xs,
|
||||
dictionary := apply_at_resolved wid_opt
|
||||
(\<lambda>e. e\<lparr>de_flags := de_flags e AND WORD_FROZEN_CLEAR_MASK\<rparr>) (dictionary vm)\<rparr>)
|
||||
| _ \<Rightarrow> 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\<lparr>de_flags := de_flags e AND WORD_FROZEN_CLEAR_MASK\<rparr>)"
|
||||
using assms by (simp add: forth_unfreeze_word_def apply_at_resolved_def)
|
||||
|
||||
(* ── FROZEN? ( caddr u -- flag ) ───────────────────────────────────────── *)
|
||||
|
||||
definition forth_frozen_query :: "nat option \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_frozen_query wid_opt vm =
|
||||
(case data_stack vm of
|
||||
len # caddr # xs \<Rightarrow>
|
||||
(if \<not> resolve_len_ok len then vm\<lparr>data_stack := to_forth_bool False # xs\<rparr>
|
||||
else case wid_opt of
|
||||
None \<Rightarrow> vm\<lparr>data_stack := to_forth_bool False # xs\<rparr>
|
||||
| Some wid \<Rightarrow>
|
||||
(case dictionary vm wid of
|
||||
None \<Rightarrow> vm\<lparr>data_stack := to_forth_bool False # xs\<rparr>
|
||||
| Some e \<Rightarrow> vm\<lparr>data_stack :=
|
||||
to_forth_bool (de_flags e AND WORD_FROZEN \<noteq> 0) # xs\<rparr>))
|
||||
| _ \<Rightarrow> 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 "\<not> resolve_len_ok len"
|
||||
shows "data_stack (forth_frozen_query wid_opt vm) = -1 # xs \<or>
|
||||
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 \<noteq> 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 \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_heat_store wid_opt vm =
|
||||
(case data_stack vm of
|
||||
len # caddr # heat # xs \<Rightarrow>
|
||||
(if \<not> resolve_len_ok len then vm\<lparr>data_stack := xs\<rparr>
|
||||
else vm\<lparr>data_stack := xs,
|
||||
dictionary := apply_at_resolved wid_opt
|
||||
(\<lambda>e. e\<lparr>de_heat := heat\<rparr>) (dictionary vm)\<rparr>)
|
||||
| _ \<Rightarrow> 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\<lparr>de_heat := heat\<rparr>)"
|
||||
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 \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_heat_fetch wid_opt vm =
|
||||
(case data_stack vm of
|
||||
len # caddr # xs \<Rightarrow>
|
||||
(if \<not> resolve_len_ok len then vm\<lparr>data_stack := 0 # xs\<rparr>
|
||||
else case wid_opt of
|
||||
None \<Rightarrow> vm\<lparr>data_stack := 0 # xs\<rparr>
|
||||
| Some wid \<Rightarrow>
|
||||
(case dictionary vm wid of
|
||||
None \<Rightarrow> vm\<lparr>data_stack := 0 # xs\<rparr>
|
||||
| Some e \<Rightarrow> vm\<lparr>data_stack := de_heat e # xs\<rparr>))
|
||||
| _ \<Rightarrow> 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) (\<lambda>e. e\<lparr>de_heat := heat\<rparr>) (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 \<Rightarrow> vm_state" where
|
||||
"forth_decay_rate_fetch vm =
|
||||
vm\<lparr>data_stack := DECAY_RATE_PER_US_Q16_DEFAULT # data_stack vm\<rparr>"
|
||||
|
||||
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
|
||||
\<comment> \<open>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.\<close>
|
||||
by simp
|
||||
|
||||
(* ── SHOW-HEAT, ALL-HEATS -- NOT MODELLED ─────────────────────────────── *)
|
||||
|
||||
lemma show_heat_not_modelled: True
|
||||
\<comment> \<open>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.\<close>
|
||||
by simp
|
||||
|
||||
lemma all_heats_not_modelled: True
|
||||
\<comment> \<open>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.\<close>
|
||||
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
|
||||
Reference in New Issue
Block a user