Quantum Cadence: Post-Quantum Consensus with Multiple Concurrent Proposers

Quantum Cadence: Post-Quantum Consensus with Multiple Concurrent Proposers Mohammad Mussadiq Jalalzai , Tobias Klenze , and Jovan Komatovic

⋆

arXiv:2610.32803v1 [cs.DC] 23 Oct 2026

Category Labs

Abstract. The consensus protocols of most high-performance blockchains use quorum certificates, which bundle the signatures of a quorum of validators. Signature schemes such as BLS can aggregate the signatures of a whole quorum into a single short signature, which keeps these certificates small. A large-scale quantum computer would break these schemes, and no post-quantum scheme with comparable aggregate size and aggregation time is known. Without aggregation, a certificate holds one large post-quantum signature per member of the quorum, so it becomes infeasible for each validator to broadcast certificates, as modern consensus protocols often require. We present Quantum Cadence, a post-quantum consensus protocol with multiple concurrent proposers that avoids certificates altogether: every validator counts quorums among the messages it has received itself. Its safety and liveness do not even depend on signatures, although we add signatures to obtain accountability. Quantum Cadence builds on Cadence and replaces its slot consensus, Chorus, with Quantum Chorus, which keeps the optimal fast-path latency of Chorus: dissemination followed by two rounds of votes. When its fast path fails, Quantum Chorus runs Coda, our signature-free Byzantine agreement for multiple proposers. We also outline how the Conductor, which schedules the slots of Cadence, can be adapted to Quantum Cadence. In simulations with 200 validators, Quantum Chorus has a latency comparable to that of Chorus and scales better with the number of proposers.

1

Introduction

Large-scale quantum computers would break the signature schemes that blockchains use today. Several parts of a blockchain rely on these signatures, from the transactions that users sign to the votes that validators exchange in the consensus protocol. This paper is about consensus: we present Quantum Cadence, a post-quantum version of Cadence [4], a consensus protocol with multiple concurrent proposers. Cadence divides time into slots and finalizes one block per slot, which merges the proposals that several proposers disseminate for that slot. Each slot is finalized by its own instance of a single-shot consensus protocol, which Cadence calls the slot consensus and instantiates with Chorus. Because blocks do not build on their predecessors, these instances run independently, and many slots can be in progress at once. Cadence calls this extreme pipelining: no slot waits for the block of an earlier slot, so blocks can follow one another at intervals shorter than the network delay. A second protocol, the Conductor, schedules the slots, at a regular interval in normal operation and more slowly under asynchrony, so that the number of open slots stays bounded. In the common case, Chorus finalizes a slot on its fast path in three communication rounds, and a fallback path takes over when the fast path cannot finish. Besides safety and liveness, Cadence provides short-term censorship resistance: shortly after the network becomes synchronous, the block of every slot contains the proposal of every correct proposer. Many messages of Chorus carry quorum certificates, most of them made of signatures from 2f + 1 of the n = 3f + 1 validators, of which at most f are faulty. In Chorus, these signatures are combined into one compact aggregate signature that anyone can verify, with a pairing-based scheme such as BLS [7], which a quantum computer would break. Moving to post-quantum signatures changes two things. Each post-quantum signature is at least several times larger than a traditional one, and the post-quantum aggregation schemes known today produce aggregates that are orders of magnitude larger than a BLS aggregate signature and take far longer to compute. Without aggregation, a certificate is a list of 2f + 1 of these larger signatures, whose size grows with the number of validators. If every validator broadcast even one such certificate per slot, the transmission delays alone would be unacceptable at the bandwidth available to validators, and Chorus sends certificates for every proposer. Quantum Cadence therefore keeps the structure of Cadence, one instance of the slot consensus per slot under the Conductor, but does without certificates: no validator ever has to prove a quorum ⋆

Author order: alphabetical by last name.

2

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

to another, as each validator observes quorums in the messages it receives itself. Simply removing the certificates from Chorus does not work, because several of its parts rely on them. Our slot consensus, Quantum Chorus, changes these parts. Its fast path keeps the structure of Chorus, dissemination followed by two voting rounds, but no vote carries a certificate. Its fallback path is new: Chorus ends its fallback path with an agreement that accepts only certified inputs, and Quantum Chorus replaces it by Coda, a signature-free Byzantine agreement based on Forget-IT [1]. Quantum Chorus goes further than removing certificates: it needs no signatures for safety and liveness, which rest only on authenticated channels and collision-resistant hashing. We add post-quantum signatures to obtain accountability: validators sign their messages, so the correct validators can prove to anyone that a validator misbehaved. Proofs of finality for parties outside consensus, such as light clients and bridges, are outside the scope of this paper; certificates of ordinary post-quantum signatures can serve them, since such a certificate need not be broadcast by every validator. The Conductor needs changes too. Cadence proves the guarantees of the Conductor with the help of certificates: a correct validator that finishes a slot forwards its certificate, so the others finish within one message delay. The Conductor also relies on an agreement among the validators, which has to be made post-quantum as well. We outline how the Conductor can work without certificates and with a signature-free agreement, and leave its full specification and analysis to a later version. The fast path of Quantum Chorus keeps the optimal latency of Chorus [4]: correct validators finalize in three communication rounds, dissemination included, and reach speculative finality one round earlier, even when some proposers are offline. Even without certificates, post-quantum signatures are large enough that their number matters, and Quantum Chorus is designed to keep the number of signatures small: in each slot, a validator signs at most two votes, each covering all proposers, and Coda uses no signatures at all. In Chorus, by contrast, a validator signs its vote on each proposer separately, so its number of signatures grows with the number of proposers. We evaluate Quantum Chorus against Chorus in simulation, for 200 validators with 1 Gbps links: its latency is comparable to that of Chorus, and it scales better with the number of proposers. With 20 proposers, a validator finalizes a slot on average about 200 ms after a proposer’s broadcast, and reaches speculative finality about 50 ms earlier. After recalling Cadence and Chorus in Section 2, we turn to the core of the paper: Quantum Chorus, which Section 4 describes step by step together with its guarantees, and its fallback consensus, Coda, presented in Section 5. We then outline how the slot consensus runs within the Conductor in Section 6, evaluate the cost of Quantum Chorus in Section 7, and discuss related work in Section 8; the proofs are in Appendices A and B.

2

Background: Cadence and Chorus

Cadence [4] runs among n = 3f + 1 validators, at most f of which are Byzantine, over a partially synchronous network: after an unknown global stabilization time (GST), every message between correct validators arrives within a known bound ∆. The validators have synchronized clocks, which Cadence uses to schedule the slots: the Conductor gives each slot a deadline, the time at which validators vote on the proposals they have received, and each slot then finalizes one block in its own single-shot instance of Chorus. In the rest of this section, we describe Chorus for a single slot, whose deadline we denote by D. If the slot’s starting time D − ∆ is at least GST + G, for a grace period G, the Conductor ensures that every correct validator starts participating by D − ∆. For an earlier slot, a validator may learn the deadline only after it has passed, and it then starts participating and votes at once. Each slot has a fixed set of proposers. A proposer erasure-codes its proposal into n chunks, any f + 1 of which suffice to decode it, commits to the chunks with a Merkle root, and sends each validator its chunk, together with a Merkle proof under the root and the proposer’s signature on the root. (In Chorus, proposals are also encrypted before encoding and can be decrypted no earlier than the deadline. This provides hiding, a property that fairness between proposers requires: no proposer can craft its proposal in reaction to the others’. We leave this step out, as this paper does not address hiding.) A correct proposer does so when it starts participating, so in a slot whose starting time is at least GST + G, the chunks of correct proposers arrive by the deadline. At D, each validator votes once per proposer: for the Merkle root of the proposer’s chunk, with the chunk attached, if it holds a valid one, and for the empty value ⊥ otherwise. A validator that holds a valid chunk from every proposer before D may cast its votes right away instead (early voting). Chorus agrees on one entry per proposer: either the Merkle root of the proposer’s proposal, which selects the proposal for the slot’s block, or ⊥, which excludes the proposer. The block consists of the selected proposals, except any whose chunks turn out not to be a valid encoding. Every correct validator

3. MODEL

3

can recover the proposals of every block that Chorus finalizes (data availability). Validators exchange entries in meta-blocks, vectors with one entry per proposer, in which every entry carries a certificate that justifies it. In the common case, the certificate is a FastQC: a quorum certificate formed from 2f + 1 matching votes, all for the same root or all for ⊥, which Chorus implements as a compact aggregate signature. A validator that holds a FastQC for every proposer assembles the fast meta-block and broadcasts a fast vote on it, together with the meta-block, and it finalizes the entries once it receives 2f + 1 fast votes on the same entries. This is the fast path, three communication rounds in all: dissemination and two rounds of votes. A validator may also speculatively finalize one round earlier, that is, treat the fast meta-block as final as soon as it assembles it; this speculation is reverted only if some validator equivocated. If the fast path does not finish, for instance because a proposal reached only some correct validators by the deadline, the fallback path takes over. From time D + ∆ on, a validator that holds 2f + 1 votes but cannot assemble a fast meta-block announces that it casts no fast vote and casts a second round of perproposer votes, after which the validators run a multi-valued validated Byzantine agreement (MVBA). Each validator proposes a fast meta-block if it has assembled one or received one with a fast vote, and otherwise a fallback meta-block. A fallback meta-block carries 2f + 1 announcements that no fast vote was cast, and it certifies each entry in one of three ways: with a FastQC, with f + 1 matching votes of the second round, or, for ⊥, with two different roots signed by the proposer, which prove that it equivocated. The external validity of the MVBA admits only such certified meta-blocks, so each validator can check a proposed meta-block on its own. Once the MVBA decides, validators cast commit votes on the decided meta-block, and a validator finalizes the slot once it holds 2f + 1 of these votes. Chorus guarantees proposal inclusion: in a slot whose starting time is at least GST + G, the block contains the proposal of every correct proposer. This gives Cadence its short-term censorship resistance: a transaction that a correct proposer includes in its proposal enters the block of that slot, so it is neither censored nor deferred to a later block. Quantum Chorus keeps this property, as well as agreement, termination, and speculative finality.

3

Model

We consider n = 3f + 1 validators, at most f of which are Byzantine and may deviate arbitrarily from the protocol; the others are correct. Validators communicate over point-to-point authenticated channels: the recipient of a message can tell who sent it. Reliability, however, is not assumed. A broadcast unicasts its message to every validator and retransmits it, again and again, until the broadcast is explicitly abandoned ; a point-to-point send retransmits to its recipient in the same way. A message is alive at time τ if its broadcast or point-to-point send has been initiated, but not abandoned, by time τ , and forever-alive if, once initiated, it is never abandoned. A forever-alive message of a correct validator is eventually received by every correct recipient, including after the recipient recovers from a crash or starts participating. We use this model throughout the paper. It is similar to the model of Forget-IT [1], which, however, communicates by broadcasts only. Bounding memory is meaningful only with unreliable channels: with reliable channels, undelivered messages must be buffered until delivery, as Cadence observes while retaining reliable channels [4]. With signatures and certificates, bounded memory is well understood; without them, it is not obvious, which motivates our model and the persistent-memory bound for Coda (Section 5). Crashes and persistent memory. Beyond corrupting validators, the adversary may temporarily crash a correct validator, which eventually recovers. A crash strikes only between handler executions. It leaves the validator’s persistent memory intact, timers included, and wipes the rest of its state, notably the received messages that it has not stored in persistent memory. Upon recovering, the validator resumes execution from its persistent memory. We assume that a crash does not abandon the validator’s ongoing broadcasts: their retransmission resumes upon recovery. This assumption costs no generality, as every message a validator broadcasts is recorded in its persistent memory, so that a recovery procedure could simply re-initiate their broadcasts. Partial synchrony and clocks. We adopt the standard partially synchronous model: an unknown Global Stabilization Time (GST) splits the execution into an asynchronous period and a synchronous one. After GST, message delays are bounded by the known ∆: for every time τ , a message of a correct validator that remains alive throughout [τ, max(τ, GST) + ∆] is received by every correct recipient during [max(τ, GST), max(τ, GST)+∆]. This applies to broadcasts and point-to-point sends, including messages

4

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

received and lost before τ . Since a message sent before GST may be lost, ∆ also covers the wait for its next retransmission. The adversary crashes correct validators only before GST, and every crashed validator recovers before GST, so that all correct validators are continuously online from GST onward. Local computation is instantaneous, and each validator executes only finitely many handlers in any finite time interval. As in Cadence, validators have synchronized clocks. Cryptography. We use a collision-resistant hash function. Every validator holds a key pair of a postquantum signature scheme. The protocol needs signatures only for accountability, that is, to prove misbehavior, as the accountability lemmas and the speculation lemma do (Lemmas 2, 7 and 8). Agreement, proposal inclusion, termination, and halting rest on the authenticated channels and on the hash function. Slots. Each slot of Quantum Cadence has a deadline D, and we call D − ∆ the slot’s starting time. A validator participates in a slot from the time it starts running the slot consensus for that slot, a time that the Conductor determines (Section 6). We call a slot timely if its starting time D − ∆ is at least GST and every correct validator starts participating in it by D − ∆. In Cadence, the Conductor ensures that every slot whose starting time is at least GST + G is timely, where the grace period G is the time the Conductor needs to settle after GST (Section 2). We expect the Conductor of Quantum Cadence to do the same (Section 6).

4

Quantum Chorus: The Slot Consensus of Quantum Cadence

Quantum Chorus takes the place of Chorus: in every slot, it finalizes one block. Like Chorus, it agrees on one entry per proposer, a Merkle root or a value that excludes the proposer, but its metablocks carry no certificates: a meta-block is just a vector with one entry per proposer. Validators agree on a meta-block, and finalizing a meta-block finalizes the slot’s block, which consists of the proposals behind its roots. For every finalized block, these proposals can be recovered. Here, we first describe the protocol and present its pseudocode. Then, we state its guarantees. 4.1

Protocol Description

Setting. Quantum Chorus runs in the model of Section 3. Some of the validators are proposers, each of which disseminates one proposal in the slot we describe. Proposals are encoded with an erasure code, any f + 1 of whose n symbols suffice to decode, and committed to with Merkle trees over the hash function. Conventions. Every rule fires as soon as its condition holds, and a handler runs to completion before the next one starts. Time guards remain enabled after their deadline. Algorithm 1 never abandons a broadcast or a point-to-point send, also not when the validator halts, so all its messages are foreveralive.1 A validator keeps no message of the slot that arrives before it starts participating: retransmission delivers the message again once it participates (Section 3). Every message, and every tuple that a validator signs, also contains the slot number, which we omit from the notation. Throughout the paper, “f + 1 messages” means messages from f + 1 different validators, and likewise for other counts. The steps. We now describe the protocol step by step. Figure 1 gives a bird’s-eye view, simplified for a single proposer, and Algorithm 1 gives the pseudocode for a validator pi . Steps 1 to 3 (dissemination, a vote at the deadline, and a path vote) serve both paths. The fast path ends after them: a validator finalizes once, for every proposer, 2f + 1 path votes (defined in Step 3) carry matching fast entries. The fallback path continues with Steps 4 to 6 and ends in Coda. Step 1: Dissemination (∆ time before the deadline). Dissemination proceeds exactly as in Chorus. Each proposer pj encodes its proposal into n erasure-coded symbols and builds a Merkle tree over them, with root ρj . It then sends to each validator pi the i-th symbol, pi ’s assigned chunk, together with the Merkle proof of the chunk’s inclusion under ρj and the header ⟨j, ρj ⟩ signed by pj (line 36). 1

In Quantum Cadence, we expect the Conductor to keep the number of open slots bounded, as in Cadence, and to end the broadcasts of slots that no correct validator needs any more (Section 6).

4. QUANTUM CHORUS: THE SLOT CONSENSUS OF QUANTUM CADENCE

5

Algorithm 1 Quantum Chorus: Pseudocode (for validator pi ) 1: Notation: 2: - Entries for a proposer pj are positive, ⟨j, ρ⟩, or negative, ⟨j, ⊥⟩. 3: Local variables (persistent memory): 4: chunk i [j] ← none for every proposer pj ▷ pi ’s validated chunk of pj ’s proposal, together with its root ρj 5: entry i [j] ← none for every proposer pj ▷ pi ’s path-vote entry: ⟨fast, v⟩ or ⟨fallback, v⟩ 6: adopted i [j] ← none for every proposer pj ▷ value adopted for the fallback consensus 7: finalized i ← false ▷ whether pi has finalized (set by finalize) 8: Messages sent, halt status, and completion of once-only steps 9: Received Finalized messages (at most one per validator) 10: votes i ← ∅ ▷ received valid Vote messages 11: pathVotes i ← ∅ ▷ received PathVote messages 12: Rules: 13: - Persist all received messages of this algorithm; halting does not abandon broadcasts. 14: - A received ⟨Chunk, ρ, d, π, σ⟩ from a proposer pj is valid only if σ is a valid signature of pj on ⟨j, ρ⟩ and π proves that d is the i-th symbol under ρ. 15: - A received ⟨Vote, E, C, σ⟩ from pr is added to votes i only if σ is a valid signature of pr on E, E holds an entry ⟨j, ·⟩ for every proposer pj , and C holds, for every positive entry ⟨j, ρ⟩, pr ’s symbol with a valid Merkle proof under ρ. 16: - A received ⟨PathVote, F, σ⟩ from pr is added to pathVotes i only if σ is a valid signature of pr on F . 17: - At most one Vote from each validator is added to votes i , and at most one PathVote to pathVotes i . 18: - A path-vote entry ⟨fallback, ·⟩ for pj is accepted upon receipt. An entry ⟨fast, ρ⟩ for pj is accepted as soon as votes i holds f + 1 positive entries ⟨j, ρ⟩; an entry ⟨fast, ⊥⟩ once votes i holds f + 1 negative entries for pj . 19: Functions: 20: - clean(j): ▷ Step 4: a clean set for proposer pj , or none 21: return the first set S obtained by pi of 2f + 1 accepted entries for pj , from different validators, such that all fast entries in S carry the same value; none if no such set exists 22: - adopt(S): ▷ Step 5: the adoption rule, reading a clean set S 23: if S holds an entry ⟨fast, ⊥⟩: return ⊥ ▷ unambiguous: all fast entries in S agree 24: else if S holds an entry ⟨fast, ρ⟩: 25: Decode the proposal from the f + 1 chunks that corroborated the entry, and re-encode it 26: if the recomputed root equals ρ: return ρ 27: else return ⊥ ▷ invalid encoding: the proposal is excluded 28: else if S holds f + 1 entries ⟨fallback, ρ⟩ for the same ρ: return ρ 29: else return ⊥ 30: upon starting: ▷ Step 1: dissemination at time D − ∆ 31: if pi is a proposer: 32: Encode the proposal into n erasure-coded symbols d1 , . . . , dn 33: Build a Merkle tree over d1 , . . . , dn with root ρi 34: σi ← Signi (⟨i, ρi ⟩) ▷ signed header: binds the root to the proposer 35: for each validator pr : 36: send ⟨Chunk, ρi , dr , πr , σi ⟩ to pr ▷ πr : Merkle proof of dr 37: upon receipt of a valid ⟨Chunk, ρ, d, π, σ⟩ from a proposer pj and chunk i [j] = none and time has not passed D: 38: chunk i [j] ← ⟨ρ, d, π, σ⟩ 39: upon time reaches D or chunk i [j] ̸= none for every proposer pj : ▷ Step 2: deadline vote at time D or earlier (runs once) 40: for each proposer pj : 41: if chunk i [j] ̸= none: Ej ← ⟨j, ρj ⟩ ▷ positive entry 42: else Ej ← ⟨j, ⊥⟩ ▷ negative entry: no valid chunk by the deadline 43: E ← (Ej )proposer pj 44: C ← {⟨ρ, d, π⟩ from chunk i [j] : Ej is positive} ▷ no signed headers 45: σi ← Signi (E) ▷ one signature over the whole entry vector 46: broadcast ⟨Vote, E, C, σi ⟩ 47: upon time reaches D + ∆ and |votes i | ≥ 2f + 1, or for every proposer pj , votes i holds 2f + 1 entries for pj that name the same value: ▷ Step 3: path vote (runs once) 48: for each proposer pj : 49: if votes i holds 2f + 1 positive entries ⟨j, ρ⟩ for the same Merkle root ρ: entry i [j] ← ⟨fast, ρ⟩ 50: else if votes i holds 2f + 1 negative entries for pj : entry i [j] ← ⟨fast, ⊥⟩ 51: else if votes i holds f + 1 positive entries ⟨j, ρ⟩ for some Merkle root ρ: 52: Decode the proposal from the chunks attached to these entries, and re-encode it 53: if the recomputed root equals ρ: entry i [j] ← ⟨fallback, ρ⟩ 54: else entry i [j] ← ⟨fallback, ⊥⟩ 55: else entry i [j] ← ⟨fallback, ⊥⟩ 56: F ← (entry i [j])proposer pj 57: σi ← Signi (F ) ▷ one signature over the whole path vote 58: broadcast ⟨PathVote, F, σi ⟩ 59: if every entry of F is fast, with entry i [j] = ⟨fast, vj ⟩ for every proposer pj , and ¬finalized i : 60: for each pj whose vj is a root: re-encode the proposal decoded from f + 1 chunks under vj 61: if the root differs: vj ← ⊥ 62: speculatively finalize the meta-block (vj )proposer pj 63: upon for every proposer pj , pathVotes i holds 2f + 1 messages whose entry for pj is ⟨fast, vj ⟩ for the same vj , and, for every pj whose vj is a root, votes i holds f + 1 positive entries ⟨j, vj ⟩: ▷ fast path (at any time) 64: for each pj whose vj is a root: decode the proposal from these chunks and re-encode it; if the root differs: vj ← ⊥
65: finalize the meta-block x = (vj )proposer pj and broadcast ⟨Finalized, x⟩, unless already finalized 66: 67: 68: 69: 70: 71: 72: 73: 74: 75: 76: 77:

upon time reaches D + 2∆ and clean(j) ̸= none for every proposer pj : for each proposer pj : adopted i [j] ← adopt(clean(j)) a ← (adopted i [j])proposer pj input a to the fallback consensus upon the fallback consensus outputs x: x[j] ← ⊥ for every proposer pj with x[j] = empty finalize the meta-block x and broadcast ⟨Finalized, x⟩, unless already finalized upon receipt of ⟨Finalized, x⟩ from f + 1 validators, for the same x: finalize the meta-block x and broadcast ⟨Finalized, x⟩, unless already finalized upon receipt of ⟨Finalized, x⟩ from 2f + 1 validators, for the same x: finalize the meta-block x and broadcast ⟨Finalized, x⟩, unless already finalized; halt

▷ Step 5: adoption (runs once)

▷ Step 6 ▷ x[j] = ⊥ excludes pj

6

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic 1. Disseminate one chunk per validator, with root ρj and Merkle proof

2. Vote at the deadline

3. Path vote after 2f +1 Votes

Fast path (any time)

valid chunk ⇒ positive ρj , chunk attached

2f +1 matching ⇒ fast entry ρj /⊥

2f +1 matching fast entries ⇒ finalize ρj /⊥

no valid chunk ⇒ negative ⊥ broadcast in a Vote fast path decode

fallback path

both paths

may rebuild a proposal from f +1 chunks and check its encoding; if invalid, replace its root by ⊥

decode

else, after D+∆ decode

f +1 positive for ρj ⇒ fallback entry ρj else fallback entry ⊥ broadcast in a PathVote

4–6. Fallback decode

clean set: 2f +1 accepted entries, fast ones agree ⇒ adopt ρj /⊥

decode

fast entry ⇒ speculatively finalize

input to Coda; output ⇒ finalize time

D−∆

deadline D

D+∆

D + 2∆

Fig. 1: Quantum Chorus, simplified for a single proposer pj . Time flows left to right. In a timely slot (Section 3), a step starts at the latest at the time marked below its box, and in the common case every correct validator finalizes on the fast path by D + 2∆. With several proposers, every vote and path vote carries one entry per proposer, and a validator speculates, finalizes on the fast path, or inputs to Coda only once the condition shown holds for every proposer; a path vote may thus hold a fast entry for one proposer and a fallback entry for another. Crucially, no message ever carries a certificate: every quorum is observed locally, by each validator in the messages it receives. Step 2: Voting (at the deadline). The deadline step, too, mirrors Chorus. When time reaches the deadline D, a correct validator pi forms one entry per proposer: a positive entry ⟨j, ρj ⟩ if a valid chunk of pj ’s proposal has arrived (the chunk assigned to pi , whose Merkle proof verifies against a header signed by pj ), and a negative entry ⟨j, ⊥⟩ otherwise, attesting that nothing arrived on time. It broadcasts the entries in a single Vote message, attaching for every positive entry its assigned chunk, that is, the root, the symbol, and its Merkle proof (line 46). Crucially, the message carries one signature, computed over the entire vector of entries: unlike in Chorus, where each entry is signed on its own, no entry is ever signed individually, and a validator vouches for its whole vote. We also underline that the signed header is not included in the vote. Therefore, a vote contains a single signature. A correct validator that holds a valid chunk from every proposer before the deadline sends this vote right away instead of at the deadline (early voting, as in Cadence). Step 3: Path votes. At the end of the first post-deadline round, namely, once 2f + 1 valid votes have been received and time has reached D + ∆, a correct validator pi examines the received votes and forms, for each proposer pj separately, a path-vote entry, distinguishing three cases. – First, if pi observes 2f + 1 positive entries for pj with the same Merkle root ρj , or 2f + 1 negative entries for pj , its entry is a fast entry, carrying ρj in the former case and ⊥ in the latter (lines 49 and 50). The important difference from Chorus lies in what a fast entry carries. In Chorus, a fast vote comes with its own justification: the FastQC that aggregates the 2f + 1 deadline votes behind it. Here, there is no certificate to attach. A fast entry is only a claim: pi states that it has seen a quorum for pj , and offers no proof. – Second, if no such quorum exists but pi observes f + 1 positive entries for pj with the same root ρj (ties broken arbitrarily), it proceeds as in Chorus: it collects the chunks attached to those entries, decodes the proposal, and re-encodes it. If the recomputed root matches, its entry is a fallback entry for ρj (line 51). – Third, if the reconstruction fails, or if no root gathers even f +1 positive entries, its entry is a fallback entry for ⊥. Having formed all entries, pi broadcasts them in a single PathVote message (line 58). A validator does not wait for D + ∆ if, for every proposer, it already holds 2f + 1 votes whose entries for that proposer name the same value: all its entries are then fast, and waiting cannot change them, since no two values can each be matched by 2f + 1 of at most n votes. From the deadline onward, the fast path thus proceeds at the speed of the network, as in Chorus. As with the deadline vote, the message carries a single signature,

4. QUANTUM CHORUS: THE SLOT CONSENSUS OF QUANTUM CADENCE

7

computed over the entire vector of entries. Finally, pi speculatively finalizes the meta-block formed by its fast entries if and only if every entry of its path vote is fast and it has not finalized yet (line 62), after checking the encodings. A fast entry is formed without decoding and may carry the root of an invalid encoding, so, for every fast entry for a root, pi rebuilds the proposal from the chunks attached to the votes behind the entry and re-encodes it; if the recomputed root differs, it replaces the root by ⊥. A speculatively finalized block can still be reverted, but any reversion leaves behind a proof of misbehavior (Lemma 2). Finalizing on the fast path (at any time). If, at any point in time, a correct validator holds, for every proposer pj , 2f + 1 path votes whose entries for pj are fast entries for the same value vj , a root or ⊥, it finalizes the meta-block (vj )proposer pj (line 65). Before finalizing, it waits until it holds, for every root vj , f +1 Votes positive for vj (the correct validators whose Votes are behind the fast entries have broadcast them), rebuilds the proposal from their chunks, and re-encodes it; if the recomputed root differs from vj , the encoding is invalid, and the validator replaces vj by ⊥. The result of this check does not depend on which chunks are used: a valid encoding decodes to the same proposal from any f + 1 of its symbols, and an invalid one never re-encodes to the root, whichever symbols are used. A correct validator finalizes at most once, and announces its finalization with a Finalized message, which the halting rule below uses. Finalizing does not end its part in the slot: it keeps running the protocol, the fallback consensus included, until it halts. Step 4: Accepting second-round entries. We now turn to the second post-deadline round, the round during which path votes travel, and, from here on, refer to the entries of path votes collectively as second-round entries. The key notion of this step is that of accepting a second-round entry. Crucially, accepting an entry is not the same as receiving the path vote that carries it, and acceptance is decided entry by entry (line 18). – A fallback entry is accepted the moment it is received. – A fast entry, in contrast, must earn its acceptance. Namely, recalling that a fast entry is a bare claim of a quorum, pi accepts one only once it sees the claim corroborated by f + 1 matching deadline entries: a fast entry for a root ρj is accepted once pi has received f + 1 votes with a positive entry ⟨j, ρj ⟩, each carrying its sender’s chunk of the proposal, whereas a fast entry for ⊥ is accepted once pi has received f + 1 votes with a negative entry for pj . The chunks are essential for data availability (as we explain later). A single path vote may therefore contain, at the same time, an accepted entry for one proposer and a not yet accepted entry for another. Now, a clean set for proposer pj is a set of 2f + 1 accepted second-round entries for pj , from different validators, whose fast entries all agree: any two fast entries in the set carry the same root, or both carry ⊥. Fallback entries are left unconstrained. For example, a set of 2f + 1 accepted fallback entries for pj is clean: it holds no fast entries to disagree. Similarly, a set in which five fast entries all carry the same root, and all remaining entries are fallback entries, is clean as well. By contrast, a set holding a fast entry for one root and a fast entry for a different one is not clean, and neither is a set holding a fast entry for some root alongside a fast entry for ⊥. With this notion in hand, the second post-deadline round ends at pi once (1) time has reached D +2∆, and (2) pi holds a clean set for every proposer. We underline that the clean sets of different proposers may come from different validators. Also, several clean sets may exist for one proposer, and they need not agree, so pi reads the first one it obtains (line 21). Step 5: Adopting a meta-block. With the second post-deadline round over, pi adopts a value for every proposer, a Merkle root or ⊥, thereby forming the meta-block it inputs to the fallback path. The adoption rule for proposer pj reads pi ’s clean set for pj (line 68). 1. If the clean set holds a fast entry for ⊥, pi adopts ⊥. If it holds a fast entry for a root ρj , pi does not take the root on faith: it decodes the proposal from the f + 1 chunks that corroborated the entry and re-encodes it, and it adopts ρj if the recomputed root is ρj , and ⊥ otherwise (line 26). (The rule is unambiguous: the set being clean, all fast entries in it agree.) Adopting a root from a fast entry thus rests on a proposal that pi has rebuilt itself. 2. If, instead, the clean set consists of fallback entries alone, pi examines them: if f + 1 of them carry the same root, pi adopts that root, and otherwise it adopts ⊥. It then inputs the adopted meta-block to the fallback consensus (line 70).

8

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

Step 6: The fallback consensus. The fallback path now takes over. In Chorus, the fallback consensus black box is an MVBA, whose external validity admits only certified meta-blocks. Here, we replace it with Byzantine agreement with per-proposer strong unanimity, which Coda implements (Section 5). The primitive takes as input, from each validator, a meta-block: one entry per proposer, each a Merkle root or ⊥. It outputs a meta-block in which an entry may also take the special value empty, the primitive’s own way of outputting nothing for a proposer (note that ⊥ ̸= empty). The primitive satisfies the following four properties: – Agreement: No two correct validators output different meta-blocks. – Termination: If every correct validator inputs, every correct validator eventually outputs. – Strong unanimity (per proposer): If all correct validators that input a meta-block input the same value for proposer pj , a root or ⊥, then no correct validator outputs empty for pj . – Obligation (per proposer): If a correct validator outputs a value v ̸= empty for proposer pj , then some correct validator input v for pj . Agreement, strong unanimity, and obligation hold even if some correct validators stop taking part in the primitive, possibly before inputting, as validators do when they halt (see the paragraph on halting below); termination is required only when no correct validator stops taking part, since once a correct validator halts, the halting gadget makes every correct validator that participates finalize without the fallback consensus. With the primitive in place, the fallback path is simple. Every correct validator inputs its adopted meta-block. Once the primitive outputs a meta-block x, a correct validator replaces every entry empty of x by ⊥ and finalizes the result: a root includes its proposer, whereas ⊥ excludes it (line 73). Inputting the adopted meta-block to the primitive (line 70) and starting the primitive form one handler, and so do an output of the primitive and the finalization it causes (line 73), so that a crash cannot fall between them. On halting. In Chorus, a correct validator halts the moment it finalizes — and it can afford to. Namely, it holds a quorum certificate (an aggregate signature) attesting to its finalization: a self-contained proof it can disseminate reliably, so that it reaches everyone even after the validator halts, to convince everyone else to stop as well. Here, that luxury is gone: there is no aggregate signature to hand out. And simply halting upon finalizing would be dangerous — the protocol could silently lose a quorum of correct validators and, with it, termination for the validators still running. In Quantum Chorus, therefore, a correct validator must not halt upon finalizing. Fortunately, the problem admits an easy fix: a halting gadget, in the style of Bracha’s amplification [8] (lines 74 and 76). – Upon finalizing a value v, a correct validator broadcasts a special message: ⟨Finalized, v⟩. – Upon receiving f + 1 matching Finalized messages, a correct validator finalizes v and broadcasts ⟨Finalized, v⟩ itself, unless it has already finalized. – Upon receiving 2f + 1 matching Finalized messages, a correct validator finalizes v (if it has not already) and halts. The f +1 threshold keeps the echo honest: among f +1 matching messages, at least one comes from a correct validator, so the echoed value is indeed the finalized one. Finalizing at this threshold is therefore safe, and it lets every correct validator that starts participating at time S finalize by time max(S, H, GST)+∆, where H is the time at which the first correct validator halts. The 2f + 1 threshold makes halting safe: among 2f + 1 matching messages, at least f + 1 come from correct validators, whose echoes eventually push every correct validator over the 2f + 1 bar: no correct validator halts alone. Halting also has a constant bound: if every correct validator starts participating by time T , every correct validator halts by time max(T, H, GST) + 2∆, since it finalizes by time max(T, H, GST) + ∆ and then halts within ∆ (Lemma 5). The Finalized messages of correct validators match, since all correct validators finalize the same meta-block. Until it halts, a correct validator keeps taking part in the fallback consensus, even after finalizing on the fast path. A validator that has halted handles no more messages of the slot, including those of the fallback consensus, but its ongoing broadcasts remain alive and keep retransmitting. In this version, these broadcasts never end. We expect the protocol that schedules the slots (in Quantum Cadence, the Conductor) to end them once it has moved far enough ahead that no correct validator needs the slot’s messages any more (Section 6). A correct validator that finalizes through the halting gadget finalizes a meta-block that some correct validator finalized on the fast path or on the fallback path: the first correct validator to broadcast ⟨Finalized, x⟩ did so upon finalizing x on one of the two paths, since finalizing through the gadget requires f + 1 Finalized messages for x, one of them from a correct validator that broadcast earlier. This replaces the commitment certificates of Chorus: instead of receiving a transferable certificate from another validator, each validator observes a quorum of matching Finalized messages itself.

4. QUANTUM CHORUS: THE SLOT CONSENSUS OF QUANTUM CADENCE

9

Data availability. As described, validators agree, proposer by proposer, on a Merkle root or on exclusion. A Merkle root, however, is only a digest, whereas what Quantum Chorus must ultimately provide is the proposal the proposer originally disseminated. We must therefore argue that whenever a root is finalized for pj , some correct validator holds the corresponding proposal and can send it to the others. The argument is per proposer, so we fix a proposer pj . Consider first the fast path. A correct validator that finalizes a root ρ for pj on the fast path holds the proposal itself: before finalizing, it rebuilt the proposal from f + 1 chunks under ρ, and it kept ρ only because the proposal re-encodes to it (line 64). The fallback path asks for slightly more care. Suppose a Merkle root ρ is output for pj on the fallback path. As ρ ̸= empty, obligation guarantees that some correct validator input ρ for proposer pj . We argue that some correct validator then holds the proposal behind ρ in full. Recall from the adoption rule the two ways in which a correct validator comes to input ρ. 1. It may have adopted ρ off a clean set holding a fast entry for ρ. Before adopting, it decoded the proposal from the f + 1 chunks that corroborated the entry and checked that it re-encodes to ρ (line 26). It therefore holds the proposal. 2. Otherwise, it adopted ρ off a clean set consisting of fallback entries alone, f + 1 of which carry ρ. Recall how a fallback entry for ρ comes to be: its sender collected chunks, decoded the proposal, and re-encoded it back to ρ. Among these f + 1 senders, at least one is correct, and that validator holds the proposal in its entirety. In either case, some correct validator holds the proposal and can send it to the others. Finally, a correct validator that finalizes through the halting gadget finalizes a meta-block that some correct validator finalized on the fast path or on the fallback path (see the paragraph on halting), so some correct validator holds the proposal in this case too. How a correct validator obtains chunks it lacks, for instance after finalizing through the halting gadget, lies outside the protocol. We assume only a retrieval mechanism, with retransmission over the same unreliable channels, by which a correct validator eventually obtains data that another correct validator holds. It runs outside the slot’s instance, so halting stops neither side: correct validators keep the data in persistent memory also after halting, and a halted validator still obtains data through it. 4.2

Guarantees

