Seamless Reconfiguration for DAG-BFT

Seamless Reconfiguration for DAG BFT Michael Yiqing Hu National University of Singapore, Singapore

Leander Jehl University of Stavanger, Norway

Paul Franke-Bergmann Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Jialin Li National University of Singapore, Singapore

Christian Berger

arXiv:2610.00896v1 [cs.DC] 1 Oct 2026

Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Abstract Byzantine Atomic Broadcast in Asynchronous networks has been studied extensively for decades. The FLP impossibility result rules out deterministic consensus in a fully asynchronous setting, motivating randomized protocols that combine reliable broadcast with private coins to achieve termination with probability one. More recently, DAG-Rider popularized a new abstraction in which processes continuously reliably broadcast blocks to construct a directed acyclic graph (DAG) and then locally derive a total order using a randomized perfect coin. This separation of dissemination from ordering has renewed interest in asynchronous DAG-based Byzantine fault tolerance and inspired numerous protocols that improve expected latency or throughput. Reconfiguration, however, remains largely unexplored. Existing DAG-based BFT protocols generally assume a static set of processes, whereas deployed systems must occasionally add or remove nodes in response to operational demands. Existing solutions are not seamless; they either pause the system or delay membership changes until a predetermined epoch boundary. This may be impractical and can introduce downtime. However, a seamless solution is non-trivial; agreement on when to start utilizing a new configuration may yield a logical round number that was already surpassed by the concurrent asynchronous dissemination. In this work, we present a seamless reconfiguration protocol for asynchronous DAG-based Byzantine atomic broadcast. Our protocol allows the DAG to continue growing while the membership and corresponding quorum thresholds change, without halting the system. To the best of our knowledge, ours is the first protocol to provide seamless reconfiguration for DAG-based Byzantine atomic broadcast in a fully asynchronous network.

2012 ACM Subject Classification Keywords and phrases Dummy keyword Digital Object Identifier 10.4230/LIPIcs... © Michael Yiqing Hu, Leander Jehl, Paul Franke-Bergmann, Jialin Li, and Christian Berger; licensed under Creative Commons License CC-BY 4.0 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

1

Introduction

The search for scalable Asynchronous Byzantine atomic broadcast (BAB) protocols has culminated in DAG-based protocols [3, 10, 13, 15, 21, 22], which decouple transaction dissemination from consensus: a dissemination layer continuously reliably broadcasts blocks and assembles them, in a sequence of logical rounds, with each message referencing a quorum threshold number of blocks from the previous round. A separate consensus layer then selects a monotonic canonical list of leader blocks from the DAG. Ordering each block’s causal history in the order of that list, yields the total order. The consensus layer utilizes what has already been disseminated and requires no additional communication. To overcome the FLP impossibility result [11], leader blocks are selected utilizing a randomized perfect coin [4, 6, 18, 20], yielding expected liveness with probability one. Existing work on DAG-based protocols largely assumes static membership, i.e. the set of processes is fixed and known to all. Deployed systems, however, do not run on a fixed set of processes: operators must add and remove nodes in response to operational demands and failures. This requires more than informing processes of a change: quorum thresholds must be adjusted, and joining and leaving processes need a procedure for taking up and relinquishing their protocol tasks. Deployments today, therefore, either pause the protocol while the change is installed or defer it to a predetermined epoch boundary [2, 9, 24]. However, both options surrender the property that makes these protocols attractive in the first place. Dissemination achieves throughput by never waiting for agreement, so halting it to install a membership change wastes that advantage; a reconfiguration is usually prompted by the very failure it is meant to repair. We would rather have reconfiguration be seamless: dissemination should never need to stop on its account, so correct processes keep producing and delivering blocks and advancing rounds while the membership and its quorum thresholds change, and none waits for a predetermined boundary. The classical way to reconfigure a long-lived replicated service routes the change through the consensus layer [9, 17, 19]. The new membership is ordered as an ordinary command and installed at the log position where it was decided, or a fixed number of commands later. Such a single switching point would be useful for a DAG, since quorum thresholds change with the membership and every process must know which threshold a round demands. In an asynchronous execution, processes may learn the decision and apply the new configuration at different times. Dissemination, which runs ahead of ordering by design, may meanwhile produce blocks beyond the switching point under the old configuration. This direct use of a single switching point therefore does not make reconfiguration seamless: dissemination would have to wait for the decision, or discard those blocks. Reconfiguration without consensus avoids the need for such a point, and has been studied for distributed storage [1, 14, 23], lattice agreement [16], and, most relevant here, Byzantine reliable broadcast [12]. These approaches share the idea of multi-configuration operation: an operation begun in one configuration may complete in another, and different processes may complete it in different ones. However, reconfiguring a DAG-based BAB asks for more on top of this, since the thresholds that govern DAG construction and the randomized perfect coin that drives ordering have to be reconfigured as well; while staying consistent with the underlying reliable broadcast. In this paper, we present a seamless reconfiguration procedure for DAG-based BAB. To allow consistent reconfiguration of reliable broadcast, perfect coin and DAG construction, we extend the idea of multi-configuration operation to the DAG itself. Every block records the configuration its broadcaster has installed, the reconfiguration it has pending, and the

XX:1

XX:2

Seamless Reconfiguration for DAG BFT

configurations enabled in its round. Each correct old member enables both configurations for four rounds after the round in which it installs the transition. Retained processes continue producing blocks throughout the transition, and already DAG-delivered blocks remain in the DAG. Our procedure therefore does not require processes to agree on the exact round in which a new configuration is enabled, while ensuring that new processes take up block production when needed, and that the consensus layer cannot produce conflicting leaders from different configurations. To the best of our knowledge, we provide the first provably correct seamless reconfiguration protocol for DAG-based Byzantine atomic broadcast in a fully asynchronous network. In total, we make the following contributions: We define Dynamic DAG-structured Byzantine Broadcast, a reconfigurable dissemination abstraction whose integrity, consistency, causal closure and per-round quorum progress hold even while correct processes sit at different stages of a transition (Section 3). Being independent of the ordering layer, it can carry other ordering rules. We define Dynamic DAG Byzantine Atomic Broadcast on top, and make explicit which guarantees of the static problem must be given up under a changing membership, and why (Section 3). We give a seamless reconfiguration protocol implementing both, from configuration-scoped reliable broadcast, the four-round transition window, and a state transfer admitting joining processes without pausing dissemination (Section 4). We adapt DAG-Rider’s randomized leader election to a changing membership by scoping its perfect coin to a single configuration, and prove that the composition satisfies our definitions (Section 5).

2

Background

DAG-based protocols for Byzantine atomic broadcast decouple transaction dissemination from consensus [10, 15]. For illustration, we informally recall the seminal protocol of that line, DAG-Rider [15]. DAG-Rider builds a DAG structured in logical rounds, with each process contributing at most one block per round. The logical rounds are further segmented into waves. In DAG-Rider, every subsequent four rounds form a wave. Blocks carry a payload and reference at least a quorum of the preceding round’s blocks as their parents. Processes share blocks using reliable broadcast [5], this ensures non-equivocation. Since correct processes eventually complete their reliable broadcasts, there will always exist sufficient blocks to proceed. The DAG itself only provides a partial order to the blocks. A separate ordering layer is then utilized to obtain a total order from the DAG. DAG-Rider achieves this by identify certain blocks as leaders. Leaders are identified by a perfect coin constructed by obtaining sufficient signature shares from blocks belonging to the last round of the wave. This allows ensures there exist a canonical list of leaders ordered by the wave number; and every correct process will eventually derive a prefix of this canonical list. Each leader in the list can have it’s causal history ordered in the same manner to obtain a total order of blocks that exist in the DAG. Crucially, this ordering layer does not require any additional communication; all information required has already been disseminated. In this work, we utilize DAG-Rider as a framework to build a seamless reconfigurable DAG Byzantine Atomic Broadcast algorithm. We make changes to the reliable broadcast, DAG construction as well as leader election components to enable seamless addition and removal of processes.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

3

Problem Definition and Primitives

3.1

System Model

We consider a message-passing system whose processes are identified by public keys. Corruptions are adaptive and permanent. A process is uncorrupted at an event if it has not been corrupted before that event, and is correct if it is never corrupted. An uncorrupted process follows the protocol; after corruption, it becomes byzantine and may behave arbitrarily. The quantitative fault bound is configuration-specific and is stated below. A process is active while it executes at least one prescribed protocol task. An active correct process continues those tasks and processes every delivered protocol message. The network is asynchronous: message delays are finite but unbounded. Any message sent to a recipient is eventually delivered.

3.2

Configurations and membership

In an execution, a reconfigurable system can evolve through multiple configurations. We write Rl for a coinfiguration with identifier l and Πl for the membership set of Rl . R1 is the initial configuration of the system. For any configuration Rl with processes Πl let   nl − 1 nl = |Πl | ≥ 4, fl = , ql = nl − fl . 3 Thus nl ≥ 3fl + 1,

ql ≥ 2fl + 1,

ql − fl = nl − 2fl ≥ fl + 1.

We assume that at most fl identities in Πl are ever corrupted during an execution. This bounds all identities corrupted over the execution, not merely simultaneous corruptions. The corruption schedule and membership policy preserve this bound for every configuration. For our randomized perfect coin we assume that each Πl is represented as a duplicate-free list sorted by canonical public-key encoding, so all correct processes assign the same position to each member. Consecutive configurations differ by the addition or removal of at most one process. A removal is permitted only if nl ≥ 5, so the resulting configuration still contains at least four processes. A removed process will not be added back in any future configurations.

3.3

Authentication

We assume an unforgeable digital-signature scheme. For process pi and message x, signi (x) is pi ’s signature and verifyi (σ, x) returns true exactly when σ is a valid signature by pi on x. We also assume a public collision-resistant hash function Hash(·). For every configuration Rl , each pi ∈ Πl receives a key share for each of two independent, domain-separated threshold-signature schemes: (ql , nl ) = (nl − fl , nl )

and

(fl + 1, nl ).

The first produces quorum certificates for Byzantine reliable broadcast (BRB); the second supplies the shares used to select one member of Πl in each wave, as specified in Section 3.8.1. In a (t, nl ) scheme, any t valid shares on the same message combine into a unique signature verifiable under that scheme’s public key, while fewer than t shares cannot produce a valid signature. The two schemes have distinct public keys and domains. BRB We write ShareSignBRB i,l (x) and ValidSharei,l (σ, x) for BRB share generation and verificaCOIN COIN tion, and ShareSigni,l (x) and ValidSharei,l (σ, x) for their coin counterparts. Note that each threshold-signature is scoped to a particular configuration Rl .

XX:3

XX:4

Seamless Reconfiguration for DAG BFT

3.4

Rounds and DAG notation

The protocol is organized into logical rounds r = 1, 2, . . .. A round number is a protocol index and imposes no timing bound in the asynchronous network. Four consecutive rounds form a wave. We write first(w) = 4w − 3 and last(w) = 4w for the first and last round in a wave w. For process pi , DAGi [r] is the round-r layer of its local directed acyclic graph, and S DAGi = r≥1 DAGi [r]. A stored round-r block has the form B = ⟨m, r, µ, C⟩,

µ = ⟨h, R, P, E, ID⟩,

where m is the payload and C is a quorum certificate from configuration R, that certifies delivery by a configuration-scoped Byzantine reliable broadcast (BRB) instance. The structure µ contains metadata. The symbol ⊥ to denotes absence. The field h is ⊥ in round 1 and otherwise contains references to parent blocks in round r − 1; R is the declared configuration; and ID is the broadcaster identity. Fields P and E hold reconfiguration related information, detailed below in Section 3.5. P is a pending reconfiguration message or ⊥; E is a set of enabled configurations. We write parents(µ) = h,

local(µ) = R,

pending(µ) = P,

enabled(µ) = E,

ID(µ) = ID.

The pair (r, ID(µ)) is the block’s round-broadcaster slot. A parent is referenced directly by h; an ancestor is reached by following one or more parent references. A set of blocks is ancestor-closed if it contains every ancestor of each block it contains. For B, B ′ ∈ DAGi , write B ⇝i B ′ if B = B ′ or B ′ is an ancestor of B. Thus ⇝i is reflexive and points from a block toward its causal history. We omit the subscript when the local process is immaterial.

3.5

Reconfiguration Model

Processes receive reconfiguration messages of the form Rl = ⟨RECONFIG, Πl , l, δl ⟩. Here RECONFIG is a fixed domain tag, Πl is the membership set, l is the configuration identifier, and δl is the earliest logical round in which Rl may occur in a block’s pending field. We write members(Rl ) = Πl ,

number(Rl ) = l,

earliest(Rl ) = δl .

The process to determine the membership of a new configuration is out of scope. An externally authorized message may be produced by Byzantine agreement among current members or reliably broadcasted by a trusted reconfiguration dealer; for simplicity, we assume the latter. The trusted dealer needs to ensure that: (1) reconfigurations form a sequence, using consecutive numbers as identifiers, (2) reconfiguration messages carry unforgeable evidence authenticating its complete tuple, (3) each reconfiguration adds or removes at most one process, (4) earliest rounds δl ensure configurations are well-spaced and do not overlap, and finally (5) each execution contains only finitely many reconfigurations. The passage from Rl to Rl+1 is a transition; reconfiguration denotes the overall mechanism. A process in Πl ∩ Πl+1 is retained, one in Πl+1 \ Πl is joining, and one in Πl \ Πl+1 is removed. We write ValidReconfiguration(Rl , Rl+1 ) when the reconfiguration messages are correctly authenticated and follow the assumptions above. We call Rl → Rl+1 a valid transition exactly when ValidReconfiguration(Rl , Rl+1 ) holds. The distribution mechanism sends each valid Rl+1 to every correct process in Πl ∪ Πl+1 to which the transition applies. Eventual delivery ensures that each such recipient receives it. Sl−1 For every l ≥ 2, the authenticated message Rl also carries the identities in c=1 Πc . We omit this list from the tuple notation. The procedure UpdateKnowni validates Rl and

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

this identity list. If Rl is the highest-numbered authenticated reconfiguration message Sl processed by UpdateKnowni , then known i = c=1 Πc . Thus known i contains the identities of all processes in R1 , . . . , Rl . Point (4) above ensures a correct member of Πl starts the transition to Rl+1 only while installed in Rl . A correct joining process may authenticate the reconfiguration message Rl+1 before installing Rl , but invokes the transition only after it has installed Rl , as enforced by δl+1 . In (Section 4.2) we provide an issuance rule, that can be used by the dealer to set δl . Disjointness of transitions is not an assumption, but follows from the issuance rule, proved in lemma 52.

Enabled Configurations and Transition Windows. A process pi stores a current configuration local i , the potentially empty next pending authenticated reconfiguration message pending i and a map enabled-configs i [r] with a set of configurations for every round. Whenever enabled-configs i [r] is assigned at a correct process pi , it is assigned only once and is thereafter immutable. Its value has one of the following forms: {Rc } or {Rl , Rl+1 }, where the second form records the two configurations of an authenticated valid transition Rl → Rl+1 . We call {Rc } a singleton enabled-configs. The transition protocol determines which of these forms a process assigns in each round. Because processes advance asynchronously, an enabledconfigs value is local to a process and logical round; the occurrence of the pair at one correct process does not imply that every correct process has assigned the pair in that round. When pi broadcasts a block in round r, it includes local i , pending i , and enabled-configs i [r] as R, P, E in the blocks metadata µ. We say a round r is singleton-enabled for Rc at pi when enabled-configs i [r] = {Rc }. Similarly, a block B = ⟨m, r, µ, C⟩ with local(µ) = Rc and enabled(µ) = {Rc } is singletonenabled for Rc . The transition window of Rl → Rl+1 is the set of logical rounds r for which some correct process pi satisfies enabled-configs i [r] = {Rl , Rl+1 }.

Finite Reconfiguration and Stability. We assume that each execution contains only finitely many reconfiguration messages, although their number is not bounded a priori, while logical rounds remain infinite. Together with R1 , these messages define a finite sequence R1 , . . . , RL with final configuration RL . We further assume that at least qL correct members of ΠL remain active and continue the prescribed protocol tasks. A wave is stable under RL if all four of its rounds are singleton-enabled for RL at every correct process in ΠL that remains active. If all finitely many reconfigurations complete, there exists a round r∗ where all waves that follow are stable.

3.6

Configuration-scoped Byzantine Reliable Broadcast

We use a configuration scoped variant of Byzantine Reliable Broadcast[5] (BRB) to distribute blocks. For round r and broadcaster pk , a call BRB-Broadcastk (m, r, µ) proposes ⟨m, r, µ⟩ for slot (r, pk ). The metadata µ is the same as in a DAG block, explained in Section 3.4. A corresponding output at pi is BRB-Deliveri (m, r, µ, C), where C combines ql distinct valid BRB vote shares and verifies under the BRB public key of Rl = local(µ). The voters, threshold, and key are scoped to the declared configuration, but the slot remains (r, pk ) and is not configuration-indexed.

XX:5

XX:6

Seamless Reconfiguration for DAG BFT

Configuration-scoped BRB differs from standard BRB in that correct processes only participate after validating the metadata µ, and that delivery creates a certificate. A correct process pi participates in a BRB instance ⟨m, r, µ⟩ only if pi ∈ Πl for local(µ) = Rl , and Rl ∈ enabled-configs i [r]. Additionally, µ must be well-formed according to the validity rules given below. The certificates enable processes to share valid evidence of BRB delivery, allowing an alternative for processes to add blocks into their DAG (see Section 4.1). Configurationscoped BRB provides the following safety properties. Agreement. If two correct processes BRB-deliver values for the same round-broadcaster slot, they BRB-deliver the same value. Integrity. A correct process BRB-delivers at most one value for a round-broadcaster slot. Every delivered value has a valid certificate for its declared configuration; if the broadcaster is correct, the value is the one supplied to its prescribed BRB-Broadcast invocation. We used a modified version of Bracha’s[5] BRB. Lemmas 4 and 50 prove that algorithm 2 satisfies these properties, including when a slot is certified during a transition.

Configuration-authorized Block Validity. A correct process echoes or votes for a BRB instance ⟨m, r, µ⟩ only after checking the metadata µ as follows. Because a certificate requires ql shares and at most fl members of the declared configuration are ever corrupted, Byzantine members alone cannot certify a block that fails any of these checks. The metadata µ is valid if the corresponding conditions hold: The recorded field enabled(µ) must be the singleton {local(µ)} or the authenticated pair of a valid transition, and must contain local(µ), and the broadcaster must belong to members(local(µ)). The pending field must be ⊥ or a valid reconfiguration message for the successor of local(µ) whose earliest inclusion round has been reached: the authorization for Rl+1 binds δl+1 , so a block in a round r < δl+1 whose pending field contains Rl+1 is rejected. Except in round 1, the block must also carry exactly qc parent references, where Rc = local(µ) is its declared configuration. The sole exception is the joining process’s transition block (Section 4): during an addition, a block declared under Rl+1 by the member in Πl+1 \ Πl may carry ql references instead of ql+1 . Validators accept the smaller count only when the transition Rl → Rl+1 is valid and both enabled(µ) and their own enabled-configs i [r] equal {Rl , Rl+1 }. Certification checks only the number of parent references, never the referenced parents themselves; parents are validated during DAG delivery (Section 3.7). A valid certificate thus attests all of these checks wherever the block is later obtained. The complete predicate appears in algorithms 1 and 2.

3.7

Dynamic DAG-structured Byzantine Broadcast

Our protocol implements Dynamic DAG-structured Byzantine Broadcast (Dynamic DAGBB). Dynamic DAG-BB is a repeated, round-indexed broadcast abstraction over the finite configuration sequence R1 , . . . , RL . In round r, a process pi may invoke DAG-Appendi (m, r). Consequently, a processes pj may DAG-deliver a block B = ⟨m, r, µ, C⟩ with the same message m and ID(µ) = i, adding it to a local datastructure DAGj at level r (DAGj [r]). A block contains parent and configuration metadata, as defined in Section 3.4. A referenced parent with metadata µ′ is authorized only if its broadcaster belongs to a configuration in enabled(µ′ ) and its declared configuration is no newer than the child’s. Hence a certified block from a member removed by Rl+1 that records {Rl , Rl+1 } may serve as a parent and count

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

toward parent quorums, while its broadcaster cannot broadcast, echo, or vote under Rl+1 . A block is admissible exactly when its certificate is valid, its metadata passes the instancevalidity rules of Section 3.6, and its referenced parents are admissible and authorized and satisfy the applicable parent-count rule, including the round-1 rule and the joining-process exception. A parent-quorum condition is the protocol’s round-specific requirement that a process hold enough admissible blocks of the preceding layer to advance. ▶ Definition 1 (Dynamic DAG-structured Byzantine Broadcast). A Dynamic DAG-structured Byzantine Broadcast satisfies the following properties in every execution, including while correct processes are at different stages of a transition. 1. DAG-Integrity. For each round-broadcaster slot, a correct process DAG-delivers at most one block, and every DAG-delivered block is admissible. If the broadcaster is correct, the blocks payload m originates from the append operation prescribed for that process and round. 2. DAG-Consistency. If two correct processes DAG-deliver blocks B and B ′ for the same round-broadcaster slot, then B = B ′ . 3. Causal Closure. Before a correct process DAG-delivers a block, it has already DAGdelivered every referenced parent and, recursively, every ancestor of those parents. 4. Per-Round Quorum Progress. Consider a round r with applicable quorum threshold qc . If at least qc active correct members for which the protocol prescribes a round-r append enter the round and invoke that operation, then every active correct process whose advancement depends on this quorum eventually DAG-delivers sufficient admissible blocks from distinct broadcaster slots to satisfy an applicable round-advancement condition and advance to round r + 1. During Rl → Rl+1 , the applicable quorum threshold may be either ql or ql+1 . 5. Reconfiguration Completion. Every valid transition eventually completes at every correct retained or joining process. Every correct removed process eventually reaches the point at which it may leave. Per-Round Quorum Progress includes dissemination of the blocks needed for advancement. For a protocol satisfying Reconfiguration Completion, the finite reconfiguration sequence and the continued execution of the correct processes in ΠL that remain active imply an infinite suffix of stable waves.

BRB to DAG Upon an invocation of DAG-Appendi (m, r), the process snapshots local i , pending i , and enabled-configs i [r]. It then waits for the required parents, constructs µ using their references and the snapshotted values, and starts the configuration-scoped BRB instance for ⟨m, r, µ⟩. A successful instance produces the certificate C. Similarly, BRB delivery alone does not insert B = ⟨m, r, µ, C⟩ into the DAG. A correct process first validates the certificate and metadata, obtains every referenced parent and missing ancestor, and only then inserts B into DAGi [r]; we then say that it DAG-delivers B. A correct joining process preserves Causal Closure by validating its ancestor-closed transferred state before inserting its first block, and its two transition blocks (Section 4) supply the additional broadcaster slot needed for progress when a correct process joins.

Why Dynamic DAG-BB Does Not Require Validity or Totality. Traditional Validity requires every value broadcast by a correct process to be delivered by every correct process; Totality requires a value delivered by one correct process to be delivered by all.

XX:7

XX:8

Seamless Reconfiguration for DAG BFT

Both presume a fixed membership: a joining process did not participate in earlier broadcasts, and a removed process must eventually be allowed to stop. Indeed, the strong, departureoblivious forms of Validity and Totality are impossible in an asynchronous dynamic system, even with reliable links and a single possible crash failure [12, Appendix A.6]. Dynamic DAGBB therefore demands only what progress and safety need: Per-Round Quorum Progress supplies every active correct process whose advancement depends on the applicable quorum with sufficient admissible blocks to satisfy an applicable round-advancement condition, while DAG-Integrity, DAG-Consistency, and Causal Closure provide safety. Universal delivery of every block is unnecessary; the atomic-broadcast layer separately ensures agreement on the finalized leader sequence. However, once the stable wave is reached, then we may ensure totality and validity once more.

3.8

Dynamic DAG Byzantine Atomic Broadcast

As in DAG-Rider [15], we define a rule to consistently select blocks from the DAG, based on a global perfect coin included in the last round of a wave. However, our coin is scoped to configuration. Blocks causally located between selected blocks can also be ordered deterministically as in previous work.

3.8.1

Configuration-scoped Perfect Coin

As with DAG-Rider’s global perfect coin, each coin instance (Rl , w) selects one process of Πl . Unlike there, every instance is scoped to one configuration: instances of different configurations use separate keys, and their shares are never combined. In the threshold implementation used by the protocol, a member invokes an instance by releasing its valid share for that instance. For security parameter λ, let negl(λ) denote a negligible function. The coin satisfies the following four properties. Agreement. If two correct processes obtain an output for (Rl , w), they obtain the same process. Termination. If at least fl + 1 correct processes invoke the coin for (Rl , w), every invocation by a correct process eventually returns. Unpredictability. As long as fewer than fl + 1 members have invoked the coin for (Rl , w), its output, conditioned on the adversary’s current view, is computationally indistinguishable from a uniformly random member of Πl , except with probability negl(λ). Fairness. Every process in Πl is selected with probability 1/nl . The threshold-share implementation and the rule that maps the selected member to a first-round block are described in Section 4. Coin Unpredictability is used only to prove Probabilistic progress; safety uses only Agreement and signature uniqueness. For each correct process’s block B = ⟨m, r, µ, C⟩, where r is the last round of a wave, m includes a local(µ)-scoped coin share.

3.8.2

Atomic-broadcast Abstraction

To realize an atomic-broadcast abstraction, we define a rule to consistently select blocks from the DAG. These blocks are called leaders. For an active correct process pi , finalized-values i is its local sequence of DAG blocks selected by the ordering layer; these blocks are its finalized leaders. A block is finalized at pi when it is appended to this sequence, and finalized-values i [k] denotes the k-th block in the sequence. DAG-Rider states Byzantine Atomic Broadcast using reliable-broadcast integrity, agreement, and validity together with total order [15]. A changing membership forces two

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

relaxations. Our ordering primitive does not claim that every proposed block is eventually finalized, so we omit proposal validity. A removed process must be allowed to leave, so eventual agreement is required only of the correct members of the final configuration that remain active. The dynamic DAG Byzantine Atomic Broadcast is the goal of this work. ▶ Definition 2 (Dynamic DAG Byzantine Atomic Broadcast). A leader-level Dynamic DAG Byzantine Atomic Broadcast consists of an underlying Dynamic DAG-structured Byzantine Broadcast satisfying definition 1 and, at each process, a sequence of finalized leader blocks satisfying the following properties. 1. Integrity. For every active correct process pi and wave w, finalized-values i contains at most one block from w, and no block occurs more than once. Every finalized block has already been inserted into DAGi . 2. Total Order. At every point in an execution, the finite sequences finalized-values i of active correct processes are pairwise comparable by prefix. Consequently, if one active correct process finalizes B before B ′ , no active correct process finalizes B ′ without first finalizing B. 3. Probabilistic Progress. Let RL be the final configuration of the execution. With probability one, every correct process pj ∈ ΠL that remains active finalizes infinitely many blocks. After a correct process is removed and leaves, no requirement is imposed on further extensions of its finalized-values sequence. Our rule, specified in Section 4.3 selects at most one block per wave. Lemma 51 proves that the broadcast, DAG, state-transfer, and reconfiguration algorithms implement Dynamic DAGBB. Leader Integrity, Total Order, and Probabilistic Progress are established in corollary 64 and theorems 65 and 72, and theorem 3 composes them into Dynamic DAG Byzantine Atomic Broadcast. A proof sketch appears in Section 5.

4

Seamless DAG Reconfiguration

Our protocol extends ordinary round-based DAG production with a four-round configuration transition. During a transition, blocks declared under the installed configuration may carry the pending reconfiguration, and every block records the configurations enabled in its round. This lets retained processes continue producing blocks while a joining process connects the existing causal history to blocks declared under the next configuration. The ordering layer counts coin shares only in singleton-enabled rounds, so a transition preserves Causal Closure and Per-Round Quorum Progress without combining shares from different configurations. We describe the protocol in words below; its complete validation predicates, message handlers, and retry loops appear in Section A.

4.1

Ordinary DAG Operation

At the beginning of round r, process pi uses its installed configuration local i , pending reconfiguration pending i , and enabled-configs i [r], which is immutable once assigned, to construct a block for DAGi [r]. Suppose local i = Rl when pi enters round r > 1. At the start of its append invocation, it snapshots local i , pending i , and enabled-configs i [r]. It then waits until the preceding DAG layer contains the admissible blocks required by the applicable parent-quorum condition, selects their hashes and broadcaster identities as the parent set h, and constructs µ = ⟨h, Rl , P, E, pi ⟩ , where Rl , P , and E are the snapshotted values. A reconfiguration received

XX:9

XX:10

Seamless Reconfiguration for DAG BFT

while the process waits for the applicable parent-quorum condition therefore cannot change this block’s pending field or enabled set. If P = ̸ ⊥ but r < earliest(P ), the process does not broadcast the block; correct BRB echoers and voters enforce the same check. It then invokes the Rl -scoped BRB of Section 3.6 on ⟨m, r, µ⟩ by calling DAG-Appendi (m, r). A successful BRB instance produces a certificate C, but this certificate alone does not make the certified object a DAG block. A recipient validates the block according to the admissibility rules of Section 3, recursively obtains every referenced parent and missing ancestor, and only then inserts B = ⟨m, r, µ, C⟩ into its local DAG and DAG-delivers it. Consequently, every block DAG-delivered by a correct process is admissible and is accompanied by its complete causal history. A process enters round r + 1 once DAGi [r] contains enough admissible round-r blocks to satisfy the applicable parent-quorum condition. Thus, a correct process may advance even if it has not yet delivered the block itself proposed. In round r, a process installed in Rl ordinarily waits for ql admissible round-r blocks before entering round r + 1. If r = r0 + 3 is its last round before completing a transition installed in round r0 , it instead waits for ql+1 admissible round-r blocks that are eligible as parents of the next block declared under Rl+1 .

State Availability The procedures mentioned here further enable processes to include blocks in their DAG indirectly. Three actions leads to a process pi sending a block B ∈ DAGi to every identity in known i without first receiving a request. (1) The BRB vote-receive handler sends one when it combines qc valid shares into a certificate, (2) when a process adds a B into its local DAG, or (3) when FloodDAG is called and one of every block in the local DAG is broadcasted to knowni . When a new configuration message R is received, and UpdateKnowni updates known i ; FloodDAG will be invoked. Once a process receives a block in these manners, it is buffered until it becomes admissible.

4.2

Beginning and Completing a Configuration Change

In this section, we consider one transition from Rl to Rl+1 . By well-spacing (Section 3.5), different transitions happen in non-overlapping logical rounds. If a correct process records {Rl , Rl+1 } in one round, no other correct process records the pair for a different transition in that round. To ensure well-spacing, a dealer can "listen" to the DAG. In practice, the dealer may repeatedly request complete, ancestor-closed DAGs from members of Πl and validate every reply. Eventual delivery ensures that it receives a complete DAG from a correct member. It waits until the downloaded state contains ql certified blocks declared under Rl in some round s, and then issues Rl+1 with δl+1 = s + 2. We show in lemmas 6–10 that this leads to well-spacing. When a member of Πl receives Rl+1 , it authenticates and buffers the message. Once it has installed Rl and reached the authenticated earliest inclusion round, it records Rl+1 in pending i ; only append operations started after that point copy the message into block metadata. A block is marked by Rl+1 if its own pending field contains Rl+1 or an ancestor is marked by Rl+1 . Thus the mark propagates through the DAG’s causal history. When a process with local i = Rl completes a round r containing at least fl + 1 marked blocks from distinct broadcaster slots in Πl , it invokes InstallTransitioni (Rl , Rl+1 , r). We call r its install transition round. The process enables both configurations in the next four rounds: enabled-configs i [s] = {Rl , Rl+1 },

