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