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.
128 lines
5.6 KiB
Plaintext
128 lines
5.6 KiB
Plaintext
theory StarForth_Concurrent
|
|
imports StarForth_Transition StarForth_Loop7_Heartrate StarForth_Loop3_Decay
|
|
begin
|
|
|
|
(* =========================================================================
|
|
StarForth_Concurrent — Non-Interference and Mutex Safety
|
|
|
|
SORRY-FREE. Every result here is fully proved from 2 axioms:
|
|
A1 heartbeat_exec_neutral (StarForth_Transition)
|
|
A4' word_physics_transparent (StarForth_Transition)
|
|
|
|
The exec_equiv quotient (≃) from StarForth_Transition is the common thread:
|
|
A1 says heartbeat_step is the identity in vm_state/≃.
|
|
A4' says word execution is a congruence law for ≃.
|
|
Together they make arbitrary word sequences independent of heartbeat timing.
|
|
======================================================================== *)
|
|
|
|
(* =========================================================================
|
|
Section 1: Single-word non-interference (proved from exec_after_n_heartbeats_eq)
|
|
======================================================================== *)
|
|
|
|
theorem heartbeat_noninterference:
|
|
"\<forall>n k vm.
|
|
data_stack (word_table n ((heartbeat_step ^^ k) vm))
|
|
= data_stack (word_table n vm)"
|
|
using exec_after_n_heartbeats_eq exec_equiv_ds by blast
|
|
|
|
theorem heartbeat_noninterference_rs:
|
|
"\<forall>n k vm.
|
|
return_stack (word_table n ((heartbeat_step ^^ k) vm))
|
|
= return_stack (word_table n vm)"
|
|
using exec_after_n_heartbeats_eq exec_equiv_rs by blast
|
|
|
|
(* =========================================================================
|
|
Section 2: Trace-level non-interference (proved by induction over ≃)
|
|
|
|
foldl_word_table_eq: if two initial states are exec-equivalent (≃), then
|
|
running any word sequence on each produces exec-equivalent (not
|
|
identical -- CORRECTED 2026-08-13, see StarForth_Transition.thy's note
|
|
at word_physics_transparent for why full equality was never provable)
|
|
states. The proof is structural: at each step word_physics_transparent
|
|
(A4') gives ≃ of the successors, which is exactly what arbitrary: s1 s2
|
|
needs to carry the induction through.
|
|
|
|
heartbeat_trace_noninterference follows immediately by instantiating with
|
|
s1 = (heartbeat_step ^^ k) vm, s2 = vm, using heartbeat_n_exec_neutral.
|
|
|
|
○ CODE-MUST-MATCH: the inductive argument holds only if word_physics_transparent
|
|
holds for every word — see the audit protocol in StarForth_Transition.thy.
|
|
======================================================================== *)
|
|
|
|
(* Restated 2026-08-13 with explicit object-level \<forall>/\<longrightarrow> instead of
|
|
assumes/shows + arbitrary: s1 s2 -- the assumes/arbitrary combination
|
|
was not reliably carrying "s1 \<simeq> s2" into the Nil case as Nil.prems
|
|
despite multiple tactics (simp, rule, metis with the fact named
|
|
explicitly all failed identically); this form sidesteps the whole
|
|
revert-and-generalize mechanism by quantifying s1/s2 in the goal from
|
|
the start. *)
|
|
lemma foldl_word_table_eq:
|
|
"\<forall>s1 s2. s1 \<simeq> s2 \<longrightarrow>
|
|
foldl (\<lambda>s n. word_table n s) s1 ws \<simeq> foldl (\<lambda>s n. word_table n s) s2 ws"
|
|
proof (induction ws)
|
|
case Nil
|
|
show ?case by simp
|
|
next
|
|
case (Cons w ws)
|
|
show ?case
|
|
proof (intro allI impI)
|
|
fix s1 s2 :: vm_state
|
|
assume h: "s1 \<simeq> s2"
|
|
have heq: "word_table w s1 \<simeq> word_table w s2"
|
|
using h word_physics_transparent by blast
|
|
have "foldl (\<lambda>s n. word_table n s) (word_table w s1) ws
|
|
\<simeq> foldl (\<lambda>s n. word_table n s) (word_table w s2) ws"
|
|
using Cons.IH heq by blast
|
|
thus "foldl (\<lambda>s n. word_table n s) s1 (w # ws)
|
|
\<simeq> foldl (\<lambda>s n. word_table n s) s2 (w # ws)"
|
|
by simp
|
|
qed
|
|
qed
|
|
|
|
theorem heartbeat_trace_noninterference:
|
|
"\<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 foldl_word_table_eq [rule_format, OF heartbeat_n_exec_neutral] exec_equiv_ds
|
|
by blast
|
|
|
|
(* =========================================================================
|
|
Section 3: Mutex safety (proved from lock_state algebra)
|
|
======================================================================== *)
|
|
|
|
definition concurrent_locks_safe :: "vm_state \<Rightarrow> bool" where
|
|
"concurrent_locks_safe vm \<longleftrightarrow>
|
|
(\<forall>t u. tuning_lock vm = LockHeld t \<longrightarrow> tuning_lock vm = LockHeld u \<longrightarrow> t = u) \<and>
|
|
(\<forall>t u. dict_lock vm = LockHeld t \<longrightarrow> dict_lock vm = LockHeld u \<longrightarrow> t = u)"
|
|
|
|
lemma mutex_exclusive:
|
|
"tuning_lock vm = LockHeld t \<Longrightarrow> tuning_lock vm = LockHeld u \<Longrightarrow> t = u"
|
|
by simp
|
|
|
|
lemma concurrent_locks_safe_trivial:
|
|
"concurrent_locks_safe vm"
|
|
by (simp add: concurrent_locks_safe_def)
|
|
|
|
lemma vm_step_preserves_lock_safety:
|
|
assumes "vm \<rightarrow>[e] vm'"
|
|
shows "concurrent_locks_safe vm'"
|
|
by (simp add: concurrent_locks_safe_def)
|
|
|
|
(* =========================================================================
|
|
Section 4: Word execution determinism under ≃ (corollaries of A4')
|
|
======================================================================== *)
|
|
|
|
lemma word_exec_deterministic:
|
|
assumes "s1 \<simeq> s2"
|
|
shows "data_stack (word_table n s1) = data_stack (word_table n s2)"
|
|
using word_physics_transparent [OF assms] exec_equiv_ds by blast
|
|
|
|
lemma word_exec_rs_deterministic:
|
|
assumes "s1 \<simeq> s2"
|
|
shows "return_stack (word_table n s1) = return_stack (word_table n s2)"
|
|
using word_physics_transparent [OF assms] exec_equiv_rs by blast
|
|
|
|
end
|