s ∈ {r + 1, r + 2, r + 3, r + 4}.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

p1

∗

∗

XX:11

∗

p2

∗

∗

p3 p4

∗

p5 sees fl + 1 marked blocks in round r + 3 and starts in round r + 5

p5 r

r+1 Rl block, {Rl } Rl+1 block, {Rl+1 }

r+2 ∗

r+3

r+4

Rl block, marked by Rl+1 Rl+1 block, {Rl , Rl+1 }

r+5

r+6

Rl block, {Rl , Rl+1 }

r+7

r+8

Rl quorum Rl+1 quorum

Figure 1 Adding p5 when Πl = {p1 , p2 , p3 , p4 } and Πl+1 = Πl ∪ {p5 }, with Byzantine p4 . For each block, {·} denotes its enabled-configs in its µ. p5 begins DAG-Transition-Append in round r + 5 before starting normal operations in round r + 7. Blocks from p5 in rounds r + 5, r + 6 are transition blocks; having ql parents instead of ql+1 .

It remains installed in Rl through round r + 3 and installs Rl+1 at the beginning of round r + 4, before ordinary block production. Correct members of Πl need not choose the same install transition round, but corollary 29 shows that their choices differ by at most one round.

Joining Procedure Let pj ∈ Πl+1 \ Πl . After receiving the authenticated pair ⟨Rl , Rl+1 ⟩, the joining process repeatedly requests admissible blocks from every identity in known j and sends another request after accepting a reply or when known j changes. An active correct process that receives a request satisfying the state-request handler’s conditions replies with a finite, ancestor-closed set of blocks from its local DAG. The joining process accepts the set only if every block has valid certified metadata, and every referenced parent and its ancestors are included in the set. The joining process also inserts blocks it accepts into its local DAG in increasing round order. Before inserting a block, it validates the block and ensures that every referenced parent and ancestor has already been inserted. It applies the same rule to blocks received individually, requesting any missing parents and ancestors from the identities in known j . The joining process continues requesting blocks until its local DAG contains a round with at least ql admissible blocks in distinct broadcaster slots belonging to Πl , including at least fl + 1 blocks marked by Rl+1 . Per Section 4.1, processes will occasionally send their blocks as a broadcast to other processes. Messages sent to a joining process before it activates remain pending and are processed after activation. Consequently, obtaining the required causal history does not depend on any particular process remaining active until the joining process later requests it. As soon as the preceding condition holds, the joining process chooses the smallest qualifying round currently present in its local DAG and denotes it by u. It uses u as its install transition round and continues obtaining blocks until it has ql admissible round-(u + 1) blocks in distinct broadcaster slots belonging to Πl . It continues receiving and validating additional blocks throughout the rest of the joining procedure. In round u + 1, it remains passive: it neither produces a block nor sends a BRB echo or vote share. In rounds u + 2 and u + 3, the joining process invokes DAG-Transition-Append and

XX:12

Seamless Reconfiguration for DAG BFT

p1

∗

p2

∗

∗

∗

p3 p4

∗

p5

∗

r

r+1

r+2

p5 stops producing blocks at round r + 6, and completely leaves when it sees fl+1 + 1 blocks in round r + 7

r+3

r+4

r+5

r+6

r+7

Figure 2 Removing p5 when Πl = {p1 , p2 , p3 , p4 , p5 } and Πl+1 = Πl \ {p5 }, with Byzantine p4 . p5 completes InstallTransition at round r+6 but does not leave (it continues helping complete reliable broadcasts and responding to requests for DAG blocks) until sufficient blocks exist in round r+7.

produces a transition block declared under Rl+1 . The round-(u + 2) block uses ql parents from the downloaded round-(u + 1) layer. The round-(u + 3) block also uses ql admissible parents and may reference transition blocks in the preceding layer. By lemma 34, every correct member of Πl enabled-configs are {Rl , Rl+1 } in rounds u + 2 and u + 3, thus transition blocks obtain Rl+1 -scoped BRB certificates. These blocks contribute the additional broadcaster slot that may be needed by processes with an early install transition round; when ql+1 > ql . At the beginning of round u + 4, the joining process installs Rl+1 and starts its ordinary protocol tasks. Processes accept transition blocks only during the rounds, when both configurations in the transition are enabled. Hence, a Byzantine joining process cannot reuse the exception in a later singleton-enabled round.

Leaving Procedure A leaving process pi ∈ Πl \ Πl+1 installs the transition as other nodes in Πl . However, when installing the transition in round r, pi does not produce blocks in round r + 4 or later. Process pi continues helping complete reliable broadcasts and responding to requests for DAG blocks; while its departure condition remains pending, pi continues processing BRB messages and receiving, validating, and inserting blocks and their missing ancestors. Once it has inserted fl+1 + 1 admissible round-(r + 5) blocks from distinct broadcasters in Πl+1 , it invokes one final FloodDAG before stopping its remaining tasks; finally proceeding to leave. This enables a lagging process to eventually obtain the required blocks to progress. Let r0 be process pj ’s install transition round for Rl → Rl+1 . If pj is in round rj ∈ {r0 + 2, r0 + 3}, it may also advance when its local DAG contains at least ql+1 admissible round-(rj + 1) blocks eligible as parents of a block declared under Rl+1 . These blocks need not all be declared under Rl+1 themselves. The process can therefore advance even if its own round-rj block has not yet been certified. The same condition is available during additions and removals. This behavior is formalized in lemmas 36–38.

4.3

Configuration-scoped Leader Election

After explaining how block production crosses a configuration change, we turn to ordering the resulting DAG. We explain how a sequence of leaders (anchor blocks) is created. Blocks located between these leaders can be ordered deterministically, as done in previous work [15]. As in DAG-Rider, four consecutive rounds form a wave: first-round blocks are leader

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

candidates, while last-round blocks provide causal support and carry the shares used to reconstruct the wave’s threshold coin. Because a wave may intersect a configuration change, all coin shares and support thresholds are scoped to one configuration. A last-round block B = ⟨m, r, µ, C⟩ is an Rl -typed leader-voting block for wave w when r = last(w),

local(µ) = Rl ,

enabled(µ) = {Rl },

and B carries a valid Rl -scoped coin share for w. This coin share is distinct from a BRB vote share. A block with enabled(µ) = {Rl , Rl+1 } does not count as a leader-voting block, but may be a leader candidate. Further, shares from different configurations (e.g. Rl and Rl+1 -typed) are never combined. Every broadcaster that is uncorrupted when producing a leader-voting block fixes the block’s parent set before generating and releasing its coin share. For stable waves under RL , this ordering lets the proof fix the common core before fL + 1 distinct valid shares have been released, as shown in lemma 68. From fl + 1 distinct valid shares, WaveLeader(Rl , w) reconstructs the unique Rl -scoped coin. If the coin selects pj ∈ Πl , WaveLeader(Rl , w) returns pj ’s round-first(w) block declared under Rl , if that block is in the local DAG; otherwise it returns ⊥. A process may receive certified leader-voting blocks declared under different configurations in the same last round. However, as shown in lemma 54, all correct broadcasters whose blocks are singleton-enabled in that round use the same configuration. For every other configuration Rc , only Byzantine broadcasters can produce leader-voting blocks of that type, yielding at most fc distinct slots. This is fewer than the fc + 1 shares needed to reconstruct the Rc -scoped coin. Consequently, at most one configuration can have at least fc +1 leader-voting blocks in a wave, even when a reconfiguration is ongoing. For configuration Rl and wave w, let B = WaveLeader(Rl , w) ̸= ⊥ be the first-round block selected by the reconstructed coin. Process pi identifies B as a direct anchor when at least ql distinct Rl -typed leader-voting blocks X in round last(w) satisfy X ⇝i B. Here X ⇝i B means that B is in X’s causal history; the relation follows parent references toward earlier blocks. The process checks this condition on completing the wave and whenever it later DAG-delivers another leader-voting block for that wave. Rechecking matters because correct processes may receive the same last-round blocks in different orders. Once a process identifies a direct anchor B ⋆ in wave k, it scans the ancestors of B ⋆ for anchors from earlier waves that it has not previously processed, in reverse wave order. When it examines a wave w < k, it accepts that wave’s candidate B ′ only when, for some configuration Rl , at least fl + 1 distinct Rl -typed leader-voting blocks X for wave w satisfy B ⋆ ⇝i X ⇝i B ′ . Recall that ⇝i points toward causal history: the later anchor B ⋆ contains X in its ancestry, and X in turn contains B ′ . Only the voting blocks of B ′ ’s own wave are counted, although voting blocks of later waves may also lie between B ⋆ and B ′ . An accepted B ′ becomes the scan anchor for the next iteration and is prepended to the result; a wave with no acceptable candidate is skipped. The full backward scan rooted at a direct anchor determines its canonical leader prefix: a prefix of the total order of leader blocks that all active correct processes will eventually derive (lemma 61). The serialized local procedure Elect performs this scan and atomically appends the missing suffix to finalized-values i . When one process identifies a direct anchor, delivering ql many Rl -typed leader-voting blocks in one round, the causal history of any direct anchor in a later wave will include fl + 1 of these blocks. Thus other processes will accept the same anchor in a later backward scan. The detailed helper definitions and election procedure appear in algorithms 8 and 9.

XX:13

XX:14

Seamless Reconfiguration for DAG BFT

Together, transition blocks preserve Per-Round Quorum Progress across transitions, while requiring the leader-voting blocks for each decision to declare one configuration prevents a decision from combining configurations. Transitions may prevent a leader from being elected in some waves. To ensure the liveness of leader election, we rely on the assumption that reconfigurations eventually cease.

5

Correctness

We sketch the main arguments; complete proofs appear in Section B. ▶ Theorem 3 (Correctness of Dynamic DAG Byzantine Atomic Broadcast). Under the model of Section 3, suppose that the dealer follows the issuance rule of Section 4.2. For Probabilistic Progress, also assume the conditional probability requirement of Section B.3. For every finite sequence of reconfiguration messages, with no a priori bound on its length, the protocol of Section 4 implements the leader-level Dynamic DAG Byzantine Atomic Broadcast of definition 2. Proof sketch. Broadcast safety and reconfiguration progress. Certificate validation, authenticated proposal and echo checks, and one delivery per slot give BRB Integrity. In each round, certificates can use only one configuration or the two configurations of one valid transition. Their quorums intersect in a correct process that votes at most once in the slot, so the slot cannot have certificates for different values or under both configurations (lemmas 4, 5, and 50). BRB Integrity and Agreement give DAG-Integrity and DAG-Consistency, while obtaining and validating every parent and missing ancestor before inserting any block, including a transferred block, gives Causal Closure (lemma 51). Fix a valid transition Rl → Rl+1 . By lemma 45, let t be the earliest install transition round among correct processes in members(Rl ). A correct process that installs in round t has DAG-delivered fl + 1 blocks marked by Rl+1 . Every round-(t + 1) block from a correct broadcaster in members(Rl ) is marked: either its pending field contains Rl+1 , or its ql round-t parent slots intersect those fl + 1 marked slots. Every round-(t + 1) parent quorum counted under Rl uses distinct broadcaster slots in members(Rl ), and therefore contains at least ql − fl ≥ fl + 1 blocks from correct broadcasters (lemmas 9 and 13). Block broadcasts after DAG delivery and FloodDAG let correct lagging and joining processes obtain and validate certified, ancestor-closed history (lemmas 23 and 24). Using this dissemination and the marking argument above, every correct process in members(Rl ) installs in round t or t + 1. A correct joining process eventually broadcasts its two transition blocks (corollary 29 and lemmas 39 and 46). Because install rounds may differ by one, AdvanceRound also accepts ql+1 admissible following-round blocks in the last two transition rounds. If a required correct process stops before the ordinary condition holds, its final FloodDAG supplies blocks satisfying the ordinary or following-round condition, so the wait terminates without skipping a round (lemmas 26 and 37 and corollary 41). Even if an added process is Byzantine or a process is removed, the fault bound leaves enough correct processes to supply the required parent quorums. Thus the protocol satisfies Per-Round Quorum Progress and Reconfiguration Completion (lemmas 49 and 51). Moreover, a following configuration’s earliest inclusion round exceeds t + 5, and no installation precedes that inclusion round. Hence distinct transition windows do not overlap (lemma 52); wellspacing is derived rather than assumed. Integrity and Total Order. An Rc -typed leader-voting block records enabled(µ) = {Rc } and carries a valid Rc -scoped coin share. If Ra and Rb respectively supplied fa + 1 and fb + 1

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

such blocks in distinct broadcaster slots, each collection would contain a correct broadcaster. By lemma 54, those broadcasters cannot record different singleton enabled-configs values in the same logical round. Thus at most one configuration can supply the fc + 1 leadervoting blocks needed to reconstruct a coin for a wave. Threshold-signature uniqueness and DAG-Consistency then make the selected leader unique (lemma 56). A direct anchor identified from Rl -typed leader-voting blocks is reached by at least ql such blocks in the last round of its wave. Every later-wave block DAG-delivered by a correct process reaches at least 2fl + 1 Rl -declared blocks in that round. Both collections use distinct broadcaster slots from members(Rl ), so DAG-Consistency gives at least ql + (2fl + 1) − nl = fl + 1 common blocks. These blocks satisfy the backward-scan acceptance condition. Hence a later backward scan accepts the earlier direct anchor when it reaches that wave (lemma 58 and corollary 60). Each scan depends only on its starting anchor’s immutable causal history. The finalized leader sequences of active correct processes are therefore nested prefixes, giving Integrity and Total Order (lemmas 61 and 62, corollary 64, , and theorem 65). Probabilistic Progress. After the finitely many transitions, the final configuration RL remains installed and every correct RL -member that remains active advances through infinitely many stable waves. Each such wave w has a common core [7, 8] Kw of qL firstround blocks in the causal history of every last-round block DAG-delivered by a correct process. Every correct RL -member that remains active eventually DAG-delivers all blocks in Kw and at least qL distinct RL -typed leader-voting blocks, each of which reaches every block in Kw (corollaries 66, 67, and 69 and lemma 68). In every stable wave, the coin selects the broadcaster of a block in Kw with probability bounded below by a fixed positive constant, regardless of the outcomes of earlier waves (Section B.3). When this happens, every correct RL -member that remains active eventually identifies that block as a direct anchor, unless it has already identified a direct anchor in a later wave (proposition 70). The probability of seeing no further selections from a common core is therefore zero, regardless of how earlier waves ended. Consequently, every correct RL -member that remains active identifies direct anchors in arbitrarily late stable waves with probability one (lemma 71). Processing these anchors extends the nested finalized leader sequences with blocks from arbitrarily late waves. Hence every such process finalizes infinitely many blocks with probability one (lemma 62). ◀

6

Conclusion and Open Questions

In this work we present the first seamless reconfiguration protocol for DAG-based Byzantine atomic broadcast in a fully asynchronous network. Membership and quorum thresholds change while dissemination continues. Reconfiguration occurs seamlessly by processes locally interpreting their view of the DAG. We conclude this paper with several open questions that we leave to future work: Firstly, is it possible to for reconfigurations to be seamless and non-blocking when transition windows are allowed to overlap. Furthermore, is it possible to extend reconfigurations to not preclude removal and addition of more than one processes at a time. Lastly, if a downgrade to a partially-synchronous model would invite even more elegant solutions.

XX:15

XX:16

Seamless Reconfiguration for DAG BFT

References 1 2 3

4 5 6

7 8

9

10

11

12

13

14

15

16

Marcos K Aguilera, Idit Keidar, Dahlia Malkhi, and Alexander Shraer. Dynamic atomic storage without consensus. Journal of the ACM (JACM), 58(2):1–32, 2011. Aptos Labs. Staking. https://aptos.dev/network/blockchain/staking#validator-states, 2026. Aptos Documentation. Balaji Arun, Zekun Li, Florian Suri-Payer, Sourav Das, and Alexander Spiegelman. Shoal++: High throughput dag bft can be fast and robust! In 22nd USENIX Symposium on Networked Systems Design and Implementation (NSDI 25), pages 813–826. USENIX Association, 2025. Dan Boneh, Ben Lynn, and Hovav Shacham. Short signatures from the Weil pairing. Journal of Cryptology, 17:297–319, 2001. Gabriel Bracha. Asynchronous byzantine agreement protocols. Inf. Comput., 75(2):130–143, November 1987. doi:10.1016/0890-5401(87)90054-X. Christian Cachin, Klaus Kursawe, and Victor Shoup. Random oracles in constantinople: Practical asynchronous byzantine agreement using cryptography. Journal of Cryptology, 18(3):219–246, 2005. doi:10.1007/s00145-005-0318-0. Ran Canetti. Studies in secure multiparty computation and applications. 1995. Ran Canetti and Tal Rabin. Fast asynchronous byzantine agreement with optimal resilience. In Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, STOC ’93, page 42–51, New York, NY, USA, 1993. Association for Computing Machinery. doi: 10.1145/167088.167105. Allen Clement, Natacha Crooks, Neil Giridharan, and Alex Shamis. It’s not a lie if you don’t get caught: simplifying reconfiguration in smr through dirty logs. arXiv preprint arXiv:2602.09441, 2026. George Danezis, Eleftherios Kokoris-Kogias, Alberto Sonnino, and Alexander Spiegelman. Narwhal and tusk: A dag-based mempool and efficient bft consensus. In Proceedings of the 17th European Conference on Computer Systems (EuroSys), pages 34–50. ACM, 2022. doi:10.1145/3492321.3519594. Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM, 32(2):374–382, 1985. doi:10.1145/ 3149.214121. Rachid Guerraoui, Jovan Komatovic, Petr Kuznetsov, Yvonne-Anne Pignolet, Dragos-Adrian Seredinschi, and Andrei Tonkikh. Dynamic byzantine reliable broadcast. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020), volume 184 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1–23:18. Schloss Dagstuhl – LeibnizZentrum für Informatik, 2021. doi:10.4230/LIPIcs.OPODIS.2020.23. Michael Yiqing Hu, Alvin Hong Yao Yan, Yihan Yang, Xiang Liu, and Jialin Li. Lemonshark: Asynchronous dag-bft with early finality. In 23rd USENIX Symposium on Networked Systems Design and Implementation (NSDI 26), pages 469–492. USENIX Association, 2026. Leander Jehl, Roman Vitenberg, and Hein Meling. Smartmerge: A new approach to reconfiguration for atomic storage. In Yoram Moses, editor, Distributed Computing 29th International Symposium, DISC 2015, Tokyo, Japan, October 7-9, 2015, Proceedings, volume 9363 of Lecture Notes in Computer Science, pages 154–169. Springer, 2015. doi:10.1007/978-3-662-48653-5\_11. Idit Keidar, Eleftherios Kokoris-Kogias, Oded Naor, and Alexander Spiegelman. All you need is dag. In Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing (PODC), pages 165–175. ACM, 2021. doi:10.1145/3465084.3467905. Petr Kuznetsov, Thibault Rieutord, and Sara Tucci Piergiovanni. Reconfigurable lattice agreement and applications. In Pascal Felber, Roy Friedman, Seth Gilbert, and Avery Miller, editors, 23rd International Conference on Principles of Distributed Systems, OPODIS 2019, Neuchâtel, Switzerland, December 17-19, 2019, volume 153 of LIPIcs, pages 31:1–31:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs. OPODIS.2019.31, doi:10.4230/LIPICS.OPODIS.2019.31.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

17 18

19 20 21

22

23

24

Leslie Lamport. Paxos made simple. ACM SIGACT News, 32(4):51–58, December 2001. Benoît Libert, Marc Joye, and Moti Yung. Born and raised distributively: Fully distributed non-interactive adaptively-secure threshold signatures with short shares. ACM symposium on Principles of Distributed computing, 2014. Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys, 22(4):299–319, December 1990. doi:10.1145/98163.98167. Victor Shoup. Practical threshold signatures. In International Conference on the Theory and Application of Cryptographic Techniques, 2000. Alexander Spiegelman, Balaji Arun, Rati Gelashvili, and Zekun Li. Shoal: Improving dag-bft latency and robustness. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, 2023. Alexander Spiegelman, Neil Giridharan, Alberto Sonnino, and Lefteris Kokoris-Kogias. Bullshark: Dag bft protocols made practical. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS). ACM, 2022. doi: 10.1145/3548606.3563519. Alexander Spiegelman, Idit Keidar, and Dahlia Malkhi. Dynamic Reconfiguration: Abstraction and Optimal Asynchronous Solution. In Andréa Richa, editor, 31st International Symposium on Distributed Computing (DISC 2017), volume 91 of Leibniz International Proceedings in Informatics (LIPIcs), pages 40:1–40:15, Dagstuhl, Germany, 2017. Schloss Dagstuhl – LeibnizZentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/ LIPIcs.DISC.2017.40, doi:10.4230/LIPIcs.DISC.2017.40. The MystenLabs Team. The sui smart contracts platform. Technical report, Mysten Labs, 2020. URL: https://docs.sui.io/doc/sui.pdf.

XX:17

XX:18

Seamless Reconfiguration for DAG BFT

A

Full Algorithms

Throughout the algorithms, Ra , Rb , Rc denote configurations; r, s, u denote logical rounds; m denotes a block payload, whose optional coin-share field is coin(m); µ denotes block metadata; C denotes a BRB certificate; B denotes a certified block; ID denotes a process identity; and ⊥ denotes absence.

A.1

Local Variables and Threshold Functions

At process pi , local i is the installed configuration and pending i is either the authenticated next reconfiguration message currently recorded by the process or ⊥. The Boolean joining i is true while pi is performing the joining operation. The set passive-rounds i contains rounds in which pi must not broadcast a block, echo, or vote. The immutable value enabled-configs i [r] records either a singleton set {Rc } or an authenticated pair {Ra , Rb } enabled by pi in round r. The value ri is the current logical round. After the round-advancement task starts, its serialized AdvanceRoundi loop is the only task that changes this value and always changes it from r to r + 1. The value IDi is the identity of pi , and DAGi [r] is the set of blocks that pi has DAG-delivered in round r. The set known i contains the identities of the members of every configuration covered by the highest-numbered authenticated reconfiguration message processed by pi . It is used only to choose the recipients of protocol messages; it does not change membership, eligibility, or a quorum threshold. For a configuration Rc , the projections members(Rc ), number(Rc ), and earliest(Rc ) return its membership, configuration number, and earliest inclusion round. The values nc , fc , and qc are the membership size, fault bound, and quorum threshold of Rc . For an enabled-configs value E, Recipients(E) is the union of the members of the configurations in E. ValidReconfiguration(Rl , Rl+1 ) validates the authorization evidence, consecutive configuration numbers, earliest inclusion round, and membership difference. UpdateKnowni (Rc ) authenticates Rc and the identities carried by it and adds those identities and the members of Rc to known i . If this enlarges known i , the procedure invokes FloodDAGi so that the newly known identities are sent the blocks currently stored by pi . ValidSign(C, m, r, µ) validates C against the complete BRB value and the threshold public key of the configuration declared in that value. ValidEnabled(µ) checks that the enabled field is either the declared configuration alone or the pair belonging to a valid transition. ValidPending(r, µ) checks that a non-⊥ pending field is the valid successor of the declared configuration and is not used before its earliest inclusion round. JoiningMetadata(µ, Ra , Rb ) checks that Ra → Rb is a valid transition, the block declares Rb , its enabled field is {Ra , Rb }, and its broadcaster belongs to members(Rb ) \ members(Ra ). ValidParentCounti (s, µ) is evaluated by a correct process before it echoes or votes. Ordinarily it requires qb parents for a block declared under Rb . For metadata satisfying JoiningMetadata(µ, Ra , Rb ), the qa -parent exception is accepted only when the process’s immutable enabled-configs value for round s equals the pair {Ra , Rb } recorded by the block. This permits the exception in any round in which that value is assigned; the metadata does not prove the added process’s locally chosen install transition round. The correct joining process uses the exception only for its two prescribed transition appends. A qb parent count remains the ordinary alternative and does not depend on the exception. CertifiedParentCount(s, µ) is used when validating an already certified block. It does not consult the receiving process’s local enabled-configs value, because at least one correct voter

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

applied ValidParentCount before the certificate was formed. It checks the ordinary qb count or the permitted joining-process count recorded in the certified metadata. Algorithm 1 Local variables and threshold functions at process pi 1: local i ← R1 ; pendingi ← ⊥; joiningi ← false; passive-roundsi ← ∅ 2: known i ← members(R1 ) ▷ Known identities 3: enabled-configsi [1] ← {R1 } and enabled-configsi [r] ← ⊥ for every r ≥ 2 4: IDi ← pi ; ri ← 1 5: For Rl = ⟨RECONFIG, Πl , l, δl ⟩, let members(Rl ) = Πl , number(Rl ) = l, and earliest(Rl ) = δl . 6: For every Rc , let nc = |members(Rc )|, fc = ⌊(nc − 1)/3⌋, and qc = nc − fc . ValidReconfiguration(Rl , Rl+1 ) ⇐⇒ (Rl = R1 ∨ Rl has valid authorization evidence) ∧ Rl+1 has valid authorization evidence ∧ that evidence covers the exact value earliest(Rl+1 ) ∧ earliest(Rl+1 ) > 1 ∧ number(Rl+1 ) = number(Rl ) + 1 ∧ |members(Rl ) △ members(Rl+1 )| ≤ 1. Use the block-metadata tuple and projections from Section 3. S 7: Recipients(E) = members(R). R∈E

known i is used only for communication; it does not alter membership, eligibility, thresholds, or Recipients(E). Receipt of an authenticated Rc also provides dealer-authenticated evidence for the identities that appeared in R1 , . . . , Rc−1 .

8: procedure UpdateKnowni (Rc ) 9: if Rc or the identities carried by it from R1 , . . . , Rc−1 fail authentication then 10: return 11: K ← known i 12: add every member of Rc and every identity carried by Rc to known i 13: if known i ̸= K then 14: FloodDAGi 15: DAGi [r] ← ∅ for every r ≥ 1. 16: ValidSign(C, m, r, µ) holds iff C is a valid BRB quorum certificate for ⟨m, r, µ⟩ under the threshold public key of local(µ). ValidEnabled(µ) ⇐⇒ enabled(µ) = {local(µ)} ∨ ∃Ra , Rb : enabled(µ) = {Ra , Rb } ∧ ValidReconfiguration(Ra , Rb ), ValidPending(r, µ) ⇐⇒ pending(µ) = ⊥ ∨ ValidReconfiguration(local(µ), pending(µ))

∧ r ≥ earliest(pending(µ)) , JoiningMetadata(µ, Ra , Rb ) ⇐⇒ local(µ) = Rb ∧ enabled(µ) = {Ra , Rb } ∧ ValidReconfiguration(Ra , Rb ) ∧ ID(µ) ∈ members(Rb ) \ members(Ra ).

17: function ValidParentCounti (s, µ) 18: Rb ← local(µ); E ← enabled(µ) 19: if s > 1 and enabled-configsi [s] = E and ∃Ra : JoiningMetadata(µ, Ra , Rb ) then 20: return |parents(µ)| ∈ {qa , qb } 21: return |parents(µ)| = qb 22: function CertifiedParentCount(s, µ) 23: if s = 1 then 24: return parents(µ) = ⊥ 25: if parents(µ) = ⊥ or its broadcaster IDs are not pairwise distinct then 26: return false 27: Rb ← local(µ) 28: if ∃Ra : JoiningMetadata(µ, Ra , Rb ) then 29: return |parents(µ)| ∈ {qa , qb } ▷ Joining-process exception 30: return |parents(µ)| = qb ▷ A correct voter checked ValidParentCounti

A.2

Configuration-Scoped Byzantine Reliable Broadcast

ECHOSi [m, r, µ] stores one valid echo signature per sender for the specified BRB value. V OT ESi [m, r, µ] similarly stores valid BRB vote shares. The Boolean values echoed i [r, ID], voted i [r, ID], and delivered i [r, ID] ensure that pi echoes, votes, and delivers at most once for a round-broadcaster slot. A message for a round whose enabled-configs value is not yet assigned is buffered until that assignment is made.

XX:19

XX:20

Seamless Reconfiguration for DAG BFT

Algorithm 2 Configuration-scoped BRB at process pi 1: ECHOSi [m, r, µ] ← ∅; V OT ESi [m, r, µ] ← ∅ on first access 2: echoed i [r, ID], voted i [r, ID], delivered i [r, ID] ← false for every (r, ID) Future-round messages are buffered until enabled-configsi [r] ̸= ⊥, then processed normally. ValidInstancei (r, µ) ⇐⇒ enabled-configsi [r] ̸= ⊥ ∧ local(µ) ∈ enabled-configsi [r] ∧ local(µ) ∈ enabled(µ) ∧ ID(µ) ∈ members(local(µ)) ∧ ValidEnabled(µ) ∧ ValidPending(r, µ)

∧ r = 1 ∨ ValidParentCounti (r, µ) , MaySendBRBi (Rc , r) ⇐⇒ enabled-configsi [r] ̸= ⊥ ∧ Rc ∈ enabled-configsi [r] ∧ pi ∈ members(Rc ) ∧ r ∈ / passive-roundsi .

3: procedure BRB-Broadcasti (m, r, µ) 4: if ¬MaySendBRBi (local(µ), r) then 5: return 6: broadcast ⟨m, r, µ⟩ to Recipients(enabled(µ))

▷ The BRB proposal is configuration-scoped upon receiving ⟨m, r, µ⟩ from pj 7: Rc ← local(µ); ID ← ID(µ) 8: if ValidInstancei (r, µ) ∧ pj = ID ∧ MaySendBRBi (Rc , r) ∧ ¬echoed i [r, ID] then 9: e ← ⟨echo, m, r, µ⟩; echoed i [r, ID] ← true 10: broadcast ⟨echo, signi (e), m, r, µ⟩ to Recipients(enabled(µ)) upon receiving ⟨echo, σj , m, r, µ⟩ from pj 11: Rc ← local(µ); e ← ⟨echo, m, r, µ⟩ 12: if ValidInstancei (r, µ) ∧ pj ∈ members(Rc ) ∧ verifyj (σj , e) then 13: ECHOSi [m, r, µ][j] ← σj 14: if |ECHOSi [m, r, µ]| ≥ qc then 15: SendVotei (m, r, µ)

16: procedure SendVotei (m, r, µ) 17: Rc ← local(µ); ID ← ID(µ) 18: if MaySendBRBi (Rc , r) ∧ ¬voted i [r, ID] then 19: v ← ⟨vote, m, r, µ⟩; voted i [r, ID] ← true 20: broadcast ⟨vote, ShareSignBRB i,c (v), m, r, µ⟩ to Recipients(enabled(µ)) upon receiving ⟨vote, σj , m, r, µ⟩ from pj

21: Rc ← local(µ); ID ← ID(µ); v ← ⟨vote, m, r, µ⟩ 22: if ValidInstancei (r, µ) ∧ pj ∈ members(Rc ) ∧ ValidShareBRB j,c (σj , v) then 23: V OT ESi [m, r, µ][j] ← σj 24: if |V OT ESi [m, r, µ]| ≥ fc + 1 then 25: SendVotei (m, r, µ) 26: if |V OT ESi [m, r, µ]| ≥ qc ∧ ¬delivered i [r, ID] then 27: C ← the threshold signature from exactly qc entries of V OT ESi [m, r, µ] 28: B ← ⟨m, r, µ, C⟩ 29: broadcast ⟨certified-block, B⟩ to known i ▷ Flood the complete certificate 30: delivered i [r, ID] ← true 31: trigger BRB-Deliveri (m, r, µ, C)

