yeah.lean

import Std
import Lean.Elab.Tactic.Omega

/-!
# The dining philosophers problem, for five philosophers

This file separates three properties which are easy to conflate:

* `fork_has_at_most_one_owner` is **mutual exclusion**: one fork cannot be held
  by two philosophers.
* `step_is_one_fork_pickup` says that picking up forks is sequential: a pickup
  transition acquires exactly one fork, never two atomically.
* `HasForwardMove` is a local **progress** property: some legal pickup can occur.

The first two safety properties do not imply the third.  In the usual
"take the left fork, then wait for the right fork" protocol, every philosopher
can take their left fork.  At that point every right fork is owned by the next
philosopher, nobody is eating, and no pickup transition is enabled.

`every_left_pick_permutation_deadlocks` proves that this does not depend on the
order in which the five philosophers make their first pickup.
-/

namespace DiningPhilosophers

/-- The integers `0, 1, 2, 3, 4`, with the bound carried in the type. -/
abbrev Philosopher := Fin 5

/-- Forks are also numbered `0, 1, 2, 3, 4`. -/
abbrev Fork := Fin 5

/--
A fixed-size array of five forks.  `s f = none` means that fork `f` is on the
table; `s f = some p` means that philosopher `p` holds it.

Using a function on `Fin 5` rather than Lean's mutable `Array` gives exactly the
same mathematical object while making extensional proofs straightforward.
`State.toArray` below supplies an executable array view.
-/
abbrev State := Fork → Option Philosopher

def State.toArray (s : State) : Array (Option Philosopher) :=
  Array.ofFn s

/-- Philosopher `p`'s left fork has the same number as `p`. -/
def leftFork (p : Philosopher) : Fork := p

/-- Philosopher `p`'s right fork is the next fork around the circular table. -/
def rightFork (p : Philosopher) : Fork :=
  ⟨(p.val + 1) % 5, Nat.mod_lt _ (by decide)⟩

theorem rightFork_ne_self (p : Philosopher) : rightFork p ≠ p := by
  revert p
  native_decide

def initial : State := fun _ => none

def Holds (s : State) (p : Philosopher) (f : Fork) : Prop :=
  s f = some p

def ForkFree (s : State) (f : Fork) : Prop :=
  s f = none

/-- Replacing one fork's entry models one atomic pickup. -/
def assign (s : State) (f : Fork) (p : Philosopher) : State :=
  fun g => if g = f then some p else s g

/-- Mutual exclusion follows from storing only one optional owner per fork. -/
theorem fork_has_at_most_one_owner
    (s : State) (f : Fork) (p q : Philosopher)
    (hp : Holds s p f) (hq : Holds s q f) : p = q := by
  exact Option.some.inj (hp.symm.trans hq)

/-- Which hand/fork a philosopher is trying to acquire. -/
inductive Hand where
  | left
  | right
  deriving DecidableEq, Repr

structure Pickup where
  philosopher : Philosopher
  hand : Hand
  deriving DecidableEq, Repr

/--
The deliberately naive protocol studied here:

* a left fork may be taken when it is free;
* a right fork may be taken only after the philosopher holds their left fork.

There is no "put the left fork back while waiting" transition.  This is the
standard protocol whose circular wait produces a deadlock.
-/
def CanTakeLeft (s : State) (p : Philosopher) : Prop :=
  ForkFree s (leftFork p)

def CanTakeRight (s : State) (p : Philosopher) : Prop :=
  Holds s p (leftFork p) ∧ ForkFree s (rightFork p)

instance (s : State) (p : Philosopher) : Decidable (CanTakeLeft s p) := by
  unfold CanTakeLeft ForkFree
  infer_instance

instance (s : State) (p : Philosopher) : Decidable (CanTakeRight s p) := by
  unfold CanTakeRight Holds ForkFree
  infer_instance

/-- One atomic transition; its successful branches update precisely one fork. -/
def step (s : State) (a : Pickup) : Option State :=
  match a.hand with
  | .left =>
      if CanTakeLeft s a.philosopher then
        some (assign s (leftFork a.philosopher) a.philosopher)
      else
        none
  | .right =>
      if CanTakeRight s a.philosopher then
        some (assign s (rightFork a.philosopher) a.philosopher)
      else
        none

/-- A relation spelling out what it means for a transition to acquire one fork. -/
def OneForkPickup (s t : State) : Prop :=
  ∃ f p, ForkFree s f ∧ t = assign s f p

