在另一个Casper上使用形式化方法在之前的一篇文章中，我谈到了…… | Yoichi Hirai | Medium

另一种 Casper 的形式化方法

在 之前的文章 中，我谈到了证实 Vitalik 的 Casper 的性质。这篇文章是关于 Vlad 的 Casper。它们有很大的不同。这两个 Casper 不仅仅是两种不同的协议，而是两种对协议设计的相反方法。

Vitalik 的 Casper 看起来可实现。它是一种直接构建，首先解决一个简单问题，然后逐步增加复杂性以满足实际需求。

Vlad 的 Casper 更像是寻找根本困难的努力。它留下了一些非根本性的问题开放，专注于问题的本质。问题的核心来自异步，消息可以被延迟和重排。这相当于节点以任意速率减慢。这反过来又等于攻击者可以在任何时刻进行任意多的操作。问题的核心是如何仅通过观察主观的过去来建立对未来的安全知识。

当前形式下的 Vlad 的 Casper 并未指定验证者之间的通信方式。是基于轮次的吗？不是，但即使是基于轮次的协议也可以作为 Vlad 的 Casper 的一种实现来分析。它有活跃性假设吗？没有，但可以在 Vlad 的 Casper 上附加任意的消息延迟或验证者的活跃性假设。它是许多协议的干细胞。它也是可以衡量许多不同外观算法的标准。

我想这只是 Vlad 的 Casper 的 5%，但不知为何，Vlad 和我在 Isabelle/HOL 中证明了他的一部分 Casper。代码在 GitHub 上可用。

在这一部分的最后，最重要的概念是估计安全性：“基于视图的估计是安全的。”它的特殊之处在于，任何参与者都可以仅通过查看他们对过去的视图来判断一个估计是否安全，而安全性会告诉他们估计永远不会改变。这就是仅通过观察主观的过去来建立对未来的安全知识的解决方案。Vlad 的 Casper 更进一步，描述了一个保证估计安全性的算法，但我们尚未在 Isabelle/HOL 中形式化这个算法。

一旦达到了某个阶段，就需要停止讨论并开始编写代码。这与软件开发是一样的。第一行通常是无聊的。这就是为什么有时候提前展望并自由讨论是重要的。在知道我们想要什么之后，我们有时可以忍受那些无聊的部分。

验证者。验证者是什么？我们知道的不多。我们只是说，验证者的数量与整数一样多。在 Isabelle/HOL 中，整数是无穷的。

datatype validator = Validator int

在我们这样说之后，Isabelle/HOL 允许我们比较两个验证者，并查看它们是否相等。它不允许我们“添加”或“乘”验证者。它不允许我们询问一个验证者是否比另一个验证者大。这样的情况很舒服。我们受到许多错误的保护。

验证者有权重。我们只讨论将权重分配给验证者的函数。

type_synonym weight = “validator ⇒ int”

在我们这样说之后，Isabelle/HOL 在看到 weight 时，不会将 weight 替换为更长的定义，而是将其视为 validator => int，这是接受验证者并返回整数的（通常总的）函数的类型。该函数仅在每个验证者上返回一个整数。

当然，我们可以指定权重函数的属性。

definition tie_breaking :: “validator set ⇒ weight ⇒ bool”
where
“tie_breaking V w =
 ( ∀ S0 S1.
 S0 ⊆ V ⟶
 S1 ⊆ V ⟶
 S0 ≠ S1 ⟶
 sum w S0 ≠ sum w S1 )”

在输入这些行后，Isabelle/HOL 知道 tie_breaking 有意义。它不会自动用冗长的定义替换 tie_breaking 的出现，但它知道 tie_breaking 是被定义的。一些插件甚至查看定义的内容来确定如何（不）证明某些内容。

权重函数 w 在验证者集 V 上是 tie_breaking 的当且仅当，对于 V 的任意不同子集 S0 和 S1，W 在 S0 上的总和不等于 w 在 S1 上的总和。

形式化的初始部分既无聊又危险。这里的一个错误可能会导致后面几千行的错误。也许我们应该进行一个实验。假设有两个权重为一的验证者；那么割断属性就不应该成立。我们准备一个统一的权重函数，将每个验证者都赋予 1。

