Skip to content

Commit e7076ee

Browse files
ctchouctchou
committed
feat(FLP): some technical machineries for reasoning about diamond and fairness properties
1 parent 43f68e9 commit e7076ee

4 files changed

Lines changed: 389 additions & 2 deletions

File tree

‎Cslib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,9 @@ public import Cslib.Computability.Automata.NA.Sum
2323
public import Cslib.Computability.Automata.NA.ToDA
2424
public import Cslib.Computability.Automata.NA.Total
2525
public import Cslib.Computability.Distributed.FLP.Algorithm
26+
public import Cslib.Computability.Distributed.FLP.CanReachVia
2627
public import Cslib.Computability.Distributed.FLP.Consensus
28+
public import Cslib.Computability.Distributed.FLP.FairScheduler
2729
public import Cslib.Computability.Languages.Congruences.BuchiCongruence
2830
public import Cslib.Computability.Languages.Congruences.RightCongruence
2931
public import Cslib.Computability.Languages.ExampleEventuallyZero

‎Cslib/Computability/Distributed/FLP/CanReachVia.lean‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
/-
2+
Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ching-Tsun Chou
5+
-/
6+
7+
module
8+
9+
public import Cslib.Computability.Distributed.FLP.Algorithm
10+
11+
/-! # Reachability via a subset of processes
12+
-/
13+
14+
@[expose] public section
15+
16+
namespace Cslib.FLP
17+
18+
open Function Set Sum Multiset
19+
20+
variable {P M S : Type*} [DecidableEq P] [DecidableEq M]
21+
22+
/-- `a.CanReachVia ps s1 s2` means that state `s2` is reachable from state `s1` via a finite
23+
execution of algorithm `a` in which all messages received have destinations in `ps`. -/
24+
def Algorithm.CanReachVia (a : Algorithm P M S) (ps : Set P) (s1 s2 : State P M S) : Prop :=
25+
∃ xs, a.lts.MTr s1 xs s2 ∧ xs.Forall (DestIn ps)
26+
27+
/-- `InpEqOn ps inp1 inp2` means that inputs `inp1` and `inp2` agree on all processes in `ps`. -/
28+
def InpEqOn (ps : Set P) (inp1 inp2 : P → Bool) : Prop :=
29+
∀ p, p ∈ ps → inp1 p = inp2 p
30+
31+
namespace CanReachVia
32+
33+
variable {a : Algorithm P M S}
34+
35+
/-- `a.CanReachVia ps s s'` implies `a.lts.CanReach s s'` for any `ps`. -/
36+
theorem canReach {ps : Set P} {s s' : State P M S}
37+
(h : a.CanReachVia ps s s') : a.lts.CanReach s s' := by
38+
obtain ⟨xs, h_mtr, _⟩ := h
39+
use xs
40+
41+
/-- `a.CanReachVia ps s s` is true for any `ps`. -/
42+
theorem refl (ps : Set P) (s : State P M S) :
43+
a.CanReachVia ps s s := by
44+
use []
45+
simp [LTS.MTr.refl]
46+
47+
/-- Extending `CanReachVia` on the left by one step. -/
48+
theorem stepL {ps : Set P} {x : Action P M} {s1 s2 s3 : State P M S}
49+
(hx : DestIn ps x) (h1 : a.lts.Tr s1 x s2) (h2 : a.CanReachVia ps s2 s3) :
50+
a.CanReachVia ps s1 s3 := by
51+
obtain ⟨xs, _, _⟩ := h2
52+
use (x :: xs)
53+
grind [LTS.MTr.stepL, List.forall_cons]
54+
55+
private lemma diamond_helper
56+
{ps : Set P} {x : Action P M} {s s1 s2 : State P M S}
57+
(hx : DestIn ps x) (h1 : a.lts.Tr s x s1) (h2 : a.CanReachVia psᶜ s s2) :
58+
∃ s', a.CanReachVia psᶜ s1 s' ∧ a.lts.Tr s2 x s' := by
59+
obtain ⟨xs2, h_mtr2, h_via2⟩ := h2
60+
induction h_mtr2 generalizing s1
61+
case refl s =>
62+
use s1
63+
simp_all [refl]
64+
case stepL s y t2 ys s2 h_tr2 h_mtr2 h_ind =>
65+
obtain ⟨h_y, h_ys⟩ := (List.forall_cons (DestIn psᶜ) y ys).mp h_via2
66+
obtain ⟨t1, h_tr1, h_tr21⟩ := Algorithm.tr_diamond hx h1 h_y h_tr2
67+
obtain ⟨s', h_crv1, h_tr2'⟩ := h_ind h_tr21 h_ys
68+
use s', ?_, h_tr2'
69+
exact stepL h_y h_tr1 h_crv1
70+
71+
/-- A diamond property for `CanReachVia`. This theorem formalizes Proposition 1 of [Volzer2004]. -/
72+
theorem diamond {ps : Set P} {s s1 s2 : State P M S}
73+
(h1 : a.CanReachVia ps s s1) (h2 : a.CanReachVia psᶜ s s2) :
74+
∃ s', a.CanReachVia psᶜ s1 s' ∧ a.CanReachVia ps s2 s' := by
75+
obtain ⟨xs1, h_mtr1, h_via1⟩ := h1
76+
induction h_mtr1 generalizing s2
77+
case refl s =>
78+
use s2
79+
simp_all [refl]
80+
case stepL s x t1 xs s1 h_tr1 h_mtr1 h_ind =>
81+
obtain ⟨h_x, h_xs⟩ := (List.forall_cons (DestIn ps) x xs).mp h_via1
82+
obtain ⟨t2, h_crv, h_tr2⟩:= diamond_helper h_x h_tr1 h2
83+
obtain ⟨s', h_crv1, h_crv2⟩ := h_ind h_crv h_xs
84+
use s', h_crv1
85+
exact stepL h_x h_tr2 h_crv2
86+
87+
/-- If inputs `inp1` and `inp2` agree on all processes in `ps` and state `s` is reachable from
88+
the initial state determined by `inp1` by receiving messages with destinations in `ps` only,
89+
then there exists a state `s2` that agrees with `s` on the states of all processes and is
90+
reachable from the initial state determined by `inp2` by receiving messages with destinations
91+
in `ps` only. This theorem is implicitly used in the proof of Lemma 1 of [Volzer2004]. -/
92+
theorem subset_inp [Fintype P] {ps : Set P} {inp1 inp2 : P → Bool} {s1 : State P M S}
93+
(he : InpEqOn ps inp1 inp2) (hr : a.CanReachVia ps (a.start inp1) s1) :
94+
∃ s2, a.CanReachVia ps (a.start inp2) s2 ∧ s2.proc = s1.proc := by
95+
obtain ⟨xs, h_mtr, h_xs⟩ := hr
96+
obtain ⟨ss, _, h_ss0, _, _⟩ := LTS.Execution.of_mTr h_mtr
97+
suffices h_inv : ∀ k, (_ : k ≤ xs.length) →
98+
∃ s2, a.lts.MTr (a.start inp2) (xs.take k) s2 ∧ s2.proc = ss[k].proc ∧
99+
∀ m, m.dest ∈ ps → s2.msgs.count m = ss[k].msgs.count m by
100+
obtain ⟨s2, _⟩ := h_inv xs.length (by simp)
101+
use s2, ?_, by grind
102+
use xs, by grind
103+
intro k h_k
104+
induction k
105+
case zero =>
106+
use a.start inp2, by grind [LTS.MTr], by grind [Algorithm.start]
107+
intro m h_m
108+
simp only [h_ss0, Algorithm.start, count_map, Message.ext_iff]
109+
congr
110+
grind [InpEqOn]
111+
case succ k h_ind =>
112+
obtain ⟨s2, h_mtr, h_proc, h_msgs⟩ := h_ind (by grind)
113+
obtain (_ | ⟨m, h_m⟩) := Option.eq_none_or_eq_some xs[k]
114+
· use s2, ?_, ?_, ?_
115+
· have h_tr : a.lts.Tr s2 xs[k] s2 := by grind [Algorithm.lts]
116+
grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr]
117+
· grind [Algorithm.tr_none]
118+
· grind [Algorithm.tr_none]
119+
· obtain ⟨_, h_k1⟩ : m ∈ ss[k].msgs ∧ ss[k + 1] = a.recvMsg m ss[k] := by grind [Algorithm.lts]
120+
use a.recvMsg m s2, ?_, ?_, ?_
121+
· have := List.forall_mem_iff_forall_getElem.mp <| List.forall_iff_forall_mem.mp h_xs
122+
have h_tr : a.lts.Tr s2 xs[k] (a.recvMsg m s2) := by
123+
grind [Algorithm.lts, DestIn, one_le_count_iff_mem]
124+
grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr]
125+
· grind [Algorithm.recvMsg]
126+
· intro m1 h_m1
127+
by_cases h1 : m1 = m
128+
· simp [h_k1, Algorithm.recvMsg, h_proc, h1, count_erase_self]
129+
grind
130+
· simp [h_k1, Algorithm.recvMsg, h_proc, count_erase_of_ne h1]
131+
grind
132+
133+
end CanReachVia
134+
135+
end Cslib.FLP