theorem step_is_one_fork_pickup {s t : State} {a : Pickup}
    (h : step s a = some t) : OneForkPickup s t := by
  rcases a with ⟨p, hand⟩
  cases hand with
  | left =>
      simp only [step] at h
      split at h
      next enabled =>
        injection h with ht
        exact ⟨leftFork p, p, enabled, ht.symm⟩
      next => simp at h
  | right =>
      simp only [step] at h
      split at h
      next enabled =>
        injection h with ht
        exact ⟨rightFork p, p, enabled.2, ht.symm⟩
      next => simp at h

/-- A direct formalization of "nobody picks two forks at the same time". -/
def OneForkAtATime : Prop :=
  ∀ ⦃s t : State⦄ ⦃a : Pickup⦄, step s a = some t → OneForkPickup s t

theorem model_obeys_one_fork_at_a_time : OneForkAtATime := by
  intro s t a h
  exact step_is_one_fork_pickup h

/-- A philosopher eats exactly when they hold both adjacent forks. -/
def Eating (s : State) (p : Philosopher) : Prop :=
  Holds s p (leftFork p) ∧ Holds s p (rightFork p)

/-- Local, scheduler-independent progress: at least one pickup is enabled. -/
def HasForwardMove (s : State) : Prop :=
  ∃ a t, step s a = some t

/-- A stuck state in which nobody has reached the eating state. -/
def Deadlocked (s : State) : Prop :=
  (∀ p, ¬ Eating s p) ∧ ¬ HasForwardMove s

/-- The state after every philosopher has taken their left fork. -/
def allLeft : State := fun f => some f

theorem nobody_eats_in_allLeft (p : Philosopher) : ¬ Eating allLeft p := by
  intro h
  have same : rightFork p = p := Option.some.inj h.2
  exact rightFork_ne_self p same

theorem allLeft_step_is_disabled (a : Pickup) : step allLeft a = none := by
  rcases a with ⟨p, hand⟩
  cases hand <;> simp [step, CanTakeLeft, CanTakeRight, ForkFree, allLeft]

theorem allLeft_has_no_forward_move : ¬ HasForwardMove allLeft := by
  rintro ⟨a, t, h⟩
  rw [allLeft_step_is_disabled] at h
  contradiction

theorem allLeft_is_deadlocked : Deadlocked allLeft := by
  exact ⟨nobody_eats_in_allLeft, allLeft_has_no_forward_move⟩

/--
The proposed one-fork-at-a-time rule is satisfied, yet a deadlocked state
exists.  This is the logical statement that the rule is insufficient for
forward progress.
-/
theorem proposed_rule_does_not_guarantee_forward_progress :
    OneForkAtATime ∧ ∃ s, Deadlocked s := by
  exact ⟨model_obeys_one_fork_at_a_time, allLeft, allLeft_is_deadlocked⟩

/-!
## Every permutation of the first pickups has the same bad result

Since each philosopher's left fork has their own number, those five first
pickups never conflict.  `afterLeftPickups order` is the exact ownership array
after the philosophers named in `order` have taken their left forks.
-/

def allPhilosophers : List Philosopher := [0, 1, 2, 3, 4]

def IsCompletePickupOrder (order : List Philosopher) : Prop :=
  order.Perm allPhilosophers

def afterLeftPickups (order : List Philosopher) : State := fun f =>
  if f ∈ order then some f else none

/--
The set-based description above really is produced by the operational `step`:
if `p` has not picked yet, their left fork is free and their pickup extends the
recorded history by one entry.
-/
theorem fresh_left_pick_is_a_legal_step
    (picked : List Philosopher) (p : Philosopher) (fresh : p ∉ picked) :
    step (afterLeftPickups picked) ⟨p, .left⟩ =
      some (afterLeftPickups (p :: picked)) := by
  have enabled : CanTakeLeft (afterLeftPickups picked) p := by
    simp [CanTakeLeft, ForkFree, leftFork, afterLeftPickups, fresh]
  simp only [step, enabled, ↓reduceIte]
  congr 1
  funext f
  by_cases same : f = p
  · subst f
    simp [assign, afterLeftPickups, leftFork, fresh]
  · simp [assign, afterLeftPickups, leftFork, same]

theorem every_philosopher_is_listed : ∀ p : Philosopher, p ∈ allPhilosophers := by
  native_decide

