0.1 Symbols And Structure

• 表决 $B$

  struct Ballot {
    dec: Decree,      // 表决的内容
    vot: Set<Node>,   // 表决投票通过的节点
    qrm: Set<Node>,   // 表决参与的节点
    bal: u64,         // 表决编号
  }

  A ballot is said to be successful, if every quorum member voted. In math: $$ B_{qrm} \subseteq B_{vot} $$
• 投票 $v$

  struct Vote {
    pst: Node,        // 本投票的节点
    bal: u64,         // 本投票的表决编号
    dec: Decree,      // 本投票表决的内容
  }

• 表决的集合 $\beta$

• $Votes(\beta)$：所有在 $\beta$ 中的表决的投票的集合 $$Votes(\beta) = \{v:(v_{pst}\in B_{vot})\cap(v_{bal}=B_{bal}), B \in \beta\}$$
• $Max(b, p, \beta)$：在由节点 $p$ 投给 $\beta$ 中的表决的投票中，编号小与等于 $b$ 的最大投票 $$Max(b, p,\beta)=max\{v \in Votes(\beta):(v_{pst}=p)\land(v_{bal}<b)\}\cup\{null_{p}\}$$
• $MaxVote(b, Q, \beta)$：在集合 $Q$ 中的任意一个节点投给 $\beta$ 中的表决的投票中，编号小于等于 $b$ 的最大投票 $$MaxVote(b,Q,\beta)=max\{v\in Votes(\beta):(v_{pst}\in Q)\cap(v_{val}<b)\}\cup\{null_p\}$$

那么如果条件$B1(\beta)-B3(\beta)$满足的情况下，那么系统将满足一致性，并且是可进展的。

• $B1(\beta) \triangleq \forall B,B’ \in \beta:(B \ne B’) \implies (B_{bal} \ne B’_{bal})$
• $B2(\beta) \triangleq \forall B,B’ \in \beta:B_{qrm}\cap B’_{qrm} \ne \emptyset $
• $B3(\beta) \triangleq \forall B \in \beta: (MaxVote(B_{bal},B_{qrm},\beta)_{bal}\ne - \infty) \implies B_{dec} = MaxVote(B_{bal}, B_{qrm}, \beta)_{dec} $

如果 $\beta$ 中的表决 $B$ 是成功的，那么 $\beta$ 中更大编号的表决和 $B$ 的表决内容相同。 $$ ((B_{qrm} \subseteq B_{vot})\land(B’_{bal}>B_{bal})) \implies (B’_{dec}=B_{dec}) $$

定义集合 $\Psi(B, \beta)$: $\Psi(B, \beta) \triangleq \{B’\in \beta:(B’_{bal}>B_{bal})\land(B’_{dec}\ne B_{dec}) \}$，表示 $\beta$ 中编号比 $B$ 大并且表决内容不相同的表决的集合。

1. $ C = min\{B’:B’\in \Psi(B, \beta)\} $
2. $ C_{bal} < B_{bal} $
3. $ C_{qrm} \cap B_{bot} \ne \emptyset $ 因为 $B2$ 和 假设中的 $B$ 表决是成功的，也就是 $ B_{qrm} \subseteq B_{vot} $
4. $ MaxVote(C_{bal},C_{qrm},\beta)_{bal} \ge B_{bal} $ 因为 $C_{qrm}$ 和 $B$ 的投票者一定有交集
5. $ MaxVote(C_{bal}, C_{qrm}, \beta)\in Votes(\beta)$
6. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{dec} = C_{dec} $
7. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{dec} \ne B_{dec} $
8. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{bal} > B_{bal} $
9. $ MaxVote(C_{bal}, C_{qrm}, \beta) \in Votes(\Psi(B, \beta)) $
10. $ MaxVote(C_{bal}, C_{qrm}, \beta)_{bal} < C_{bal} $
11. 9, 10 和 1 矛盾。

在满足 $B1(\beta)$，$B2(\beta)$，$B3(\beta)$ 的情况下， $$((B_{qrm} \subseteq B_{vot})\land(B’_{qrm}\subseteq B’_{vot})) \implies (B’_{dec} = B_{dec}) $$

$$ \forall B\in\beta, b > B_{bal}, Q \cap B_{qrm} \ne \emptyset $$ 如果 $B1(\beta)$，$B2(\beta)$，$B3(\beta)$ 满足，那么存在一个 $ B’, B’_{bal}=b, B’_{qrm}=B’_{vot}=Q $ 使得 $B1(\beta\cup\{B’\})$，$B2(\beta\cup\{B’\})$，$B3(\beta\cup\{B’\})$ 成立。