OVM Compiler

This document describes a practical aspect of OVM with implementation.

DEMO

Why we need compiler?

For instance, plasma construction has StateUpdate and it has Property. If Property size is very large, it's hard to send it to aggregator and smart contract. Secondaly, we want to reduce gas cost of dispute. Claim with big property would take high gas cost for dispute.

Thus, we want compile big proposition with free variables to one predicate.

Pre-difinition

Predicate(not atomic proposition) has isValidChallenge method.

Data structure

struct Property {
  predicate: address,
  inputs: bytes[]
}
struct Challenge {
  property: Property,
  challengeInput: bytes
}

A or B

contract OrPredicate {

  function isValidChallenge(property, challenge) {
    assert(challenge.property.predicate == AndPredicate.address)
    assert(challenge.property.inputs[0].predicate == NotPredicate.address)
    assert(challenge.property.inputs[0].inputs[0] == property.inputs[0])
    assert(challenge.property.inputs[1].predicate == NotPredicate.address)
    assert(challenge.property.inputs[1].inputs[0] == property.inputs[1])

  }
}

A and B

contract AndPredicate {
  function isValidChallenge(property, challenge) {
    var choice = property.inputs[challenge.challengeInput]
    assert(challenge.property.predicate == NotPredicate.address)
    assert(challenge.property.inputs[0] == choice)
  }
}

SignedBy

contract SignedByPredicate {

  function decideTrue(property) {
    assert(ecverify(property.inputs[0], property.inputs[1]))
    UAC.decideProperty(property, true)
  }
}

Compile

• Reduce claim size
• Reduce the gas cost of claim
• Reduce challenge cost

The logic to compile

1. Calculate interactive points
2. Generate predicate contracts for each interactive point
3. Each contract has isValidChallenge and decideTrue methods
4. isValidChallenge should check the child interactive point
5. decideTrue should check the property is true using child interactive points

Example

MyPredicate() := ¬∃ tx: Foo(tx) and Bar(tx)

P: ¬∃ tx: Foo(tx) and Bar(tx)
Q: ∃ tx: Foo(tx) and Bar(tx)

P: choose tx1
P: Foo(tx1) and Bar(tx1)

Q: choose ¬Foo(tx1)
P: Foo(tx1)

Q: choose ¬Bar(tx1)
P: Bar(Tx1)

Compiled predicate contract.
isValidChallenge methods are intaractive points.

contract MyPredicate {
  function isValidChallenge(Property property, bytes[] challengeInput, Property challenge): bool {
    if (property.inputs[0] == 1) {
      isValidChallenge1(property, challengeInput, challenge)
    }else if (property.inputs[0] == 2) {
        //...
    }
  }

  function isValidChallenge1(Property property, bytes[] challengeInput, Property challenge): bool {
    // check property is "¬∃ tx: Foo(tx) and Bar(tx)"
    assert(property.inputs[0] == 1)
    // check challenge is "∃ tx: Foo(tx) and Bar(tx)"
    assert(challenge.inputs[0] == 2)
  }

  function decideTrue(Property property, bytes[] witness): bool {
    if (property.inputs[0] == 2) {
      decideTrue2(property, witness)
    }
  }

  function decideTrue2(Property property, bytes[] witness): bool {
    // ∃ tx: Foo(tx) and Bar(tx)
    var tx = witness[0]
    if Foo(tx) and Var(tx) {
      UAC.decideTrue(keccak(property))
    }
  }
}

Library Compiling

Compiled PropertyId

Challenge Compiled Property