We now state the guarantees of the slot consensus; Appendix A proves them. Agreement, termination, and proposal inclusion are three of the properties that Cadence requires of a slot consensus, and we state them similarly to Cadence [4]; of the other three, slot safety (a finalized block carries the slot’s number) holds trivially, and we do not address hiding and quiescence (a correct validator sends messages for a slot only while it participates in it). Agreement, speculation, and the complexity bound hold for every slot, termination and halting for every slot in which every correct validator starts participating, and proposal inclusion and the accountability lemmas for every timely slot (Section 3). Lemma 1 (Agreement). Quantum Chorus satisfies agreement: correct validators never finalize conflicting blocks for the slot. Lemma 2 (Speculation). In Quantum Chorus, if a correct validator speculatively finalizes a block that differs from the block that a correct validator finalizes, then the misbehavior of at least one faulty validator can be proven. Lemma 3 (Proposal inclusion). Quantum Chorus satisfies proposal inclusion: if the slot is timely, the finalized block contains the proposals of all correct proposers. Lemma 4 (Termination). Quantum Chorus satisfies termination: if every correct validator starts participating in the slot, every correct validator eventually finalizes a block for the slot. Each correct validator then obtains the block’s proposals through the retrieval mechanism of Section 4.1. A correct validator keeps taking part in the slot after finalizing, until it halts (see the paragraph on halting in Section 4.1), and the protocol that schedules the slots, the Conductor in Quantum Cadence, would complete the slot at that point (Section 6).

10

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

Lemma 5 (Halting). If every correct validator starts participating in the slot, every correct validator eventually halts. Moreover, if every correct validator has finalized by time T , every correct validator halts by time max(T, GST) + ∆. Lemma 6 (Message complexity & signature count). In Quantum Chorus, every message that a correct validator sends in dissemination ( Chunk) or in voting ( Vote and PathVote) carries exactly one signature. Moreover, a correct validator initiates at most one broadcast of a Vote, at most one of a PathVote, and at most one of a Finalized message, and, if it is a proposer, initiates at most one Chunk send to each validator, retransmissions aside. Accountability. We now turn the signatures of the voting path into evidence. When the fast path fails in a timely slot, someone is to blame, and we show that, as long as the Byzantine validators are few enough, the correct validators collectively hold a transferable proof against a specific proposer. The threshold is half the fault tolerance: with up to f Byzantine validators, f of them can each sign a negative entry for a correct proposer, so no count of negative entries below f + 1 proves anything, and, as it turns out, the protocol cannot guarantee f + 1 of them per proposer. With at most ⌊f /2⌋ Byzantine validators, however, ⌊f /2⌋ + 1 signed negative entries are enough to convict, and the protocol does guarantee them. Lemma 7 (Accountability under ⌊f /2⌋ faults). Suppose that the slot is timely and that at most ⌊f /2⌋ validators are Byzantine. If some correct validator has not finalized by time D + 2∆, then there exists a proposer pj such that the correct validators collectively hold either (1) two Chunk messages signed by pj that carry different roots, or (2) a Chunk message signed by pj together with at least ⌊f /2⌋ + 1 Vote messages, from different validators, whose entry for pj is negative. Lastly, we exploit a feature of the fallback consensus presented in Section 5. Its first view is a leaderless view, in which every validator votes for its own input. When the inputs of all correct validators coincide, this view decides within two message delays, whatever the faulty validators do. A failure to decide quickly therefore reveals that correct validators adopted different values, and the evidence behind that disagreement can be traced back either to a proposer or to a validator that equivocated. Lemma 8 (Accountability under f faults). Suppose that Quantum Chorus runs with Coda as its fallback consensus and that the slot is timely. If some correct validator has not finalized by time D+4∆, then there exists a proposer pj such that either some correct validator holds 2f + 1 PathVote messages, from different validators, whose entry for pj is a fallback entry, or two correct validators together hold two Vote messages signed by the same validator whose entries for pj differ.

5

Coda: Our Fallback Consensus

This section presents Coda, an implementation of the Byzantine agreement with per-proposer strong unanimity that Quantum Chorus requires. Unlike a generic Byzantine agreement, Coda is built for multiple concurrent proposers: validators input and decide meta-blocks, with one entry per proposer, and strong unanimity and obligation hold for each proposer separately. Coda builds on Forget-IT [1], a leader-based Byzantine agreement protocol that needs no cryptography beyond authenticated channels and keeps its persistent memory constant. Section 5.3 lists how it differs from Forget-IT. Coda satisfies the four properties that Step 6 of Section 4 requires, which Section 5.2 restates in the terms of Coda. Under favorable conditions, Coda decides within two message delays, in its first view, which has no leader. Moreover, Coda bounds its persistent memory: for a fixed number of proposers, it is constant in the number of validators when no proposer equivocated before Coda started, and at most linear in it otherwise. It does not grow with the number of views, so a long asynchronous period costs no persistent memory. The leaderless view. The first view of Coda has no leader. It consists of two voting rounds, with an implicit proposal step: each validator votes right away for its own input. When all correct validators start Coda at the same time, after GST, with the same meta-block, this view decides within two message delays. For the guarantees of Coda, the leaderless view is an optimization. Without it, Coda would begin with a view change that starts at once and turns the validators’ inputs into the values that the first leader proposes, and would remain correct, but its best-case latency would grow from two message delays to five: two for the view change and three for the view of the first leader, if that leader is correct.

5. CODA: OUR FALLBACK CONSENSUS

11

The leaderless view has a practical motivation. In a deployment, proposers do not send their chunks at the slot’s starting time, but as late as they can while still reaching all correct validators by the deadline, so that their proposals include the transactions that arrived shortly before it. Occasionally, a proposer fails to do so, and its chunks reach only between f + 1 and 2f validators in time. The votes for that proposer then hold neither 2f + 1 positive nor 2f + 1 negative entries, and the fast path fails. Suppose that the slot is timely and that all validators follow the protocol, except that some proposers send their chunks after the starting time, so that these reach only between f + 1 and 2f validators in time, which makes these proposers faulty in the model of Section 3. Suppose also that their other messages still arrive within ∆, which the model guarantees only for correct validators. Then every correct validator receives the same votes and path votes, adopts the same meta-block at time D + 2∆, with the late proposals included through fallback entries, and finalizes in the leaderless view by D + 4∆, instead of by D + 7∆ without it, and then only if the first leader is correct. Omission failures, asynchrony, and Byzantine voters can give correct validators different inputs or delay the votes of view 1 past its timeout, in which case the leaderless view may end without a decision and a later view decides. The leaderless view also gives Lemma 8 its time bound. Faulty validators can make the fast path fail without leaving evidence of their faults while all correct validators still adopt the same meta-block. Without the leaderless view, a faulty first leader could then delay the decision further, again without evidence. With it, if all correct validators adopt the same meta-block, they finalize by D + 4∆ whatever the faulty validators do. If some correct validator has not finalized by then, the correct validators thus adopted different values for some proposer, and such a difference always leaves evidence, as the proof of the lemma shows. 5.1

Protocol Description

Model. Coda runs in the model of Section 3, but it does not need the synchronized clocks of that model: each validator uses only its local clock, and only to measure the time elapsed since it entered a view. Its proofs allow arbitrary drift of the local clocks before GST and require only drift-free clocks after GST. Coda uses no cryptography beyond the authentication of channels, so its guarantees hold even against a computationally unbounded adversary, unlike those of Quantum Chorus, which relies on a collision-resistant hash function. The conventions of Section 4.1 on firing rules, time guards, and counting messages apply to Algorithm 2 as well. From the time it starts Coda, a validator keeps the Coda messages it receives for its previous view and later views. Upon entering a view, it discards the kept messages of views below its new previous view, and a crash erases them all. Kept messages count toward every rule whose condition they complete later, also one that a view entry completes. Before it starts Coda, a validator executes none of its rules. A correct validator may also stop taking part in Coda, that is, execute none of its handlers from some time on while its broadcasts remain alive, as validators of Quantum Chorus do when they halt. Protocol overview. Every validator starts Coda with a meta-block, its input (input i for validator pi ): in Quantum Chorus, the meta-block it adopted in Step 5 of Section 4, which holds a root or ⊥ for each proposer. Coda decides a meta-block whose entry for each proposer pj is either a value that a correct validator input for pj or the special value empty, which, like ⊥, excludes pj . Coda decides empty for pj only if the inputs of correct validators differ for pj . Inside Coda, an entry of a meta-block may also be empty. The protocol unfolds in views 1, 2, 3, . . .. View 1 has no leader, and every later view V has a leader, leader(V ), which rotates round-robin among the validators and proposes a meta-block at the beginning of its view. In each view, validators vote in two rounds. They first send vote-1 messages for a meta-block, in view 1 for their own input and later for the leader’s proposal. A validator that receives 2f +1 vote-1 messages for the same meta-block x sends a vote-2 message for x, unless it has sent one in the view already. A validator that receives 2f + 1 vote-2 messages for x decides x. Every view, also one that decided, ends with a view change, in which validators exchange echo messages. These announce, for each proposer, values that are safe to carry into the next view, that is, consistent with every decision made in this view or an earlier one. A validator enters the next view with a meta-block of such values, its guard for that view. Coda has no rule for stopping: validators keep running it after they decide, since the others may still need their messages to decide. In Quantum Chorus, a validator stops running Coda when it halts through the halting gadget of Section 4, which it does only after finalizing. State. A validator keeps two meta-blocks for each of its current and previous views. Its guard for view V is the meta-block with which it entered V : its input for view 1, and safe values from the view change for later views. A correct leader of V proposes its guard. The guard reflects the earlier views: if a meta-block

12

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

Deciding in view V Step 1: proposal leader(V ) broadcasts its guard x: ⟨prepare, V, x⟩ view 1: skipped

Step 2: first vote once x is justified (f +1 echos of V −1 for each entry): broadcast ⟨vote-1, V, x⟩

(no leader)

view 1: own input, at once

Step 3: second vote on 2f +1 ⟨vote-1, V, x⟩, if no vote-2 sent in V : lock x, broadcast ⟨vote-2, V, x, g⟩, where g is its own guard

Step 4: decide on 2f +1 vote-2 of V or V −1 with the same lock x ̸= none: decide x the view continues

vote-2 messages of view V , each with its sender’s lock (or none) and guard The view change Step 5: timeout 5∆ after entry, if no vote-2 sent in V : broadcast ⟨vote-2, V, none, g⟩ (no lock), where g is its own guard

Step 6: echo safe values from 5∆ after entry, for every set S of 2f +1 accepted vote-2 of V with no two different locks, and every proposer pj : broadcast ⟨echo, V, j, v⟩, where v is the lock’s entry for pj if S holds a lock, else the entry for pj that f +1 guards in S share, else empty

Step 7: next view on f +1 echos with the same value for the same proposer: echo it too on 2f +1 ⟨echo, V, j, x[j]⟩ for every proposer pj : enter view V +1 with guard x

view V +1, with guard x

Fig. 2: One view V of Coda. A correct validator sends at most one vote-2 message in V , with its lock in Step 3 or without a lock in Step 5, and both the decision of Step 4 and the echoes of Step 6 use these messages. The view change ends every view, also one that decided, and moves the validator to view V + 1 with a guard, which it proposes in Step 1 if it leads V + 1. View 1 has no leader and starts at Step 2. was decided in a view smaller than V , it is the guard for V of every correct validator that enters V . A validator’s lock for view V is the meta-block for which it received 2f + 1 vote-1 messages in V before sending its vote-2 message, or none if there is none. The lock reflects view V itself: a view can decide only a meta-block that at least f + 1 correct validators locked in it. The vote-2 message of a validator in view V carries its lock and its guard: the view change needs both to determine which values are safe. In persistent memory, a validator keeps its current view, the time it entered that view, and whether it has decided. For its current and previous views, it also keeps its guard, its lock, and the votes and echoes it has broadcast. The Coda messages that a validator receives, echoes included, are not kept in persistent memory, so a crash erases them. After a crash, retransmission delivers again the messages whose broadcasts are still alive. Corroboration. Without certificates, a validator cannot show others that it holds a quorum. Coda relies instead, in two places, on corroboration by f + 1 messages, as Quantum Chorus does for fast entries. A validator votes for a leader’s proposal only once the proposal is justified, that is, for each of its entries, f + 1 echoes of the previous view announce that entry as safe. The view change counts a vote-2 message that claims a lock only once it is accepted, that is, f + 1 vote-1 messages for the lock have arrived. Among f + 1 messages from different validators, at least one comes from a correct validator. Every entry of a justified proposal thus has an echo from a correct validator, possibly a different one for each entry, and every accepted lock has a vote-1 message for it from a correct validator. The steps of a view. Algorithm 2 gives the pseudocode, which we describe in seven steps, shown in Figure 2: Steps 1 to 4 follow the message rounds of a view, and Steps 5 to 7 form the view change. Step 1: Proposal (views V ≥ 2). The leader of a view V ≥ 2 opens it by broadcasting its guard x in a message ⟨prepare, V, x⟩ (line 33). View 1 has no leader and skips this step. Step 2: First vote. In view 1, every validator broadcasts ⟨vote-1, 1, x⟩ upon starting, for its own input x (line 32). A validator in a view V ≥ 2 that has received the leader’s ⟨prepare, V, x⟩ broadcasts ⟨vote-1, V, x⟩ as soon as x is justified : for every proposer pj , it has received f + 1 echo messages of view V − 1 that announce x[j] as safe for pj , so that at least one correct validator announced it (line 34). A validator sends at most one vote-1 message per view. Step 3: Second vote. A validator that receives 2f + 1 vote-1 messages of its current view V for the same meta-block x sets its lock for V to x, whether or not it voted for x itself, and broadcasts ⟨vote-2, V, x, g⟩,

5. CODA: OUR FALLBACK CONSENSUS

13

where g is its guard for V (lines 37 to 40). It skips this step if it has already broadcast a vote-2 message in V . No two correct validators lock different meta-blocks in the same view, since two sets of 2f + 1 vote-1 messages from different validators share a correct sender, which sends only one vote-1 message per view. Step 4: Decision. Upon receiving 2f +1 vote-2 messages of the same view, its current or its previous one, with the same lock x ̸= none, a validator decides x, unless it has decided before (line 41). The previous view counts as well, since a validator may enter the next view before these messages reach it. The view change. A view may end without a decision, for instance view 1 when correct validators have different inputs, and a later view when its leader is faulty. The view change, Steps 5 to 7, ends every view and moves the validators to the next one. It carries every decision forward: if a meta-block x was decided in view V or earlier, every correct validator that enters a later view has guard x there, and correct validators vote only for x in later views. Step 5: Timeout. A validator that has been in a view V for 5∆, measured on its local clock, and has not broadcast a vote-2 message in V broadcasts one without a lock, ⟨vote-2, V, none, g⟩, where g is its guard for V (line 45). The view change, which needs 2f + 1 vote-2 messages, can thus proceed even if no meta-block gathers 2f + 1 vote-1 messages. Step 6: Echoing safe values. The view change reads the locks and guards that the vote-2 messages of the view carry, and it counts only accepted messages (see the paragraph on corroboration): a vote-2 message with a lock x is accepted once f + 1 vote-1 messages for x of the same view have arrived (line 17), one without a lock on receipt, and at most one per sender and view. A lock needs this corroboration here because a single lock determines the values echoed for a whole set of messages. The decision of Step 4 needs none, as it counts 2f + 1 messages with the same lock. Once 5∆ has elapsed since the validator entered its current view V , for every set S of 2f + 1 accepted vote-2 messages of V whose locks are all the same meta-block, and for every proposer pj , it echoes a value v, that is, it broadcasts ⟨echo, V, j, v⟩, which announces v as safe for pj in view V + 1 (line 47). It chooses v as follows. – If S holds a lock ℓ, then v = ℓ[j]. – Otherwise, v is the entry for pj that the guards of f + 1 messages in S share, or empty if there is none. The set S may mix messages without a lock and messages with the same lock. Two different locks, however, are never allowed in the same set S. Since no two correct validators lock different meta-blocks in a view (Step 3), one of the senders of conflicting locks is faulty, and the messages of the correct validators carry no conflicting locks. As long as it cannot form a set without conflicting locks, the validator therefore waits for further messages. As the rule fires for every such set S, a validator may echo several values for one proposer in a view. A validator need not enumerate the sets S, however: it suffices to count the accepted vote-2 messages by lock and by guard entry, and Appendix B.3 gives the conditions on these counts. The delay of 5∆ is long enough that, if every correct validator has started Coda by GST and none stops taking part, then in a view whose leader is correct and which no correct validator enters before GST, every correct validator locks the leader’s meta-block before any correct validator leaves the view. The values that correct validators echo are safe. If view V decided a meta-block x, at least f + 1 correct validators locked x, so every such set S holds the lock x. If an earlier view decided x, every correct validator entered V with guard x and votes in V only for x, so an accepted lock in S is x, and if S holds no lock, the guards of the correct validators in S share the entry x[j]. Step 7: Entering the next view. Echoes are amplified as in Bracha’s broadcast [8]: upon f + 1 echoes with the same value for the same proposer, of its current or previous view, a validator echoes that value too, for the same view (line 61). A validator enters the next view once, for every proposer, 2f + 1 echoes of the same view agree. Precisely, let V be its current view, or a later one if the validator has fallen behind. Once it has received, for every proposer pj , 2f + 1 messages ⟨echo, V, j, v⟩ with the same value v, it enters view V + 1 with the guard whose entry for each proposer pj is the value v of these echoes (line 53). The 2f + 1 echoes for one proposer may come from other validators than those for another proposer. A validator keeps the state of its current and previous views only, and upon entering a view, it abandons its broadcasts of the views before the previous one (lines 14 and 15), which bounds its persistent memory however many views pass. A validator that has fallen behind may therefore never receive the messages of the views it missed. Instead, once it has received, for a later view V and every proposer pj , f + 1 messages

14

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

⟨echo, V, j, v⟩ with the same value v, it catches up by entering view V directly, with the guard built in the same way from these echoes (line 57). One of these echoes comes from a correct validator, which has thus reached view V , and values safe for view V + 1 are safe for V as well. 5.2

Guarantees

