Robert Allan James
422ef2fa29
Isabelle toolchain replaced (was genuinely 2011, 14+ years stale) and every theory file fixed to actually compile -- most had apparently never been checked under a working Isabelle at all. Fixed the vm_state self-reference in StarForth_Base.thy properly (word_table is now a free-standing global constant, not a circular record field), corrected the word_physics_transparent axiom (was claiming full state equality from mere exec-equivalence, provably too strong), and worked through 14 years of HOL-Library drift plus several missing-hypothesis bugs across the physics-loop and ACL theories. Two genuine (non-tactical) bugs found and left oops-flagged rather than silently resolved: forth_roll's index arithmetic disagrees with both its own test lemma and the real C ROLL implementation (three-way inconsistency), and pm_wf isn't actually preserved by pm_record_hit/pm_record_miss. Both need a decision, not a proof-script fix. Full writeup in FABRIC-2.md item 5.2.
167 lines
9.3 KiB
Plaintext
167 lines
9.3 KiB
Plaintext
theory StarForth_Correctness
|
||
imports
|
||
StarForth_Stack_Words
|
||
StarForth_Arithmetic_Words
|
||
StarForth_Logical_Words
|
||
StarForth_Return_Stack_Words
|
||
StarForth_Memory_Words
|
||
StarForth_Loop1_Heat
|
||
StarForth_Loop2_Window
|
||
StarForth_Loop3_Decay
|
||
StarForth_Loop4_Pipeline
|
||
StarForth_Loop5_WinInf
|
||
StarForth_Loop6_DecayInf
|
||
StarForth_Loop7_Heartrate
|
||
StarForth_Concurrent
|
||
begin
|
||
|
||
(* =========================================================================
|
||
StarForth_Correctness — Top-Level Totality Theorem
|
||
|
||
SORRY-FREE. Every claim in this file is either:
|
||
✓ proved from definitions (fully mechanised)
|
||
○ proved from an explicit named axiom (audit-required, no sorry)
|
||
|
||
EXPLICIT AXIOM INVENTORY (2 axioms total — no sorry):
|
||
|
||
A1 ×1. heartbeat_exec_neutral (StarForth_Transition)
|
||
heartbeat_step vm ≃ vm
|
||
The heartbeat is the identity in vm_state/≃ (exec_equiv).
|
||
C audit: src/vm_time.c vm_tick() must NOT write to
|
||
data_stack, return_stack, or memory. (word_table dropped
|
||
from this list 2026-08-13: it is a free-standing global
|
||
constant now, not a vm_state field, so vm_tick() cannot
|
||
write to it at all.)
|
||
The physics substate is unconstrained — the heartbeat may
|
||
evolve it freely and non-monotonically.
|
||
The former 8 field axioms are now proved lemmas from A1.
|
||
|
||
A4'×1. word_physics_transparent (StarForth_Transition)
|
||
s1 ≃ s2 ⟹ word_table n s1 ≃ word_table n s2
|
||
(corrected 2026-08-13: conclusion is ≃, not literal
|
||
equality -- see the note at its declaration)
|
||
Word execution is a congruence law for ≃.
|
||
Word audit: every Level 1 word body must read ONLY the three
|
||
fields in exec_equiv — never any physics field.
|
||
|
||
Physics invariants (A2/A3) remain removed — clamping suffices.
|
||
heartbeat_trace_noninterference is a proved theorem (foldl induction).
|
||
|
||
TRANSITIVITY CHAIN:
|
||
word semantics (✓ Level 1)
|
||
→ physics invariants (✓ Level 2, proved by clamping — axiom-free)
|
||
→ concurrent non-interference (✓ A1 + A4', fully proved)
|
||
→ OS-level correctness (by transitivity, not in scope here)
|
||
======================================================================== *)
|
||
|
||
(* =========================================================================
|
||
Section 1: Level 1 — Primitive word correctness (all ✓)
|
||
======================================================================== *)
|
||
|
||
thm drop_normal \<comment> \<open>✓ DROP pops TOS\<close>
|
||
thm dup_normal \<comment> \<open>✓ DUP duplicates TOS\<close>
|
||
thm swap_normal \<comment> \<open>✓ SWAP exchanges top two\<close>
|
||
thm over_normal \<comment> \<open>✓ OVER copies second to top\<close>
|
||
thm rot_normal \<comment> \<open>✓ ROT cycles top 3\<close>
|
||
thm swap_involutive \<comment> \<open>✓ SWAP ∘ SWAP = identity\<close>
|
||
thm rot_nrot_inverse \<comment> \<open>✓ ROT ∘ -ROT = identity (corrected name, 2026-08-13)\<close>
|
||
thm add_normal \<comment> \<open>✓ + pops 2, pushes sum\<close>
|
||
thm mul_commutative \<comment> \<open>✓ * is commutative (corrected name, 2026-08-13)\<close>
|
||
thm negate_involutive \<comment> \<open>✓ NEGATE ∘ NEGATE = identity\<close>
|
||
thm abs_nonneg \<comment> \<open>✓ ABS result ≥ 0 (corrected name, 2026-08-13)\<close>
|
||
thm and_normal \<comment> \<open>✓ AND bitwise\<close>
|
||
thm zero_eq_zero \<comment> \<open>✓ 0= of 0 is FORTH_TRUE (corrected name, 2026-08-13)\<close>
|
||
thm zero_tests_exhaustive \<comment> \<open>✓ {0=, 0<, 0>} partition ℤ (corrected name, 2026-08-13)\<close>
|
||
thm to_r_then_from_r \<comment> \<open>✓ >R then R> round-trip\<close>
|
||
thm store_then_fetch \<comment> \<open>✓ ! then @ identity\<close>
|
||
thm cstore_then_cfetch \<comment> \<open>✓ C! then C@ round-trip\<close>
|
||
|
||
(* =========================================================================
|
||
Section 2: Physics field preservation by word execution (all ✓)
|
||
======================================================================== *)
|
||
|
||
lemma pure_ds_word_preserves_physics:
|
||
"rolling_window (vm\<lparr>data_stack := xs\<rparr>) = rolling_window vm"
|
||
"heartbeat (vm\<lparr>data_stack := xs\<rparr>) = heartbeat vm"
|
||
"decay_slope_q48 (vm\<lparr>data_stack := xs\<rparr>) = decay_slope_q48 vm"
|
||
"pipeline_metrics (vm\<lparr>data_stack := xs\<rparr>) = pipeline_metrics vm"
|
||
"last_inference (vm\<lparr>data_stack := xs\<rparr>) = last_inference vm"
|
||
"ssm_l8 (vm\<lparr>data_stack := xs\<rparr>) = ssm_l8 vm"
|
||
"dictionary (vm\<lparr>data_stack := xs\<rparr>) = dictionary vm"
|
||
by simp_all
|
||
(* The word_table conjunct here was removed 2026-08-13: word_table is a
|
||
free-standing global constant now, not a vm_state field, so
|
||
"word_table (vm\<lparr>...\<rparr>)" no longer type-checks -- true by construction. *)
|
||
|
||
(* =========================================================================
|
||
Section 3: Level 2 — Physics invariants (all ✓ or ○)
|
||
======================================================================== *)
|
||
|
||
thm window_advance_preserves_invariant \<comment> \<open>✓ advance preserves window_invariant\<close>
|
||
thm window_grow_preserves_invariant \<comment> \<open>✓ grow preserves window_invariant\<close>
|
||
thm window_shrink_preserves_invariant \<comment> \<open>✓ shrink preserves window_invariant\<close>
|
||
thm vm_decay_step_slope_pos \<comment> \<open>✓ decay step preserves slope_wf\<close>
|
||
thm decay_step_dict_unchanged \<comment> \<open>✓ decay does not touch dictionary\<close>
|
||
thm pm_accuracy_upper_bound \<comment> \<open>✓ accuracy ≤ Q48_ONE\<close>
|
||
thm clamp_window_in_range \<comment> \<open>✓ clamped window ∈ [MIN,MAX]\<close>
|
||
thm apply_window_inference_preserves_invariant \<comment> \<open>✓ proved by clamping (set_eff_window)\<close>
|
||
thm clamp_slope_wf \<comment> \<open>✓ clamped slope satisfies slope_wf\<close>
|
||
thm apply_slope_inference_preserves_wf \<comment> \<open>✓ slope inference preserves slope_wf\<close>
|
||
thm hb_shorten_preserves_wf \<comment> \<open>✓ shorten preserves hb_state_wf\<close>
|
||
thm hb_lengthen_preserves_wf \<comment> \<open>✓ lengthen preserves hb_state_wf\<close>
|
||
thm hb_fire_tick_preserves_wf \<comment> \<open>✓ tick increment preserves hb_state_wf\<close>
|
||
|
||
(* =========================================================================
|
||
Section 4: Level 3 — Concurrency (all ✓ or ○)
|
||
======================================================================== *)
|
||
|
||
thm heartbeat_noninterference \<comment> \<open>✓ one word: heartbeat does not affect result\<close>
|
||
thm heartbeat_noninterference_rs \<comment> \<open>✓ one word: return_stack unaffected\<close>
|
||
thm heartbeat_trace_noninterference \<comment> \<open>✓ proved (foldl induction + A4')\<close>
|
||
thm mutex_exclusive \<comment> \<open>✓ at most one holder per lock\<close>
|
||
thm concurrent_locks_safe_trivial \<comment> \<open>✓ trivial from lock_state algebra\<close>
|
||
|
||
(* =========================================================================
|
||
Section 5: Master correctness theorem (proved — no sorry)
|
||
======================================================================== *)
|
||
|
||
(* The master theorem collects all correctness invariants into a single
|
||
provable conjunction. Every conjunct is either directly proved or follows
|
||
from an explicitly named axiom (A1, A4' listed in the header). *)
|
||
theorem starforth_correctness_totality:
|
||
fixes vm :: vm_state
|
||
assumes wf: "wf_vm vm"
|
||
shows
|
||
(* Level 1: key wf_vm invariants hold. Level 2: physics invariants
|
||
from wf_vm (comment moved out here 2026-08-13 -- it was previously
|
||
embedded mid-string at the "rw_eff_window" line, which is inside a
|
||
quoted prop and does not parse as a comment there; genuine syntax
|
||
error, not a version issue). *)
|
||
"length (data_stack vm) \<le> STACK_SIZE \<and>
|
||
length (return_stack vm) \<le> STACK_SIZE \<and>
|
||
\<not> vm_error vm \<and>
|
||
rw_eff_window (rolling_window vm) \<ge> ADAPTIVE_MIN_WINDOW_SIZE \<and>
|
||
rw_eff_window (rolling_window vm) \<le> ROLLING_WINDOW_SIZE \<and>
|
||
rw_act_window (rolling_window vm) \<le> ROLLING_WINDOW_SIZE \<and>
|
||
rw_act_window (rolling_window vm) =
|
||
min (rw_total_exec (rolling_window vm)) ROLLING_WINDOW_SIZE \<and>
|
||
decay_slope_q48 vm > 0 \<and>
|
||
hb_tick_target_ns (heartbeat vm) > 0"
|
||
using wf by (simp add: wf_vm_def)
|
||
|
||
(* Corollary: non-interference for a word executed after k heartbeat ticks. *)
|
||
corollary word_result_heartbeat_independent:
|
||
"\<forall> n k vm.
|
||
data_stack (word_table n ((heartbeat_step ^^ k) vm))
|
||
= data_stack (word_table n vm)"
|
||
using heartbeat_noninterference by blast
|
||
|
||
(* Corollary: trace-level non-interference (proved theorem). *)
|
||
corollary trace_result_heartbeat_independent:
|
||
"\<And> words vm k.
|
||
data_stack (foldl (\<lambda>s n. word_table n s) ((heartbeat_step ^^ k) vm) words)
|
||
= data_stack (foldl (\<lambda>s n. word_table n s) vm words)"
|
||
using heartbeat_trace_noninterference by blast
|
||
|
||
end
|