109 lines
4.7 KiB
Plaintext
109 lines
4.7 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 (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm))
|
|
= data_stack (word_table vm n vm)"
|
|
by (simp add: exec_after_n_heartbeats_eq)
|
|
|
|
theorem heartbeat_noninterference_rs:
|
|
"\<forall>n k vm.
|
|
return_stack (word_table (heartbeat_step ^^ k $ vm) n (heartbeat_step ^^ k $ vm))
|
|
= return_stack (word_table vm n vm)"
|
|
by (simp add: exec_after_n_heartbeats_eq)
|
|
|
|
(* =========================================================================
|
|
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 identical states. The proof is
|
|
structural: at each step word_physics_transparent (A4') gives FULL state
|
|
equality of the successors (not just exec-field agreement), so the remaining
|
|
foldl is trivially identical — no propagation of equivalence is needed.
|
|
|
|
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.
|
|
======================================================================== *)
|
|
|
|
lemma foldl_word_table_eq:
|
|
assumes "s1 \<simeq> s2"
|
|
shows "foldl (\<lambda>s n. word_table s n s) s1 ws
|
|
= foldl (\<lambda>s n. word_table s n s) s2 ws"
|
|
proof (induction ws arbitrary: s1 s2)
|
|
case Nil thus ?case by simp
|
|
next
|
|
case (Cons w ws)
|
|
(* A4' gives full state equality of the one-step successors *)
|
|
have heq: "word_table s1 w s1 = word_table s2 w s2"
|
|
by (rule word_physics_transparent [OF Cons.prems])
|
|
show ?case by (simp add: heq)
|
|
qed
|
|
|
|
theorem heartbeat_trace_noninterference:
|
|
"\<And> words vm k.
|
|
data_stack
|
|
(foldl (\<lambda>s n. word_table s n s) (heartbeat_step ^^ k $ vm) words)
|
|
= data_stack
|
|
(foldl (\<lambda>s n. word_table s n s) vm words)"
|
|
using foldl_word_table_eq [OF heartbeat_n_exec_neutral] by simp
|
|
|
|
(* =========================================================================
|
|
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 s1 n s1) = data_stack (word_table s2 n s2)"
|
|
using word_physics_transparent [OF assms] by simp
|
|
|
|
lemma word_exec_rs_deterministic:
|
|
assumes "s1 \<simeq> s2"
|
|
shows "return_stack (word_table s1 n s1) = return_stack (word_table s2 n s2)"
|
|
using word_physics_transparent [OF assms] by simp
|
|
|
|
end
|