theorem complete_order_has_no_duplicates
    (order : List Philosopher) (h : IsCompletePickupOrder order) :
    order.Nodup := by
  exact h.nodup_iff.mpr (by native_decide)

theorem complete_order_reaches_allLeft
    (order : List Philosopher) (h : IsCompletePickupOrder order) :
    afterLeftPickups order = allLeft := by
  funext f
  have inCanonical : f ∈ allPhilosophers := every_philosopher_is_listed f
  have inOrder : f ∈ order := h.mem_iff.mpr inCanonical
  simp [afterLeftPickups, allLeft, inOrder]

/--
This is the promised counterexample to the proposed progress argument, in its
strongest order-independent form: *every* permutation of the five left-fork
pickups reaches the same deadlock.
-/
theorem every_left_pick_permutation_deadlocks
    (order : List Philosopher) (h : IsCompletePickupOrder order) :
    Deadlocked (afterLeftPickups order) := by
  rw [complete_order_reaches_allLeft order h]
  exact allLeft_is_deadlocked

/-!
## Deadlock freedom versus starvation freedom

Deadlock freedom is a property of reachable states.  Starvation freedom is a
strictly more temporal statement: it talks about what must eventually happen
along executions, so it also needs an explicit scheduler-fairness assumption.
-/

/-- States obtainable from `initial` by zero or more successful pickups. -/
inductive Reachable : State → Prop where
  | initial : Reachable initial
  | next {s t : State} (a : Pickup) :
      Reachable s → step s a = some t → Reachable t

/-- Every duplicate-free collection of completed left pickups is reachable. -/
theorem afterLeftPickups_reachable
    (picked : List Philosopher) (noDuplicates : picked.Nodup) :
    Reachable (afterLeftPickups picked) := by
  induction picked with
  | nil =>
      have emptyPickupsAreInitial :
          afterLeftPickups [] = DiningPhilosophers.initial := by
        funext f
        simp [afterLeftPickups, DiningPhilosophers.initial]
      rw [emptyPickupsAreInitial]
      exact Reachable.initial
  | cons p ps inductionHypothesis =>
      have parts := List.nodup_cons.mp noDuplicates
      have tailReachable := inductionHypothesis parts.2
      exact Reachable.next ⟨p, .left⟩ tailReachable
        (fresh_left_pick_is_a_legal_step ps p parts.1)

theorem allLeft_reachable : Reachable allLeft := by
  have reached := afterLeftPickups_reachable allPhilosophers (by native_decide)
  have complete : IsCompletePickupOrder allPhilosophers := List.Perm.refl _
  rw [complete_order_reaches_allLeft allPhilosophers complete] at reached
  exact reached

/-- The naive protocol would be deadlock-free if no reachable state deadlocked. -/
def ProtocolDeadlockFree : Prop :=
  ∀ s, Reachable s → ¬ Deadlocked s

/-- The reachable `allLeft` state refutes deadlock freedom. -/
theorem naive_protocol_is_not_deadlock_free : ¬ ProtocolDeadlockFree := by
  intro claimedDeadlockFreedom
  exact claimedDeadlockFreedom allLeft allLeft_reachable allLeft_is_deadlocked

/--
An infinite execution may either take a successful step or stutter for one
scheduler tick.  Stuttering is needed to discuss executions after a deadlock and
executions in which the scheduler delays an enabled philosopher.
-/
abbrev Execution := Nat → State

def ValidExecution (execution : Execution) : Prop :=
  ∀ n,
    execution (n + 1) = execution n ∨
      ∃ a, step (execution n) a = some (execution (n + 1))

def ActionEnabled (s : State) (a : Pickup) : Prop :=
  ∃ t, step s a = some t

def ActionTaken (execution : Execution) (n : Nat) (a : Pickup) : Prop :=
  step (execution n) a = some (execution (n + 1))

/--
Weak fairness: if one particular pickup remains enabled at every time from `n`
onwards, then that pickup is eventually taken.  This rules out a scheduler that
ignores a continuously enabled action forever.
-/
def WeaklyFair (execution : Execution) : Prop :=
  ∀ a n,
    (∀ m, n ≤ m → ActionEnabled (execution m) a) →
      ∃ m, n ≤ m ∧ ActionTaken execution m a

/--
Holding the left fork without holding the right records a concrete outstanding
request to eat in this minimal model.
-/
def WaitingToEat (s : State) (p : Philosopher) : Prop :=
  Holds s p (leftFork p) ∧ ¬ Eating s p

