proof/: add StarForth_StarForth_Words.thy (starforth_words.c coverage)
5 of 12 words fully modelled: ENTROPY@/ENTROPY! (XT-pop gap sidestepped same as ACL words, but note this file's is_valid_dict_entry is a real membership-check safety improvement over acl_words.c's null-only check), RESET-ENTROPY (dictionary-wide bulk reset, same technique as ACL-INIT-PRIMITIVES), ZUSE-AUTHENTICATE (single-field set), VERSION (identity, no stack effect at all). TOP-WORDS/SEED/RANDOM/WAIT get guard/shape only -- SEED and RANDOM both depend on g_prng_state, a file-scope C static shared across the whole Tripod fleet (yet another instance of the recurring file-scope-static-instead-of-per-VM pattern, here meaning every VM draws from the same RNG stream). WORD-ENTROPY/(-/ INIT not modelled (pure printf / TIB dependency / real filesystem I/O plus a custom text parser). Finding: register_starforth_words registers its 10 words, bootstraps the STARFORTH vocabulary, then re-registers 12 words (same 10 plus ENTROPY@/ENTROPY!) into that vocabulary context -- noted as the second file where registration order matters for which body actually runs, judgment on intentionality deferred to the largely-unmodelled vocabulary chain mechanics. Suite now 44 theories, green.
This commit is contained in:
Robert Allan James
@@ -28,6 +28,7 @@ session "StarForth" = "HOL-Library" +
|
||||
StarForth_Physics_Diagnostic_Words
|
||||
StarForth_Physics_Benchmark_Words
|
||||
StarForth_Physics_Pipelining_Diagnostic_Words
|
||||
StarForth_StarForth_Words
|
||||
StarForth_Loop1_Heat
|
||||
StarForth_Loop2_Window
|
||||
StarForth_Loop3_Decay
|
||||
|
||||
@@ -0,0 +1,298 @@
|
||||
theory StarForth_StarForth_Words
|
||||
imports StarForth_Base
|
||||
begin
|
||||
|
||||
(* =========================================================================
|
||||
Mirrors: src/word_source/starforth_words.c
|
||||
Registers: ENTROPY@ ENTROPY! WORD-ENTROPY RESET-ENTROPY TOP-WORDS (-
|
||||
INIT VERSION SEED RANDOM WAIT ZUSE-AUTHENTICATE
|
||||
|
||||
── Registration finding: words are registered TWICE ─────────────────────
|
||||
`register_starforth_words` (line 802) registers 10 words, calls
|
||||
`vm_bootstrap_root_vocabulary(vm, "STARFORTH")`, then re-registers 12
|
||||
words (the same 10 plus ENTROPY@/ENTROPY!) "in the STARFORTH vocabulary
|
||||
context" per its own comment. Whether this is intentional vocabulary-
|
||||
system plumbing or a real double-registration bug is outside this
|
||||
theory's scope to judge (it would need the vocabulary-chain mechanics
|
||||
StarForth_Vocabulary_Words.thy already flagged as file-scope-static and
|
||||
largely unmodelled) -- noted here since it's the second file in the
|
||||
sweep (after defining_words.c/dictionary_manipulation_words.c) where
|
||||
registration ORDER matters for which word body actually runs.
|
||||
|
||||
── XT-pop gap, same convention as ACL words ─────────────────────────────
|
||||
ENTROPY@/ENTROPY! pop a raw address, cast it to `DictEntry*`, and
|
||||
ADDITIONALLY validate it via `is_valid_dict_entry` (a dictionary
|
||||
membership walk) before use -- a real safety improvement over
|
||||
acl_words.c's `pop_xt` (null check only). Modelled the same way
|
||||
ACL_Pin_Monotone/StarForth_ACL_Words.thy do: operating on an
|
||||
already-resolved `dict_entry`, not the pop/cast/validate mechanism
|
||||
(still the same underlying "cast cell_t <-> DictEntry*" gap).
|
||||
|
||||
── Scope ─────────────────────────────────────────────────────────────
|
||||
Fully modelled: ENTROPY@, ENTROPY!, RESET-ENTROPY (dictionary-wide bulk
|
||||
reset, same technique as ACL-INIT-PRIMITIVES), ZUSE-AUTHENTICATE
|
||||
(single-field set), VERSION (stdout-only identity, no stack effect at
|
||||
all -- doesn't even touch data_stack).
|
||||
Guard/shape only, body deferred: TOP-WORDS (printf display), SEED
|
||||
(mutates `g_prng_state`, a file-scope C static with no vm_state
|
||||
counterpart), RANDOM (result depends on the same unmodelled PRNG state
|
||||
via `prng_next()`), WAIT (loops calling `vm_tick(vm)`, which does far
|
||||
more than the heartbeat sub-transitions StarForth_Loop7_Heartrate.thy
|
||||
models -- composing it accurately is its own project).
|
||||
Not modelled at all: WORD-ENTROPY (pure printf, but included as an
|
||||
identity for completeness), `(-` (TIB/input-buffer dependency, the
|
||||
documented cluster from StarForth_String_Words.thy/StarForth_System_
|
||||
Words.thy), INIT (real filesystem I/O + a substantial custom text
|
||||
parser rewriting `NNNN LOAD` references -- a whole subsystem, not a
|
||||
word-level property).
|
||||
======================================================================== *)
|
||||
|
||||
(* ── ENTROPY@ ( addr -- n ) ────────────────────────────────────────────── *)
|
||||
|
||||
definition forth_entropy_fetch :: "vm_state \<Rightarrow> dict_entry \<Rightarrow> vm_state" where
|
||||
"forth_entropy_fetch vm e =
|
||||
(if ds_full vm then set_error vm
|
||||
else vm\<lparr>data_stack := de_heat e # data_stack vm\<rparr>)"
|
||||
|
||||
lemma entropy_fetch_underflow_note: True
|
||||
\<comment> \<open>The C underflow guard (`vm->dsp < 0` before the pop) and the
|
||||
null/validity checks on the popped address are all part of the
|
||||
unmodelled XT-pop/cast/validate mechanism (see file header) -- once
|
||||
an already-resolved `dict_entry` is in hand, as modelled here, only
|
||||
the destination stack-overflow guard remains a real vm_state
|
||||
condition.\<close>
|
||||
by simp
|
||||
|
||||
lemma entropy_fetch_normal:
|
||||
assumes "\<not> ds_full vm"
|
||||
shows "data_stack (forth_entropy_fetch vm e) = de_heat e # data_stack vm"
|
||||
by (simp add: forth_entropy_fetch_def assms)
|
||||
|
||||
(* ── ENTROPY! ( n addr -- ) ────────────────────────────────────────────── *)
|
||||
(* C pops addr first (TOS), then value -- matches the ( n addr -- ) stack
|
||||
comment: addr is on top, n below it. *)
|
||||
|
||||
definition forth_entropy_store :: "nat \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_entropy_store wid vm =
|
||||
(case data_stack vm of
|
||||
addr # value # xs \<Rightarrow>
|
||||
vm\<lparr>data_stack := xs,
|
||||
dictionary := (case dictionary vm wid of
|
||||
None \<Rightarrow> dictionary vm
|
||||
| Some e \<Rightarrow> (dictionary vm)(wid := Some (e\<lparr>de_heat := value\<rparr>)))\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma entropy_store_underflow_nil:
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_entropy_store wid vm)"
|
||||
by (simp add: forth_entropy_store_def set_error_def assms)
|
||||
|
||||
lemma entropy_store_underflow_one:
|
||||
assumes "data_stack vm = [x]"
|
||||
shows "vm_error (forth_entropy_store wid vm)"
|
||||
by (simp add: forth_entropy_store_def set_error_def assms)
|
||||
|
||||
lemma entropy_store_found:
|
||||
assumes "data_stack vm = addr # value # xs"
|
||||
assumes "dictionary vm wid = Some e"
|
||||
shows "data_stack (forth_entropy_store wid vm) = xs"
|
||||
and "dictionary (forth_entropy_store wid vm) wid = Some (e\<lparr>de_heat := value\<rparr>)"
|
||||
using assms by (simp_all add: forth_entropy_store_def)
|
||||
|
||||
(* ── RESET-ENTROPY ( -- ) : dictionary-wide bulk reset ───────────────────── *)
|
||||
(* C: for every entry with execution_heat > 0, zero de_heat AND the three
|
||||
physics fields temperature_q8/avg_latency_ns/last_active_ns. Entries
|
||||
with execution_heat = 0 already are left untouched (redundant given
|
||||
they're already all-zero in practice, but modelled faithfully -- the
|
||||
guard is on de_heat only, not on the physics fields independently). *)
|
||||
|
||||
definition reset_entropy_entry :: "dict_entry \<Rightarrow> dict_entry" where
|
||||
"reset_entropy_entry e =
|
||||
(if 0 <s de_heat e
|
||||
then e\<lparr>de_heat := 0,
|
||||
de_physics := (de_physics e)
|
||||
\<lparr>dp_temperature_q8 := 0, dp_avg_latency_ns := 0, dp_last_active_ns := 0\<rparr>\<rparr>
|
||||
else e)"
|
||||
|
||||
definition forth_reset_entropy :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_reset_entropy vm =
|
||||
vm\<lparr>dictionary := (\<lambda>wid. map_option reset_entropy_entry (dictionary vm wid))\<rparr>"
|
||||
|
||||
lemma reset_entropy_hot_entry_zeroed:
|
||||
assumes "dictionary vm wid = Some e"
|
||||
assumes "0 <s de_heat e"
|
||||
shows "dictionary (forth_reset_entropy vm) wid =
|
||||
Some (e\<lparr>de_heat := 0,
|
||||
de_physics := (de_physics e)
|
||||
\<lparr>dp_temperature_q8 := 0, dp_avg_latency_ns := 0, dp_last_active_ns := 0\<rparr>\<rparr>)"
|
||||
using assms by (simp add: forth_reset_entropy_def reset_entropy_entry_def)
|
||||
|
||||
lemma reset_entropy_cold_entry_untouched:
|
||||
assumes "dictionary vm wid = Some e"
|
||||
assumes "\<not> 0 <s de_heat e"
|
||||
shows "dictionary (forth_reset_entropy vm) wid = Some e"
|
||||
using assms by (simp add: forth_reset_entropy_def reset_entropy_entry_def)
|
||||
|
||||
lemma reset_entropy_preserves_absence:
|
||||
assumes "dictionary vm wid = None"
|
||||
shows "dictionary (forth_reset_entropy vm) wid = None"
|
||||
using assms by (simp add: forth_reset_entropy_def)
|
||||
|
||||
lemma reset_entropy_data_stack_unchanged:
|
||||
"data_stack (forth_reset_entropy vm) = data_stack vm"
|
||||
by (simp add: forth_reset_entropy_def)
|
||||
|
||||
lemma reset_entropy_never_errors:
|
||||
"vm_error (forth_reset_entropy vm) = vm_error vm"
|
||||
by (simp add: forth_reset_entropy_def)
|
||||
|
||||
(* ── ZUSE-AUTHENTICATE ( -- ) : single-field set ──────────────────────────── *)
|
||||
|
||||
definition forth_zuse_authenticate :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_zuse_authenticate vm = vm\<lparr>zuse_session := True\<rparr>"
|
||||
|
||||
lemma zuse_authenticate_sets_session:
|
||||
"zuse_session (forth_zuse_authenticate vm) = True"
|
||||
by (simp add: forth_zuse_authenticate_def)
|
||||
|
||||
lemma zuse_authenticate_data_stack_unchanged:
|
||||
"data_stack (forth_zuse_authenticate vm) = data_stack vm"
|
||||
by (simp add: forth_zuse_authenticate_def)
|
||||
|
||||
lemma zuse_authenticate_never_errors:
|
||||
"vm_error (forth_zuse_authenticate vm) = vm_error vm"
|
||||
by (simp add: forth_zuse_authenticate_def)
|
||||
|
||||
(* ── VERSION ( -- ) : stdout-only, no stack effect at all ────────────────── *)
|
||||
|
||||
definition forth_version :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_version vm = vm"
|
||||
|
||||
lemma version_identity: "forth_version vm = vm"
|
||||
by (simp add: forth_version_def)
|
||||
|
||||
(* ── WORD-ENTROPY ( -- ) : stdout-only display, identity ──────────────────── *)
|
||||
|
||||
definition forth_word_entropy :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_word_entropy vm = vm"
|
||||
|
||||
lemma word_entropy_identity: "forth_word_entropy vm = vm"
|
||||
by (simp add: forth_word_entropy_def)
|
||||
|
||||
(* ── TOP-WORDS ( n -- ) : guard/pop only, display body not modelled ──────── *)
|
||||
|
||||
definition forth_top_words_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_top_words_guard vm =
|
||||
(case data_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
|
||||
|
||||
lemma top_words_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_top_words_guard vm)"
|
||||
by (simp add: forth_top_words_guard_def set_error_def assms)
|
||||
|
||||
lemma top_words_pops_one:
|
||||
assumes "data_stack vm = n # xs"
|
||||
shows "data_stack (forth_top_words_guard vm) = xs"
|
||||
by (simp add: forth_top_words_guard_def assms)
|
||||
|
||||
(* ── SEED ( n -- ) : guard/pop only, PRNG state not modelled ─────────────── *)
|
||||
|
||||
definition forth_seed_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_seed_guard vm =
|
||||
(case data_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
|
||||
|
||||
lemma seed_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_seed_guard vm)"
|
||||
by (simp add: forth_seed_guard_def set_error_def assms)
|
||||
|
||||
lemma seed_pops_one:
|
||||
assumes "data_stack vm = n # xs"
|
||||
shows "data_stack (forth_seed_guard vm) = xs"
|
||||
by (simp add: forth_seed_guard_def assms)
|
||||
|
||||
lemma seed_global_not_modelled: True
|
||||
\<comment> \<open>g_prng_state is a file-scope C static (line 71), not a vm_state
|
||||
field -- ANOTHER instance of the file-scope-static-instead-of-per-VM
|
||||
pattern this sweep has now found many times (see StarForth_System_
|
||||
Words.thy/StarForth_Vocabulary_Words.thy for the aggregated write-up
|
||||
candidates), but here the effect is arguably WORSE: it means SEED
|
||||
re-seeds a single process-wide RNG shared by every VM in the Tripod
|
||||
fleet, and RANDOM below draws from that same shared stream.\<close>
|
||||
by simp
|
||||
|
||||
(* ── RANDOM ( lo hi -- n ) : guard/shape only, result not modelled ───────── *)
|
||||
|
||||
definition forth_random_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_random_guard vm =
|
||||
(case data_stack vm of
|
||||
hi # lo # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>
|
||||
| _ \<Rightarrow> set_error vm)"
|
||||
|
||||
lemma random_underflow_nil:
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_random_guard vm)"
|
||||
by (simp add: forth_random_guard_def set_error_def assms)
|
||||
|
||||
lemma random_underflow_one:
|
||||
assumes "data_stack vm = [x]"
|
||||
shows "vm_error (forth_random_guard vm)"
|
||||
by (simp add: forth_random_guard_def set_error_def assms)
|
||||
|
||||
lemma random_pops_two:
|
||||
assumes "data_stack vm = hi # lo # xs"
|
||||
shows "data_stack (forth_random_guard vm) = xs"
|
||||
by (simp add: forth_random_guard_def assms)
|
||||
|
||||
lemma random_result_not_modelled: True
|
||||
\<comment> \<open>Result depends on prng_next(), which draws from the same unmodelled
|
||||
g_prng_state global as SEED -- see seed_global_not_modelled.\<close>
|
||||
by simp
|
||||
|
||||
(* ── WAIT ( n -- ) : guard + non-positive-n no-op modelled, loop deferred ── *)
|
||||
|
||||
definition forth_wait_guard :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_wait_guard vm =
|
||||
(case data_stack vm of
|
||||
[] \<Rightarrow> set_error vm
|
||||
| n # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>)"
|
||||
|
||||
lemma wait_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_wait_guard vm)"
|
||||
by (simp add: forth_wait_guard_def set_error_def assms)
|
||||
|
||||
lemma wait_nonpositive_ticks_is_pop_only: True
|
||||
\<comment> \<open>C: `if (ticks <= 0) return;` -- once the underflow guard passes and
|
||||
ticks \<le>s 0, the word's entire remaining effect is the pop already
|
||||
captured by forth_wait_guard.\<close>
|
||||
by simp
|
||||
|
||||
lemma wait_loop_not_modelled: True
|
||||
\<comment> \<open>ticks > 0: calls vm_tick(vm) that many times. vm_tick does far more
|
||||
than the heartbeat_state sub-transitions StarForth_Loop7_Heartrate.thy
|
||||
models (hb_fire_tick etc. operate on heartbeat_state alone) --
|
||||
composing an accurate n-times vm_tick transition is its own project,
|
||||
not attempted here.\<close>
|
||||
by simp
|
||||
|
||||
(* ── (- , INIT -- NOT MODELLED ────────────────────────────────────────── *)
|
||||
|
||||
lemma paren_dash_not_modelled: True
|
||||
\<comment> \<open>(- : consumes vm->input_buffer/input_pos -- the TIB/input-subsystem
|
||||
dependency already documented as a deferred cluster in StarForth_
|
||||
String_Words.thy/StarForth_System_Words.thy.\<close>
|
||||
by simp
|
||||
|
||||
lemma init_not_modelled: True
|
||||
\<comment> \<open>INIT: real filesystem I/O (fopen/fread on ./capsules/core/init.4th)
|
||||
plus a substantial custom text parser that rewrites `NNNN LOAD`
|
||||
block references while copying into the block subsystem -- a whole
|
||||
subsystem-level operation, not a word-level property.\<close>
|
||||
by simp
|
||||
|
||||
end
|
||||
Reference in New Issue
Block a user