‎Cslib/Computability/Distributed/FLP/FairScheduler.lean‎

Lines changed: 250 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,250 @@
1+
/-
2+
Copyright (c) 2026 Ching-Tsun Chou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ching-Tsun Chou
5+
-/
6+
7+
module
8+
9+
public import Cslib.Computability.Distributed.FLP.Consensus
10+
public import Cslib.Foundations.Data.OmegaSequence.InfOcc
11+
public import Mathlib.Data.List.ReduceOption
12+
13+
/-! # Machinery for constructing infinite fair executions
14+
15+
The main goal of this file is to define a `fairScheduler` that, given a function `d`
16+
of type `DeliverMsg`, a state predicate `q`, and a state `s0` of an algorithm `a`,
17+
constructs an infinite execution of `a` starting from state `s0` in which all processes
18+
from a set `ps` are fair and `q` is true infinitely often. With additional assumptions,
19+
we may also want to require that all actions in the infinite execution satisfy an action
20+
predicate `r`.
21+
-/
22+
23+
@[expose] public section
24+
25+
namespace Cslib.FLP
26+
27+
open Function Set Multiset Filter ωSequence
28+
29+
variable {P M S : Type*} [DecidableEq P] [DecidableEq M]
30+
31+
/-- Given a state `s` and a message `m`, a function `d` of type `DeliverMsg` is supposed to
32+
return `(xs, t)` where `xs` is a finite execution from `s` to `t` in which `m` is delivered. -/
33+
def DeliverMsg P M S := State P M S → Message P M → List (Action P M) × State P M S
34+
35+
/-- `d.ForallActions r` requires that all actions returned by `d` satisfy `r`. -/
36+
def DeliverMsg.ForallActions (d : DeliverMsg P M S) (r : Action P M → Prop) : Prop :=
37+
∀ s m, (d s m).fst.Forall r
38+
39+
/-- `d.foldList s ml ms` uses `d` to deliver all messages that are in `ml` but not in `ms` from
40+
state `s`. Note that if a message `m` in `ml` is delivered during the delivery of an earlier
41+
message, `m` is added to `ms` so that it is not processed again. -/
42+
def DeliverMsg.foldList (d : DeliverMsg P M S) (s : State P M S) :
43+
List (Message P M) → Finset (Message P M) → List (Action P M) × State P M S
44+
| [], _ => ([], s)
45+
| m :: ml, ms =>
46+
if m ∈ ms then
47+
d.foldList s ml ms
48+
else
49+
let (xl1, s1) := d s m
50+
let ms' := ms ∪ xl1.reduceOption.toFinset
51+
let (xl2, s2) := d.foldList s1 ml ms'
52+
(xl1 ++ xl2, s2)
53+
54+
open scoped Classical in
55+
/-- `d.scheduleMsgs ps s` schedules and delivers all messages which are in-flight in state `s`
56+
and have destinations in `ps` in some order (as determined by choice). If no such message exists,
57+
then the the stuttering step is taken. -/
58+
noncomputable def DeliverMsg.scheduleMsgs (d : DeliverMsg P M S) (ps : Set P)
59+
(s : State P M S) : List (Action P M) × State P M S :=
60+
let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps)
61+
if ms = 0 then
62+
([none], s)
63+
else
64+
d.foldList s ms.toList ∅
65+
66+
namespace DeliverMsg
67+
68+
variable {d : DeliverMsg P M S}
69+
70+
/-- If `d.ForallActions r`, then `d.foldList s ml ms` can only use actions satisfying `r`. -/
71+
theorem foldList_forallActions {r : Action P M → Prop}
72+
(s : State P M S) (ml : List (Message P M)) (ms : Finset (Message P M))
73+
(h : d.ForallActions r) : (d.foldList s ml ms).fst.Forall r := by
74+
induction ml generalizing s ms <;>
75+
grind [DeliverMsg.foldList, DeliverMsg.ForallActions, List.Forall, List.forall_append]
76+
77+
end DeliverMsg
78+
79+
/-- Starting from state `s0`, `a.fairSchedular d ps s0` constructs an infinite sequence of
80+
finite executions of `a` by repeatedly applying `d.scheduleMsgs ps`. -/
81+
noncomputable def Algorithm.fairScheduler (a : Algorithm P M S) (d : DeliverMsg P M S) (ps : Set P)
82+
(s0 : State P M S) : ℕ → List (Action P M) × State P M S
83+
| 0 => ([], s0)
84+
| k + 1 => d.scheduleMsgs ps (a.fairScheduler d ps s0 k).snd
85+
86+
/-- The infinite sequence of states forming the end states of the finite executions constructed
87+
by `Algorithm.fairScheduler`. -/
88+
noncomputable def Algorithm.fairSegEnds (a : Algorithm P M S) (d : DeliverMsg P M S)
89+
(ps : Set P) (s0 : State P M S) : ωSequence (State P M S) :=
90+
ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).snd)
91+
92+
/-- The infinite sequence of finite action sequences from the finite executions constructed
93+
by `Algorithm.fairScheduler`. -/
94+
noncomputable def Algorithm.fairSegActions (a : Algorithm P M S) (d : DeliverMsg P M S)
95+
(ps : Set P) (s0 : State P M S) : ωSequence (List (Action P M)) :=
96+
(ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).fst)).tail
97+
98+
/-- `a.FairDeliverMsg d ps q` says that for any state `s` of `a` satisfying `q` and
99+
any message `m` which is in-flight in `s` and whose destination is in `ps`, `d s m`
100+
produces a legal finite execution of `a` in which `m` is delivered and which ends in
101+
a state satisfying `q` again. -/
102+
def Algorithm.FairDeliverMsg (a : Algorithm P M S) (d : DeliverMsg P M S)
103+
(ps : Set P) (q : State P M S → Prop) : Prop :=
104+
∀ s m, m ∈ s.msgs ∧ m.dest ∈ ps ∧ q s →
105+
let (xl, t) := d s m
106+
a.lts.MTr s xl t ∧ some m ∈ xl ∧ q t
107+
108+
namespace FairScheduler
109+
110+
variable {a : Algorithm P M S}
111+
112+
/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of
113+
`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/
114+
theorem fairScheduler_init {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) :
115+
a.fairSegEnds d ps s0 0 = s0 := by
116+
grind [Algorithm.fairScheduler, Algorithm.fairSegEnds]
117+
118+
/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of
119+
`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/
120+
theorem fairScheduler_step {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) (k : ℕ) :
121+
d.scheduleMsgs ps (a.fairSegEnds d ps s0 k) =
122+
(a.fairSegActions d ps s0 k, a.fairSegEnds d ps s0 (k + 1)) := by
123+
grind [Algorithm.fairScheduler, Algorithm.fairSegEnds, Algorithm.fairSegActions]
124+
125+
/-- If `d.ForallActions r`, then `a.fairSegActions d ps s0` can only use actions satisfying `r`. -/
126+
theorem fairSeg_forallActions {d : DeliverMsg P M S} {r : Action P M → Prop}
127+
(ps : Set P) (s0 : State P M S) (k : ℕ) (ha : d.ForallActions r) (hn : r none) :
128+
(a.fairSegActions d ps s0 k).Forall r := by
129+
grind [fairScheduler_step (a := a) (d := d) ps s0 k,
130+
DeliverMsg.scheduleMsgs, DeliverMsg.foldList_forallActions, List.Forall]
131+
132+
/-- The correctness of `d.foldList s ml ms` under the assumption `a.FairDeliverMsg d ps q`. -/
133+
theorem fairDeliverMsg_foldList {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
134+
(hd : a.FairDeliverMsg d ps q) (s : State P M S)
135+
(ml : List (Message P M)) (ms : Finset (Message P M))
136+
(hs : q s ∧ ∀ m, m ∈ ml → ¬ m ∈ ms → m ∈ s.msgs ∧ m.dest ∈ ps) :
137+
let (xl, t) := d.foldList s ml ms
138+
a.lts.MTr s xl t ∧ q t ∧ ∀ m, m ∈ ml → ¬ m ∈ ms → some m ∈ xl := by
139+
induction ml generalizing s ms
140+
case nil => grind [DeliverMsg.foldList, LTS.MTr]
141+
case cons m ml h_ind =>
142+
by_cases h_m : m ∈ ms
143+
· grind [DeliverMsg.foldList]
144+
· let xl1 := (d s m).fst
145+
let s1 := (d s m).snd
146+
let ms' := ms ∪ xl1.reduceOption.toFinset
147+
have (m' : Message P M) : m' ∈ xl1.reduceOption.toFinset ↔ some m' ∈ xl1 := by
148+
simp [List.mem_toFinset, List.reduceOption_mem_iff]
149+
have (m' : Message P M) : m' ∈ ml → ¬ m' ∈ ms' → m' ∈ s1.msgs := by
150+
grind [Algorithm.FairDeliverMsg, Algorithm.mTr_notRcvd_enabled]
151+
grind [DeliverMsg.foldList, Algorithm.FairDeliverMsg, LTS.MTr.comp]
152+
153+
/-- The correctness of `d.scheduleMsgs ps s` under the assumption `a.FairDeliverMsg d ps q`. -/
154+
theorem fairDeliverMsg_scheduleMsgs {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
155+
(hd : a.FairDeliverMsg d ps q) (s : State P M S) (hs : q s) :
156+
let xl := (d.scheduleMsgs ps s).fst
157+
let t := (d.scheduleMsgs ps s).snd
158+
q t ∧ a.lts.MTr s xl t ∧ xl.length > 0 ∧ ∀ m, m ∈ s.msgs → m.dest ∈ ps → some m ∈ xl := by
159+
classical
160+
intro xl t
161+
let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps)
162+
by_cases h_ms : ms = 0
163+
· have h1 : xl = [none] ∧ t = s := by grind [DeliverMsg.scheduleMsgs]
164+
simp [ms, eq_zero_iff_forall_notMem] at h_ms
165+
split_ands <;> try grind
166+
simp only [h1]
167+
apply LTS.MTr.single
168+
grind [Algorithm.lts]
169+
· have : q t ∧ a.lts.MTr s xl t ∧ ∀ m, m ∈ ms.toList → some m ∈ xl := by
170+
grind [DeliverMsg.scheduleMsgs, fairDeliverMsg_foldList hd s ms.toList ∅ (by simp [ms, hs])]
171+
split_ands <;> try grind [mem_toList, mem_filter]
172+
obtain ⟨m, h_ms⟩ := exists_mem_of_ne_zero h_ms
173+
suffices some m ∈ xl by grind
174+
grind [mem_toList]
175+
176+
/-- The correctness of `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0`
177+
under the assumption `a.FairDeliverMsg d ps q`. -/
178+
theorem fair_fairSegs {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
179+
(hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) :
180+
let ts := a.fairSegEnds d ps s0
181+
let xls := a.fairSegActions d ps s0
182+
∀ k, q (ts k) ∧ a.lts.MTr (ts k) (xls k) (ts (k + 1)) ∧ (xls k).length > 0 ∧
183+
∀ m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k := by
184+
classical
185+
intro ts xls k
186+
induction k <;> grind [fairScheduler_init, fairScheduler_step, fairDeliverMsg_scheduleMsgs]
187+
188+
/-- Given an infinite sequence of non-empty finite executions of algorithm `a`,
189+
if all messages with destinations in `ps` that are in-flight at the beginning of each
190+
finite execution are delivered in that finite execution, then those finite executions can
191+
be concatenated into an infinite execution of `a` in which every process in `ps` is fair. -/
192+
theorem flatten_fairSegs {ps : Set P}
193+
{ts : ωSequence (State P M S)} {xls : ωSequence (List (Action P M))}
194+
(hmtr : ∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1)))
195+
(hpos : ∀ k, (xls k).length > 0)
196+
(hsch : ∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) :
197+
∃ ss, a.lts.OmegaExecution ss xls.flatten ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧
198+
∀ p, p ∈ ps → ProcFair p ss xls.flatten := by
199+
obtain ⟨ss, h_omega, h_ts⟩ := LTS.OmegaExecution.flatten_mTr hmtr hpos
200+
use ss, h_omega, h_ts
201+
rintro p h_m m ⟨rfl⟩
202+
by_contra! ⟨k, h_k, h_k'⟩
203+
have h_xls : ∃ᶠ n in atTop, n ∈ xls.cumLen '' univ := by
204+
apply frequently_iff_strictMono.mpr
205+
use xls.cumLen
206+
grind [cumLen_strictMono]
207+
obtain ⟨j, _, h_j⟩ : ∃ j, k ≤ xls.cumLen j ∧ m ∈ (ts j).msgs := by
208+
obtain ⟨n, _, j, _, _⟩ := frequently_atTop.mp h_xls k
209+
grind [Algorithm.omega_notRcvd_enabled h_omega h_k h_k']
210+
obtain ⟨i, _, _⟩ := List.getElem_of_mem <| hsch j m h_j h_m
211+
grind [extract_flatten hpos j]
212+
213+
/-- Under the assumption `a.FairDeliverMsg d ps q`, the infinite sequence of finite executions
214+
of `a` represented by `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0` can be concatenated
215+
into an infinite execution of `a` in which every process in `ps` is fair and `q` is true at
216+
the ends of all those finite executions. -/
217+
theorem fair_omegaExecution {d : DeliverMsg P M S} {ps : Set P} {q : State P M S → Prop}
218+
(hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0) :
219+
let ts := a.fairSegEnds d ps s0
220+
let xls := a.fairSegActions d ps s0
221+
∃ ss, a.lts.OmegaExecution ss xls.flatten ∧
222+
ss 0 = s0 ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧
223+
(∀ k, q (ss (xls.cumLen k))) ∧ (∀ k, (xls k).length > 0) ∧
224+
∀ p, p ∈ ps → ProcFair p ss xls.flatten := by
225+
intro ts xls
226+
obtain ⟨h_q, hmtr, hpos, hsch⟩ :
227+
(∀ k, q (ts k)) ∧
228+
(∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1))) ∧
229+
(∀ k, (xls k).length > 0) ∧
230+
(∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) := by
231+
grind [fair_fairSegs hd s0 hs0]
232+
obtain ⟨ss, _, _, _⟩ := flatten_fairSegs hmtr hpos hsch
233+
have : ss 0 = s0 := by grind [fairScheduler_init]
234+
use ss
235+
grind
236+
237+
/-- If `d.ForallActions r`, then the concatenation of all `a.fairSegActions d ps s0` segments
238+
can only use actions satisfying `r`. -/
239+
theorem omega_forall_actions {d : DeliverMsg P M S} {ps : Set P}
240+
{q : State P M S → Prop} {r : Action P M → Prop}
241+
(hd : a.FairDeliverMsg d ps q) (s0 : State P M S) (hs0 : q s0)
242+
(ha : d.ForallActions r) (hn : r none) :
243+
∀ k, r ((a.fairSegActions d ps s0).flatten k) := by
244+
have hpos : ∀ k, (a.fairSegActions d ps s0 k).length > 0 := by grind [fair_fairSegs hd s0 hs0]
245+
simp only [forall_flatten_iff hpos]
246+
grind [fairSeg_forallActions]
247+
248+
end FairScheduler
249+
250+
end Cslib.FLP

0 commit comments

Comments
 (0)