在本文中，我們描述了樂觀虛擬機器（ovm）：一種旨在支援所有2層（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必須定義其用於衍生未來以太坊狀態的假設。
概念2：本地假設
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個以太坊幣。而無需啟動鏈上交易！
概念4：樂觀的期貨圓錐體
請記住，“以太坊期貨錐”僅受最終確定塊的限制-這是一個完全可追溯的過程。在最後一節中，我們回顧了一種樂觀的方法，這種方法基於本地資訊和本地對未來的假設來限制期貨，這是一個前瞻性的過程。這兩種方法可以相互“分層”，以充分利用這兩個領域：區塊鏈共識的安全性，以及本地訊息傳輸的速度、效率和隱私。
我們可以用一個期貨錐體來視覺化這個混合過程，這個錐體不僅在每個塊之後限制未來的以太坊狀態，而且基於本地資訊限制塊之間的未來狀態。在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的形式證明。
