A Gentle Guide to the OVM — Plasma Edition —

contradicting property to a claim: ∀X (cat(X) →cute(X))…gotta love this kitten.

Quick Recap

In the last post to update our OVM development plan, we gave a high-level explanation on our OVM implementation architecture, breaking it down into 3 main components, Predicate, Client, and Frontend.
Here is a quick recap of what we’ll deliver/contribute in research for each part,

1. For OVM: develop core contracts that can be a command tower of various applications regardless of L2 scaling constructions.
2. For Predicate: research smart contract development methodologies and versatile combination for wider usage.
3. For Client: build a universal L2 client, including network, storage such as aggregator and light client, etc.
4. For Frontend: provide developer APIs.

As we illustrated our development roadmap in the second half of the post, we are currently developing L2 client for Plasma in Rust in addition to writing core OVM contracts in Solidity. In this post, we will provide an up-close view of our current Plasma implementation on the OVM and talk about the standardization along with other OVM implementation teams clarifying the uniqueness of our development! After reading this post, you will not only see our latest R&D progress since the last post but also become a master of OVM, so let’s get into it together!

📣Attention:
We are currently recruiting developers who can build L2 applications on top of our framework! If you would love to prove that various applications are possible on the OVM design, especially to build those to be showcased at DEVCON5(which really is around the corner, happening on Oct. 6–8), please leave a comment!

Table of contents

This post includes:

• Definitions of the new OVM terminologies
• OVM Architecture Design
• Our Plasma implementation 👈🆕
• Standardization of the OVM and CEL’s dev focus

Glossary: Define New OVM Terminologies

This section provides definitions of OVM terminologies, especially the ones you should be familiar with when you want to investigate the architecture with code-base understanding (links to the source codes of our Plasma implementation (WIP) are in the next section)

Also, I’ll leave amazing resources for those of you want to begin with OVM introductory articles here 😊(creds to PG!):

• Introducing the OVM
• The OVM loves your scaling solution
• Introduction to OVM slides in Japanese (OVM入門編の日本語版資料)

OVM Architecture Design

OVM: L1 Contracts + Client Decider

• Universal Adjudication Contract: the core of the OVM, single theory of commands to all the L2 scaling construction logics
• Deposit & Exit Contract: gateway to L2, a generic contract to handle deposit requests and exit finalizations. Users deposit their assets and initial states from L1 before they start updating them in the L2. In the context of Plasma, checkpoints are also finalized by this contract.
• Predicate Contract: called by Universal Adjudication Contract to validate/dispute the submitted property, always return true or false
• ForAllSuchThat predicate: ForAllSuchThat predicate is one of the basic predicates to attest claims, but it’s a little bit special in a way that it requires all the nested properties to return true. On L1, only one contradiction is needed to turn this claim down.
• ThereExistSuchThat predicate: ThereExistSuchThat predicate requires at least one nested property to return true to confirm the validity of an attested claim. If it passes the dispute period without any true from nested properties.

Therefore it’s important to make sure that inner nested predicates can express a logical negation to complete a fraud-proof verification

• Not predicate: when you want to claim a logical negation of one property A, you can use Not predicate Not(A).
• And predicate: When you want to claim a logical negation of And(A, B), you have to prove Not(A)or Not(B).
• Or predicate: When you want to claim a logical negation of Or(A, B), you have to prove Not(A) and Not(B).
• Other predicates: situation-specific (not necessarily versatile) predicate, say a certain type of witness exists, then this predicate returns true.
• Quantifier: extract a set of states or messages that are necessary to determine whether a claim is valid.
• Decider: predicate-specific contract to decide true/false for each predicate. Contains logic that defines what constitutes valid states stored in the L2 DB. May need a piece of information extracted by Quantifiers to make decisions.

L2 Client

The client can also evaluate submitted claims to true or false by local information.

• Logic: define the way to send transactions (including signing and counter-signing)
• Message Database: stores the data of states that a user would be wanting to exit
• Frontend: interface between users and client

Types of Data in the OVM

On-chain Data

• Claim: a user-submitted statement expressed in the form of first-order logic that can be evaluated to true/false by the Universal Adjudication Contract. Claims can be disputed by its contradicting claim. Should be stated in the form of universal quantifier: for all xxx such that, or existential quantifier: there exists xxx to translate it to first-order-logic

Local Information: off-chain data used by L1 contracts and client deciders to optimistically make decisions on the possible future Ethereum state; the OVM state transition.

• Property: a set of information consisting of a proposition submitted as a claim to Universal Decision Contract and what can validate the claim

Property = {
  predicateAddress: Address, // predicate that validates the property on L1
  input: Bytes, // what is being decided by the predicate
}

• Witness: part of the local information used by Deciders to approve claims
• Implication: a condition where as soon as we gain a piece of information an A, we can immediately deduce that it must also be a B, such as

And(Foo, Bar) -> Foo 
And(Foo, Bar) -> Bar

Plasma PoC Overview

