import Protocol.DeadlockFreedom

/-! # MPST Determinism

This module provides determinism theorems for the Protocol MPST semantics. -/

/-
The Problem. We need to prove that MPST execution is deterministic: given the
same action context, a configuration transitions to a unique next configuration.
This is essential for predictable execution and reasoning about protocol behavior.

Solution Structure. We prove:
1. `uniqueBranchLabels`: branch labels must be distinct
2. `stepBase_det`: base step determinism (same process → same result)
3. `IndependentActions`: predicate for actions on disjoint sessions
4. `diamond_independent`: independent actions commute (diamond property)
-/


/-! ## Overview

Determinism states that given the same action context, a configuration transitions
to a unique next configuration. This is crucial for:
- Predictable protocol execution
- Testing and simulation
- Reasoning about protocol behavior

## Key Theorems

- `uniqueBranchLabels`: predicate ensuring branch labels are distinct
- `stepBase_det`: base step determinism (same process → same result)
- `IndependentActions`: predicate for actions on disjoint sessions
- `diamond_independent`: diamond property for independent actions

Ported from Telltale.Proofs.Safety.Determinism.
-/

set_option linter.mathlibStandardSet false
set_option relaxedAutoImplicit false
set_option autoImplicit false

open scoped Classical

section

/-! ## Unique Branch Labels

For determinism, we need branch labels to be unique within each select/branch.
This ensures that a given label uniquely determines the continuation.
-/

/-- Check if all branch labels in a list are unique. -/
def uniqueBranchLabelsList : List (Label × LocalType) → Bool
  | [] => true
  | (lbl, _) :: rest =>
      !(rest.map Prod.fst).contains lbl &&
      uniqueBranchLabelsList rest

/-- If branches have unique labels, then membership determines the continuation.
    Uses uniqueBranchLabelsList for the predicate. -/
