Plasma Group Blog
Published in

Plasma Group Blog

It’s basically just the Oracle Virtual Machine + Eclipse IDE *on the blockchain*. Java’s back baby.

Introducing the OVM

A Correct-by-Construction Approach to Layer 2

In this post we describe the Optimistic Virtual Machine (OVM): a virtual machine designed to support all layer 2 (L2) protocols. Its generality comes from a reframing of L2 as an “optimistic” fork choice rule layered on top of Ethereum. The formalization borrows heavily from CBC Casper research, and describes . This implies a possible unification of all “layer 2 scalability” constructions (Lightning, Plasma, etc) under a single theory and virtual machine: the OVM.

This post will:

  1. Introduce the language of the OVM.
  2. Describe how a class of L2 applications can be compiled end-to-end using a universal dispute contract.

Part 1: Describing L2 With a Unified Language

Layer 1 (L1) gives us a trusted, but expensive, virtual machine (VM). Layer 2 provides an interface for efficiently using the expensive L1 VM — instead of transactions directly updating the L1 state, we use off-chain data to guarantee what happen to L1 state. We call this guarantee an “optimistic decision.”

We will soon describe this process as part of the OVM’s state transition function. However, first let’s build intuition for what we mean by “restrict expectation of future L1 state” with a few key concepts.

🔑 Concept 1: The Ethereum Futures Cone

One can imagine future Ethereum states as an infinite expanse which contains everything that could ever happen to the blockchain. Every transaction that could be signed, every DAO that could be hacked — all possible futures. To avoid cliché this post will not mention the word: “quantum.”

However, even in the face of infinite futures we can still restrict possible futures based on the Ethereum Virtual Machine’s rules. For example, in the EVM, if 5 ETH has been burned to the address 0x000…, we know that all future Ethereum blocks will still have 5 ETH burned. This parallels CBC’s future protocol states (great illustrations by Barnabé Monnot here!).

We can visualize the process of gradually restricting possible futures as an infinitely large “cone” of possibilities that shrinks every time we mine & finalize a new block.

Animation of the Ethereum futures cone. If Alice Burns 5 ETH, she knows it’s burned in all possible future blocks.

🔑 Concept 2: Local Information

L2 extends the consensus protocol with local information (eg. off-chain messages). For example, a signed channel update, or an inclusion proof for a plasma block.

Off-chain message passing… Vizzzualized!

The OVM uses this local information to make we call a new decision an OVM state transition. But first, the OVM must define assumptions which it uses to derive possible future Ethereum states.

🔑 Concept 3: Local Assumptions

OVM programs define assumptions which, based on local information, determines what Ethereum states are possible. This can be expressed as a function satisfies_assumptions(assumptions, ethereum_state, local_information) => true/false. If satisfies_assumptions(...) returns true then the ethereum_state is possible based on these particular assumptions, and our local_information.

In many L2 solutions, this takes the form of a “dispute liveness assumption.” For example, participants in a channel assume that they will dispute any malicious withdrawal. So, we return false for any Ethereum state which contains a malicious, undisputed withdrawal.

Two forks, one where `satisfies_assumptions(…)` returns true, the other in which it returns false based on the “dispute liveness assumption.”

🔑 Concept 4: Optimistic Decisions

With our local assumptions eliminating impossible futures, we may finally make “optimistic decisions” about the future. The following would be a common optimistic decision in a payment channel:

The Last 🔑: The Optimistic Futures Cone

Remember that the “Ethereum futures cone” was only restricted by finalizing blocks — an entirely retrospective process. In the last section we reviewed an optimistic approach which restricts futures based on and about the future — a prospective process. These two approaches may be “layered” on top of one-another to get the best of both worlds: the security of blockchain consensus, plus the speed, efficiency, & privacy of local message transfer.

We can visualize this hybrid process with a futures cone that not only restricts future Ethereum states after each block, but also restricts future states between blocks based on local information. Deciding on a new restriction is considered a “state transition” in the OVM.

Alice’s Optimistic Futures Cone “narrows” when she receives new off-chain messages.

A Unified Language

The above concepts may be used as the basis of a shared language and execution model for layer 2. This includes:

- Zero Confirmation Transactions
- The Lightning Network
- Cross-shard state schemes
- Plasma, Channels, Truebit
…and more — all within a shared notation.

