自于将L2重新定义为以太坊之上的乐观分叉选择规则。形式化大量借鉴了CBC Casper的研究，并将2层描述为1层共识的直接延伸。这意味着在单一理
自于将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的形式证明。（链三丰）