In this subsection, we state the correctness and complexity guarantees of Coda, which Appendix B proves. Coda satisfies the four properties that Step 6 of Section 4 requires of the fallback consensus (Lemmas 11 to 14). In the terms of Coda, in which a validator inputs a meta-block and decides one, they read as follows. – Agreement: No two correct validators decide different meta-blocks. – Termination: If every correct validator starts Coda, every correct validator eventually decides. – Strong unanimity (per proposer): If all correct validators that input a meta-block input the same value other than empty for a proposer pj , no correct validator decides a meta-block whose entry for pj is empty. – Obligation (per proposer): If a correct validator decides a meta-block whose entry for a proposer pj is a value v ̸= empty, some correct validator input v for pj . Agreement, strong unanimity, and obligation hold in every execution, whatever the timing, and also when correct validators stop taking part in Coda, possibly before inputting (Appendix B). Termination needs every correct validator to start Coda at some point and none to stop taking part. To simplify its proof, Appendix B adopts the participation convention that every correct validator starts Coda by GST. Under this convention, Lemma 12 also bounds the time. Let V be the first view greater than 1 that no correct validator enters before GST and whose leader is correct. Then every correct validator decides within 5∆ of the first entry into V by a correct validator. In Quantum Chorus, a correct validator starts Coda when it adopts a meta-block (Step 5 of Section 4), possibly after GST. The convention costs no generality: if the last correct validator starts Coda at a time Tstart after GST, the termination proofs hold with Tstart in place of GST, as Appendix B shows. In Quantum Chorus, a correct validator may also halt before it inputs, in which case it never starts Coda. Once a correct validator halts, the halting gadget of Section 4 makes every correct validator that participates finalize (Claim 2). Complexity Finally, we bound, in terms of the number k of proposers, the message complexity of Coda, the number of messages that correct validators send per view, retransmissions aside, and the size of the persistent memory of a correct validator. We count memory and message sizes in words: a word holds a value (a root, ⊥, or empty), a view number, or a validator identifier, so a meta-block occupies k words, and a message occupies a constant number of words, for its type and view number, beyond the meta-blocks or value that it carries. For every proposer pj , let Pj = {input w [j] | pw is correct and inputs} denote the set of values that correct validators input for pj , and let c = maxj |Pj |. In general, |Pj | ≤ n, as each correct validator inputs one value per proposer. When Quantum Chorus invokes Coda and the proposer pj did not equivocate, every correct validator inputs for pj either the Merkle root of pj ’s proposal or ⊥, so |Pj | ≤ 2. The per-validator broadcast counts and the persistent-memory bound below are stated in terms of c: they do not depend on n when c = O(1), and they grow by a factor of n in the worst case. Lemma 9 (Message complexity). For every view V , each correct validator initiates at most 3 + (c + 1)k broadcasts of messages of view V . Hence, retransmissions aside, correct validators send O(ckn2 ) messages of each view, which is O(kn2 ) when c = O(1). The same accounting bounds the communication of a correct validator in words: a prepare or a vote-1 message carries one meta-block, a vote-2 message carries two, and an echo message carries one value, for O(ckn) words per view. We now turn to memory. Lemma 10 (Persistent memory). Each correct validator stores O(ck) words in persistent memory for Coda, which is O(k) words when c = O(1). 5.3

Differences from Forget-IT

Coda keeps the structure of Forget-IT’s views: a prepare message, two rounds of votes, locks, guards carried in vote-2 messages, the acceptance rule for these messages, and a view change that reads their

5. CODA: OUR FALLBACK CONSENSUS

15

Algorithm 2 Coda: Pseudocode (for validator pi ) 1: Notation: 2: - A meta-block x assigns a value x[j] ∈ Value ∪ {empty} to each proposer pj . 3: - Value is the set of values that validators input for a proposer (in Quantum Chorus, a root or ⊥), and empty ∈ / Value. 4: - none denotes absent state (no lock, no message); it is never proposed, voted for, or decided. 5: Global variables (persistent memory): 6: View view i 7: Time of entry into the current view and whether pi has decided

▷ pi ’s current view

8: View-specific variables (persistent memory), indexed by view V : 9: MetaBlock guard i [V ] ← none ▷ the meta-block with which pi entered view V , which it proposes if it leads view V 10: MetaBlock lock i [V ] ← none ▷ pi ’s locked meta-block for view V , if any 11: Message vote1 i [V ], vote2 i [V ] ← none ▷ vote-1 and vote-2 messages broadcast by pi in view V 12: Set(Message) sent i [V ] ← ∅ ▷ echo messages of view V broadcast by pi 13: Rules: 14: - Validator pi maintains (in persistent memory) view-specific variables for views view i and view i − 1 only, and no received Coda messages. 15: - Upon entering view V , abandon all ongoing broadcasts of Coda messages from views smaller than V − 1. 16: - A vote-2 message is accepted only if its guard is a meta-block and its lock is either none or a meta-block. 17: - A received message ⟨vote-2, V, x, ·⟩ with x ̸= none is accepted only after pi has received f + 1 messages ⟨vote-1, V, x⟩. 18: - A received message ⟨vote-2, V, none, ·⟩ is accepted immediately upon reception. 19: - For each view V , at most one ⟨vote-2, V, ·, ·⟩ message is accepted from each validator. 20: Functions: 21: - echo(View V, Proposer pj , Value ∪ {empty} v): ▷ broadcasts each echo at most once, and records it 22: if ⟨echo, V, j, v⟩ ∈ / sent i [V ]: 23: sent i [V ] ← sent i [V ] ∪ {⟨echo, V, j, v⟩}; broadcast ⟨echo, V, j, v⟩ 24: 25:

- justified(MetaBlock x): ▷ checks whether every entry of x was echoed as safe in the previous view return whether pi has received f + 1 messages ⟨echo, view i − 1, j, x[j]⟩ for every proposer pj

26: upon starting: 27: guard i [1] ← pi ’s input 28: enter view 1 29: upon entering view V : 30: view i ← V ; record the time of entry 31: if V = 1: 32: vote1 i [1] ← ⟨vote-1, 1, guard i [1]⟩; broadcast vote1 i [1] 33: else if pi = leader(V ): broadcast ⟨prepare, V, guard i [V ]⟩

▷ update the current view ▷ view 1 is the leaderless view ▷ everyone votes for its own input ▷ leader proposes a meta-block

34: upon receipt of ⟨prepare, view i , x⟩ from leader(view i ) and justified(x): 35: if vote1 i [view i ] = none: 36: vote1 i [view i ] ← ⟨vote-1, view i , x⟩; broadcast vote1 i [view i ] 37: upon receipt of 2f + 1 ⟨vote-1, view i , x⟩ messages for the same meta-block x: 38: if vote2 i [view i ] = none: 39: lock i [view i ] ← x 40: vote2 i [view i ] ← ⟨vote-2, view i , lock i [view i ], guard i [view i ]⟩; broadcast vote2 i [view i ]

▷ lock on the meta-block x

41: upon receipt of 2f + 1 ⟨vote-2, V, x, ·⟩ messages for the same meta-block x ̸= none and some V ∈ {view i − 1, view i }: 42: if pi has not decided yet: trigger decide(x) ▷ decide the meta-block x 43: upon 5∆ time has elapsed since entering view view i : 44: if vote2 i [view i ] = none: 45: vote2 i [view i ] ← ⟨vote-2, view i , none, guard i [view i ]⟩; broadcast vote2 i [view i ]

▷ timeout: no lock

46: ▷ the view change: what is safe to carry into the next view, proposer by proposer 47: upon 5∆ time has elapsed since entering view view i and existence of a set S of 2f + 1 accepted ⟨vote-2, view i , ·, ·⟩ messages whose non-none locks are all identical: ▷ fires once for every such set S 48: if there exists a non-none lock ℓ in S: invoke echo(view i , pj , ℓ[j]) for every proposer pj ▷ a lock exists: echo it 49: else: for every proposer pj : 50: if some G ∈ Value ∪ {empty} is the entry for pj in the guards of f + 1 messages in S: 51: invoke echo(view i , pj , G) ▷ echo the entry for pj that f + 1 guards in S share 52: else: invoke echo(view i , pj , empty) ▷ the guards for pj diverge: echo empty 53: upon receipt of 2f + 1 messages ⟨echo, V, j, x[j]⟩ for every proposer pj , for some meta-block x and some V ≥ view i : 54: guard i [V + 1] ← x 55: enter view V + 1 56: ▷ catching up: a correct validator has reached view V , and x is safe to carry into it 57: upon receipt of f + 1 messages ⟨echo, V, j, x[j]⟩ for every proposer pj , for some meta-block x and some V > view i : 58: guard i [V ] ← x 59: enter view V 60: ▷ amplification, for the current view and the one below it 61: upon receipt of f + 1 messages ⟨echo, V, j, v⟩ for some pj , some v ∈ Value ∪ {empty}, and some V ∈ {view i − 1, view i }: 62: invoke echo(V, pj , v)

16

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

locks and guards. It differs in five main points. First, every view of Forget-IT has a leader, and its guards start as a special value safe, which means that every value is safe. Coda adds the leaderless view 1, and its guards start as the validators’ inputs. Second, a Forget-IT validator votes for a proposal only if it equals its guard or its guard is safe, it may relax its guard to safe within a view, and a leader whose guard is safe proposes its own input. A Coda validator votes for any justified proposal of the leader, its guard stays fixed within a view, and a leader proposes exactly its guard. Third, Forget-IT passes the outcome of a view change through three phases of echoes, in which safe counts toward a quorum for every value. Coda has a single phase of echoes per proposer, amplified as in Bracha’s broadcast, in which empty is an ordinary value that counts only for itself. These changes give Coda strong unanimity and obligation per proposer, whereas Forget-IT guarantees validity only when all processes are correct and the network is synchronous from the start. Fourth, a Forget-IT validator sends at most two echoes per phase and view, the second one for safe. As empty counts for no other value, a Coda validator may instead echo, for one proposer, empty and every value that correct validators input for it, so its messages and persistent memory grow with the number of such values (Section 5.2). Fifth, Coda lacks two entry rules of Forget-IT, by which the next leader enters on f + 1 echoes of the last phase and the other validators on its proposal and f + 1 echoes of the second phase, and which let Forget-IT decide within three message delays of a correct leader’s entry after GST. In Coda, the first view with a correct leader that starts after GST decides within 5∆ of the first entry into it (Lemma 12).

6

Integration with the Conductor

Within Cadence, the slot consensus runs under the Conductor, which opens the slots. The Conductor groups slots into windows of consecutive slots with evenly spaced deadlines, and a validator opens the next window only once enough slots of the earlier windows are complete, which in Cadence means that the validator has finalized the blocks of these slots; this keeps the number of open slots bounded. Once per window, the validators agree on the first deadline of the next window through an agreement on a core set (ACS) [4]. We expect Quantum Cadence to keep the algorithm of the Conductor and to change two things around it: the ACS and the point at which a validator completes a slot. This version of the paper outlines these changes but does not specify them in full or analyze them. In the model of Section 3, in which validators may crash and channels are unreliable, the Conductor also needs changes similar to those made to the slot consensus: a validator keeps retransmitting the messages that others may still need, such as its Finalized messages and those of the ACS, until the Conductor has moved far enough ahead; we leave these changes to a later version. A signature-free ACS. The ACS can be built without signatures, following Ben-Or, Kelmer, and Rabin [6]: each validator disseminates its proposal with a reliable broadcast [8], and one binary agreement per validator decides whether that validator’s proposal enters the set. For the binary agreements, Coda can be used with a single proposer and the values 0 and 1, reading an output of empty as 0. An ACS instance would end with the same halting rule as a slot (Section 4.1), with the set in place of the metablock: a validator would hand the set to the Conductor when it halts in the instance, and then stop running it. Completion at halting. The analysis of the Conductor in Cadence relies on totality: once a correct validator completes a slot after GST, every correct validator does so shortly after. In Quantum Chorus, finalizing has no such constant bound, but halting does (Section 4.1): if every correct validator starts participating by time T , every correct validator halts by time max(T, H, GST) + 2∆, where H is the time at which the first correct validator halts. A validator therefore completes a slot when it halts, and it opens a window when it halts in the ACS instance that fixes the window’s first deadline. This bound counts from the last correct validator’s start, however, and a validator that is behind does not participate yet. To bring it up to date, each validator retransmits one cumulative FinalizedUpTo message, which it replaces every ∆ with an up-to-date one, and keeps only the most advanced one from each peer. The message refers to a single chain that lists the finalized meta-blocks in slot order, with the output of each window’s ACS instance inserted where the Conductor may open that window, that is, after the earlier slots that must be complete first. It names the last point of the chain up to which its sender has finalized every slot and every ACS instance, with a hash over the chain up to that point. These messages need not name the same point: once f + 1 validators have named a point or a later one, with hashes that fit a single chain, a validator fetches the chain from them, checks it against the hashes, and finalizes every slot and every ACS instance up to that point, and once 2f + 1 have, it halts in them,

7. EVALUATION

Chorus

Quantum Chorus, 0 B

1000

0

231 213 216 229

196 198 200 211

175 182 184 194

197 206 206 206

100

187 195 195 195

100

200

170 179 179 179

561

20 Proposers

Full finality (ms)

772 354 394

5

298 213 249 386

360 213 193 225

Upload (Mbps)

500

0

5000 B

300

750

250

1000 B

17

5

20 Proposers

100

Fig. 3: Average upload per validator (left) and mean latency to full finality (right), for 200 validators with 1 Gbps links. Chorus uses BLS signatures, and the signature sizes refer to Quantum Chorus. Each latency bar consists of the latency with unlimited bandwidth (light, value inside the bar) and the increase at 1 Gbps (dark), with the total above the bar. With unlimited bandwidth, the latency of Quantum Chorus does not depend on the signature size. which completes these slots and opens these windows. Totality would then hold within a constant time, whatever a validator’s lag, for the prefixes of completed slots that the Conductor counts. With these changes, we expect the guarantees of the Conductor to carry over: the number of open slots would stay bounded at all times, correct validators would open each slot within a constant time of one another after GST, and, for a constant grace period G, every slot whose starting time is at least GST + G would be timely (Section 3).

7

Evaluation

We compare Quantum Chorus with Chorus in simulation, for 200 validators of equal stake, each with a 1 Gbps link, whose locations follow the geographic distribution of stake in the Monad validator set on October 1, 2026. The simulation covers propagation, transmission and queueing delays, but no local computation. We simulate only the fast path, without faults or message loss. Slots start every 100 ms, and each carries 500 KB of proposal data, divided equally among 5, 20 or 100 proposers. We do not fix a signature scheme and instead vary the signature size up to 5000 bytes. This range covers the parameter sets of ML-DSA [19] and of Falcon [15], which NIST has selected for standardization. It excludes the larger SLH-DSA signatures [20]. Since safety and liveness need no signatures, we also simulate a signature size of zero, which gives the cost of the protocol without signatures. Figure 3 shows the average upload of a validator and the mean latency from a proposer’s broadcast until a validator finalizes the slot (full finality, as opposed to speculative finality), averaged over all pairs of proposer and validator. Speculative finality comes about 50 ms earlier: with 20 proposers, for instance, Quantum Chorus reaches it after 145 to 155 ms on average, depending on the signature size. In terms of bandwidth, the two protocols differ mainly in the size of their consensus messages. Chunks account for about 180 Mbps of every validator’s upload, in every configuration and for both protocols, and consensus messages for the rest. Since post-quantum signatures are much larger than BLS signatures, Quantum Chorus with large signatures needs more upload than Chorus when there are few proposers. However, a Quantum Chorus vote carries one signature, while a Chorus vote carries a signature or certificate for every proposer, so Quantum Chorus scales better with the number of proposers. Message sizes matter less for latency. With 1 Gbps links, they cause transmission and queueing delays that are small relative to the propagation delays: compared with no signatures, even 5000-byte signatures add at most 16 ms to the latency of Quantum Chorus. With 5 or 20 proposers, Chorus finalizes up to 19 ms earlier than Quantum Chorus. At 100 proposers, the larger messages of Chorus delay it enough that Quantum Chorus finalizes up to 18 ms earlier. The two protocols send the same kinds of messages in the same rounds, dissemination followed by two rounds of votes, so one might expect them to have the same latency when bandwidth is unlimited

18

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

and message sizes do not matter. In fact, Chorus is then slightly faster (by less than 10 ms), because its validators broadcast the certificates they form or receive: a validator can cast its fast vote as soon as it receives a meta-block of certificates from another validator, and can finalize as soon as it receives a certificate of 2f + 1 fast votes. Quantum Chorus forms no compact certificates, so each validator collects the votes itself. Without this forwarding, the two protocols behave identically from a networking standpoint and have the same latency. Simulation details. Each run covers three overlapping slots, of which we measure the middle one, and we average over 200 trials. Both protocols use early voting and quorums of 135 validators. All messages of a validator share its 1 Gbps uplink, and propagation delays follow RIPE Atlas measurements. We make optimizations that a deployment would make. Votes do not carry chunks. Instead, as in Deterministic RaptorCast [10], which Cadence uses in practice [4], each proposer sends every validator its chunks in separate packets, and validators forward enough of these packets for every validator to decode every proposal. A validator’s votes take priority over the chunks it forwards, and, as in the evaluation of Cadence [4, Section 8], each proposer starts disseminating at its own lead time before the deadline rather than at the starting time D − ∆, as in Algorithm 1.

8

Related Work

Byzantine consensus. Byzantine consensus asks n processes, of which at most f may deviate arbitrarily from the protocol, to agree on a common value [21,18]. Fischer, Lynch, and Paterson showed that no deterministic protocol solves it under asynchrony, even if only one process may crash [14]. Deterministic protocols do solve it under synchrony [12] and under partial synchrony [13], the model of Cadence and of this paper, and randomized protocols solve it under asynchrony [5,22]. Quantum Chorus and Coda are deterministic. Byzantine consensus without signatures. Protocols that use no cryptography beyond authenticated channels, called information-theoretic or unauthenticated, tolerate a computationally unbounded adversary. Their safety and liveness thus rest on no signature that a quantum computer could forge. Since a validator cannot prove a quorum to another without signatures, these protocols often use the amplification of Bracha’s reliable broadcast [8]: a validator that receives f + 1 matching messages repeats the message, and one that receives 2f + 1 acts on it. Coda uses this rule for the echoes of its view change (Section 5.1), and Quantum Chorus for the Finalized messages of its halting gadget (Section 4.1). Among the information-theoretic protocols for partial synchrony, IT-HotStuff [3] and TetraBFT [24] keep persistent memory constant, send O(n2 ) messages per view, and are optimistically responsive. Their good-case latency, the latency when the network is synchronous from the start and the leader of the first view is correct, is six and five message delays, respectively. Forget-IT [1] reduces it to three, which is optimal [2]. Coda builds on Forget-IT (Section 5.3). Simple-IT [25] replaces quorum certificates by reliable broadcast and a reliable notification primitive. With Bracha’s reliable broadcast, its good-case latency is four message delays, one more than that of Forget-IT, but its design allows pipelining. Consensus with post-quantum signatures. Protocols can keep their certificates with post-quantum signatures, but at a cost. Post-quantum signatures can be aggregated, although the aggregates are much larger than a BLS aggregate signature and take much longer to compute [16,11]. Certificates can also stay lists of ordinary signatures: in HotStuff-style protocols [23], the leader collects the votes and disseminates the certificate together with its next proposal, for instance with AVID [9]. The drawback of these protocols is latency: every round of votes passes through the leader, so a decision typically takes more message delays than in protocols in which validators send their votes to all. The distributed quorum signature (DQS) [16] instead stops sending certificates: it turns them from network messages into local events, weak certificates for safety and strong ones for liveness, and is built from ordinary signatures and a Brachastyle broadcast of approvals. It takes the place of quorum signatures in an existing protocol: a validator that creates a weak certificate broadcasts an approval for it. Quantumglow, the post-quantum version of Alpenglow, follows this approach [17, Section 5].

