介绍OVM：一种构造即正确的方法……

这基本上只是 Oracle Virtual Machine + Eclipse IDE 在区块链上。Java 再次回归了。

更新： 本文描述了我们现在称之为 OGS 或者乐观游戏语义（Optimistic Game Semantics）的内容。要深入了解 OGS，请查看 这篇论文! 如需获取 OVM 的最新信息，请访问 Optimism.io ❤️

介绍 OVM

一种正确构建方法的二层链

在这篇文章中，我们描述了乐观虚拟机（OVM）：一种设计用于支持所有二层（L2）协议的虚拟机。它的通用性来自于将 L2 重新框定为基于以太坊的“乐观”分叉选择规则。该形式化过程在很大程度上借鉴了 CBC Casper 研究，并将 二层视为对一层共识的直接扩展。这暗示着所有“二层可扩展性”结构（如 Lightning、Plasma 等）可能在单一理论和虚拟机 OVM 下统一。

本文将：

1. 介绍 OVM 的语言。
2. 描述如何使用通用争议合约实现一类 L2 应用的端到端编译。

第一部分：用统一语言描述 L2

第一层（L1）为我们提供了一个值得信赖但昂贵的虚拟机（VM）。第二层提供一个接口来高效使用昂贵的 L1 VM —— 而不是让交易直接更新 L1 状态，我们使用链下数据来保证 未来 会发生什么在 L1 状态上。我们称这种保证为“乐观决策”。

做出乐观决策的三步骤：

1. 查看 L1，判断未来可能发生什么。

2. 查看链下消息及其在 L1 使用时的保证。

3. 根据这些保证限制我们对未来 L1 状态的预期。

我们将很快将这个过程描述为 OVM 的 状态转换函数 的一部分。然而，首先让我们通过一些关键概念来建立我们对“限制未来 L1 状态的期望”所指内容的直觉。

🔑 概念 1：以太坊未来锥

可以想象未来的以太坊状态为一个无限的广阔空间，其中包含可能发生在区块链上的一切。每个可能签署的交易，每个 可能被攻击的 DAO —— 所有可能的未来。为了避免陈词滥调，本文将不提及：“量子”。

然而，即使在面对无限的未来时，我们仍然可以根据以太坊虚拟机的规则 限制可能的未来。例如，在 EVM 中，如果 5 ETH 被燃烧到地址 0x000...，我们知道所有未来的以太坊区块仍然会有 5 ETH 被燃烧。这与 CBC 的未来协议状态并行（Barnabé Monnot 提供的精彩插图 在这里）。

我们可以将逐渐限制可能未来的过程可视化为一个无限大的“锥体”，每次在挖掘和确认一个新区块时，这个锥体都会缩小。

以太坊未来锥的动画。如果 Alice 燃烧了 5 ETH，她知道它将在所有可能的未来区块中被燃烧。

注意，在 L1 中，所有未来状态的可能限制都是通过挖掘和围绕（确认）新区块形成共识来完成的——这是一种在 EVM 内产生不可逆状态转换的过程。

🔑 概念 2：本地信息

L2 使用本地信息（例如，链下消息）扩展共识协议。例如，一个签名的通道更新，或一个 plasma 区块的包含证明。

链下消息传递……可视化效果！

OVM 使用这些本地信息来做出 乐观决策 —— 我们称新的决策为 OVM 状态转换。但首先，OVM 必须定义它用来推导可能的未来以太坊状态的假设。

🔑 概念 3：本地假设

OVM 程序定义的假设基于本地信息，决定哪些以太坊状态是可能的。可以表示为函数 satisfies_assumptions(assumptions, ethereum_state, local_information) => true/false。如果 satisfies_assumptions(...) 返回 true，那么 ethereum_state 是基于这些假设和我们的 local_information 可能的。

在许多 L2 解决方案中，这种假设表现在“争议生存假设”中。例如，通道中的参与者假设他们将争议任何恶意提款。因此，我们会对任何包含恶意、未争议提款的以太坊状态返回 false。

两个分叉，一个中 `satisfies_assumptions(…)` 返回 true，另一个中基于“争议生存假设”返回 false。

🔑 概念 4：乐观决策

通过我们的本地假设消除不可能的未来之后，我们终于可以对未来做出“乐观决策”。以下是在支付通道中的一个常见乐观决策：

乐观决定余额（使用我们上面定义的三步过程）：

1. 查看 L1，判断 Alice 是否与 Bob 在支付通道中。

2. 查看链下消息，确定：a) Alice 拥有最高签名的 nonce，向她发送 5 ETH；b) Alice 在争议期间可以提取她的 5 ETH；c) Alice 可以根据她的“争议生存假设”回应任何无效提款。

3. 将我们对未来 L1 状态的期望限制为只包含 Alice 被发送 5 ETH 的状态。

Alice 现在可以乐观地决定她最终将在以太坊的所有未来状态中至少拥有 5 ETH。 — 而无需链上交易！

最后一个 🔑：乐观未来锥

请记住，“以太坊未来锥”仅通过确认区块进行限制——这是一个完全追溯的过程。在最后一部分中，我们回顾了一种乐观的方法，该方法根据 本地 信息 和 本地假设 对未来进行限制——这是一种前瞻性的过程。这两种方法可以“叠加”在一起，结合两者的优势：区块链共识的安全性，加上本地消息传递的速度、效率和隐私。

