Try   HackMD

Plasma Chamber Spec(OVM version)

Introduction

Hello! This document describes Cryptoeconomics Lab's L2 client and framework specification.

Who should read this document

This document is written primarily for developers who will use our OVM core framework.

  • Developers who wants to contribute to develop our OVM client should read SDK and framework spec described here (link).
  • Developers who want to integrate our OVM framework to new blockchain system should read L1 adaptor spec described here (link).
  • Developers who want to contricute to OVM language and L2 smart contract should read OVM spec and DSL section.

Background

What is OVM?

Universal Client-

CEL's framewor- k

Since OVM is concept we had to implement concrete system to benefit from OVM's- advantage.
CEL's framework is making OVM real by some components, OVM contract, OVM client and compiler.

Contributers

Cryptoeconomics Lab, inc.
OVM was proposed by Plasma Group.

Core Design

  • L1 agnostic design
  • Hybrid Layer 2 construction using OVM
  • Multi-platform design

Once developer write the appilcation, it runs on many L1 and many platforms.
And also they don't have to write less client logic as possible.

table of contents

  • SDK Spec
  • Framework Spec
  • L1 Adaptor
  • Client Spec
  • OVM Spec

Whole Architecture

Compatibility

Serialization

Plasma Chamber uses ethereum ABI encoding.

Github repositories of our implementation

Client Core: L1 agnostic OVM Client.
Ethereum Client: Ethereum specific L2 implementation using Client Core.
Lite Client: Plasma specific lite client using ethereum client.
Contract:　group of contracts that are needed to support OVM’s claim decision.

Plasma SDK Spec

Basic APIs

  • getBalance

Send Transaction API

Query API

Great step to query language by @tkmct

L1 Adaptor Spec

The main purpose of implementing L1 Adaptor is to support new Layer 1 blockchain.
Developer can implement L1 Adaptor following interfaces below.

  • Coder
  • Wallet
  • ContractWrapper
  • EventWatcher

Coder

Coder provides Encoder for specific Layer 1 block chain. Developer can implement Encoding adapted new blockchain.

L1 adaptor must implements Encoder and Decoder for following primitive types.

  • Address
  • BigNumber
  • Bytes
  • Tuple
  • Struct
  • List

Wallet

Wallet's responsibility is key management. Wallet provides L1 specific private key management ways.

Wallet Class

ContractWrapper and EventWatcher

ContractWrapper and EventWatcher provides concrete interface to access L1 Contract.

AdjudicatorContract Class

CommitmentContract Class

DepositContract Class

ERC20Contract Class

OwnershipPayout Class

Examples

Client Spec

Design client spec to fit many platforms such as mobile phone, browser and micro computer.

https://hackmd.io/3003WCghTou-oXGBcTmuUg?both

OVM Spec

Overview

OVM is the concept to standardize L2 dispute logic. L2 developers write property to define dispute logic for Layer 2 protocol.
Every properties are claimed to the same Contract called Adjudication Contract. Properties are written by predicate logic and it can be prove to true or false under dispute logic.
For example, users deposit their asset to Deposit Contract and finally withdraw asset from Deposit Contract. In this scenario, Property stands for the condition which users can withdraw money from Deposit Contract.
In this document, we describe how we can implement OVM contract.

Property

Property stadns for dispute logic and we can claim every Properties to Adjudicator Contract. Property has its predicate address and array of input.

e.g.) This claim stands for the preimage of hash doesn't exist.

PreimageNotExists(hash) := Not(∃preimage ∈ Bytes(): IsValidPreimage(hash, preimage))

In this case, the PreimageNotExists(hash) property is like following structure.

{
  predicateAddress: Not.address,
  inputs: [{
    predicateAddress: ThereExists.address,
    inputs: ["preimage", {
      predicateAddress: IsValidPreimage,
      inputs: [hash, "preimage"]
    }]
  }]
}

e.g.) Plasma Checkpoint Property stands for history of StateUpdate is valid.

Checkpoint(su) := ∀b < B: ∀su ∈ SU(): su().

Inputs of Property

Primitive Type size description
Address 20 encoded by L1 specific Coder
Bytes 20- bytes
Integer 32 encoded by L1 specific Coder
Property Nested property will be encoded by Coder
Range 64 encoded by L1 specific Coder
Constant 1-19 "C" + bytes(constant value)
Label 1-19 "L" + bytes
Variable 1-19 "V" + bytes(variable name)

Decider and Quantifier

We are using quantifier elimination technich to make OVM contract imeplementation simple.
There are 2 rules. So evetything is decider in our implementation.

|original proposition|eliminated|
|–-|–-|–-|
|∀b∈Quantifier(a):Foo(b)|∀b∈Bytes(a):Not(Quantifier(b, a)) or Foo(b)|
|∃b∈Quantifier(a):Foo(b)|∃b∈Bytes(a):Quantifier(b, a) and Foo(b)|

Local information

Deciders use local information to make decision.

Contract Spec

Adjudacation Contract

claimProperty