ValidInstancei (r, µ) checks that the declared configuration is enabled at pi in round r, that the broadcaster belongs to that configuration, and that the enabled, pending, and parent fields are valid. MaySendBRBi (Rc , r) checks whether pi may broadcast, echo, or vote under Rc in round r: Rc must be enabled, pi must be a member, and the round must not be passive. BRB-Broadcasti (m, r, µ) sends the proposed value to the members of the configurations recorded in the enabled field. Let Rc = local(µ). After collecting qc valid echoes, pi calls SendVotei . Receipt of fc + 1 valid votes also causes a process that has not yet voted to call SendVotei . Receipt of qc valid votes produces the certificate C and certified block B. The complete certified block is then sent to every identity in known i , and the algorithm triggers BRB-Deliveri . The temporary values e and v are the exact echo and vote messages that are signed. The temporary Rc and ID are the declared configuration and broadcaster identity obtained from µ.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

A.3

DAG Append and DAG Delivery

For a block B, RB , EB , and IDB denote its declared configuration, enabled field, and broadcaster identity. ref(B) is the hash-and-identity reference stored in a child block. The set scheduled i prevents pi from starting more than one concurrent fetch operation for the same block. ParentBlocksi (R, r) contains the stored round-r blocks that may be selected as parents of a block whose declared configuration is R. Every such block comes from an identity permitted by its own enabled field, and its declared configuration number is no greater than that of R. Every block in this set is certified and admissible because only an admissible block is inserted in DAGi . For a supplied block set D, let D[v] denote its round-v blocks. ValidParentSeti (B, D) checks that every parent reference of B names a matching block in round r − 1 of the supplied block set D and that each named parent satisfies the configuration checks used by ParentBlocks. For round 1, it instead requires the parent field to be ⊥. ValidCertifiedMetadatai (B) validates the certificate, configuration evidence, broadcaster membership, enabled field, pending field, and certified parent count. Admissiblei (B) additionally requires all of B’s referenced parents to be present and valid in DAGi . DAG-Appendi (m, r) records the installed, pending, and enabled-configs values at the beginning of the invocation. For r > 1, it waits for the applicable parent quorum, selects the blocks in the temporary set S, and places their references in h. Only after h is fixed, a singleton-enabled last-round invocation sets coin(m) to the configuration-scoped coin share; every other correct invocation sets it to ⊥. The procedure then constructs µ and invokes BRB. ScheduleFetchi (B) starts FetchAndDeliveri (B) if the block is neither stored nor already being fetched. FetchAndDeliveri (B) first validates the certificate and metadata. It then requests every missing parent from all identities currently in known i , repeating the request when known i changes. Once all parents are present, it calls AddAndDeliveri (B). AddAndDeliveri (B) prevents two blocks from occupying the same round-broadcaster slot, inserts an admissible block into DAGi , sends the certified block to every identity in known i , and outputs DAG-Deliveri . FloodDAGi takes the finite set of blocks currently stored in DAGi and sends each certified block to every identity in known i . An active correct process continues invoking this procedure while it remains active. The temporary set K used by a fetch operation is a copy of known i that lets the operation detect when new identities have been added. A dag-reply is sent in response to a dag-request. In contrast, a certified-block message is sent without waiting for a request when a certificate is completed, when a block is inserted, or when FloodDAG is invoked. Both message types are passed to the same validation and fetching procedure.

A.4

Reconfiguration

transition i is either ⊥ or ⟨Rl , Rl+1 , r⟩, where r is the install transition round chosen by pi . LocalBlocksi (Rl , r) contains the round-r blocks stored at pi whose broadcaster identities belong to Πl . This definition selects blocks by broadcaster identity; it does not require every selected block to be declared under Rl . For a valid transition Rl → Rl+1 , Markedi (Rl , Rl+1 , B) holds when B or one of its ancestors contains Rl+1 in its pending field. MarkedBlocksi (Rl , Rl+1 , r) counts marked blocks in LocalBlocksi (Rl , r).

XX:21

XX:22

Seamless Reconfiguration for DAG BFT

Algorithm 3 DAG-Append and DAG-Deliver at process pi 1: scheduled i ← ∅ ▷ Certified blocks received before activation are queued. For B = ⟨m, r, µ, C⟩, write RB = local(µ), EB = enabled(µ), IDB = ID(µ), and ref(B) = ⟨Hash(⟨m, r, µ⟩), IDB ⟩. ParentBlocksi (R, r) = {B ∈ DAGi [r] | IDB ∈ Recipients(EB ) ∧ number(RB ) ≤ number(R)}. For a candidate DAG D, ValidParentSeti (B, D) ⇐⇒ (r = 1 ∧ parents(µ) = ⊥) ∨ ′

r > 1 ∧ ∀ρ ∈ parents(µ), ∃B ∈ D[r − 1] :

2:

′

ref(B ) = ρ ∧ IDB ′ ∈ Recipients(EB ′ ) ∧ number(RB ′ ) ≤ number(RB ) . ValidCertifiedMetadatai (B) ⇐⇒ r ≥ 1 ∧ ValidSign(C, m, r, µ) ∧ (RB = R1 ∨ RB has valid authorization evidence)∧ IDB ∈ members(RB ) ∧ RB ∈ EB ∧ ValidEnabled(µ)∧ 3: ValidPending(r, µ)∧ CertifiedParentCount(r, µ). 4: Admissiblei (B) ⇐⇒ ValidCertifiedMetadatai (B) ∧ ValidParentSeti (B, DAGi ) ▷ Before certification, a correct echoer or voter uses ValidParentCounti () in algorithm 2.

5: procedure DAG-Appendi (m, r) 6: (Rc , Pc , Ec ) ← (local i , pending i , enabled-configsi [r]) 7: if Pc ̸= ⊥ and r < earliest(Pc ) then 8: return 9: if r = 1 then 10: h←⊥ 11: else 12: await |ParentBlocksi (Rc , r − 1)| ≥ qc 13: S ← any qc blocks in ParentBlocksi (Rc , r − 1) 14: h ← {ref(B ′ ) : B ′ ∈ S} 15: if r = last(w) for some w and Ec = {Rc } then 16: set coin(m) ← ShareSignCOIN i,c (⟨w⟩) 17: else 18: set coin(m) ← ⊥ 19: µ ← ⟨h, Rc , Pc , Ec , IDi ⟩ 20: BRB-Broadcasti (m, r, µ)

▷ Freeze the round metadata

▷ The parent set is already fixed

upon BRB-Deliveri (m, r, µ, C) do

21: ScheduleFetchi (⟨m, r, µ, C⟩) upon receiving ⟨certified-block, B⟩ or ⟨dag-reply, B⟩ do

22: ScheduleFetchi (B) 23: procedure ScheduleFetchi (B) 24: let B = ⟨m, r, µ, C⟩ 25: if B ∈ / DAGi [r] and B ∈ / scheduled i then 26: scheduled i ← scheduled i ∪ {B} 27: spawn FetchAndDeliveri (B) 28: procedure FetchAndDeliveri (B) 29: let B = ⟨m, r, µ, C⟩ 30: if ¬ValidCertifiedMetadatai (B) then 31: return 32: if r > 1 then 33: for all ρ = ⟨α, ID ′ ⟩ ∈ parents(µ) do 34: while ∄B ′ ∈ DAGi [r − 1] : ref(B ′ ) = ρ do 35: K ← known i 36: broadcast ⟨dag-request, r − 1, ID ′ ⟩ to every process in K 37: await ∃B ′ ∈ DAGi [r − 1] : ref(B ′ ) = ρ or known i ̸= K 38: if Admissiblei (B) then 39: AddAndDeliveri (B) upon receiving ⟨dag-request, s, ID⟩ from pj do

40: if ∃B ∈ DAGi [s] : IDB = ID then 41: send ⟨dag-reply, B⟩ to pj 42: procedure AddAndDeliveri (B) 43: let B = ⟨m, r, µ, C⟩ 44: if B ∈ / DAGi [r] and ∄B ′ ∈ DAGi [r] : IDB ′ = IDB then 45: DAGi [r] ← DAGi [r] ∪ {B} 46: scheduled i ← scheduled i \ {B} 47: broadcast ⟨certified-block, B⟩ to every process in known i 48: output DAG-Deliveri (m, r, µ) 49: procedure S FloodDAGi 50: D← DAGi [u] u≥1 51: for all B ∈ D do 52: broadcast ⟨certified-block, B⟩ to every process in known i

▷ Finite snapshot

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

AdmissibleIDsi (R, u) contains the distinct identities in members(R) for which pi stores an admissible round-u block. On receiving Rl+1 , a member of Rl authenticates it, updates known i , waits until it has installed Rl and reached the earliest inclusion round, and then records Rl+1 in pending i . AdvanceRoundi is the only task that changes ri after round advancement starts, and its loop processes one value r = ri at a time. Normally it waits for the parent quorum required in round r and then sets ri to r + 1. The temporary Rc identifies the configuration whose quorum is required: it is normally the installed configuration, but it becomes Rl+1 in the last round before the transition completes. There is one additional way to advance by one round while transition i = ⟨Rl , Rl+1 , r0 ⟩. If r ∈ {r0 + 2, r0 + 3} and the process has at least ql+1 blocks in ParentBlocksi (Rl+1 , r + 1), it may set ri to r + 1 without first satisfying the ordinary round-r condition. These are certified, admissible blocks because ParentBlocksi selects blocks already inserted in DAGi . This rule lets a transitioning process use a later DAG layer that it received from another process. It never assigns a round beyond r + 1: after the increment, the same serialized loop evaluates the rule again for the new current round. In particular, reaching r0 + 4 invokes FinishTransitioni through the beginning-of-round rule before further advancement can occur. If the additional condition is used in round r0 + 2, the same stored round-(r0 + 3) set satisfies the ordinary condition in round r0 + 3 on the next iteration; the two increments are separate and no round is skipped. UpdateConfigsi (r) first learns a pending reconfiguration that appears in a marked block, if necessary. If at least fl + 1 blocks are marked, it calls InstallTransitioni ; otherwise it assigns the old singleton enabled-configs value for the following round. InstallTransitioni (Rl , Rl+1 , r) records the transition and assigns {Rl , Rl+1 } in rounds r + 1 through r + 4. FinishTransitioni (Rl+1 ) installs Rl+1 and clears the pending and transition values. The beginning-of-round rule calls it before ordinary block production in round r + 4, so an ordinary append in that round snapshots Rl+1 rather than Rl . After a removed process finishes the transition, it stops starting new block-production operations and stops round advancement, leader-election, and finalization tasks. While the departure wait is pending, every block-production operation invoked in an earlier round continues until it reaches BRB-Broadcast. The process continues its remaining BRB and DAG tasks, including processing received blocks, obtaining missing ancestors, and repeatedly invoking FloodDAG. It waits until

|AdmissibleIDsi (Rl+1 , r + 5)| ≥ fl+1 + 1, invokes one final FloodDAG, and then stops its remaining tasks.

A.5 A.5.1

Joining Process Transition Append

DAG-Transition-Appendi is used only by a joining process in rounds r0 + 2 and r0 + 3, where r0 is its install transition round. It waits for ql admissible parents, stores their references in h, declares Rl+1 , records the enabled pair {Rl , Rl+1 }, sets coin(m) = ⊥, and invokes the Rl+1 -scoped BRB.

XX:23

XX:24

Seamless Reconfiguration for DAG BFT

Algorithm 4 Reconfiguration procedure at process pi 1: transition i ← ⊥ 2: LocalBlocksi (Rl , r) = {⟨m, r, µ, C⟩ ∈ DAGi [r] | ID(µ) ∈ members(Rl )}. 3: For B = ⟨m, r, µ, C⟩, define Markedi (Rl , Rl+1 , B) ⇐⇒ ValidReconfiguration(Rl , Rl+1 ) ∧ ′

′

′

′

′

′

′

∃r , B = ⟨m , r , µ , C ⟩ ∈ DAGi [r ] : ′

′

B ⇝i B ∧ pending(µ ) = Rl+1 .

4: MarkedBlocksi (Rl , Rl+1 , r) = |{B ∈ LocalBlocksi (Rl , r) | Markedi (Rl , Rl+1 , B)}|. 5: AdmissibleIDsi (R, u) = {ID(µ) | B = ⟨m, u, µ, C⟩ ∈ DAGi [u], ID(µ) ∈ members(R), Admissiblei (B)}. receiving Rl+1 = ⟨RECONFIG, Πl+1 , l + 1, δl+1 ⟩, where Rl is its unique authenticated predecessor already known to pi , 6: upon with pi ∈ members(Rl ) and ValidReconfiguration(Rl , Rl+1 ) do 7: UpdateKnowni (Rl+1 ) 8: if number(local i ) > number(Rl ) then 9: return 10: await local i = Rl and ri ≥ earliest(Rl+1 ) 11: pending i ← Rl+1

12: procedure AdvanceRoundi 13: while true do 14: r ← ri
await local i ∈ enabled-configsi [r] and transition i = ⊥ ∨ (transition i = ⟨Rl , Rl+1 , r0 ⟩ ∧ r ≤ r0 + 3) 15: 16: Rl ← local i 17: if transition i = ⟨Rl , Rl+1 , r0 ⟩ and r = r0 + 3 then 18: Rc ← Rl+1 19: else 20: R c ← Rl 21: await either |ParentBlocksi (Rc , r)| ≥ qc 22: 23: 24:

or transition i = ⟨Rl , Rl+1 , r0 ⟩, r ∈ {r0 + 2, r0 + 3}, and |ParentBlocksi (Rl+1 , r + 1)| ≥ ql+1 if transition i = ⊥ then UpdateConfigsi (r) ri ← r + 1

25: procedure FinishTransitioni (Rl+1 ) 26: local i ← Rl+1 ; pending i ← ⊥; transition i ← ⊥ 27: procedure UpdateConfigsi (r) 28: Rl ← local i 29: if pending i = ⊥ and there exist Rl+1 and B ∈ LocalBlocksi (Rl , r) with Markedi (Rl , Rl+1 , B) then 30: UpdateKnowni (Rl+1 ) 31: pending i ← Rl+1 32: Rl+1 ← pending i 33: if Rl+1 ̸= ⊥ and MarkedBlocksi (Rl , Rl+1 , r) ≥ fl + 1 then 34: InstallTransitioni (Rl , Rl+1 , r) 35: else 36: enabled-configsi [r + 1] ← {Rl } 37: procedure InstallTransitioni (Rl , Rl+1 , r) 38: transition i ← ⟨Rl , Rl+1 , r⟩ 39: enabled-configsi [s] ← {Rl , Rl+1 } for every s ∈ {r + 1, r + 2, r + 3, r + 4} 40: upon the beginning of round r + 4, before ordinary block production, with transition i = ⟨Rl , Rl+1 , r⟩ and pi ∈ members(Rl ) do FinishTransitioni (Rl+1 ) if pi ∈ / members(Rl+1 ) then stop starting new block-production operations, and stop round advancement, leader-election, and finalization tasks at pi 44: while the departure wait below is pending, continue every previously invoked DAG-Append or DAG-Transition-Append until it reaches BRB-Broadcast 45: await |AdmissibleIDsi (Rl+1 , r + 5)| ≥ fl+1 + 1 46: FloodDAGi 47: stop all tasks at pi

41: 42: 43:

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Algorithm 5 Joining-process validation and transition append at pi 1: procedure DAG-Transition-Appendi (m, s, Rl , Rl+1 , r0 ) 2: if joining i = false or transition i ̸= ⟨Rl , Rl+1 , r0 ⟩ or s ∈ / {r0 + 2, r0 + 3} then 3: return 4: await |ParentBlocksi (Rl+1 , s − 1)| ≥ ql 5: S ← any ql blocks in ParentBlocksi (Rl+1 , s − 1) 6: h ← {⟨Hash(⟨m′ , s − 1, µ′ ⟩), ID(µ′ )⟩ | ⟨m′ , s − 1, µ′ , C ′ ⟩ ∈ S} 7: set coin(m) ← ⊥ 8: µ ← ⟨h, Rl+1 , ⊥, enabled-configsi [s], IDi ⟩ 9: BRB-Broadcasti (m, s, µ)

A.5.2

State Transfer

accepted-state-replies i counts state replies that have satisfied the state-reply handler’s conditions and have been merged. It lets ContinueDownloadi send another request after each accepted reply; the temporary a is the counter value recorded before the current request. ValidStatei (D, Rl+1 ) validates a finite set D received in a state reply. It rejects conflicting round-broadcaster slots, conflicts with DAGi , invalid certificates or metadata, and missing parents. For each round v, D[v] denotes the round-v blocks in that finite set. For every B = ⟨m, u, µ, C⟩ ∈ D, it also requires number(local(µ)) ≤ number(Rl+1 ), every configuration in enabled(µ) to have number at most number(Rl+1 ), and any non-⊥ pending(µ) to have number at most number(Rl+1 ). MergeStatei (D) processes the rounds of a valid set in increasing order so that parents are inserted before their children. DiscoverBegini (Rl , Rl+1 ) waits until some local DAG layer contains blocks from at least ql broadcaster identities in Πl , including at least fl + 1 blocks marked by Rl+1 , and returns the least such round. The procedure ContinueDownloadi , with arguments Rl and Rl+1 , repeatedly sends a state request to every identity in known i while pi is joining. It repeats after processing a state reply that satisfies the state-reply handler’s conditions or after known i changes. The temporary K is the value of known i used for the current request. The received set is written as Dj when it was sent by pj ; Di is the set sent by pi when it answers another process’s request. The state-request handler runs at every active process. A request satisfying its guard—a valid transition and a requester added by that transition— causes the recipient to send its finite ancestor-closed stored blocks for which the declared configuration, every configuration in the enabled field, and any non-⊥ pending configuration have number at most number(Rl+1 ). The state-reply handler and the other state-transfer operations run only while the receiving process is joining.

A.5.3

Joining Operation

HistoryTasksi contains certified-block receipt, DAG request/reply and state-reply processing, fetching, DAG delivery, and repeated FloodDAG invocations. CatchUpTasksi contains the BRB proposal, echo, and vote receive handlers and AdvanceRound. PostJoinTasksi contains the remaining protocol tasks, including ordinary block production. The first set starts before state discovery, the second starts after DiscoverBegin has returned u and the joining process has obtained the required round-(u + 1) blocks, and the third starts after the transition completes.

XX:25

XX:26

Seamless Reconfiguration for DAG BFT

Algorithm 6 Complete, ancestor-closed DAG state transfer 1: accepted-state-repliesi ← 0 The state-request handler below runs at every active process. All other actions in this algorithm run while pi is joining. 2: function ValidStatei (D, Rl+1 ) 3: For every round v, let D[v] = {⟨m, v, µ, C⟩ ∈ D} 4: if D is not finite, contains distinct blocks in the same round-broadcaster slot, or contains a block distinct from the block in the same round-broadcaster slot of DAGi then 5: return false ^

6:

ValidCertifiedMetadatai (B) ∧ ValidParentSeti (B, D)

return

B=⟨m,u,µ,C⟩∈D

∧ number(local(µ)) ≤ number(Rl+1 ) ∧ ∀R ∈ enabled(µ) : number(R) ≤ number(Rl+1 ) ∧

pending(µ) = ⊥ ∨ number(pending(µ)) ≤ number(Rl+1 )

7: procedure MergeStatei (D) 8: for all rounds u represented in D, in increasing order do 9: for all B = ⟨m, u, µ, C⟩ ∈ D do 10: AddAndDeliveri (B) 11: function DiscoverBegini (Rl , Rl+1 ) 12: await there exists u ≥ 1 such that |LocalBlocksi (Rl , u)| ≥ ql and MarkedBlocksi (Rl , Rl+1 , u) ≥ fl + 1 13: return the least such u 14: procedure ContinueDownloadi (Rl , Rl+1 ) 15: while joining i = true do 16: K ← known i 17: a ← accepted-state-repliesi 18: broadcast ⟨state-request, Rl , Rl+1 ⟩ to every process in K 19: await either joining i = false, accepted-state-repliesi > a, or known i ̸= K receiving ⟨state-reply, Rl , Rl+1 , Dj ⟩ from pj ∈ known i with joining i = true, pending i = Rl+1 , 20: upon ValidReconfiguration(Rl , Rl+1 ), and ValidStatei (Dj , Rl+1 ) do 21: MergeStatei (Dj ) 22: accepted-state-repliesi ← accepted-state-repliesi + 1 23: upon receiving ⟨state-request, Rl , Rl+1 ⟩ from pj with ValidReconfiguration(Rl , Rl+1 ) and pj ∈ members(Rl+1 ) \ members(Rl ) do 24: UpdateKnowni (Rl+1 ) S 25: Di ← the maximal finite ancestor-closed subset of DAGi [u] for which every B = ⟨m, u, µ, C⟩ satisfies u≥1

26:

number(local(µ)) ≤ number(Rl+1 ), number(R) ≤ number(Rl+1 ) for every R ∈ enabled(µ), and pending(µ) = ⊥ or number(pending(µ)) ≤ number(Rl+1 ) send ⟨state-reply, Rl , Rl+1 , Di ⟩ to pj

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Algorithm 7 Joining operation at process pi 1: Let HistoryTasksi consist of certified-block receipt, DAG request/reply and state-reply handlers, fetch/deliver workers, and repeated FloodDAG.

2: Let CatchUpTasksi consist of the BRB proposal, echo, and vote receive handlers and AdvanceRound. 3: PostJoinTasksi = all remaining non-joining protocol tasks, including ordinary block production. The task sets are pairwise disjoint. The state-request handler is not in these sets and runs whenever pi is active. History tasks may insert and DAG-deliver certified blocks but never invoke DAG-Append or DAG-Transition-Append, echo, vote, or advance a round. 4: upon receiving the authenticated pair ⟨Rl , Rl+1 ⟩, where Rl+1 = ⟨RECONFIG, Πl+1 , l + 1, δl+1 ⟩, such that ValidReconfiguration(Rl , Rl+1 ), pi ∈ / members(Rl ), and pi ∈ members(Rl+1 ) do 5: UpdateKnowni (Rl+1 ) 6: stop all protocol tasks except the state-request handler and this joining operation 7: start HistoryTasksi 8: pending i ← Rl+1 ; local i ← R1 ; enabled-configsi [1] ← {R1 } 9: joining i ← true 10: spawn ContinueDownloadi (Rl , Rl+1 ) 11: r ← DiscoverBegini (Rl , Rl+1 ) 12: local i ← Rl 13: passive-roundsi ← passive-roundsi ∪ {r + 1} 14: InstallTransitioni (Rl , Rl+1 , r) 15: await |LocalBlocksi (Rl , r + 1)| ≥ ql 16: ri ← r + 1 17: start CatchUpTasksi 18: upon the beginning of round s with input m and transition i = ⟨Rl , Rl+1 , r⟩ and s ∈ {r + 2, r + 3} do 19: DAG-Transition-Appendi (m, s, Rl , Rl+1 , r) 20: upon the beginning of round r + 4, before ordinary block production, with joiningi = true and transition i = ⟨Rl , Rl+1 , r⟩ do 21: FinishTransitioni (Rl+1 ) 22: joining i ← false 23: start PostJoinTasksi

A.6

Leader Election and Finalization

VotingBlocksi (Rl , w) contains the singleton-enabled last-round blocks for wave w that are declared under Rl and carry a valid Rl -scoped coin share. WaveConfigsi (w) contains the configurations for which at least one such block is present. Sharesi (Rl , w) extracts one valid coin share per broadcaster from those blocks. Supporti (B, Rl , w) counts the Rl -typed leader-voting blocks whose causal history contains B. HistorySupporti (B ⋆ , B, Rl , w) counts the leader-voting blocks that lie in the causal history of B ⋆ and whose own causal history contains B. WaveLeader(Rl , w) combines exactly fl + 1 valid coin shares. The resulting configurationscoped coin selects one member of Πl . The function returns that member’s locally stored round-first(w) block declared under Rl , and returns ⊥ otherwise. The temporary Sl,w is the combined coin signature. finalized-values i is the sequence of elected leader blocks finalized by pi . processed-wave i is the greatest wave through which its backward scan has completed. TryElecti (w) constructs A, the set of locally available coin-selected candidates having support at least ql . It calls Electi only when this set contains exactly one block. Electi (B, k) scans the unprocessed waves preceding k in reverse order. The temporary v is the previously processed wave, L is the sequence being constructed, and B ⋆ is the most recently accepted block used for the next causal-history check. For each earlier wave, Ew contains the candidates having history support at least fl + 1. A unique such candidate is prepended to L. The procedure then appends L to finalized-values i and sets processed-wave i to k. Invocations of TryElecti and Electi at one process are serialized.

XX:27

XX:28

Seamless Reconfiguration for DAG BFT

Algorithm 8 Leader-selection helpers at process pi Use the four-round wave boundaries first(w) and last(w) defined in Section 3. We use LocalBlocksi from  algorithm 4 and ⇝i from Section 3.4. VotingBlocksi (Rl , w) = B | B = ⟨m, last(w), µ, C⟩, B ∈ LocalBlocksi (Rl , last(w)), local(µ) = Rl , enabled(µ) = {Rl }, COIN

coin(m) ̸= ⊥ ∧ ValidShareID(µ),l (coin(m), ⟨w⟩) . ▷ Blocks with both configurations enabled remain in the DAG but do not participate in leader election WaveConfigsi (w) = {Rl | VotingBlocksi (Rl , w) ̸= ∅}. Every broadcaster pj that is uncorrupted at production fixes the parent set of its singleton-enabled last-round block before generating and releasing its share. The share is τj,l,w = ShareSignCOIN j,l (⟨w⟩). Sharesi (Rl , w) =



⟨j, τj,l,w ⟩

∃B = ⟨m, last(w), µ, C⟩ : B ∈ VotingBlocksi (Rl , w), j = ID(µ) and τj,l,w = coin(m) .

Supporti (B, Rl , w) =



X = ⟨mX , last(w), µX , CX ⟩ ∈ VotingBlocksi (Rl , w),

ID(µX )

⋆

HistorySupporti (B , B, Rl , w) =

X ⇝i B

.

ID(µX )

X = ⟨mX , last(w), µX , CX ⟩ ∈ VotingBlocksi (Rl , w),



⋆

B ⇝i X ∧ X ⇝ i B

.

1: function WaveLeader(Rl , w) ▷ Coin and candidate under Rl if |Sharesi (Rl , w)| < fl + 1 then return ⊥ Sl,w ← the threshold signature generated from exactly fl + 1 entries of Sharesi (Rl , w) pj ← the process selected by the fair configuration-scoped coin reconstructed from Sl,w ▷ The coin selects this first-round slot 6: return the block Bj = ⟨mj , first(w), µj , Cj ⟩ in LocalBlocksi (Rl , first(w)) with local(µj ) = Rl and ID(µj ) = j, or ⊥ if no such block exists

2: 3: 4: 5:

Algorithm 9 Leader election and finalization at process pi 1: finalized-valuesi ← ⟨⟩; processed-wavei ← 0

▷ Store elected leader blocks in wave order The event handler and its calls to TryElect and Elect execute as one serialized local task; a later trigger waits until the current invocation returns. upon completing wave w, or upon DAG-delivering a new block in VotingBlocksi (Rl , w) for some Rl , do 2: TryElecti (w)

3: procedure TryElecti (w) 4: if w ≤ processed-wavei then 5: return A←

∃Rl ∈ WaveConfigsi (w) : B = WaveLeader(Rl , w) ∧ B ̸= ⊥,

B

▷ All sufficiently supported Supporti (B, Rl , w) ≥ ql .

6: 7:

candidates if A = {B} then Electi (B, w)

8: procedure Electi (B, k) 9: v ← processed-wavei 10: if k ≤ v then 11: return 12: L ← ⟨B⟩ 13: B⋆ ← B 14: forw ← k − 1 downto v + 1 do Ew ←

B

′

▷ Scan unprocessed waves backward

▷ Current scan anchor ′

′

∃Rl ∈ WaveConfigsi (w) : B = WaveLeader(Rl , w) ∧ B ̸= ⊥, ⋆

′

HistorySupporti (B , B , Rl , w) ≥ fl + 1 .

15: 16: 17: 18: 19:

▷ All candidates supported through B ⋆ if Ew = {B ′ } then prepend B ′ to L B⋆ ← B′ ▷ Continue from the accepted earlier leader atomically append the blocks of L, in order, to finalized-valuesi processed-wavei ← k ▷ Ambiguous skipped waves are not reconsidered

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

B

Proofs

Proof Conventions. We use the system model, configuration notation, definitions of active and correct processes, and definitions of configuration-scoped BRB, Dynamic DAG-structured Byzantine Broadcast, and Dynamic DAG Byzantine Atomic Broadcast from Section 3. In particular, nl , fl , and ql have the meanings fixed there. The following consequences will be used repeatedly: nl ≥ 3fl + 1,

ql ≥ 2fl + 1,

ql − fl = nl − 2fl ≥ fl + 1.

Throughout, the issuance-rule assumption states that the dealer follows the issuance rule of Section 4.2: before issuing Rl+1 , it observes, in correct ancestor-closed DAG snapshots, ql certified blocks from distinct broadcaster slots, all declared under Rl , in round earliest(Rl+1 )− 2. For clarity, a process is active while it executes at least one protocol task. An active correct process continues every task prescribed at that stage and processes every delivered protocol message. A correct member of an installed configuration remains active until the reconfiguration protocol permits it to leave. A correct joining process becomes active for statetransfer when it receives the authenticated pair ⟨Rl , Rl+1 ⟩ that adds it. A joining process that is temporarily passive with respect to block production and BRB may therefore still be active because it continues its prescribed state-transfer tasks. Once a removed process is permitted to leave and stops all prescribed tasks, it is no longer active. When a process enters its transition-completion round, the FinishTransition beginning-of-round action executes before that round’s ordinary block production snapshots its metadata. For a removed process, stopping block production means that it starts no new block-production operation. While its departure wait is pending, every DAG-Append or DAG-Transition-Append operation invoked in an earlier round continues until it reaches BRB-Broadcast. If the departure condition becomes true first, the process performs its final FloodDAG and may then stop the still-pending operation with its other remaining tasks. For a fixed transition Rl → Rl+1 , an old member is a process in members(Rl ). Thus, a correct old member is a correct process in members(Rl ), whether it is retained in Rl+1 or removed by the transition. The term old describes membership relative to the transition, not whether the process is active; activity is stated separately when required.

Configuration-Level Induction Hypothesis. For a valid transition Rl → Rl+1 , let δl+1 = earliest(Rl+1 ). The configuration-level induction hypothesis for Rl states that: 1. Every correct member of Rl has installed Rl ; 2. Every correct process removed by the preceding transition has reached the point at which it may leave; 3. BRB Agreement holds in every round before δl+1 ; and 4. There is a logical round that every active correct member of Rl eventually enters with Rl installed and in which at least ql active correct members invoke the prescribed Rl -declared DAG-Append operation and reach its call to BRB-Broadcast. For R1 , the clauses concerning a preceding transition are vacuous. This hypothesis is a proof invariant, not an additional assumption on the execution. It is established for every issued transition by lemma 48; its induction step from Rl to Rl+1 is lemma 47.

XX:29

XX:30

Seamless Reconfiguration for DAG BFT

