diff --git a/proof/ROOT b/proof/ROOT index 2e8ab8a..b3817ac 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -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 diff --git a/proof/StarForth_StarForth_Words.thy b/proof/StarForth_StarForth_Words.thy new file mode 100644 index 0000000..026c830 --- /dev/null +++ b/proof/StarForth_StarForth_Words.thy @@ -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 \ dict_entry \ vm_state" where + "forth_entropy_fetch vm e = + (if ds_full vm then set_error vm + else vm\data_stack := de_heat e # data_stack vm\)" + +lemma entropy_fetch_underflow_note: True + \ \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.\ + by simp + +lemma entropy_fetch_normal: + assumes "\ 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 \ vm_state \ vm_state" where + "forth_entropy_store wid vm = + (case data_stack vm of + addr # value # xs \ + vm\data_stack := xs, + dictionary := (case dictionary vm wid of + None \ dictionary vm + | Some e \ (dictionary vm)(wid := Some (e\de_heat := value\)))\ + | _ \ 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\de_heat := value\)" + 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 \ dict_entry" where + "reset_entropy_entry e = + (if 0 de_heat := 0, + de_physics := (de_physics e) + \dp_temperature_q8 := 0, dp_avg_latency_ns := 0, dp_last_active_ns := 0\\ + else e)" + +definition forth_reset_entropy :: "vm_state \ vm_state" where + "forth_reset_entropy vm = + vm\dictionary := (\wid. map_option reset_entropy_entry (dictionary vm wid))\" + +lemma reset_entropy_hot_entry_zeroed: + assumes "dictionary vm wid = Some e" + assumes "0 de_heat := 0, + de_physics := (de_physics e) + \dp_temperature_q8 := 0, dp_avg_latency_ns := 0, dp_last_active_ns := 0\\)" + 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 "\ 0 vm_state" where + "forth_zuse_authenticate vm = vm\zuse_session := True\" + +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 \ 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 \ 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 \ vm_state" where + "forth_top_words_guard vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ vm\data_stack := xs\)" + +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 \ vm_state" where + "forth_seed_guard vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ vm\data_stack := xs\)" + +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 + \ \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.\ + by simp + +(* ── RANDOM ( lo hi -- n ) : guard/shape only, result not modelled ───────── *) + +definition forth_random_guard :: "vm_state \ vm_state" where + "forth_random_guard vm = + (case data_stack vm of + hi # lo # xs \ vm\data_stack := xs\ + | _ \ 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 + \ \Result depends on prng_next(), which draws from the same unmodelled + g_prng_state global as SEED -- see seed_global_not_modelled.\ + by simp + +(* ── WAIT ( n -- ) : guard + non-positive-n no-op modelled, loop deferred ── *) + +definition forth_wait_guard :: "vm_state \ vm_state" where + "forth_wait_guard vm = + (case data_stack vm of + [] \ set_error vm + | n # xs \ vm\data_stack := xs\)" + +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 + \ \C: `if (ticks <= 0) return;` -- once the underflow guard passes and + ticks \s 0, the word's entire remaining effect is the pop already + captured by forth_wait_guard.\ + by simp + +lemma wait_loop_not_modelled: True + \ \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.\ + by simp + +(* ── (- , INIT -- NOT MODELLED ────────────────────────────────────────── *) + +lemma paren_dash_not_modelled: True + \ \(- : 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.\ + by simp + +lemma init_not_modelled: True + \ \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.\ + by simp + +end