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