Claims property and instantiate new challenge game.

isDecided

Gets the claim is decided or not.

decideClaimToTrue

Set the game decision true whose dispute period has passed.

decideClaimToFalse

Set the game decision false when its challenge is set true.

removeChallenge

Removes challenge whose decision is set as false.

setPredicateDecision

This is called from Predicate. It sets a game decision. For example, you know signature of IsValidSignature(message, address, signature), you can set the game decision true which has this claim through IsValidSignature predicate.

challenge

Adds new challenge game. AC must check the challenge is valid of parent game.

Predicate

Required functions of each Predicate

  • isValidChallenge
  • decide

isValidChallenge validates valid child node of game tree. I explain game tree.

I write the "challenge rule table" defining challenge function which applies the challenge table below recursively.
For example, challenge(¬p) = p.

Valid Challenge

A challengeInput B
¬p ∅ B,p
p0 ∧p1 i ∈ {0,1} B,¬pi | challenge(pi)
p0 ∨p1 ∅ B,¬p0 ∧¬p1
∃x ∈ X : p(x) ∅ B, ∀x ∈ X : ¬p(x)
∀x ∈ X : p(x) t∈X B, ¬p(x/t) | challenge(p(x/t))

If we have ∀x ∈ X : ∀y ∈ Y : p(x, y), challenge is ¬p(x/s,y/t).
"|" means if left isn't atomic.

Immediately decide table

original witness condition
P_0 ∨ P_1 i decide(p_i)
¬¬P ∅ decide(P)
∃x ∈ X : p(x) t∈X decide(p(x/t))
P_0 ∧ P_1 ∅ decide(P_0) and decide(P_1)

Deposit Contract example

An example of Plasma deposit contract.
Deposit contract provides checkpoint property.

deposit(amount: uint256, initialStateObject: Property) {
  Range range = calculateNextRange(amount);
  stateUpdate = StateUpdate(range, initialStateObject)
  Property checkpointProperty = checkpoint(range, block_number, stateUpdate)
  storeProperty(checkpointProperty)
}

You can see description here.

Commitment Contract

Commitment contract provides StateUpdate property.

verify_inclusion(state_update): bool {
  return MerkleTree[state_update.block_number].checkMembership(state_update)
}

(TODO: write description)

Plasma Predicate

We can construct Plasma Predicate from atomic predicates.

Plasma predicate can be instantiate as StateObject. StateObject is Property and its inputs differs by each Plasma Predicate.

e.g.) OwnershipPredicate has only owner address in 0 index of inputs.

StateUpdate

struct StateUpdate {
  blockNumber: Integer,
  tokenAddress: Address,
  range: Range,
  stateObject: Property
}

Property({
  address: StateUpdate.address,
  inputs: [depositContractAddress, range, blockNumber, stateObject]
})

Ownership Predicate

Ownership(owner, tx) := ∃sig ∈ Bytes(), IsValidSignature(tx, owner, sig).

Required functions of predicate

  • isValidChallenge
  • decide
  • finalizeExit

(TODO: write description about finalizeExit of Plasma Predicate)

Payout Contract

Domain Specific Language

Predicate Logic

Ownership(owner, tx) := ∃sig ∈ Bytes(), IsValidSignature(tx, owner, sig).

DSL

def ownership(owner, tx) := SignedBy(tx, owner)

Compiling Property

We can compile big property to small single property, and also we can build library for complex property such as atomic swap.

Why compile?

To avoid big property, we need wrapperd decider synthesized by multiple deciders.
However developers don't want to write specific decider and predicate.
So, OVM compiler should compile Properties with free variables.

How compile

https://hackmd.io/@syuhei/rySwGUOvS

Custome generator

If you wanna support new L1 protocol, you can develop specific generators following generator interface and abstract syntax tree of DSL.
We can show 2 examples of generator in https://github.com/cryptoeconomicslab/ovm-compiler/tree/master/packages, solidity-generator and ethereum-generator.(ethereum-generator generates EVM bytecode).

Reference

Atomic Predicates

  • Equal(a, b)
  • IsLessThan(num, upperBound)
  • IsValidSignature(message, signature, publicKey, verifierKey)
  • IsValidHash(hash, preimage)
  • IsContained(sub: Range, range: Range)
  • VerifyInclusion(leaf, token, range, root, inclusion_proof)
  • IsSameAmount(amount, range)
  • VerifyConcat(bytes, a, b)
  • VerifyRoot(root, address, block_number)

Library

  • SignedBy(message, publicKey, verifierKey)
  • IncludedAt(leaf, token, range, root)

Quantifier

  • LessThan(upperBound)
  • Root(address, block_number)
  • Concat(a, b)
  • Hash(preimage)
  • Range(start, end)
  • SU(block_number, token, range?)
  • Tx(token, range, block_number)

Challenges

  • L2 fee mechanism
  • In the case of that clients discard and update local information(O.Rollup)
  • circular reference property
Last changed by 
 
Shuhei Hiya
1
387
Published on HackMD