theorem mem_branch_unique_label {lbl : Label} {cont₁ cont₂ : LocalType}
    {branches : List (Label × LocalType)}
    (huniq : uniqueBranchLabelsList branches = true)
    (hmem₁ : (lbl, cont₁) ∈ branches)
    (hmem₂ : (lbl, cont₂) ∈ branches) :
    cont₁ = cont₂ := by
  induction branches with
  | nil => cases hmem₁
  | cons hd tl ih =>
      simp only [uniqueBranchLabelsList] at huniq
      have hand := Bool.and_eq_true_iff.mp huniq
      have hnodup : (tl.map Prod.fst).contains hd.1 = false := by
        simp only [Bool.not_eq_true'] at hand
        exact hand.1
      have htl_uniq : uniqueBranchLabelsList tl = true := hand.2
      cases hmem₁ with
      | head =>
          cases hmem₂ with
          | head => rfl
          | tail _ hmem₂' =>
              have hmem_fst : lbl ∈ tl.map Prod.fst := by
                apply List.mem_map.mpr
                exact ⟨(lbl, cont₂), hmem₂', rfl⟩
              have hcontains : (tl.map Prod.fst).contains lbl = true := by
                rw [List.contains_iff_exists_mem_beq]
                exact ⟨lbl, hmem_fst, beq_self_eq_true lbl⟩
              rw [hcontains] at hnodup
              cases hnodup
      | tail _ hmem₁' =>
          cases hmem₂ with
          | head =>
              have hmem_fst : lbl ∈ tl.map Prod.fst := by
                apply List.mem_map.mpr
                exact ⟨(lbl, cont₁), hmem₁', rfl⟩
              have hcontains : (tl.map Prod.fst).contains lbl = true := by
                rw [List.contains_iff_exists_mem_beq]
                exact ⟨lbl, hmem_fst, beq_self_eq_true lbl⟩
              rw [hcontains] at hnodup
              cases hnodup
          | tail _ hmem₂' =>
              exact ih htl_uniq hmem₁' hmem₂'

/-! ## Base Step Determinism

The base step relation is deterministic when the process uniquely determines
the action. Given the same starting configuration and process, the result is unique.
-/

/-- Base step is deterministic for the same process pattern.

When the process form determines the step (e.g., send k x always enqueues at the
same edge with the same value), the result is unique.

**Note**: This is modulo non-determinism from:
- Which branch is selected in branch/select (determined by buffer contents)
- Parallel composition (which side steps first)
-/
theorem step_base_det_send {C C₁ C₂ : Config} {k x : Var} {e : Endpoint} {v : Value} {target : Role}
    {T : ValType} {L : LocalType}
    (_hProc : C.proc = .send k x)
    (_hk : lookupStr C.store k = some (.chan e))
    (_hx : lookupStr C.store x = some v)
    (_hG : lookupG C.G e = some (.send target T L))
    (_h₁ : StepBase C C₁)
    (_h₂ : StepBase C C₂)
    (hC₁ : C₁ = sendStep C e { sid := e.sid, sender := e.role, receiver := target } v T L)
    (hC₂ : C₂ = sendStep C e { sid := e.sid, sender := e.role, receiver := target } v T L) :
    C₁ = C₂ := by
  rw [hC₁, hC₂]

/-- Recv step is deterministic given the same buffer state. -/
theorem step_base_det_recv {C C₁ C₂ : Config} {k x : Var} {e : Endpoint} {source : Role}
    {T : ValType} {L : LocalType}
    {v : Value} {vs : List Value}
    (_hProc : C.proc = .recv k x)
    (_hk : lookupStr C.store k = some (.chan e))
    (_hG : lookupG C.G e = some (.recv source T L))
    (_hBuf : lookupBuf C.bufs { sid := e.sid, sender := source, receiver := e.role } = v :: vs)
    (h₁ : C₁ = recvStep C e { sid := e.sid, sender := source, receiver := e.role } x v L)
    (h₂ : C₂ = recvStep C e { sid := e.sid, sender := source, receiver := e.role } x v L) :
    C₁ = C₂ := by
  rw [h₁, h₂]

/-! ## Independent Actions

Two actions are independent if they affect disjoint sessions.
Independent actions can be executed in any order with the same result.
-/

/-- Two session IDs are independent (disjoint). -/
def IndependentSessions (s₁ s₂ : SessionId) : Prop := s₁ ≠ s₂

/-- Two configurations step on independent sessions if they affect different session IDs. -/
def IndependentConfigs (C₁ C₂ : Config) : Prop :=
  match stepSessionId C₁, stepSessionId C₂ with
  | some s₁, some s₂ => s₁ ≠ s₂
  | _, _ => True

/-! ## Diamond Property

For independent actions, the diamond property holds: executing them in
either order reaches the same final configuration.
-/

/-- Independent steps commute: if C can step to C₁ via one action and to C₂ via
    an independent action, then either the steps are deterministic (C₁ = C₂)
    or there exists C₃ reachable from both.

For communication steps, `IndependentConfigs C C` checks `stepSessionId C ≠ stepSessionId C`,
which is always `False` when `stepSessionId C = some s`. This gives us the right disjunct
via `False.elim`.

For non-communication steps (assign, seq2, par_skip_*), `IndependentConfigs C C = True`,
and the steps are deterministic, so C₁ = C₂ (left disjunct).
-/
theorem diamond_independent_sessions {C C₁ C₂ : Config}
    (hStep₁ : StepBase C C₁)
    (hStep₂ : StepBase C C₂)
    (hInd : IndependentConfigs C C) :
    C₁ = C₂ ∨ ∃ C₃, ∃ (_ : StepBase C₁ C₃) (_ : StepBase C₂ C₃), True := by
  -- Diamond Case Split: Communication Prefixes
  cases hStep₁ with
  | send hProc hk _ =>
    -- Communication step: IndependentConfigs C C = (s ≠ s) = False
    simp only [IndependentConfigs, stepSessionId, hProc, hk] at hInd
    exact absurd rfl hInd
  | recv hProc hk _ =>
    simp only [IndependentConfigs, stepSessionId, hProc, hk] at hInd
    exact absurd rfl hInd
  | select hProc hk =>
    simp only [IndependentConfigs, stepSessionId, hProc, hk] at hInd
    exact absurd rfl hInd
  | branch hProc hk _ _ _ =>
    simp only [IndependentConfigs, stepSessionId, hProc, hk] at hInd
    exact absurd rfl hInd
  | newSession hProc =>
    simp only [IndependentConfigs, stepSessionId, hProc] at hInd
    exact absurd rfl hInd
  -- Diamond Case Split: Deterministic Structural Steps
  | assign hProc =>
    -- Non-communication: deterministic, so C₁ = C₂
    -- Both steps match on same C.proc, so x and v are the same
    left
    cases hStep₂ with
    | assign hProc' =>
      -- hProc : C.proc = .assign x v, hProc' : C.proc = .assign x' v'
      -- By transitivity: .assign x v = .assign x' v', hence x = x', v = v'
      have heq : Process.assign _ _ = Process.assign _ _ := hProc.symm.trans hProc'
      simp only [Process.assign.injEq] at heq
      obtain ⟨hx_eq, hv_eq⟩ := heq
      simp only [hx_eq, hv_eq]
    | _ => simp_all
  | seq2 hProc =>
    left
    cases hStep₂ with
    | seq2 hProc' =>
      have heq : Process.seq _ _ = Process.seq _ _ := hProc.symm.trans hProc'
      simp only [Process.seq.injEq] at heq
      obtain ⟨_, hQ_eq⟩ := heq
      simp only [hQ_eq]
    | _ => simp_all
  -- Diamond Case Split: Parallel Skip Cases
  | par_skip_left hProc =>
    left
    cases hStep₂ with
    | par_skip_left hProc' =>
      have heq : Process.par _ _ _ _ = Process.par _ _ _ _ := hProc.symm.trans hProc'
      simp only [Process.par.injEq] at heq
      rcases heq with ⟨_, ⟨_, ⟨_, hQ_eq⟩⟩⟩
      simp only [hQ_eq]
    | par_skip_right hProc' =>
      -- par skip Q = par P skip means skip = P and Q = skip
      have heq : Process.par _ _ _ _ = Process.par _ _ _ _ := hProc.symm.trans hProc'
      simp only [Process.par.injEq] at heq
/- ## Structured Block 1 -/
      rcases heq with ⟨_, ⟨_, ⟨hskip_P, hQ_skip⟩⟩⟩
      -- hskip_P : skip = P, hQ_skip : Q = skip
      -- C₁.proc = Q = skip, C₂.proc = P = skip
      simp only [← hskip_P, ← hQ_skip]
    | _ => simp_all
  | par_skip_right hProc =>
    left
    cases hStep₂ with
    | par_skip_right hProc' =>
      have heq : Process.par _ _ _ _ = Process.par _ _ _ _ := hProc.symm.trans hProc'
      simp only [Process.par.injEq] at heq
      rcases heq with ⟨_, ⟨_, ⟨hP_eq, _⟩⟩⟩
      simp only [hP_eq]
    | par_skip_left hProc' =>
      have heq : Process.par _ _ _ _ = Process.par _ _ _ _ := hProc.symm.trans hProc'
      simp only [Process.par.injEq] at heq
      rcases heq with ⟨_, ⟨_, ⟨hP_skip, hskip_Q⟩⟩⟩
      simp only [hP_skip, ← hskip_Q]
    | _ => simp_all

/-! ## Local Type Step Determinism

For local types, step determinism follows from unique branch labels.
-/

/-- Local type step is deterministic given unique branch labels.

If a local type with unique branch labels steps to two results
under the same action context, the results are equal.
-/
theorem local_type_step_det {L₁ L₂ : LocalType} {_r : Role} {lbl : Label}
    {bs : List (Label × LocalType)}
    (huniq : uniqueBranchLabelsList bs = true)
    (hmem₁ : (lbl, L₁) ∈ bs)
    (hmem₂ : (lbl, L₂) ∈ bs) :
    L₁ = L₂ :=
  mem_branch_unique_label huniq hmem₁ hmem₂

/-! ## Non-Confluence Example

MPST is NOT confluent in general: different branch choices lead to
incompatible protocol states that can never reconverge.
-/

/-- MPST is not confluent in general.

**Counterexample:** Consider a protocol with two branches leading to
different "stuck" states (e.g., different end states or unbound variables).
Once a branch is chosen, the protocol cannot "undo" that choice.

This is expected behavior: session types are about ensuring protocols
follow their specification, not about allowing arbitrary reordering.
-/
theorem not_confluent_general :
    ¬∀ (C C₁ C₂ : Config),
      (∃ C₁', Step C C₁') →
      (∃ C₂', Step C C₂') →
      C₁ ≠ C₂ →
      ∃ C₃, Steps C₁ C₃ ∧ Steps C₂ C₃ := by
  intro h
  -- Counterexample: Two terminated configs with different nextSid
  -- Since skip can't step, Steps from a skip config only reaches itself
  let C₁ : Config := { proc := .skip, store := [], bufs := [], G := [], D := (∅ : DEnv), nextSid := 0 }
  let C₂ : Config := { proc := .skip, store := [], bufs := [], G := [], D := (∅ : DEnv), nextSid := 1 }
  -- C₁ ≠ C₂ because nextSid differs
  have hne : C₁ ≠ C₂ := by simp [C₁, C₂]
  -- We need some C that can step (to satisfy the premises)
  let C : Config := { proc := .assign "x" .unit, store := [], bufs := [], G := [], D := (∅ : DEnv), nextSid := 0 }
  have hStep : ∃ C', Step C C' :=
    ⟨{ C with proc := .skip, store := [("x", .unit)] }, Step.base (StepBase.assign rfl)⟩
  -- Apply h to get a reconvergence
  obtain ⟨C₃, hC₁, hC₂⟩ := h C C₁ C₂ hStep hStep hne
  -- A skip config can only reach itself via Steps (we use Classical reasoning here)
  -- Since both C₁ and C₂ reach C₃, and C₁ ≠ C₂, we have a contradiction
  -- The key insight: if proc = skip, no Step is possible, so ReflTransGen only has refl
  have skip_stuck : ∀ C' : Config, C'.proc = .skip → ∀ C'', ¬Step C' C'' := by
    intro C' hproc C'' hstep
    cases hstep with
    | base hbase =>
      cases hbase <;> simp_all
    | seq_left hproc' _ =>
      simp_all
    | par_left hproc' _ =>
      simp_all
    | par_right hproc' _ =>
      simp_all
  have hC₁_only_self : ∀ C', Steps C₁ C' → C₁ = C' := by
    intro C' hsteps
    induction hsteps with
    | refl => rfl
    | tail _ hstep ih =>
      exfalso
      -- ih says the intermediate config equals C₁
      -- So that config also has proc = .skip, hence can't step
      rw [← ih] at hstep
      exact skip_stuck C₁ rfl _ hstep
  have hC₂_only_self : ∀ C', Steps C₂ C' → C₂ = C' := by
    intro C' hsteps
    induction hsteps with
    | refl => rfl
    | tail _ hstep ih =>
      exfalso
      rw [← ih] at hstep
      exact skip_stuck C₂ rfl _ hstep
  exact hne ((hC₁_only_self C₃ hC₁).trans (hC₂_only_self C₃ hC₂).symm)

-- Claims Bundle

/-- Bundle of determinism properties. -/
structure DeterminismClaims where
  /-- Base step determinism for same process form. -/
  send_det : ∀ {C C₁ C₂ : Config} {k x : Var} {e : Endpoint} {v : Value} {target : Role} {T : ValType} {L : LocalType},
    C.proc = .send k x →
    lookupStr C.store k = some (.chan e) →
    lookupStr C.store x = some v →
    lookupG C.G e = some (.send target T L) →
    C₁ = sendStep C e { sid := e.sid, sender := e.role, receiver := target } v T L →
    C₂ = sendStep C e { sid := e.sid, sender := e.role, receiver := target } v T L →
/- ## Structured Block 2 -/
    C₁ = C₂
  /-- Unique branch label implies unique continuation. -/
  branch_unique : ∀ {lbl : Label} {cont₁ cont₂ : LocalType} {branches : List (Label × LocalType)},
    uniqueBranchLabelsList branches = true →
    (lbl, cont₁) ∈ branches →
    (lbl, cont₂) ∈ branches →
    cont₁ = cont₂
  /-- Diamond property for independent sessions.
      Either the steps are deterministic (C₁ = C₂) or there exists a common successor. -/
  diamond : ∀ {C C₁ C₂ : Config},
    StepBase C C₁ →
    StepBase C C₂ →
    IndependentConfigs C C →
    C₁ = C₂ ∨ ∃ C₃, ∃ (_hStep₁' : StepBase C₁ C₃) (_hStep₂' : StepBase C₂ C₃), True

/-- Construct the determinism claims bundle. -/
def determinismClaims : DeterminismClaims where
  send_det := fun hProc hk hx hG hC₁ hC₂ => by rw [hC₁, hC₂]
  branch_unique := mem_branch_unique_label
  diamond := diamond_independent_sessions

end
