Fairness of dynamic concurrent runs

This file adds the first fairness layer on top of Concurrent.ProcessOver.Run.

The key design choice is that fairness is phrased in terms of stable Tickets, not raw frontier events. This matters because the concrete event type available at one residual process state need not even be comparable with the event type at a later state, while a ticket is meant to name the same scheduling obligation across time and across different presentations of the same protocol.

The closed-world Process API is recovered as a specialization of these generic definitions.

def Interaction.Concurrent.ProcessOver.Run.Always (P : ℕ → Prop) : Prop

Always P means that the temporal property P holds at every time index.

def Interaction.Concurrent.ProcessOver.Run.Eventually (P : ℕ → Prop) : Prop

Eventually P means that P holds at some time index.

def Interaction.Concurrent.ProcessOver.Run.EventuallyAlways (P : ℕ → Prop) : Prop

EventuallyAlways P means that from some time onward, P keeps holding forever.

def Interaction.Concurrent.ProcessOver.Run.InfinitelyOften (P : ℕ → Prop) : Prop

InfinitelyOften P means that P holds at arbitrarily late time indices.

theorem Interaction.Concurrent.ProcessOver.Run.always_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : Always P → Always Q

theorem Interaction.Concurrent.ProcessOver.Run.eventually_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : Eventually P → Eventually Q

theorem Interaction.Concurrent.ProcessOver.Run.eventuallyAlways_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : EventuallyAlways P → EventuallyAlways Q

theorem Interaction.Concurrent.ProcessOver.Run.infinitelyOften_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : InfinitelyOften P → InfinitelyOften Q

def Interaction.Concurrent.ProcessOver.Ticketed.enabledAt {Γ : Spec.Node.Context} (ticketed : Ticketed Γ) (run : ticketed.toProcess.Run) (ticket : ticketed.Ticket) (n : ℕ) : Prop

enabledAt ticketed run ticket n means that at time n, there exists some complete transcript of the current process step whose stable ticket is ticket.

def Interaction.Concurrent.ProcessOver.Ticketed.firedAt {Γ : Spec.Node.Context} (ticketed : Ticketed Γ) (run : ticketed.toProcess.Run) (ticket : ticketed.Ticket) (n : ℕ) : Prop

firedAt ticketed run ticket n means that the actual transcript chosen by the run at time n has stable ticket ticket.

def Interaction.Concurrent.ProcessOver.Ticketed.WeakFairOn {Γ : Spec.Node.Context} (ticketed : Ticketed Γ) (run : ticketed.toProcess.Run) (ticket : ticketed.Ticket) : Prop

Weak fairness for one ticket: if the ticket is continuously enabled from some point onward, then it fires infinitely often.

def Interaction.Concurrent.ProcessOver.Ticketed.StrongFairOn {Γ : Spec.Node.Context} (ticketed : Ticketed Γ) (run : ticketed.toProcess.Run) (ticket : ticketed.Ticket) : Prop

Strong fairness for one ticket: if the ticket is enabled infinitely often, then it is fired infinitely often.

def Interaction.Concurrent.ProcessOver.Ticketed.WeakFair {Γ : Spec.Node.Context} (ticketed : Ticketed Γ) (run : ticketed.toProcess.Run) : Prop

A run is weakly fair when every ticket is weakly fair.

def Interaction.Concurrent.ProcessOver.Ticketed.StrongFair {Γ : Spec.Node.Context} (ticketed : Ticketed Γ) (run : ticketed.toProcess.Run) : Prop

A run is strongly fair when every ticket is strongly fair.

theorem Interaction.Concurrent.ProcessOver.Ticketed.fired_implies_enabled {Γ : Spec.Node.Context} (ticketed : Ticketed Γ) (run : ticketed.toProcess.Run) (ticket : ticketed.Ticket) (n : ℕ) : ticketed.firedAt run ticket n → ticketed.enabledAt run ticket n

The actually fired ticket at time n is always enabled at time n.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.Always (P : ℕ → Prop) : Prop

The closed-world specialization of Always.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.Eventually (P : ℕ → Prop) : Prop

The closed-world specialization of Eventually.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.EventuallyAlways (P : ℕ → Prop) : Prop

The closed-world specialization of EventuallyAlways.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Run.InfinitelyOften (P : ℕ → Prop) : Prop

The closed-world specialization of InfinitelyOften.

theorem Interaction.Concurrent.Process.Run.always_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : Always P → Always Q

theorem Interaction.Concurrent.Process.Run.eventually_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : Eventually P → Eventually Q

theorem Interaction.Concurrent.Process.Run.eventuallyAlways_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : EventuallyAlways P → EventuallyAlways Q

theorem Interaction.Concurrent.Process.Run.infinitelyOften_mono {P Q : ℕ → Prop} (himp : ∀ (n : ℕ), P n → Q n) : InfinitelyOften P → InfinitelyOften Q

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Ticketed.enabledAt {Party : Type u} (ticketed : Ticketed Party) (run : Run ticketed.toProcess) (ticket : ticketed.Ticket) (n : ℕ) : Prop

The closed-world specialization of enabledAt.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Ticketed.firedAt {Party : Type u} (ticketed : Ticketed Party) (run : Run ticketed.toProcess) (ticket : ticketed.Ticket) (n : ℕ) : Prop

The closed-world specialization of firedAt.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Ticketed.WeakFairOn {Party : Type u} (ticketed : Ticketed Party) (run : Run ticketed.toProcess) (ticket : ticketed.Ticket) : Prop

The closed-world specialization of weak fairness for one ticket.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Ticketed.StrongFairOn {Party : Type u} (ticketed : Ticketed Party) (run : Run ticketed.toProcess) (ticket : ticketed.Ticket) : Prop

The closed-world specialization of strong fairness for one ticket.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Ticketed.WeakFair {Party : Type u} (ticketed : Ticketed Party) (run : Run ticketed.toProcess) : Prop

The closed-world specialization of weak fairness.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Ticketed.StrongFair {Party : Type u} (ticketed : Ticketed Party) (run : Run ticketed.toProcess) : Prop

The closed-world specialization of strong fairness.

theorem Interaction.Concurrent.Process.Ticketed.fired_implies_enabled {Party : Type u} (ticketed : Ticketed Party) (run : Run ticketed.toProcess) (ticket : ticketed.Ticket) (n : ℕ) : ticketed.firedAt run ticket n → ticketed.enabledAt run ticket n