plasma-group / ovm Goto Github PK

Let me introduce Plasma claims which we are working on, for collaboration!

Plasma claims

There are two claims for Plasma, checkpoint claim and exit claim.

Checkpoint claim

This claim claims that the coin has valid history.

plasma_checkpoint(block_number, coin_range, plasma_contract_address) :=
for all b such thath b < block_number:
   for all state_update such that withinBlockRange(b, coin_range):
      And(
        IncludedAtBlock(state_update),
        IsDeprecated(state_update.property),
        IsEqual(state_update.plasma_contract_address, plasma_contract_address)
      )

This is state_update format.

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

IsDeprecated predicate decides providing property, such as SignedByPredicate.
For client, withinBlockRange returns included state_updates within certain range, and check exclusion if there is no state_update in provided range. For smart contract, check provided state_update is within the coin_range.

Exit claim

This claim claims the state update wasn't deprecated.

plasma_exit(block_number, state_update) :=
And(
  IncludedAtBlock(block_number, state_update, plasma_contract_address),
  Not(IsDeprecated(state_update)),
  IsEqual(state_update.plasma_contract_address, plasma_contract_address)
)

To exit state from Plasma, users should claim both checkpoint and exit claims.

Challenging

• A challenger can prove undecided contradiction of IncludedAtBlock(block_number, state_update) in exit claim showing Not(IncludedAtBlock(block_number, state_update)).
• A challenger can prove deprecation showing IsDeprecated(state_update). This is contradiction of exit claim.
• A challenger can prove invalid history showing And(IncludedAtBlock(state_update), Not(IsDeprecated(state_update))). In this case, exitor should show inclusion of challenging state_update.

Rust Implementation

checkpoint property: https://github.com/cryptoeconomicslab/plasma-rust-framework/blob/8333757a576870575a98a618376aeb84cddbfe16/ovm/src/statements/plasma.rs#L11
exit property: we are still working on this;;)

The topic I wanna clarify in this issue is about predicate design. And I believe PG know the same difficulty. In short, how quantifier quantify inner properties.

Simple example.

I describe the problem using simple example below.

claim(b) :=
For All blockNumber Such That blockNumber < b:
  FooPredicate(blockNumber)

In this formulation, when FooPredicate(1) and FooPredicate(2) are True, claim(3) is True.

The property for client.

{
  decider: ForAllSuchThatDecider,
  input: {
    quantifier: LessThanQuantifier,
    quantifierParameters: b,
    propertyFactory: (blockNumber) => {
      return  FooDecider(blockNumber)
    }
  }
}

The claim for Universal Adjudicator contract.

Claim = {
    predicate: FOR_ALL_SUCH_THAT,
    input: {
        quantifier: LESS_THAN_QUANTIFIER,
        quantifierParameters: b,
        innerProperty: {
          predicate: FooPredicate,
          input: bb // blockNumber
        }
    }
}

let's say, now Alice called claimProperty with b=5.
Anyone can prove contradiction showing "FooPredicate(1) is False". Let's say Bob prove contradiction.
Bob should send the claim like below. It means bb must be less than 5, but isn't constant value.

{
  predicate: FooPredicate,
  input: 1
}

Problem

bb in claim is not constant value but variable. So we should express variable inside innerProperty.
And LessThanQuantifier should verify bb which is used in "innerProperty" is less than upperBound.

note: quantify was called from FOR_ALL_SUCH_THAT.quantify, and FOR_ALL_SUCH_THAT.quantify was called from verifyImplication.

If we implement LessThanQuantifier, quantify should check

• _toQuantify should be same as _parameters.innerProperty applied bb
• bb should be less than parameter.upperBound.

contract LessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
        // `bb` inside _parameters.innerProperty should be less than _parameters.upperBound
      let bb = _implicationProofElement
      assert(bb < _parameters.upperBound)
      // should check that _parameters.innerProperty(bb) and _toQuantify are same property
    }
}

Solutions?

I'm looking for appropriate solution for this. these are my very rough ideas but I have no concrete solutions yet.

Are there any ways to make innerProperty the function returning property?

Can we use create2?

contract LessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
      let bb = _implicationProofElement.bb
      assert(bb < _parameters.upperBound)
      check_equality(_parameters.innerProperty(bb), _toQuantify)
    }
}

innerProperty is reducer?

contract LessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
      let bb = _parameters.innerProperty.reduce(_toQuantify)
      assert(bb < _parameters.upperBound)
    }
}

Specific quantifier?

contract SpecificLessThanQuantifier {
    quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
      assert(_toQuantify.input[0].predicate == FooPredicate)
      assert(_toQuantify.input[0].input.bb < _parameters.upperBound)
    }
}

I would love to explore scaling Aragon DAOs via OVM. Currently options like PoA or Substrate are being considered, but both lack the cryptoeconomic guarantees of Ethereum which I cherish so dearly (decentralization, no censorship, no trusted 3rd parties). Without doing weeks of research, how can I start to get a better idea of:

• if this is currently possible
• if it's possible what that would look like (is it as simple as redeploying vanilla Ethereum contracts or do they have to be rewritten/augmented in some kind of predicate format)?

FTR if it was possible to deploy contracts via Rust/WASM and not Solidity/JS that would be a dream come true... just saying :)