In part 2 of this post, we will expand upon this language and show how the correct-by-construction approach motivates a specific OVM runtime. Based on first-order logic, it supports existing L2 designs —including those for ETH2.

But first, if you’re weird like us and want to see some fancy maths, the following is a formalization of the key concepts we just reviewed:

A Step Further: Building an OVM Runtime

Excited by the realization that L2 can be described in a unified language, we soon found ourselves asking: how do we make this useful? Can we create a generic L2 runtime environment, supporting different L2 designs?

It turns out, for a broad class of OVM programs, we can. The trick is to build a dispute contract which interprets the same mathematic expressions the OVM is based on. This enables a high-level language written in predicate logic.

The Universal Dispute Contract

To do this, we create an arbitration contract handling user-submitted “claims”–expressions which evaluate to true/false. For example, “the preimage to hash X does NOT exist.”

Disputes involve counter-claims which logically contradict. For example, “the preimage to hash X DOES exist” would contradict the first claim. This generalizes L2 “challenges”: at the end of the day, all disputes are logical contradictions (they can’t both be true).

After a dispute timeout, the contract can decide true for an unchallenged claim. However, if a contradiction is shown, it needs to make a choice. The logic of decisions about true/false statements is called predicate calculus.

Predicates 2.0

In developing generalized plasma, we realized that pluggable “predicate contracts” enabled custom optimistic execution. What we now understand is that a pluggable system of predicates isn’t generalized plasma — . In this light, a plasma contract is just a composition of predicates.

Predicate contracts are the logical “evaluators” — deciding true or false on inputs. Critically, they can decide based on other predicates. This means a small set of interacting predicates can arbitrate a vast number of L2 systems.

Example Predicates

Let’s go over some example predicates used in first-order logic.

NOT
This predicate performs a logical negation: NOT(aPredicate, anInput). It can be contradicted by claiming aPredicate(anInput).

AND
This predicate is the logical AND operator, taking the form AND(predicate1, input1, predicate2, input2) . It can be contradicted by either NOT(predicate1, input1) or NOT(predicate2, input2) .

WITNESS_EXISTS
This predicate claims some witness data exists: WITNESS_EXISTS(verifier, parameters) . It is a fundamental building block blockchains give to L2 systems using a liveness assumption. It decides true only if it receives some witness such that verifier.verify(parameters, witness) returns true.

UNIVERSAL_QUANTIFIER
This predicate represents universal quantification (“for all”) based on some quantifier (“such that”)— UNIVERSAL_QUANTIFIER(aQuantifier, aPredicate) . It contradicts with NOT(aPredicate, someInput) if and only if aQuantifier.quantify(someInput) returns true.

Composing a State Channel

A class of widely-understood layer 2 systems is state channels, so let’s compose a state channel with predicates. Withdrawing from a state channel is like claiming the following: “For all state updates with a higher nonce than this withdrawn_update, there does not exist a unanimous signature by all channel participants.”

To the universal dispute contract, then, we would claim the following:

UNIVERSAL_QUANTIFIER(HAS_HIGHER_NONCE_QUANTIFIER(withdrawn_update), NOT(WITNESS_EXISTS(VERIFY_MULTISIG, withdrawn_update.participants)))

For Math folks, this might look more familiar as the following expression:

Thus, state channels can be built by composing four simple predicates.

An Optimistic Future

With very few predicates, this universal dispute contract can arbitrate many L2 systems: plasma flavors, state channels, optimistic cross-shard state schemes, Truebit, and so on. The predicate runtime provides a shared platform for each approach — enabling improved developer tooling. It effectively cuts the work of L2 developers in half because the predicate expressions are interpreted both on-chain and off-chain.

Beyond the predicate runtime, the OVM has broader implications:

  1. Communication — Mathematical models for previously bespoke concepts.
  2. Interoperability — Shared memory for all optimistic execution.
  3. Security — Formal proofs for L2 & the predicate runtime.

Stay tuned for our paper detailing the OVM and the predicate runtime. In the meantime, you can further satiate your appetite with early drafts of the contracts.

Please tweet questions @plasma_group, or better yet join in the discussion at the plasma.build forum–onwards!

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store