概念1：以太坊期貨圓錐體
注意，在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的形式證明。
