From e7076ee8c5532df2cf659633d899e60059633e41 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Mon, 1 Jun 2026 10:52:11 -0700 Subject: [PATCH 1/2] feat(FLP): some technical machineries for reasoning about diamond and fairness properties --- Cslib.lean | 2 + .../Distributed/FLP/CanReachVia.lean | 135 ++++++++++ .../Distributed/FLP/FairScheduler.lean | 250 ++++++++++++++++++ Cslib/Computability/Distributed/FLP/README.md | 4 +- 4 files changed, 389 insertions(+), 2 deletions(-) create mode 100644 Cslib/Computability/Distributed/FLP/CanReachVia.lean create mode 100644 Cslib/Computability/Distributed/FLP/FairScheduler.lean diff --git a/Cslib.lean b/Cslib.lean index c0269e0bb..18793d1a3 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -23,7 +23,9 @@ public import Cslib.Computability.Automata.NA.Sum public import Cslib.Computability.Automata.NA.ToDA public import Cslib.Computability.Automata.NA.Total public import Cslib.Computability.Distributed.FLP.Algorithm +public import Cslib.Computability.Distributed.FLP.CanReachVia public import Cslib.Computability.Distributed.FLP.Consensus +public import Cslib.Computability.Distributed.FLP.FairScheduler public import Cslib.Computability.Languages.Congruences.BuchiCongruence public import Cslib.Computability.Languages.Congruences.RightCongruence public import Cslib.Computability.Languages.ExampleEventuallyZero diff --git a/Cslib/Computability/Distributed/FLP/CanReachVia.lean b/Cslib/Computability/Distributed/FLP/CanReachVia.lean new file mode 100644 index 000000000..826cb58b8 --- /dev/null +++ b/Cslib/Computability/Distributed/FLP/CanReachVia.lean @@ -0,0 +1,135 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Computability.Distributed.FLP.Algorithm + +/-! # Reachability via a subset of processes +-/ + +@[expose] public section + +namespace Cslib.FLP + +open Function Set Sum Multiset + +variable {P M S : Type*} [DecidableEq P] [DecidableEq M] + +/-- `a.CanReachVia ps s1 s2` means that state `s2` is reachable from state `s1` via a finite +execution of algorithm `a` in which all messages received have destinations in `ps`. -/ +def Algorithm.CanReachVia (a : Algorithm P M S) (ps : Set P) (s1 s2 : State P M S) : Prop := + ∃ xs, a.lts.MTr s1 xs s2 ∧ xs.Forall (DestIn ps) + +/-- `InpEqOn ps inp1 inp2` means that inputs `inp1` and `inp2` agree on all processes in `ps`. -/ +def InpEqOn (ps : Set P) (inp1 inp2 : P → Bool) : Prop := + ∀ p, p ∈ ps → inp1 p = inp2 p + +namespace CanReachVia + +variable {a : Algorithm P M S} + +/-- `a.CanReachVia ps s s'` implies `a.lts.CanReach s s'` for any `ps`. -/ +theorem canReach {ps : Set P} {s s' : State P M S} + (h : a.CanReachVia ps s s') : a.lts.CanReach s s' := by + obtain ⟨xs, h_mtr, _⟩ := h + use xs + +/-- `a.CanReachVia ps s s` is true for any `ps`. -/ +theorem refl (ps : Set P) (s : State P M S) : + a.CanReachVia ps s s := by + use [] + simp [LTS.MTr.refl] + +/-- Extending `CanReachVia` on the left by one step. -/ +theorem stepL {ps : Set P} {x : Action P M} {s1 s2 s3 : State P M S} + (hx : DestIn ps x) (h1 : a.lts.Tr s1 x s2) (h2 : a.CanReachVia ps s2 s3) : + a.CanReachVia ps s1 s3 := by + obtain ⟨xs, _, _⟩ := h2 + use (x :: xs) + grind [LTS.MTr.stepL, List.forall_cons] + +private lemma diamond_helper + {ps : Set P} {x : Action P M} {s s1 s2 : State P M S} + (hx : DestIn ps x) (h1 : a.lts.Tr s x s1) (h2 : a.CanReachVia psᶜ s s2) : + ∃ s', a.CanReachVia psᶜ s1 s' ∧ a.lts.Tr s2 x s' := by + obtain ⟨xs2, h_mtr2, h_via2⟩ := h2 + induction h_mtr2 generalizing s1 + case refl s => + use s1 + simp_all [refl] + case stepL s y t2 ys s2 h_tr2 h_mtr2 h_ind => + obtain ⟨h_y, h_ys⟩ := (List.forall_cons (DestIn psᶜ) y ys).mp h_via2 + obtain ⟨t1, h_tr1, h_tr21⟩ := Algorithm.tr_diamond hx h1 h_y h_tr2 + obtain ⟨s', h_crv1, h_tr2'⟩ := h_ind h_tr21 h_ys + use s', ?_, h_tr2' + exact stepL h_y h_tr1 h_crv1 + +/-- A diamond property for `CanReachVia`. This theorem formalizes Proposition 1 of [Volzer2004]. -/ +theorem diamond {ps : Set P} {s s1 s2 : State P M S} + (h1 : a.CanReachVia ps s s1) (h2 : a.CanReachVia psᶜ s s2) : + ∃ s', a.CanReachVia psᶜ s1 s' ∧ a.CanReachVia ps s2 s' := by + obtain ⟨xs1, h_mtr1, h_via1⟩ := h1 + induction h_mtr1 generalizing s2 + case refl s => + use s2 + simp_all [refl] + case stepL s x t1 xs s1 h_tr1 h_mtr1 h_ind => + obtain ⟨h_x, h_xs⟩ := (List.forall_cons (DestIn ps) x xs).mp h_via1 + obtain ⟨t2, h_crv, h_tr2⟩:= diamond_helper h_x h_tr1 h2 + obtain ⟨s', h_crv1, h_crv2⟩ := h_ind h_crv h_xs + use s', h_crv1 + exact stepL h_x h_tr2 h_crv2 + +/-- If inputs `inp1` and `inp2` agree on all processes in `ps` and state `s` is reachable from +the initial state determined by `inp1` by receiving messages with destinations in `ps` only, +then there exists a state `s2` that agrees with `s` on the states of all processes and is +reachable from the initial state determined by `inp2` by receiving messages with destinations +in `ps` only. This theorem is implicitly used in the proof of Lemma 1 of [Volzer2004]. -/ +theorem subset_inp [Fintype P] {ps : Set P} {inp1 inp2 : P → Bool} {s1 : State P M S} + (he : InpEqOn ps inp1 inp2) (hr : a.CanReachVia ps (a.start inp1) s1) : + ∃ s2, a.CanReachVia ps (a.start inp2) s2 ∧ s2.proc = s1.proc := by + obtain ⟨xs, h_mtr, h_xs⟩ := hr + obtain ⟨ss, _, h_ss0, _, _⟩ := LTS.Execution.of_mTr h_mtr + suffices h_inv : ∀ k, (_ : k ≤ xs.length) → + ∃ s2, a.lts.MTr (a.start inp2) (xs.take k) s2 ∧ s2.proc = ss[k].proc ∧ + ∀ m, m.dest ∈ ps → s2.msgs.count m = ss[k].msgs.count m by + obtain ⟨s2, _⟩ := h_inv xs.length (by simp) + use s2, ?_, by grind + use xs, by grind + intro k h_k + induction k + case zero => + use a.start inp2, by grind [LTS.MTr], by grind [Algorithm.start] + intro m h_m + simp only [h_ss0, Algorithm.start, count_map, Message.ext_iff] + congr + grind [InpEqOn] + case succ k h_ind => + obtain ⟨s2, h_mtr, h_proc, h_msgs⟩ := h_ind (by grind) + obtain (_ | ⟨m, h_m⟩) := Option.eq_none_or_eq_some xs[k] + · use s2, ?_, ?_, ?_ + · have h_tr : a.lts.Tr s2 xs[k] s2 := by grind [Algorithm.lts] + grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr] + · grind [Algorithm.tr_none] + · grind [Algorithm.tr_none] + · obtain ⟨_, h_k1⟩ : m ∈ ss[k].msgs ∧ ss[k + 1] = a.recvMsg m ss[k] := by grind [Algorithm.lts] + use a.recvMsg m s2, ?_, ?_, ?_ + · have := List.forall_mem_iff_forall_getElem.mp <| List.forall_iff_forall_mem.mp h_xs + have h_tr : a.lts.Tr s2 xs[k] (a.recvMsg m s2) := by + grind [Algorithm.lts, DestIn, one_le_count_iff_mem] + grind [List.take_add_one, LTS.MTr.stepR (lts := a.lts) h_mtr h_tr] + · grind [Algorithm.recvMsg] + · intro m1 h_m1 + by_cases h1 : m1 = m + · simp [h_k1, Algorithm.recvMsg, h_proc, h1, count_erase_self] + grind + · simp [h_k1, Algorithm.recvMsg, h_proc, count_erase_of_ne h1] + grind + +end CanReachVia + +end Cslib.FLP diff --git a/Cslib/Computability/Distributed/FLP/FairScheduler.lean b/Cslib/Computability/Distributed/FLP/FairScheduler.lean new file mode 100644 index 000000000..075e87ba7 --- /dev/null +++ b/Cslib/Computability/Distributed/FLP/FairScheduler.lean @@ -0,0 +1,250 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Computability.Distributed.FLP.Consensus +public import Cslib.Foundations.Data.OmegaSequence.InfOcc +public import Mathlib.Data.List.ReduceOption + +/-! # 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`. +-/ + +@[expose] public section + +namespace Cslib.FLP + +open Function Set Multiset Filter ωSequence + +variable {P M S : Type*} [DecidableEq P] [DecidableEq M] + +/-- 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. -/ +def DeliverMsg P M S := State P M S → Message P M → List (Action P M) × State P M S + +/-- `d.ForallActions r` requires that all actions returned by `d` satisfy `r`. -/ +def DeliverMsg.ForallActions (d : DeliverMsg P M S) (r : Action P M → Prop) : Prop := + ∀ s m, (d s m).fst.Forall r + +/-- `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. -/ +def DeliverMsg.foldList (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 + | [], _ => ([], s) + | m :: ml, ms => + if m ∈ ms then + d.foldList s ml ms + else + let (xl1, s1) := d s m + let ms' := ms ∪ xl1.reduceOption.toFinset + let (xl2, s2) := d.foldList s1 ml ms' + (xl1 ++ xl2, s2) + +open scoped Classical in +/-- `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. -/ +noncomputable def DeliverMsg.scheduleMsgs (d : DeliverMsg P M S) (ps : Set P) + (s : State P M S) : List (Action P M) × State P M S := + let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps) + if ms = 0 then + ([none], s) + else + d.foldList s ms.toList ∅ + +namespace DeliverMsg + +variable {d : DeliverMsg P M S} + +/-- If `d.ForallActions r`, then `d.foldList s ml ms` can only use actions satisfying `r`. -/ +theorem foldList_forallActions {r : Action P M → Prop} + (s : State P M S) (ml : List (Message P M)) (ms : Finset (Message P M)) + (h : d.ForallActions r) : (d.foldList s ml ms).fst.Forall r := by + induction ml generalizing s ms <;> + grind [DeliverMsg.foldList, DeliverMsg.ForallActions, List.Forall, List.forall_append] + +end DeliverMsg + +/-- Starting from state `s0`, `a.fairSchedular d ps s0` constructs an infinite sequence of +finite executions of `a` by repeatedly applying `d.scheduleMsgs ps`. -/ +noncomputable def Algorithm.fairScheduler (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 + | 0 => ([], s0) + | k + 1 => d.scheduleMsgs ps (a.fairScheduler d ps s0 k).snd + +/-- The infinite sequence of states forming the end states of the finite executions constructed +by `Algorithm.fairScheduler`. -/ +noncomputable def Algorithm.fairSegEnds (a : Algorithm P M S) (d : DeliverMsg P M S) + (ps : Set P) (s0 : State P M S) : ωSequence (State P M S) := + ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).snd) + +/-- The infinite sequence of finite action sequences from the finite executions constructed +by `Algorithm.fairScheduler`. -/ +noncomputable def Algorithm.fairSegActions (a : Algorithm P M S) (d : DeliverMsg P M S) + (ps : Set P) (s0 : State P M S) : ωSequence (List (Action P M)) := + (ωSequence.mk (fun k ↦ (a.fairScheduler d ps s0 k).fst)).tail + +/-- `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. -/ +def Algorithm.FairDeliverMsg (a : Algorithm P M S) (d : DeliverMsg P M S) + (ps : Set P) (q : State P M S → Prop) : Prop := + ∀ s m, m ∈ s.msgs ∧ m.dest ∈ ps ∧ q s → + let (xl, t) := d s m + a.lts.MTr s xl t ∧ some m ∈ xl ∧ q t + +namespace FairScheduler + +variable {a : Algorithm P M S} + +/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of +`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/ +theorem fairScheduler_init {d : DeliverMsg P M S} (ps : Set P) (s0 : State P M S) : + a.fairSegEnds d ps s0 0 = s0 := by + grind [Algorithm.fairScheduler, Algorithm.fairSegEnds] + +/-- Re-stating the definition of `Algorithm.fairScheduler` as a mutual recursion of +`Algorithm.fairSegEnds` and `Algorithm.fairSegActions`. -/ +theorem fairScheduler_step {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)) := by + grind [Algorithm.fairScheduler, Algorithm.fairSegEnds, Algorithm.fairSegActions] + +/-- If `d.ForallActions r`, then `a.fairSegActions d ps s0` can only use actions satisfying `r`. -/ +theorem fairSeg_forallActions {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) : + (a.fairSegActions d ps s0 k).Forall r := by + grind [fairScheduler_step (a := a) (d := d) ps s0 k, + DeliverMsg.scheduleMsgs, DeliverMsg.foldList_forallActions, List.Forall] + +/-- The correctness of `d.foldList s ml ms` under the assumption `a.FairDeliverMsg d ps q`. -/ +theorem fairDeliverMsg_foldList {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, m ∈ ml → ¬ m ∈ ms → m ∈ s.msgs ∧ m.dest ∈ ps) : + let (xl, t) := d.foldList s ml ms + a.lts.MTr s xl t ∧ q t ∧ ∀ m, m ∈ ml → ¬ m ∈ ms → some m ∈ xl := by + induction ml generalizing s ms + case nil => grind [DeliverMsg.foldList, LTS.MTr] + case cons m ml h_ind => + by_cases h_m : m ∈ ms + · grind [DeliverMsg.foldList] + · let xl1 := (d s m).fst + let s1 := (d s m).snd + let ms' := ms ∪ xl1.reduceOption.toFinset + have (m' : Message P M) : m' ∈ xl1.reduceOption.toFinset ↔ some m' ∈ xl1 := by + simp [List.mem_toFinset, List.reduceOption_mem_iff] + have (m' : Message P M) : m' ∈ ml → ¬ m' ∈ ms' → m' ∈ s1.msgs := by + grind [Algorithm.FairDeliverMsg, Algorithm.mTr_notRcvd_enabled] + grind [DeliverMsg.foldList, Algorithm.FairDeliverMsg, LTS.MTr.comp] + +/-- The correctness of `d.scheduleMsgs ps s` under the assumption `a.FairDeliverMsg d ps q`. -/ +theorem fairDeliverMsg_scheduleMsgs {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) : + let xl := (d.scheduleMsgs ps s).fst + let t := (d.scheduleMsgs ps s).snd + q t ∧ a.lts.MTr s xl t ∧ xl.length > 0 ∧ ∀ m, m ∈ s.msgs → m.dest ∈ ps → some m ∈ xl := by + classical + intro xl t + let ms := s.msgs.filter (fun m ↦ m.dest ∈ ps) + by_cases h_ms : ms = 0 + · have h1 : xl = [none] ∧ t = s := by grind [DeliverMsg.scheduleMsgs] + simp [ms, eq_zero_iff_forall_notMem] at h_ms + split_ands <;> try grind + simp only [h1] + apply LTS.MTr.single + grind [Algorithm.lts] + · have : q t ∧ a.lts.MTr s xl t ∧ ∀ m, m ∈ ms.toList → some m ∈ xl := by + grind [DeliverMsg.scheduleMsgs, fairDeliverMsg_foldList hd s ms.toList ∅ (by simp [ms, hs])] + split_ands <;> try grind [mem_toList, mem_filter] + obtain ⟨m, h_ms⟩ := exists_mem_of_ne_zero h_ms + suffices some m ∈ xl by grind + grind [mem_toList] + +/-- The correctness of `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0` +under the assumption `a.FairDeliverMsg d ps q`. -/ +theorem fair_fairSegs {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) : + let ts := a.fairSegEnds d ps s0 + let 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, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k := by + classical + intro ts xls k + induction k <;> grind [fairScheduler_init, fairScheduler_step, fairDeliverMsg_scheduleMsgs] + +/-- 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 flatten_fairSegs {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, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) : + ∃ ss, a.lts.OmegaExecution ss xls.flatten ∧ (∀ k, ss (xls.cumLen k) = ts k) ∧ + ∀ p, p ∈ ps → ProcFair p ss xls.flatten := by + obtain ⟨ss, h_omega, h_ts⟩ := LTS.OmegaExecution.flatten_mTr hmtr hpos + use ss, h_omega, h_ts + rintro p h_m m ⟨rfl⟩ + by_contra! ⟨k, h_k, h_k'⟩ + have h_xls : ∃ᶠ n in atTop, n ∈ xls.cumLen '' univ := by + apply frequently_iff_strictMono.mpr + use xls.cumLen + grind [cumLen_strictMono] + obtain ⟨j, _, h_j⟩ : ∃ j, k ≤ xls.cumLen j ∧ m ∈ (ts j).msgs := by + obtain ⟨n, _, j, _, _⟩ := frequently_atTop.mp h_xls k + grind [Algorithm.omega_notRcvd_enabled h_omega h_k h_k'] + obtain ⟨i, _, _⟩ := List.getElem_of_mem <| hsch j m h_j h_m + grind [extract_flatten hpos j] + +/-- 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 fair_omegaExecution {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) : + let ts := a.fairSegEnds d ps s0 + let xls := a.fairSegActions d ps s0 + ∃ ss, 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, p ∈ ps → ProcFair p ss xls.flatten := by + intro ts xls + obtain ⟨h_q, hmtr, hpos, hsch⟩ : + (∀ k, q (ts k)) ∧ + (∀ k, a.lts.MTr (ts k) (xls k) (ts (k + 1))) ∧ + (∀ k, (xls k).length > 0) ∧ + (∀ k m, m ∈ (ts k).msgs → m.dest ∈ ps → some m ∈ xls k) := by + grind [fair_fairSegs hd s0 hs0] + obtain ⟨ss, _, _, _⟩ := flatten_fairSegs hmtr hpos hsch + have : ss 0 = s0 := by grind [fairScheduler_init] + use ss + grind + +/-- If `d.ForallActions r`, then the concatenation of all `a.fairSegActions d ps s0` segments +can only use actions satisfying `r`. -/ +theorem omega_forall_actions {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) := by + have hpos : ∀ k, (a.fairSegActions d ps s0 k).length > 0 := by grind [fair_fairSegs hd s0 hs0] + simp only [forall_flatten_iff hpos] + grind [fairSeg_forallActions] + +end FairScheduler + +end Cslib.FLP diff --git a/Cslib/Computability/Distributed/FLP/README.md b/Cslib/Computability/Distributed/FLP/README.md index 7bc8e7bd3..6f3ccaa75 100644 --- a/Cslib/Computability/Distributed/FLP/README.md +++ b/Cslib/Computability/Distributed/FLP/README.md @@ -12,8 +12,6 @@ consensus is impossible in the presence of even a single crash fault. 2. `Consensus.lean` defines what it means for a distributed algorithm to solve the consensus problem in a fault-tolerant way and proves some basic properties. -*The following files will appear in future PRs:* - 3. `FairScheduler.lean` contains a technical machinery for constructing "fair executions", which is used in the proof of `PseudoConsensus.of_consensus` in `PseudoConsensus.lean` and in the proof of `OnePseudoConsensus.fair_nonUniform` in `Impossibility.lean`. @@ -21,6 +19,8 @@ consensus is impossible in the presence of even a single crash fault. 4. `CanReachVia.lean` defines the notion of reachability via a subset of processes and proves some of its properties. +*The following files will appear in future PRs:* + 5. `PseudoConsensus.lean` defines the notion of a fault-tolerant "pseudo-consensus" algorithm, which is central to Völzer's proof, and proves that every `f`-tolerant consensus algorithm is also a `f`-tolerant pseudo-consensus algorithm. From f22636fb2582bbbd51838129bcf9210729dfff5c Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Fri, 5 Jun 2026 08:53:16 -0700 Subject: [PATCH 2/2] Incorporate Shreyas Srinivas's comments --- .../Distributed/FLP/Algorithm.lean | 17 ++++++++++------- .../Distributed/FLP/CanReachVia.lean | 9 +++++++++ .../Distributed/FLP/FairScheduler.lean | 16 ++++++++-------- 3 files changed, 27 insertions(+), 15 deletions(-) diff --git a/Cslib/Computability/Distributed/FLP/Algorithm.lean b/Cslib/Computability/Distributed/FLP/Algorithm.lean index ccd90dbf6..8a858af0f 100644 --- a/Cslib/Computability/Distributed/FLP/Algorithm.lean +++ b/Cslib/Computability/Distributed/FLP/Algorithm.lean @@ -202,13 +202,16 @@ theorem tr_diamond {ps : Set P} {x1 x2 : Action P M} {s s1 s2 : State P M S} (hx1 : DestIn ps x1) (hs1 : a.lts.Tr s x1 s1) (hx2 : DestIn psᶜ x2) (hs2 : a.lts.Tr s x2 s2) : ∃ s', a.lts.Tr s1 x2 s' ∧ a.lts.Tr s2 x1 s' := by - cases x1 <;> cases x2 <;> try grind [Algorithm.lts] - case some m1 m2 => - have hd : m1.dest ≠ m2.dest := by grind [DestIn] - obtain ⟨h_m1, rfl⟩ := hs1 - obtain ⟨h_m2, rfl⟩ := hs2 - simp only [Algorithm.lts, exists_eq_right_right] - grind [recvMsg_comm (a := a) hd h_m1 h_m2] + cases x1 <;> cases x2 + · grind [Algorithm.lts] + · grind [Algorithm.lts] + · grind [Algorithm.lts] + · case some m1 m2 => + have hd : m1.dest ≠ m2.dest := by grind [DestIn] + obtain ⟨h_m1, rfl⟩ := hs1 + obtain ⟨h_m2, rfl⟩ := hs2 + simp only [Algorithm.lts, exists_eq_right_right] + grind [recvMsg_comm (a := a) hd h_m1 h_m2] /-- A message that is in-flight stays in-flight as long as it is not received (finite execution version). -/ diff --git a/Cslib/Computability/Distributed/FLP/CanReachVia.lean b/Cslib/Computability/Distributed/FLP/CanReachVia.lean index 826cb58b8..7b8f40e38 100644 --- a/Cslib/Computability/Distributed/FLP/CanReachVia.lean +++ b/Cslib/Computability/Distributed/FLP/CanReachVia.lean @@ -9,6 +9,15 @@ module public import Cslib.Computability.Distributed.FLP.Algorithm /-! # Reachability via a subset of processes + +This file develops a theory of reachability via a subset of processes, that is, what happens +when only a subset of processes can receive messages and take steps. It culminates with two +"diamond properties" of this more refined reachability relation. + +## References + +* [Volzer2004] H. Völzer, A constructive proof for FLP. + Information Processing Letters 92(2), (October 2004) 83–87. -/ @[expose] public section diff --git a/Cslib/Computability/Distributed/FLP/FairScheduler.lean b/Cslib/Computability/Distributed/FLP/FairScheduler.lean index 075e87ba7..9e9d622c5 100644 --- a/Cslib/Computability/Distributed/FLP/FairScheduler.lean +++ b/Cslib/Computability/Distributed/FLP/FairScheduler.lean @@ -162,16 +162,16 @@ theorem fairDeliverMsg_scheduleMsgs {d : DeliverMsg P M S} {ps : Set P} {q : Sta by_cases h_ms : ms = 0 · have h1 : xl = [none] ∧ t = s := by grind [DeliverMsg.scheduleMsgs] simp [ms, eq_zero_iff_forall_notMem] at h_ms - split_ands <;> try grind - simp only [h1] - apply LTS.MTr.single - grind [Algorithm.lts] + simp only [h1, hs, List.length_cons, List.length_nil, zero_add, Order.lt_one_iff, true_and] + split_ands + · apply LTS.MTr.single + grind [Algorithm.lts] + · grind · have : q t ∧ a.lts.MTr s xl t ∧ ∀ m, m ∈ ms.toList → some m ∈ xl := by grind [DeliverMsg.scheduleMsgs, fairDeliverMsg_foldList hd s ms.toList ∅ (by simp [ms, hs])] - split_ands <;> try grind [mem_toList, mem_filter] - obtain ⟨m, h_ms⟩ := exists_mem_of_ne_zero h_ms - suffices some m ∈ xl by grind - grind [mem_toList] + obtain ⟨m, _⟩ := exists_mem_of_ne_zero h_ms + have : some m ∈ xl := by grind [mem_toList] + split_ands <;> grind [mem_toList, mem_filter] /-- The correctness of `a.fairSegEnds d ps s0` and `a.fairSegActions d ps s0` under the assumption `a.FairDeliverMsg d ps q`. -/