Machinery for constructing infinite fair executions

The main goal of this file is to define a fairScheduler that, given a function d of type DeliverMsg, a state predicate q, and a state s0 of an algorithm a, constructs an infinite execution of a starting from state s0 in which all processes from a set ps are fair and q is true infinitely often. With additional assumptions, we may also want to require that all actions in the infinite execution satisfy an action predicate r.

def Cslib.FLP.DeliverMsg (P : Type u_4) (M : Type u_5) (S : Type u_6) : Type (max (max (max (max (max (max u_6 u_5) u_4) u_5) u_4) (max u_6 u_5) u_4) u_5 u_4)

Given a state s and a message m, a function d of type DeliverMsg is supposed to return (xs, t) where xs is a finite execution from s to t in which m is delivered.

Equations

• Cslib.FLP.DeliverMsg P M S = (Cslib.FLP.State P M S → Cslib.FLP.Message P M → List (Cslib.FLP.Action P M) × Cslib.FLP.State P M S)

def Cslib.FLP.DeliverMsg.ForallActions {P : Type u_1} {M : Type u_2} {S : Type u_3} (d : DeliverMsg P M S) (r : Action P M → Prop) : Prop

d.ForallActions r requires that all actions returned by d satisfy r.

Equations

• d.ForallActions r = ∀ (s : Cslib.FLP.State P M S) (m : Cslib.FLP.Message P M), List.Forall r (d s m).1

