# Generalized Paxos Made Byzantine
## 5 Byzantine Fault Tolerant Protocol
### Agreement Protocol
Since the verification phase prevents non-commutative sequences from being accepted by a quorum, every proven sequence in a ballot is extensible to equivalent sequences which means that the largest proven sequence is simply the most up-to-date sequence of the previous ballot. To prove that the leader can only propose extensions to previous values by picking the largest proven sequence as its proposal's prefix, we need to assert that a proven sequence is an extension of any previous sequence. However, since that is the same result that we are trying to prove, we must use induction to do so:

**1. Base Case**: In the first ballot, any proven sequence will be an extension of the empty command \(\bot\) and, therefore, an extension of the previous sequence. **2. Induction Hypothesis**: Assume that, for some ballot \(b\), any sequence that gathers \(2f+1\) verification votes from acceptors is an extension of previous proven sequences. **3. Inductive Step**: By the quorum intersection property, in a classic ballot \(b+1\), the _phase 1b_ quorum will contain ballot \(b^{\prime}\)s proven sequences. Given the largest proven sequence \(s\) in the _phase 1b_ quorum (which, by our hypothesis, is an extension of any previous proven sequences), by picking \(s\) as the prefix of its _phase 2a_ proposal (Algorithm 7, lines [41-47]), the leader will assemble a proposal that is an extension of any previous proven sequence. In the second case, a proposer's proposal \(c\) is appended to an acceptor's \(val_{a}\) variable. By definition of the append operation, \(val_{a}\sqsubseteq val_{a}\bullet c\) which means that the acceptor's new value \(val_{a}\bullet c\) is an extension of previous ones. 1.3. For any pair of proposals \(s\) and \(s^{\prime}\), at any given instant, \(\forall x\in\mathcal{P},\exists\sigma_{1},\sigma_{2},\sigma_{3},\sigma_{4}\in \mathcal{P}\cup\{\bot\},\forall b,b^{\prime}\in\mathcal{B},(maj\_accepted(s,b) \vee(min\_accepted(s,b)\wedge s\bullet\sigma_{1}\sim x\bullet\sigma_{2})) \wedge(maj\_accepted(s^{\prime},b^{\prime})\vee(min\_accepted(s^{\prime},b ^{\prime})\wedge s\bullet\sigma_{1}\sim x\bullet\sigma_{2}))\implies s \bullet\sigma_{3}\sim s^{\prime}\bullet\sigma_{4}\)

**Proof:** By 1.2 and by definition of \(s\bullet\sigma_{1}\sim x\bullet\sigma_{2}\). 1.4. At any given instant, \(\forall s,s^{\prime}\in\mathcal{P},\forall l_{i},l_{j}\in\mathcal{L},learned (l_{i},s)\wedgelearned(l_{j},s^{\prime})\implies\exists\sigma_{1},\sigma_{2} \in\mathcal{P}\cup\{\bot\},s\,\bullet\sigma_{1}\sim s^{\prime}\bullet\sigma _{2}\)

**Proof:** By 1.1 and 1.3. 1.5. Q.E.D. 2. At any given instant, \(\forall l_{i},l_{j}\in\mathcal{L},learned(l_{j},learned_{j})\wedgelearned(l _{i},learned_{i})\implies\exists\sigma_{1},\sigma_{2}\in\mathcal{P}\cup\{\bot \},learned_{i}\bullet\sigma_{1}\simlearned_{j}\bullet\sigma_{2}\)

**Proof:** By 1. 3. Q.E.D. ### Nontriviality

**Theorem 2**. : _If all proposers are correct, learned\({}_{l}\) can only contain proposed commands._

**Proof:**

1. At any given instant, \(\forall l_{i}\in\mathcal{L},\forall s\in\mathcal{P},learned(l_{i},s)\implies \forall x\in\mathcal{P},\exists\sigma\in\mathcal{P},\forall b\in\mathcal{B}, \ maj\_accepted(s,b)\vee(min\_accepted(s,b)\wedge(s\sim x\bullet\sigma\lor x \sim s\bullet\sigma))\)

**Proof:** By Algorithm 9 lines [16; 30; 41] and Algorithm 10 lines [1; 2; 3; 1; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18], if a correct learner learned a sequence \(s\) at any given instant then either \(N-f\) or \(f+1\) (if \(s\) is universally commutative) acceptors must have executed _phase \(2b\)_ for \(s\). 2. At any given instant, \(\forall s\in\mathcal{P},\forall b\in\mathcal{B},maj\_accepted(s,b)\lor min\_accepted(s,b)\implies \mathit{proposed}(s)\)

**Proof:** By Algorithm 9 lines [18; 19; 20; 21; 22; 23], for either \(N-f\) or \(f+1\) acceptors to accept a proposal it must have been proposed by a proposer (note that the leader is considered a distinguished proposer). 3.