definition uniform_weight :: “validator ⇒ int”
where
“uniform_weight v = 1”

在这个统一的权重函数上，两个验证者的割断属性应该不成立。

lemma should_be_false: “¬ tie_breaking {Validator 0, Validator 1} uniform_weight“

当用户输入这个语句时，Isabelle/HOL 会尝试找到一个反例，持续一两秒（如果你想要更长的检查时间，可以输入 nitpick）。同时 Isabelle/HOL 将该语句回显，以作为需要证明的目标。

proof (prove)
goal (1 subgoal):
 1. ¬ tie_breaking {Validator 0, Validator 1} uniform_weight

现在由用户来决定如何证明这一点。我说：“使用割断属性的定义来缩小目标。”

apply(simp add: tie_breaking_def)

Isabelle/HOL 立刻回应结果。

proof (prove)
goal (1 subgoal):
 1. ∃S0⊆{Validator 0, Validator 1}. ∃S1⊆{Validator 0, Validator 1}. S0 ≠ S1 ∧ sum uniform_weight S0 = sum uniform_weight S1

缩小后的语句表示；存在两个不同的子集 {Validator 0, Validator 1}，其上统一权重的总和是相同的。

又一次轮到我了。我必须选择 S0 和 S1 来证明割断属性。当我实际执行这一操作时（我不再展示命令），Isabelle/HOL 确认定理成立。

theorem should_be_false:
¬ tie_breaking {Validator 0, Validator 1} uniform_weight

我有另一个猜想：任何权重函数在一组无限的验证者上应该是割断的。在 Isabelle/HOL 中，对无限集的总和被定义为零。我还没有检查这个猜想，而是继续讨论赌博和视图。

在 Vlad 的 Casper 中，验证者签署赌注。赌注包含一个估计。直观地说，估计是对共识结果的预测，但我们并不依赖于这种直觉。我们的问题是建立对验证者行为的一些标准，并最终建立一个惩罚和奖励验证者的游戏。验证者可能仅以计算机程序或蜜蜂群的形式实现。因此，询问验证者的意图并没有太大意义。整个游戏必须使用仅可观察的行为定义。

谁观察验证者的行为？我不知道。我们现在并不需要知道。无论谁观察验证者的赌注，观察结果将包含由验证者签署的一组赌注。

最终，我们将希望在历史上形成一个共识。所需的历史可能是线性的，也可能不是。根据历史的内容，一些事件可能与其他事件兼容。那种组合学会带来自己的麻烦。因此，目前的问题是一个二元选择：选择两个值之一。这是再次推迟一个较小问题并专注于本质的行为。

Isabelle/HOL 有一个包含两个值的类型：布尔型。通过这个，我们定义了一种名为估计的类型。

datatype estimate = Estimate bool

在我输入这一点之后，Estimate True 和 Estimate False 是两个不同的估计。没有其他估计。

赌注是通过一个验证者（签署者）、一个估计和一组赌注（理由）三元组的形式递归定义的。我说是“递归定义的”，因为否则这个句子无法形成定义。赌注的理由可以包含第一个相关的赌注吗？可以用一个赌注开始，然后找到一个理由，再找到它的理由，依此类推，无限吗？这两个问题的答案都是“不”，我们稍后会证明，但那只是因为我说了“递归”。

在 Isabelle/HOL 中，每个数据类型定义都被视为递归定义。我不必说“递归”。

datatype bet =
 Bet “estimate * validator * bet list”

这里发生了一些棘手的事情。我不知道 Isabelle/HOL 如何处理这个。以某种方式，Isabelle/HOL 在后台证明了一个定理（这个语句看起来特别丑陋，但不要害怕。Isabelle/HOL 通常在 UI 上看起来非常好）：

BetsAndValidators.bet.induct:
 (⋀xa. (⋀xaa xaaa xaaaa. xaa ∈ Basic_BNFs.snds xa ⟹ xaaa ∈ Basic_BNFs.snds xaa ⟹ xaaaa ∈ set xaaa ⟹ ?P xaaaa) ⟹
 ?P (Bet xa)) ⟹
 ?P ?bet

这允许根据数学归纳法证明关于所有赌注的事情。