/--
Trace-level starvation freedom: every outstanding request is eventually
satisfied on that execution.
-/
def StarvationFree (execution : Execution) : Prop :=
  ∀ p n, WaitingToEat (execution n) p →
    ∃ m, n ≤ m ∧ Eating (execution m) p

/--
Protocol-level starvation freedom quantifies over every weakly fair execution
starting at any reachable state.  Quantifying over reachable suffixes is
equivalent to examining suffixes of executions beginning at `initial`.
-/
def ProtocolStarvationFree : Prop :=
  ∀ s, Reachable s →
    ∀ execution, execution 0 = s →
      ValidExecution execution → WeaklyFair execution →
        StarvationFree execution

/-- The infinite execution which remains in the reachable circular deadlock. -/
def frozenDeadlock : Execution := fun _ => allLeft

theorem frozenDeadlock_is_valid : ValidExecution frozenDeadlock := by
  intro n
  exact Or.inl rfl

/--
The frozen deadlock is weakly fair, vacuously: no pickup is enabled, so no action
is continuously enabled and fairness creates no obligation.
-/
theorem frozenDeadlock_is_weakly_fair : WeaklyFair frozenDeadlock := by
  intro a n continuouslyEnabled
  have enabledNow := continuouslyEnabled n (Nat.le_refl n)
  rcases enabledNow with ⟨t, h⟩
  simp [frozenDeadlock, allLeft_step_is_disabled] at h

theorem every_philosopher_waits_in_allLeft (p : Philosopher) :
    WaitingToEat allLeft p := by
  exact ⟨rfl, nobody_eats_in_allLeft p⟩

theorem frozenDeadlock_is_not_starvation_free :
    ¬ StarvationFree frozenDeadlock := by
  intro claimedStarvationFreedom
  have eventuallyEats :=
    claimedStarvationFreedom 0 0 (every_philosopher_waits_in_allLeft 0)
  rcases eventuallyEats with ⟨m, _, eats⟩
  exact nobody_eats_in_allLeft 0 eats

/--
Even after adding weak scheduler fairness, the naive protocol is not
starvation-free: a reachable deadlock gives a fair infinite execution on which
every philosopher waits forever.
-/
theorem naive_protocol_is_not_starvation_free : ¬ ProtocolStarvationFree := by
  intro claimedStarvationFreedom
  have traceIsStarvationFree :=
    claimedStarvationFreedom allLeft allLeft_reachable frozenDeadlock rfl
      frozenDeadlock_is_valid frozenDeadlock_is_weakly_fair
  exact frozenDeadlock_is_not_starvation_free traceIsStarvationFree

/-!
The literal rule "a philosopher cannot pick up two forks in one transition" is
therefore a safety/atomicity rule, not a progress rule.  Progress needs an extra
protocol constraint which breaks circular wait (for example, global fork
ordering, a waiter/arbitrator, or atomic acquisition of both forks), plus a
fairness assumption if the intended theorem is temporal starvation-freedom.
-/

#eval (initial.toArray.map (Option.map Fin.val))
#eval (allLeft.toArray.map (Option.map Fin.val))

end DiningPhilosophers

/-!
# A positive dining-philosophers protocol

The naive left-first protocol in `DiningPhilosophers.lean` is neither
deadlock-free nor starvation-free.  This file gives a complete positive model
for five philosophers using a central round-robin waiter.

The protocol contract is deliberately explicit:

1. all five philosophers repeatedly request to eat;
2. the waiter visits them in circular order `0, 1, 2, 3, 4, 0, ...`;
3. for the current philosopher, the waiter executes `request`, `grant`, and
   `release` in that order;
4. `grant` atomically assigns both adjacent forks, so no philosopher can hold
   one fork while waiting for the other;
5. `release` frees both forks and advances the waiter.

Because scheduling is part of the protocol, starvation freedom has a concrete
bound instead of an unproved fairness assumption: from *any* configuration,
every philosopher eats within the next 15 transitions.  For five philosophers
the worst actual delay is 14 transitions; `Fin 15` represents offsets `0..14`.
-/

namespace DiningPhilosophers.RoundRobinWaiter

/-- The local phase of the philosopher currently visited by the waiter. -/
inductive Phase where
  | thinking
  | hungry
  | eating
  deriving DecidableEq, Repr