我们可以将这一混合过程可视化为一个未来锥，它不仅在每个区块后限制未来以太坊状态，还根据本地信息在区块之间限制未来状态。决定新的限制被视为 OVM 中的“状态转换”。

当 Alice 收到新的链下消息时，她的乐观未来锥“收缩”。

统一语言

上述概念可用作二层的共享语言和执行模型的基础。这包括：

- 零确认交易

- Lightning 网络

- 跨分片状态方案

- Plasma、通道、Truebit

……以及更多 —— 所有这些都在共享符号系统中。

在本文的第二部分中，我们将扩展这一语言，展示这种正确构建的方法如何激励特定的 OVM 运行时。基于一阶逻辑，它支持现有的 L2 设计——包括 那些针对 ETH2 的设计。

但是首先，如果你和我们一样喜欢看一些花哨的数学，下文是我们刚才回顾的关键概念的形式化：

进一步构建 OVM 运行时

兴奋于 L2 可以用统一语言描述的事实，我们很快提出了一个问题：我们如何使这变得有用？我们能否创建一个支持不同 L2 设计的通用 L2 运行环境？

事实证明，对一个广泛类的 OVM 程序而言，我们可以做到。技巧在于构建一个争议合约，它解释 OVM 基于的相同数学表达。这允许以谓词逻辑编写高级语言。

通用争议合约

要做到这一点，我们创建一个处理用户提交的“声明”的仲裁合约——这些表达式的求值为 true/false。例如，“哈希 X 的原像不存在。”

争议涉及逻辑上矛盾的反声明。例如，“哈希 X 的原像存在” 将与第一个声明相矛盾。这推广了 L2 的“挑战”：到头来，所有争议都是逻辑矛盾（它们不可能同时为真）。

在争议超时后，合约可以对未被挑战的声明判定真。然而，如果出现矛盾，它需要做出选择。对真/假声明的决策逻辑称为 谓词演算。

谓词 2.0

在开发 通用 plasma 的过程中，我们意识到可插拔的“谓词合约”使定制乐观执行成为可能。我们现在所理解的是，一个可插拔的谓词系统并不是通用 plasma —— 它是通用的二层。从这个角度看，plasma 合约只是一组谓词的组合。

谓词合约是逻辑的“评估者” —— 决定输入为真或假的。在关键点上，它们可以基于其他谓词做出判断。这意味着一小组相互作用的谓词可以仲裁大量的 L2 系统。

示例谓词

让我们回顾一些在一阶逻辑中使用的示例谓词。

NOT

该谓词执行逻辑否定：NOT(aPredicate, anInput)。如果声称 aPredicate(anInput)，则可以对其进行反驳。

AND

该谓词是逻辑与运算符，形式为 AND(predicate1, input1, predicate2, input2)。可以通过 NOT(predicate1, input1) 或 NOT(predicate2, input2) 进行反驳。

WITNESS_EXISTS

该谓词声称某些证人数据存在：WITNESS_EXISTS(verifier, parameters)。这是链给二层系统使用生存假设的 基本构建块。仅当收到某个 witness 使得 verifier.verify(parameters, witness) 返回 true 时，它才决定为真。

UNIVERSAL_QUANTIFIER

该谓词表示基于某个 量词（“对所有”）的 全称量化（“如此”）—— UNIVERSAL_QUANTIFIER(aQuantifier, aPredicate)。仅当且仅当 aQuantifier.quantify(someInput) 返回 true 时，若与 NOT(aPredicate, someInput) 对立。

组合状态通道

一种广泛理解的二层系统是状态通道，因此让我们用谓词组合一个状态通道。从状态通道提款类似于声明以下内容：“对于所有比此 withdrawn_update 更高 nonce 的状态更新，没有所有通道参与者的统一签名。”

那么，对于通用争议合约，我们将声明如下：

UNIVERSAL_QUANTIFIER(HAS_HIGHER_NONCE_QUANTIFIER(withdrawn_update), NOT(WITNESS_EXISTS(VERIFY_MULTISIG, withdrawn_update.participants)))

对于数学领域的人来说，这可能看起来更熟悉，如下表达式：

因此，状态通道可以通过组合四个简单的谓词来构建。

一个乐观的未来

凭借极少的谓词，这个通用争议合约可以仲裁许多 L2 系统：各种 plasma 变种、状态通道、乐观跨片状态方案、Truebit，等等。谓词运行时为每种方法提供了一个共享平台 —— 提高开发者工具的使用效率。它有效地 将 L2 开发者的工作量减半，因为谓词表达式在链上和链下均被解释。

超越谓词运行时，OVM 具有更广泛的意义：

1. 通信 —— 针对以前定制概念的数学模型。
2. 互操作性 —— 为所有乐观执行提供共享内存。
3. 安全性 —— L2 和谓词运行时的形式化证明。

敬请关注我们详细介绍 OVM 和谓词运行时的论文。在此期间，你可以通过 合同的早期草稿 来进一步满足你的好奇心。

如果有问题，请在 Twitter 上 @plasma_group 进行提问，或者更好的是加入 plasma.build 论坛 进行讨论——继续前进！

PG 感谢以下个人对本文结构的评论和编辑：V、Will Meister 和 Akhila Raju.

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