So how do you use this system and express Plasma’s logic? Here is what we designed it! Although this is not a production-ready set of source codes, it would be a good example to explain how Plasma is possible on the OVM.

State updates

To begin with, this is the data structure of state updates that should be included in Plasma blocks.

{
  coin_range: [0, 5000],
  block_number: 10,
  property: {/*property for defining deprecation logic*/}
}

Checkpointing and Exiting

For simple Plasma Cash construction, we require two following types of claims.

Checkpoint claim

Checkpoint claims are created to prove that a specified coin has a valid history. You can see our Rust codes here (link subject to change).

To construct it with predicates. the claim should be expressed as;

plasma_checkpoint(block_number, coin_range) :=
ForAllSuchThat(
  LessThanQuantifier(block_number),
  (b) => {
    ForAllSuchThat(
      WithinBlockRangeQuantifier(b, coin_range),
      state_update,
      (state_update) => {
        IsDeprecated(state_update)
      }
    )
  }
)

This statement should be expressed in English as follows;

State updates within this coin range included in a block less than the current block number are all deprecated.

IsDeprecated function decidesstate_update.property in generalized Plasma. StateUpdate.property would be, for instance, SignedByPredicate(tx, owner_address) to verify signatures of coin owners. WithinBlockRange quantifier's behavior is a little bit more complex than other predicates. This returns all state updates included in a specific coin_range in L2 and verifies their inclusion/exclusion proof.

Exit claim

Exit claims are created to prove that a specified state update has not been deprecated yet.

In the OVM specific format, the claim would be expressed as;

plasma_exit(block_number, state_update) :=
And(
  IncludedAtBlock(block_number, state_update),
  Not(IsDeprecated(state_update)),
  Not(
    ThereExistsSuchThat(
      NewerCheckpoint(block_number)
      (checkpoint) => {
　　      IsIntersected(checkpoint.coin_range, state_update.coin_range)
      }
    )
  )
)

This statement should be expressed in English as follows;

There exists a state update s such that s is included in the block, and for all state updates with a higher nonce than s, there does not exist a deprecation witness

When both of these claims are decided, users can finally finalize their exits and withdraw their assets to L1.

Challenging

Challenge claims are created, of course, when someone wants to challenge some exit. Using the And negation rule (when you want to reject And(A, B), you just have to prove Not(A) or Not(B)) users have to submit a contradiction claim either about inclusion or deprecation.

Therefore, to challenge IncludedAtBlock(block_number, state_update)claiming that one's state update is not included atblock_number, the challenger submit a contradiction claim to an exit as long as the dispute period is not over.

Challenge for checkpoint (invalid history challenge) was complex in Plasma cash spec, but OVM can now make it much simpler. A challenger can prove invalid history showing Not(IsDeprecated(state_update)) as a contradiction against checkpoint claim.

And another way to challenge is to prove deprecation of exit showing IsDeprecated(state_update). This is contradicting to a exit claim.

Also, when users delete an outdated exit, they should show a checkpoint which satisfies IsIntersected(checkpoint.coin_range, state_update.coin_range) and newer than block_number.

L1 <->L2 Interaction

Now, let’s construct an L2 client using the claims logically designed like above. One of the great things of the OVM is we can universally use the same claim design logics not only in L1 but also in L2 clients.

Plasma Client and Aggregator Workflow

• Sender makes transaction and signature, then send these to an aggregator
• Aggregator collects transactions and signature
• The recipient receives local information which includes witness and inclusion proof from sender and aggregator
• The recipient decides exit-claim to verify that receiving coins are valid. Checkpoint claim behave like History Manager
• When a client handles a new exit, the client should decide its exit-claim. If the claim is false, we can challenge the exit!

Plasma client sample

Plasma aggregator client sample

Where to standardize and what CEL is focusing on to build

In order to lay a foundation for greater abstraction and welcome more of the various L2 applications developers, we are trying to standardize the architecture design that would be necessary to share with other constructions. We are now to have lots of discussion about where to standardize here in the OVM repo created by Plasma Group. The journey has just begun, so if you have an idea please join us there for greater standardization.

There’s more to come!

Using the Plasma client implementation/framework, we are going to build some application in ETHBoston happening in the beginning of September. After coming back from Boston, we will be able to provide a cool outcome of the hacking and explain how to develop an application with our framework in detail so stay tuned for the next post!

Also, please go see the links below if you want to explore further on our OVM contracts and Plasma implementation in Rust.

• OVM Contracts repo
• Rust Client repo

And don’t hesitate to tweet us any question/comment if you have one and you can ask us directly in our Telegram group!

• CEL’s official Twitter:

Cryptoeconomics Lab

• CEL’s official Telegram group in English:

Cryptoeocnomics Lab R&D

• CEL’s official Telegram group in Japanese:

JP OVM Dev Group

Co-authors: Shuhei Hiya, Takamichi Tsutsumi, Yuriko Nishijima, CEL research team