信标链协议|技术贴 | 形式化验证Gasper共识机制的终局性（finalization）( 二 ) 机制|技术|验证|

动态验证者集合（也即信标链协议所实现的）引入了另一个有挑战性的问题：系统不再那么能够可靠地惩罚恶意验证者，因为他们可能会在作恶之后、保证金被实际罚没之前离开网络。而可罚没下限属性使得调整活跃验证者集合的可变幅度、维持最低水平的可追责性成为可能。
验证 Gasper 的终局性 Gasper 旨在为终局性提供一个数学化的、精确的、可用来形式化地证明其正确性的描述；这种正确性也是证明信标链协议安全性的关键。以太坊平台正日渐被用作大型金融交易系统的股价，更突出了安全性保证的前所未有的重要性。
与以太坊基金会通力合作，我们已经使用 Coq证明助手，形式化了 Gasper 在动态验证者集合一般条件下的终局性机制。我们在这一条件下指出并证明了Gasper的所有三种关键属性：可追责的安全性、似然活性以及可罚没下限；所有证明都使用了同一个 Coq 模型。
对协议的演绎论证给了我们对相关主张正确性和安全性的极大信心，因为演绎论证保证没有未经指明的假设，也没有无效的演绎推理步骤。它也明确了为使论点成立所需的所有假设。形式化过程也能反哺协议的描述，使协议的描述能更准确、更完整。
这里我们仅对这一成就给出概要的说明。完整的细节可见：

该项目的技术报告
该项目的 Github 代码库

建模及验证方法第一步是开发一个协议的模型，让我们能够表达出所有我们希望形式化地指出并证明的关键属性。这个模型建立在我们之前验证 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 这样的符号来表示区块父子关系（ <code>h1就是h2的父辈），以此模拟检查点区块树。
接下来我们使用 h1 来定义祖先关系，<code>h1就是h2的祖先，而h2就是h1的后代（h1 和 h2 可以是同一个区块）。至于祖先关系的属性，比如祖先的祖先也是祖先，与父子关系的属性类同。
全局状态。状态可表示为由合理化投票组成的有限集合，投票的形式是(v, s, t, s_h, t_h)，而v是发起投票的验证者，s和t是 TA 支持的来源区块和目标区块，而s_h和t_h是它们的见证高度（attestation height）。某一个投票是否有人发起过可通过一个布尔成员断言确定：
实例规范基于这些定义以及它们相应的属性，我们定义出了模型中的所有其它结构和属性，包括罚没条件、团体交集属性（quorum intersection property），还有合理化以及终局化。举例而言，在一次违反协议的事件中，罚没某个团体的属性可使用如下的抽象成员约束而得到定义：

信标链协议|技术贴 | 形式化验证Gasper共识机制的终局性（finalization）

文章图片
该命题指出，罚没一个团体意味着，在某些区块 bL和bR处存在着两个绝对多数团体vL和vR，这两个团体的交集就是被罚没验证者（发起了双重投票或者环绕投票）的完整集合。注意，在活跃验证者集合一直固定的特殊条件下，这些绝对多数集合的交集的权重至少是所有保证金的 1/3。
另一个例子是一个终局化分叉（即违反安全性的情形）的定义：
该命题指出两个相互矛盾的区块 b1和b2都被终局化了（因为