自于將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的形式證明。