Use of AI Tools The protocols and the main ideas of this paper are our own. We used large language models to help draft and revise parts of the text and the simulator. The authors take full responsibility for the content of this paper.

8. RELATED WORK

19

References 1. Abraham, I., Das, S., Efron, Y., Komatovic, J.: Forget-IT: Optimal good-case latency for information-theoretic BFT. In: Proceedings of the ACM Symposium on Principles of Distributed Computing (PODC). pp. 478–488 (2026). https://doi.org/10.1145/3796701.3815965, also IACR ePrint 2026/355 2. Abraham, I., Nayak, K., Ren, L., Xiang, Z.: Good-case latency of Byzantine broadcast: A complete categorization. In: Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing (PODC). pp. 331–341 (2021). https://doi.org/10.1145/3465084.3467899 3. Abraham, I., Stern, G.: Information theoretic HotStuff. In: 24th International Conference on Principles of Distributed Systems (OPODIS 2020). LIPIcs, vol. 184, pp. 11:1–11:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.OPODIS.2020.11 4. Babel, K., Elsheimy, F., Heimbach, L., Jalalzai, M.M., Klenze, T., Komatovic, J., Milionis, J., Setrin, M., Shoup, V.: Cadence: Extreme pipelining with multiple concurrent proposers. arXiv:2607.02275 (2026) 5. Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols (extended abstract). In: Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing (PODC). pp. 27–30 (1983). https://doi.org/10.1145/800221.806707 6. Ben-Or, M., Kelmer, B., Rabin, T.: Asynchronous secure computations with optimal resilience. In: Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing (PODC). pp. 183–192 (1994). https://doi.org/10.1145/197917.198088 7. Boneh, D., Lynn, B., Shacham, H.: Short signatures from the Weil pairing. In: Advances in Cryptology – ASIACRYPT 2001. LNCS, vol. 2248, pp. 514–532. Springer (2001). https://doi.org/10.1007/3-540-45682-1_ 30 8. Bracha, G.: Asynchronous Byzantine agreement protocols. Information and Computation 75(2), 130–143 (1987). https://doi.org/10.1016/0890-5401(87)90054-X 9. Cachin, C., Tessaro, S.: Asynchronous verifiable information dispersal. In: Proceedings of the 24th IEEE Symposium on Reliable Distributed Systems (SRDS). pp. 191–202 (2005). https://doi.org/10.1109/RELDIS. 2005.9 10. Category Labs: MIP-10: Deterministic RaptorCast. Monad Improvement Proposals, no. 10 (2026), https: //mips.monad.xyz/MIPs/MIP-10 11. Centelles, A., Dao, Q., Badakhshan, M., Thaler, J.: Aerie: Efficient aggregation of Falcon signatures. IACR Cryptology ePrint Archive, Paper 2026/2501 (2026), https://eprint.iacr.org/2026/2501 12. Dolev, D., Strong, H.R.: Authenticated algorithms for Byzantine agreement. SIAM Journal on Computing 12(4), 656–666 (1983). https://doi.org/10.1137/0212045 13. Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. Journal of the ACM 35(2), 288–323 (1988). https://doi.org/10.1145/42282.42283 14. Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. Journal of the ACM 32(2), 374–382 (1985). https://doi.org/10.1145/3149.214121 15. Fouque, P.A., Hoffstein, J., Kirchner, P., Lyubashevsky, V., Pornin, T., Prest, T., Ricosset, T., Seiler, G., Whyte, W., Zhang, Z.: Falcon: Fast-Fourier lattice-based compact signatures over NTRU. Specification v1.2, https://falcon-sign.info/falcon.pdf (2020) 16. Kniep, Q., Sliwinski, J., Wattenhofer, R.: Byzantine fault-tolerant post-quantum distributed quorum signatures. arXiv:2607.17700 (2026) 17. Kniep, Q., Sliwinski, J., Wattenhofer, R.: Solana Alpenglow consensus: Increased bandwidth, reduced latency. White paper v1.2, Anza, July 29, 2026, https://www.anza.xyz/alpenglow (2026) 18. Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Transactions on Programming Languages and Systems 4(3), 382–401 (1982). https://doi.org/10.1145/357172.357176 19. National Institute of Standards and Technology: Module-lattice-based digital signature standard. Federal Information Processing Standards Publication 204, National Institute of Standards and Technology (2024). https://doi.org/10.6028/NIST.FIPS.204 20. National Institute of Standards and Technology: Stateless hash-based digital signature standard. Federal Information Processing Standards Publication 205, National Institute of Standards and Technology (2024). https://doi.org/10.6028/NIST.FIPS.205 21. Pease, M.C., Shostak, R.E., Lamport, L.: Reaching agreement in the presence of faults. Journal of the ACM 27(2), 228–234 (1980). https://doi.org/10.1145/322186.322188 22. Rabin, M.O.: Randomized Byzantine generals. In: 24th Annual Symposium on Foundations of Computer Science (FOCS). pp. 403–409. IEEE Computer Society (1983). https://doi.org/10.1109/SFCS.1983.48 23. Yin, M., Malkhi, D., Reiter, M.K., Gueta, G.G., Abraham, I.: HotStuff: BFT consensus with linearity and responsiveness. In: Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing (PODC). pp. 347–356 (2019). https://doi.org/10.1145/3293611.3331591 24. Yu, Q., Losa, G., Wang, X.: TetraBFT: Reducing latency of unauthenticated, responsive BFT consensus. In: Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing (PODC). pp. 257–267 (2024). https://doi.org/10.1145/3662158.3662783 25. Yu, Q., Villacis, J., Losa, G., Xiang, Z., Wang, X.: Simple-IT: Practical low-latency signature-free BFT consensus. arXiv:2606.14404 (2026)

20

A

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

Proofs for Quantum Chorus

This appendix proves the lemmas of Section 4. A.1

Core Properties

A correct validator finalizes on the fast path (line 65), on the fallback path (line 73), or through the halting gadget (lines 74 and 76). We first show that a finalization through the halting gadget repeats a finalization on one of the two paths. Claim 1 (Finalizations through the halting gadget). If a correct validator finalizes a meta-block x through the halting gadget at time t, then some correct validator finalized x on the fast path or on the fallback path by time t. Proof. A correct validator broadcasts ⟨Finalized, x⟩ exactly when it finalizes x. Finalizing x through the halting gadget requires ⟨Finalized, x⟩ messages from f + 1 validators, at least one of them correct, which therefore finalized x earlier. Hence, the first correct validator to finalize x did so on the fast path or on the fallback path, and if a correct validator finalizes x through the halting gadget at time t, this first finalization happened by time t. ⊓ ⊔ The proofs below compare finalized meta-blocks entry by entry. A speculative or fast-path finalization does not take the values of the fast entries as they are: before finalizing, a validator replaces a root whose proposal does not re-encode to it by ⊥ (lines 60 and 64). For a value v, a root or ⊥, we call the result of this check the checked value of v: ⊥ if v is a root whose proposal does not re-encode to v, and v otherwise. It does not depend on which chunks are used (see finalizing on the fast path in Section 4). Lemma 1 (Agreement). Quantum Chorus satisfies agreement: correct validators never finalize conflicting blocks for the slot. Proof. It suffices to show that correct validators finalize the same meta-block, as a meta-block determines its block. Fix a proposer pj , and consider two correct validators finalizing meta-blocks x and y. By Claim 1, some correct validator also finalizes x on the fast path or on the fallback path, and so does one for y; we may therefore assume that both finalizations are made on these two paths. To prove the lemma, we show that x[j] = y[j], going through the three possible combinations of paths. – If both validators finalize on the fast path, quorum intersection settles the matter: there are 2f + 1 path votes whose entry for pj is a fast entry for some value v whose checked value is x[j], and 2f + 1 whose entry for pj is a fast entry for some value w whose checked value is y[j]. The two sets of senders intersect in a correct validator, which issued a single path vote (Lemma 6), and thus a single entry for pj . Hence, v = w, and x[j] = y[j]. – If both validators finalize on the fallback path, the agreement property of the fallback consensus gives them the same output. Both finalize this output after replacing its entries empty by ⊥ (line 73), so x = y. – The interesting case is the mixed one: without loss of generality, say x is finalized on the fast path and y on the fallback path. As x is finalized on the fast path, there exist 2f + 1 path votes whose entry for pj is a fast entry for some value v whose checked value is x[j]. By quorum intersection, any clean set for pj , being a set of 2f + 1 accepted entries for pj from different validators, contains at least one of these fast entries: the two sets of senders intersect in a correct validator, whose unique entry for pj is a fast entry for v. The adoption rule then leaves little choice. If v = ⊥, every correct validator adopts ⊥ for pj . If v is a root ρ, every correct validator decodes the proposal from the f + 1 chunks that corroborated the fast entry and re-encodes it. As the result of the check does not depend on the chunks used, either every correct validator adopts ρ (if the check passes) or every correct validator adopts ⊥ (if it fails). In all cases, all correct validators that input a meta-block input the same value, namely the checked value of v, for pj . Strong unanimity now ensures that no correct validator outputs empty for pj , while obligation ensures that the output value for pj was input by a correct validator. Hence, y[j] is the checked value of v, that is, y[j] = x[j]. In every case, x[j] = y[j]: the two validators finalize the same meta-block, and therefore the same block, which concludes the proof. ⊔ ⊓ Lemma 2 (Speculation). In Quantum Chorus, if a correct validator speculatively finalizes a block that differs from the block that a correct validator finalizes, then the misbehavior of at least one faulty validator can be proven.

A. PROOFS FOR QUANTUM CHORUS

21

Proof. Suppose a correct validator ps speculatively finalizes a meta-block x, and fix a proposer pj . Let v be the value of the fast entry of ps for pj , a Merkle root or ⊥, and let v̂ be its checked value, so that x[j] = v̂ (line 62). Throughout the proof, we say that a Vote message matches v if its entry for pj is ⟨j, v⟩: a positive entry for v when v is a root, and a negative entry when v = ⊥. The speculation rests on 2f + 1 Vote messages matching v, sent by 2f + 1 distinct validators, and ps holds all of them (lines 49, 50, and 62). A finalization through the halting gadget repeats one on the fast path or on the fallback path (Claim 1), so it suffices to consider these two paths. Observe first that every fast-path finalization rests, for pj , on fast entries for v, and thus finalizes v̂ for pj . Namely, a fast-path finalization rests on 2f + 1 PathVotes whose entries for pj are fast entries for the same value, and at least one of them comes from a correct validator. That validator issued its fast entry upon receiving 2f + 1 Vote messages matching the entry’s value, while ps holds 2f + 1 Vote messages matching v. The two sets of senders intersect in a correct validator, which sent a single Vote (Lemma 6), so the fast entry is for v. A reversion, therefore, can only originate from the fallback path. On the fallback path, the proof relies on signatures. A Vote message is signed by its sender as a whole: it carries a single signature over the entire vector of entries. Consequently, two Vote messages from the same validator whose entries for pj differ are two distinct messages signed by that validator, which is a transferable proof of its misbehavior. In particular, if f + 1 distinct validators send Vote messages that do not match v, then, as (f + 1) + (2f + 1) = 3f + 2 > n, one of them also sent one of the 2f + 1 Votes matching v that ps holds, and whoever holds the two messages holds the proof. The argument below produces exactly such a pair of sets: the 2f + 1 matching Votes held by ps , and f + 1 non-matching Votes held by some correct validator. We claim that, short of provable misbehavior, no correct validator inputs to the fallback consensus a value y for pj with y ̸= v̂. Strong unanimity and obligation, applied to proposer pj , then ensure that the fallback consensus outputs v̂, and the lemma follows: every correct validator that inputs a meta-block inputs v̂ for pj , so strong unanimity rules out empty, and obligation gives v̂. As pj is arbitrary and x[j] = v̂, every meta-block that a correct validator finalizes is x unless misbehavior can be proven, and its block is then the block that ps speculatively finalized. To prove this claim, suppose that a correct validator pi inputs a value y for pj with y ̸= v̂, and recall the three ways in which it may have adopted y (line 68). This implies that y ̸= v: a root that a correct validator inputs passes the check, as the paragraph on data availability shows, so y = v would give v̂ = v = y. In each of the three scenarios below, we show that some correct validator holds f + 1 Vote messages that do not match v, which gives the proof of misbehavior described above. – In the first scenario, pi ’s clean set for pj holds a fast entry for y, and y is either ⊥ or a root that passed the decode–re-encode check. For that fast entry to enter the clean set, it had to be accepted: pi received f + 1 Vote messages matching y (line 18). As y ̸= v, these messages do not match v, and pi holds them. – In the second scenario, pi ’s clean set holds a fast entry for a root ρ that failed the check, so pi adopted y = ⊥. If ρ ̸= v, the f + 1 Votes that corroborated the fast entry do not match v, and pi holds them. If ρ = v, then v fails the check as well, as its result does not depend on the chunks used, so v̂ = ⊥ = y, which contradicts y ̸= v̂. – In the third scenario, pi ’s clean set consists of fallback entries alone. If y is a root, the clean set holds f + 1 fallback entries for y, at least one issued by a correct validator pw , which issued it only upon receiving f + 1 Vote messages with a positive entry for y (line 51). As y ̸= v, these f + 1 messages do not match v, and pw holds them. If y = ⊥, then v̂ ̸= ⊥: v is a root ρ with a valid encoding. Moreover, fewer than f + 1 fallback entries of the clean set carry ρ, for otherwise pi would have adopted ρ. The clean set holds 2f + 1 entries from distinct validators, of which at least f + 1 come from correct validators, so some correct validator pw issued a fallback entry for pj that does not carry ρ. Consider the Vote messages that pw held when it issued its PathVote, at least 2f + 1 of them (line 58). We claim that at least f + 1 of them are not positive for ρ. If they hold fewer than f + 1 positive entries for ρ, the claim is immediate. Otherwise, they hold f + 1 positive entries for ρ. As the encoding is valid, decoding them would have yielded a fallback entry for ρ, which pw did not issue. The rule (line 51) allows this only if pw decoded another root instead, that is, only if some ρ′ ̸= ρ also gathered f + 1 positive entries at pw . Those f + 1 messages, positive for ρ′ , are not positive for ρ. In both cases, pw holds f + 1 Vote messages that do not match v, as required. In every case that does not contradict y ̸= v̂, a correct validator holds f +1 signed Vote messages that do not match v, while ps holds 2f + 1 signed Vote messages that do. Both sets remain in persistent memory

22

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

across crashes. Together, the two sets expose a validator that signed two different Vote messages, which is precisely the misbehavior the lemma promises to prove. ⊔ ⊓ Lemma 3 (Proposal inclusion). Quantum Chorus satisfies proposal inclusion: if the slot is timely, the finalized block contains the proposals of all correct proposers. Proof. Fix a correct proposer pj . Let ρj denote the Merkle root of pj ’s proposal. Every correct validator receives its chunk, with a valid Merkle proof under ρj and a header signed by pj , by the deadline, while it participates: as the slot is timely, pj initiates its send upon starting, by time D − ∆ ≥ GST (line 36), and never abandons it, and every correct validator participates from D − ∆ on, so the delay bound of Section 3 delivers the chunk during [D − ∆, D], and the validator records it (line 37) unless it has halted by then. As channels are authenticated and pj sends each validator a single chunk, every Vote that a correct validator broadcasts thus includes a positive entry ⟨j, ρj ⟩. Hence, every fast entry for pj that a correct validator issues names ρj : it rests on 2f + 1 Votes with matching entries for pj , at least f + 1 of them from correct validators. Moreover, as pj is correct, its encoding is valid: any f + 1 chunks under ρj decode to its proposal, which re-encodes to ρj . It suffices to show that every meta-block x that a correct validator finalizes satisfies x[j] = ρj , as the block of such a meta-block contains the proposal of pj . Consider first a correct validator finalizing a meta-block x on the fast path. It holds 2f +1 PathVotes whose entry for pj is a fast entry for some value v whose checked value is x[j]. At least one of them comes from a correct validator, whose fast entry for pj names ρj . Hence, v = ρj , and, as the encoding is valid, x[j] = ρj . The fallback path is no more accommodating. First, no correct validator ever accepts a fast entry for pj naming a value y ̸= ρj : acceptance requires f + 1 Votes whose entry for pj matches y, whereas every correct validator’s entry for pj is positive for ρj , leaving at most f such Votes. Second, every fallback entry for pj that a correct validator issues names ρj : the validator holds at least 2f + 1 Votes, at least f + 1 of them from correct validators and thus positive for ρj , and only the at most f Byzantine validators can send Votes that are not positive for ρj , whether negative or positive for another root (a Vote carries no header signed by the proposer, so the checks of line 15 allow any root), so no other root reaches f + 1 positive entries. It therefore decodes the proposal from chunks under ρj , and the proposal re-encodes to ρj . Consequently, every set of 2f + 1 accepted entries for pj from different validators is clean, its fast entries name ρj , and at least f + 1 of its entries, those from correct validators, are fast or fallback entries for ρj . The adoption rule therefore returns ρj for every correct validator’s clean set for pj : if the set holds a fast entry, the entry names ρj , and the decode–re-encode check passes, the encoding being valid; otherwise, at least f + 1 of its fallback entries, those from correct validators, name ρj , and only the at most f entries from Byzantine validators can name another root or ⊥, so no other root reaches f + 1 entries. Every correct validator thus adopts ρj for pj , and inputs a meta-block whose entry for pj is ρj , if it inputs one. Strong unanimity for proposer pj ensures that no correct validator outputs empty for pj , and obligation ensures that the output value for pj was input by a correct validator. Hence, the output meta-block x satisfies x[j] = ρj . A finalization through the halting gadget repeats one on the two paths (Claim 1), so its meta-block satisfies this as well. In both cases, every meta-block x that a correct validator finalizes satisfies x[j] = ρj , and its block contains the proposal of pj . ⊔ ⊓ Once a correct validator halts, the halting gadget makes every correct validator that participates finalize; the proofs of termination and accountability below use this. Claim 2 (Finalization after a halt). If a correct validator halts at time H, then every correct validator that starts participating at time S finalizes by time max(S, H, GST) + ∆. Proof. By time H, the halting validator received ⟨Finalized, x⟩ messages, for some meta-block x, from 2f + 1 validators, at least f + 1 of them correct (line 76). These correct validators initiated their broadcasts by time H and never abandon them. By the delay bound of Section 3 with τ = max(S, H), a correct validator that starts participating at time S therefore receives their messages during [max(S, H, GST), max(S, H, GST)+∆]. This interval starts no earlier than S, so the validator participates when the messages arrive, unless it has halted. A correct validator that has halted by then has finalized, as it finalizes when it halts. Any other correct validator keeps the messages in persistent memory, and thus holds f + 1 of them by time max(S, H, GST) + ∆ and finalizes by then (line 74). ⊔ ⊓ Lemma 4 (Termination). Quantum Chorus satisfies termination: if every correct validator starts participating in the slot, every correct validator eventually finalizes a block for the slot.