一个赌注的发送者是包含在赌注中的验证者：

fun sender :: “bet ⇒ validator”
where
“sender (Bet (_, v, _)) = v”

一个赌注的估计是赌注中包含的估计：

fun est :: “bet ⇒ estimate”
where
“est (Bet (e, _, _)) = e”

一个赌注证明一个赌注合法当且仅当前者是后者理由之一：

fun justifies :: “bet ⇒ (bet ⇒ bool)”
where
“justifies b (Bet (e, v, js)) = (b ∈ set js)”

一个赌注依赖于一个赌注，意味着有从后者到前者的一系列理由。“justifies” 是赌注之间的二元关系，而 “is_dependency” 是该关系的传递闭包。

传递闭包可以定义为：

inductive tran :: “(bet ⇒ bet ⇒ bool) ⇒ (bet ⇒ bet ⇒ bool)”
where
  tran_simple: “R x y ⟹ tran R x y”
| tran_composit: “tran R x y ⟹ R y z ⟹ tran R x z”

“tran R” 是一种最小的赌注之间的二元关系，以至于在两种情况下成立：“tran R x y”：

1）简单的 “R x y” 成立；以及当

2）“tran R x y” 和 “R y z” 成立。

我必须说“最小的”，因为上述两个条件不够具体，以标识一个唯一的二元关系 “tran R”。例如，即使“tran R”连接每两个赌注，这些条件也能成立。（“最小的”这种事存在吗？好问题！ https://softech.informatik.uni-kl.de/homepage/teaching/SVHOL12/slides6a.pdf）

在完成这些之后，我们可以说 “is_dependency” 是 “justifies” 的传递闭包。

definition is_dependency :: “bet ⇒ bet ⇒ bool”
where
“is_dependency = tran justifies”

在传递闭包的定义中，我说“tran R x y”和“R y z”。我可以添加第三种情况“R x y”和“tran R y z”，但这不应该改变传递闭包。

lemma is_dependency_tail_first :
 “tran R y z ⟹ R x y ⟹ tran R x z”

证明是对传递闭包的归纳。

我说赌注的定义是递归的。因此我可以证明两个赌注在依赖关系上互不相连。没有理由的循环。没有恶性循环，可以这么说。

lemma dependency_no_cycle :
 “∀ a. is_dependency a b ⟶ ¬ is_dependency b a”

证明的过程是对 b 的归纳。这个证明是有趣的，因为归纳没有减少循环的大小。

一个不那么激动的事实是“is_dependency”确实是传递的。

lemma dependency_is_transitive :
 “is_dependency y z ⟹
  ∀ x. is_dependency x y ⟶ is_dependency x z”

证明是对传递闭包的归纳。

经过那么多的官僚主义，这里有一个有意义的概念。当验证者签署两个不同的赌注且两者互不依赖时，该验证者就发生了歧视。这是 Casper 等同于双重支出的情形。歧视意味着未保持自己线性的历史。

definition equivocation :: “bet ⇒ bet ⇒ bool”
where
“equivocation b0 b1 =
 (sender b0 = sender b1 ∧ ¬ is_dependency b0 b1
 ∧ ¬ is_dependency b1 b0 ∧ b0 ≠ b1 )”

这表示，当两个赌注 b0 和 b1 来自同一个发送者，且两者都不相互依赖时，它们就形成了歧视，且它们不同。

一个视图是一组不包含歧视的赌注。

definition is_view :: “bet set ⇒ bool”
where
“is_view bs = (∀ b0 b1. b0 ∈ bs ⟶ b1 ∈ bs ⟶ ¬ equivocation b0 b1)”

一组赌注是一个视图当且仅当该组中没有两个赌注形成歧视。

我们通常对来自验证者的最新赌注感兴趣。

definition latest_bets :: “bet set ⇒ validator ⇒ bet set”
where
“ latest_bets bs v =
   { l . l ∈ bs ∧ sender l = v
      ∧ (¬ (∃ b’. b’ ∈ bs ∧ sender b’ = v ∧ is_dependency l b’))}“

非常抱歉，v（一个字母）和 ∨（逻辑或符号）看起来非常相似。在上述定义中，仅有字母 v，而不是逻辑或符号。来自验证者 v 的投注集合 bs 中最新的投注包括这些投注，且其发送者为 v，且不依赖于 bs 中来自 v 的任何赌注。

