theory StarForth_Transition imports StarForth_Mutex begin (* ========================================================================= StarForth_Transition — Labeled Transition System SPECIFICATION ROLE: ground truth for how ExecThread and HeartbeatThread interact. C code must be written so that every execution of vm_tick() satisfies heartbeat_exec_neutral and every word satisfies word_physics_transparent. EXPLICIT AXIOM INVENTORY (this theory) — 2 axioms total: A1 ×1 heartbeat_exec_neutral (C audit: src/vm_time.c) A4'×1 word_physics_transparent (definition audit: Level 1 word theories) The former 8 field axioms are now PROVED from A1 via exec_equiv. The physics substate (rolling_window, heartbeat rate, decay_slope_q48, …) is intentionally unconstrained — the heartbeat is designed to evolve it non-monotonically. exec_equiv makes that silence explicit and structural. ======================================================================== *) (* ========================================================================= Section 1: Thread and action datatypes ======================================================================== *) datatype thread = ExecThread | HeartbeatThread datatype action = ExecWord nat | HeartTick | AcquireTuning nat | ReleaseTuning nat | AcquireDict nat | ReleaseDict nat type_synonym event = "thread \ action" (* ========================================================================= Section 2: Exec-equivalence — the quotient that separates exec from physics Two vm_states are exec-equivalent when they agree on every field that word execution depends on. Physics fields are ABSENT by design: the heartbeat is an adaptive non-monotone controller of those fields, and no ordering or preservation claim is made about them here. exec_equiv is the congruence that collapses heartbeat_step to the identity in the exec quotient vm_state/≃, and under which word execution is a well-defined endomorphism. ======================================================================== *) (* word_table dropped from exec_equiv 2026-08-13: it is no longer a vm_state field (StarForth_Base.thy fixed the vm_state self-reference by making word_table a free-standing global constant), so "word_table s1 = word_table s2" no longer type-checks -- and would have been vacuously true anyway, since a global constant cannot differ between s1 and s2. *) definition exec_equiv :: "vm_state \ vm_state \ bool" (infix "\" 50) where "s1 \ s2 \ data_stack s1 = data_stack s2 \ return_stack s1 = return_stack s2 \ memory s1 = memory s2" lemma exec_equiv_refl [simp, intro]: "vm \ vm" by (simp add: exec_equiv_def) lemma exec_equiv_sym: "s1 \ s2 \ s2 \ s1" by (simp add: exec_equiv_def) lemma exec_equiv_trans: "s1 \ s2 \ s2 \ s3 \ s1 \ s3" by (simp add: exec_equiv_def) lemma exec_equiv_ds: "s1 \ s2 \ data_stack s1 = data_stack s2" by (simp add: exec_equiv_def) lemma exec_equiv_rs: "s1 \ s2 \ return_stack s1 = return_stack s2" by (simp add: exec_equiv_def) lemma exec_equiv_mem:"s1 \ s2 \ memory s1 = memory s2" by (simp add: exec_equiv_def) (* exec_equiv_wt removed 2026-08-13: word_table is global now, not read from state, so this fact no longer type-checks and is not needed. *) (* ========================================================================= Section 3: Heartbeat axiom — A1 ×1 (collapsed from ×8) The heartbeat step is the IDENTITY in the exec quotient: heartbeat_step vm and vm are exec-equivalent. This is the only claim the proof framework makes about heartbeat_step relative to exec-visible state. The physics substate (rolling_window, heartbeat rate, decay_slope_q48, pipeline_metrics, last_inference, ssm_l8, tuning_lock, dict_lock, heat thresholds, dictionary, vm_error, vm_halted, vm_mode) is not mentioned — the heartbeat may evolve it freely, non-monotonically, as the adaptive feedback loops require. That freedom is the design intent. ⚠ AUDIT OBLIGATION (src/vm_time.c): Read every code path reachable from vm_tick() — including vm_tick_window_tuner, vm_tick_slope_validator, and all inference_engine.c callees — and verify that NONE of those paths write to the following three fields: data_stack (vm->data_stack / vm->ds_top) return_stack (vm->return_stack / vm->rs_top) memory (vm->memory[]) Those three fields are exactly exec_equiv. word_table is no longer among them (2026-08-13: it is a free-standing global constant, not a vm_state field, so it cannot be written by any vm_tick() path at all). Everything else is free. ○ CODE-MUST-MATCH: if a future refactor moves any of those four fields into the heartbeat's write set, exec_equiv must be updated and a new audit performed before the axiom can be accepted. ======================================================================== *) axiomatization heartbeat_step :: "vm_state \ vm_state" where heartbeat_exec_neutral: "heartbeat_step vm \ vm" (* ========================================================================= Section 4: Single-step field lemmas — PROVED from A1 (not axioms) These carry [simp] so downstream proofs continue to work without change. ======================================================================== *) lemma heartbeat_ds [simp]: "data_stack (heartbeat_step vm) = data_stack vm" using heartbeat_exec_neutral by (simp add: exec_equiv_def) lemma heartbeat_rs [simp]: "return_stack (heartbeat_step vm) = return_stack vm" using heartbeat_exec_neutral by (simp add: exec_equiv_def) lemma heartbeat_mem [simp]: "memory (heartbeat_step vm) = memory vm" using heartbeat_exec_neutral by (simp add: exec_equiv_def) (* heartbeat_wt removed 2026-08-13: word_table no longer varies by state. *) (* ========================================================================= Section 5: n-fold heartbeat exec-neutrality and field preservation ======================================================================== *) lemma heartbeat_n_exec_neutral: "(heartbeat_step ^^ n) vm \ vm" proof (induction n) case 0 show ?case by simp next case (Suc k) show "(heartbeat_step ^^ Suc k) vm \ vm" using exec_equiv_trans [OF heartbeat_exec_neutral Suc.IH] by simp qed lemma heartbeat_n_steps_ds [simp]: "data_stack ((heartbeat_step ^^ n) vm) = data_stack vm" using heartbeat_n_exec_neutral by (simp add: exec_equiv_def) lemma heartbeat_n_steps_rs [simp]: "return_stack ((heartbeat_step ^^ n) vm) = return_stack vm" using heartbeat_n_exec_neutral by (simp add: exec_equiv_def) lemma heartbeat_n_steps_mem [simp]: "memory ((heartbeat_step ^^ n) vm) = memory vm" using heartbeat_n_exec_neutral by (simp add: exec_equiv_def) (* heartbeat_n_steps_wt removed 2026-08-13: word_table no longer varies by state -- see the note at heartbeat_wt above. *) (* ========================================================================= Section 6: Word physics transparency — A4' ×1 (congruence form) Word execution is a well-defined endomorphism on the exec quotient: if two states are exec-equivalent, executing any word on each produces exec-equivalent results. This is the congruence law that makes word sequences independent of interleaved heartbeat ticks. CORRECTED 2026-08-13: the conclusion was full state equality ("word_table n s1 = word_table n s2"), not \-equivalence. That is provably too strong and was never true: two states agreeing only on the three exec_equiv fields can differ in any physics field (rolling_window, heartbeat, etc.), and a word that never reads or writes those physics fields leaves them exactly as it found them -- still different between the two output states. Concretely, this broke StarForth_Concurrent.thy's foldl_word_table_eq at the empty-list base case, which reduced to needing s1 = s2 from s1 \ s2 alone -- genuinely unprovable. The audit protocol below only ever justified the \ form: "the word body only reads the three exec_equiv fields" gives identical NEW data_stack/return_stack/memory (since those three inputs agree by \), but says nothing about physics fields the word doesn't touch, which simply carry through from s1/s2 respectively and so can still differ. \ is exactly the right conclusion strength -- it is silent about physics fields, which is what the design has always wanted. ⚠ AUDIT PROTOCOL: for each word registered in word_table, verify its body only reads data_stack, return_stack, memory — the three fields of exec_equiv (word_table itself is no longer one of them since 2026-08-13; it is a fixed global, not part of state to read). These are exactly the fields a FORTH word may observe. ○ CODE-MUST-MATCH: no word in src/word_source/ may read rolling_window, heartbeat, decay_slope_q48, pipeline_metrics, last_inference, ssm_l8, tuning_lock, dict_lock, heat thresholds, or any other physics field. ======================================================================== *) (* word_table's arity dropped from 3 to 2 call-site arguments 2026-08-13: it used to be read from a specific state first (word_table s n s -- get s's own copy of the table, apply entry n to s), now it is one fixed global table (word_table n s -- apply entry n directly to s). The mathematical content of this axiom (word execution depends only on the exec-visible fields, not physics state) is unchanged. *) axiomatization where word_physics_transparent: "\ (s1 :: vm_state) (s2 :: vm_state) n. s1 \ s2 \ word_table n s1 \ word_table n s2" (* ========================================================================= Section 7: Consequences — all proved from A1 + A4' ======================================================================== *) lemma exec_after_heartbeat_eq: "word_table n (heartbeat_step vm) \ word_table n vm" by (rule word_physics_transparent [OF heartbeat_exec_neutral]) lemma exec_after_heartbeat_ds: "data_stack (word_table n (heartbeat_step vm)) = data_stack (word_table n vm)" using exec_after_heartbeat_eq exec_equiv_ds by blast lemma exec_after_heartbeat_rs: "return_stack (word_table n (heartbeat_step vm)) = return_stack (word_table n vm)" using exec_after_heartbeat_eq exec_equiv_rs by blast lemma exec_after_n_heartbeats_eq: "word_table n ((heartbeat_step ^^ k) vm) \ word_table n vm" by (rule word_physics_transparent [OF heartbeat_n_exec_neutral]) (* ========================================================================= Section 8: Single-step transition relation ======================================================================== *) inductive vm_step :: "vm_state \ event \ vm_state \ bool" ("_ \[_] _" [60, 0, 61] 60) where StepExec: "\ vm_error vm \ \ vm_halted vm \ vm' = word_table n vm \ vm \[(ExecThread, ExecWord n)] vm'" | StepHeartTick: "\ vm_halted vm \ vm' = heartbeat_step vm \ vm \[(HeartbeatThread, HeartTick)] vm'" | StepAcqTuning: "tuning_lock vm = LockFree \ vm' = vm\tuning_lock := LockHeld t\ \ vm \[(if t = EXEC_THREAD then ExecThread else HeartbeatThread, AcquireTuning t)] vm'" | StepRelTuning: "tuning_lock vm = LockHeld t \ vm' = vm\tuning_lock := LockFree\ \ vm \[(if t = EXEC_THREAD then ExecThread else HeartbeatThread, ReleaseTuning t)] vm'" | StepAcqDict: "dict_lock vm = LockFree \ vm' = vm\dict_lock := LockHeld t\ \ vm \[(if t = EXEC_THREAD then ExecThread else HeartbeatThread, AcquireDict t)] vm'" | StepRelDict: "dict_lock vm = LockHeld t \ vm' = vm\dict_lock := LockFree\ \ vm \[(if t = EXEC_THREAD then ExecThread else HeartbeatThread, ReleaseDict t)] vm'" (* ========================================================================= Section 9: Traces and reachability ======================================================================== *) type_synonym trace = "(vm_state \ event \ vm_state) list" fun valid_trace :: "trace \ bool" where "valid_trace [] = True" | "valid_trace [(s, e, s')] = (s \[e] s')" | "valid_trace ((s, e, s') # rest) = (s \[e] s' \ (case rest of [] \ True | (s0, _, _) # _ \ s0 = s') \ valid_trace rest)" definition reachable :: "vm_state \ vm_state \ bool" where "reachable s0 s' \ s0 = s' \ (\tr. valid_trace tr \ tr \ [] \ fst (hd tr) = s0 \ snd (snd (last tr)) = s')" definition exec_events :: "trace \ (vm_state \ nat \ vm_state) list" where "exec_events tr = [(s, n, s'). (s, (ExecThread, ExecWord n), s') \ tr]" end