Within the proof for Rl → Rl+1 , “the conclusions for preceding transitions” means the conclusions already established for transitions ending at Rl , including the bounds on install transition rounds and the conclusions about transition completion, permission for removed correct processes to leave, and BRB Agreement. We use the install transition round and marked-block terminology of Section 4. For a process with install transition round ai , round ai + 3 is its final transition round and round ai + 4 is its transition-completion round. Throughout, an enabled-configs value is the process-local value enabled-configs i [r]. For a round-r block with metadata µ, enabled(µ) is the enabled-configs value recorded by the broadcaster. If a correct process pi produces the block, then enabled(µ) = enabled-configs i [r]. For a Byzantine broadcaster, the recorded field need not represent genuine process-local state. By contrast, local(µ) is the block’s single declared configuration and determines the configuration under which its BRB certificate is formed. Except for the joining process’s DAG-Transition-Append, a parent-quorum condition at process pi uses the same configuration Rc both to select eligible round-s parents and to set the required threshold: |ParentBlocksi (Rc , s)| ≥ qc . In the exceptional append, the joining process selects eligible parents from ParentBlocksi (Rl+1 , s) but needs only ql of them. Thus, Rl+1 determines which parents are eligible, whereas the predecessor threshold ql determines how many are required. For an AdvanceRoundi iteration with frozen current round r and selected configuration Rc , we call |ParentBlocksi (Rc , r)| ≥ qc the ordinary parent-quorum condition. When transition i = ⟨Rl , Rl+1 , r0 ⟩ and r ∈ {r0 +2, r0 +3}, we call |ParentBlocksi (Rl+1 , r+1)| ≥ ql+1 the additional transition-round condition. For a correct process, an ordinary block is a block produced by its prescribed DAG-Append operation, rather than by DAG-Transition-Append. Whenever a result below says that BRB Agreement holds for a round-broadcaster slot, we prove and use the following certificate-level statement: any two valid quorum certificates for that slot bind the same complete BRB value. This statement implies the BRB Agreement property of Section 3.6, and it also rules out a conflicting certified block received through a certified-block message, state reply, or DAG reply even when the recipient did not first BRB-deliver that block. The certificate-level statement is established by lemma 5 and is preserved in every later result that invokes that lemma to establish BRB Agreement. We say that BRB Agreement holds in round r when it holds for every round-broadcaster slot in round r, and that it holds through round r when it holds for every round-broadcaster slot whose round index is at most r. For a correct process pi and blocks in its DAG, we use the causal relation Y ⇝i X from Section 3; thus X is in the causal history of Y . When a statement has already fixed the correct process whose DAG is under discussion, we may omit the subscript and write Y ⇝ X. For any block Y = ⟨mY , rY , µY , CY ⟩ and any round s ≤ rY , let HY,i (s) = {X = ⟨mX , s, µX , CX ⟩ ∈ DAGi [s] | Y ⇝i X} denote the round-s layer of the causal history of Y at pi . After fixing pi , we abbreviate this set by HY (s).

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Proof Roadmap. The proof proceeds in six steps. 1. BRB Integrity and Agreement. Under the configuration-level induction hypothesis, the issuance rule gives the starting conditions for each transition (lemmas 7 and 8). Lemma 4 proves Integrity, and lemma 5 proves Agreement when certificates use one configuration or the two configurations of one valid transition. Lemma 17 establishes alignment and Agreement in every round in which a correct old member’s assigned enabled-configs value contains Rl . 2. DAG delivery and round advancement. Lemma 20 proves that every correct process’s DAG contains the ancestors of each stored block. Lemmas 24 and 25 establish dissemination under their stated Agreement, validation, and activity conditions. Lemma 26 and corollary 28 give the corresponding round-advancement results. 3. Transition progress, completion, and departure. Lemmas 45 and 46 establish the earliest correct old-member install transition round t and, for a correct joining process, the discovery round u. Corollary 29 and lemma 32 bound the install transition rounds, and lemma 35 covers the remaining joining-process Agreement case. Corollary 41 and lemmas 42 and 43 prove transition progress, completion, and permission to leave. Lemma 44 supplies the round required for the next configuration-level induction step. 4. Configuration-level induction and Dynamic DAG-structured Byzantine Broadcast. Lemmas 47 and 48 establish the induction hypothesis throughout the authenticated configuration sequence for every configuration with an issued successor. Lemmas 49–51 then establish Reconfiguration Completion and Dynamic DAG-structured Byzantine Broadcast. 5. Leader Integrity and Total Order. Lemma 52 proves that transition windows are disjoint. Lemmas 56, 61, and 62 establish consistent leader choices and nested leader sequences. Corollary 64 and theorem 65 conclude Leader Integrity and Total Order. 6. Probabilistic Progress. After the final reconfiguration, corollaries 66 and 67 establish continuing round progress under RL . Lemma 68 and corollary 69 establish the common core and its availability. Under the conditional probability requirement, proposition 70, lemma 71, , and theorem 72 prove that every correct RL -member that remains active finalizes infinitely many blocks with probability one. Theorem 3 combines these results to establish Dynamic DAG Byzantine Atomic Broadcast.

B.1

Dynamic DAG-structured Byzantine Broadcast Progress and Reconfiguration

Assumptions and Process Operations. We use the system and reconfiguration assumptions of Section 3. Correct processes invoke the prescribed DAG-Append or DAG-Transition-Append operation. Each authenticated Rc carries dealer-authenticated evidence for every identity that appeared in R1 , . . . , Rc−1 . On accepting Rc , a correct process pi invokes UpdateKnowni (Rc ). If Rc is the highest-numbered Sc reconfiguration message it has processed, then known i = d=1 members(Rd ), and immediately UpdateKnowni (Rc ) invokes one finite FloodDAG whenever this set grows. Every later insertion sends its complete certified block to every identity in known i , every active correct process repeatedly invokes FloodDAG, and a removed correct process performs one final finite flood before stopping its remaining DAG tasks. Certified-block messages addressed to an identity before it activates are queued and processed when it activates. While active, a correct process executes the prescribed certified-block receive, fetch, FloodDAG, and applicable state-request

XX:31

XX:32

Seamless Reconfiguration for DAG BFT

and state-reply handlers. These are protocol actions, not an assumption that a particular process storing a block remains available until every lagging process catches up. When Rl+1 adds a process, the dealer sends it the authenticated pair ⟨Rl , Rl+1 ⟩. The joining process therefore knows the full membership and thresholds of Rl without receiving all earlier reconfiguration messages. Every valid quorum certificate for a complete value ⟨m, s, µ⟩ contains a vote from a correct process pv that checked ValidParentCountv (s, µ) when the certificate was formed. A process pi later validating a certified block B = ⟨m, s, µ, C⟩ may therefore apply CertifiedParentCount(s, µ); it need not reconstruct its own enabledconfigs value for the earlier round. The predicate ValidCertifiedMetadatai (B) requires the declared configuration to be R1 or to carry valid authorization evidence, and applies the corresponding checks to every configuration named by the metadata. In particular, suppose a certified block B = ⟨m, s, µ, C⟩ satisfies JoiningMetadata(µ, Rl , Rl+1 ) and uses ql parents while declaring Rl+1 . If ql < ql+1 , a correct process pv accepts this parent count only if enabled-configs v [s] = {Rl , Rl+1 } and ValidReconfiguration(Rl , Rl+1 ) hold. If ql = ql+1 , the parent count satisfies the ordinary rule and does not require the voter’s enabled-configs value to equal the pair. In either case, a process that later receives B applies CertifiedParentCount(s, µ) to the immutable metadata and does not require its own enabled-configs value for round s. The analysis uses the issuance-rule assumption; lemma 52 derives from it that transition windows of distinct transitions are disjoint. A block is admissible at process pi if it passes all checks required for insertion into pi ’s DAG: its certificate and metadata are valid, and its referenced parents satisfy the applicable identity, configuration-number, and parent-count checks. In particular, if µ′ is the metadata of a parent, that parent’s broadcaster belongs to members(Rc ) for some Rc ∈ enabled(µ′ ). During a transition, enabled(µ′ ) may be the pair {Rl , Rl+1 } comprising the two configurations of a valid transition; hence a certified block from a process removed by Rl+1 may still be used as a parent during that transition. The parent must also satisfy number(local(µ′ )) ≤ number(local(µ)), where µ is the child metadata. A valid round-r certificate declared under Rc contains a share from at least one correct voter pv satisfying Rc ∈ enabled-configs v [r]. The lemmas below therefore determine which configurations may be declared by valid round-r certificates. Correct processes apply the same metadata checks to parents selected by Byzantine broadcasters. Accordingly, at process pi , B ∈ LocalBlocksi (Rl , r) means that B is already in DAGi [r] and hence has passed the applicable DAG-insertion predicate, and that its broadcaster slot belongs to members(Rl ). It does not assert that the block is declared under Rl , i.e., it need not satisfy local(µ) = Rl . The prescribed DAG-Append invocation by pi snapshots local i , pending i , and enabled-configs i [r] before waiting for parents and records those values in the block metadata. Moreover, a correct process rejects a pending reconfiguration in any round earlier than the authenticated earliest-inclusion round earliest(Rc ) of that pending configuration Rc . The authenticated reconfiguration message covers that round. Hence neither a delayed correct append nor a Byzantine broadcaster can obtain a certificate that places a later message in a block’s pending field before that round. For a fixed transition Rl → Rl+1 , we say that the round-r enabled-configs values assigned by correct processes in members(Rl ) are aligned if every assigned value is one of {Rl },

{Rl , Rl+1 },

{Rl+1 },

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

and there do not exist correct pi , pj ∈ members(Rl ) such that enabled-configs i [r] = {Rl }

and

enabled-configs j [r] = {Rl+1 }.

Here and below, an “assigned” value means a value different from ⊥. Thus the pair may coexist with either singleton, but the old and new singletons cannot coexist. Here the old singleton is {Rl } and the new singleton is {Rl+1 }. A pair belonging to another transition in the same round is excluded within the alignment proofs by the predecessor-completion and earliest-inclusion bounds, and in general by lemma 52. Whenever one of these correct processes pi starts a round-r append with metadata µ, it records enabled(µ) = enabled-configs i [r]. Consequently, the enabled(µ) fields recorded by round-r blocks produced by these correct processes are drawn from the aligned process-local values. The alignment condition is stated for process-local enabled-configs values because a correct process may assign a value for a round without producing a block in that round.

BRB Integrity and Agreement when Certificates Use One Configuration or the Two Configurations of One Valid Transition. The BRB algorithm supplies Integrity independently of reconfiguration. Agreement is proved separately after restricting the configurations that can certify one slot. ▶ Lemma 4 (BRB Integrity). The configuration-scoped BRB algorithm in algorithm 2 satisfies BRB Integrity. Moreover, every valid certificate in a correct broadcaster’s round-broadcaster slot binds the complete value supplied to that broadcaster’s prescribed BRB invocation. Proof. A correct process BRB-delivers at most once per slot and only after verifying a certificate under the declared configuration’s threshold key. Under the BRB algorithm, a correct process first votes for a value declared under Rc only after receiving either qc valid echoes or fc + 1 valid votes for that value. When the declared broadcaster is correct, consider the earliest correct process that votes for the certified value. This process cannot use the fc + 1-vote relay rule: among those votes at least one is correct, contradicting the choice of the earliest correct voter. It must therefore have received qc valid echoes, including a correct echo. A correct process sends an echo only after receiving the authenticated initial message from the declared broadcaster. Hence a value attributed to a correct broadcaster originates in that broadcaster’s prescribed BRB invocation. ◀ ▶ Lemma 5 (Two valid certificates for one round-broadcaster slot cannot bind different values within one configuration or one valid transition). Fix a round-broadcaster slot (r, ID). Any two valid BRB quorum certificates for this slot under the same declared configuration bind the same complete BRB value ⟨m, r, µ⟩ and, by threshold-signature uniqueness, are the same certificate. For any valid transition Rl → Rl+1 , a valid certificate for this slot declared under Rl and a valid certificate for this slot declared under Rl+1 cannot both be formed. Consequently, if certificates for the slot can be formed only under one configuration or under the two configurations of one valid transition, any two valid certificates for the slot bind the same complete BRB value. In particular, any two correct processes that BRB-deliver for the slot deliver that same value.

XX:33

XX:34

Seamless Reconfiguration for DAG BFT

Proof. If two certificates are declared under the same configuration Rc , their voter sets intersect in at least 2qc − nc ≥ fc + 1 members and hence in a correct process. If one certificate is declared under Rl and the other under Rl+1 , an addition gives a voter-set intersection of at least ql + ql+1 − nl+1 ≥ fl+1 + 1, whereas a removal gives an intersection of at least ql + ql+1 − nl ≥ fl + 1. If the memberships are unchanged, then nl+1 = nl , fl+1 = fl , and ql+1 = ql , so the intersection has size at least 2ql − nl ≥ fl + 1. In all three cases, the intersection contains a correct process. A correct process casts at most one vote in a fixed round-broadcaster slot, and that vote binds the complete value ⟨m, r, µ⟩. Therefore, certificates under one configuration bind the same tuple and, by threshold-signature uniqueness under that configuration’s key, are the same certificate. Certificates declared under the two configurations of the valid transition cannot both be formed, because a correct process in their voter-set intersection would have to vote twice in the slot. ◀

B.1.1

Consequences of the Issuance Rule for Earliest-Inclusion and Install Transition Rounds

Consequences of the Issuance Rule. For the lemmas in this subsection, fix a transition Rl → Rl+1 , let δl+1 = earliest(Rl+1 ), and suppose that, before issuing Rl+1 , the dealer observes, as its issuance rule in Section 4.2 prescribes, ql certified blocks from distinct broadcaster slots, all declared under Rl , in round δl+1 − 2. ▶ Lemma 6 (No certified block below δl+1 contains Rl+1 in its pending field). No certified block below round δl+1 has pending field Rl+1 . Proof. Every correct echoer and voter rejects a block in round s < δl+1 whose pending field contains Rl+1 . At most fc members of any declared configuration Rc are Byzantine, and qc > fc . Byzantine members alone therefore cannot form a quorum certificate. ◀ ▶ Lemma 7 (Before acting in round δl+1 − 1, an active correct Rl -member has installed Rl and completed any transition into it). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption, let δl+1 = earliest(Rl+1 ), and assume the configuration-level induction hypothesis for Rl and the conclusions already established for preceding transitions. Every correct process pi ∈ members(Rl ) that is still active when it reaches logical round δl+1 − 1 has already installed Rl . If l > 1, it has also completed the transition into Rl before performing any round-(δl+1 − 1) protocol action. Proof. The claim is immediate for the initial configuration R1 . Otherwise, let t′ be the earliest correct old-member install transition round for the preceding transition into Rl . The

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

conclusions already established for the preceding transition imply that every correct process retained in Rl installs in round t′ or t′ + 1 and completes the transition at the beginning of round t′ + 4 or t′ + 5. A correct process added by that transition has install transition round in {t′ − 1, t′ , t′ + 1} and also completes by round t′ + 5. Before round t′ + 4, no correct process in members(Rl−1 ) can produce a block declared under Rl . Such blocks can occupy at most the fl Byzantine slots and, for an addition, the joining process’s slot. Since fl + 1 < ql , the observed ql blocks in round δl+1 − 2 imply δl+1 − 2 ≥ t′ + 4. Thus every active correct process in members(Rl ) completes the transition into Rl by t′ + 5 ≤ δl+1 − 1. ◀ ▶ Lemma 8 (Every assigned round-δl+1 enabled-configs value of a correct Rl -member is {Rl }). Every correct process pi ∈ members(Rl ) for which enabled-configs i [δl+1 ] is assigned satisfies enabled-configs i [δl+1 ] = {Rl }. Proof. By lemma 7, pi has completed the transition into Rl . By lemma 6, no block below δl+1 is marked by Rl+1 , so no correct process can invoke InstallTransition with an install transition round below δl+1 . An invocation with install transition round ai assigns {Rl , Rl+1 } only to rounds ai + 1, . . . , ai + 4; it never changes the value for round ai . Hence the assigned value for round δl+1 is {Rl }. ◀ ▶ Lemma 9 (From round δl+1 −1 until transition completion, every block a correct process counts toward an Rl parent quorum has an Rl -member broadcaster). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption, let δl+1 = earliest(Rl+1 ), and assume the configuration-level induction hypothesis for Rl and the conclusions already established for preceding transitions. Let pi be correct. Before pi invokes FinishTransitioni (Rl+1 ), let s ≥ δl+1 − 1 be any round for which the protocol requires pi to satisfy |ParentBlocksi (Rl , s)| ≥ ql . Then every block B = ⟨m, s, µ, C⟩ ∈ ParentBlocksi (Rl , s) satisfies ID(µ) ∈ members(Rl ). Proof. The conclusions already established for preceding transitions imply that configurations earlier than Rl−1 cannot contribute certified blocks in these rounds. Hence the only possible broadcaster identity outside members(Rl ) comes from the immediately preceding membership members(Rl−1 ). If the transition into Rl added a member, then members(Rl−1 ) ⊆ members(Rl ), so there is no such identity. Suppose instead that the transition removed one member, so |members(Rl−1 )| = nl + 1. Among the observed ql round-(δl+1 − 2) blocks declared under Rl , at least ql − fl = nl − 2fl have correct broadcasters. For each such correct broadcaster ph , let ah be its install transition round for Rl−1 → Rl . Because that transition is a removal, ph is retained; there is no joining process whose DAG-Transition-Append can declare Rl before transition completion. By algorithm 4, an ordinary block produced by ph declares Rl only after FinishTransition executes at the beginning of round ah + 4. Its observed Rl -declared block in round δl+1 − 2 therefore implies ah + 4 ≤ δl+1 − 2.

XX:35

XX:36

Seamless Reconfiguration for DAG BFT

Thus δl+1 − 1 ≥ ah + 5, whereas InstallTransition assigns {Rl−1 , Rl } only in rounds ah + 1, . . . , ah + 4. Moreover, by lemma 10, no correct process installs Rl → Rl+1 with an install transition round below δl+1 . Hence every assigned value in round s ≥ δl+1 − 1 excludes Rl−1 . For the fixed round s, if enabled-configs h [s] is unassigned, ph emits no share; otherwise it refuses every round-s BRB instance declared under Rl−1 . Because nl − 2fl ≥ fl−1 + 1, fewer than ql−1 vote shares can ever be emitted for such an instance. Delayed messages cannot increase that number. A block declared under Rl+1 cannot belong to ParentBlocksi (Rl , s) because it violates number(Rl+1 ) ≤ number(Rl ). Every remaining counted block therefore has a broadcaster in members(Rl ), including a member removed by Rl → Rl+1 . ◀ ▶ Lemma 10 (No correct process invokes InstallTransition with install transition round below δl+1 ). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuancerule assumption, and let δl+1 = earliest(Rl+1 ). No correct process pi ∈ members(Rl ) ∪ members(Rl+1 ) invokes InstallTransitioni (Rl , Rl+1 , ai ) with ai < δl+1 . Consequently, if  t = min ai : pi ∈ members(Rl ) is correct and invokes InstallTransitioni (Rl , Rl+1 , ai ) exists, then t ≥ δl+1 . Proof. An invocation with install transition round ai is justified by fl + 1 round-ai blocks marked for Rl → Rl+1 : at a correct old member through MarkedBlocksi (Rl , Rl+1 , ai ) ≥ fl + 1 in algorithm 4, and at a joining process through the discovery condition of algorithm 6. A marked block has, in its reflexive causal history, a certified block whose pending field contains Rl+1 , and the causal history of a round-ai block lies in rounds at most ai . By lemma 6, no certified block below round δl+1 has pending field Rl+1 . Hence no round-ai block is marked when ai < δl+1 , and no such invocation occurs. ◀

B.1.2

Enabled-Configs Alignment and BRB Agreement During Rl → Rl+1

Alignment of Assigned Enabled-Configs Values and BRB Agreement. We first establish two prerequisites: a following reconfiguration Rl+1 → Rl+2 cannot become applicable while correct processes may still assign enabled-configs values containing Rl , and evidence of Rl → Rl+1 propagates through marked blocks. We then rule out a first logical round in which alignment or BRB Agreement fails. This establishes that the enabled-configs values assigned by correct processes remain aligned for Rl → Rl+1 and that every valid certificate is declared under either Rl or Rl+1 throughout the transition. ▶ Lemma 11 (Issuing Rl+2 requires a correct Rl -member to invoke InstallTransition for Rl → Rl+1 ). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption. If the dealer issues Rl+2 , then there exist a correct process pi ∈ members(Rl ) and a round ai such that pi invokes InstallTransitioni (Rl , Rl+1 , ai ). In particular, the set of install transition rounds of correct processes in members(Rl ) is nonempty.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Proof. Without an invocation of InstallTransition by a correct old member, blocks declared under Rl+1 can occupy only the fl+1 Byzantine Rl+1 -member slots and, during an addition, the joining process’s single slot. These are fewer than ql+1 distinct roundbroadcaster slots. The dealer’s issuance rule (Section 4.2) requires it to observe, before issuing Rl+2 , at least ql+1 certified blocks declared under Rl+1 in distinct broadcaster slots in one round; this cannot happen unless a correct old member has invoked InstallTransition for Rl → Rl+1 . ◀ ▶ Lemma 12 (If t is the earliest correct old-member install transition round for Rl → Rl+1 , then earliest(Rl+2 ) ≥ t + 6). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption, and suppose that the dealer issues Rl+2 . Let t be the earliest install transition round among correct processes in members(Rl ) for Rl → Rl+1 . This round exists by lemma 11. Then earliest(Rl+2 ) ≥ t + 6. Proof. A correct process in members(Rl ) declares Rl+1 in a block only after invoking FinishTransition, which occurs at the beginning of round ai + 4 for its install transition round ai ≥ t. Hence no correct old member produces an Rl+1 -declared block before round t + 4. As in the proof of lemma 11, certified Rl+1 -declared blocks in any round below t + 4 therefore occupy at most the fl+1 Byzantine Rl+1 -member slots and, during an addition, the joining process’s single slot; a correct joining process may indeed produce its Rl+1 -declared transition blocks before round t + 4. Since fl+1 + 1 < ql+1 , no round below t + 4 contains ql+1 certified Rl+1 -declared blocks in distinct round-broadcaster slots. The first round in which the dealer can observe ql+1 such blocks is therefore at least t + 4. The dealer’s snapshot rule sets earliest(Rl+2 ) two rounds above the observed round, so earliest(Rl+2 ) ≥ t + 6. ◀ ▶ Lemma 13 (Every round-(t + 1) block produced by a correct Rl -member is marked for Rl → Rl+1 at every correct process that DAG-delivers it). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and assume the conclusions already established for preceding transitions. Let t be the earliest install transition round among correct processes in members(Rl ). Suppose BRB Agreement holds through round t. Let X = ⟨m, t + 1, µX , CX ⟩ be a certified block produced by a correct process in members(Rl ). At every correct process pi that DAG-delivers X, Markedi (Rl , Rl+1 , X) holds. Equivalently, for every such pi , there exist a round s and a block X ′ = ⟨m′ , s, µ′ , C ′ ⟩ ∈ DAGi [s] such that X ⇝i X ′

and

pending(µ′ ) = Rl+1 .

Proof. An installation with install transition round t is justified by fl + 1 marked round-t blocks. Each such block either records Rl+1 in its own pending field or has an earlier ancestor that does. By lemma 6, no such pending field can occur below round δl+1 , so t ≥ δl+1 , and the Agreement premise includes round δl+1 . Let M be the set of the fl + 1 marked round-t blocks that justify the earliest installation. By lemma 9, these blocks occupy distinct

XX:37

XX:38

Seamless Reconfiguration for DAG BFT

round-broadcaster slots in members(Rl ), and Agreement in round t ensures that whenever another correct process DAG-delivers a block in one of these slots, it delivers the same certified block and its required ancestry; the block is therefore marked there as well. Let X be a round-(t + 1) block produced by a correct member of members(Rl ). If its broadcaster installed in round t, the pending field in X contains Rl+1 . Otherwise, its prescribed Rl -declared DAG-Append block has ql round-t parents. Their slots and M lie in the same nl -member configuration, so |HX (t) ∩ M| ≥ ql + (fl + 1) − nl = 1. Thus X has a marked ancestor and is itself marked.

◀

▶ Lemma 14 (Every correct Rl -member that advances to round t + 2 has install transition round t or t + 1 for Rl → Rl+1 ). Under the assumptions and notation of lemma 13, let pi ∈ members(Rl ) be correct. If |ParentBlocksi (Rl , t + 1)| ≥ ql and pi advances to round t + 2, then it has invoked InstallTransitioni (Rl , Rl+1 , ai ) for some ai ∈ {t, t + 1}. Moreover, every correct process in members(Rl ) that ever invokes InstallTransition for this transition has an install transition round in {t, t + 1}. Proof. Consider a correct process that advances through round t + 1 without installing in round t. It obtains ql admissible round-(t + 1) blocks in ParentBlocksi (Rl , t + 1). By lemma 9, their broadcasters occupy distinct slots in members(Rl ). At most fl are Byzantine, so at least ql − fl = nl − 2fl ≥ fl + 1 were produced by correct broadcasters and are marked by lemma 13. The process therefore invokes InstallTransition in round t+1. A process that invokes in a later round necessarily advances through round t + 1 first, so no correct install transition round lies outside {t, t + 1}. ◀ ▶ Lemma 15 (If a correct Rl -member’s round-r enabled-configs value contains Rl , every valid round-r certificate is declared under Rl or Rl+1 ). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and assume the conclusions already established for preceding transitions. Let δl+1 = earliest(Rl+1 ). Let r ≥ δl+1 , suppose BRB Agreement holds through round r − 1, and suppose there exists a correct process pi ∈ members(Rl ) such that enabled-configs i [r] ̸= ⊥

and

Rl ∈ enabled-configs i [r].

Then every valid BRB quorum certificate for a complete BRB value ⟨m, r, µ⟩ satisfies local(µ) ∈ {Rl , Rl+1 }. Proof. There is no configuration earlier than Rl to exclude when l = 1. Suppose l > 1. By lemma 7, every active correct Rl -member has completed the transition into Rl before acting in round δl+1 − 1, and therefore does not enable an earlier configuration in round r.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

For the case of a correct process removed by the immediately preceding transition, let t′ be that transition’s earliest correct install transition round and let ah be the removed process’s install transition round. Corollary 29, applied to that preceding transition, gives ah ≤ t′ + 1, while the bound established in the proof of lemma 7 gives t′ + 5 ≤ δl+1 − 1. Hence ah + 4 ≤ t′ + 5 ≤ δl+1 − 1 < r. If the removed process has already stopped, it contributes no share. If it is still processing BRB messages, its removal procedure nevertheless assigns no enabled-configs value after round ah + 4, so it cannot echo or vote in round r. The conclusions for still earlier transitions exclude their removed correct processes in the same way. Thus, under every configuration Rc with c < l, only its at most fc < qc Byzantine members can contribute round-r vote shares, which are insufficient to form a quorum certificate. Suppose Rl+2 exists. By lemma 11, let t be the earliest install transition round for Rl → Rl+1 . By lemma 12, earliest(Rl+2 ) ≥ t + 6. If r ≤ t + 1, then directly r < earliest(Rl+2 ). If r ≥ t + 2, Agreement through r − 1 includes Agreement through t. Let pi be the process in the premise. If pi invokes InstallTransition, then lemmas 13 and 14 place its install transition round in {t, t + 1}. Since InstallTransition with install transition round ai assigns the pair exactly in rounds ai + 1, . . . , ai + 4, its round-r value containing Rl implies r ≤ t + 5. Otherwise, assigning a value for a round r ≥ t + 2 requires pi to advance through round t + 1; the same lemmas would then force it to install by that round, a contradiction. Hence r ≤ t + 5 < earliest(Rl+2 ). In either case, r < earliest(Rl+2 ). By lemmas 10 and 12, the earliest-inclusion rounds strictly increase along the issued configuration sequence. Thus r < earliest(Rc ) for every issued Rc with c ≥ l + 2. Correct processes reject a configuration before its authenticated earliestinclusion round, so none of these configurations can obtain enough correct votes for a round-r certificate. If Rl+2 does not exist, authentication excludes a later configuration directly. Thus every valid round-r certificate is declared under either Rl or Rl+1 . ◀ ▶ Lemma 16 (Agreement through round r preserves round-(r + 1) enabled-configs alignment while a correct old member still enables Rl ). Fix a valid issued transition Rl → Rl+1 under the configuration-level induction hypothesis for Rl , let r ≥ δl+1 = earliest(Rl+1 ), and suppose BRB Agreement holds through round r. If a correct process pi ∈ members(Rl ) has an assigned round-(r + 1) enabled-configs value containing Rl , then all round-(r + 1) enabled-configs values assigned by correct processes in members(Rl ) are aligned. Proof. We first show that no round-(r + 1) value assigned by a correct Rl -member involves a configuration other than Rl and Rl+1 . By lemma 7, every correct Rl -member completes the transition into Rl before acting in round δl+1 − 1, so values involving Rl−1 are assigned only for rounds below δl+1 ≤ r; the conclusions for preceding transitions exclude earlier configurations. If a value involving Rl+2 or a later configuration is ever assigned, then Rl+2 is issued, so by lemma 11 the earliest install transition round t for Rl → Rl+1 exists, and by lemmas 10 and 12 such a value is assigned only for rounds at least earliest(Rl+2 ) + 1 ≥ t + 7. If t > r, then r + 1 ≤ t < t + 7; if t ≤ r, the last paragraph below shows r + 1 ≤ t + 5 < t + 7. In every case, every assigned round-(r + 1) value is {Rl }, {Rl , Rl+1 }, or {Rl+1 }. It remains to exclude the coexistence of {Rl } and {Rl+1 }. If no correct process has invoked InstallTransition by round r, no pair or new singleton has been assigned for round r + 1, and alignment is immediate. If the earliest install transition round is t = r,

XX:39

XX:40

Seamless Reconfiguration for DAG BFT