不论验证者如何，我们还可以讨论一组赌注中的最新赌注。

definition is_latest_in :: “bet ⇒ bet set ⇒ bool”
where
“is_latest_in b bs =
  (b ∈ bs ∧ (¬ (∃ b’. b’ ∈ bs ∧ is_dependency b b’)))”

一赌注在一组赌注中最新当且仅当该赌注是该集合的一个元素，且该赌注不依赖于集合中的任何赌注。

当一个集非空时，它有一个元素：

definition is_non_empty :: “‘a set ⇒ bool”
where
“is_non_empty bs = ( ∃b. b∈bs )”

当一组赌注是有限且非空时，它有最新赌注：

lemma latest_existence’ :
 “finite bs ⟹ is_non_empty bs ⟶ (∃ l. is_latest_in l bs)”

这取决于理由链不形成循环的事实。有限性是必要的，因为否则所有赌注可能属于一个无限的理由链。

一个来自验证者的最新赌注有一个有趣的特点，除非该验证者发生歧视，否则只能有一个。当有来自同一个验证者的两个不同最新赌注时，它们形成歧视。

lemma two_latests_are_equivocation :
 “b0 ∈ latest_bets bs v ⟹ b1 ∈ latest_bets bs v ⟹ b0 ≠ b1 ⟹ equivocation b0 b1”

当任意两个元素相等时，一个集合最多只包含一个元素：

definition at_most_one :: “‘a set ⇒ bool”
where
“at_most_one s = (∀ x y. x ∈ s ⟶ y ∈ s ⟶ x = y)”

由于视图不包含歧视，视图可以最多包含来自一个验证者的一个最新赌注：

lemma view_has_at_most_one_latest_bet :
 “is_view bs ⟹ at_most_one (latest_bets bs v)”

有时我们对在一组赌注中签署赌注的验证者感兴趣：

definition observed_validators :: “bet set ⇒ validator set”
where
 “observed_validators bs =
({v :: validator. ∃b. b ∈ bs ∧ v = sender b })”

被观察的赌注组合中的验证者包括在该集合中签署了一些赌注的那些验证者。请注意，这并不考虑集合外的理由。

因此，在一个非空的赌注集合中，我们可以找到一些验证者。

lemma observed_validators_exist_in_non_empty_bet_set :
 “is_non_empty bs ⟹ is_non_empty (observed_validators bs)”

也许更有趣的是，如果赌注集合非空，则观察到的验证者总是有最新的赌注。

lemma observed_validator_has_latest_bet :
 “finite bs ⟶ v ∈ (observed_validators bs) ⟶ is_non_empty (latest_bets bs v)”

将上述两个引理结合起来，我们知道总是存在至少一个具有最新赌注的验证者，这样的验证者在有限的非空赌注集合中。

lemma latest_bets_exist_in_non_empty_bet_set :
 “finite bs ⟹
 is_non_empty bs ⟹
 ∃v::validator.(is_non_empty (latest_bets bs v))”

我们对当前支持哪个估计的验证者感兴趣。当一个验证者在估计上有最新赌注时，我们称之为具有该估计的最新赌注。

definition has_a_latest_bet_on ::
 “bet set ⇒ validator ⇒ estimate ⇒ bool”
where
“has_a_latest_bet_on bs v e =
 (∃ b. b ∈ latest_bets bs v ∧ est b = e)”

在一个视图中，验证者不能在不同的估计上有最新赌注：

lemma validator_in_view_contributes_to_at_most_one_estimates_weight :
 “is_view bs ⟹
 ∀v. v∈(observed_validators bs) ⟶ at_most_one {e. (has_a_latest_bet_on bs v e)}”

最新赌注与权重函数相结合，为一组赌注中的估计提供权重。权重是具有该估计的最新赌注的验证者的权重总和。

definition weight_of_estimate ::
 “bet set ⇒ weight ⇒ estimate ⇒ int”
where
“weight_of_estimate bs w e =
 sum w { v. has_a_latest_bet_on bs v e }”