/--
Only the waiter's current philosopher needs a stored phase.  Every other
philosopher is waiting (`hungry`) for their next turn.
-/
structure Config where
  turn : Philosopher
  phase : Phase
  deriving DecidableEq, Repr

def initialConfig : Config :=
  { turn := 0, phase := .thinking }

/-- Exhaustive elimination principle specialized to the fixed five philosophers. -/
theorem philosopher_cases (p : Philosopher) :
    p = 0 ∨ p = 1 ∨ p = 2 ∨ p = 3 ∨ p = 4 := by
  have bounded : p.val < 5 := p.isLt
  have values :
      p.val = 0 ∨ p.val = 1 ∨ p.val = 2 ∨ p.val = 3 ∨ p.val = 4 := by
    omega
  rcases values with h | h | h | h | h
  · left; exact Fin.ext h
  · right; left; exact Fin.ext h
  · right; right; left; exact Fin.ext h
  · right; right; right; left; exact Fin.ext h
  · right; right; right; right; exact Fin.ext h

/-- The waiter moves clockwise after a release. -/
def nextTurn (p : Philosopher) : Philosopher :=
  rightFork p

/--
The complete deterministic state transition.  The three phases make request,
grant/eat, and release observably distinct.
-/
def next : Config → Config
  | ⟨p, .thinking⟩ => ⟨p, .hungry⟩
  | ⟨p, .hungry⟩ => ⟨p, .eating⟩
  | ⟨p, .eating⟩ => ⟨nextTurn p, .thinking⟩

inductive Action where
  | request
  | grant
  | release
  deriving DecidableEq, Repr

def scheduledAction : Config → Action
  | ⟨_, .thinking⟩ => .request
  | ⟨_, .hungry⟩ => .grant
  | ⟨_, .eating⟩ => .release

/-- Exactly the action selected by the waiter may occur. -/
def step (c : Config) (a : Action) : Option Config :=
  if a = scheduledAction c then some (next c) else none

theorem scheduled_step_succeeds (c : Config) :
    step c (scheduledAction c) = some (next c) := by
  simp [step]

/-!
## Fork ownership and safety
-/

/--
Forks are free outside the eating phase.  While `turn` is eating, that
philosopher owns exactly their two adjacent forks.  This is the atomic grant.
-/
def forkState (c : Config) : State :=
  match c.phase with
  | .eating => fun f =>
      if f = leftFork c.turn ∨ f = rightFork c.turn then some c.turn else none
  | .thinking => initial
  | .hungry => initial

def LocalPhase (c : Config) (p : Philosopher) : Phase :=
  if p = c.turn then c.phase else .hungry

def EatingNow (c : Config) (p : Philosopher) : Prop :=
  LocalPhase c p = .eating

def WaitingToEat (c : Config) (p : Philosopher) : Prop :=
  LocalPhase c p = .hungry

instance (c : Config) (p : Philosopher) : Decidable (EatingNow c p) := by
  unfold EatingNow
  infer_instance

instance (s : State) (p : Philosopher) :
    Decidable (DiningPhilosophers.Eating s p) := by
  unfold DiningPhilosophers.Eating Holds
  infer_instance

/-- The phase-level and concrete two-fork definitions of eating coincide. -/
theorem eatingNow_iff_holds_both_forks (c : Config) (p : Philosopher) :
    EatingNow c p ↔ DiningPhilosophers.Eating (forkState c) p := by
  rcases c with ⟨turn, phase⟩
  rcases philosopher_cases turn with rfl | rfl | rfl | rfl | rfl <;>
    rcases philosopher_cases p with rfl | rfl | rfl | rfl | rfl <;>
      cases phase <;> native_decide

/-- No fork can have two distinct owners in any waiter configuration. -/
theorem fork_mutual_exclusion
    (c : Config) (f : Fork) (p q : Philosopher)
    (hp : Holds (forkState c) p f) (hq : Holds (forkState c) q f) :
    p = q := by
  exact fork_has_at_most_one_owner (forkState c) f p q hp hq

/-- At most one philosopher can be eating at a time. -/
theorem at_most_one_eating
    (c : Config) (p q : Philosopher)
    (hp : EatingNow c p) (hq : EatingNow c q) : p = q := by
  unfold EatingNow LocalPhase at hp hq
  split at hp
  next pIsTurn =>
    split at hq
    next qIsTurn => exact pIsTurn.trans qIsTurn.symm
    next => contradiction
  next => contradiction

/-!
## Deadlock freedom
-/