a correct process has either not yet invoked InstallTransition and assigns {Rl }, or has invoked it and assigns {Rl , Rl+1 } to round r + 1; only the old singleton and the pair coexist, and r + 1 = t + 1 ≤ t + 5. Suppose t ≤ r − 1. Agreement through round r includes Agreement through t. By lemmas 13 and 14, every correct old member that advances through round t + 1 invokes InstallTransition with install transition round t or t + 1. The process in the premise has assigned a value for round r+1 ≥ t+2; hence it has either already invoked InstallTransition or advanced through round t + 1 and was forced to invoke it. Since its round-(r + 1) value still contains Rl , and an invocation with install transition round ai assigns {Rl , Rl+1 } only to rounds ai + 1, . . . , ai + 4, we have r + 1 ≤ t + 5. Any correct process with an assigned round-(r + 1) value that has advanced through round t + 1 likewise has install transition round t or t + 1, so its value is {Rl , Rl+1 } or {Rl+1 }; one that has not advanced through round t + 1 either installed in round t and assigned the pair through round t + 4, or has assigned no value beyond round t + 1 < r + 1. Hence the old and new singleton values cannot coexist. The assigned values are aligned in every case. ◀ ▶ Lemma 17 (Enabled-configs values remain aligned and BRB Agreement holds while a correct Rl -member still enables Rl ). Fix a valid issued transition Rl → Rl+1 under the configurationlevel induction hypothesis for Rl , and let δl+1 = earliest(Rl+1 ). For every logical round r ≥ δl+1 such that some correct pi ∈ members(Rl ) has an assigned round-r enabled-configs value containing Rl : 1. the assigned round-r enabled-configs values of correct processes in members(Rl ) are aligned for Rl → Rl+1 ; and 2. BRB Agreement holds for every round-broadcaster slot (r, ID). Proof. First observe that, if the lemma’s premise holds in round r, it also holds in every round from δl+1 through r. It is enough to prove this for the immediately preceding round. Let a correct Rl -member have an assigned round-r enabled-configs value containing Rl , where r > δl+1 . If the process assigned this value while advancing from round r − 1 to round r, it had already assigned its round-(r − 1) value. For one transition, a correct process’s assigned values change only from the old singleton to the pair and then to the new singleton. Because the round-r value still contains Rl , the round-(r − 1) value also contains Rl . If InstallTransition assigned the round-r value in advance, then r is one of the next four rounds assigned the pair {Rl , Rl+1 }. Its immediately preceding value was either assigned the same pair by that invocation or was assigned before the invocation and still contained Rl . Repeating this argument reaches δl+1 . Suppose the lemma is false, and let r be the least round satisfying its premise in which either conclusion fails. By the Agreement clause of the configuration-level induction hypothesis for Rl , BRB Agreement holds through round δl+1 − 1. If r = δl+1 , alignment follows from lemma 8. If r > δl+1 , the property just proved and the minimality of r give BRB Agreement through round r − 1. Applying lemma 16 to round r − 1 therefore gives alignment in round r. In either case, BRB Agreement holds through round r − 1. Hence lemma 15 restricts every valid round-r certificate to Rl or Rl+1 , and lemma 5 gives BRB Agreement in round r. Both conclusions hold, contradicting the choice of r. ◀ ▶ Lemma 18 (No correct Rl -member’s enabled-configs value contains Rl at or after earliest(Rl+2 )). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose Rl+2 exists. For every correct process pi ∈ members(Rl ) and every logical round s, enabled-configs i [s] ̸= ⊥ ∧ Rl ∈ enabled-configs i [s]

=⇒

s < earliest(Rl+2 ).

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Proof. By lemma 11, an earliest install transition round t exists, and lemma 12 gives earliest(Rl+2 ) ≥ t + 6. By lemmas 13, 14, and 17, every correct process in members(Rl ) that advances from round t + 1 to round t + 2 invokes InstallTransition in round t or t + 1. For such a process, every assigned enabled-configs value containing Rl has round index at most t+5. A process that does not advance through round t+1 either invoked InstallTransition in round t, in which case that invocation assigned values equal to {Rl , Rl+1 } only through round t+4, or did not invoke it, in which case round advancement assigned no enabled-configs value beyond round t + 1. Hence every such s satisfies s ≤ t + 5 < earliest(Rl+2 ). ◀ ▶ Lemma 19 (BRB Agreement holds before earliest(Rl+1 ) and in every later round where a correct Rl -member’s enabled-configs value contains Rl ). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and let δl+1 = earliest(Rl+1 ). BRB Agreement holds for every roundbroadcaster slot whose round index s satisfies either s < δl+1 , or s ≥ δl+1

and

pi is correct,

∃ pi ∈ members(Rl ) : enabled-configs i [s] ̸= ⊥,

Rl ∈ enabled-configs i [s].

Proof. For every s < δl+1 , BRB Agreement is exactly the Agreement clause of the configurationlevel induction hypothesis for Rl . For every s ≥ δl+1 satisfying the second condition in the statement, lemma 17 gives BRB Agreement in every round-broadcaster slot of round s. ◀

B.1.3

DAG Progress and Round Advancement under BRB Agreement

Having established BRB Agreement for the rounds considered above, we next separate certification from advancement. First, if the correct processes needed by a round-r BRB instance continue those tasks until certificates form, the resulting certified blocks and their ancestors reach every correct recipient that remains active while waiting. Second, during a transition, a correct process in round r0 + 2 or r0 + 3 can also advance after receiving ql+1 admissible blocks from the following round. The transition-progress proofs below show that one of these two ways of completing each affected AdvanceRound iteration occurs before any correct process on which that progress depends stops its BRB and DAG tasks. ▶ Lemma 20 (A correct process’s local DAG is ancestor-closed). At every correct process pi , if B ∈ DAGi [r], then every parent and ancestor named by B is also in DAGi . Proof. Initially the DAG is empty. When the certified block B is received outside statetransfer, FetchAndDeliveri (B) invokes AddAndDeliveri (B) only after every named parent has been inserted; its recursive parent tasks apply the same rule. When a joining process pi receives a state-reply payload D for Rl+1 , ValidStatei (D, Rl+1 ) accepts only an ancestorclosed set containing at most one block in each round-broadcaster slot, and MergeStatei (D) invokes AddAndDeliveri (B) for accepted blocks B in increasing round order. These are the only insertion cases, so induction over insertions proves the claim. ◀ ▶ Lemma 21 (A certified block declared under Rc with qc parents has an admissible parent quorum). Let pi be correct and let X = ⟨m, s + 1, µ, C⟩ ∈ DAGi [s + 1] be admissible. Put Rc = local(µ) and suppose |parents(µ)| = qc . Then |{B ∈ DAGi [s] : ref(B) ∈ parents(µ)}| = qc ,

XX:41

XX:42

Seamless Reconfiguration for DAG BFT

and every block in this set belongs to ParentBlocksi (Rc , s). Proof. The displayed premise gives exactly qc parent references, and CertifiedParentCount(s + 1, µ) ensures that their broadcaster identities are distinct. Local DAG ancestor closure puts the matching blocks in DAGi [s], and ValidParentSeti (X, DAGi ) applies exactly the broadcaster and configuration-number checks in ParentBlocksi (Rc , s). ◀ ▶ Lemma 22 (Transferred state is validated independently of its sender). Let pi be correct and let D be a state-reply payload for which ValidStatei (D, Rl+1 ) holds. Every block B = ⟨m, s, µ, C⟩ that MergeStatei (D) inserts carries a valid BRB certificate for its complete payload, satisfies CertifiedParentCount(s, µ) and the referenced-parent checks, and is inserted together with all of its ancestors. Moreover, D contains at most one block in every round-broadcaster slot. These conclusions do not depend on whether the process that sent D is correct. Proof. All stated properties are checked from D and the certificates bound to its blocks. The predicate ValidStatei (D, Rl+1 ) checks that D is ancestor-closed and contains at most one block in every round-broadcaster slot. For each block B = ⟨m, s, µ, C⟩, it also checks ValidCertifiedMetadatai (B), including CertifiedParentCount(s, µ), and every parent’s hash and identity. It rejects a block if its metadata names a configuration numbered later than l + 1. The reply-construction rule applies the same bound. MergeStatei (D) processes accepted blocks in increasing round order, so every named parent is inserted before its child. The sender’s identity is not an input to any of these checks. ◀ ▶ Lemma 23 (The known-identity set contains the members of every processed configuration). If Rh is the highest-numbered authenticated reconfiguration message processed by UpdateKnowni (Rh ) at a correct process pi , then known i =

