|
| 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.Foundations.Semantics.LTS.OmegaExecution |
| 10 | + |
| 11 | +/-! # Distributed algorithms for solving the consensus problem |
| 12 | +
|
| 13 | +In the consensus problem, each process of a distributed algorithm is given a boolean value |
| 14 | +at the beginning. Then by exchanging messages asynchronously, they are supposed to agree on |
| 15 | +one of the initial boolean values. This file contains a very general definition of such |
| 16 | +a distributed algorithm. |
| 17 | +
|
| 18 | +Borrowing an idea from Leslie Lamport, we allow the LTS defined by such an algorithm to |
| 19 | +"stutter" at any time, in the sense of taking a dummy step without changing the |
| 20 | +global state of the distributed algorithm. This idea enables us to focus on infinite |
| 21 | +executions alone without loss of generality, because an algorithm that has run out of |
| 22 | +useful steps to take can always take the stuttering step. Pathological executions in which |
| 23 | +the stuttering step is taken forever when there is useful work to be done are outlawed by |
| 24 | +the fairness assumptions defined in `Consensus.lean`. |
| 25 | +
|
| 26 | +The types `P`, `M`, and `S` below are the types of processes (more precisely, process identifiers), |
| 27 | +messages contents, and process states. Eventually `P` will be assumed to be finite in the form of |
| 28 | +`[Fintype P]`, but that assumption will be added only where necessary. No assumption whatsoever |
| 29 | +will be made about `M` and `S`. In particular, they could be infinite. |
| 30 | +-/ |
| 31 | + |
| 32 | +@[expose] public section |
| 33 | + |
| 34 | +namespace Cslib.FLP |
| 35 | + |
| 36 | +open Set Sum Multiset |
| 37 | + |
| 38 | +variable {P M S : Type*} [DecidableEq P] [DecidableEq M] |
| 39 | + |
| 40 | +/-- The type of messages that processes send to each other. -/ |
| 41 | +@[ext] |
| 42 | +structure Message (P M : Type*) where |
| 43 | + /-- The destination of a message. -/ |
| 44 | + dest : P |
| 45 | + /-- The content of the message, where the `Bool` option is used to carry to the |
| 46 | + initial boolean value to each process. -/ |
| 47 | + msg : Bool ⊕ M |
| 48 | +deriving DecidableEq |
| 49 | + |
| 50 | +/-- The type of a process's local state. -/ |
| 51 | +structure ProcState (S : Type*) where |
| 52 | + /-- The internal state of a process. -/ |
| 53 | + state : S |
| 54 | + /-- The state component used by a process to signal the boolean value it decides on. -/ |
| 55 | + out : Option Bool |
| 56 | + |
| 57 | +/-- The global state of the distributed algorithm. -/ |
| 58 | +structure State (P M S : Type*) where |
| 59 | + /-- A multiset containing all messages that are in-flight (namely, they have been sent but |
| 60 | + not yet received). Note that being a multiset implies that the messages are not ordered. -/ |
| 61 | + msgs : Multiset (Message P M) |
| 62 | + /-- A map giving the local states of all processes. -/ |
| 63 | + proc : P → ProcState S |
| 64 | + |
| 65 | +/-- The specification of a distributed algorithm for solving the consensus problem. |
| 66 | +Note that each field below can depend on a process's identifier (recall that each `Message` |
| 67 | +contains its destination's identifier), so the algorithm is not required to be uniform |
| 68 | +across processes. -/ |
| 69 | +structure Algorithm (P M S : Type*) where |
| 70 | + /-- A map specifying the initial state of each process. -/ |
| 71 | + init : P → S |
| 72 | + /-- A map specifying how a process changes its internal state upon receiving a message. -/ |
| 73 | + next : Message P M → ProcState S → S |
| 74 | + /-- A map specifying what messages a process sends out upon receiving a message. -/ |
| 75 | + send : Message P M → ProcState S → Multiset (Message P M) |
| 76 | + /-- A map specifying the boolean decision a process makes upon receiving a message, |
| 77 | + where `none` means that no decision is made. -/ |
| 78 | + out : Message P M → ProcState S → Option Bool |
| 79 | + |
| 80 | +/-- The type of labels of the LTS defined by an `Algorithm`, where `some m` denotes |
| 81 | +the reception of message `m` and `none` denotes a stuttering step. -/ |
| 82 | +abbrev Action (P M : Type*) := Option (Message P M) |
| 83 | + |
| 84 | +/-- `DestIn ps x` means that if `x ≠ none`, then `x = some m` with `m.dest ∈ ps`. -/ |
| 85 | +def DestIn (ps : Set P) : Action P M → Prop |
| 86 | + | some m => m.dest ∈ ps |
| 87 | + | none => True |
| 88 | + |
| 89 | +/-- Given `inp : P → Bool`, the initial state of the algorithm `a` contains a single message |
| 90 | +carrying the boolean value `inp p` to each process `p`, where the initial internal state is |
| 91 | +`a.init p` and no decision has been made. The assumption `[Fintype P]` is made because |
| 92 | +a multiset may contain only finitely many elements. -/ |
| 93 | +def Algorithm.start [Fintype P] (a : Algorithm P M S) (inp : P → Bool) : State P M S where |
| 94 | + msgs := Multiset.map (fun p ↦ ⟨p, inl (inp p)⟩) Finset.univ.val |
| 95 | + proc := fun p ↦ ⟨a.init p, none⟩ |
| 96 | + |
| 97 | +/-- The specification of how the global state of the algorithm changes when a process `p` |
| 98 | +receives a message `m`. (This function will be used only when such a message `m` exists.) |
| 99 | +Note that once `p` has made a boolean decision in its `out` field, it is not allowed to |
| 100 | +"change its mind" anymore. -/ |
| 101 | +def Algorithm.recvMsg (a : Algorithm P M S) (m : Message P M) (s : State P M S) : State P M S := |
| 102 | + let p := m.dest |
| 103 | + { msgs := s.msgs.erase m + a.send m (s.proc p) |
| 104 | + proc := fun q ↦ |
| 105 | + if q = p then |
| 106 | + ⟨ a.next m (s.proc p), |
| 107 | + if (s.proc p).out.isNone then a.out m (s.proc p) else (s.proc p).out ⟩ |
| 108 | + else s.proc q } |
| 109 | + |
| 110 | +/-- The transition relation of the LTS defined by the algorithm `a`. |
| 111 | +Note that the stuttering step is always allowed. -/ |
| 112 | +def Algorithm.lts (a : Algorithm P M S) : LTS (State P M S) (Action P M) where |
| 113 | + Tr s x s' := match x with |
| 114 | + | some m => m ∈ s.msgs ∧ s' = a.recvMsg m s |
| 115 | + | none => s' = s |
| 116 | + |
| 117 | +/-- `a.Reachable inp s` means that `s` is a reachable state of `a` given the initial `inp`. -/ |
| 118 | +def Algorithm.Reachable [Fintype P] |
| 119 | + (a : Algorithm P M S) (inp : P → Bool) (s : State P M S) : Prop := |
| 120 | + a.lts.CanReach (a.start inp) s |
| 121 | + |
| 122 | +/-- `s.ProcDecided p b` means that process `p` is decided on the boolean value `b` |
| 123 | +in the state `s`. -/ |
| 124 | +abbrev State.ProcDecided (s : State P M S) (p : P) (b : Bool) : Prop := |
| 125 | + (s.proc p).out = some b |
| 126 | + |
| 127 | +/-- `s.Decided b` means that at least one process is decided on the boolean value `b` |
| 128 | +in the state `s`. -/ |
| 129 | +def State.Decided (s : State P M S) (b : Bool) : Prop := |
| 130 | + ∃ p, s.ProcDecided p b |
| 131 | + |
| 132 | +/-- `s.Agreed` says that all boolean values decided on in state `s` must agree with each other. -/ |
| 133 | +def State.Agreed (s : State P M S) : Prop := |
| 134 | + ∀ b b', s.Decided b ∧ s.Decided b' → b = b' |
| 135 | + |
| 136 | +/-- `a.SafeConsensus` says that in any reachable state of `a`, (1) all boolean values decided on |
| 137 | +in that state must agree with each other and (2) that boolean value (if it exists) must be |
| 138 | +one of the boolean values given by `inp` at the beginning. `a.SafeConsensus` is the minimal |
| 139 | +correctness requirement on `a` and is a safety property (hence its name). -/ |
| 140 | +def Algorithm.SafeConsensus [Fintype P] (a : Algorithm P M S) : Prop := |
| 141 | + ∀ inp s, a.Reachable inp s → s.Agreed ∧ ∀ b, s.Decided b → ∃ p, inp p = b |
| 142 | + |
| 143 | +namespace Algorithm |
| 144 | + |
| 145 | +variable {a : Algorithm P M S} {inp : P → Bool} |
| 146 | + |
| 147 | +/-- The stuttering step does not change the global state. -/ |
| 148 | +theorem tr_none {s s' : State P M S} (h : a.lts.Tr s none s') : s = s' := by |
| 149 | + grind [Algorithm.lts] |
| 150 | + |
| 151 | +/-- The initial state is reachable. -/ |
| 152 | +theorem reachable_start [Fintype P] : |
| 153 | + a.Reachable inp (a.start inp) := by |
| 154 | + simp [Algorithm.Reachable, LTS.CanReach.refl] |
| 155 | + |
| 156 | +/-- If `s` is reachable from the initial state and `s'` is reachable from `s`, |
| 157 | +then `s'` is reachable from the initial state. -/ |
| 158 | +theorem reachable_stable [Fintype P] {s s' : State P M S} |
| 159 | + (hr : a.Reachable inp s) (hc : a.lts.CanReach s s') : a.Reachable inp s' := by |
| 160 | + obtain ⟨xs, _⟩ := hr |
| 161 | + obtain ⟨xs', _⟩ := hc |
| 162 | + use xs ++ xs' |
| 163 | + grind [LTS.MTr.comp] |
| 164 | + |
| 165 | +/-- If `p` is decided on the boolean value `b` in `s` and `s'` is reachable from `s`, |
| 166 | +then `p` is still decided on `b` in `s'`. -/ |
| 167 | +theorem procDecided_stable {s s' : State P M S} {p : P} {b : Bool} |
| 168 | + (hd : s.ProcDecided p b) (hc : a.lts.CanReach s s') : s'.ProcDecided p b := by |
| 169 | + obtain ⟨xs, h_mtr⟩ := hc |
| 170 | + induction h_mtr <;> grind [Algorithm.lts, Algorithm.recvMsg] |
| 171 | + |
| 172 | +/-- If at least one process is decided on the boolean value `b` in `s` and `s'` is reachable |
| 173 | +from `s`, then at least one process is still decided on `b` in `s'`. -/ |
| 174 | +theorem decided_stable {s s' : State P M S} {b : Bool} |
| 175 | + (hd : s.Decided b) (hc : a.lts.CanReach s s') : s'.Decided b := by |
| 176 | + obtain ⟨p, _⟩ := hd |
| 177 | + use p |
| 178 | + grind [procDecided_stable] |
| 179 | + |
| 180 | +/-- If `m1` and `m2` are both inflight and they have different destinations, |
| 181 | +then receiving them in either order produces the same end state. -/ |
| 182 | +theorem recvMsg_comm {m1 m2 : Message P M} {s : State P M S} |
| 183 | + (hd : m1.dest ≠ m2.dest) (h1 : m1 ∈ s.msgs) (h2 : m2 ∈ s.msgs) : |
| 184 | + m2 ∈ (a.recvMsg m1 s).msgs ∧ m1 ∈ (a.recvMsg m2 s).msgs ∧ |
| 185 | + a.recvMsg m2 (a.recvMsg m1 s) = a.recvMsg m1 (a.recvMsg m2 s) := by |
| 186 | + rw [State.mk.injEq] |
| 187 | + split_ands |
| 188 | + · grind [Algorithm.recvMsg, mem_erase_of_ne] |
| 189 | + · grind [Algorithm.recvMsg, mem_erase_of_ne] |
| 190 | + · have he1 (x) : (s.msgs.erase m1 + x).erase m2 = (s.msgs.erase m1).erase m2 + x := by |
| 191 | + grind [erase_add_left_pos, mem_erase_of_ne] |
| 192 | + have he2 (x) : (s.msgs.erase m2 + x).erase m1 = (s.msgs.erase m1).erase m2 + x := by |
| 193 | + grind [erase_add_left_pos, mem_erase_of_ne, erase_comm] |
| 194 | + simp [Algorithm.recvMsg, hd, hd.symm, he1, he2, add_assoc] |
| 195 | + grind [add_comm] |
| 196 | + · ext p |
| 197 | + by_cases h_p1 : p = m1.dest <;> by_cases h_p2 : p = m2.dest <;> |
| 198 | + simp [Algorithm.recvMsg, h_p1, h_p2, hd, hd.symm] |
| 199 | + |
| 200 | +/-- A diamond property for the transition relation `a.lts.Tr`. -/ |
| 201 | +theorem tr_diamond {ps : Set P} {x1 x2 : Action P M} {s s1 s2 : State P M S} |
| 202 | + (hx1 : DestIn ps x1) (hs1 : a.lts.Tr s x1 s1) |
| 203 | + (hx2 : DestIn psᶜ x2) (hs2 : a.lts.Tr s x2 s2) : |
| 204 | + ∃ s', a.lts.Tr s1 x2 s' ∧ a.lts.Tr s2 x1 s' := by |
| 205 | + cases x1 <;> cases x2 <;> try grind [Algorithm.lts] |
| 206 | + case some m1 m2 => |
| 207 | + have hd : m1.dest ≠ m2.dest := by grind [DestIn] |
| 208 | + obtain ⟨h_m1, rfl⟩ := hs1 |
| 209 | + obtain ⟨h_m2, rfl⟩ := hs2 |
| 210 | + simp only [Algorithm.lts, exists_eq_right_right] |
| 211 | + grind [recvMsg_comm (a := a) hd h_m1 h_m2] |
| 212 | + |
| 213 | +/-- A message that is in-flight stays in-flight as long as it is not received |
| 214 | +(finite execution version). -/ |
| 215 | +theorem mTr_notRcvd_enabled {s t : State P M S} {xl : List (Action P M)} {m : Message P M} |
| 216 | + (hst : a.lts.MTr s xl t) (hs : m ∈ s.msgs) (hxl : ¬ some m ∈ xl) : m ∈ t.msgs := by |
| 217 | + induction hst |
| 218 | + case refl _ => assumption |
| 219 | + case stepL s x s1 xl t h_tr h_mtr h_ind => |
| 220 | + rcases Option.eq_none_or_eq_some x <;> |
| 221 | + grind [Algorithm.lts, Algorithm.recvMsg, mem_erase_of_ne] |
| 222 | + |
| 223 | +/-- A message that is in-flight stays in-flight as long as it is not received |
| 224 | +(infinite execution version). -/ |
| 225 | +theorem omega_notRcvd_enabled |
| 226 | + {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} {k : ℕ} {m : Message P M} |
| 227 | + (he : a.lts.OmegaExecution ss xs) (hm : m ∈ (ss k).msgs) (hn : ∀ j, k ≤ j → xs j ≠ some m) : |
| 228 | + ∀ j, k ≤ j → m ∈ (ss j).msgs := by |
| 229 | + intro j h_j |
| 230 | + obtain ⟨i, rfl⟩ : ∃ i, j = k + i := by use j - k; grind |
| 231 | + induction i |
| 232 | + case zero => grind |
| 233 | + case succ i _ => |
| 234 | + rcases Option.eq_none_or_eq_some (xs (k + i)) <;> |
| 235 | + grind [he (k + i), Algorithm.lts, Algorithm.recvMsg, mem_erase_of_ne] |
| 236 | + |
| 237 | +end Algorithm |
| 238 | + |
| 239 | +end Cslib.FLP |
0 commit comments