def HasForwardMove (c : Config) : Prop :=
  ∃ a t, step c a = some t

def Deadlocked (c : Config) : Prop :=
  ¬ HasForwardMove c

inductive Reachable : Config → Prop where
  | initial : Reachable initialConfig
  | next {c d : Config} (a : Action) :
      Reachable c → step c a = some d → Reachable d

def ProtocolDeadlockFree : Prop :=
  ∀ c, Reachable c → ¬ Deadlocked c

/-- Stronger than reachable-state deadlock freedom: every `Config` can move. -/
theorem every_config_has_a_forward_move (c : Config) : HasForwardMove c := by
  exact ⟨scheduledAction c, next c, scheduled_step_succeeds c⟩

theorem every_config_is_not_deadlocked (c : Config) : ¬ Deadlocked c := by
  intro isDeadlocked
  exact isDeadlocked (every_config_has_a_forward_move c)

/-- The round-robin waiter protocol is deadlock-free. -/
theorem protocol_is_deadlock_free : ProtocolDeadlockFree := by
  intro c _
  exact every_config_is_not_deadlocked c

/-!
## Executions and starvation freedom
-/

/-- Run the waiter for exactly `ticks` deterministic transitions. -/
def run (start : Config) : Nat → Config
  | 0 => start
  | n + 1 => next (run start n)

def executionFrom (start : Config) : Nat → Config :=
  run start

theorem run_add (start : Config) (n k : Nat) :
    run start (n + k) = run (run start n) k := by
  induction k with
  | zero => simp [run]
  | succ k inductionHypothesis =>
      simp only [run]
      exact congrArg next inductionHypothesis

/--
An execution is valid when it starts in the stated configuration and follows
the waiter's transition on every scheduler tick.
-/
def ValidExecutionFrom (start : Config) (execution : Nat → Config) : Prop :=
  execution 0 = start ∧ ∀ n, execution (n + 1) = next (execution n)

theorem valid_execution_is_run
    {start : Config} {execution : Nat → Config}
    (valid : ValidExecutionFrom start execution) :
    execution = executionFrom start := by
  funext n
  induction n with
  | zero => exact valid.1
  | succ n inductionHypothesis =>
      rw [valid.2 n, inductionHypothesis]
      rfl

/-- Every philosopher is served within offsets `0..14` from every state. -/
theorem bounded_service (c : Config) (p : Philosopher) :
    ∃ offset : Fin 15, EatingNow (run c offset.val) p := by
  rcases c with ⟨turn, phase⟩
  rcases philosopher_cases turn with rfl | rfl | rfl | rfl | rfl <;>
    rcases philosopher_cases p with rfl | rfl | rfl | rfl | rfl <;>
      cases phase <;> native_decide

/-- Trace-level starvation freedom for this explicit request/eat cycle. -/
def StarvationFree (execution : Nat → Config) : Prop :=
  ∀ p n, WaitingToEat (execution n) p →
    ∃ m, n ≤ m ∧ EatingNow (execution m) p

/--
Every canonical round-robin execution is starvation-free.  The proof converts
the finite `bounded_service` witness into an absolute future time `n + offset`.
-/
theorem executionFrom_is_starvation_free (start : Config) :
    StarvationFree (executionFrom start) := by
  intro p n _
  obtain ⟨offset, served⟩ := bounded_service (executionFrom start n) p
  refine ⟨n + offset.val, Nat.le_add_right n offset.val, ?_⟩
  rw [show executionFrom start (n + offset.val) =
      run (executionFrom start n) offset.val by
        exact run_add start n offset.val]
  exact served

def ProtocolStarvationFree : Prop :=
  ∀ start, Reachable start →
    ∀ execution, ValidExecutionFrom start execution →
      StarvationFree execution

/-- The round-robin waiter protocol is starvation-free. -/
theorem protocol_is_starvation_free : ProtocolStarvationFree := by
  intro start _ execution valid
  rw [valid_execution_is_run valid]
  exact executionFrom_is_starvation_free start

/-!
The two positive results have different logical shapes:

* `protocol_is_deadlock_free` needs only the existence of the next scheduled
  action in each state;
* `protocol_is_starvation_free` uses the cyclic schedule and the finite bound
  that every philosopher reaches `.eating` within 15 transitions.
-/

#eval (List.range 15).map fun tick =>
  let c := run initialConfig tick
  (tick, c.turn.val, c.phase)

end DiningPhilosophers.RoundRobinWaiter