A. PROOFS FOR QUANTUM CHORUS

23

Proof. If some correct validator halts, every correct validator finalizes by Claim 2, as it eventually participates. Otherwise, no correct validator halts, so that all of them keep taking part in the fallback consensus, and it suffices to prove that every correct validator eventually inputs a meta-block to the fallback consensus: from there, the termination of the fallback consensus carries the day, as a correct validator finalizes the output meta-block (line 73). We prove this below. Every correct validator eventually participates and broadcasts a Vote (line 46), so every correct validator eventually holds 2f + 1 Votes and, once time reaches D + ∆ (or earlier, see Step 3), forms an entry for every proposer and broadcasts its PathVote (line 58). Fix a proposer pj . Crucially, if a correct validator issues a fast entry for pj , then every correct validator eventually accepts it. Namely, the issuer formed its fast entry upon receiving 2f + 1 Votes whose entry for pj matches the fast entry, at least f + 1 of which come from correct validators, and correct validators keep their Vote broadcasts foreveralive. The f + 1 corroborating Votes thus eventually reach every correct validator, and the fast entry is accepted (line 18). Fallback entries, recall, are accepted the moment they are received. Consequently, every correct validator eventually accepts the entries for pj of all correct validators, of which there are at least 2f + 1. Once that happens, if not before, the accepted entries for pj contain a clean set. Indeed, no two correct validators issue fast entries for pj naming different values: each rests on 2f + 1 Votes with matching entries for pj , and two such sets of Votes intersect in a correct validator, which sent a single Vote and thus a single entry for pj . The entries of the correct validators for pj thus form a set of 2f + 1 accepted entries whose fast entries all agree: a clean set. Hence, every correct validator eventually holds a clean set for every proposer, and, once time has reached D + 2∆, adopts a value for each of them (line 68). The adoption rule is a local computation that always completes: where it calls for decoding, the f + 1 chunks it needs arrived with the Votes that corroborated the fast entry in question. Every correct validator therefore inputs a meta-block to the fallback consensus, which is all we needed. ⊔ ⊓ Lemma 5 (Halting). If every correct validator starts participating in the slot, every correct validator eventually halts. Moreover, if every correct validator has finalized by time T , every correct validator halts by time max(T, GST) + ∆. Proof. For the time bound, suppose that every correct validator has finalized by time T . All correct validators finalize the same meta-block x (see the proof of Lemma 1), and each of them broadcasts ⟨Finalized, x⟩ when it finalizes. By time T , the at least 2f + 1 correct validators have thus initiated these broadcasts, which are forever-alive and so reach every correct validator by time max(T, GST) + ∆. A correct validator that has not halted by then holds ⟨Finalized, x⟩ from 2f + 1 validators, participates, as it has finalized, and halts by that time (line 76). For the first statement, if every correct validator starts participating in the slot, every correct validator eventually finalizes (Lemma 4), so there is a time T by which all of them have, and the bound applies. ⊔ ⊓ A.2

Complexity

Lemma 6 (Message complexity & signature count). In Quantum Chorus, every message that a correct validator sends in dissemination ( Chunk) or in voting ( Vote and PathVote) carries exactly one signature. Moreover, a correct validator initiates at most one broadcast of a Vote, at most one of a PathVote, and at most one of a Finalized message, and, if it is a proposer, initiates at most one Chunk send to each validator, retransmissions aside. Proof. We inspect the three message types (Algorithm 1). A Chunk carries the proposer’s signature on its header ⟨j, ρj ⟩, together with a symbol and a Merkle proof. A Vote carries the sender’s single signature over its entire vector of entries. Its entries are unsigned, and the chunks attached to positive entries consist of a root, a symbol, and a Merkle proof: the proposer’s signed header, which the sender verified upon receiving the chunk, is stored locally and never forwarded (line 46). A PathVote only carries the sender’s single signature over its entire vector of entries (line 58). As for the number of messages, Step 1 runs at most once at each proposer and sends one Chunk to each validator (line 36). Step 2 runs at most once and broadcasts one Vote (line 46). Step 3 runs at most once and broadcasts one PathVote (line 58). No rule initiates any of these sends or broadcasts a second time, also after recovery. Retransmissions repeat a send or broadcast that was already initiated, and the counts exclude them. The halting gadget adds at most one Finalized message per correct validator, which carries no signature. ⊓ ⊔

24

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

A.3

Accountability

Lemma 7 (Accountability under ⌊f /2⌋ faults). Suppose that the slot is timely and that at most ⌊f /2⌋ validators are Byzantine. If some correct validator has not finalized by time D + 2∆, then there exists a proposer pj such that the correct validators collectively hold either (1) two Chunk messages signed by pj that carry different roots, or (2) a Chunk message signed by pj together with at least ⌊f /2⌋ + 1 Vote messages, from different validators, whose entry for pj is negative. Proof. As the slot is timely, every correct validator starts participating in it by time D − ∆ ≥ GST, and none crashes from then on (Section 3). Let t ≤ ⌊f /2⌋ denote the number of Byzantine validators, so that at least n − t ≥ 2f + 1 + ⌈f /2⌉ validators are correct. We first show that halting does not interfere with the argument below. If some correct validator halts by time D + ∆, every correct validator finalizes by D + 2∆ (Claim 2, as GST ≤ D − ∆ and every correct validator starts participating by D − ∆), and there is nothing to prove. Otherwise, no correct validator halts by D + ∆, and every correct validator broadcasts its PathVote by then, as used below. A correct validator that halts later has finalized before halting; in particular, a correct validator that has not finalized by D + 2∆ has not halted by then. Next, we show that some correct validator pw issued a fallback entry for some proposer pj . Let pi be a correct validator that has not finalized by time D + 2∆, and hence has not halted by then. As the slot is timely, pi has received, by time D + 2∆, the PathVotes of all correct validators, broadcast by time D + ∆. If, for every proposer, the entries of all correct validators were fast entries naming the same value, pi would hold, for every proposer, n − t ≥ 2f + 1 PathVotes with matching fast entries, and would finalize by time D + 2∆ (line 65), the chunks it needs having arrived with the Votes by D + ∆, contrary to its choice. Hence, for some proposer pj , either two correct validators issued fast entries for pj naming different values, or some correct validator issued a fallback entry for pj . The former is impossible: each of the two fast entries rests on 2f + 1 Votes whose entries for pj match its value, the two sets of senders share at least (2f + 1) + (2f + 1) − n = f + 1 > t validators, hence a correct one, and a correct validator sends a single Vote, and thus a single entry for pj . Therefore, some correct validator pw issued a fallback entry for pj . We now examine what pw saw. As pw issued a fallback entry, it formed its path vote at time D + ∆, since a path vote formed earlier holds fast entries only. As the slot is timely, by time D + ∆, pw has received the Votes of all n − t correct validators, broadcast by time D. Let P denote the number of these Votes whose entry for pj is positive, and N the number whose entry for pj is negative, so that P + N = n − t ≥ 2f + 1 + ⌈f /2⌉. As pw issued a fallback entry for pj , it observed fewer than 2f + 1 negative entries for pj , and, for every root ρ, fewer than 2f + 1 positive entries naming ρ (lines 49 and 50). In particular, N ≤ 2f , hence P ≥ ⌈f /2⌉ + 1 ≥ 1: some correct validator formed a positive entry for pj , which it does only upon receiving a Chunk whose header is signed by pj (line 37), and which it stores. The correct validators thus hold a Chunk signed by pj . Two cases remain. – If the positive entries of correct validators for pj name two different roots, then two correct validators hold Chunk messages signed by pj with different roots: this is item (1). – Otherwise, all P positive entries name the same root ρ, so P ≤ 2f , and N = (n − t) − P ≥ 2f + 1 + ⌈f /2⌉ − 2f = ⌈f /2⌉ + 1 ≥ ⌊f /2⌋ + 1. These N Votes come from different correct validators, are signed by their senders, and pw holds them, as it received the Votes of all correct validators by D + ∆: together with the Chunk above, this is item (2). ⊔ ⊓ Lemma 8 (Accountability under f faults). Suppose that Quantum Chorus runs with Coda as its fallback consensus and that the slot is timely. If some correct validator has not finalized by time D+4∆, then there exists a proposer pj such that either some correct validator holds 2f + 1 PathVote messages, from different validators, whose entry for pj is a fallback entry, or two correct validators together hold two Vote messages signed by the same validator whose entries for pj differ. Proof. As the slot is timely, every correct validator starts participating in it by time D − ∆ ≥ GST, and none crashes from then on (Section 3). At least 2f + 1 validators are correct. We first show that halting does not interfere with the argument below. If some correct validator halts by time D + 3∆, every correct validator finalizes by D + 4∆ (Claim 2, as GST ≤ D − ∆ and every correct validator starts participating by D − ∆), and there is nothing to prove. Otherwise, no correct validator halts by D + 3∆, and the broadcasts below are made by then. A correct validator that halts later has finalized before halting; in particular, a correct validator that has not finalized by D + 4∆ has not halted by then. Next, we pin down the timeline. Every correct validator broadcasts its Vote by time D and its PathVote by time D + ∆, and every correct validator receives them by times D + ∆ and D + 2∆,

B. PROOFS FOR CODA

25

respectively. By time D + 2∆, moreover, every correct validator has accepted every entry of every correct PathVote: fallback entries are accepted on receipt, and a correct fast entry is corroborated by f + 1 correct Votes that arrived by D + ∆. As in the proof of termination, the entries of the correct validators form a clean set for every proposer, so every correct validator adopts a meta-block and inputs it to the fallback consensus at time D + 2∆ (line 70). The pre-fallback broadcasts are forever-alive, and the view-1 broadcasts of Coda remain alive through D + 4∆: as all correct validators enter view 1 at time D + 2∆, none enters a higher view before D + 7∆ (by the proof of Claim 14, which applies unchanged when validators halt), and a validator abandons a broadcast of Coda only upon entering a higher view (line 15), not when it decides or halts. Suppose that all correct validators input the same meta-block a. Upon entering the leaderless view 1 at time D + 2∆, every correct validator broadcasts ⟨vote-1, 1, a⟩ (Algorithm 2). By time D + 3∆, every correct validator has received 2f + 1 such messages, locks a, and broadcasts ⟨vote-2, 1, a, ·⟩. By time D + 4∆, every correct validator has received 2f + 1 vote-2 messages with lock a (line 41), and finalizes. Consequently, if some correct validator has not finalized by time D + 4∆, the inputs of the correct validators are not all identical: two correct validators pi and pk adopted different values for some proposer pj . We fix this pj and distinguish two cases, according to the fast entries for pj issued by correct validators. Recall that all such fast entries name the same value v: each rests on 2f + 1 Votes matching it, and two such sets of Votes intersect in a correct validator, which sent a single Vote. – No correct validator issued a fast entry for pj . Then all 2f + 1 or more correct validators issued fallback entries for pj , and, by time D + 2∆, every correct validator holds their signed PathVotes: the conclusion of the lemma. – Some correct validator pc issued a fast entry for pj , naming v. If the clean set of pi or of pk for pj consists of fallback entries alone, that validator holds 2f + 1 signed PathVotes, from different validators, with fallback entries for pj : the conclusion of the lemma. Otherwise, both clean sets hold fast entries, naming values ui and uk . Adopting from a fast entry is a deterministic function of the value it names (line 68): ⊥ is adopted as ⊥, and a root is adopted as itself if the decode–re-encode check passes and as ⊥ if it fails, where the result of the check depends only on the root: every f + 1 chunks under a valid encoding decode to the same proposal, and no chunks under an invalid one re-encode to it. Had ui = uk , the two validators would therefore have adopted the same value, decoding failure or not. Hence ui ̸= uk , and at least one of them, say ui , differs from v. The fast entry for ui was accepted by pi , which therefore holds f + 1 Votes, from different validators, matching ui (line 18). Meanwhile, pc holds 2f + 1 Votes, from different validators, matching v. As (f + 1) + (2f + 1) = 3f + 2 > n, some validator sent both a Vote matching ui and a Vote matching v, that is, two Votes with different entries for pj . Validators pi and pc together hold them: two Votes signed by the same validator that differ, a transferable proof of that validator’s misbehavior. ⊓ ⊔

B

Proofs for Coda

This appendix proves the guarantees of Coda stated in Section 5.2, under the model and conventions of Section 5.1. B.1

Core Properties

The proofs of agreement, strong unanimity, and obligation allow correct validators to stop taking part in Coda (Section 5.1). They reason only about the events that correct validators cause: the messages they broadcast and accept, the views they enter, the variables they write, and their decisions. They trace each such event to the rule that caused it and to messages received, or events that occurred, before it, and none of them uses that a correct validator keeps running, which only the termination proofs assume. A validator that stops taking part causes no events from then on: it executes no handler, and its retransmissions repeat messages it broadcast before. We start by proving that Coda satisfies agreement. Agreement. We begin with a few structural observations about Coda, and then prove agreement. The first observation is that the current view of a correct validator only grows. Claim 3. If a correct validator pi enters a view V1 ≥ 1 at some time, and enters a view V2 ≥ 1 at a later time, then V2 > V1 .

26

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

Proof. Validator pi updates view i exactly when it enters a view, setting view i to the entered view (line 30). Views are entered at three places only. The first is line 28, upon starting, which happens once and precedes every other entry. The second is line 55, which enters a view V +1 under the condition V ≥ view i (line 53). The third is line 59, which enters a view V under the condition V > view i (line 57). The last two thus enter a view greater than view i . Recovery preserves view i and does not repeat initialization. Hence, V2 > V1 . ⊔ ⊓ Next, we show that a correct validator commits to a single vote of each kind per view, and that its lock, once set, is the one its vote-2 message carries. Claim 4. Let pi be a correct validator, and let V ≥ 1 be a view. Then: 1. Validator pi writes vote1 i [V ], vote2 i [V ], and lock i [V ] only at times at which view i = V , and at most once each. 2. Validator pi broadcasts at most one ⟨vote-1, V, ·⟩ and at most one ⟨vote-2, V, ·, ·⟩ message, each at a time at which view i = V . 3. If pi broadcasts ⟨vote-2, V, x, G⟩, then x is the value of lock i [V ] and G is the value of guard i [V ] at the time of the broadcast, and lock i [V ] = x holds from that time onward. Proof. We first prove part (1). The variable vote1 i [V ] is written at line 32, within the handler that enters view V = 1 and hence after view i is set to 1 (line 30), and at line 36, which acts on view view i . The two sites are mutually exclusive: the second belongs to a rule triggered by a prepare message from leader(view i ) (line 34), whereas view 1 has no leader (line 31). The first site is reached only once, as view 1 is entered only once (Claim 3), and the second is guarded by vote1 i [view i ] = none (line 35). The variable vote2 i [V ] is written at line 40 and at line 45. Both sites act on view view i , and both are guarded by vote2 i [view i ] = none (lines 38 and 44). The variable lock i [V ] is written at line 39 alone, within the same handler and under the same guard. It remains to observe that these variables are never reset: the only mechanism that discards them is the memory rule (line 14), which discards the variables of a view once it falls below view i − 1. By Claim 3, such a view is never entered again, and, as shown above, the variables of a view other than view i are never written. Part (2) follows: each of these write sites broadcasts the message it has just written, while view i = V by part (1) (lines 32, 36, 40, and 45), and no other line of Coda broadcasts a vote-1 or a vote-2 message. Part (3) follows as well. Both sites that create a vote-2 message for view V fill it with the current value of guard i [V ]. The site at line 40 fills in the current value of lock i [V ], and the site at line 45 fills in none, which is the current value of lock i [V ] there: lock i [V ] is written only in the handler that also writes vote2 i [V ] (line 39), and vote2 i [V ] = none at the timeout site (line 44). By part (1), lock i [V ] is never written again. ⊔ ⊓ The next two claims trace the values that correct validators vote for, and the locks that they accept, back to their origin. Claim 5. If a correct validator pi broadcasts ⟨vote-1, V, x⟩ for a view V > 1, then, for every proposer pj , validator pi has received f + 1 messages ⟨echo, V − 1, j, x[j]⟩ from distinct validators. Proof. As established in the proof of Claim 4, the only site that creates a vote-1 message for a view V > 1 is line 36, and its rule is triggered only by a message ⟨prepare, view i , x⟩ that is justified (line 34), where view i = V . A meta-block x is justified only if, for every proposer pj , the validator has received f + 1 messages ⟨echo, V − 1, j, x[j]⟩ from distinct validators (line 25). ⊔ ⊓ Claim 6. If a correct validator accepts a message ⟨vote-2, V, x, ·⟩ with x ̸= none, then some correct validator has broadcast ⟨vote-1, V, x⟩. Proof. Such a message is accepted only once its recipient has received f + 1 messages ⟨vote-1, V, x⟩ from distinct validators (line 17), at most f of which are faulty. ⊓ ⊔ We now introduce the first decision of the execution. If no correct validator ever decides, agreement holds vacuously. We therefore assume throughout the remainder of the agreement proof that some correct validator does decide. We say that a correct validator decides in view V if it triggers decide on the strength of 2f + 1 ⟨vote-2, V, ·, ·⟩ messages (line 41). Its current view is then V or V + 1. Definition 1 (View Vdec ). Let Vdec denote the smallest view in which a correct validator decides.

B. PROOFS FOR CODA

27

