形式化验证 Gasper 共识机制
形式化验证 Gasper 共识机制
Gasper 是一个由信标链协议（即将到来的以太坊 2.0 网络的底层协议）实现的抽象的权益证明协议层。Gasper 的关键部分就是一套终局性机制（finality mechanism），用于保证交易的持存性（durability）和系统的不间断运作不会被攻击破坏。
Gasper
罚没条件（slashing Conditions）
Gasper 定义了两个条件（也称罚没条件）来定义何谓自相矛盾的投票：
- 双重投票（Double-voting）：验证者发布了两个截然不同的投票，但两个投票的目标高度是同一个高度。
- 环绕投票（Surround-voting）：验证者发布的一个投票所关联的两个检查点恰好在自己所发布的另一个投票的两个检查点高度范围内。
发起双重投票的验证者被认为违反了第一罚没条件；而发起环绕投票的验证者则违反了第二罚没条件。不论是哪种情况，违反规则的验证者都会被扣除大量保证金。
正确性（Correctness Properties）
与其它拜占庭容错型（Byzantine Fault Tolerance，BFT）协议相同，Gasper 协议的一个关键底层假设是绝大多数验证者（超过 2/3，以保证金数量定义）是诚实的、会遵循协议的要求。在此假设下，Gasper 有两大基本属性：
- 可追责的安全性（Accountable Safety）：不会有两个属于不同分叉的区块都被终局化，除非有至少 1/3 的验证者（以保证金数量计）被罚没；
- 似然活性（Plausible Liveness）：无论区块链过往发生了什么事，区块的终局化进程永远不会陷入僵局。
此外，在验证者集合会动态变化的环境（因为验证者会离开网络，也会有新验证者加入，活跃验证者集合可能会发生改变）中，第三种属性量化了在有人违反协议规则时可被罚没的保证金体量： - 可罚没下限（Slashable bound）：只要能够使用协议外条件来控制验证者的**和退出参数条件，就能证明（在打破安全性时）可被罚没的保证金数量有一个下限。
动态验证者集合（也即信标链协议所实现的）引入了另一个有挑战性的问题：系统不再那么能够可靠地惩罚恶意验证者，因为他们可能会在作恶之后、保证金被实际罚没之前离开网络。而可罚没下限属性使得调整活跃验证者集合的可变幅度、维持最低水平的可追责性成为可能。
建模及验证方法
第一步是开发一个协议的模型，让我们能够表达出所有我们希望形式化地指出并证明的关键属性。这个模型建立在我们之前验证 Casper FFG 的安全性和活性的工作基础上（此前的模型已经定义了 Gasper 终局性机制的早期版本）。
这一模型有三个主要的结构化模块：
验证者和团体（Validators and quorums）。验证者被抽象地表示为一个有限型（finite type）的成员（成员数量有限，而且可以枚举），写为 Validator : finType 。每个验证者都有一份保证金；这一事实我们建模成一个未解释的函数 stake : {fmap Validator -> nat}，保存验证者与其保证金数量（一个自然数）的映射。此外，给定一个验证者集合，其权重 wt 定义为该集合中所有验证者保证金数量的总和：
\sum 是求和运算符；stake.[st_fun v] 则给出了相应于验证者 v 的保证金数量（st_fun 即假设每个验证者都必须在系统中有一份保证金）。
wt 函数的几个属性源自其定义，例如：空验证者集的权重必然为 0，两个互不相交的集合的合集的权重就是各自权重的和。这些属性在涉及可罚没下限属性中关于权重的推理时会派上用场。
此外，因为我们要模拟动态的验证者集合，也就是活跃验证者的集合可能会随区块发生改变，我们声明了一个抽象的（有限）映射 vset : {fmap Hash -> {set Validator}}，给出一个区块处的活跃验证者集合。现在，使用 vset 和 wt，我们就能定义什么是绝对多数集合：
在某个区块处，如果活跃验证者集合的一个子集的权重超过整个集合权重的 2/3，则该子集就是一个绝对多数集合。
区块树。我们用区块哈希的有限型来模拟一个区块 Hash:finType，另外，用 genesis 代表创世区块。我们使用符号 h1 <~ h2 这样的符号来表示区块父子关系（ h1 就是 h2 的父辈），以此模拟检查点区块树。
接下来我们使用 h1 <~* h2 来定义祖先关系，h1 就是 h2 的祖先，而 h2 就是 h1 的后代（h1 和 h2 可以是同一个区块）。至于祖先关系的属性，比如祖先的祖先也是祖先，与父子关系的属性类同。
全局状态。状态可表示为由合理化投票组成的有限集合，投票的形式是 (v, s, t, s_h, t_h)，而 v 是发起投票的验证者，s 和 t 是 TA 支持的来源区块和目标区块，而 s_h 和 t_h 是它们的见证高度（attestation height）。某一个投票是否有人发起过可通过一个布尔成员断言确定：
原文链接：https://runtimeverification.com/blog/formally-verifying-finality-in-gasper-the-core-of-the-beacon-chain/
为了理解Gasper，我们先要了解三个基本概念：
纪元边界(Epoch boundary):Gasper把12秒定义为了一个基本时间槽(slot),然后把64个slot定义为一个**纪元(epoch).**那么每个纪元开始的那个区块就成为边界区块，用EBB(B,j)=C表示，第j个epoch的区块B的边界区块是区块C
委员会：所有的验证者被分配到每一个epoch中，构成了一个大的委员会，并且对于每一个slot从这个大的委员会选出一个特定的委员会。再每一个slot中，由一个验证者来打包出块，该委员会的其他成员使用HLMD GHOST（LMD GHOST的一个轻微变种，后面会讲）附上认可这个区块的证明。
验证和敲定(Justification and Finalization)：这个其实和Casper FFG很像，不过这里不是对单个检查点操作，而是对所有的纪元边界区块进行操作。