h [

members(Rc ),

c=1

and this set never shrinks. In particular, upon receiving a valid Rl+1 , every correct recipient in members(Rl ) ∪ members(Rl+1 ) knows every identity in that union before the retained-process handler executes its wait for local i = Rl and ri ≥ earliest(Rl+1 ), or the joining process begins state transfer. Proof. Each authenticated Rh carries the identities that appeared in R1 , . . . , Rh−1 . The UpdateKnowni (Rh ) procedure authenticates that carried set and unions it and members(Rh ) into known i . Processing Rh through UpdateKnowni (Rh ) therefore gives the displayed equality, and subsequent invocations only enlarge the set. Both handlers invoke the procedure before those actions. ◀ ▶ Lemma 24 (Conditional DAG delivery of certified causal history to a correct process). Let ph and pj be correct, and let D be a finite ancestor-closed subset of DAGh . Because every block has finitely many parents, all in the preceding round, the causal history of a finite set of blocks is finite; by lemma 20, the causal history of blocks stored by ph is contained in DAGh . Suppose that pj ∈ known h while ph still performs its prescribed communication and DAG tasks. Then ph sends every block in D to pj ; if ph is removed, it does so before stopping its remaining tasks. Suppose additionally that pj is active or eventually becomes active and, while any block in D is missing, continues processing certified-block messages and running FetchAndDeliver; that every B ∈ D satisfies ValidCertifiedMetadataj (B) and the referenced-parent checks once

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

its parents are present; and that no different block already in DAGj occupies the same round-broadcaster slot as a block in D. Then pj eventually DAG-delivers every block in D. For a correct removed process pj , the second conclusion applies only before it leaves. An application to such a process must show that the condition for leaving keeps these receive and FetchAndDeliver actions active until the blocks used to satisfy that condition and their ancestors have been DAG-delivered. No delivery is claimed after pj leaves. Proof. Fix X ∈ D. If pj is already in known h when X is inserted, AddAndDeliverh (X) sends the complete certified block to pj . Otherwise, let Rc be the authenticated reconfiguration message processed by the first UpdateKnownh (Rc ) invocation that adds pj to known h . That invocation executes a finite FloodDAGh over the blocks then stored at ph , and therefore sends X if X was inserted before that invocation. The invocation and the insertion of X are ordered local events: if the insertion occurs first, FloodDAGh sends X; if it occurs second, AddAndDeliverh (X) sends X. Repeated invocations of FloodDAGh provide additional copies while ph remains active, and, if ph is removed, its final invocation sends every block then stored before it stops. Thus every block in D is sent to pj before a removed ph stops its remaining tasks. Reliable delivery is unaffected by the sender’s later departure. A copy sent before pj activates remains queued and is processed after pj activates. Assume now the additional premises for delivery at pj . We prove the following statement by induction on s ≥ 1: every block in D whose round is at most s is eventually inserted into DAGj . For s = 1, let X ∈ D be a round-1 block. It has no parents. Upon receipt, pj either already has a live FetchAndDeliverj (X) task or schedules one. For the fixed block X, membership in scheduled j cannot refer only to a task that returned after a failed check: ValidCertifiedMetadataj (X) is deterministic and true by assumption; a task with a missing parent waits instead of returning; and, once all parents are present, the assumed referenced-parent and slot conditions permit insertion unless X is already present. The assumed checks imply Admissiblej (X), so the procedure invokes AddAndDeliverj (X), which inserts and DAG-delivers the block unless it is already present. For the induction step, let X ∈ D be a round-s block with s > 1, and assume the statement through round s − 1. Because D is ancestor-closed, every parent referenced by X belongs to D and lies in round s − 1. The induction hypothesis therefore inserts all of these parents into DAGj . Once the last missing parent is inserted, each parent condition tested by FetchAndDeliverj (X) is true. Because pj continues that task, the procedure resumes, verifies the now-present parents, and obtains Admissiblej (X). The round-broadcaster-slot premise then permits AddAndDeliverj (X) to insert and DAG-deliver X, unless it was already present. This proves the induction statement. Since D is finite, it has a greatest round, so the statement for that round covers every block in D. Blocks may arrive in any order because each FetchAndDeliverj (X) task waits until the parents of X are present. ◀ ▶ Lemma 25 (A correct broadcaster’s round-r block is certified and delivered while the required processes remain active). Fix a configuration Rl and a logical round r for which BRB Agreement holds for every round-broadcaster slot in rounds at most r. Let G ⊆ members(Rl ) contain at least ql active correct processes. Suppose every pi ∈ G enters round r, invokes its prescribed round-r DAG-Append operation with frozen value ⟨mi , r, µi ⟩, and reaches that invocation’s call to BRB-Broadcast. At that call, suppose it satisfies local(µi ) = Rl

and

Rl ∈ enabled-configs i [r],

and suppose MaySendBRBi (Rl , r) holds, so the call passes its guard. Fix pk ∈ G, and let ⟨mk , r, µk ⟩ be the complete BRB value proposed by its DAG-Append invocation. If, while no

XX:43

XX:44

Seamless Reconfiguration for DAG BFT

correct process in G has formed a certificate for this value, every process in G remains active and continues its prescribed BRB tasks, then a valid certificate Ck declared under Rl is eventually formed. Moreover, the resulting block Bk = ⟨mk , r, µk , Ck ⟩ is eventually DAG-delivered by every correct process pj ∈ members(Rl ) such that, while Bk is missing, pj remains active and continues processing certified-block messages and running FetchAndDeliver. Proof. Let the fixed correct broadcaster propose ⟨mk , r, µk ⟩. Its declared configuration is the frozen Rl , even if the broadcaster installs another configuration before this delayed call. Since G ⊆ members(Rl ) ⊆ Recipients(enabled(µk )), every process in G receives the proposal, echo, and vote messages for this BRB instance. Every pi ∈ G passes the stated MaySendBRBi (Rl , r) guard and continues the prescribed BRB handlers. The required echoes and votes are therefore sent to every process in Recipients(enabled(µk )). Eventual message delivery causes a correct process ph ∈ G to receive ql valid votes and form Ck . The Agreement premise makes this the unique BRB value for the slot. In the vote-message receive handler, ph constructs Bk and sends ⟨certified-block, Bk ⟩ to every identity in known h before triggering BRB-Deliverh (mk , r, µk , Ck ). Since ph has processed Rl , lemma 23 gives members(Rl ) ⊆ known h . Thus the complete certified block is sent to every Rl -member before ph can leave, and its later departure does not prevent delivery. Before invoking BRB-Broadcast, pk stored every block named by parents(µk ) and, by lemma 20, every ancestor of those blocks. For each correct Rl -member that remains active while any of these blocks is missing, lemma 24 delivers this finite ancestor-closed set from pk ; if pk is removed, its final FloodDAG sends the set before it stops. The Agreement premise excludes a different block in any relevant round-broadcaster slot. Consequently, if a correct Rl -member px receives Bk , it obtains all of its named parents, satisfies Admissiblex (Bk ), and DAG-delivers Bk . Therefore, the certified-block message sent by ph when it forms Ck makes every correct Rl -member that remains active while Bk is missing DAG-deliver Bk . ◀ ▶ Lemma 26 (Delivery of ql+1 admissible round-(r + 1) blocks advances a transitioning process from round r). Let pj be correct with transition j = ⟨Rl , Rl+1 , r0 ⟩, and let r ∈ {r0 + 2, r0 + 3}. Suppose BRB Agreement holds through round r + 1. Let ph be correct and suppose that DAGh [r + 1] contains a set Q ⊆ ParentBlocksh (Rl+1 , r + 1) of at least ql+1 blocks in distinct round-broadcaster slots. Suppose pj ∈ known h while ph still performs its prescribed communication and DAG tasks. If, while its round-r AdvanceRound iteration is pending, pj remains active and continues processing certified-block messages and running FetchAndDeliver, then pj eventually advances to round r + 1. Proof. Let D contain Q and all of their ancestors. It is a finite ancestor-closed subset of DAGh . The blocks have valid certified metadata and referenced parents, and Agreement through round r + 1 excludes a different block in any of their slots. Thus lemma 24 makes pj DAG-deliver D while the iteration remains pending. Because every block in Q is then present in DAGj [r + 1], and the remaining conditions in ParentBlocksj (Rl+1 , r + 1) depend only on the certified metadata, Q ⊆ ParentBlocksj (Rl+1 , r + 1). Hence |ParentBlocksj (Rl+1 , r + 1)| ≥ ql+1 ,

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

which is the permitted additional transition-round condition in round r. The iteration therefore terminates and increments rj . ◀ ▶ Lemma 27 (Continued activity delivers a round-r parent quorum to every correct Rl -member). Fix a configuration Rl and a logical round r for which BRB Agreement holds for every round-broadcaster slot in rounds at most r. Let G ⊆ members(Rl ) contain at least ql correct processes. Suppose every pk ∈ G enters round r, invokes its prescribed round-r DAG-Append operation, and reaches that invocation’s call to BRB-Broadcast with proposed metadata µk satisfying local(µk ) = Rl , Rl ∈ enabled-configs k [r], and MaySendBRBk (Rl , r), so the call passes its guard. Suppose moreover that, while a certificate for any of these selected round-r values is missing, every process in G remains active and continues its prescribed BRB tasks. Let pj ∈ members(Rl ) be correct. If, while fewer than ql of the resulting blocks are present in DAGj [r], pj remains active and continues its prescribed BRB receive task, processing certified-block messages, and running FetchAndDeliver, then pj eventually DAG-delivers at least ql admissible round-r blocks in distinct round-broadcaster slots. Hence |ParentBlocksj (Rl , r)| ≥ ql . Proof. Choose any ql processes in G. For each chosen process, the certification premises of lemma 25 hold: the selected processes are correct eligible Rl -members, their prescribed appends reach BRB-Broadcast, and they continue the BRB tasks until every selected certificate is formed. The condition above that pj remains active and continues its receive and fetch tasks is exactly the corresponding condition in lemma 25. Apply that lemma once to each selected broadcaster. Process pj eventually DAG-delivers all ql blocks. They occupy distinct round-broadcaster slots, and their metadata make them members of ParentBlocksj (Rl , r), proving the displayed condition. ◀ ▶ Corollary 28 (An ordinary parent quorum advances a correct process when the additional transition-round condition is unavailable). Fix Rl , r, and a set G ⊆ members(Rl ) of at least ql correct processes. Suppose BRB Agreement holds through round r and every process in G reaches and passes the BRB-Broadcast call of its prescribed Rl -declared round-r append, with MaySendBRBk (Rl , r) holding for every pk ∈ G. Let pj ∈ members(Rl ) be correct and executing a round-r AdvanceRound iteration whose ordinary condition is |ParentBlocksj (Rl , r)| ≥ ql and suppose that, throughout these round-r iterations, every px ∈ G ∪ {pj } satisfies ∄Ra , Rb , rx :

transition x = ⟨Ra , Rb , rx ⟩ ∧ r ∈ {rx + 2, rx + 3}.

Then pj eventually advances to round r + 1. Proof. Suppose, for contradiction, that pj never advances. The additional condition is unavailable, so its ordinary condition remains false. The process therefore cannot reach a later departure point and remains active, processing certified blocks and running FetchAndDeliver. If some ph ∈ G advances from round r, the additional condition is unavailable there as well, so ph stores ql blocks counted by ParentBlocksh (Rl , r). Let D contain those blocks and their ancestors. The set is finite and ancestor-closed. Both processes have authenticated Rl , hence pj ∈ known h ; Agreement through round r excludes a conflicting block in any selected slot. The sends made upon insertion, subsequent FloodDAG invocations, and the final invocation if ph is later removed satisfy the sending premise of lemma 24. That lemma makes pj DAG-deliver the selected quorum, a contradiction.

XX:45

XX:46

Seamless Reconfiguration for DAG BFT

Otherwise no process in G advances from round r. None can reach a later departure point, so all remain active and continue their BRB tasks while their selected certificates are missing. The condition in lemma 27 that these processes continue the required tasks therefore holds, and that lemma makes pj DAG-deliver ql admissible round-r blocks, again a contradiction. ◀

B.1.4

Install-Transition-Round Bounds and BRB Agreement for a Correct Joining Process

▶ Corollary 29 (If t is the minimum install transition round among correct old members, every correct old member has install transition round t or t + 1). Fix a valid issued transition Rl → Rl+1 and assume the configuration-level induction hypothesis for Rl defined above. If t is the earliest install transition round among correct processes in members(Rl ), then every such process eventually invokes InstallTransition in round t or t + 1. Proof. By the configuration-level induction hypothesis for Rl , there is a round s0 that every active correct Rl -member eventually enters and in which at least ql active correct members invoke the prescribed append and reach its BRB-Broadcast call. If s0 > t + 1, sequential round execution means that every correct old member has already advanced through round t + 1 before entering s0 . If s0 ≤ t + 1, induct from s0 through t + 1. In each such round, at least ql active correct old members invoke the prescribed append and reach its broadcast call. Indeed, the first transition is installed only while round t is completed, and its additional advancement condition is unavailable through round t + 1; ordinary entry into the next round supplies the same predecessor quorum on which the next append waits. For rounds below δl+1 , BRB Agreement is supplied by the Agreement clause of the induction hypothesis; at and above δl+1 , it is supplied by lemma 17. Therefore corollary 28 makes every correct old member enter the next round. Thus every correct old member reaches round t+2 after collecting the required round-(t+1) quorum. By lemma 14, its install transition round belongs to {t, t + 1}. ◀ For the next results, suppose the transition from Rl to Rl+1 adds a correct process pj . Let u be the round returned by DiscoverBeginj (Rl , Rl+1 ), and let t be the earliest install transition round among correct processes in members(Rl ). ▶ Lemma 30 (The minimum install transition round among correct old members is at most u+1). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose it adds a correct process pj . Let u be the round returned by DiscoverBeginj (Rl , Rl+1 ), and assume that t is the earliest round in which a correct process in members(Rl ) invokes InstallTransition for this transition. Then t ≤ u + 1. Proof. Let M be any fl +1 marked round-u blocks present in DAGj [u] when DiscoverBegin returns. Suppose t > u + 1. A round-(u + 1) block X produced by a correct process in members(Rl ) is then a block from the prescribed Rl -declared DAG-Append operation with ql round-u parents. By lemma 9, their slots and M lie in the same nl -member configuration, so |HX (u) ∩ M| ≥ ql + (fl + 1) − nl = 1. BRB Agreement in round u, from lemma 19, identifies the intersecting slot with the same marked block. Every such X is therefore marked.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

XX:47

Let s0 be the logical round whose existence is required by clause (iv) of the configurationlevel induction hypothesis for Rl . If s0 > u + 1, every correct old member advances through round u + 1 before entering s0 . If s0 ≤ u + 1, the supposition t > u + 1 lets us induct from s0 through u + 1: in every such round at least ql correct old members invoke their prescribed DAG-Append operation and reach its broadcast call, BRB Agreement holds by lemma 19, and corollary 28 advances every correct old member. Any such process obtains ql round-(u + 1) blocks, at least ql − fl ≥ fl + 1 of which have correct broadcasters and are marked. It invokes InstallTransition, contradicting t > u + 1. ◀ ▶ Lemma 31 (The minimum install transition round among correct old members is at least u−1). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose it adds a correct process pj . Let u be the round returned by DiscoverBeginj (Rl , Rl+1 ), and assume that t is the earliest round in which a correct process in members(Rl ) invokes InstallTransition for this transition. Then t ≥ u − 1. Proof. Suppose t ≤ u − 2. Agreement through round t + 1 follows from the Agreement clause of the configuration-level induction hypothesis for Rl and lemma 17. By lemma 10, t ≥ earliest(Rl+1 ). A correct old member that installs in round t has Rl in its assigned enabled-configs values for rounds t + 1 and t + 2, so the premises of lemma 15 hold in both rounds. By lemma 13, every round-(t+1) block produced by a correct process in members(Rl ) is marked. When DiscoverBegin returns, round u satisfies its two local DAG conditions. Since u ≥ t + 2, choose any block counted in LocalBlocksj (Rl , u) and repeatedly follow a parent in the immediately preceding round until reaching a block Z ∈ DAGj [t + 2]. Such a parent exists at every step because every imported round-s′ block with metadata µ′ passes CertifiedParentCount(s′ , µ′ ), and lemma 20 places every chosen parent in the joining process’s DAG. The joining process has produced no block before discovery returns. By lemma 15, Z declares Rl or Rl+1 and has at least ql distinct round-(t + 1) parents. Let B = ⟨mB , t + 1, µB , CB ⟩ be one of these parents. If local(µB ) = Rl , then ValidCertifiedMetadataj (B) gives ID(µB ) ∈ members(Rl ). Otherwise, lemma 15 in round t + 1 gives local(µB ) = Rl+1 , and ValidCertifiedMetadataj (B) gives ID(µB ) ∈ members(Rl+1 ). This identity also belongs to members(Rl ) because the sole added process has not yet produced a block. At least ql − fl ≥ fl + 1 of these parent broadcasters are correct, and their blocks are marked by lemma 13. Ancestor closure places all these parents in DAGj [t + 1]. Thus round t + 1 already satisfies both conditions checked by DiscoverBegin. The minimality of u gives u ≤ t + 1, contradicting t ≤ u − 2. ◀ ▶ Lemma 32 (The install transition round of the joining process differs by at most one from the minimum install transition round among correct old members). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose it adds a correct process pj . Let u be the round returned by DiscoverBeginj (Rl , Rl+1 ), and assume that t is the earliest round in which a correct process in members(Rl ) invokes InstallTransition for this transition. Then t ∈ {u − 1, u, u + 1}. Proof. The claim follows from lemmas 30 and 31.

◀

XX:48

Seamless Reconfiguration for DAG BFT

▶ Lemma 33 (Every correct old member’s install transition round differs by at most one from the install transition round of the joining process). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose it adds a correct process pj . Let u be the round returned by DiscoverBeginj (Rl , Rl+1 ), and let t be the earliest install transition round among correct processes in members(Rl ). Then every correct pi ∈ members(Rl ) eventually invokes InstallTransition for this transition. Let ai denote the round of that invocation. Then t = u − 1 =⇒ ai ∈ {u − 1, u}, t = u =⇒ ai ∈ {u, u + 1}, t = u + 1 =⇒ ai = u + 1. Proof. The first two cases follow from corollary 29. Suppose t = u + 1. Every correct round-(u + 1) block has ql round-u parents. Their slots intersect the fl + 1 marked round-u slots used by DiscoverBegin, and round-u BRB Agreement identifies an intersecting slot with the same marked block. Hence every such round-(u + 1) block is marked. Every correct old member eventually reaches that round. Among the ql blocks it obtains before advancing, at least ql − fl ≥ fl + 1 have correct broadcasters and are therefore marked. It consequently installs while processing round u + 1, so ai = u + 1. ◀ ▶ Lemma 34 (Every correct old member has enabled-configs value {Rl , Rl+1 } in rounds u + 2 and u + 3). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose it adds a correct process pj . Let u be the round returned by DiscoverBeginj (Rl , Rl+1 ), and let t be the earliest install transition round among correct processes in members(Rl ). Then every correct pi ∈ members(Rl ) satisfies enabled-configs i [u + 2] = enabled-configs i [u + 3] = {Rl , Rl+1 }. The joining protocol prescribes DAG-Transition-Appendj in precisely these two rounds. Proof. By lemmas 32 and 33, a correct process’s install transition round ai belongs to {u − 1, u, u + 1}. The four rounds assigned the pair are: ai u−1 u u+1

rounds s with enabled-configs i [s] = {Rl , Rl+1 } u, u + 1, u + 2, u + 3 u + 1, u + 2, u + 3, u + 4 u + 2, u + 3, u + 4, u + 5

In every case, the value in rounds u + 2 and u + 3 is {Rl , Rl+1 }.

◀

▶ Lemma 35 (If the joining process enables both configurations after correct old members stop voting under Rl , BRB Agreement holds in that round). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose it adds a correct process pj . Let u be the round returned by DiscoverBeginj (Rl , Rl+1 ); the joining protocol uses u as pj ’s install transition round. Let s be a logical round such that enabled-configs j [s] = {Rl , Rl+1 }, and suppose every correct pi ∈ members(Rl ) satisfies one of the following conditions: either it never assigns enabled-configs i [s] and therefore never sends a round-s BRB echo or vote, or its assigned value satisfies Rl ∈ / enabled-configs i [s].

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Then the configuration-scoped BRB algorithm satisfies Agreement for every round-broadcaster slot (s, ID). Proof. By lemmas 32 and 33, this case can occur only when the earliest install transition round is t = u − 1, every correct process in members(Rl ) installs in round u − 1, and s = u + 4 = t + 5. If Rl+2 exists, then lemma 12 gives s = t + 5 < t + 6 ≤ earliest(Rl+2 ). By lemmas 10 and 12, earliest-inclusion rounds increase strictly along the issued sequence. Also, s = t + 5 ≥ earliest(Rl+1 ). For any c < l, a correct round-s voter under Rc would be a member of members(Rc ) whose round-s enabled-configs value contains Rc . Applying lemma 18 to that preceding transition would give s < earliest(Rc+2 ) ≤ earliest(Rl+1 ), a contradiction. If Rl+2 exists, then s < earliest(Rl+2 ) ≤ earliest(Rc ) for every c ≥ l + 2. A correct member of Rc enables Rc only in rounds greater than its install transition round for Rc−1 → Rc . By lemma 10, that install transition round is at least earliest(Rc ). Hence no such member can vote under Rc in round s. If Rl+2 does not exist, authentication excludes every later configuration directly. Since Byzantine members alone cannot form a certificate, every round-s certificate is declared under Rl or Rl+1 . By the first alternative in the lemma statement, a correct old member that never assigns its round-s value sends no round-s BRB echo or vote. By the second alternative, a correct old member that does assign the value excludes Rl and is therefore ineligible to echo or vote for an instance declared under Rl . The joining process is not a member of Rl and cannot vote in an instance declared under Rl . At most the fl Byzantine members can vote in such an instance, fewer than the ql shares required for a certificate. Consequently, every round-s certificate is declared under Rl+1 . The quorum-intersection argument for two certificates declared under Rl+1 gives Agreement. ◀

B.1.5

Parent-Quorum Progress During Reconfiguration

The next six results prove conditional progress: they assume that some correct old member has installed the transition and, when the added process is correct, that its state-transfer discovery has returned. These assumptions are discharged later by lemmas 45 and 46; thus the conditional arguments are not used to prove their own premises. ▶ Lemma 36 (The additional transition-round condition advances a correct process to its transition-completion round). Suppose a correct process pi has transition i = ⟨Rl , Rl+1 , ai ⟩. If, while ri = ai + 2, |ParentBlocksi (Rl+1 , ai + 3)| ≥ ql+1 , then pi eventually reaches the beginning of round ai +4 and invokes FinishTransitioni (Rl+1 ). The same conclusion holds if, while ri = ai + 3, |ParentBlocksi (Rl+1 , ai + 4)| ≥ ql+1 . Proof. In the first case, the additional disjunct of AdvanceRound is true with the frozen value r = ai + 2, so the procedure assigns ri ← ai + 3. Its next serialized iteration selects

XX:49

XX:50

Seamless Reconfiguration for DAG BFT

Rl+1 for the ordinary final-transition-round condition. The same round-(ai + 3) blocks satisfy that condition, so it assigns ri ← ai + 4. In the second case, the additional disjunct is true with r = ai + 3 and directly causes the assignment ri ← ai + 4. In either case the beginning-of-round rule then invokes FinishTransitioni (Rl+1 ). Each iteration writes only r + 1, and the serialized AdvanceRound loop is the only post-activation writer of ri . ◀ ▶ Lemma 37 (Before stopping, a correct process stores blocks sufficient for another correct process’s transition-round advancement). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl . Assume that the earliest correct old-member install transition round t exists. If the transition adds a correct process, assume that its DiscoverBegin call returns a round u. Let pi , ph be correct retained, joining, or removed processes with install transition rounds ai , ah . Let r ∈ {ai + 1, ai + 2, ai + 3}. If ph stops all protocol tasks, then, immediately before its final FloodDAG, DAGh has the following state: 1. if r = ai + 1, it contains the blocks required by pi ’s ordinary round-r condition; and 2. if r ∈ {ai + 2, ai + 3}, it contains either the blocks required by pi ’s ordinary round-r condition or at least ql+1 blocks in ParentBlocksh (Rl+1 , r + 1). These conclusions do not depend on whether pi begins its round-r iteration before or after ph sends that final flood. Proof. By corollary 29, every correct old member has install transition round in {t, t + 1}. If the transition does not add a correct process, these are all correct retained or removed processes. Otherwise, let u be the correct joining process’s install transition round. By lemmas 32 and 33, if t = u − 1, all correct retained, joining, or removed processes install in {u − 1, u}; if t = u, they install in {u, u + 1}; and if t = u + 1, they install in {u, u + 1}. Thus the install transition rounds of every two correct retained, joining, or removed processes differ by at most one. Consequently, if ah = ai − 1, every such correct process installs in {ai − 1, ai }; if ah = ai + 1, every such correct process installs in {ai , ai + 1}. The DAG never removes a block, so it is enough to inspect how ph crosses the relevant logical rounds before it can stop. If ah = ai , the two processes have the same applicable conditions in round r. In round ai + 1 the additional condition is unavailable, so crossing the round stores the blocks required by the ordinary condition. In either of the next two rounds, crossing it stores those blocks or at least ql+1 blocks in ParentBlocksh (Rl+1 , r + 1). If r = ai + 1, the ordinary condition at pi uses ql . For ah ∈ {ai , ai + 1}, process ph cannot cross logical round r without storing the blocks required by that ordinary round-r condition. If ah = ai − 1, the round is ph ’s penultimate transition round. It either stores the ql blocks required by that ordinary condition or advances using ql+1 blocks in round r + 1. That latter set contains a correct old-member block. For an addition, nl+1 ≥ 5 and ql+1 > fl+1 + 1, so excluding at most fl+1 Byzantine slots and the single joining-process slot leaves such a block. A removal leaves nl+1 ≥ 4, hence fl+1 ≥ 1; together with fl ≤ fl+1 + 1 and ql+1 ≥ 2fl+1 + 1, this gives ql+1 > fl . With unchanged membership, ql+1 = ql > fl . The correct old-member block is declared under Rl : if ax is its broadcaster’s install transition round, the bound above gives ax ∈ {ai − 1, ai }, and the block is produced in round r + 1 = ai + 2 < ax + 4, before that broadcaster completes. It therefore has ql round-r parents. Ancestor closure and lemma 21 therefore place the ordinary round-r set in DAGh before it stops. Suppose first that r = ai + 2. If ah = ai + 1, then round r is only ah + 1 at ph , where the additional condition is unavailable; crossing it stores the ordinary ql round-r set required by pi . If ah = ai − 1, round r is ph ’s final transition round. Crossing it stores a ql+1 set in round r or r + 1. In the latter case the second set in the statement is already present. In the former

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

case, ph cannot stop all tasks immediately upon completing the transition. If it is removed by this transition, its departure rule first obtains fl+1 + 1 admissible round-(r + 2) blocks from distinct Rl+1 -member broadcasters. At least one has a correct broadcaster; choose that block. If ax is the chosen correct broadcaster’s install transition round, the bound above gives ax ≤ ai , so ax + 4 ≤ ai + 4 = r + 2. Completion occurs at the beginning of that round, before block production, so the chosen block is an ordinary Rl+1 -declared block with exactly ql+1 eligible round-(r + 1) parents. They form the required set. If it belongs to members(Rl+1 ), any later removal occurs only after it has continued advancing, and its first advancement from round r + 1 with Rl+1 installed has no additional disjunct and stores a ql+1 round-(r + 1) set. Thus that set is present before the final flood. Now suppose that r = ai + 3. If ah = ai − 1, then ph has already completed this transition at the beginning of round r. If it is removed by this transition, its DAG contains the fl+1 + 1 admissible round-(r + 1) blocks from distinct Rl+1 -member broadcasters. Choose one with a correct broadcaster. If ax is the chosen correct broadcaster’s install transition round, the bound above gives ax ≤ ai , so ax + 4 ≤ ai + 4 = r + 1. Completion occurs before block production in that round, so this is an ordinary Rl+1 -declared block with exactly ql+1 eligible round-r parents. If it belongs to members(Rl+1 ), it cannot be removed later without first taking its ordinary Rl+1 advancement from round r. Either way its DAG stores the ql+1 round-r set required by pi before it stops. If ah = ai + 1, then r is ph ’s penultimate transition round. Crossing it stores either a ql round-r set or a ql+1 round-(r + 1) set. For a removal or unchanged membership, ql ≥ ql+1 , and every block eligible under Rl is also eligible under Rl+1 , so the former contains the blocks required by pi ’s ordinary condition. For an addition, ql may equal ql+1 − 1. Process ph must then cross its final transition round r + 1 before it can stop. It stores a ql+1 set in round r + 1 or r + 2. In the first case the second set in the statement is present. In the second, the set in round r + 2 contains a block with a correct broadcaster because ql+1 > fl+1 . Every correct process that produces a round-(r + 2) block has installed Rl+1 before block production: if ax is its install transition round, the bound above gives ax ≤ ai + 1, so ax + 4 ≤ ai + 5 = r + 2. Thus this is an ordinary Rl+1 -declared block with exactly ql+1 round-(r + 1) parents. By lemma 21, those parents form the required round-(r + 1) set. These cases exhaust the possible relative install transition rounds of pi and ph . ◀ ▶ Lemma 38 (Every AdvanceRound iteration in rounds ai +1, ai +2, ai +3 eventually terminates). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl . Assume that the earliest correct old-member install transition round t exists. If the transition adds a correct process, assume that its DiscoverBegin call returns a round u. Let pi be a correct retained, joining, or removed process with install transition round ai . Then every AdvanceRoundi iteration before the beginning of round ai + 4 eventually terminates. If the transition adds a correct process pj , then the wait |LocalBlocksj (Rl , u + 1)| ≥ ql that precedes rj ← u + 1 and the start of CatchUpTasksj in algorithm 7 also eventually terminates. In particular: 1. an iteration whose ordinary condition uses Rl eventually satisfies that condition, or, if its current round is ai + 2, eventually satisfies |ParentBlocksi (Rl+1 , ai + 3)| ≥ ql+1 ; 2. in round ai + 3, process pi eventually satisfies |ParentBlocksi (Rl+1 , ai + 3)| ≥ ql+1

XX:51

XX:52

Seamless Reconfiguration for DAG BFT

or |ParentBlocksi (Rl+1 , ai + 4)| ≥ ql+1 . Moreover, if two correct Rl+1 -members complete at the beginnings of consecutive rounds c and c + 1, then the earlier process eventually satisfies its ordinary round-c parent-quorum condition. Proof. By corollary 29 and lemmas 32 and 33, the install transition rounds of any two correct retained, joining, or removed processes differ by at most one. The threshold counts used below are the following. There are at least ql correct old members. After a removal there are at least ql+1 correct retained members. After an addition, if the joining process is correct, the correct old members together with it contain at least ql+1 ≤ ql + 1 correct members; if it is Byzantine, the fault bound for Rl+1 leaves at least ql+1 correct old members. With unchanged membership the two thresholds are equal. Moreover, lemma 34 makes every correct old member eligible for the correct joining process’s round-(u + 2) and round-(u + 3) BRB instances. For every round-broadcaster slot used below, BRB Agreement is already available without invoking the later global BRB-safety theorem. While a correct old member still enables Rl , it follows from lemma 19; for the only round in which the joining process still enables both configurations and no correct old member still enables Rl , it follows from lemma 35; and once only Rl+1 can certify a slot, it follows from the same-configuration quorum-intersection case of lemma 5. If the transition adds a correct process pj , we treat its wait |LocalBlocksj (Rl , u + 1)| ≥ ql as a wait of round index u + 1 = aj + 1 whose ordinary condition is |ParentBlocksj (Rl , u + 1)| ≥ ql , the ordinary condition of its round-(u + 1) AdvanceRound iteration, with no additional condition. By lemma 9, applied to pj in round u + 1 ≥ δl+1 , every block in ParentBlocksj (Rl , u + 1) has a broadcaster in members(Rl ), so that condition implies the wait’s condition. While the wait is pending, HistoryTasksj runs, so pj processes certified-block messages and runs FetchAndDeliver. Suppose that some such wait, or some AdvanceRound iteration before its process’s transition-completion round, never terminates. There are finitely many correct retained, joining, or removed processes and at most four such waits at each. Choose a nonterminating wait with the least logical-round index s, and let pi execute it. Let Rc and qc be the configuration and threshold in its ordinary condition. Thus Rc = Rl and qc = ql unless s = ai + 3, in which case Rc = Rl+1 and qc = ql+1 . Choose correct processes whose prescribed round-s blocks can fill that ordinary condition. If Rc = Rl , choose ql correct old members. If Rc = Rl+1 , choose ql+1 correct retained members after a removal, ql+1 correct retained members when membership is unchanged, and, after an addition, choose ql+1 correct processes from the correct old members together with the correct joining process when it is correct, or from the correct old members when it is Byzantine. A correct joining process is selected only in a round in which the protocol prescribes one of its two transition appends or ordinary post-join production; its passive round u + 1 is never needed for a new-configuration parent set. For every selected block, also choose correct members to perform the prescribed BRB tasks for its declared configuration: ql correct old members for an Rl -declared block and ql+1 correct Rl+1 -members for an Rl+1 -declared block. None of these chosen members is in a passive round when the selected instance is prescribed. First suppose that a selected producer or a member selected to perform the BRB tasks has already stopped all protocol tasks. It stopped only after a removal rule and sent a final finite FloodDAG. By lemma 37, its final DAG contained the blocks required by pi ’s

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

ordinary round-s condition, or, when the additional condition is available, the permitted ql+1 round-(s + 1) set. Both processes had authenticated Rl+1 , so pi ∈ known h for the stopped process ph . The final flood was therefore sent to pi , even if pi had not yet begun this iteration. Reliable queued delivery, the certificate-level form of BRB Agreement established above, and lemma 24 make pi insert the set and its ancestors and satisfy the applicable condition, a contradiction. Hence no selected process has already stopped. Every selected producer ph eventually enters round s. A correct old member enters round t + 2 by the proof of corollary 29, and every round from t + 2 to s − 1 is one of its transition rounds; the correct joining process is selected only for s ≥ u + 2, and its waits begin at round u + 1 once DiscoverBegin has returned. Hence a producer that never enters round s is permanently blocked in a wait of smaller round index, contradicting the choice of s. If a selected producer entered s through its ordinary condition, the predecessor set on which its prescribed round-s append waits is already in its DAG. The producer is not in its passive round, so MaySendBRBh (Rc , s) holds, and the lifecycle rule keeps the already invoked append live until it reaches and passes BRB-Broadcast. If instead a selected producer ph entered s through the additional condition, it already stores ql+1 certified round-s blocks. When Rc = Rl+1 , dissemination of that set and its ancestors directly satisfies pi ’s ordinary condition, contradicting the choice of pi . It remains to consider this event when Rc = Rl . It can occur only for a producer whose install transition round is one less than ai . Its certified round-s set contains a block produced by a correct old member and declared under Rl : after an addition, exclude the at most fl+1 Byzantine slots and the single joining-process slot; after a removal or unchanged membership, the applicable threshold similarly leaves a correct old-member slot. No correct old member has completed this transition before producing a block in this case, where the producer’s install transition round is one less than ai . The chosen ordinary block has exactly ql round-(s − 1) parents. By lemma 21, those parents belong to ParentBlocksh (Rl , s − 1). Dissemination of its causal history therefore discharges the predecessor waits of the selected old-member round-s appends. Thus the selected appends reach and pass their BRB-Broadcast calls unless the correct process whose DAG contains the certified round-s set has already satisfied pi ’s condition. The immutable round-s enabled-configs values make every member selected to perform the BRB tasks eligible for the selected instance. For every selected producer px , advancing a local round does not change MaySendBRBx (Rc , s) because it consults the immutable historical round-s value. The BRB handlers likewise apply ValidInstancex (s, µ) to the immutable rounds value. If a selected producer or a member selected to perform the BRB tasks is the first one that stops all protocol tasks while a selected certificate is missing, apply the same finalFloodDAG argument above. The strengthened lemma 37 applies independently of whether the stop precedes or follows the start of pi ’s wait, and again contradicts nontermination. In the remaining case, every chosen member continues its prescribed BRB tasks while the selected certificates are missing. For each selected proposal, the chosen members send the required echoes and votes, so its certificate is formed. The certified-block messages sent when certificates are assembled and blocks are inserted, together with FloodDAG, deliver the selected blocks and their ancestors to pi . When pi is the joining process, each such sender eventually processes Rl+1 , after which pi belongs to its known-identity set by lemma 23, and the FloodDAG invoked by UpdateKnown resends every block it stored earlier. BRB Agreement excludes a conflicting block in every selected slot. Hence lemma 24 makes pi obtain the blocks required by its ordinary parent-quorum condition, again a contradiction. Thus, if the transition adds a correct process pj , its wait |LocalBlocksj (Rl , u + 1)| ≥ ql terminates, and

XX:53

XX:54

Seamless Reconfiguration for DAG BFT

every AdvanceRound iteration before its process’s transition-completion round terminates. Finally, suppose correct Rl+1 -members px and py complete at the beginnings of consecutive rounds c and c + 1, respectively. Process py executes its final transition-round iteration in round c. Apply the result just proved to that iteration. If it satisfies its ordinary parentquorum condition, dissemination directly supplies px ’s ordinary round-c condition. If it uses the ql+1 admissible round-(c + 1) blocks permitted by the additional transition-round condition and px has already advanced to c + 1, then px ’s round-c condition has already terminated. Otherwise, that round-(c + 1) set contains a block with a correct broadcaster: after an addition, exclude at most fl+1 Byzantine slots and the joining slot; after a removal or unchanged membership, ql+1 exceeds the applicable old-configuration fault bound as shown above. Every correct old member has completed before producing in round c + 1, so this is an ordinary Rl+1 -declared block. By lemma 21, its ql+1 parents belong to ParentBlocksx (Rl+1 , c) after their causal history is disseminated. Thus px ’s ordinary round-c condition eventually holds. Correct Rl+1 -members are not removed by this transition, and lemma 12 prevents a following transition from authorizing a departure during these rounds. This proves every conclusion. ◀ ▶ Lemma 39 (Every transition-round AdvanceRound iteration whose parent-quorum threshold is ql eventually terminates). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl . Assume that an earliest install transition round t among correct processes in members(Rl ) exists. If the transition adds a correct process pj , also assume that DiscoverBeginj (Rl , Rl+1 ) returns a round u. Then every correct retained, joining, or removed process pi with install transition round ai whose current AdvanceRound iteration has an ordinary ql condition eventually advances. It either satisfies that condition or, in round ai + 2, satisfies the additional transition-round condition with threshold ql+1 . For a correct joining process with install transition round u, both ql waits in its prescribed round-(u + 2) and round-(u + 3) DAG-Transition-Append invocations eventually become true, and both invocations reach BRB-Broadcast. Proof. Apply conclusion 1 of lemma 38. If the additional condition is used, lemma 36 also discharges the final transition-round iteration. For a correct joining process, lemma 38 shows that the wait preceding CatchUpTasksj terminates and that its round-(u+1) iteration terminates through |ParentBlocksj (Rl , u+1)| ≥ ql , the additional condition being unavailable in round u + 1. Since ParentBlocksj (Rl , u + 1) ⊆ ParentBlocksj (Rl+1 , u + 1), the ql wait of the round-(u + 2) transition append is already satisfied when that append starts. For the round-(u + 3) append, either its ql admissible round-(u + 2) blocks are delivered directly or at least ql+1 admissible round-(u + 3) blocks are delivered. The latter set contains a block produced by a correct old member or by the correct joining process, with at least ql round-(u + 2) parents. Ancestor closure and the certified parent-count check therefore supply the pending append’s ql set. In both rounds the enabled-configs premise for the BRB call follows from lemma 34, so each invocation reaches BRB-Broadcast. ◀ ▶ Lemma 40 (Every final transition-round AdvanceRound iteration eventually terminates). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl . Assume that an earliest install transition round t among correct processes in members(Rl ) exists. If the transition adds a correct process pj , also assume that DiscoverBeginj (Rl , Rl+1 ) returns a round u. Then every correct retained, joining, or removed process pi with install transition round ai eventually

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

advances from its final transition round ai + 3. It either DAG-delivers ql+1 admissible blocks in that round or DAG-delivers ql+1 admissible blocks in round ai + 4 and uses the additional condition. Moreover, if two correct Rl+1 -members complete at the beginnings of consecutive rounds c and c + 1, then the earlier process eventually satisfies its ordinary round-c parent-quorum condition. Proof. Apply conclusion 2 and the final conclusion of lemma 38. In the additional-condition case, lemma 36 reaches the completion boundary. ◀ ▶ Corollary 41 (Every correct retained, joining, or removed process reaches its transition-completion round). Under the premises of lemma 39, every correct retained, joining, or removed process with install transition round ai eventually reaches the beginning of round ai + 4. A correct process removed by the transition then continues the communication, BRB, fetch, and DAG tasks prescribed by its departure procedure. Proof. Apply lemmas 39 and 40. The serialized algorithm increments one round at a time, so the beginning-of-round rule is executed at ai + 4. ◀

B.1.6

Transition Completion

▶ Lemma 42 (Once a correct old member installs the transition and any correct joining process completes discovery, every correct Rl+1 -member completes the transition). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl . Assume that the earliest install transition round t among correct processes in members(Rl ) exists. If the transition adds a correct process pj , also assume that DiscoverBeginj (Rl , Rl+1 ) returns a round u. Then every correct process pi ∈ members(Rl+1 ) eventually installs Rl+1 , completes this transition, and continues its prescribed protocol tasks with local i = Rl+1 . Proof. Every required round advancement occurs by corollary 41. By corollary 29, every correct retained member invokes InstallTransition with an install transition round ai ∈ {t, t + 1}. If the transition adds a correct process pj , the joining procedure invokes InstallTransition with aj = u, where u is returned by DiscoverBegin. The progress corollary makes each process advance through round ai + 3. At the beginning of round ai + 4, the applicable protocol rule invokes FinishTransitioni (Rl+1 ), which installs Rl+1 and completes the transition. ◀ ▶ Lemma 43 (A removed correct process eventually reaches the point at which the protocol permits it to leave). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuancerule assumption and the configuration-level induction hypothesis for Rl , and assume that its earliest install transition round exists. Let pi ∈ members(Rl ) \ members(Rl+1 ) be correct. Let t be the earliest correct old-member install transition round. By corollary 29, pi invokes InstallTransition in some round ai ∈ {t, t + 1}. Eventually,   B = ⟨m, ai + 5, µ, C⟩ ∈ DAGi [ai + 5], ID(µ) ≥ fl+1 + 1. ID(µ) ∈ members(Rl+1 ), Admissiblei (B) Once this condition holds, pi stops its remaining communication and DAG tasks and may leave.

XX:55

XX:56

Seamless Reconfiguration for DAG BFT

Proof. Process pi installs Rl+1 and completes its transition at the beginning of round ai + 4. It stops starting new block-production operations and stops round advancement, leaderelection, and finalization tasks. While its departure wait is pending, every block-production operation invoked earlier remains live until it invokes BRB-Broadcast. It also continues processing certified-block messages, running FetchAndDeliver, and performing the remaining communication and DAG tasks prescribed during the departure wait. Put v = ai + 5. Because this transition removes a process, every Rl+1 -member is retained, and at least ql+1 of them are correct. By lemma 42, all correct retained members have completed by the beginning of round t + 5. We first show that some correct retained process stores at least ql+1 admissible round-v blocks in distinct Rl+1 -member slots. If v = t + 5, let c+ be the latest completion round of a correct retained process. By corollary 29, c+ ∈ {t + 4, t + 5}. Suppose first that c+ = t + 5. The processes that complete in round t + 5 enter that round by corollary 41, while the last conclusion of lemma 40 makes every process that completed in round t + 4 satisfy its ordinary round-(t + 4) condition and enter round t + 5. If any correct retained process uses the additional condition to enter round t + 5, it already stores the required round-v set. Otherwise every correct retained process enters round v with its ordinary round-(v − 1) set, so at least ql+1 correct prescribed round-v appends reach BRB-Broadcast. Suppose instead that c+ = t + 4. The removed correct process pi has an assigned round(t + 4) enabled-configs value containing Rl , so lemma 19 gives Agreement through that round. Moreover, every correct retained process has completed this transition, and lemmas 6 and 12 keeps a following transition from being installed before round t + 6. Thus the additional condition is unavailable in the selected round-(t + 4) iterations. If a correct retained process used the additional condition to enter round t + 4, it stores ql+1 admissible round-(t + 4) blocks. Dissemination of that set and its ancestors makes every correct retained process satisfy its ordinary round-(t + 4) condition, enter round v, and make its prescribed round-v append reach BRB-Broadcast. Otherwise every correct retained process entered round t + 4 with its ordinary round-(t + 3) set, and, because completion precedes block production, at least ql+1 correct prescribed Rl+1 -declared round-(t + 4) appends reach BRB-Broadcast. Applying corollary 28 to each correct retained process makes all of them enter round v with the ordinary round-(v − 1) set, so at least ql+1 correct prescribed round-v appends reach BRB-Broadcast. If v = t + 6, first apply the same dichotomy to round t + 5. A process that used the additional condition already stores ql+1 certified round-(t+5) blocks; otherwise the prescribed round-(t + 5) DAG-Append operations reach BRB-Broadcast. Here ai = t + 1, so the removed correct process’s immutable round-(t + 5) enabled-configs value still contains Rl ; lemma 19, together with the BRB Agreement clause of the configuration-level induction hypothesis for Rl , gives Agreement through round t + 5. Each correct retained process px whose prescribed round-(t + 5) append reaches BRB-Broadcast belongs to Rl+1 , has Rl+1 in its immutable enabled-configs value, and is not passive, so its call passes MaySendBRBx (Rl+1 , t + 5). Each such process has completed the transition into Rl+1 . If Rl+2 exists, lemmas 6 and 12 prevents installing the following transition before round t + 6; if it does not exist, there is no following transition. Hence the additional condition is unavailable in every selected round-(t + 5) iteration. Thus corollary 28 supplies a correct process whose DAG contains such a set. Dissemination makes every correct retained member px obtain that set and advance ordinarily to v. Its round-v append then uses those round-(v − 1) parents, passes MaySendBRBx (Rl+1 , v), and reaches BRB-Broadcast. In either case, if a correct retained process already stores the selected round-v set, fix it

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

as ph . Otherwise apply corollary 28 to the ql+1 correct processes whose prescribed round-v appends reach BRB-Broadcast. Each such process px is a non-passive Rl+1 -member with Rl+1 in its immutable round-v enabled-configs value, so its call passes MaySendBRBx (Rl+1 , v). We next verify the corollary’s Agreement premise. The removed correct process pi has Rl in each assigned enabled-configs value before and during its install round; InstallTransition then assigns {Rl , Rl+1 } in rounds ai + 1, . . . , ai + 4 = v − 1. Thus lemma 19, together with the BRB Agreement clause of the configuration-level induction hypothesis for Rl , gives Agreement through round v − 1. It remains to prove Agreement in round v. If v = t + 5 and some correct Rl -member still has an assigned round-v enabled-configs value containing Rl , then lemma 19 gives Agreement. If no such process exists, a certificate declared under Rl cannot be formed: its Byzantine members alone are fewer than ql ; the conclusions for preceding transitions similarly exclude every earlier configuration. If Rl+2 exists, lemma 12 gives earliest(Rl+2 ) ≥ t + 6 > v, and authenticated consecutive processing prevents Rl+3 or any later configuration from being enabled before Rl+2 . If Rl+2 does not exist, authentication excludes every later configuration directly. Thus only Rl+1 can certify in round v, and the same-configuration case of lemma 5 gives Agreement. If v = t + 6, every correct old member’s four rounds assigned {Rl , Rl+1 } end by t + 5. Hence Rl , every earlier configuration, and their Byzantine members cannot supply a quorum in round v. If a following Rl+2 exists, it cannot be enabled in round v: its earliest-inclusion round is at least t + 6; therefore no certified block below v can mark it by lemma 6 applied to the following transition, and an old member can invoke InstallTransition from round-v marked blocks only after its pending ordinary round-v wait terminates. That invocation assigns the new enabled pair beginning in round v + 1. Likewise, a process joining in Rl+2 can discover no qualifying marked round below v, and its invocation assigns the pair only after its returned round. Authenticated consecutive processing prevents Rl+3 or any later configuration from being enabled before Rl+2 . If Rl+2 does not exist, authentication excludes every later configuration directly. Consequently only Rl+1 can certify in round v, and same-configuration quorum intersection again gives Agreement. By round v, every correct retained process has completed the transition into Rl+1 , so the additional condition for that transition is unavailable in round v. A following transition cannot make that condition applicable during the same execution of the round-v AdvanceRound loop, because UpdateConfigs runs only after the ordinary round-v condition. The corollary therefore makes some correct retained process ph advance from v, and its ordinary condition places the required set in DAGh . Every block in the selected round-v set occupies an Rl+1 -member broadcaster slot. Indeed, this transition removes only pi . Process pi is correct and starts no block-production operation for round v after completing in round ai + 4, so BRB Integrity excludes a valid round-v certificate in its slot. The conclusions for preceding transitions exclude identities belonging only to a configuration earlier than Rl from producing a certified block in round v. Every other member of members(Rl ) is retained in Rl+1 . If Rl+2 exists, lemma 12 places its earliest-inclusion round at or after t + 6, and lemma 6 applied to that transition shows that no earlier certified block can mark it. Thus it cannot be installed before round t + 6; even if it is installed when v = t + 6, that invocation assigns its enabled pair beginning only in round v + 1. Authenticated consecutive processing also prevents a later configuration from being enabled first. If Rl+2 does not exist, authentication excludes every later configuration. Hence no configuration later than Rl+1 is enabled in round v. Thus the selected distinct slots belong to members(Rl+1 ).

XX:57

XX:58

Seamless Reconfiguration for DAG BFT

Suppose, for contradiction, that the displayed condition never becomes true. Then pi does not reach the instruction that stops its remaining tasks, so it continues processing certified-block messages and running FetchAndDeliver. The selected round-v set in DAGh contains at least ql+1 − fl+1 ≥ fl+1 + 1 blocks with correct broadcasters; choose that many and include their ancestors. The removed identity belongs to known h , so the certified-block messages sent when these blocks are inserted and during FloodDAG invocations are addressed to pi . BRB Agreement through round v − 1 = ai + 4 excludes a different block in every ancestor slot, and BRB Integrity excludes a different certified value in each selected correct broadcaster’s round-v slot. Hence lemma 24 makes pi DAG-deliver the selected blocks. Their distinct broadcaster identities all belong to Rl+1 , so the displayed departure condition holds, a contradiction. Hence the condition eventually holds. Process pi performs the prescribed final finite FloodDAG and only then stops and leaves; messages it already sent remain deliverable. ◀ ▶ Lemma 44 (Every correct Rl+1 -member reaches a round in which ql+1 correct members’ prescribed appends reach BRB-Broadcast). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl . Assume that the earliest install transition round t among correct processes in members(Rl ) exists. If the transition adds a correct process pj , also assume that DiscoverBeginj (Rl , Rl+1 ) returns a round u. Then there exists a logical-round index s such that: 1. every correct process in members(Rl+1 ) eventually enters round s with installed configuration Rl+1 ; and 2. at least ql+1 distinct active correct processes in members(Rl+1 ) invoke their prescribed DAG-Append operation in round s and reach its BRB-Broadcast call. Proof. For each correct pi ∈ members(Rl+1 ), let ci be the round at whose beginning it completes the transition. By lemma 42, every ci is finite. Since members(Rl+1 ) is finite, let c− = min{ci : pi ∈ members(Rl+1 ) is correct}

and

c+ = max{ci : pi ∈ members(Rl+1 ) is correct}.

The bounds on the completion rounds give c+ ≤ c− + 1. If c− = c+ , every correct member enters round c+ when it completes the transition. Otherwise c+ = c− + 1. Members that complete in round c+ enter that round by lemma 42. For each member that completes in round c− , the final conclusion of lemma 40 supplies its ordinary round-c− parent quorum, so it also advances to c+ . Thus every correct member enters round c+ with Rl+1 installed. Completion occurs before round-c+ block production. If every correct member entered c+ through its ordinary condition, each already has the ql+1 round-(c+ − 1) blocks on which its ordinary round-c+ append waits. Thus at least nl+1 − fl+1 = ql+1 correct members invoke that append and reach BRB-Broadcast. Take s = c+ . Otherwise, some correct member entered c+ through the additional condition and therefore already stores ql+1 admissible round-c+ blocks. The certified-block messages sent upon insertion and FloodDAG invocations disseminate that set and its ancestors to every correct Rl+1 -member. After all have reached c+ , their transitions are complete, so the set satisfies their ordinary round-c+ advancement condition and they enter c+ + 1. Their round-(c+ + 1) appends use that same round-c+ set as parents and reach BRB-Broadcast. Take s = c+ + 1. In both cases the two conclusions hold. ◀

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

B.1.7

XX:59

Establishing the Prerequisites and Applying the Configuration-Level Induction

The preceding conditional progress results apply once their prerequisites hold. We now prove that some correct old member invokes InstallTransition and, when the transition adds a correct process, that DiscoverBegin returns at the joining process. We then prove the configuration-level induction hypothesis for Rl+1 . ▶ Lemma 45 (Some correct Rl -member eventually invokes InstallTransition for Rl → Rl+1 ). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl . Then there exist a correct process pi ∈ members(Rl ) and a logical round ai such that pi eventually invokes InstallTransitioni (Rl , Rl+1 , ai ). Consequently, the set of install transition rounds of correct processes in members(Rl ) is nonempty, and its minimum  t = min ai

pi ∈ members(Rl ) is correct and pi invokes InstallTransitioni (Rl , Rl+1 , ai )



exists. Proof. Every correct process that receives Rl+1 authenticates and buffers it. Authentication and consecutive numbering exclude a conflicting message. Suppose, for contradiction, that no correct process in members(Rl ) ever invokes InstallTransition. Every enabled-configs value subsequently assigned by such a process then equals {Rl }. Starting from the logical round whose existence is required by clause (iv) of the configuration-level induction hypothesis for Rl , BRB Agreement for certificates declared under Rl and induction on the logical round using corollary 28 make every active correct old member enter every later logical round. The induction invariant includes at least ql correct appends that reach BRB-Broadcast: clause (iv) gives the base, the contradiction hypothesis makes the additional transition condition unavailable in every round, and ordinary entry supplies the parent set needed by the next append. Consequently, after installing Rl , every correct old member that has received Rl+1 eventually reaches earliest(Rl+1 ). Its reconfiguration handler then completes the wait and assigns pending i ← Rl+1 . Choose a set S of fl +1 correct old members. Eventual message delivery ensures that every member of the finite set S receives Rl+1 and eventually makes this pending assignment. For each member, let si be the first logical round whose append begins after the handler assigns pending i ← Rl+1 , and let s = maxpi ∈S si . Because these processes continue advancing, every member of S eventually enters round s and produces a certified block whose pending field contains Rl+1 . Let M be these fl + 1 marked round-s blocks. If a correct old member invokes InstallTransition while processing round s, the contradiction is immediate. Otherwise, let X be any round-(s + 1) block produced by a correct old member. The round-broadcaster slots occupied by its ql round-s parents intersect the fl + 1 slots occupied by M. BRB Agreement in round s ensures that an intersecting slot denotes the same marked block, so X is marked. Thus every round-(s + 1) block from a correct old broadcaster is marked. Any correct old member that advances from that round obtains ql blocks in distinct round-broadcaster slots occupied by members of Rl , at least ql − fl ≥ fl + 1 of which have correct broadcasters and are marked. It therefore invokes InstallTransition, contradicting the assumption. ◀

XX:60

Seamless Reconfiguration for DAG BFT

▶ Lemma 46 (DiscoverBegin at a correct joining process eventually terminates). Fix a valid transition Rl → Rl+1 in an execution satisfying the issuance-rule assumption and the configuration-level induction hypothesis for Rl , and suppose it adds a correct process pj . Let t be the earliest install transition round among correct processes in members(Rl ), whose existence follows from lemma 45. Then DiscoverBeginj (Rl , Rl+1 ) eventually terminates and returns the least qualifying round u present in DAGj when its wait is discharged: that round contains blocks in at least ql distinct round-broadcaster slots occupied by members of Rl , including at least fl + 1 blocks marked for Rl → Rl+1 . Proof. The distribution mechanism sends the authenticated pair ⟨Rl , Rl+1 ⟩ to pj , so the joining handler can validate the transition and obtain Πl , ql , and fl . BRB Agreement through round t follows from lemma 19. By lemma 13, every correct round-(t+1) block in members(Rl ) is marked. At least ql correct old-member round-(t + 1) appends reach BRB-Broadcast: entry into that round used the ordinary round-t condition, and the additional condition is unavailable before round t + 2. BRB Agreement and corollary 28 therefore make a correct old member store at least ql round-(t + 1) blocks in distinct old-member broadcaster slots. Any such set contains at least ql − fl = nl − 2fl ≥ fl + 1 blocks with correct broadcasters, and all of those blocks are marked. Fix one correct old member ph , let Q be such a set in DAGh , and let D contain Q and all of its ancestors. The set is finite because each block has finitely many parents in the preceding round, and lemma 20 gives D ⊆ DAGh . Process ph eventually receives Rl+1 . Upon that receipt, UpdateKnownh (Rl+1 ) adds pj to known h and invokes FloodDAGh . That invocation, certified-block messages sent upon insertion, later invocations of FloodDAGh , and a final invocation if ph is later removed send every block in D to pj . Suppose, for contradiction, that DiscoverBeginj (Rl , Rl+1 ) never returns. The joining protocol starts HistoryTasksj before invoking DiscoverBeginj (Rl , Rl+1 ); those tasks continue processing certified-block messages and running FetchAndDeliver. The blocks in D pass the required metadata and referenced-parent checks, and BRB Agreement through round t + 1 excludes a different block in any of their round-broadcaster slots. Therefore, lemma 24 makes pj DAG-deliver D. Consequently, DAGj contains the ql distinct blocks in Q, whose broadcaster identities belong to Rl , including at least fl + 1 marked blocks, even if ph has already departed. Thus DAGj eventually contains a round satisfying the two discovery conditions, contradicting the assumption that DiscoverBeginj (Rl , Rl+1 ) never returns. Therefore its wait is eventually discharged, and it returns the least qualifying round then present in DAGj ; it makes no claim about blocks merged only after the return. The repeated request ⟨state-request, Rl , Rl+1 ⟩ to every identity in known j provides an additional retrieval path, and one sufficient state reply would establish the same condition, but the proof does not require a process that stores a block to remain active until it receives a request. Whenever a reply is used, its safety is sender-independent by lemma 22. ◀ ▶ Lemma 47 (A valid transition establishes completion, departure, progress, and the BRB Agreement premise for the next induction step). Fix a valid transition Rl → Rl+1 in an execution satisfying the system and reconfiguration assumptions of Section 3 and the issuancerule assumption, and assume the configuration-level induction hypothesis for Rl . Then the following conclusions hold:

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

XX:61

1. Every correct process pi ∈ members(Rl+1 ) eventually invokes InstallTransitioni (Rl , Rl+1 , ai ) for some finite round ai , reaches the beginning of round ai +4, and invokes FinishTransitioni (Rl+1 ). Immediately afterward, local i = Rl+1 ,

pending i = ⊥,

transition i = ⊥.

2. Every correct process in members(Rl ) \ members(Rl+1 ) eventually reaches the point at which the protocol permits it to leave. 3. There is a logical round s that every correct process in members(Rl+1 ) eventually enters with Rl+1 installed and in which at least ql+1 active correct members invoke the prescribed DAG-Append operation and reach its BRB-Broadcast call. 4. If a valid transition Rl+1 → Rl+2 is issued, then BRB Agreement holds for every roundbroadcaster slot whose round index is less than δl+2 = earliest(Rl+2 ). If no following transition is issued, BRB Agreement holds for every round-broadcaster slot whose round index is at least δl+1 . Consequently, if Rl+1 → Rl+2 is issued, the configuration-level induction hypothesis holds for Rl+1 . Proof. By lemma 45, the earliest install transition round t among correct processes in members(Rl ) exists. If the transition adds a correct process pj , lemma 46 supplies the round u returned by DiscoverBeginj (Rl , Rl+1 ). Every correct retained process invokes InstallTransition in round t or t + 1 by corollary 29. A correct joining process invokes InstallTransition with install transition round u by algorithm 7. Hence the premises of corollary 41 hold. That corollary supplies each required round advancement, and lemma 42 shows that every correct Rl+1 -member reaches the beginning of its round ai + 4. At that point, the retained-process and joining-process rules in algorithms 4 and 7 invoke FinishTransitioni (Rl+1 ); the definition of that procedure in algorithm 4 gives the stated post-transition values. This proves the first conclusion. If a correct process is removed, lemma 43 proves the second conclusion; otherwise it is vacuous. Finally, lemma 44 proves the third conclusion. For the fourth conclusion, if Rl+1 → Rl+2 is issued, fix a round r < δl+2 ; otherwise, fix any round r ≥ δl+1 . If r < δl+1 , BRB Agreement follows directly from the configuration-level induction hypothesis for Rl . Suppose instead that r ≥ δl+1 . There are three cases. 1. If some correct old member has an assigned round-r enabled-configs value containing Rl , apply lemma 19. 2. Suppose no correct old member has such a value, but the transition adds a correct process whose round-r value is {Rl , Rl+1 }. Every correct old member then either has no assigned value and sends no round-r BRB echo or vote, or has an assigned value excluding Rl . Lemma 35 gives Agreement. 3. Otherwise, no correct process eligible to vote enables Rl . Earliest-inclusion rounds increase strictly along the issued sequence by lemmas 10 and 12. For any c < l, a correct round-r voter under Rc would be a member of members(Rc ) whose round-r enabled-configs value contains Rc . Applying lemma 18 to that preceding transition would give r < earliest(Rc+2 ) ≤ earliest(Rl+1 ) = δl+1 , contradicting r ≥ δl+1 . If Rl+2 is issued, then r < earliest(Rl+2 ) ≤ earliest(Rc ) for every c ≥ l + 2. A correct member of Rc enables Rc only in rounds greater than its install transition round for Rc−1 → Rc . By lemma 10, that install transition round is at least earliest(Rc ). Hence no

XX:62

Seamless Reconfiguration for DAG BFT

such member can vote under Rc in round r. If Rl+2 is not issued, authentication excludes every later configuration directly. Since Byzantine members alone cannot form a certificate, every valid round-r certificate is declared under Rl+1 . Two such certificate quorums intersect in a correct process, which votes for at most one value in a round-broadcaster slot, so BRB Agreement holds. These cases cover every required round and prove the fourth conclusion. When a successor transition is issued, conclusions 1, 2, 4, and 3 establish clauses (i), (ii), (iii), and (iv), respectively, of the configuration-level induction hypothesis for Rl+1 . ◀ ▶ Lemma 48 (The configuration-level induction hypothesis holds for every configuration with an issued successor). For every issued valid transition Rl → Rl+1 in the authenticated configuration sequence, the configuration-level induction hypothesis for Rl defined above holds. Proof. Proceed by induction on l. For l = 1, every correct process in members(R1 ) starts in round 1 with R1 installed by algorithm 1, while the clauses concerning a preceding transition and removed processes are vacuous. By the rule in Section 4 that invokes DAG-Append at the beginning of a round, every active correct process in members(R1 ) invokes the prescribed operation in round 1. Since at most f1 of the n1 members of R1 are Byzantine, at least n1 − f1 = q1 active correct processes in members(R1 ) make that invocation. A round-1 append has no parent wait, so each reaches its BRB-Broadcast call. Before δ2 = earliest(R2 ), only an instance declared under R1 can receive correct votes. Quorum intersection for two certificates declared under R1 therefore gives BRB Agreement in every round below δ2 . Thus the hypothesis holds for R1 . For the induction step, suppose the hypothesis holds for Rl and that Rl+1 → Rl+2 is issued. Authenticated consecutive processing implies that Rl → Rl+1 was issued. Apply lemma 47 to that transition. Its four conclusions establish the configuration-level induction hypothesis for Rl+1 . ◀ ▶ Lemma 49 (Every valid transition completes at all correct retained or joining processes and eventually permits all correct removed processes to leave). In every execution satisfying the system and reconfiguration assumptions of Section 3 and the issuance-rule assumption, every valid transition Rl → Rl+1 issued in the authenticated configuration sequence has the following properties. Each correct process pi ∈ members(Rl+1 ) eventually invokes InstallTransitioni (Rl , Rl+1 , ai ) for some finite round ai , reaches the beginning of round ai + 4, and invokes FinishTransitioni (Rl+1 ). Immediately afterward, local i = Rl+1 ,

pending i = ⊥,

transition i = ⊥.

Moreover, every correct process in members(Rl ) \ members(Rl+1 ) eventually reaches the point at which the protocol permits it to leave. Proof. By lemma 48, the configuration-level induction hypothesis holds for Rl . The first two conclusions of lemma 47 respectively establish completion at every correct retained or joining process and permitted departure for every correct removed process. ◀

B.1.8

BRB Agreement for Every Round-Broadcaster Slot and Dynamic DAG-Structured Byzantine Broadcast Correctness

▶ Lemma 50 (The configuration-scoped BRB algorithm satisfies Agreement for every round-broadcaster slot). The configuration-scoped BRB algorithm in algorithm 2 satisfies BRB Agreement for every round-broadcaster slot.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Proof. Let R1 , . . . , RL be the finite authenticated configuration sequence. If L = 1, authentication and configuration authorization imply that every valid certificate is declared under R1 . Any two certificates for the same round-broadcaster slot then have voter quorums that intersect in a correct process. Since a correct process votes for at most one value in a slot, the certificates cannot certify different values. Suppose now that L ≥ 2. By lemma 48, the configuration-level induction hypothesis holds before every issued transition. In particular, its Agreement clause covers every round before δ2 = earliest(R2 ). Apply lemma 47 successively to the transitions R1 → R2 , . . . , RL−1 → RL . For every non-final transition, the fourth conclusion of that lemma extends Agreement to every round before the following transition. For RL−1 → RL , there is no following transition, so the same conclusion establishes Agreement in every remaining logical round. Thus BRB Agreement holds for every round-broadcaster slot in the execution. ◀ ▶ Lemma 51 (The protocol implements Dynamic DAG-structured Byzantine Broadcast). Under the system and reconfiguration assumptions of Section 3, the issuance-rule assumption, and the protocol’s known i and admissibility checks, the protocol specified in algorithms 2–7 implements a Dynamic DAG-structured Byzantine Broadcast satisfying definition 1. Proof. Configuration-scoped BRB Agreement and Integrity. Lemma 4 proves Integrity for every configuration-scoped BRB instance, and lemma 50 proves Agreement for every roundbroadcaster slot across the complete configuration sequence. DAG-Integrity. Fix a correct process pj . A block B = ⟨m, r, µ, C⟩ is inserted into DAGj [r] only after the corresponding BRB instance produces the valid quorum certificate C. BRB Integrity and Agreement prevent a correct process from accepting two certified values for one round-broadcaster slot. If the broadcaster pi is correct, the initial BRB message for that slot originates from its prescribed DAG-Appendi or DAG-Transition-Appendi invocation. Thus every block inserted under a correct broadcaster’s identity originates from the prescribed append invocation, and each correct process DAG-delivers at most one block for each round-broadcaster slot. DAG-Consistency. Suppose two correct processes DAG-deliver blocks for the same roundbroadcaster slot. BRB Agreement from lemma 50 makes their (m, r, µ) tuples identical, and threshold-signature uniqueness makes their certificates identical. Hence they DAG-deliver the same block B = ⟨m, r, µ, C⟩. Causal Closure. Fix a block B = ⟨m, r, µ, C⟩ DAG-delivered by a correct process, and let Rc = local(µ) be the configuration under which C is formed. By lemma 20, the certified-block receive and fetch procedures and the validated state-reply merge procedure insert every parent and ancestor before its descendant. The remaining checks establish that every referenced parent is admissible. If µ′ is the metadata of a parent, then number(local(µ′ )) ≤ number(local(µ)). The insertion check also verifies that the parent broadcaster belongs to members(Rd ) for some Rd ∈ enabled(µ′ ): the unique configuration when enabled(µ′ ) is a singleton, or either configuration when it is the authenticated pair of a valid transition. A correct joining process need not reconstruct the earlier process-local values enabled-configs k [s]. Because qc > fc , the block’s BRB certificate includes a share from a correct voter pv that checked the complete (m, r, µ) tuple and applied the applicable parent-count rule. Suppose JoiningMetadata(µ, Rl , Rl+1 ) holds and the block uses ql parents while declaring Rl+1 . If ql < ql+1 , that check required enabled-configs v [r] = enabled(µ) = {Rl , Rl+1 }.

XX:63

XX:64

Seamless Reconfiguration for DAG BFT

Here {Rl , Rl+1 } is the authenticated pair satisfying ValidReconfiguration(Rl , Rl+1 ). If ql = ql+1 , the parent count satisfies the ordinary rule and does not imply this equality. Finally, a correct joining process inserts only validated, ancestor-closed state into the local DAG. Hence every DAG-delivered block is stored together with every parent and ancestor required by Causal Closure. Per-Round Quorum Progress. BRB Agreement for every round-broadcaster slot follows from lemma 50. When the prescribed correct appends reach BRB-Broadcast and the correct processes needed to form the certificates continue their BRB tasks, lemma 27 delivers the certified current-round blocks and their ancestors. When the additional condition is unavailable, corollary 28 removes the separate lifetime premise for the processes needed to form the certificates: either a correct process first stores the current-round quorum and sends it, or all of those processes remain active long enough to certify it. During a transition, a process that advances without satisfying its ordinary parentquorum condition does so only by satisfying the additional condition, which requires ql+1 admissible blocks from the next round. The ancestor-closure and final-FloodDAG arguments in lemma 38 then give every affected correct process either the blocks required by its ordinary parent-quorum condition or the ql+1 admissible next-round blocks allowed by the additional condition in its last two transition rounds. Lemmas 39 and 40 apply these alternatives to the parent-quorum conditions with thresholds ql and ql+1 , including the ordinary condition of a process that completes the transition one round before another correct member. Thus every active correct process whose prescribed round advancement depends on the applicable quorum eventually DAG-delivers sufficient admissible blocks from distinct broadcaster slots to satisfy an applicable round-advancement condition and enter the next round. This establishes Per-Round Quorum Progress as stated in definition 1. Finally, lemma 49 proves the completion clause of definition 1: every retained or joining correct process completes a valid transition, and every removed correct process reaches the point at which it may leave. ◀

B.2 B.2.1

Leader Integrity and Total Order Alignment of Enabled-Configs Values Across Correct Processes in the Same Logical Round

lemma 17 establishes alignment for correct members of the old configuration throughout one transition. We first include a correct joining process for that transition and then compose the result across the finite configuration sequence. For every issued transition used below, lemma 48 supplies the configuration-level induction hypothesis required by the lemmas that fix one transition. ▶ Lemma 52 (Transition windows of distinct valid transitions are disjoint). In every execution satisfying the assumptions of Section 3 and the issuance-rule assumption, the following holds. For a valid issued transition Rl → Rl+1 , let  Wl = s

∃ correct pi : enabled-configs i [s] = {Rl , Rl+1 }

be its transition window. If Wl ̸= ∅, then the earliest install transition round tl among correct old members exists and Wl ⊆ [tl , tl + 5]. For any two valid issued transitions with l < m and Wl , Wm ̸= ∅, every round in Wm exceeds every round in Wl . In particular, Wl ∩ Wm = ∅: for every logical round s there is at most one index l such that some correct process pi satisfies enabled-configs i [s] = {Rl , Rl+1 }.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

XX:65

Proof. A correct process pi assigns the pair {Rl , Rl+1 } only through an invocation InstallTransitioni (Rl , Rl+1 , a), which assigns it exactly to rounds a + 1, . . . , a + 4, and only correct members of members(Rl ) and a correct process joining in the transition invoke it. Hence, if Wl = ̸ ∅, some correct process invokes InstallTransition for the transition and tl exists. Because the transition is issued, lemma 48 supplies the configuration-level induction hypothesis for Rl . By corollary 29, every correct member of members(Rl ) that invokes InstallTransition does so in round tl or tl + 1, and by lemmas 32 and 33, a correct joining process does so in a round ul ∈ {tl − 1, tl , tl + 1}. Every assignment of this pair therefore covers rounds in [a + 1, a + 4] with tl − 1 ≤ a ≤ tl + 1, so Wl ⊆ [tl , tl + 5]. Now fix l < m with Wl , Wm ̸= ∅. For every k with l ≤ k < m, the transition Rk+1 → Rk+2 is issued, so lemma 11 yields a correct invocation of InstallTransition for Rk → Rk+1 , and tk exists. Lemma 12 gives earliest(Rk+2 ) ≥ tk + 6, and lemma 10 gives tk+1 ≥ earliest(Rk+2 ). Hence tk+1 ≥ tk + 6 for every such k, and min Wm ≥ tm ≥ tl + 6(m − l) > tl + 5 ≥ max Wl . Every round of Wm therefore exceeds every round of Wl , and the windows are disjoint.

◀

▶ Lemma 53 (Correct members of Rl and Rl+1 cannot assign {Rl } and {Rl+1 } in the same round). In an execution satisfying the assumptions of Section 3, fix a valid issued transition Rl → Rl+1 and let δl+1 = earliest(Rl+1 ). Fix a logical round r ≥ δl+1 , and suppose some correct pi ∈ members(Rl ) ∪ members(Rl+1 ) satisfies enabled-configs i [r] ̸= ⊥

and

Rl ∈ enabled-configs i [r].

Then every correct process pj ∈ members(Rl ) ∪ members(Rl+1 ) with enabled-configs j [r] ̸= ⊥ satisfies  enabled-configs j [r] ∈ {Rl }, {Rl , Rl+1 }, {Rl+1 } . Moreover, there do not exist two such correct processes pj and pk for which enabled-configs j [r] = {Rl }

and

enabled-configs k [r] = {Rl+1 }.

Proof. By lemma 48, the configuration-level induction hypothesis holds for Rl . By lemma 45, let t be the earliest install transition round. By corollary 29, every correct process in members(Rl ) installs in round t or t + 1. Its successive immutable enabled-configs values are {Rl }, then {Rl , Rl+1 }, and then {Rl+1 }, and two such processes cannot have the two different singleton values in the same round. If a correct process joins, lemmas 32 and 33 gives the same alternatives between its enabled-configs values and those of the old members. To exclude earlier configurations, fix c < l. By lemmas 12 and 52, every round assigned the pair {Rc , Rc+1 } is below earliest(Rc+2 ). Earliest-inclusion rounds increase strictly along the issued sequence by lemmas 10 and 12. Therefore, earliest(Rc+2 ) ≤ earliest(Rl+1 ) = δl+1 ≤ r, so no such pair is assigned in round r. Since r > 1, a correct process assigning the singleton {Rc } in round r is a member of members(Rc ). Lemma 18 would then give r < earliest(Rc+2 ), which is also impossible.

XX:66

Seamless Reconfiguration for DAG BFT

The premise and the install transition round bounds above now give r ≤ t + 5. If Rl+2 exists, lemma 12 gives r ≤ t + 5 < earliest(Rl+2 ) ≤ earliest(Rc )

for every c ≥ l + 2.

A correct process assigns a value containing such an Rc only after an invocation of InstallTransition for Rc−1 → Rc or Rc → Rc+1 . By lemma 10 and the increasing earliest-inclusion rounds, either invocation assigns such values only to rounds greater than earliest(Rc ). Thus no configuration after Rl+1 occurs in an assigned round-r value. If Rl+2 does not exist, authentication excludes every later configuration directly. The stated alternatives therefore cover all assigned values in round r. ◀ ▶ Lemma 54 (Enabled-configs values assigned to correct processes in one logical round involve at most one valid transition). Fix a logical round r and correct processes pi and pj such that Ei := enabled-configs i [r] ̸= ⊥,

Ej := enabled-configs j [r] ̸= ⊥.

Then either Ei = Ej = {Rc } for some configuration Rc , or there is a valid transition Rl → Rl+1 such that  Ei , Ej ∈ {Rl }, {Rl , Rl+1 }, {Rl+1 } and at least one of Ei and Ej equals {Rl , Rl+1 }. In particular, if Ei and Ej are both singletons, then Ei = Ej . Proof. It suffices to prove the stronger claim for the collection of all assigned round-r values at correct processes. For a generic correct process px , inspect enabled-configs x [r]. Each process moves through the authenticated configuration sequence in consecutive order, and for each transition its successive enabled-configs values are the old singleton, then the pair comprising the two configurations of that valid transition, then the new singleton. Suppose one such value is {Rl , Rl+1 }, and let t be the earliest install transition round for this transition. Lemma 52 excludes every other transition pair in round r and gives r ≤ t + 5. The pair is assigned only to rounds after its install transition round, so lemma 10 also gives r > earliest(Rl+1 ). Consider any assigned singleton {Rc } with c < l. Since r > 1, the correct process assigning it is a member of members(Rc ). By lemma 18, r < earliest(Rc+2 ) ≤ earliest(Rl+1 ), a contradiction. Here earliest-inclusion rounds increase strictly along the issued sequence by lemmas 10 and 12. If an assigned singleton {Rc } has c ≥ l + 2, then Rl+2 exists, and lemma 12 gives r ≤ t + 5 < earliest(Rl+2 ) ≤ earliest(Rc ). A correct process assigns {Rc } only after completing the transition into Rc . By lemma 10, its install transition round is at least earliest(Rc ), so such a singleton can be assigned only to a round greater than earliest(Rc ), again a contradiction.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

XX:67

Thus every assigned value is {Rl }, {Rl , Rl+1 }, or {Rl+1 }. Lemma 53 forbids the two singleton enabled-configs values from coexisting. Suppose instead that all enabled-configs values in the round are singletons. If r = 1, all assigned values equal {R1 }, so assume r ≥ 2. Consider two of them, {Ra } and {Rb }, with a < b. If b = a + 1, lemma 53 excludes their coexistence. If b ≥ a + 2, instance authorization implies that the process assigning {Ra } is a correct member of members(Ra ). Let pa be that process; then Ra ∈ enabled-configs a [r], so lemma 18 gives r < earliest(Ra+2 ). Consider the correct process assigning {Rb }. It assigned this singleton only after completing the transition Rb−1 → Rb , either as a retained member of members(Rb−1 ) or as the process joining in that transition; a process removed by that transition stops round advancement and never assigns {Rb }. In both cases its install transition round for Rb−1 → Rb is at least earliest(Rb ) by lemma 10, and it assigns {Rb } only for rounds greater than that install transition round. Hence r > earliest(Rb ). Since b ≥ a+2 and earliest-inclusion rounds increase along the issued sequence, as noted above, earliest(Rb ) ≥ earliest(Ra+2 ), so r > earliest(Ra+2 ) — the opposite inequality. This contradiction excludes nonadjacent singleton values. Thus all singleton enabled-configs values are identical. The two cases prove both claims. ◀ By lemma 51, DAG-Consistency and Causal Closure hold for every block inserted by a correct process. Consequently, the ancestor relation between two stored blocks is independent of the correct process storing them; we omit the process subscript when reasoning about fixed block objects. By algorithm 2, a correct process pi votes for a configuration-scoped BRB instance declared under Rl in round r only when Rl ∈ enabled-configs i [r]. Invocations of Electi are serialized by the requirement in algorithm 9. For a correct process pi , write WaveLeaderi (Rl , w) for the result of evaluating WaveLeader(Rl , w) at pi .

B.2.2

Leader Uniqueness and Direct-Anchor Reachability

Unique Wave Leaders and Their Reachability from Later Blocks. We first show that, in one wave, at most one configuration can have leader-voting blocks in more distinct broadcaster slots than its fault bound. It follows that a wave has at most one accepted leader. We then show that every later-wave block reaches at least fl +1 leader-voting blocks that reach an earlier direct anchor. This makes backward scans deterministic and their leader sequences nested. ▶ Lemma 55 (In one wave, two configurations cannot each have leader-voting blocks in more slots than their respective fault bounds). Let pi and pj be correct processes and let w ≥ 1. Suppose DAGi contains Ra -typed leader-voting blocks for wave w in at least fa + 1 distinct round-broadcaster slots, and DAGj contains Rb -typed leader-voting blocks for that wave in at least fb + 1 distinct round-broadcaster slots. Then Ra = Rb . Proof. Each collection contains a block whose broadcaster is correct. Let X = ⟨mX , last(w), µX , CX ⟩ and Y = ⟨mY , last(w), µY , CY ⟩ be such blocks. By the definitions of Ra -typed and Rb -typed leader-voting blocks, local(µX ) = Ra ,

enabled(µX ) = {Ra },

local(µY ) = Rb ,

enabled(µY ) = {Rb }.

Let r = last(w), and let px and py be the broadcasters of X and Y . Correct broadcasters set enabled(µX ) = enabled-configs x [r] and enabled(µY ) = enabled-configs y [r]. By lemma 54, the

XX:68

Seamless Reconfiguration for DAG BFT

same logical round cannot be singleton-enabled for two different configurations at correct broadcasters. Applying this fact to X and Y gives Ra = Rb . ◀ ▶ Lemma 56 (All blocks identified as direct anchors or accepted during backward scans for one wave are identical). For every wave w, all blocks that correct processes either identify as a direct anchor for w or accept for w during a backward scan are identical. Proof. Let pi and pj be correct processes. Let B be selected as the coin candidate and then b identified as a direct anchor at pi or accepted there during a backward scan, and define B b analogously at pj . Suppose B and B are obtained using Rl -typed and Rs -typed leader-voting blocks, respectively. A direct anchor identified using Rl -typed blocks has at least ql ≥ fl + 1 distinct Rl -typed leader-voting blocks that reach it. If a backward scan with current anchor Y accepts B, at least fl + 1 distinct Rl -typed leader-voting blocks X satisfy Y ⇝ X ⇝ B. Thus either way of obtaining B provides at least fl + 1 Rl -typed leader-voting blocks. The b All blocks same argument provides at least fs + 1 Rs -typed leader-voting blocks for B. b counted for B lie in round last(w) of DAGi , and all blocks counted for B lie in that same round of DAGj . By DAG-Integrity, distinct blocks within each collection occupy distinct round-broadcaster slots. Hence the two collections satisfy the premises of lemma 55, which gives Rl = Rs . The two candidates are therefore WaveLeaderi (Rl , w) and WaveLeaderj (Rl , w). Thresholdsignature uniqueness implies that any two correct processes that reconstruct the coin for (Rl , w) obtain the same signature and selected member, hence the same round-broadcaster slot in round first(w). DAG-Consistency makes the block occupying that slot unique, so both b Hence all direct-anchor identifications and invocations select the same block and B = B. backward-scan acceptances for wave w select the same block. ◀ By lemma 56, a wave has at most one direct anchor. If wave k has one, denote it by Dk . Thus every backward scan begun from wave k starts with scan anchor Dk . The next lemma is the dynamic counterpart of DAG-Rider’s leader connectivity lemma [15, Lemma 2]. ▶ Lemma 57 (If a direct anchor is identified using Rl -typed leader-voting blocks, every certified last-round block is declared under Rl by an Rl -member). Let w be a wave, and suppose a correct process pd identifies a block Dw as a direct anchor for w using Rl -typed leader-voting blocks. Let r = last(w). For every block B = ⟨m, r, µ, C⟩ such that C is a valid BRB quorum certificate for ⟨m, r, µ⟩ under the configuration declared by µ, local(µ) = Rl

and

ID(µ) ∈ members(Rl ).

In particular, its round-broadcaster slot is (r, ID(µ)), where ID(µ) ∈ members(Rl ). Proof. Put r = last(w). Identifying Dw as a direct anchor gives a set S = {X | X is an Rl -typed leader-voting block for w in DAGd , X ⇝ Dw }

with

|S| ≥ ql .

By the definition of a direct anchor and DAG-Integrity, the blocks counted in S occupy distinct round-broadcaster slots. At most fl of their broadcasters are corrupted, so the set G of correct broadcaster processes represented in S satisfies |G| ≥ ql − fl = nl − 2fl .

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

XX:69

For each pi ∈ G, write Xi = ⟨mi , r, µi , Ci ⟩ for its block in S. Because Xi is Rl -typed, it records enabled(µi ) = {Rl }. Correctness of the broadcaster gives enabled-configs i [r] = {Rl }, so pi issues no round-r BRB vote share for an instance declared under a configuration other than Rl . Suppose, for contradiction, that a valid round-r certificate is declared under Rc ̸= Rl . Since qc > fc , that certificate contains a share from a correct voter pv . The voter applied ValidInstancev (r, µ), and hence Rc ∈ enabled-configs v [r]. Choose any pi ∈ G. Since pi and pv are correct, lemma 54 applies to their round-r enabled-configs values. The value at pi is {Rl }, whereas the value at pv contains Rc ̸= Rl . Hence the latter value must comprise the two configurations of one valid transition: enabled-configs v [r] = {Rl , Rc }. For some process p, the memberships of Rl and Rc are either identical or satisfy members(Rc ) = members(Rl ) ∪ {p}

or

members(Rc ) = members(Rl ) \ {p}.

Consequently, |G∩members(Rc )| ≥

( nl − 2fl ,

members(Rc ) = members(Rl ) or members(Rc ) = members(Rl ) ∪ {p},

nl − 2fl − 1,

members(Rc ) = members(Rl ) \ {p}.

From fc = ⌊(nc − 1)/3⌋, the first lower bound is at least fc + 1 in both the unchangedmembership and addition cases, and the second is at least fc + 1 in the removal case. Thus at least fc + 1 correct members of Rc refuse every Rc -declared instance in round r. At most nc − (fc + 1) = qc − 1 shares remain available, contradicting the assumed valid Rc certificate. Hence every valid round-r certificate is declared under Rl . Finally, let pv be a correct voter whose share occurs in such a certificate declared under Rl ; one exists because ql > fl . Since pv applied ValidInstancev (r, µ), the broadcaster-membership clause gives ID(µ) ∈ members(local(µ)) = members(Rl ). ◀

This proves both claims.

▶ Lemma 58 (Every later-wave block DAG-delivered by a correct process reaches 2fl + 1 distinct blocks broadcast by Rl -members in the direct anchor’s last round). Let w be a wave, and suppose a correct process pd identifies a block Dw as a direct anchor for w using Rl -typed leader-voting blocks. Let r = last(w). Let pi be correct and let Y ∈ DAGi [s] be DAG-delivered by pi , where s belongs to a wave w′ > w. Use HY (r) as the abbreviation for HY,i (r) fixed in the Proof Conventions. Then |HY (r)| ≥ 2fl + 1. For every X = ⟨mX , r, µX , CX ⟩ ∈ HY (r), local(µX ) = Rl

and

ID(µX ) ∈ members(Rl ).

Moreover, the blocks in HY (r) have distinct broadcaster identifiers: for any X, X ′ ∈ HY (r), X ̸= X ′

=⇒

ID(µX ) ̸= ID(µX ′ ).

XX:70

Seamless Reconfiguration for DAG BFT

Proof. We first show that a correct broadcaster remains active through round r + 1 and has an enabled-configs value containing Rl in that round. Let S be the set of Rl -typed leader-voting blocks used to identify the direct anchor. Since |S| ≥ ql > fl , some U ∈ S has a correct broadcaster pu . Because U is Rl -typed and pu is correct, enabled-configs u [r] = {Rl }. The process is active when it produces U . If a correct process invokes InstallTransition with install transition round a for a transition that removes it, algorithm 4 assigns the authenticated pair in rounds a + 1 through a + 4. The process may produce blocks only through round a + 3 and stops before producing a round-(a + 4) block. Since U records the singleton {Rl }, no earlier invocation can make pu stop before it advances from round r to round r + 1. Hence pu remains active through that advancement. If a transition from Rl is underway, this advancement precedes its completion or departure, so corollary 41 advances pu . Otherwise, initialization when l = 1, or conclusion 3 of lemma 47 for the transition into Rl when l > 1, supplies a round reached by every correct Rl -member. Sequential round execution and repeated application of corollary 28 while pu has not invoked InstallTransition for a transition from Rl then supply at least ql correct processes in each round whose prescribed appends reach BRB-Broadcast and advance pu ; if pu invokes InstallTransition first, corollary 41 supplies the remaining advancement. Thus pu eventually advances from round r to round r + 1. Its next enabled-configs value is either {Rl } or {Rl , Rs } for a valid transition Rl → Rs . In either case, Rl ∈ enabled-configs u [r + 1]. Now fix a correct process pz and let Z = ⟨mZ , r + 1, µZ , CZ ⟩ ∈ DAGz [r + 1] be arbitrary. Put Rc = local(µZ ). The valid certificate CZ declared under Rc contains a share from a correct voter pv . The voter applied ValidInstancev (r + 1, µZ ), so Rc ∈ enabled-configs v [r + 1]. Together with the value at pu , lemma 54 implies that either Rc = Rl or Rc = Rs , where either Rl → Rs or Rs → Rl is a valid transition. If the special parent-count rule for a block produced by DAG-Transition-Append does not apply, then |parents(µZ )| = qc : this is ql when Rc = Rl and qs when Rc = Rs . If that special rule applies, the block declares the successor configuration but uses the predecessor’s quorum size. The correct voter then requires its round-(r + 1) enabled-configs value to equal the authenticated pair recorded by µZ . Same-round alignment with the value at pu makes that pair {Rl , Rs }, where either Rl → Rs or Rs → Rl is a valid transition. The parent count is therefore ql , or it is qs for a configuration connected to Rl by one valid transition. In all cases the count is at least 2fl +1. We have ql ≥ 2fl +1. Whenever the qs case occurs, equal memberships give qs = ql . If members(Rs ) = members(Rl ) ∪ {p} for some process p, then qs ≥ ql . If members(Rs ) = members(Rl ) \ {p} for some process p, then qs ∈ {ql , ql − 1}, where the latter is possible only when ql ≥ 2fl + 2. Causal Closure places all distinct parents of Z in the local round-r layer, and Z reaches each of them. Therefore |HZ (r)| ≥ 2fl + 1. The preceding argument proves the base case v = r + 1 for every block DAG-delivered by a correct process. We now prove by induction on v > r + 1 that, for every correct process pa , every block T ∈ DAGa [v] satisfies |HT (r)| ≥ 2fl + 1.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

XX:71

Choose any round-(v − 1) parent P of T . Causal Closure gives P ∈ DAGa [v − 1], so the induction hypothesis yields |HP (r)| ≥ 2fl + 1. Since T ⇝a P , causal transitivity gives HP (r) ⊆ HT (r), and hence |HT (r)| ≥ 2fl + 1. If s = r + 1, the base case gives the claim for Y . If s > r + 1, take pa = pi and v = s in the induction. Thus the bound holds for Y in all cases. Every X ∈ HY (r) is DAG-delivered at pi and therefore carries a valid certificate. Applying lemma 57 gives local(µX ) = Rl

and

ID(µX ) ∈ members(Rl ).

Finally, if two blocks X, X ′ ∈ HY (r) had the same broadcaster identity, they would occupy the same round-broadcaster slot. DAG-Integrity at pi then gives X = X ′ . Thus distinct blocks in HY (r) have distinct broadcaster identities. ◀ ▶ Lemma 59 (The causal history of every later-wave block contains fl + 1 leader-voting blocks that reach the earlier direct anchor). Let w be a wave, and suppose a correct process pd identifies a block Dw as a direct anchor for w using Rl -typed leader-voting blocks. Let pi be any correct process, and let Y be a block DAG-delivered by pi whose round belongs to a wave w′ > w. Then DAGi contains at least fl + 1 Rl -typed leader-voting blocks X for wave w, with pairwise distinct broadcaster identities, such that Y ⇝i X ⇝i Dw . Proof. Put r = last(w), and let S be the set of at least ql Rl -typed leader-voting blocks that reach Dw in the definition of a direct anchor. Define IS = {ID(µX ) | X = ⟨mX , r, µX , CX ⟩ ∈ S} , IY = {ID(µX ) | X = ⟨mX , r, µX , CX ⟩ ∈ HY (r)} . The direct-anchor test counts distinct round-broadcaster slots, so |IS | ≥ ql . By lemma 58, |IY | ≥ 2fl + 1. Both sets are subsets of members(Rl ), which has size nl . Therefore |IS ∩ IY | ≥ |IS | + |IY | − nl ≥ (nl − fl ) + (2fl + 1) − nl = fl + 1. For each identity in this intersection, S and HY (r) contain a block in the same roundbroadcaster slot. DAG-Consistency makes those two blocks identical. Hence at least fl + 1 blocks lie in S ∩ HY (r), and every such block X satisfies Y ⇝i X ⇝i Dw . Their broadcaster identities are pairwise distinct by construction.

◀

▶ Corollary 60 (A later backward scan accepts an earlier direct anchor). Suppose Dw is a direct anchor identified using Rl -typed leader-voting blocks. Let a backward scan at a correct process pi have current anchor Y , where Y belongs to a wave later than w. Then the scan accepts Dw when it reaches wave w. Proof. Causal Closure gives the scanning process Dw , the fl + 1 distinct Rl -typed leadervoting blocks from lemma 59, and their coin shares. These blocks satisfy the backward-scan acceptance condition for Dw , so the process reconstructs the unique coin for (Rl , w) and obtains WaveLeaderi (Rl , w) = Dw . By lemma 56, it cannot accept a different block for wave w. ◀

XX:72

Seamless Reconfiguration for DAG BFT

B.2.3

Backward Scans, Finalized Leader Sequences, and Total Order

Deterministic Backward Scans and Prefix-Comparable Leader Sequences. For a wave k with direct anchor Dk and a correct process pi with Dk ∈ DAGi , define Φi,k by a conceptual, read-only execution of the backward-scan rule in Electi . Initialize the temporary sequence to ⟨Dk ⟩ and the scan anchor to Dk , and apply the same acceptance test to waves k − 1, k − 2, . . . , 1. Unlike an actual invocation, this full scan ignores processed-wave i and does not modify any persistent state. ▶ Lemma 61 (Full backward scans rooted at the same direct anchor produce the same leader sequence). Let k be a wave with direct anchor Dk . For any correct processes pi and pj , evaluate Φi,k and Φj,k at arbitrary local states in which Dk ∈ DAGi and Dk ∈ DAGj , respectively. Then Φi,k = Φj,k . Thus the full backward scan rooted at Dk is independent of both the correct process executing it and any blocks outside Dk ’s causal history that are delivered later. Proof. Fix a wave w < k and a scan anchor Y stored by correct processes pi and pj . By DAG-Consistency and Causal Closure, both store the same causal history of Y , including its blocks, metadata, certificates, coin shares, and parent references. Although WaveConfigsx (w), Sharesx (Rc , w), and WaveLeaderx (Rc , w) inspect all of DAGx for x ∈ {i, j}, the backward-scan candidate set depends only on Y ’s causal history. To see this, suppose Rc contributes a candidate at pi : B ′ = WaveLeaderi (Rc , w) ̸= ⊥,

HistorySupporti (Y, B ′ , Rc , w) ≥ fc + 1.

The counted leader-voting blocks have distinct broadcaster identities and satisfy Y ⇝ X ⇝ B ′ . Hence these blocks, their valid coin shares, and B ′ itself all lie in Y ’s causal history and are stored by pj . The shares suffice to reconstruct the coin for (Rc , w). Threshold-signature uniqueness gives the same selected round-broadcaster slot, and DAGConsistency gives the same block B ′ in that slot. Thus WaveLeaderj (Rc , w) = B ′ . The values HistorySupporti (Y, B ′ , Rc , w) and HistorySupportj (Y, B ′ , Rc , w) are equal because both count exactly the same identities in the shared causal history of Y . Therefore Rc contributes the same candidate at pj . Applying this argument in both directions shows that the candidate sets are identical. The argument applies to arbitrary local states containing Y , including states before and after later deliveries at one process. In particular, a block outside Y ’s causal history has history support zero, while any candidate meeting the threshold already has enough coin shares in that history. Later deliveries therefore cannot change the candidate set. Finally, a contributing configuration Rc supplies at least fc + 1 Rc -typed leader-voting blocks in distinct round-broadcaster slots. By lemma 55, at most one configuration can contribute a candidate for wave w. The candidate set is therefore either empty or the same singleton at every correct process storing Y . A fixed scan anchor consequently gives the same accept-or-skip decision and, upon acceptance, the same next anchor. Since both full backward scans start at Dk , induction over descending wave numbers gives Φi,k = Φj,k . ◀ By lemma 61, denote the common sequence Φi,k by Φk .

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

▶ Lemma 62 (The leader sequence from an earlier direct anchor is a prefix of the sequence from a later direct anchor). Write ⪯ for the prefix relation. If h < k are waves with direct anchors, then Φh ⪯ Φk . Proof. Now let h < k be waves with direct anchors. When the full backward scan rooted at Dk reaches wave h, its scan anchor belongs to a wave whose index is greater than h. By corollary 60, the scan accepts Dh and sets its anchor to Dh . Every subsequent decision below h is then identical to the full backward scan rooted at Dh . Since earlier leaders are prepended, Φh is a prefix of Φk . ◀ Set Φ0 = ⟨⟩. By lemma 62, Φ0 and all sequences Φk for waves k with direct anchors are nested under the prefix relation. Hence there is a unique finite or infinite sequence Φ for which every Φk is a prefix and whose elements are exactly those appearing in the Φk . We call Φ the canonical leader sequence. Every finite prefix of Φ is a prefix of some Φk , or is empty if no direct anchor exists. ▶ Lemma 63 (Every correct process’s finalized leader sequence is always a canonical leader prefix). After initialization, at every local state of a correct process pi , finalized-values i is Φ0 or Φk for some wave k with a direct anchor. Immediately after a serialized invocation of Electi returns, let v = 0 if no invocation Electi (Dx , x) has completed at pi for any wave x; otherwise, let v be the greatest wave index x for which such an invocation has completed. Then finalized-values i = Φv , where either v = 0 or v is a wave with a direct anchor. Proof. Induct on the serialized Electi invocations. Initially no Electi invocation has completed and finalized-values i = Φ0 . After initialization, Electi is the only procedure that modifies this sequence. Assume the claim holds immediately before a serialized invocation Electi (Dk , k), and let v be the greatest wave for which an Electi invocation has completed, or 0 if there is none. Wave k has a direct anchor because the procedure is invoked only after pi identifies Dk as one. If k ≤ v, the invocation returns without changing the sequence. The greatest completed wave remains v, and the sequence remains Φv . Suppose instead that k > v. If v = 0, the invocation executes exactly the full backward scan defining Φk and changes the finalized leader sequence to Φk . If v > 0, the induction hypothesis gives finalized-values i = Φv , and wave v has a direct anchor. The invocation performs exactly the iterations of the full backward scan for Φk above wave v. When that full backward scan reaches v, corollary 60 makes it accept Dv , after which its decisions below v produce Φv . Since Φv ⪯ Φk , there is a unique suffix Ψ such that Φk = Φv · Ψ. The invocation appends exactly Ψ, changing the finalized leader sequence from Φv to Φk . In the case k > v, wave k is the greatest argument of a completed Electi invocation when the call returns. During an invocation, the finalized leader sequence is unchanged before its single append; immediately afterward it is already the next canonical leader prefix. Thus the invariant holds at every local state. ◀ ▶ Corollary 64 (Every active correct process finalizes at most one block per wave, never finalizes a block twice, and finalizes only blocks already in its DAG). For every wave w and active correct process pi , finalized-values i contains at most one block from w and contains no block more than once. Every block in the sequence has already been inserted into the process’s local DAG.

XX:73

XX:74

Seamless Reconfiguration for DAG BFT

Proof. Each backward scan visits a wave at most once, and an invocation for a later direct anchor scans only waves whose indices exceed the greatest wave already processed. Together with lemma 56, this lets a correct process pi append at most one leader for each wave. Serialization in algorithm 9 prevents concurrent invocations from duplicating that output. Every appended block was returned by WaveLeaderi (Rl , w) for some configuration Rl and wave w. By its definition, every non-⊥ return is a locally available first-round DAG block and has therefore already been inserted into DAGi . Thus every candidate for wave w belongs to round first(w). Distinct waves have distinct first rounds, so the same block cannot be selected for two different waves. Thus all requirements of Integrity in definition 2 hold. ◀ ▶ Theorem 65 (Finalized leader sequences at active correct processes are always prefix-comparable). At every time, the finalized leader sequences of any two active correct processes are prefix-comparable. Consequently, if the sequence of an active correct process pi contains a block B before a distinct block B ′ , then the sequence of every active correct process pj that contains B ′ also contains B before B ′ . Proof. By lemma 63, at every point each correct process’s finalized leader sequence is a canonical leader prefix. By lemma 62, all canonical leader prefixes are pairwise comparable under ⪯. Both local sequences are prefixes of Φ. Since B precedes B ′ in Φ, every prefix containing B ′ contains all earlier elements of Φ, including B. This is exactly the stated total-order property. ◀

B.3 B.3.1

Probabilistic Progress Progress After Stabilization at RL

Eventual Stability. ▶ Corollary 66 (After some round, every correct RL -member that remains active enables only RL , and every certificate is declared under RL ). There exist a final configuration RL and a round r⋆ such that every correct process pi ∈ members(RL ) that remains active has installed RL and, for every round r ≥ r⋆ that it executes, enabled-configs i [r] = {RL }. Every certified block in a round r ≥ r⋆ is declared under RL and has a broadcaster identity in members(RL ). Proof. Finiteness of the reconfiguration sequence gives a final configuration RL . If L = 1, then RL = R1 is installed at initialization. If L > 1, the transition into RL completes by lemma 49. In either case, no later reconfiguration message exists. Assume first that L > 1. For every earlier configuration Rc , only members of members(Rc ) can vote for a certificate declared under Rc . Completion of the transition out of each Rc gives a finite logical-round cutoff ρc beyond which no correct member of Rc assigns an enabledconfigs value containing Rc . For c ≤ L − 2, this follows from lemma 18. For c = L − 1, every correct retained old member has a finite install transition round ai by lemma 49, and every correct removed old member has one by lemma 43. An invocation with install transition round ai assigns values containing RL−1 only through round ai + 4; afterward a retained member assigns only {RL }, while a removed member executes no later protocol rounds after its permitted departure. Taking the maximum of these finitely many bounds gives ρL−1 . Because every configuration is finite, one cutoff suffices for all of its correct members.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

Completion of the transition into RL also gives a finite cutoff beyond which every correct RL -member that remains active has installed RL and assigns only {RL }. When L > 1, choose r⋆ larger than these finitely many logical-round cutoffs. When L = 1, take r⋆ = 1; initialization and the absence of a later configuration imply that every enabled-configs value assigned by a correct process is {R1 }. In either case, every correct process pi ∈ members(RL ) that remains active then assigns enabled-configs i [r] = {RL }

for every round r ≥ r⋆ that it executes.

A certificate in round r ≥ r⋆ declared under an earlier configuration Rc would require qc > fc votes and hence a vote from a correct process whose round-r enabled-configs value contains Rc , which is impossible above the chosen cutoff. Since no later configuration exists, every certificate in a round r ≥ r⋆ is declared under RL . The BRB broadcaster-membership check then restricts it to one of the nL round-broadcaster slots of RL . ◀ ▶ Corollary 67 (Every correct RL -member that remains active completes every round r ≥ r⋆ ). Under the conclusion of corollary 66, for every correct process pi ∈ members(RL ) that remains active and every r ≥ r⋆ , process pi eventually DAG-delivers at least qL admissible round-r blocks in ParentBlocksi (RL , r), completes round r, and enters round r + 1. Proof. If L = 1, take r0 = 1; every active correct process in members(R1 ) enters that round, and at least qL of them invoke the prescribed append and reach its parent-free BRB-Broadcast call. If L > 1, lemma 48 supplies the induction hypothesis for RL−1 , and the third conclusion of lemma 47, applied to RL−1 → RL , supplies such a round r0 . Because the conclusion of corollary 66 remains true when its cutoff is increased, replace r⋆ by max{r⋆ , r0 }. BRB Agreement for every round-broadcaster slot from lemma 50 supplies the Agreement premise of corollary 28. We now induct on rounds r ≥ r0 . The invariant is that every correct RL -member that remains active eventually enters round r, and at least qL active correct RL -members invoke the prescribed round-r DAG-Append operation and reach its BRB-Broadcast call. The choice of r0 gives the base case. For the induction step, apply lemma 27 to those qL broadcasters. Every correct RL -member that remains active eventually DAG-delivers at least qL admissible round-r blocks in distinct broadcaster slots and hence satisfies |ParentBlocksi (RL , r)| ≥ qL . By corollary 28, every such process then completes round r and enters round r + 1. At least qL correct members remain active by the assumption in Section 3 that at least qL correct members of RL remain active, and each invokes its prescribed append upon entering round r + 1. Its ordinary entry condition supplies the same round-r parents on which that append waits, so the append reaches BRB-Broadcast and establishes the invariant for the next round. The induction first brings every correct RL -member that remains active to r⋆ and then proves the claim for every round r ≥ r⋆ . ◀

B.3.2

A Common Core in Every Stable Wave

Following the terminology of DAG-Rider [15], a set Kw is a common core of a stable wave w if it contains exactly qL certified blocks declared under RL in distinct round-broadcaster slots of round first(w) and, for every correct process pi and every block Y ∈ DAGi [last(w)], Y ⇝i B

for every B ∈ Kw .

XX:75

XX:76

Seamless Reconfiguration for DAG BFT

The next lemma proves that the blocks’ fixed parent sets determine such a common core before valid shares have been released by fL + 1 distinct broadcasters. The following corollary proves that every correct RL -member that remains active eventually DAG-delivers it. ▶ Lemma 68 (Before fL + 1 distinct broadcasters release valid coin shares, fixed parent sets determine a common core). Assume that every correct broadcaster that produces a singletonenabled last-round block releases its prescribed valid coin share in that block. Also assume that a broadcaster that is uncorrupted when it releases such a share fixes the block’s parents before generating the share, and that those parents cannot later change. Fix a stable wave w under RL with first(w) ≥ r⋆ from corollary 66, and write rk = first(w) + k − 1 for k ∈ {1, 2, 3, 4}. Before valid coin shares for (RL , w) have been released by fL + 1 distinct broadcaster identities, the fixed parent sets determine a set Kw of exactly qL certified round-r1 blocks declared under RL in distinct round-broadcaster slots. Moreover, for every correct process pi and every Y ∈ DAGi [r4 ], Kw ⊆ DAGi [r1 ]

and

Y ⇝i B

for every B ∈ Kw .

Thus Kw is a common core of w. Proof. By corollary 66, every certified block in rounds r1 , r2 , r3 , r4 is declared under RL . Correct voters in rounds r2 , r3 , r4 use the ordinary parent-count rule, since their enabledconfigs value is {RL }. Consequently, every block in rounds r2 , r3 , r4 that is DAG-delivered by a correct process has exactly qL parents in distinct round-broadcaster slots of the preceding round, with broadcaster identities in members(RL ). By corollary 67 and the assumption that every correct broadcaster producing a singletonenabled last-round block releases its prescribed valid coin share in that block, at least qL ≥ fL + 1 active correct broadcasters eventually release such shares. Consider all validshare release events for (RL , w), including events at Byzantine broadcasters, in the order chosen by the adversarial scheduler. Among the first fL + 1 distinct broadcasters, at least one is uncorrupted when its release occurs. Let X be the round-r4 block for the first such release. Because X’s broadcaster is uncorrupted when it releases the share, the second assumption in the lemma statement ensures that X’s qL round-r3 parents are already fixed before its share is generated and released. Immediately before that release, fewer than fL + 1 distinct valid shares have been released. Denote X’s fixed parent set by PX . Each block in PX is certified, so its metadata, including its parents, cannot later change; the same holds recursively for its certified ancestors. 2 There are qL pairs (Z, H ′ ) such that Z ∈ PX and H ′ is a round-r2 parent of Z. These pairs involve at most nL round-r2 broadcaster slots. Therefore, some round-r2 slot contains a parent of at least fL + 1 blocks in PX , because 2 qL f2 = nL − 2fL + L ≥ fL + 1, nL nL

where the final inequality follows from nL ≥ 3fL + 1. Among the qualifying slots, choose the one whose broadcaster appears first in the ordered list ΠL , and let H be its unique certified block. This choice depends only on the already fixed set PX . Let W = {Z ∈ PX : H is a parent of Z}. Uniqueness follows from BRB Agreement for every round-broadcaster slot in lemma 50, and |W| ≥ fL + 1. Define Kw to be the qL round-r1 parents of H. Thus Kw is fixed before the (fL + 1)-st distinct valid share for (RL , w) is released.

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

XX:77

Now consider any Y ∈ DAGi [r4 ] at a correct process pi . Its qL round-r3 parent slots intersect the at least fL + 1 slots occupied by W, since qL + |W| ≥ qL + (fL + 1) = nL + 1, and each set uses distinct broadcaster slots. Let Z ∈ W occupy a slot that also occurs among the parent slots of Y . The parent of Y in that slot and Z are in the same round-broadcaster slot, so BRB Agreement implies that they are the same block. Since H is a parent of Z, for every B ∈ Kw , Y ⇝i Z ⇝i H ⇝i B. Causal Closure places Z, H, and every block in Kw in DAGi , completing the proof.

◀

▶ Corollary 69 (Every correct RL -member that remains active eventually DAG-delivers the same common core and at least qL distinct leader-voting blocks that reach every block in it). Fix a stable wave w satisfying the premises of lemma 68, let r4 = last(w), and let Kw be the common core determined by that lemma. Every correct process pi ∈ members(RL ) that remains active eventually DAG-delivers every block in Kw and at least qL distinct RL -typed leader-voting blocks Y such that Y ⇝i B

for every B ∈ Kw .

Thus the same common core Kw is eventually present in the DAG of every correct RL -member that remains active. Proof. Choose any qL correct RL -members that remain active; their existence is guaranteed by the assumption in Section 3 that at least qL correct members of RL remain active. Corollary 67 brings them to round r4 . Upon entering that round, each selected process produces its prescribed block. Here r4 = last(w), and stability gives local(µ) = RL and enabled(µ) = {RL }. The first assumption of lemma 68 says that every correct broadcaster producing such a block releases its prescribed valid RL -scoped coin share in that block. Thus the resulting qL blocks are RL -typed leader-voting blocks in distinct slots. By lemma 23, for every selected broadcaster pk , every correct RL -member belongs to known k . The required broadcasters, processes that send BRB echoes and votes, and recipients remain active and continue the prescribed tasks in the stable suffix. For each application, take G to be these selected qL broadcasters. Therefore BRB Agreement through round r4 follows from lemma 50. Then lemma 25, applied to each selected broadcaster, makes every correct RL -member that remains active eventually DAG-deliver all qL blocks. The conclusion now follows from lemma 68 and Causal Closure. ◀

B.3.3

Direct-Anchor Recurrence and Progress

Conditional Probability Requirement. For sufficiently large security parameter λ, put εL =

qL − negl(λ) > 0. nL

Since qL = nL − fL and nL ≥ 3fL + 1, this is at least 2/3 − negl(λ). To prove Probabilistic Progress with probability one, we make the following additional requirement. For every stable wave w satisfying the premises of lemma 68, let Kw be the

XX:78

Seamless Reconfiguration for DAG BFT

common core determined by that lemma. Consider any finite execution prefix at whose end Kw has been fixed but fewer than fL + 1 distinct valid shares for (RL , w) have been released. For every adversary view occurring with positive probability at the end of such a prefix, conditioned on that view, the probability that the coin selects the broadcaster of a block in Kw is at least εL . The construction in lemma 68 determines Kw from parent sets already fixed at that point. The adversary’s view includes all earlier scheduling decisions and coin outcomes. Thus the same positive lower bound holds after every possible prior history, including any pattern of failures in earlier stable waves; coin outcomes in different waves need not be independent. For a concrete computational implementation, Unpredictability instead bounds the overall failure probability across any polynomially bounded number of waves, up to negligible error. It does not by itself imply this conditional bound after every finite execution prefix. ▶ Proposition 70 (With probability at least εL , every correct RL -member that remains active identifies a direct anchor in wave w or later). Let w be a stable wave satisfying the premises of lemma 68, and let Kw be the common core determined by that lemma. Suppose that, conditioned on the adversary’s current view after any finite execution prefix ending after Kw is fixed and before the (fL + 1)-st distinct valid share for (RL , w) is released, the coin selects the broadcaster of a block in Kw with probability at least εL . Then, after every such prefix, with conditional probability at least εL , every correct process pi ∈ members(RL ) that remains active eventually identifies a direct anchor in wave w or in a later wave. Proof. By lemma 68, Kw occupies exactly qL of the nL round-broadcaster slots and is fixed before the (fL + 1)-st distinct valid share for (RL , w) is released. By the probability bound in the proposition statement, the coin selects the broadcaster of some B ∈ Kw with probability at least εL . On this event, corollary 69 makes every correct RL -member pi that remains active DAGdeliver B and at least qL ≥ fL + 1 leader-voting blocks carrying valid shares and reaching B. From any fL + 1 of these valid shares, pi reconstructs the coin for (RL , w). Its output is B’s broadcaster, and pi has DAG-delivered B, so WaveLeaderi (RL , w) returns B. When the last of these qL leader-voting blocks arrives, the protocol rechecks w and identifies B as its direct anchor, unless pi has already identified an anchor in a later wave. Either case gives the conclusion. ◀ ▶ Lemma 71 (Every correct RL -member that remains active identifies direct anchors in arbitrarily late stable waves with probability one). Let RL and r⋆ be as in corollary 66. Assume that the premises of lemma 68 hold for every stable wave w under RL with first(w) ≥ r⋆ . For each such wave, let Kw be the common core determined by that lemma. Also assume that, for every such wave, conditioned on the adversary’s current view after any finite execution prefix ending after Kw is fixed and before the (fL + 1)-st distinct valid share for (RL , w) is released, the coin selects the broadcaster of a block in Kw with probability at least εL . Then, over the configuration-scoped perfect coins, with probability one, for every correct process pi ∈ members(RL ) that remains active and every wave index b ≥ 1, there exists a stable wave h ≥ b in which pi identifies a direct anchor. Proof. By corollary 67, every correct RL -member that remains active advances through all rounds of infinitely many stable waves. In every such wave w, at least qL ≥ fL + 1 correct broadcasters release valid shares, which are sufficient to reconstruct the coin for (RL , w). Fix any starting wave index b. When each common core is determined, the adversary’s view includes all preceding coin outcomes. Averaging the conditional lower bound over views in

M. Y. Hu, L. Jehl, P. Franke-Bergmann, J. Li, and C. Berger

which the coins in earlier stable waves with indices at least b did not select a broadcaster from their respective common cores shows that the next coin selects such a broadcaster with conditional probability at least εL > 0. Thus the conditional-probability chain rule gives, for every N ≥ 1,   in none of the first N stable waves h ≥ b does the coin ≤ (1 − εL )N . Pr for (RL , h) select the broadcaster of a block in Kh As N tends to infinity, the right-hand side tends to zero. Hence the probability that no stable wave h ≥ b has this property is zero. Taking the countable union over starting wave indices b shows that, with probability one, the coin selects a broadcaster from the common core in arbitrarily late stable waves. Whenever this occurs in a wave h, proposition 70 shows that every correct RL -member that remains active identifies a direct anchor in wave h or a later wave. ◀ ▶ Theorem 72 (Probabilistic Progress). Let RL and r⋆ be as in corollary 66, and suppose that the two premises of lemma 68 hold in every stable wave w with first(w) ≥ r⋆ . Also suppose that the conditional probability premise of lemma 71 holds for every such wave. With probability one, every correct RL -member that remains active finalizes infinitely many blocks. Proof. Fix a correct RL -member pi that remains active and any wave index b. By lemma 71, pi eventually identifies a direct anchor in some wave h ≥ b. Its serialized Electi invocation either changes its finalized leader sequence to Φh , which contains that direct anchor, or an invocation for some later wave s ≥ h has already changed the sequence to Φs . In the latter case, Φh ⪯ Φs by lemma 62, so the sequence still contains the wave-h anchor. Because b is arbitrary and direct anchors in distinct waves are distinct blocks, the lengths of pi ’s finalized leader sequences are unbounded. Hence pi finalizes infinitely many blocks with probability one. ◀

B.4

Dynamic DAG Byzantine Atomic Broadcast

The probability-one Probabilistic Progress conclusion in the following restatement uses the conditional probability bound in Section B.3. The deterministic Integrity and Total Order conclusions do not use the Unpredictability or Fairness properties of the configuration-scoped perfect coin. ▶ Theorem 3 (Correctness of Dynamic DAG Byzantine Atomic Broadcast). Under the model of Section 3, suppose that the dealer follows the issuance rule of Section 4.2. For Probabilistic Progress, also assume the conditional probability requirement of Section B.3. For every finite sequence of reconfiguration messages, with no a priori bound on its length, the protocol of Section 4 implements the leader-level Dynamic DAG Byzantine Atomic Broadcast of definition 2. Proof. We verify each component of the abstraction: Underlying Dynamic DAG-structured Byzantine Broadcast. By lemma 51, the BRB, DAG, state-transfer, and reconfiguration protocols satisfy definition 1, including completion of every valid transition. Integrity. By corollary 64, a correct process finalizes at most one leader from each wave, never inserts the same block twice in its finalized leader sequence, and finalizes only blocks already inserted in its local DAG. These are exactly the Integrity clauses of definition 2. Total Order. The canonical leader prefixes are nested by lemmas 62 and 63; hence theorem 65 gives Total Order throughout every transition, independently of eventual stability.

XX:79

XX:80

Seamless Reconfiguration for DAG BFT

Probabilistic Progress. By corollaries 66 and 67, the execution eventually has infinitely many stable waves under RL . As required by Section 4, every correct broadcaster of a singleton-enabled last-round block releases its prescribed valid coin share, and every broadcaster that is uncorrupted when releasing such a share fixes the block’s parents before generating and releasing the share. These are precisely the two premises of lemma 68. The conditional probability bound assumed by the theorem supplies the remaining premise of lemma 71. Hence theorem 72 gives Probabilistic Progress as defined in definition 2. ◀

Related documents

• Seamless Reconfiguration for DAG-BFT#1155831
• Algorithms for synchronizing network clocks#213377
• State of Peer-to-Peer (P2P) Communication across Network Address Translators (NATs)#420319
• CLASP: Chained-Request-Aware Scaling and Operator Placement for Serverless Stream Processing#793326
• CLASP: Chained-Request-Aware Scaling and Operator Placement for Serverless Stream Processing#789322