Before naming the meta-block that view Vdec decides, we check that there is only one. Claim 7. If a correct validator decides a meta-block x1 in view Vdec , and a correct validator decides a meta-block x2 in view Vdec , then x1 = x2 . Proof. Each of the two decisions requires the receipt of 2f + 1 ⟨vote-2, Vdec , ·, ·⟩ messages carrying the decided meta-block, from distinct senders (line 41). As n = 3f + 1, the two sets of senders share at least 2(2f + 1) − n = f + 1 validators, at least one of which is correct. By Claim 4(2), that validator broadcasts a single vote-2 message for view Vdec , which implies x1 = x2 . ⊔ ⊓ We may therefore speak of the meta-block that view Vdec decides. Definition 2 (Meta-block vdec ). Let vdec denote the meta-block decided by a correct validator in view Vdec . The following claim is the counting heart of the proof. A decision in view Vdec leaves behind a residue of correct vote-2 messages so large that no quorum of vote-2 messages for view Vdec can avoid it, however it is assembled. Claim 8. Let D denote the set of correct validators that broadcast ⟨vote-2, Vdec , vdec , ·⟩. Then: – |D| ≥ f + 1. – Every set of 2f + 1 ⟨vote-2, Vdec , ·, ·⟩ messages from distinct senders contains a message broadcast by a member of D. Proof. Let b ≤ f denote the number of validators that are faulty in the execution under consideration. The decision on vdec in view Vdec requires the receipt of 2f + 1 ⟨vote-2, Vdec , vdec , ·⟩ messages from distinct senders (line 41), at most b of which are faulty. The rest were broadcast by correct validators, which therefore belong to D. Thus, |D| ≥ 2f + 1 − b ≥ f + 1. Now, consider any set S of 2f +1 ⟨vote-2, Vdec , ·, ·⟩ messages from distinct senders. At most f +b ≤ 2f validators lie outside D: the b faulty ones, and the at most (n − b) − |D| ≤ (3f + 1 − b) − (2f + 1 − b) = f correct ones. As S has 2f + 1 distinct senders, at least one of them belongs to D. By Claim 4(2), that validator broadcasts a single vote-2 message for view Vdec , namely ⟨vote-2, Vdec , vdec , ·⟩, which is thus the message of S that it sent. ⊔ ⊓ We are ready for the central claim of the agreement proof: once view Vdec has decided vdec , no correct validator ever echoes, or votes for, anything else. Claim 9. Let m be a message broadcast by a correct validator pi . Then: 1. If m = ⟨echo, V, j, v⟩ with V ≥ Vdec , then v = vdec [j]. 2. If m = ⟨vote-1, V, x⟩ with V > Vdec , then x = vdec . Moreover, guard i [V ] = vdec holds at every time at which view i = V > Vdec . Proof. We proceed by induction on the order of the events of interest at correct validators, namely the broadcasts covered by the claim and the entries into views greater than Vdec . Fix such an event, and suppose that the claim holds for every event that precedes it. We establish the claim through three subclaims. Subclaim 1 If a correct validator pi enters a view W > Vdec , then guard i [W ] = vdec from that moment onward. Proof of Subclaim 1. As W > Vdec ≥ 1, validator pi enters view W at line 55 or at line 59, and sets its guard for W to a meta-block x (line 54 or 58). In the former case, W = V + 1 for a view V ≥ Vdec , and, for every proposer pj , a set of 2f + 1 messages ⟨echo, V, j, x[j]⟩ from distinct senders exists (line 53), at least f + 1 of them broadcast by correct validators. In the latter case, for every proposer pj , a set of f + 1 messages ⟨echo, W, j, x[j]⟩ from distinct senders exists (line 57), at least one of them broadcast by a correct validator, and W ≥ Vdec . Either way, for every proposer pj , some correct validator broadcast an echo for x[j], for a view at least Vdec , before the entry. The induction hypothesis (part 1) yields x[j] = vdec [j]. As this holds for every proposer, x = vdec , and the entry sets guard i [W ] ← vdec . No other line writes guard i [W ]: guards are written upon entering a view alone, and view W is entered once (Claim 3), which concludes the proof. ⋄ Subclaim 2 If m = ⟨vote-1, V, x⟩ with V > Vdec , then x = vdec .

28

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

Proof of Subclaim 2. As V > Vdec ≥ 1, Claim 5 applies: for every proposer pj , validator pi has received f + 1 messages ⟨echo, V − 1, j, x[j]⟩ from distinct validators, at least one of which was broadcast by a correct validator. As V −1 ≥ Vdec , the induction hypothesis (part 1) gives x[j] = vdec [j] for every proposer pj , that is, x = vdec . ⋄ Subclaim 3 If m = ⟨echo, V, j, v⟩ with V ≥ Vdec , then v = vdec [j]. Proof of Subclaim 3. Echo messages are broadcast at line 23 alone, so pi broadcasts m upon an invocation of echo(V, pj , v), of which Coda has two sources. – The amplification rule (line 61) requires a set of f + 1 messages ⟨echo, V, j, v⟩ from distinct senders, at least one of which was broadcast by a correct validator, and thus earlier. The induction hypothesis (part 1) gives v = vdec [j]. – The view-change rule (line 47) is triggered while view i = V by a set S of 2f +1 accepted ⟨vote-2, V, ·, ·⟩ messages, from distinct senders, whose non-none locks are all identical. The rule echoes for every proposer at once. We fix the proposer pj of m and distinguish two cases. • Case V = Vdec . By Claim 8, the set S contains a message ⟨vote-2, Vdec , vdec , ·⟩ broadcast by a correct validator. Hence, S contains a non-none lock, so the rule takes its first branch (line 48) and echoes ℓ[j] for the lock ℓ it exhibits. As all non-none locks in S are identical, ℓ = vdec , and thus v = vdec [j]. • Case V > Vdec . At least f + 1 messages of S were broadcast by correct validators. Each was broadcast at a time at which its sender’s current view was V (Claim 4(2)), and thus carries the guard of its sender at that time, whose entry for pj is vdec [j] (Claim 4(3) and the induction hypothesis, applied to that sender’s entry into view V ). We distinguish the branch the rule takes. ∗ The first branch (line 48) echoes ℓ[j] for a non-none lock ℓ of an accepted message of S. By Claim 6, some correct validator broadcast ⟨vote-1, V, ℓ⟩, so ℓ = vdec by the induction hypothesis (part 2), and thus v = vdec [j]. ∗ The second branch (line 50) is reached otherwise. Its condition asks for a value that is the entry for pj in the guards of f + 1 messages of S, and vdec [j] is such a value: as established above, at least f + 1 messages of S carry a guard whose entry for pj is vdec [j]. It is the only such value, as two values would require 2f +2 > |S| messages; hence v = vdec [j]. The condition therefore holds, and the last branch, which echoes empty, is not taken (line 52). ⋄ The three subclaims cover every event of interest, which completes the induction.

⊔ ⊓

Agreement now follows. Lemma 11 (Agreement). Coda (Algorithm 2) satisfies agreement. Proof. As Vdec is the smallest view in which a correct validator decides, it suffices to prove that no correct validator decides a meta-block other than vdec in a view V ≥ Vdec . For V = Vdec , this is Claim 7. Hence, let V > Vdec , and suppose that a correct validator decides a meta-block y ̸= none in view V . The decision requires the receipt of 2f + 1 messages ⟨vote-2, V, y, ·⟩ from distinct senders (line 41), at least one of which was broadcast by a correct validator pw . By Claim 4(3), lock w [V ] = y ̸= none, which is set only upon the receipt of 2f + 1 messages ⟨vote-1, V, y⟩ from distinct senders (lines 37 and 39), at least one of which was broadcast by a correct validator. By Claim 9(2), y = vdec , which concludes the proof. ⊔ ⊓ Termination. Termination assumes that every correct validator starts Coda and none stops taking part, and its proofs also assume that every correct validator starts by GST (the participation convention of Section 5.2). We first establish that correct validators keep advancing through views, and then that the first post-GST view with a correct leader decides. Where the proofs below speak of the 2f + 1 correct validators, they mean an arbitrary but fixed set of 2f + 1 correct validators, in case there are more. The following two claims tie echoes and view entries to one another. Claim 10. If a correct validator broadcasts ⟨echo, V, j, v⟩ for a view V ≥ 1, then some correct validator has previously entered view V . Proof. We first observe that a correct validator broadcasts an echo message for view V only while its current view is at least V : the view-change rule (line 47) echoes for view view i , and the amplification rule (line 61) echoes only for views view i − 1 and view i . As view i is set to a view only upon entering it (line 30), the sender of such a message has entered a view at least V beforehand.

B. PROOFS FOR CODA

29

Let E ⋆ denote the first entry by a correct validator into a view at least V , and let Y ≥ V be the entered view. It suffices to show that Y = V . If Y = 1, then E ⋆ is an initial entry (line 28), and Y = V follows from 1 = Y ≥ V ≥ 1. Otherwise, Y > 1, so E ⋆ occurs at line 55 or at line 59, the only two places where a view other than view 1 is entered. It does not occur at the latter: the catch-up rule requires f + 1 ⟨echo, Y, ·, ·⟩ messages from distinct senders (line 57), one of which was broadcast by a correct validator, and thus before E ⋆ , while that validator’s view was at least Y ≥ V . That validator thus entered a view at least V before E ⋆ , contradicting the minimality of E ⋆ . Hence, E ⋆ occurs at line 55, which requires 2f + 1 ⟨echo, Y − 1, ·, ·⟩ messages from distinct senders (line 53), at least f + 1 of them broadcast by correct validators before E ⋆ , while their views were at least Y − 1. By the minimality of E ⋆ , Y − 1 < V , and, as Y ≥V, Y =V. ⊔ ⊓ Claim 11. If a correct validator enters a view W > 1, then the first such entry occurs at line 55, and some correct validator has previously entered view W − 1. Proof. Let E denote the first entry by a correct validator into view W . As W > 1, it occurs at line 55 or at line 59. It does not occur at the latter: the catch-up rule requires f + 1 ⟨echo, W, ·, ·⟩ messages from distinct senders (line 57), one of which was broadcast by a correct validator, and, by Claim 10, some correct validator entered view W before that broadcast, hence before E, a contradiction. Therefore, E occurs at line 55, which requires a set of 2f +1 ⟨echo, W −1, ·, ·⟩ messages from distinct senders (line 53), at least f + 1 of which were broadcast by correct validators before E. Claim 10 then places an entry into view W − 1 before those broadcasts. ⊔ ⊓ Next, we record which messages survive on an unreliable network. Recall that a broadcast is abandoned only upon a view entry, and only for messages outside the two-view window that the entry retains (line 15). Claim 12. Let V ≥ 1 be a view such that no correct validator ever enters a view greater than V . Then every vote-1, vote-2 and echo message for view V or view V − 1 broadcast by a correct validator is forever-alive, and is therefore eventually received by every correct validator. Proof. Let m be such a message, for a view W ∈ {V − 1, V }, broadcast by a correct validator pi . Its broadcast is initiated by hypothesis, so it suffices to show that it is never abandoned. The only mechanism that abandons broadcasts is the rule at line 15, which fires upon a view entry: entering a view W ′ abandons the ongoing broadcasts of the messages of views smaller than W ′ − 1. Consider the moment at which pi broadcasts m. Its current view is then W or W + 1: a vote-1 or vote-2 message for view W is broadcast while view i = W (Claim 4(2)), and an echo message for view W is broadcast by the view-change rule while view i = W (line 47), or by the amplification rule while W ∈ {view i − 1, view i } (line 61). As entered views only grow (Claim 3), every later entry of pi is into a view W ′ ≥ W + 1, and such an entry abandons the broadcast of m exactly when W is smaller than W ′ − 1. An entry into view W + 1 therefore spares m, and only an entry into a view W ′ ≥ W + 2 abandons it. Since W ≥ V − 1, such a view satisfies W ′ ≥ V + 1, and no correct validator ever enters a view greater than V by assumption. Hence, m is forever-alive, and its retransmissions eventually reach every correct validator, also after recovery or the start of participation. ⊔ ⊓ The next claim is the engine of progress: whenever correct validators would otherwise be stranded in a view, they all reach the same verdict about it and move on. Claim 13. For every view V ≥ 1, some correct validator eventually enters view V . Proof. Suppose, by contradiction, that some view is never entered by any correct validator. By Claim 11, the set of views entered by correct validators is closed downward, and every correct validator enters view 1 upon starting (line 28). Let Vmax be the greatest view that some correct validator enters. No correct validator ever enters a view greater than Vmax , so Claim 12 applies to views Vmax and Vmax − 1 throughout. Step 1: Every correct validator eventually enters view Vmax . If Vmax = 1, this holds by initialization. Otherwise, by Claim 11, the first entry into Vmax occurs at line 55, and thus rests on a set of 2f +1 messages ⟨echo, Vmax − 1, j, x[j]⟩ for every proposer pj and some meta-block x, at least f + 1 of them, for every proposer, from correct validators. These are forever-alive, so every correct validator eventually receives f + 1 of them for every proposer pj after its last recovery. A correct validator whose view is then at most Vmax − 2 enters view Vmax − 1 on the spot, through the catch-up rule (line 57, with V = Vmax − 1 > view i ). Hence, every correct validator pi is eventually in view Vmax −1 or view Vmax , so Vmax −1 ∈ {view i −1, view i } and the amplification rule fires (line 61): pi broadcasts ⟨echo, Vmax −1, j, x[j]⟩ for every proposer pj , unless it has done so already. Hence all 2f + 1 correct validators broadcast these echoes, which are forever-alive,

30

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

so every correct validator eventually holds 2f + 1 of them for every proposer. A correct validator whose view is then Vmax − 1 enters view Vmax at line 55 (with V = Vmax − 1 ≥ view i ), and one whose view is Vmax is there already. Step 2: Every correct validator broadcasts a single vote-2 message for view Vmax , and every correct validator eventually accepts all 2f + 1 of these messages. Every correct validator is in view Vmax forever, and its clock advances at the rate of real time from GST onward, so the timer of line 43 eventually reaches 5∆ and it broadcasts a vote-2 message for Vmax (line 45), unless it has broadcast one earlier (line 40). By Claim 4(2) this message is unique, and it is forever-alive. Let S ⋆ denote the set of these 2f + 1 messages. Every member of S ⋆ is eventually accepted by every correct validator: those carrying none upon reception (line 18), and one carrying a lock x ̸= none once f + 1 ⟨vote-1, Vmax , x⟩ messages arrive (line 17), which they do: its sender locked x upon receiving 2f + 1 such messages (line 39), at least f + 1 of them broadcast by correct validators and hence forever-alive. So every correct validator eventually holds S ⋆ , with every member accepted. Step 3: All correct validators echo a common value for every proposer. The set S ⋆ satisfies the condition of the view-change rule (line 47): it consists of 2f + 1 accepted ⟨vote-2, Vmax , ·, ·⟩ messages, and all of its non-none locks are identical. The latter holds because these locks are the locks of correct validators, and no two correct validators lock different meta-blocks in the same view. Indeed, two locks on different meta-blocks would require two sets of 2f + 1 vote-1 messages for view Vmax , from distinct senders each, sharing 2(2f + 1) − n = f + 1 senders, at least one of them correct and hence broadcasting two vote-1 messages for Vmax , contradicting Claim 4(2). Moreover, the gate of line 47 is eventually open at every correct validator, as every correct validator is in view Vmax forever and its clock advances after GST. The rule fires for every set that satisfies its condition (line 47), so it fires for S ⋆ at every correct validator, and S ⋆ is the same set at every correct validator. The values it echoes are determined by S ⋆ alone. If S ⋆ contains a lock ℓ, every correct validator echoes ℓ[j] for every proposer pj . Otherwise, for every proposer pj , at most one value is the entry for pj in the guards of f + 1 messages of S ⋆ , as two such values would require 2f + 2 > |S ⋆ | messages, and every correct validator echoes that value, or empty if there is none. Contradiction. These echoes are forever-alive, so every correct validator eventually holds 2f + 1 of them for every proposer and enters view Vmax + 1 (line 55), contradicting the maximality of Vmax . ⊔ ⊓ For every view V ≥ 1, let τ (V ) denote the earliest time at which a correct validator enters view V . It is well defined by Claim 13, and τ (V ) < τ (V + 1) by Claim 11. We call a view V a post-GST view if and only if τ (V ) ≥ GST. The gate of line 47 now buys us a floor on how quickly post-GST views can pass. Claim 14. For every post-GST view V ≥ 1, no correct validator broadcasts an echo message for view V before time τ (V ) + 5∆. Hence τ (V + 1) ≥ τ (V ) + 5∆. Proof. By Claim 11, the entry into view V + 1 at time τ (V + 1) occurs at line 55, and thus rests on 2f + 1 ⟨echo, V, ·, ·⟩ messages from distinct senders, at least one of which was broadcast by a correct validator before τ (V + 1). The first echo message for view V broadcast by a correct validator is not produced by the amplification rule (line 61), which presupposes an earlier such message. It is produced by the view-change rule, which its sender evaluates for view V only once 5∆ has elapsed since it entered V (line 47). That entry occurs at or after τ (V ) ≥ GST, and clocks exhibit no drift from GST onward, so no correct validator broadcasts an echo message for view V before τ (V ) + 5∆, and the entry at τ (V + 1), which follows such a message, is not earlier. ⊓ ⊔ Claim 15. For every post-GST view V ≥ 1, every correct validator is in view V at time τ (V ) + 2∆. Proof. By Claim 14 and repeated applications of Claim 11, no correct validator enters a view greater than V before τ (V + 1) ≥ τ (V ) + 5∆. Since views never decrease (Claim 3), a validator that has entered view V by time τ (V ) + 2∆, and that cannot have entered a view above V by then, is in view V at that time. It therefore suffices to show that every correct validator enters view V by time τ (V ) + 2∆. If V = 1, every correct validator starts by GST under the participation convention of Section 5.2 and enters view 1 upon starting, so τ (1) ≤ GST. As view 1 is post-GST, τ (1) = GST, and every correct validator enters view 1 at that time. Hence, let V > 1. By Claim 11, the entry at time τ (V ), being the first into view V , occurs at line 55, and thus rests, for every proposer pj , on 2f + 1 messages ⟨echo, V −1, j, x[j]⟩ from distinct senders for some meta-block x (line 53), at least f +1 of them broadcast by correct validators before τ (V ). Each of those broadcast by a correct validator is abandoned only upon its sender entering a view greater than V , which does not happen before τ (V ) + 5∆. These f + 1 echoes per proposer are therefore alive throughout [τ (V ), τ (V ) + 2∆] and, as GST ≤ τ (V ), received by every

B. PROOFS FOR CODA

31

