` 26 D. Mazieres hence vote to confirm) contradictory statements, this means that for a given ⟨V,Q⟩, Theorem 5 ensures a set S of well-behaved nodes cannot externalize contradictory values so long as S enjoys quorum intersection despite V⧵S. This safety holds if V and Qchangeonlybetweenslots,butwhatiftheychangemid-slot(forinstance,inreaction to node crashes)? To reason about safety under reconfiguration, we join all old and new quorum slice sets, reflecting the fact that nodes may make decisions based on a combination of mes- sages from different configuration eras. To be very conservative, we might require quorum intersection of the aggregation of the present configuration with every past configuration. However, we can relax this slightly by separating nodes that have sent illegal messages from those that have merely crashed. THEOREM13. Let ⟨V ,Q ⟩,…,⟨V ,Q ⟩ be the set of configurations an FBAS has 1 1 k k experienced during agreement on a single slot. Let V = V ∪ ⋯ ∪ V and Q(v) = {q ∣ 1 k ∃j such that v ∈ V ∧ q ∈ Q (v)}. Let B ⊆ V be a set such that B contains all ill- j j behaved nodes that have sent illegal messages, though V⧵B may still contain crashed (unresponsive) nodes. Suppose nodes v and v are well-behaved, v externalizes x for 1 2 1 1 the slot, and v externalizes x . If ⟨V,Q⟩B enjoys quorum intersection, then x = x . 2 2 1 2 PROOF. For v to externalize x , it must have ratified accept(commit ⟨n ,x ⟩) in col- 1 1 1 1 laboration with a pseudo-quorum U ⊆ V. We say pseudo-quorum because U might 1 1 not be a quorum in ⟨V ,Q ⟩ for any particular j, as ratification may have involved j j messages spanning multiple configurations. Nonetheless, for ratification to succeed ∀v ∈ U ,∃j,∃q ∈ Q (v) such that q ⊆ U . It follows from the construction of Q that 1 j 1 q ∈ Q(v). Hence U is a quorum in ⟨V,Q⟩. By a similar argument a pseudo-quorum 1 U musthave ratified accept(commit ⟨n ,x ⟩), and U must be a quorum in ⟨V,Q⟩. By 2 2 2 2 B quorumintersection of ⟨V,Q⟩ , there must exist some v ∈ V⧵B such that v ∈ U ∩U . 1 2 By assumption, such a v ∉ B could not claim to accept incompatible ballots. Since v confirmedacceptingcommitforballotswithbothx andx ,itmustbethatx =x . 1 2 1 2 For liveness of a node v, we care about several things when an FBAS has undergone a series of reconfigurations ⟨V ,Q ⟩,…,⟨V ,Q ⟩ within a single slot. First, the safety 1 1 k k prerequisites of Theorem 13 must hold for v and the set of nodes v cares about, since violating safety undermines liveness and Theorem 11 requires quorum intersection. Second,thesetofill-behavednodesinthelateststate,⟨V ,Q ⟩,mustnotbev-blocking, k k as this could deny v a quorum and prevent it from ratifying statements. Finally, v’s state must never have been poisoned by a v-blocking set falsely claiming to accept a statement. To summarize, then, if B is the set of nodes that have sent illegal messages, we consider a node v to be cumulatively intact when the following conditions hold: (1) v is intact in the latest configuration ⟨V ,Q ⟩, k k (2) The aggregation of the present and all past configurations has quorum intersec- tion despite B (i.e., the prerequisite for Theorem 13 holds), and (3) B is not v-blocking in ⟨V ,Q ⟩ for any 1 ≤ j ≤ k. j j The next few theorems show that ill-behaved nodes cannot drive intact nodes into dead-end stuck states: THEOREM14. In an FBAS with quorum intersection, if no intact node is in the EXTERNALIZE phase and an intact node with ballot ⟨n,x⟩ arms its timer as described in Section 6.2.2, then, given sufficient communication, every intact node v can set bv ≥ n before any timer fires.
The Stellar Consensus Protocol Page 26 Page 28