def Cslib.FLP.DeliverMsg.foldList {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (d : DeliverMsg P M S) (s : State P M S) : List (Message P M) → Finset (Message P M) → List (Action P M) × State P M S

d.foldList s ml ms uses d to deliver all messages that are in ml but not in ms from state s. Note that if a message m in ml is delivered during the delivery of an earlier message, m is added to ms so that it is not processed again.

Equations

• One or more equations did not get rendered due to their size.
• d.foldList s [] x✝ = ([], s)

noncomputable def Cslib.FLP.DeliverMsg.scheduleMsgs {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (d : DeliverMsg P M S) (ps : Set P) (s : State P M S) : List (Action P M) × State P M S

d.scheduleMsgs ps s schedules and delivers all messages which are in-flight in state s and have destinations in ps in some order (as determined by choice). If no such message exists, then the the stuttering step is taken.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.FLP.DeliverMsg.foldList_forallActions {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {d : DeliverMsg P M S} {r : Action P M → Prop} (s : State P M S) (ml : List (Message P M)) (ms : Finset (Message P M)) (h : d.ForallActions r) : List.Forall r (d.foldList s ml ms).1

If d.ForallActions r, then d.foldList s ml ms can only use actions satisfying r.

noncomputable def Cslib.FLP.Algorithm.fairScheduler {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (d : DeliverMsg P M S) (ps : Set P) (s0 : State P M S) : ℕ → List (Action P M) × State P M S

Starting from state s0, a.fairSchedular d ps s0 constructs an infinite sequence of finite executions of a by repeatedly applying d.scheduleMsgs ps.

Equations

• a.fairScheduler d ps s0 0 = ([], s0)
• a.fairScheduler d ps s0 k.succ = d.scheduleMsgs ps (a.fairScheduler d ps s0 k).2

noncomputable def Cslib.FLP.Algorithm.fairSegEnds {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (d : DeliverMsg P M S) (ps : Set P) (s0 : State P M S) : ωSequence (State P M S)

The infinite sequence of states forming the end states of the finite executions constructed by Algorithm.fairScheduler.

Equations

• a.fairSegEnds d ps s0 = { get := fun (k : ℕ) => (a.fairScheduler d ps s0 k).2 }

noncomputable def Cslib.FLP.Algorithm.fairSegActions {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (d : DeliverMsg P M S) (ps : Set P) (s0 : State P M S) : ωSequence (List (Action P M))

The infinite sequence of finite action sequences from the finite executions constructed by Algorithm.fairScheduler.

Equations

• a.fairSegActions d ps s0 = { get := fun (k : ℕ) => (a.fairScheduler d ps s0 k).1 }.tail

def Cslib.FLP.Algorithm.FairDeliverMsg {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] (a : Algorithm P M S) (d : DeliverMsg P M S) (ps : Set P) (q : State P M S → Prop) : Prop

a.FairDeliverMsg d ps q says that for any state s of a satisfying q and any message m which is in-flight in s and whose destination is in ps, d s m produces a legal finite execution of a in which m is delivered and which ends in a state satisfying q again.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.FLP.FairScheduler.fairScheduler_init {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) : (a.fairSegEnds d ps s0) 0 = s0

Re-stating the definition of Algorithm.fairScheduler as a mutual recursion of Algorithm.fairSegEnds and Algorithm.fairSegActions.

theorem Cslib.FLP.FairScheduler.fairScheduler_step {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) (k : ℕ) : d.scheduleMsgs ps ((a.fairSegEnds d ps s0) k) = ((a.fairSegActions d ps s0) k, (a.fairSegEnds d ps s0) (k + 1))

Re-stating the definition of Algorithm.fairScheduler as a mutual recursion of Algorithm.fairSegEnds and Algorithm.fairSegActions.

theorem Cslib.FLP.FairScheduler.fairSeg_forallActions {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} {r : Action P M → Prop} (ps : Set P) (s0 : State P M S) (k : ℕ) (ha : d.ForallActions r) (hn : r none) : List.Forall r ((a.fairSegActions d ps s0) k)

If d.ForallActions r, then a.fairSegActions d ps s0 can only use actions satisfying r.

theorem Cslib.FLP.FairScheduler.fairDeliverMsg_foldList {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} (hd : a.FairDeliverMsg d ps q) (s : State P M S) (ml : List (Message P M)) (ms : Finset (Message P M)) (hs : q s ∧ ∀ m ∈ ml, m ∉ ms → m ∈ s.msgs ∧ m.dest ∈ ps) : match d.foldList s ml ms with | (xl, t) => a.lts.MTr s xl t ∧ q t ∧ ∀ m ∈ ml, m ∉ ms → some m ∈ xl

The correctness of d.foldList s ml ms under the assumption a.FairDeliverMsg d ps q.

theorem Cslib.FLP.FairScheduler.fairDeliverMsg_scheduleMsgs {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} (hd : a.FairDeliverMsg d ps q) (s : State P M S) (hs : q s) : have xl := (d.scheduleMsgs ps s).1; have t := (d.scheduleMsgs ps s).2; q t ∧ a.lts.MTr s xl t ∧ xl.length > 0 ∧ ∀ m ∈ s.msgs, m.dest ∈ ps → some m ∈ xl

The correctness of d.scheduleMsgs ps s under the assumption a.FairDeliverMsg d ps q.

theorem Cslib.FLP.FairScheduler.fair_fairSegs {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) : have ts := a.fairSegEnds d ps s0; have xls := a.fairSegActions d ps s0; ∀ (k : ℕ), q (ts k) ∧ a.lts.MTr (ts k) (xls k) (ts (k + 1)) ∧ (xls k).length > 0 ∧ ∀ m ∈ (ts k).msgs, m.dest ∈ ps → some m ∈ xls k

The correctness of a.fairSegEnds d ps s0 and a.fairSegActions d ps s0 under the assumption a.FairDeliverMsg d ps q.

theorem Cslib.FLP.FairScheduler.flatten_fairSegs {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ps : Set P} {ts : ωSequence (State P M S)} {xls : ωSequence (List (Action P M))} (hmtr : ∀ (k : ℕ), a.lts.MTr (ts k) (xls k) (ts (k + 1))) (hpos : ∀ (k : ℕ), (xls k).length > 0) (hsch : ∀ (k : ℕ), ∀ m ∈ (ts k).msgs, m.dest ∈ ps → some m ∈ xls k) : ∃ (ss : ωSequence (State P M S)), a.lts.OmegaExecution ss xls.flatten ∧ (∀ (k : ℕ), ss (xls.cumLen k) = ts k) ∧ ∀ p ∈ ps, ProcFair p ss xls.flatten

Given an infinite sequence of non-empty finite executions of algorithm a, if all messages with destinations in ps that are in-flight at the beginning of each finite execution are delivered in that finite execution, then those finite executions can be concatenated into an infinite execution of a in which every process in ps is fair.

theorem Cslib.FLP.FairScheduler.fair_omegaExecution {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) : have ts := a.fairSegEnds d ps s0; have xls := a.fairSegActions d ps s0; ∃ (ss : ωSequence (State P M S)), a.lts.OmegaExecution ss xls.flatten ∧ ss 0 = s0 ∧ (∀ (k : ℕ), ss (xls.cumLen k) = ts k) ∧ (∀ (k : ℕ), q (ss (xls.cumLen k))) ∧ (∀ (k : ℕ), (xls k).length > 0) ∧ ∀ p ∈ ps, ProcFair p ss xls.flatten

Under the assumption a.FairDeliverMsg d ps q, the infinite sequence of finite executions of a represented by a.fairSegEnds d ps s0 and a.fairSegActions d ps s0 can be concatenated into an infinite execution of a in which every process in ps is fair and q is true at the ends of all those finite executions.

theorem Cslib.FLP.FairScheduler.omega_forall_actions {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop} {r : Action P M → Prop} (hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) (ha : d.ForallActions r) (hn : r none) (k : ℕ) : r ((a.fairSegActions d ps s0).flatten k)

If d.ForallActions r, then the concatenation of all a.fairSegActions d ps s0 segments can only use actions satisfying r.