correct validator by time τ (V ) + ∆. A correct validator whose view is then at most V − 2 enters view V − 1 on the spot, through the catch-up rule (line 57). Hence, at time τ (V ) + ∆, every correct validator is in view V − 1 or view V , so V − 1 ∈ {view i − 1, view i } and the amplification rule fires (line 61): every correct validator broadcasts ⟨echo, V − 1, j, x[j]⟩ for every proposer pj by time τ (V ) + ∆, unless it has done so already. These 2f + 1 echoes are alive until τ (V ) + 5∆ for the same reason, hence received by every correct validator by time τ (V ) + 2∆, at which point every correct validator holds 2f + 1 echoes for every proposer and has entered view V . ⊔ ⊓ We are ready to prove termination. Lemma 12 (Termination). Assume that every correct validator starts Coda by GST and that no correct validator stops taking part. Coda (Algorithm 2) satisfies termination. Moreover, every correct validator decides by time τ (V ⋆ ) + 5∆, where V ⋆ is the first post-GST view greater than 1 whose leader is correct. Proof. The view V ⋆ exists: every correct validator performs finitely many steps by any given time, so only finitely many views are entered before GST and post-GST views exist (Claim 13). Moreover, the leader rotates round-robin and at least 2f + 1 validators are correct. Write T = τ (V ⋆ ) and pℓ = leader(V ⋆ ). Throughout, we use Claim 14, which gives τ (V ⋆ + 1) ≥ T + 5∆ and τ (V ⋆ + 2) ≥ T + 10∆, so that no correct validator is in a view greater than V ⋆ before time T + 5∆, nor in a view greater than V ⋆ + 1 before time T + 10∆. Step 1: By time T + 3∆, every correct validator holds a justified proposal ⟨prepare, V ⋆ , x⟩ from pℓ . By Claim 15, every correct validator, pℓ included, is in view V ⋆ at time T +2∆. Upon entering V ⋆ , the correct pℓ broadcasts ⟨prepare, V ⋆ , x⟩ for x = guard ℓ [V ⋆ ] (line 33), the meta-block with which it entered the view. This broadcast is abandoned only upon pℓ entering view V ⋆ + 2, impossible before T + 10∆, so every correct validator receives the proposal by time T + 3∆. The entry of pℓ into V ⋆ is not a catch-up entry (line 59): that would require an echo message for view V ⋆ from a correct validator, none of which exists before T + 5∆ (Claim 14), whereas pℓ enters by T + 2∆. Hence, pℓ entered V ⋆ with guard x on the strength of 2f + 1 messages ⟨echo, V ⋆ − 1, j, x[j]⟩ for every proposer pj , at least f + 1 of them from correct validators. These are alive until their senders enter view V ⋆ + 1, hence received by every correct validator by time T + 3∆, at which point justified(x) holds everywhere (line 25). Step 2: By time T + 4∆, every correct validator has broadcast ⟨vote-2, V ⋆ , x, ·⟩. Consider a correct validator pi at time T + 3∆, holding the justified proposal of Step 1 and still in view V ⋆ , as no correct validator enters V ⋆ + 1 before T + 5∆. If vote1 i [V ⋆ ] = none, the rule at line 34 fires and pi broadcasts ⟨vote-1, V ⋆ , x⟩. Otherwise, pi has already broadcast a vote-1 message for V ⋆ , and that message carries x as well, since in view V ⋆ > 1 a correct validator votes only for a proposal received from pℓ (line 34), and the correct pℓ broadcasts a single one. All 2f +1 correct validators thus broadcast ⟨vote-1, V ⋆ , x⟩ by time T + 3∆. These are alive until their senders enter view V ⋆ + 2, impossible before T + 10∆, so every correct validator receives them by time T + 4∆. At that time pi is still in view V ⋆ , again because no correct validator enters V ⋆ + 1 before T + 5∆, so the rule at line 37, which acts on the current view only, fires for V ⋆ . This is where the gate of line 47 earns its length: a shorter gate would let a correct validator leave V ⋆ before its vote-1 quorum for V ⋆ completes, and it would then never broadcast a vote-2 message for V ⋆ . At that moment, either vote2 i [V ⋆ ] = none, in which case pi locks x and broadcasts ⟨vote-2, V ⋆ , x, ·⟩ (lines 39 and 40), or vote2 i [V ⋆ ] was set earlier at line 40, the timeout of line 43 firing no earlier than T + 5∆. In the latter case, the lock is a meta-block backed by 2f + 1 vote-1 messages for V ⋆ , at least one of them from a correct validator, and is therefore x. Either way, pi has broadcast ⟨vote-2, V ⋆ , x, ·⟩ by time T + 4∆. Step 3: Every correct validator decides by time T + 5∆. By Step 2, all 2f + 1 correct validators broadcast ⟨vote-2, V ⋆ , x, ·⟩ by time T +4∆. These messages are alive until their senders enter view V ⋆ +2, impossible before T + 10∆, so every correct validator receives all of them by time T + 5∆. As x ̸= none, the rule at line 41 then fires, provided V ⋆ ∈ {view i − 1, view i } at that moment: this holds, since no correct validator is in a view greater than V ⋆ +1 before T +10∆. Hence, every correct validator decides by time T +5∆. ⊓ ⊔ The participation convention, that every correct validator starts Coda by GST, costs no generality. Suppose that every correct validator starts Coda and none stops taking part, and let T0 = max(GST, Tstart ), where Tstart is the time at which the last correct validator starts. From T0 on, every correct validator runs Coda, message delays are bounded, clocks do not drift, and no correct validator crashes. A late starter may miss broadcasts that others abandoned before it started (line 15), but the proofs above rely on the delivery only of messages of correct validators that stay alive long enough after

32

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

T0 (Claims 12 to 15 and the proof of Lemma 12), and the model delivers these to late starters as well, also if they dropped an earlier copy before starting. The termination proofs thus hold with T0 in place of GST: every correct validator decides by time τ (V ⋆ ) + 5∆, where V ⋆ is the first view greater than 1 that no correct validator enters before T0 and whose leader is correct. Strong unanimity. We now turn to strong unanimity, which Coda owes to each proposer separately. The proof rests on a single invariant, the per-proposer counterpart of Claim 9: once the correct validators agree on a proposer’s entry, that entry never departs from the agreed value, in any guard and in any message. Claim 16. Let pj be a proposer and let v ∈ Value be a value such that input w [j] = v for every correct validator pw that inputs. Let m be a message broadcast by a correct validator pi . Then: 1. If m = ⟨echo, V, j, x⟩, then x = v. 2. If m = ⟨vote-1, V, x⟩, then x[j] = v. Moreover, guard i [V ][j] = v holds at every time at which view i = V . Proof. As in the proof of Claim 9, we proceed by induction on the order of the events of interest at correct validators, namely the broadcasts covered by the claim and the entries into views. Fix such an event, and suppose that the claim holds for every event that precedes it. We establish the claim through three subclaims. Subclaim 4 If a correct validator pi enters a view W , then guard i [W ][j] = v from that moment onward. Proof of Subclaim 4. If W = 1, the entry sets guard i [1] to input i (line 27), and input i [j] = v by assumption, as pi entered view 1 upon starting Coda, when it input (line 28). If W > 1, then pi enters view W at line 55, with W = V + 1 and a meta-block x for which a set of 2f + 1 messages ⟨echo, V, j, x[j]⟩ from distinct senders exists (line 53), or at line 59, with a meta-block x for which a set of f + 1 messages ⟨echo, W, j, x[j]⟩ from distinct senders exists (line 57). In both cases, at least one of the certifying messages was broadcast by a correct validator, so x[j] = v by the induction hypothesis (part 1), and the entry sets guard i [W ] ← x (line 54 or 58). In both cases, guard i [W ][j] = v. Moreover, guards are written upon entering a view alone, and view W is entered once (Claim 3), so the value persists. ⋄ Subclaim 5 If m = ⟨vote-1, V, x⟩, then x[j] = v. Proof of Subclaim 5. If V = 1, then m is created at line 32 and carries x = guard i [1], which is input i (line 27), so x[j] = v by assumption, as pi is in view 1 and has thus input. If V > 1, then, by Claim 5, validator pi has received f + 1 messages ⟨echo, V − 1, j, x[j]⟩ from distinct validators, at least one of which was broadcast by a correct validator. The induction hypothesis (part 1) gives x[j] = v. ⋄ Subclaim 6 If m = ⟨echo, V, j, x⟩, then x = v. Proof of Subclaim 6. Message m is broadcast at line 23 upon an invocation of echo(V, pj , x), of which Coda has two sources. – The amplification rule (line 61) requires a set of f + 1 messages ⟨echo, V, j, x⟩ from distinct senders, at least one of which was broadcast by a correct validator, and thus earlier. The induction hypothesis (part 1) gives x = v. – The view-change rule (line 47) is triggered while view i = V by a set S of 2f +1 accepted ⟨vote-2, V, ·, ·⟩ messages from distinct senders. At most f of these senders are faulty, so at least f + 1 messages of S were broadcast by correct validators. Each was broadcast at a time at which its sender’s current view was V (Claim 4(2)), and thus carries the guard of its sender at that time, whose entry for pj is v (Claim 4(3) and the induction hypothesis, applied to that sender’s entry into view V ). We distinguish the branch the rule takes. • The first branch (line 48) echoes ℓ[j] for a non-none lock ℓ of an accepted message of S. By Claim 6, some correct validator broadcast ⟨vote-1, V, ℓ⟩, so ℓ[j] = v by the induction hypothesis (part 2), and thus x = v. • The second branch (line 50) is reached otherwise. Its condition asks for a value that is the entry for pj in the guards of f + 1 messages of S, and v is such a value: as established above, at least f + 1 messages of S carry a guard whose entry for pj is v. It is the only such value, as two values would require 2f + 2 > |S| messages; hence x = v. The condition therefore holds, and empty is not echoed for pj (line 52). ⋄

B. PROOFS FOR CODA

The three subclaims cover every event of interest, which completes the induction.

33

⊔ ⊓

We are finally ready to prove strong unanimity. Lemma 13 (Strong unanimity). Coda (Algorithm 2) satisfies strong unanimity. Proof. Suppose that all correct validators that input input the same value v ∈ Value for a proposer pj , and suppose, by contradiction, that a correct validator decides a meta-block x with x[j] = empty in some view V . The decision requires the receipt of 2f + 1 messages ⟨vote-2, V, x, ·⟩ from distinct senders (line 41), at least one of which was broadcast by a correct validator pw . By Claim 4(3), lock w [V ] = x ̸= none, which is set only upon the receipt of 2f + 1 messages ⟨vote-1, V, x⟩ from distinct senders (lines 37 and 39), at least one of which was broadcast by a correct validator. By Claim 16(2), x[j] = v. As v ∈ Value and empty ∈ / Value (line 3), this contradicts x[j] = empty. ⊓ ⊔ Obligation. Obligation is, like strong unanimity, owed to each proposer separately, and it is proved by the same induction, with provenance in place of uniqueness. We call a value x ∈ Value ∪ {empty} admissible for a proposer pj if x = empty or some correct validator pw input it for pj , that is, input w [j] = x. The invariant below is the counterpart of Claim 16: instead of pinning a proposer’s entry to one value, it confines that entry to the values a correct validator stands behind. Claim 17. Let pj be a proposer, and let m be a message broadcast by a correct validator pi . Then: 1. If m = ⟨echo, V, j, x⟩, then x is admissible for pj . 2. If m = ⟨vote-1, V, x⟩, then x[j] is admissible for pj . Moreover, guard i [V ][j] is admissible for pj at every time at which view i = V . Proof. We proceed by induction on the order of the events of interest at correct validators, exactly as in the proof of Claim 16, and we establish the claim through the same three subclaims. Subclaim 7 If a correct validator pi enters a view W , then guard i [W ][j] is admissible for pj from that moment onward. Proof of Subclaim 7. If W = 1, the entry sets guard i [1] to input i (line 27), and input i [j] is admissible by definition, pi being correct. If W > 1, then pi enters view W at line 55 or at line 59, and sets guard i [W ] ← x (line 54 or 58) for a meta-block x backed, for the proposer pj , by a set of 2f + 1 messages ⟨echo, W −1, j, x[j]⟩ (line 53) or of f +1 messages ⟨echo, W, j, x[j]⟩ (line 57) from distinct senders. Either way, at least one of them was broadcast by a correct validator, so x[j] is admissible by the induction hypothesis (part 1). Guards are written upon entering a view alone, and view W is entered once (Claim 3), so the value persists. ⋄ Subclaim 8 If m = ⟨vote-1, V, x⟩, then x[j] is admissible for pj . Proof of Subclaim 8. If V = 1, then m is created at line 32 and carries x = guard i [1], which is input i (line 27), whose entry for pj is admissible. If V > 1, then, by Claim 5, validator pi has received f + 1 messages ⟨echo, V − 1, j, x[j]⟩ from distinct validators, at least one of which was broadcast by a correct validator. The induction hypothesis (part 1) makes x[j] admissible. ⋄ Subclaim 9 If m = ⟨echo, V, j, x⟩, then x is admissible for pj . Proof of Subclaim 9. Message m is broadcast at line 23 upon an invocation of echo(V, pj , x), of which Coda has two sources. – The amplification rule (line 61) requires a set of f + 1 messages ⟨echo, V, j, x⟩ from distinct senders, at least one of which was broadcast by a correct validator, and thus earlier. The induction hypothesis (part 1) applies. – The view-change rule (line 47) is triggered by a set S of 2f + 1 accepted ⟨vote-2, V, ·, ·⟩ messages from distinct senders. Unlike in the proof of Claim 16, all three of its branches are reachable here, and we inspect each. • The first branch (line 48) echoes ℓ[j] for a non-none lock ℓ of an accepted message of S. By Claim 6, some correct validator broadcast ⟨vote-1, V, ℓ⟩, so ℓ[j] is admissible by the induction hypothesis (part 2).

34

Mohammad Mussadiq Jalalzai, Tobias Klenze, and Jovan Komatovic

• The second branch (line 51) echoes a value G that is the entry for pj in the guards of f + 1 messages of S. These come from distinct senders, at most f of which are faulty, so at least one of them was broadcast by a correct validator, at a time at which that sender’s current view was V (Claim 4(2)), and it carries the sender’s guard at that time (Claim 4(3)). That guard’s entry for pj is admissible by the induction hypothesis, applied to that sender’s entry into view V . Hence, so is G. • The third branch (line 52) echoes empty, which is admissible by definition. ⋄ The three subclaims cover every event of interest, which completes the induction.

⊔ ⊓

We are now ready to prove the obligation property. Lemma 14 (Obligation). Coda (Algorithm 2) satisfies obligation. Proof. Suppose that a correct validator decides a meta-block x in some view V , and let pj be a proposer with x[j] ̸= empty. We must exhibit a correct validator that input x[j] for pj . The decision requires the receipt of 2f + 1 messages ⟨vote-2, V, x, ·⟩ from distinct senders (line 41), at least one of which was broadcast by a correct validator pw . By Claim 4(3), lock w [V ] = x ̸= none, which is set only upon the receipt of 2f + 1 messages ⟨vote-1, V, x⟩ from distinct senders (lines 37 and 39), at least one of which was broadcast by a correct validator. By Claim 17(2), x[j] is admissible. As x[j] ̸= empty, some correct validator input x[j] for pj , which is precisely obligation. ⊓ ⊔ B.2

Complexity

We begin by bounding the echoes that a correct validator broadcasts for a single view. Claim 18. For every view V ≥ 1 and every proposer pj , a correct validator broadcasts at most |Pj | + 1 distinct ⟨echo, V, j, ·⟩ messages, and it initiates the broadcast of each of them at most once. Proof. By Claim 17(1), every ⟨echo, V, j, v⟩ message broadcast by a correct validator carries a value v that is admissible for pj , that is, v ∈ Pj ∪ {empty}. This leaves at most |Pj | + 1 distinct messages. Each of them is broadcast at most once. Echoes are broadcast only by the function echo, which records every message it broadcasts in sent i [V ] (line 23) and does not broadcast a recorded message again (line 22). It remains to check that the record survives as long as it is needed. A correct validator invokes echo(V, ·, ·) only while V ∈ {view i −1, view i }: the view-change rule echoes for view view i (line 47), and the amplification rule echoes for views view i − 1 and view i (line 61). Throughout that period, the memory rule retains sent i [V ] (line 14), which starts empty, and the period never resumes once view i exceeds V + 1, as views never decrease (Claim 3). ⊔ ⊓ Lemma 9 (Message complexity). For every view V , each correct validator initiates at most 3 + (c + 1)k broadcasts of messages of view V . Hence, retransmissions aside, correct validators send O(ckn2 ) messages of each view, which is O(kn2 ) when c = O(1). Proof. Fix a correct validator pi and a view V . Validator pi broadcasts at most one ⟨prepare, V, ·⟩ message, upon entering view V as its leader (line 33), which happens at most once (Claim 3). It broadcasts at most one vote-1 message and at most one vote-2 message for view V (Claim 4(2)). Finally, for every proposer pj , it broadcasts at most |Pj | + 1 ≤ c + 1 echo messages for view V (Claim 18), for at most (c + 1)k echoes in total. Every broadcast unicasts its message to each of the n validators, and at most n validators are correct, which yields the bound. ⊔ ⊓ Lemma 10 (Persistent memory). Each correct validator stores O(ck) words in persistent memory for Coda, which is O(k) words when c = O(1). Proof. We count memory in words, where a word holds a value, a view number, or a validator identifier, so that a meta-block occupies k words. By the memory rule (line 14), a correct validator retains the viewspecific variables of at most two views, alongside view i , the time at which it entered its current view, and its decision flag (one word each). For each retained view V , the variables guard i [V ] and lock i [V ] are meta-blocks, vote1 i [V ] is a message carrying one meta-block, and vote2 i [V ] is a message carrying two, for O(k) words in total, while sent i [V ] holds at most (c + 1)k messages of O(1) words each (Claim 18). The Coda messages whose broadcasts are alive belong to views view i − 1 and view i (line 15), and each of them is either recorded in these variables or a prepare message carrying guard i [V ], so keeping track of them costs O(ck) words as well. In total, O(ck) words. ⊔ ⊓

B. PROOFS FOR CODA

B.3

35

Evaluating the View-Change Rule

The view-change rule (line 47) fires once for every set S of 2f + 1 accepted vote-2 messages that satisfies its condition, but a validator can avoid enumerating these sets, since the values that the rule echoes are determined by counts. Fix a correct validator pi in view V . Let M be the ⟨vote-2, V, ·, ·⟩ messages that pi has accepted, at most one per sender (line 19), U ⊆ M those without a lock, and Lℓ ⊆ M those with lock ℓ. For a proposer pj and an entry v ∈ Value ∪ {empty}, let cj (v) be the number of messages in U whose guard has entry v for pj . Once 5∆ have elapsed since pi entered view V , some set S ⊆ M satisfying the condition of the rule causes it to invoke echo(V, pj , v) if and only if one of the following holds. 1. v = ℓ[j] for a meta-block ℓ with |Lℓ | ≥ 1 and |Lℓ | + |U | ≥ 2f + 1. We can choose 2f + 1 messages from Lℓ ∪ U , including at least one from Lℓ , to form a set with lock ℓ, on which the rule echoes the entry of ℓ for every proposer. 2. |U | ≥ 2f + 1 and cj (v) ≥ f + 1. Then f + 1 messages of U with entry v for pj , together with f further messages of U , form a set without locks in which f + 1 messages carry v, so the rule echoes v (no other entry can also P reach f + 1 in a set of 2f + 1). 3. v = empty and w∈Value∪{empty} min(cj (w), f ) ≥ 2f + 1. The rule echoes empty for pj on a set without locks in which no entry for pj is carried by f + 1 messages. Such a set contains at most f messages with each entry, so it exists exactly when at least 2f + 1 messages remain after keeping, for each entry, at most f of the messages of U that have this entry for pj . Conversely, a set satisfying the condition either has locks that are all the same meta-block ℓ, so it lies in Lℓ ∪ U and condition 1 holds, or has no locks, so it lies in U and condition 2 holds if it echoes an entry carried by f + 1 of its messages, and condition 3 holds otherwise.

Related documents

• Quantum Cadence: Post-Quantum Consensus with Multiple Concurrent Proposers#1448319
• Byzantine Fault-Tolerant Post-Quantum Distributed Quorum Signatures#386833
• The Native-Signature Boundary in Post-Quantum Distributed Authorization#639610
• Compact Shielded CSV: Post-Quantum, Private, Lightweight Client-Side Validation Blockchain#1115971
• Symphony: Taming Step Misalignments in the Network for Ring-based Collective Operations#120462