现在我们可以讨论哪个估计在竞争中处于领先地位。当一个估计的权重至少与其他估计的权重相等时，我们称之为最大权重估计。

definition is_max_weight_estimate ::
 “bet set ⇒ weight ⇒ estimate ⇒ bool”
where
“is_max_weight_estimate bs w e =
 (∀ e’.
 weight_of_estimate bs w e ≥ weight_of_estimate bs w e’)”

是否会有多个最大权重估计？在某些条件下不会：在有限的非空视图中，权重函数是正的并具有割断性。

lemma view_has_at_most_one_max_weight_estimate :
 “is_view bs ⟹
 finite bs ⟹
 is_non_empty bs ⟹
 positive_weights (observed_validators bs) w ⟹
 tie_breaking (observed_validators bs) w ⟹
 at_most_one {e. is_max_weight_estimate bs w e}”

有了最大权重估计的概念，我们现在准备描述诚实的行为。验证者不应该歧视。验证者只应产生有效的赌注。

当验证者有理由时，由于这些理由是赌注，因此存在最大权重估计。一个有效赌注是基于理由的最大权重估计。

fun is_valid :: “weight ⇒ bet ⇒ bool”
where
“is_valid w (Bet (e, v, js))
  = is_max_weight_estimate (set js) w e”

有效视图是仅包含有效赌注的视图：

definition is_valid_view :: “weight ⇒ bet set ⇒ bool”
where
“is_valid_view w bs = (is_view bs ∧ (∀ b ∈ bs. is_valid w b))”

在有效视图中，每个赌注都是诚实创建的。没有验证者歧视。所有有理由的赌注遵循最大权重规则。这里我们不讨论拜占庭故障（当验证者执行任意行动，稍微不诚实或完全随机）。也许，已证明的不诚实的赌注从视图中被删除。

到目前为止，所有论点都基于一个静态的赌注集合。现在我们谈论两个视图，一个是另一个未来的可能性。

definition is_future_view :: “weight ⇒ bet set ⇒ bet set ⇒ bool”
where
“is_future_view w b0 b1 =
 (b0 ⊇ b1 ∧ is_valid_view w b0 ∧ is_valid_view w b1)”

未来视图的定义要求这些视图都是有效视图。

我们的目标是确保基于对过去的观察建立知识。期望的知识的一种形式是估计安全性。当估计是最大权重估计时，它是安全的：

definition is_estimate_safe ::
   “weight ⇒ bet set ⇒ estimate ⇒ bool”
where
“is_estimate_safe w bs e =
 (∀ bf. is_future_view w bf bs ⟶ is_max_weight_estimate bf w e)”

当一个参与者获取到一个安全的估计时，另一个参与者也获取到一个安全的估计，理想情况下它们是相等的。如果是这种情况，任何达到安全估计的人都会共享相同的估计。

当两个视图的并集是有效视图时，它们是一致的。

definition consistent_views :: “weight ⇒ bet set ⇒ bet set ⇒ bool”
where
“consistent_views w b0 b1 =
 (is_valid_view w b0 ∧ is_valid_view w b1
 ∧ is_valid_view w (b0 ∪ b1))”

我们能够证明关于估计安全性的一个漂亮的性质。当一个估计在一个视图中是安全的，而另一个估计在另一个视图中安全时，这两个估计总是重合。

lemma consensus_safety :
 “finite b0 ⟹
 finite b1 ⟹
 is_non_empty b1 ⟹
 positive_weights (observed_validators b0) w ⟹
 positive_weights (observed_validators b1) w ⟹
 tie_breaking (observed_validators (b0 ∪ b1)) w ⟹
 is_estimate_safe w b0 e0 ⟹
 is_estimate_safe w b1 e1 ⟹
 consistent_views w b0 b1 ⟹
 e0 = e1”

基本上，当你有一个安全的估计时，你不需要担心你对世界的了解可能不完美。你不需要再了解更多。所有其他了解得足够好的参与者都会与你达成相同的估计。现在是时候大声喊出（或静静地接受定论），这个估计将成为共识。

现在还要看看如何判断一个估计在某个视图中是否安全。Vlad 这部分有书面记录。他也有一个实现。该算法的证明尚未经过机器检查。

• 原文链接： medium.com/@pirapira/for...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～