# Generalized Paxos Made Byzantine
## 5 Byzantine Fault Tolerant Protocol
### Agreement Protocol
This is encoded in the logical expression \(s\bullet\sigma_{1}\sim x\bullet\sigma_{2}\) which is true if the accepted sequence \(s\) and any other sequence \(x\) can be extended to an equivalent sequence, therefore making it impossible to result in a conflict. At any given instant, \(\forall s,s^{\prime}\in\mathcal{P},\forall b,b^{\prime}\in\mathcal{B},maj\_ accepted(s,b)\wedge maj\_accepted(s^{\prime},b^{\prime})\implies \exists\sigma_{1},\sigma_{2}\in\mathcal{P}\cup\{\bot\},s\,\bullet\sigma_{1} \sim s^{\prime}\bullet\sigma_{2}\)

**Proof:** We divide the following proof in two main cases: (1.2.1.) sequences \(s\) and \(s^{\prime}\) are accepted in the same ballot \(b\) and (1.2.2.) sequences \(s\) and \(s^{\prime}\) are accepted in different ballots \(b\) and \(b^{\prime}\). 1.2.1. At any given instant, \(\forall s,s^{\prime}\in\mathcal{P},\forall b\in\mathcal{B},maj\_accepted(s,b) \wedge maj\_accepted(s^{\prime},b)\implies\exists\sigma_{1},\sigma_{2}\in \mathcal{P}\cup\{\bot\},s\,\bullet\sigma_{1}\sim s^{\prime}\bullet\sigma_{2}\)

**Proof:** Proved by contradiction. 1.2.1.1. At any given instant, \(\forall s,s^{\prime}\in\mathcal{P},\forall\sigma_{1},\sigma_{2}\in\mathcal{P} \cup\{\bot\},\forall b\in\mathcal{B},maj\_accepted(s,b)\wedge maj\_ accepted(s^{\prime},b)\wedge s\bullet\sigma_{1}\
ot\sim s^{\prime}\bullet\sigma_{2}\)

**Proof:** Contradiction assumption. 1.2.1.2. Take a pair proposals \(s\) and \(s^{\prime}\) that meet the conditions of 1.2.1 (and are certain to exist by the previous point), then \(s\) and \(s^{\prime}\) contain non-commutative commands. **Proof:** The statement \(\forall s,s^{\prime}\in\mathcal{P},\forall\sigma_{1},\sigma_{2}\in\mathcal{P} \cup\{\bot\},s\,\bullet\sigma_{1}\
ot\sim s^{\prime}\bullet\sigma_{2}\) is trivially false because it implies that, for any combination of sequences and suffixes, the extended sequences would never be equivalent. Since there must be some \(s,s^{\prime},\sigma_{1}\) and \(\sigma_{2}\) for which the extensions are equivalent (e.g., \(s=s^{\prime}\) and \(\sigma_{1}=\sigma_{2}\)), then the statement is false. 1.2.1.3. A contradiction is found, Q.E.D. 1.2.2. At any given instant, \(\forall s,s^{\prime}\in\mathcal{P},\forall b,b^{\prime}\in\mathcal{B},maj\_ accepted(s,b)\wedge maj\_accepted(s^{\prime},b^{\prime})\wedge b\
eq b^{ \prime}\implies\exists\sigma_{1},\sigma_{2}\in\mathcal{P}\cup\{\bot\},s\, \bullet\sigma_{1}\sim s^{\prime}\bullet\sigma_{2}\)

**Proof:** To prove that values accepted in different ballots are extensible to equivalent sequences, it suffices to prove that for any sequences \(s\) and \(s^{\prime}\) accepted at ballots \(b\) and \(b^{\prime}\), respectively, such that \(b<b^{\prime}\) then \(s\sqsubseteq s^{\prime}\). By Algorithm 9 lines [11-16, 15, 16, 13, 46, 35, 46], any correct acceptor only votes for a value in variable \(val_{a}\) when it receives \(2f+1\) proofs for a matching value. Therefore, we prove that a value \(val_{a}\) that receives \(2f+1\) verification messages is always an extension of a previous \(val_{a}\) that received \(2f+1\) verification messages. By Algorithm 9 lines [32, 43], \(val_{a}\) only changes when a leader sends a proposal in a classic ballot or when a proposer sends a sequence in a fast ballot. In the first case, \(val_{a}\) is substituted by the leader's proposal which means we must prove that this proposal is an extension of any \(val_{a}\) that previously obtained \(2f+1\) verification votes. By Algorithm 7 lines [24-39, 41-47], the leader's proposal is prefixed by the largest of the proven sequences (i.e., \(val_{a}\) sequences that received \(2f+1\) votes in the verification phase) relayed by a quorum of acceptors in _phase 1b_ messages. Please note that, the verification in Algorithm 9 line [27] prevents a Byzantine leader from sending a sequence that is not an extension of previous proved sequences.