Bracha’s reliable broadcast has been the go-to Byzantine broadcast primitive since 1987. Three rounds, (O(n^2)) messages, optimal fault tolerance at (n > 3f). Textbook stuff.
I’ve been trying to get a fast multi-value agreement primitive: something where all nodes propose values and agree on one (or ⊥ if they’re hopelessly split). Reliable broadcast is the natural building block, but three rounds felt like overkill for the happy path.
So I went digging. Months of searching the literature turned up plenty of options, but they all came with catches: weaker fault models, synchrony assumptions, trusted setups. Nothing that felt like a clean win. Eventually I circled back to Bracha and noticed something hiding in plain sight: by using a larger quorum for the optimistic path…
Bracha’s reliable broadcast has been the go-to Byzantine broadcast primitive since 1987. Three rounds, (O(n^2)) messages, optimal fault tolerance at (n > 3f). Textbook stuff.
I’ve been trying to get a fast multi-value agreement primitive: something where all nodes propose values and agree on one (or ⊥ if they’re hopelessly split). Reliable broadcast is the natural building block, but three rounds felt like overkill for the happy path.
So I went digging. Months of searching the literature turned up plenty of options, but they all came with catches: weaker fault models, synchrony assumptions, trusted setups. Nothing that felt like a clean win. Eventually I circled back to Bracha and noticed something hiding in plain sight: by using a larger quorum for the optimistic path, we can deliver in two rounds when conditions are good. No new assumptions. Same fault tolerance. Just better intersection properties.
This post covers the optimized broadcast and the MVA extension I built on top of it.
0x0: Background for the Uninitiated
If you’re coming from reverse engineering or security research and have never touched distributed systems, here’s the setup.
Byzantine fault tolerance means the protocol stays correct even when some participants are actively malicious. Not just crashed or slow, but actively trying to break the system: lying, sending conflicting messages to different parties, colluding with each other. Named after the Byzantine Generals Problem.
Asynchronous model is the hardest setting for distributed protocols. Messages can be delayed arbitrarily by the adversary, there are no timeouts or clocks you can rely on, and you can’t tell a slow node from a dead one. The upside: protocols proven correct in this model stay safe no matter what happens with timing. The downside: you can’t guarantee termination if enough nodes are faulty (see FLP impossibility).
Quorum intersection is the key trick. If you require (n - f) nodes to agree on something, any two such sets overlap. With (n > 3f), the overlap is at least (f + 1) nodes, so at least one is honest. This honest node “witnesses” both sets and can prevent conflicting decisions.
0x1: The Problem
Byzantine reliable broadcast: a designated leader wants to broadcast value (v) to (n) parties, up to (f < n/3) of which are Byzantine. We need:
- Agreement: Honest parties that deliver, deliver the same value
- Validity: If the leader is honest and broadcasts (v), all honest parties eventually deliver (v)
- Totality: If one honest party delivers, all honest parties eventually deliver
Why Not Just Echo?
The naive approach fails:
upon ⟨INIT, v⟩ from leader:
send ⟨ECHO, v⟩ to all
upon E(v) ≥ n−f:
deliver(v) // broken!
A Byzantine leader can equivocate: send (x) to some parties, (y) to others. With (n = 7, f = 2): four honest parties echo (x), three echo (y). Byzantine nodes help both sides reach threshold. Two honest parties deliver different values. Agreement violated.
Quorum intersection guarantees overlap, but that overlap might be entirely Byzantine. One honest node in the overlap can’t stop conflicting echoes from both reaching (n - f).
Bracha’s Fix: Add a Voting Round
Bracha’s insight: add a READY phase that “locks in” a value. Honest parties only READY once, and only for values that reached the echo threshold. Now conflicting values can’t both reach READY quorum.
upon start as leader with input v:
send ⟨INIT, v⟩ to all
upon ⟨INIT, v⟩ from leader ∧ sentₑ = ⊥:
send ⟨ECHO, v⟩ to all; sentₑ ← v
upon E(v) ≥ n−f ∧ sentᵣ = ⊥:
send ⟨READY, v⟩ to all; sentᵣ ← v
upon R(v) ≥ f+1 ∧ sentᵣ = ⊥: // Amplification
send ⟨READY, v⟩ to all; sentᵣ ← v
upon R(v) ≥ n−f ∧ delivered = ⊥:
deliver(v)
Three rounds. Works. But when the leader is honest and the network is healthy, do we really need all three?
0x2: The Counterintuitive Insight
upon start as leader with input v:
send ⟨INIT, v⟩ to all
upon ⟨INIT, v⟩ from leader ∧ sentₑ = ⊥:
send ⟨ECHO, v⟩ to all; sentₑ ← v
upon E(v) ≥ n−f ∧ sentᵣ = ⊥:
send ⟨READY, v⟩ to all; sentᵣ ← v
upon R(v) ≥ f+1 ∧ sentᵣ = ⊥: // Amplification
send ⟨READY, v⟩ to all; sentᵣ ← v
upon R(v) ≥ n−f ∧ delivered = ⊥:
deliver(v)
Why the READY round? ECHOs alone can’t guarantee termination. A Byzantine leader can equivocate, sending different values to different parties, fragmenting honest echoes.
Standard quorum intersection gives us (n - 2f > f) overlap between any two ((n-f))-sized sets. That’s enough honest overlap to prevent two conflicting values from both reaching (n-f) ECHOs—but it doesn’t help when neither value reaches threshold. A Byzantine leader can fragment honest echoes across multiple values, leaving everyone stuck. The READY round breaks the deadlock.
0x1: The Counterintuitive Insight
The clue came from a Tendermint forum post explaining why their protocol needs a pre-vote phase. The observation: with (n = 3f+1) nodes, you need pre-vote. But with (n = 5f+1) nodes, you can skip it entirely.
I stared at this for a while. How can adding nodes let you skip a round? Rounds exist to do something. You can’t just add redundancy and magically skip a communication step…
However, it starts to make sense once you realize the extra nodes aren’t just redundancy. They change the flavor of quorum intersection. Standard quorum intersection guarantees overlap, but that overlap might be almost entirely Byzantine. A larger quorum guarantees honest nodes in the overlap. And honest nodes don’t equivocate. What if we had a majority of honest nodes right in there?
We don’t need more nodes. We need a higher threshold on the same nodes, which gives us the same stronger intersection property.
Define three thresholds:
[ \begin{aligned} Q &= n - f &&\text{(standard quorum)} \ Q_o &= \lfloor n/2 \rfloor + f + 1 &&\text{(optimistic threshold)} \ Q_a &= f + 1 &&\text{(amplification threshold)} \end{aligned} ]
The magic is in (Q_o):
Lemma (Strong Intersection): Any two sets of size Qₒ overlap in at least f+1 honest parties.
Proof: Let (S_1, S_2) be sets of size (Q_o).
[ |S_1 \cap S_2| \geq 2Q_o - n = 2(\lfloor n/2 \rfloor + f + 1) - n \geq 2f + 1 ]
Since at most (f) are Byzantine, the overlap contains at least (f + 1) honest parties. ∎
Let’s visualize why this matters. With (n = 10) and (f = 3):
Fundamentally different from standard quorum intersection. With Qₒ echoes for some value v, we know that ≥f+1 honest parties echoed v. And honest parties echo exactly once. So no conflicting value can ever reach Qₒ, or even Q, since the remaining honest parties number at most (n − f) − (f + 1) = n − 2f − 1 < Q − f.
We can deliver before the READY round completes. READYs still propagate to ensure totality.
0x2: Round-Optimized Bracha
The optimized protocol adds an “optimistic delivery” path:
upon ⟨INIT, v⟩ from leader ∧ sentₑ = ⊥:
send ⟨ECHO, v⟩ to all; sentₑ ← v
upon E(v) ≥ Qₒ ∧ delivered = ⊥: // Optimistic
if sentᵣ = ⊥: send ⟨READY, v⟩ to all; sentᵣ ← v
deliver(v); delivered ← v
upon E(v) ≥ Q ∧ sentᵣ = ⊥ ∧ delivered = ⊥: // Q echoes -> ready
send ⟨READY, v⟩ to all; sentᵣ ← v
upon R(v) ≥ Qₐ ∧ sentᵣ = ⊥ ∧ delivered = ⊥: // Amplification
send ⟨READY, v⟩ to all; sentᵣ ← v
upon R(v) ≥ Q ∧ delivered = ⊥: // Standard delivery
if sentᵣ = ⊥: send ⟨READY, v⟩ to all; sentᵣ ← v
deliver(v); delivered ← v
Note on Totality: When a process delivers via the optimistic path, it also sends
READY(v), ensuring the value propagates through amplification. Even if only one correct process initially sees Qₒ echoes (with Byzantine help), the resulting READY triggers amplification at other processes. Amplification requires only Qₐ readies (no echo-backing), allowing the value to propagate to Q readies for standard delivery. READYs propagate progressively as they arrive at slower processes.
Happy case (honest leader, healthy network): All (n - f) honest parties ECHO the same value. If the network is well-synchronized, all honest ECHOs arrive quickly, often reaching Qₒ before the READY phase begins.
Adversarial case (Byzantine leader or delayed messages): Some value reaches (Q) ECHOs but not (Q_o). Fall back to three rounds via READYs.
Safety Proof Sketch
Three cases:
Two optimistic deliveries can’t conflict: Both require (Q_o) ECHOs. By strong intersection, (\geq f+1) honest parties appear in both sets. But honest parties ECHO once. Contradiction. 1.
Optimistic delivery blocks conflicting standard delivery: If (v) gets (Q_o) ECHOs, at least (Q_o - f \geq f + 1) honest parties echoed (v). The remaining honest parties ((\leq n - f - (f+1) = n - 2f - 1)) plus (f) Byzantine can produce at most (n - f - 1 < Q) votes for any other value. 1.
Standard paths use Bracha’s original safety: Quorum intersection ensures agreement.
The TLA+ Spec
bracha_opt.tla (click to expand)
1-------------------- MODULE bracha_opt --------------------
2(*
3 Optimized Bracha Reliable Broadcast with Fast Path
4 ===================================================
5 Can Bölük, April 1, 2025.
6
7 Single-leader Byzantine reliable broadcast with optimistic 2-round
8 delivery. Falls back to standard 3-round Bracha when conditions are
9 adversarial.
10
11 Properties (n > 3f):
12 - Agreement All honest parties deliver the same value
13 - Validity If broadcaster is honest, all deliver its input
14 - Totality If one honest delivers, all honest eventually deliver
15 - Termination All honest parties eventually deliver
16
17 Synchrony: Safety holds under full asynchrony. Termination requires
18 partial synchrony (bounded message delay after GST).
19
20 Fault Model: A faulty broadcaster can send different values to different
21 recipients. Modeled via a partition function assigning each honest party
22 to a value. Faulty non-broadcasters can send arbitrary ECHO/READY.
23 *)
24
25EXTENDS Naturals, FiniteSets, TLC
26
27\* ============================================================================
28\* Protocol Parameters
29\* ============================================================================
30CONSTANTS
31 Honest, \* the set of correct processes
32 Faulty, \* the set of Byzantine processes, may be empty
33 V \* the set of valid values
34
35\* Sentinel for not yet set
36NULL ≜ "∅"
37
38\* Arbitrary value - symmetric so choice irrelevant
39Command ≜ CHOOSE v ∈ V : TRUE
40
41\* ============================================================================
42\* Definitions
43\* ============================================================================
44P ≜ Honest ∪ Faulty \* the set of all processes
45N ≜ Cardinality(P) \* total number of processes
46F ≜ Cardinality(Faulty) \* number of Byzantine processes
47
48\* Thresholds
49Q ≜ N - F \* standard quorum (2f+1 when n=3f+1)
50Qo ≜ N ÷ 2 + F + 1 \* optimistic quorum
51Qa ≜ F + 1 \* amplification (f+1)
52
53ASSUME ∧ N > 3 * F
54 ∧ V ≠ {}
55 ∧ Honest ∩ Faulty = {}
56 ∧ IsFiniteSet(Honest)
57 ∧ IsFiniteSet(Faulty)
58 ∧ IsFiniteSet(V)
59
60\* Symmetry: combine permutations across Honest, Faulty, V
61CombinePerm(ph, pf, pv) ≜
62 [x ∈ P ∪ V ↦ IF x ∈ Honest THEN ph[x]
63 ELSE IF x ∈ Faulty THEN pf[x]
64 ELSE pv[x]]
65
66Sym ≜ {CombinePerm(ph, pf, pv) :
67 ph ∈ Permutations(Honest),
68 pf ∈ Permutations(Faulty),
69 pv ∈ Permutations(V)}
70
71\* Broadcaster candidates (one of each type by symmetry)
72OneHonest ≜ IF Honest ≠ {} THEN {CHOOSE h ∈ Honest : TRUE} ELSE {}
73OneFaulty ≜ IF Faulty ≠ {} THEN {CHOOSE f ∈ Faulty : TRUE} ELSE {}
74
75\* ============================================================================
76\* Protocol State Variables
77\* ============================================================================
78VARIABLES
79 broadcaster, \* Distinguished leader process
80
81 \* === Honest party broadcast state ===
82 sent_init, \* [P -> V ∪ {NULL}]
83 sent_echo, \* [P -> V ∪ {NULL}]
84 sent_ready, \* [P -> V ∪ {NULL}]
85
86 \* === Faulty broadcaster equivocation ===
87 faulty_equivoc, \* [V -> SUBSET Honest]: partition for faulty broadcaster equivocation
88
89 \* === Per-recipient receive tracking (count-based) ===
90 rcvd_init_v, \* [Honest -> V ∪ {NULL}]: INIT value received
91 rcvd_echo_cnt, \* [Honest -> [V -> 0..N]]: count of ECHOs for v received
92 rcvd_ready_cnt, \* [Honest -> [V -> 0..N]]: count of READYs for v received
93
94 delivered \* [Honest -> V ∪ {NULL}]: Delivered value
95
96send_vars ≜ ⟨sent_init, sent_echo, sent_ready⟩
97recv_vars ≜ ⟨rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt⟩
98vars ≜ ⟨broadcaster, sent_init, faulty_equivoc, sent_echo, sent_ready,
99 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
100
101\* ============================================================================
102\* Helper Operators
103\* ============================================================================
104HasInit(p) ≜ rcvd_init_v[p] ≠ NULL
105InitValue(p) ≜ rcvd_init_v[p]
106
107SentEchoCount(v) ≜ Cardinality({src ∈ P : sent_echo[src] = v})
108SentReadyCount(v) ≜ Cardinality({src ∈ P : sent_ready[src] = v})
109
110EchoQuorum(p, t) ≜ {v ∈ V : rcvd_echo_cnt[p][v] ≥ t}
111ReadyQuorum(p, t) ≜ {v ∈ V : rcvd_ready_cnt[p][v] ≥ t}
112
113\* ============================================================================
114\* Type Invariant
115\* ============================================================================
116TypeOK ≜
117 ∧ broadcaster ∈ P
118 ∧ sent_init ∈ [P → V ∪ {NULL}]
119 ∧ faulty_equivoc ∈ [V → SUBSET Honest]
120 ∧ sent_echo ∈ [P → V ∪ {NULL}]
121 ∧ sent_ready ∈ [P → V ∪ {NULL}]
122 ∧ rcvd_init_v ∈ [Honest → V ∪ {NULL}]
123 ∧ rcvd_echo_cnt ∈ [Honest → [V → 0‥N]]
124 ∧ rcvd_ready_cnt ∈ [Honest → [V → 0‥N]]
125 ∧ delivered ∈ [Honest → V ∪ {NULL}]
126
127\* ============================================================================
128\* Protocol Initialization
129\* ============================================================================
130Init ≜
131 ∧ broadcaster ∈ OneHonest ∪ OneFaulty
132 ∧ sent_init = [src ∈ P ↦ NULL]
133 ∧ faulty_equivoc = [v ∈ V ↦ {}]
134 ∧ sent_echo = [src ∈ P ↦ NULL]
135 ∧ sent_ready = [src ∈ P ↦ NULL]
136 ∧ rcvd_init_v = [p ∈ Honest ↦ NULL]
137 ∧ rcvd_echo_cnt = [p ∈ Honest ↦ [v ∈ V ↦ 0]]
138 ∧ rcvd_ready_cnt = [p ∈ Honest ↦ [v ∈ V ↦ 0]]
139 ∧ delivered = [p ∈ Honest ↦ NULL]
140
141\* ============================================================================
142\* Message Reception
143\* ============================================================================
144
145\* Receive INIT from honest broadcaster (uniform value)
146ReceiveInitFromHonest(p) ≜
147 ∧ delivered[p] = NULL
148 ∧ rcvd_init_v[p] = NULL
149 ∧ broadcaster ∈ Honest
150 ∧ sent_init[broadcaster] ≠ NULL
151 ∧ rcvd_init_v' = [rcvd_init_v EXCEPT ![p] = sent_init[broadcaster]]
152 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo, sent_ready,
153 rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
154
155\* Receive INIT from faulty broadcaster (uses equivocation partition)
156ReceiveInitFromFaulty(p) ≜
157 ∧ delivered[p] = NULL
158 ∧ rcvd_init_v[p] = NULL
159 ∧ broadcaster ∈ Faulty
160 ∧ ∃ v ∈ V : p ∈ faulty_equivoc[v]
161 ∧ LET v ≜ CHOOSE v ∈ V : p ∈ faulty_equivoc[v]
162 IN rcvd_init_v' = [rcvd_init_v EXCEPT ![p] = v]
163 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo, sent_ready,
164 rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
165
166\* Receive one more ECHO for value v (count-based)
167ReceiveEcho(p) ≜
168 ∧ delivered[p] = NULL
169 ∧ ∃ v ∈ V :
170 ∧ rcvd_echo_cnt[p][v] < SentEchoCount(v)
171 ∧ rcvd_echo_cnt' = [rcvd_echo_cnt EXCEPT ![p][v] = @ + 1]
172 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo, sent_ready,
173 rcvd_init_v, rcvd_ready_cnt, delivered⟩
174
175\* Receive one more READY for value v (count-based)
176ReceiveReady(p) ≜
177 ∧ delivered[p] = NULL
178 ∧ ∃ v ∈ V :
179 ∧ rcvd_ready_cnt[p][v] < SentReadyCount(v)
180 ∧ rcvd_ready_cnt' = [rcvd_ready_cnt EXCEPT ![p][v] = @ + 1]
181 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo, sent_ready,
182 rcvd_init_v, rcvd_echo_cnt, delivered⟩
183
184Receive(p) ≜
185 ∨ ReceiveInitFromHonest(p)
186 ∨ ReceiveInitFromFaulty(p)
187 ∨ ReceiveEcho(p)
188 ∨ ReceiveReady(p)
189
190\* ============================================================================
191\* Faulty Party Actions
192\* ============================================================================
193
194\* Faulty broadcaster assigns honest parties to value partitions (equivocation)
195FaultyEquivocate ≜
196 ∧ broadcaster ∈ Faulty
197 ∧ faulty_equivoc = [v ∈ V ↦ {}]
198 ∧ ∃ partition ∈ [Honest → V] :
199 faulty_equivoc' = [v ∈ V ↦ {h ∈ Honest : partition[h] = v}]
200 ∧ UNCHANGED ⟨broadcaster, sent_init, sent_echo, sent_ready,
201 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
202
203\* Faulty party sends ECHO for arbitrary value
204FaultySendEcho ≜
205 ∃ f ∈ Faulty, v ∈ V :
206 ∧ sent_echo[f] = NULL
207 ∧ sent_echo' = [sent_echo EXCEPT ![f] = v]
208 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_ready,
209 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
210
211\* Faulty party sends READY for arbitrary value
212FaultySendReady ≜
213 ∃ f ∈ Faulty, v ∈ V :
214 ∧ sent_ready[f] = NULL
215 ∧ sent_ready' = [sent_ready EXCEPT ![f] = v]
216 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo,
217 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
218
219FaultyStep ≜
220 ∨ FaultyEquivocate
221 ∨ FaultySendEcho
222 ∨ FaultySendReady
223
224\* ============================================================================
225\* Honest Party Actions
226\* ============================================================================
227
228\* Honest broadcaster sends INIT (same value to all)
229LeaderInit(self) ≜
230 ∧ self = broadcaster
231 ∧ self ∈ Honest
232 ∧ sent_init[self] = NULL
233 ∧ delivered[self] = NULL
234 ∧ sent_init' = [sent_init EXCEPT ![self] = Command]
235 ∧ UNCHANGED ⟨broadcaster, faulty_equivoc, sent_echo, sent_ready,
236 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
237
238\* Upon receiving INIT: broadcast ECHO(v)
239EchoOnInit(self) ≜
240 ∧ sent_echo[self] = NULL
241 ∧ delivered[self] = NULL
242 ∧ HasInit(self)
243 ∧ sent_echo' = [sent_echo EXCEPT ![self] = InitValue(self)]
244 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_ready,
245 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
246
247\* Upon receiving Q echoes for v: broadcast READY(v)
248ReadyOnEchos(self) ≜
249 ∧ sent_ready[self] = NULL
250 ∧ delivered[self] = NULL
251 ∧ ∃ v ∈ EchoQuorum(self, Q) :
252 sent_ready' = [sent_ready EXCEPT ![self] = v]
253 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo,
254 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
255
256\* Upon receiving Qa readies for v: broadcast READY(v)
257ReadyAmplify(self) ≜
258 ∧ sent_ready[self] = NULL
259 ∧ delivered[self] = NULL
260 ∧ ∃ v ∈ ReadyQuorum(self, Qa) :
261 sent_ready' = [sent_ready EXCEPT ![self] = v]
262 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo,
263 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt, delivered⟩
264
265\* Upon receiving Q readies for v: deliver v (and send READY if not yet sent)
266DeliverOnReady(self) ≜
267 ∧ delivered[self] = NULL
268 ∧ ∃ v ∈ ReadyQuorum(self, Q) :
269 ∧ delivered' = [delivered EXCEPT ![self] = v]
270 ∧ IF sent_ready[self] = NULL
271 THEN sent_ready' = [sent_ready EXCEPT ![self] = v]
272 ELSE UNCHANGED sent_ready
273 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo,
274 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt⟩
275
276\* Upon receiving Qo echoes for v: deliver v (fast path)
277OptimisticDeliver(self) ≜
278 ∧ delivered[self] = NULL
279 ∧ ∃ v ∈ EchoQuorum(self, Qo) :
280 ∧ delivered' = [delivered EXCEPT ![self] = v]
281 ∧ IF sent_ready[self] = NULL
282 THEN sent_ready' = [sent_ready EXCEPT ![self] = v]
283 ELSE UNCHANGED sent_ready
284 ∧ UNCHANGED ⟨broadcaster, sent_init, faulty_equivoc, sent_echo,
285 rcvd_init_v, rcvd_echo_cnt, rcvd_ready_cnt⟩
286
287HonestStep(self) ≜
288 ∨ LeaderInit(self)
289 ∨ EchoOnInit(self)
290 ∨ ReadyOnEchos(self)
291 ∨ ReadyAmplify(self)
292 ∨ DeliverOnReady(self)
293 ∨ OptimisticDeliver(self)
294
295\* ============================================================================
296\* Specification
297\* ============================================================================
298Terminated ≜ ∀ p ∈ Honest : delivered[p] ≠ NULL
299
300Done ≜ Terminated ∧ UNCHANGED vars
301
302Next ≜
303 ∨ ∃ p ∈ Honest : HonestStep(p)
304 ∨ ∃ p ∈ Honest : Receive(p)
305 ∨ FaultyStep
306 ∨ Done
307
308\* Weak fairness for honest actions and message reception
309Fairness ≜
310 ∧ ∀ p ∈ Honest : WF_vars(HonestStep(p))
311 ∧ ∀ p ∈ Honest : WF_vars(Receive(p))
312
313Spec ≜ Init ∧ □[Next]_vars ∧ Fairness
314
315\* ============================================================================
316\* Safety Properties
317\* ============================================================================
318
319Agreement ≜
320 ∀ p, q ∈ Honest :
321 (delivered[p] ≠ NULL ∧ delivered[q] ≠ NULL) ⇒ delivered[p] = delivered[q]
322
323Validity ≜
324 broadcaster ∈ Honest ⇒
325 ∀ p ∈ Honest : delivered[p] ≠ NULL ⇒ delivered[p] = Command
326
327\* ============================================================================
328\* Liveness
329\* ============================================================================
330
331Termination ≜ ∀ p ∈ Honest : ◇(delivered[p] ≠ NULL)
332
333=============================================================================
Model check with n=4, f=1 (or n=7, f=2 if you have patience) and verify Agreement, Validity, and Termination.
0x3: From Broadcast to Multi-Value Agreement
The round-optimized Bracha handles the single-leader case. But what if everyone has a value to propose? This is multi-value agreement (MVA):
- Every process starts with an input value
- All honest processes deliver the same output
- If a supermajority agrees on input (v), output must be (v)
- If inputs are split, output can be (\bot) (explicit “no consensus”)
MVA is useful whenever you have a bunch of servers that need to agree on their own observations, extracting a supermajority opinion from conflicting proposals: leader election, view changes, detecting failures, etc.
The Challenge
Without a designated leader, equivocation isn’t the threat. Fragmentation is. If honest inputs split across multiple values, no single value might reach quorum. We need:
- A way to detect when no value can win
- A safe way to terminate with (\bot) in that case
- Guarantees that (\bot) only happens when genuinely necessary
Additional Thresholds
Two more:
[ \begin{aligned} Q_s &= \lfloor (n + f) / 2 \rfloor + 1 &&\text{(supermajority threshold)} \ Q_e &= \lfloor n/2 \rfloor + 1 &&\text{(echo-backing threshold)} \end{aligned} ]
If ≥Qₛ honest processes have the same input, that value must be the output (“strong validity”).
The echo-backing threshold (Q_e) prevents an adversary from exploiting message scheduling to make minority values win. More on this shortly.
0x4: The Multi-Value Protocol
The protocol extends round-optimized Bracha with:
- ECHO phase: Each process echoes its own input (not a leader’s INIT)
- READY phase: Same as before, but can also READY (\bot) if echoes fragment
- ABORT phase: New mechanism for when READYs themselves fragment
Helper definitions (where (E(v)) and (R(v)) denote counts of ECHOs and READYs received for value (v)):
$$\text{PluralityAmongEchoes} \triangleq \text{unique } \underbrace{\arg\max_v E(v)}_{\text{most echoes}} \text{, or } \bot$$
$$\text{CanWin}(x) \triangleq \underbrace{R(x)}_{\text{current}} + \underbrace{(n - \text{TotalReadies})}_{\text{outstanding}} \geq Q$$
$$\text{CanReachQuorum} \triangleq \underbrace{\max_v R(v)}_{\text{best}} + \underbrace{(n - \text{TotalReadies})}_{\text{outstanding}} \geq Q$$
$$\text{CanReachEchoBacking} \triangleq \underbrace{\max_v E(v)}_{\text{best}} + \underbrace{\max(0, n - \text{TotalEchos} - f)}_{\text{remaining honest}} \geq Q_e$$
// State variables (per process):
// sentᵣ ∈ V ∪ {⊥, ∅} - what READY was broadcast (∅ = none yet)
// delivered ∈ V ∪ {⊥, ∅} - delivered value (∅ = none yet)
// sentₐ ∈ {true, false} - whether ABORT was sent
upon start:
send ⟨ECHO, input⟩ to all
upon E(v) ≥ Q ∧ sentᵣ = ∅: // Q echoes -> ready
send ⟨READY, v⟩ to all; sentᵣ ← v
upon TotalEchoes ≥ Q ∧ (∀v: E(v) < Q) // R2: timeout path
∧ sentᵣ = ∅ ∧ delivered = ∅:
plurality ← PluralityAmongEchoes() // unique max, or ⊥ if tied
hasBacking ← plurality ≠ ⊥ ∧ E(plurality) ≥ Qₑ
if ¬hasBacking ∧ CanReachEchoBacking():
wait // more echoes may arrive
else if hasBacking:
send ⟨READY, plurality⟩ to all; sentᵣ ← plurality
else: // no backing possible, demote
send ⟨READY, ⊥⟩ to all; sentᵣ ← ⊥
upon R(v) ≥ Qₐ ∧ sentᵣ = ∅: // R3: amplify value
send ⟨READY, v⟩ to all; sentᵣ ← v
upon R(⊥) ≥ Qₐ ∧ sentᵣ = ∅: // R4: amplify ⊥
send ⟨READY, ⊥⟩ to all; sentᵣ ← ⊥
Why ties must wait: When
PluralityAmongEchoes()returns ⊥ (a tie), the protocol waits rather than immediately readying ⊥. Additional honest echoes may break the tie. Only whenCanReachEchoBacking()becomes false (all honest echoes have arrived, no value can reach (Q_e)) does the protocol commit to ⊥.
upon E(v) ≥ Qₒ ∧ delivered = ∅ // D1: fast path (2 rounds)
∧ sentᵣ ∈ {∅, v}:
if sentᵣ = ∅: send ⟨READY, v⟩; sentᵣ ← v
delivered ← v
upon R(v) ≥ Q ∧ delivered = ∅ // D2: deliver on ready quorum
∧ (sentᵣ ∈ {∅, v} ∨ ¬CanWin(sentᵣ)):
if sentᵣ = ∅: send ⟨READY, v⟩; sentᵣ ← v
delivered ← v
upon R(⊥) ≥ Q ∧ delivered = ∅ // D3: deliver on ready-⊥ quorum
∧ (sentᵣ ∈ {∅, ⊥} ∨ ¬CanWin(sentᵣ)):
if sentᵣ = ∅: send ⟨READY, ⊥⟩; sentᵣ ← ⊥
delivered ← ⊥
// Abort mechanism (READYs fragment irrecoverably)
upon sentᵣ ≠ ∅ ∧ TotalReadies ≥ Q // A1: initiate abort
∧ (∀v: R(v) < Q) ∧ R(⊥) < Q
∧ ¬CanReachQuorum():
send ⟨ABORT⟩ to all; sentₐ ← true
upon Aborts ≥ Qₐ ∧ sentᵣ ≠ ∅ // A2: amplify abort
∧ sentₐ = false:
send ⟨ABORT⟩ to all; sentₐ ← true
upon Aborts ≥ Q ∧ sentᵣ ≠ ∅ ∧ delivered = ∅ // A3: deliver on abort
∧ TotalReadies ≥ Q ∧ (∀v: R(v) ≤ Q − 2f − 1):
if sentₐ = false: send ⟨ABORT⟩; sentₐ ← true
delivered ← ⊥
Abort triggers when a process has readied, received (Q) total readies, but no value can reach (Q). ABORTs propagate via amplification, and (Q) ABORTs force delivery of (\bot).
On A3’s guard: The
∀v: R(v) ≤ Q − 2f − 1condition prevents aborting when a value could have achieved quorum elsewhere. If some value (v) got (Q) readies globally, at least (Q - f) correct processes sentREADY(v). A3 requires having heard from (Q) senders, at least (Q - f) correct. Pigeonhole: overlap (\geq (Q-f) + (Q-f) - (n-f) = Q - 2f). So we’d observe (\geq Q - 2f) readies for (v) locally, blocking the abort.
Safety Properties
Agreement: Same intersection arguments, plus: if anyone delivers (v \in V), they saw (Q_o) ECHOs or (Q) READYs for (v). For D1, (\geq Q_e) correct processes echoed (v); for D2, (\geq Q_a) correct processes readied (v). Either prevents a conflicting value from reaching delivery threshold.
Strong Validity: If (\geq Q_s) honest processes input (v), then (v) has a strict majority among all honest echoes. By Lemma 2 in the spec, any process receiving (Q) echoes either sees (Q) for (v) directly, or (v) is the majority. Either way, all READYs go to (v), and (v) is delivered.
Integrity: If someone delivers (\bot), it required (Q) READYs for (\bot) or (Q) ABORTs. Both require (\geq Q_a) honest processes to have sent (\bot)/ABORT. Only happens when no value achieved supermajority.
Synchrony Model: Safety (Agreement, Validity, Integrity) holds under full asynchrony. Only demotion-to-⊥ requires partial synchrony (correct-to-correct messages arrive within Δ after GST). Consistent with FLP.
Termination (partial synchrony): Every honest process eventually receives (Q) total echoes (since (|Honest| \geq Q)). From there:
- Some value reaches (Q_o): optimistic delivery
- Some value reaches (Q): standard delivery
- Echoes fragment: after timeout, demote to (\bot) when
CanReachEchoBacking() = false - READYs fragment: abort mechanism fires
The Echo-Backing Fix
The E(v) ≥ Qₑ guard on R2 wasn’t in the initial design. Model checking revealed a subtle attack that only surfaces in MVA (not single-leader broadcast). This echo-backing requirement applies only to R2 (plurality ready), not to R3 (amplification).
The Attack: Consider (n = 7, f = 2) with thresholds (Q = 5), (Q_o = 6), (Q_e = 4). Honest processes (h_1)–(h_4) input (x); honest (h_5) inputs (y). Byzantine processes send (\text{ECHO}(x)) to (h_1) and (\text{ECHO}(y)) to everyone else.
The adversary schedules delivery so (h_2) receives its first (Q = 5) echoes as ({B_1(y), B_2(y), h_5(y), h_1(x), h_3(x)}), giving (E(y) = 3, E(x) = 2). Without echo-backing, (h_2) would ready (y) via R2 (plurality). Similarly for (h_3, h_4, h_5).
Meanwhile, (h_1) sees (Q_o = 6) echoes for (x) and delivers via D1. If (h_2)–(h_5) ready (y) and deliver via D2, Agreement is violated.
Why Echo-Backing Blocks This: The maximum echoes for (y) at any correct process is:
$$ E(y) = \underbrace{1}_{h_5} + \underbrace{2}_{\text{Byzantine}} = 3 < 4 = Q_e $$
Since (E(y) < Qₑ), R2’s guard fails. Process (h₂) must wait. Eventually (h₂(x)) and (h₄(x)) arrive, yielding (E(x) = 4 \geq Qₑ). Now (x) is both the plurality and has echo-backing, so (h₂) readies (x).
A value with (Qₒ) echoes at any process guarantees (\geq Qₑ) echoes at every correct process (since (Qₒ - f = Qₑ)). The echo-backing guard ensures we only ready values that could plausibly have fast-path support.
Liveness (partial synchrony required): What if plurality exists but can never reach echo-backing? This happens when all correct echoes have arrived but they’re fragmented. Demotion to (\bot) requires both:
- A local timeout has fired, AND
CanReachEchoBacking() = false
Under partial synchrony, after GST all correct-to-correct messages arrive within Δ. A timeout calibrated to ≥ Δ ensures all correct echoes arrive first. Post-timeout, HonestEchoSenders equals the count of correct processes, so CanReachEchoBacking() accurately reflects whether any value can still reach (Q_e).
If any value had supermajority support ((\geq Q_s) correct inputs), it would achieve (\geq Q_e) echoes from correct processes alone, arriving before timeout.
Implementation: The timeout must fire only after all correct echoes arrive. In partial synchrony, use increasing timeouts (exponential backoff) until post-GST. Pre-GST, if a timeout fires early, don’t demote: re-check
CanReachEchoBacking()(still true if correct echoes are missing). The TLA+ model makes timeout contingent on all correct echoes having been received.
Safety vs. Liveness: Safety (Agreement, Validity) holds under full asynchrony. Only demotion-to-(\bot) liveness requires partial synchrony. Consistent with FLP.
The CanWin Fallback
The ¬CanWin(sentᵣ) fallback in D2/D3 prevents livelock. Without it, a process that sent READY for a minority value gets stuck forever when a different value achieves (Q) readies. The primary guard sentᵣ ∈ {∅, v} fails, but the process can’t deliver. The fallback lets it give up when its value is mathematically eliminated.
The TLA+ Spec
rcast.tla (click to expand)
1-------------------- MODULE rcast --------------------
2(*
3 Rapidcast MVA: Byzantine Multi-Value Agreement with Optimistic Fast Path
4 ========================================================================
5 * Version 2. Simplified state representation, abort safety fixes.
6 Can Bölük, April 3, 2025.
7
8 All processes propose values and agree on one output (or ⊥ when inputs
9 are irreconcilably split). Delivers in 2 rounds when a supermajority
10 shares the same input; falls back to 3-4 rounds otherwise.
11
12 Properties (n > 3f):
13 - Agreement No two honest processes deliver different values
14 - Strong Validity Supermajority input v: output v
15 - Weak Validity Output v ∈ V: some honest process input v
16 - Integrity Output ⊥: no supermajority existed
17 - Termination All honest processes eventually deliver
18
19 Synchrony: Safety holds under full asynchrony. Termination requires
20 partial synchrony (bounded message delay after GST).
21
22 Fault Model: Byzantine processes may equivocate (send different values
23 to different recipients). Modeled via per-recipient nondeterministic
24 message content. Honest processes broadcast uniformly.
25*)
26
27EXTENDS Naturals, FiniteSets, TLC
28
29\* ============================================================================
30\* SYNCHRONY MODEL:
31\* ============================================================================
32\* Safety holds under full asynchrony. Termination needs partial synchrony:
33\* ReadyOnTimeout's ⊥-demotion assumes all honest echoes arrive before
34\* CanReachEchoBacking becomes false. Implementation: timeout > post-GST Δ.
35\* Spec abstracts timing via fairness on honest-to-honest delivery.
36\* ============================================================================
37
38\* ============================================================================
39\* Protocol Parameters
40\* ============================================================================
41CONSTANTS
42 Honest, \* the set of correct processes
43 Faulty, \* the set of Byzantine processes, may be empty
44 V \* the set of valid values
45
46\* Sentinel values
47NULL ≜ "∅" \* not yet set
48Bottom ≜ "⊥" \* no value (abort outcome)
49VExt ≜ V ∪ {Bottom}
50
51\* ============================================================================
52\* Definitions
53\* ============================================================================
54P ≜ Honest ∪ Faulty
55N ≜ Cardinality(P)
56F ≜ Cardinality(Faulty)
57
58\* Protocol thresholds
59Q ≜ N - F \* quorum (2f+1 when n=3f+1)
60Qo ≜ N ÷ 2 + F + 1 \* optimistic delivery
61Qa ≜ F + 1 \* amplification
62Qs ≜ (N + F) ÷ 2 + 1 \* supermajority
63Qe ≜ N ÷ 2 + 1 \* echo-backing (majority)
64
65ASSUME ∧ N > 3 * F
66 ∧ V ≠ {}
67 ∧ Honest ∩ Faulty = {}
68 ∧ IsFiniteSet(Honest)
69 ∧ IsFiniteSet(Faulty)
70 ∧ IsFiniteSet(V)
71 \* Disjointness: values, parties, sentinels
72 ∧ V ∩ P = {}
73 ∧ Bottom ∉ V ∧ NULL ∉ V
74 ∧ Bottom ∉ P ∧ NULL ∉ P
75
76\* Symmetry: combine permutations across Honest, Faulty, V
77CombinePerm(ph, pf, pv) ≜
78 [x ∈ P ∪ V ↦ IF x ∈ Honest THEN ph[x]
79 ELSE IF x ∈ Faulty THEN pf[x]
80 ELSE pv[x]]
81
82Sym ≜ {CombinePerm(ph, pf, pv) :
83 ph ∈ Permutations(Honest),
84 pf ∈ Permutations(Faulty),
85 pv ∈ Permutations(V)}
86
87\* ============================================================================
88\* Protocol State Variables
89\* ============================================================================
90VARIABLES
91 input, \* [Honest -> V]: honest inputs
92
93 \* === Honest party broadcast state ===
94 sent_echo, \* [Honest -> V ∪ {NULL}]: value broadcast by honest party
95 sent_ready, \* [Honest -> VExt ∪ {NULL}]: value broadcast by honest party
96 sent_abort, \* [Honest -> BOOLEAN]: whether honest party sent abort
97
98 \* === Per-sender receive tracking ===
99 rcvd_echo, \* [Honest -> SUBSET (P × V)]: received echoes (only non-NULL)
100 rcvd_ready, \* [Honest -> SUBSET (P × VExt)]: received readies (only non-NULL)
101 rcvd_abort, \* [Honest -> SUBSET P]: senders of ABORT
102
103 delivered \* [Honest -> VExt ∪ {NULL}]: delivered value
104
105send_vars ≜ ⟨sent_echo, sent_ready, sent_abort⟩
106recv_vars ≜ ⟨rcvd_echo, rcvd_ready, rcvd_abort⟩
107vars ≜ ⟨input, sent_echo, sent_ready, sent_abort,
108 rcvd_echo, rcvd_ready, rcvd_abort, delivered⟩
109
110\* ============================================================================
111\* Helper Operators
112\* ============================================================================
113Max(a, b) ≜ IF a ≥ b THEN a ELSE b
114SetMax(S) ≜ IF S = {} THEN 0 ELSE CHOOSE x ∈ S : ∀ y ∈ S : x ≥ y
115
116\* Get echo value from sender s at process p (NULL if not received)
117GetEcho(p, s) ≜ IF ∃ v ∈ V : ⟨s, v⟩ ∈ rcvd_echo[p]
118 THEN CHOOSE v ∈ V : ⟨s, v⟩ ∈ rcvd_echo[p]
119 ELSE NULL
120
121\* Get ready value from sender s at process p (NULL if not received)
122GetReady(p, s) ≜ IF ∃ w ∈ VExt : ⟨s, w⟩ ∈ rcvd_ready[p]
123 THEN CHOOSE w ∈ VExt : ⟨s, w⟩ ∈ rcvd_ready[p]
124 ELSE NULL
125
126\* Who has sent us an echo?
127EchoSenders(p) ≜ {s ∈ P : ∃ v ∈ V : ⟨s, v⟩ ∈ rcvd_echo[p]}
128
129\* Who has sent us a ready?
130ReadySenders(p) ≜ {s ∈ P : ∃ w ∈ VExt : ⟨s, w⟩ ∈ rcvd_ready[p]}
131
132\* Counts derived from set cardinalities
133EchoCount(p, v) ≜ Cardinality({s ∈ P : ⟨s, v⟩ ∈ rcvd_echo[p]})
134ReadyCount(p, w) ≜ Cardinality({s ∈ P : ⟨s, w⟩ ∈ rcvd_ready[p]})
135AbortCount(p) ≜ Cardinality(rcvd_abort[p])
136TotalEchos(p) ≜ Cardinality(EchoSenders(p))
137TotalReadys(p) ≜ Cardinality(ReadySenders(p))
138MaxEchoCount(p) ≜ SetMax({EchoCount(p, v) : v ∈ V})
139MaxReadyCount(p) ≜ SetMax({ReadyCount(p, v) : v ∈ V})
140
141\* ============================================================================
142\* Threshold Predicates
143\* ============================================================================
144\* [RCAST-ECHO-QUORUM]
145EchoQuorum(p, t) ≜ {v ∈ V : EchoCount(p, v) ≥ t}
146
147\* [RCAST-READY-QUORUM]
148ReadyQuorum(p, t) ≜ {v ∈ V : ReadyCount(p, v) ≥ t}
149
150\* [RCAST-BOT-QUORUM]
151HasReadyBottomQuorum(p, t) ≜ ReadyCount(p, Bottom) ≥ t
152
153\* [RCAST-PLURALITY]
154\* Unique max or ⊥ if tied
155PluralityAmongReceived(p) ≜
156 LET maxCnt ≜ MaxEchoCount(p)
157 winners ≜ {v ∈ V : EchoCount(p, v) = maxCnt}
158 IN IF Cardinality(winners) = 1 ∧ maxCnt > 0
159 THEN CHOOSE v ∈ winners : TRUE
160 ELSE Bottom
161
162\* [RCAST-CAN-REACH-QUORUM]
163\* Can any value still reach quorum?
164CanReachQuorum(p) ≜
165 LET remaining ≜ N - TotalReadys(p)
166 IN MaxReadyCount(p) + remaining ≥ Q
167
168\* [RCAST-CAN-WIN]
169\* Can w still hit quorum? (TRUE if w = NULL since question is N/A)
170CanWin(p, w) ≜
171 IF w = NULL THEN TRUE
172 ELSE LET remaining ≜ N - TotalReadys(p)
173 IN ReadyCount(p, w) + remaining ≥ Q
174
175\* [RCAST-ECHO-BACKING]
176HasEchoBacking(p, v) ≜ EchoCount(p, v) ≥ Qe
177
178\* [RCAST-CAN-REACH-ECHO-BACKING]
179\* Discount up to f missing senders (Byzantine may omit forever)
180HonestEchoSenders(p) ≜ Cardinality({h ∈ Honest : ∃ v ∈ V : ⟨h, v⟩ ∈ rcvd_echo[p]})
181
182CanReachEchoBacking(p) ≜
183 LET honestRemaining ≜ Cardinality(Honest) - HonestEchoSenders(p)
184 IN MaxEchoCount(p) + honestRemaining ≥ Qe
185
186\* ============================================================================
187\* Byzantine Nondeterminism Reduction
188\* ============================================================================
189(*
190 Limit Byzantine to "interesting" values that could affect outcome.
191 Sound because unknown values can't reach thresholds (honest won't echo/ready).
192 *)
193
194\* Values that are "in play" at process p
195InterestingEchoValues(p) ≜
196 {input[h] : h ∈ Honest} \* Honest inputs
197 ∪ {v ∈ V : EchoCount(p, v) > 0} \* Already seen echoes
198
199InterestingReadyValues(p) ≜
200 {input[h] : h ∈ Honest} \* Honest inputs
201 ∪ {v ∈ V : EchoCount(p, v) > 0} \* Echoed values
202 ∪ {v ∈ V : ReadyCount(p, v) > 0} \* Already seen readies
203
204\* ============================================================================
205\* Type Invariant
206\* ============================================================================
207TypeOK ≜
208 ∧ input ∈ [Honest → V]
209 \* Honest broadcast state
210 ∧ sent_echo ∈ [Honest → V ∪ {NULL}]
211 ∧ sent_ready ∈ [Honest → VExt ∪ {NULL}]
212 ∧ sent_abort ∈ [Honest → BOOLEAN]
213 \* Per-sender receive tracking
214 ∧ rcvd_echo ∈ [Honest → SUBSET (P × V)]
215 ∧ rcvd_ready ∈ [Honest → SUBSET (P × VExt)]
216 ∧ rcvd_abort ∈ [Honest → SUBSET P]
217 ∧ delivered ∈ [Honest → VExt ∪ {NULL}]
218
219\* ============================================================================
220\* Protocol Initialization
221\* ============================================================================
222Init ≜
223 ∧ input ∈ [Honest → V]
224 \* Honest broadcast state
225 ∧ sent_echo = [h ∈ Honest ↦ NULL]
226 ∧ sent_ready = [h ∈ Honest ↦ NULL]
227 ∧ sent_abort = [h ∈ Honest ↦ FALSE]
228 \* Per-sender receive tracking
229 ∧ rcvd_echo = [p ∈ Honest ↦ {}]
230 ∧ rcvd_ready = [p ∈ Honest ↦ {}]
231 ∧ rcvd_abort = [p ∈ Honest ↦ {}]
232 ∧ delivered = [p ∈ Honest ↦ NULL]
233
234\* ============================================================================
235\* Message Reception
236\* ============================================================================
237(*
238 Byzantine equivocation: faulty senders send different values to different
239 recipients. Modeled via nondeterministic receive from faulty, constrained
240 by at-most-once per (src, dst). Honest senders broadcast uniformly.
241 *)
242
243\* Receive ECHO from an honest sender (must match what they broadcast)
244ReceiveEchoFromHonest(p, h) ≜
245 ∧ delivered[p] = NULL
246 ∧ h ∈ Honest
247 ∧ ¬∃ v ∈ V : ⟨h, v⟩ ∈ rcvd_echo[p]
248 ∧ sent_echo[h] ≠ NULL
249 ∧ rcvd_echo' = [rcvd_echo EXCEPT ![p] = @ ∪ {⟨h, sent_echo[h]⟩}]
250 ∧ UNCHANGED ⟨input, send_vars, rcvd_ready, rcvd_abort, delivered⟩
251
252\* Receive ECHO from a faulty sender (limited to interesting values)
253ReceiveEchoFromFaulty(p, f) ≜
254 ∧ delivered[p] = NULL
255 ∧ f ∈ Faulty
256 ∧ ¬∃ v ∈ V : ⟨f, v⟩ ∈ rcvd_echo[p]
257 ∧ ∃ v ∈ InterestingEchoValues(p) :
258 rcvd_echo' = [rcvd_echo EXCEPT ![p] = @ ∪ {⟨f, v⟩}]
259 ∧ UNCHANGED ⟨input, send_vars, rcvd_ready, rcvd_abort, delivered⟩
260
261ReceiveEcho(p) ≜
262 ∨ ∃ h ∈ Honest : ReceiveEchoFromHonest(p, h)
263 ∨ ∃ f ∈ Faulty : ReceiveEchoFromFaulty(p, f)
264
265\* Receive READY from an honest sender (value or ⊥)
266ReceiveReadyFromHonest(p, h) ≜
267 ∧ delivered[p] = NULL
268 ∧ h ∈ Honest
269 ∧ ¬∃ w ∈ VExt : ⟨h, w⟩ ∈ rcvd_ready[p]
270 ∧ sent_ready[h] ≠ NULL
271 ∧ rcvd_ready' = [rcvd_ready EXCEPT ![p] = @ ∪ {⟨h, sent_ready[h]⟩}]
272 ∧ UNCHANGED ⟨input, send_vars, rcvd_echo, rcvd_abort, delivered⟩
273
274\* Receive READY(v) from a faulty sender (limited to interesting values)
275ReceiveReadyValueFromFaulty(p, f) ≜
276 ∧ delivered[p] = NULL
277 ∧ f ∈ Faulty
278 ∧ ¬∃ w ∈ VExt : ⟨f, w⟩ ∈ rcvd_ready[p]
279 ∧ ∃ v ∈ InterestingReadyValues(p) :
280 rcvd_ready' = [rcvd_ready EXCEPT ![p] = @ ∪ {⟨f, v⟩}]
281 ∧ UNCHANGED ⟨input, send_vars, rcvd_echo, rcvd_abort, delivered⟩
282
283\* Receive READY(⊥) from a faulty sender
284ReceiveReadyBottomFromFaulty(p, f) ≜
285 ∧ delivered[p] = NULL
286 ∧ f ∈ Faulty
287 ∧ ¬∃ w ∈ VExt : ⟨f, w⟩ ∈ rcvd_ready[p]
288 ∧ rcvd_ready' = [rcvd_ready EXCEPT ![p] = @ ∪ {⟨f, Bottom⟩}]
289 ∧ UNCHANGED ⟨input, send_vars, rcvd_echo, rcvd_abort, delivered⟩
290
291ReceiveReady(p) ≜
292 ∨ ∃ h ∈ Honest : ReceiveReadyFromHonest(p, h)
293 ∨ ∃ f ∈ Faulty : ReceiveReadyValueFromFaulty(p, f)
294 ∨ ∃ f ∈ Faulty : ReceiveReadyBottomFromFaulty(p, f)
295
296\* Receive ABORT from an honest sender
297ReceiveAbortFromHonest(p, h) ≜
298 ∧ delivered[p] = NULL
299 ∧ h ∈ Honest
300 ∧ h ∉ rcvd_abort[p]
301 ∧ sent_abort[h] = TRUE
302 ∧ rcvd_abort' = [rcvd_abort EXCEPT ![p] = @ ∪ {h}]
303 ∧ UNCHANGED ⟨input, send_vars, rcvd_echo, rcvd_ready, delivered⟩
304
305\* Receive ABORT from a faulty sender (at any time)
306ReceiveAbortFromFaulty(p, f) ≜
307 ∧ delivered[p] = NULL
308 ∧ f ∈ Faulty
309 ∧ f ∉ rcvd_abort[p]
310 ∧ rcvd_abort' = [rcvd_abort EXCEPT ![p] = @ ∪ {f}]
311 ∧ UNCHANGED ⟨input, send_vars, rcvd_echo, rcvd_ready, delivered⟩
312
313ReceiveAbort(p) ≜
314 ∨ ∃ h ∈ Honest : ReceiveAbortFromHonest(p, h)
315 ∨ ∃ f ∈ Faulty : ReceiveAbortFromFaulty(p, f)
316
317Receive(p) ≜
318 ∨ ReceiveEcho(p)
319 ∨ ReceiveReady(p)
320 ∨ ReceiveAbort(p)
321
322\* ============================================================================
323\* Honest Party Actions
324\* ============================================================================
325
326\* E1: [RCAST-SEND-ECHO]
327\* Upon start: broadcast ECHO(input)
328SendEcho(self) ≜
329 ∧ sent_echo[self] = NULL
330 ∧ delivered[self] = NULL
331 ∧ LET v ≜ input[self]
332 IN sent_echo' = [sent_echo EXCEPT ![self] = v]
333 ∧ UNCHANGED ⟨input, sent_ready, sent_abort, recv_vars, delivered⟩
334
335\* R1: [RCAST-READY-ON-ECHO-QUORUM]
336\* Upon receiving Q echoes for value v: broadcast READY(v)
337ReadyOnEchoQuorum(self) ≜
338 ∧ sent_ready[self] = NULL
339 ∧ delivered[self] = NULL
340 ∧ ∃ v ∈ EchoQuorum(self, Q) :
341 sent_ready' = [sent_ready EXCEPT ![self] = v]
342 ∧ UNCHANGED ⟨input, sent_echo, sent_abort, recv_vars, delivered⟩
343
344\* R2: [RCAST-READY-ON-TIMEOUT]
345\* Upon timeout with Q total echoes but n