如何使用通用争议合约L2应用程序来构建状态通道

自于将L2重新定义为以太坊之上的“乐观”分叉选择规则。形式化大量借鉴了CBC Casper的研究，并将2层描述为1层共识的直接延伸。这意味着在单一理论和虚拟机：OVM下可能统一所有“2层可伸缩性”的结构（闪电，plasma等）。

介绍OVM的语言

简述如何使用通用争议合约端到端地编译一类L2应用程序。

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

第1层（L1）为我们提供了一个值得信赖但价格昂贵的虚拟机（VM）。第2层提供了一个有效而昂贵的L1 VM的接口 - 而不是直接更新L1状态的事务，我们使用离线数据来保证L1状态会发生什么。我们称此保证为“乐观的决定”。

做出乐观决策的三个步骤：

1、看看L1，找出未来可能发生的事情。

2、查看链外消息以及它们保证在L1中使用的内容。

3、基于这些保证，限制我们对未来L1状态的期望。

我们将此过程描述为OVM状态转换函数的一部分。然而，首先让我们通过一些关键概念来构建“限制对未来L1状态的期望”的想法。

概念1：以太坊期货圆锥体

可以想象未来的以太坊状态是一个无限的扩展，其中包含了区块链可能发生的一切。每个可以签署的交易，都可能慧被黑客攻击的DAO。为了避免陈词滥调，这篇文章不会提到“量子”这个词。

然而，即使面对无限期货，我们仍然可以根据以太坊虚拟机的规则限制未来的可能。例如，在EVM中，如果5 ETH被烧掉到地址0x000…，我们知道所有未来的以太坊模块仍将烧掉5 ETH。这与CBC未来的协议状态类似（Barnab_Monnot在这里提供了很好的例子！）。

我们可以将逐渐限制可能的未来的过程可视化为一个无限大的“锥形”可能性，每当我们挖掘并最终确定一个新区块时，这些可能性就会缩小。

注意，在L1中对可能的未来状态的所有限制都是通过挖掘并形成关于（最终确定）新块的共识来完成的 - 这个过程在EVM内产生不可逆的状态转换。

概念2：本地信息

L2利用本地信息（例如链下消息）扩展共识协议。 例如带符号的通道更新，或plasma区块的包含证明。

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

概念3：本地假设

OVM程序定义了基于本地信息确定以太网状态可能的假设。这可以表示为函数satisfies_assumptions（guess，ethereum_state，local_information）=》 true / false。如果satisfies_assumptions（。..）返回true，那么ethereum_state可以基于这些特定的假设和我们的local_information。

在许多L2解决方案中，这采取“争议活跃假设”的形式。例如，通道中的参与者假设他们将对任何恶意撤回提出异议。因此，对于包含恶意、无可争议的退出的任何以太坊状态，我们都会返回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个以太坊币。而无需启动链上交易！

概念5：乐观的期货圆锥体

请记住，“以太坊期货锥”仅受最终确定块的限制-这是一个完全可追溯的过程。在最后一节中，我们回顾了一种乐观的方法，这种方法基于本地信息和本地对未来的假设来限制期货，这是一个前瞻性的过程。这两种方法可以相互“分层”，以充分利用这两个领域：区块链共识的安全性，以及本地消息传输的速度、效率和隐私。

我们可以用一个期货锥体来可视化这个混合过程，这个锥体不仅在每个块之后限制未来的以太坊状态，而且基于本地信息限制块之间的未来状态。在OVM中，决定一个新的限制被认为是“状态转换”。

统一语言

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

· 零确认交易

· 闪电网络

· 跨分片状态方案

· plasma，通道，Truebit

在这篇文章的第2部分中，我们将扩展这种语言，并展示如何通过构造正确的方法激励特定的OVM运行时。基于一阶逻辑，它支持现有的L2设计 - 包括ETH2的设计。

但是首先，如果你和我们一样古怪，想要看一些奇特的数学，下面是我们刚刚回顾的关键概念的形式化：

更进一步：构建一个OVM runtime

当意识到L2可以用统一的语言来描述时，我们很快发现：我们如何使它有用？我们能创建一个通用的二级运行时环境，支持不同的二级设计吗？

事实证明，对于广泛的OVM程序，我们是可以的。诀窍是建立一个争议合同，解释OVM所基于的相同数学表达式。这使得用谓词逻辑编写的高级语言成为可能。

普遍争议合同

为此，我们创建了一个仲裁合同处理用户提交的“索赔”表达式，该表达式的值为真/假。例如，“hash X的预映像不存在。”

争议涉及逻辑上相互矛盾的反索赔。例如，“hash x的preimage确实存在”将与第一个声明相矛盾。这概括了二级语言的“挑战”：到了最后，所有的争议都是逻辑矛盾（不能都是真的）。

在争议超时后，合同可以对无异议的索赔作出真实的裁决。然而，如果出现矛盾，就需要做出选择。判断真/假语句的逻辑称为断言演算。

断言2.0（Predicates）

在开发广义Plasma时，我们认识到可插拔的“断言合约”支持自定义乐观执行。我们现在理解的是，一个可插入的断言系统不是广义plasma，而是广义第2层。

断言合约是逻辑上的“评估者”——决定输入的是真是假。关键是他们可以根据其他断言来决定。这就意味着一小组交互断言可以仲裁大量的L2系统。

断言实例

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

NOT

该断言执行逻辑否定：NOT（aPredicate， anInput），声称aPredicate（anInput）可能会引发矛盾。

AND

该断言是逻辑AND运算符，采用形式AND（predicate1，input1，predicate2，input2）。它可以与NOT（predicate1，input1）或NOT（predicate2，input2）相矛盾。

WITNESS_EXISTS

此断言声称存在某些见证数据：WITNESS_EXISTS（verifier， parameters） 。它是使用活跃度假设给L2系统提供的基本构建块区块链。只有当它收到一些witness，类似verifier.verify（parameters， witness） 返回true时，它才会确定为真。

UNIVERSAL_QUANTIFIER

这个断言代表基于一些量词（“such that”）的通用量化（“for all”） - UNIVERSAL_QUANTIFIER（aQuantifier，aPredicate）。当且仅当aQuantifier.quantify（someInput）返回true时，它与NOT（aPredicate，someInput）相矛盾。

组成状态通道

一类被广泛理解的2层系统是状态通道，所以让我们用断言组成一个状态通道。退出状态通道就像声称以下内容：“对于所有状态更新，其nonce值高于此withdrawn_update，所有通道参与者都不存在一致签名。”

那么，对于普遍争议合同，我们会声称如下：

UNIVERSAL_QUANTIFIER（HAS_HIGHER_NONCE_QUANTIFIER（withdrawn_update），NOT（WITNESS_EXISTS（VERIFY_MULTISIG，withdrawn_update.participants）））

对于Math人员，这可能看起来更熟悉如下表达式：

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

乐观的未来

由于断言很少，这种通用争议合约可以仲裁许多L2系统：plasma风格，状态通道，乐观的交叉分片状态方案，Truebit等。断言运行时为每种方法提供了一个共享平台 - 支持改进的开发人员工具。它有效地将L2开发人员的工作减少了一半，因为谓词表达式在链上和链外解释。

除了断言runtime，ovm还有更广泛的含义：

· 沟通-先前定制概念的数学模型。

· 互操作性-所有乐观执行的共享内存。

· 安全性-二级语言和断言runtime的形式证明。