CEL's plasma claims design

[syuhei176]

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;;)

[ben-chain]

This is fantastic, thanks for posting!!! 😃Super exciting!

Here is a possible attack which I have been thinking about for generalized plasma checkpoints. I am not sure if this post has it, I think it depends on how isDeprecated works.

What I am worried about is the aggregator including a deprecated claim (for a different coinrange) as the state_upate.property. We do not want this to be used to verifyImplication for a contradiction.

This could be solved by making isDeprecated never return true for verifyImplication. Maybe this was your plan! However, maybe we want the predicates to use the same dispute architecture and be able to use verifyImplication. Do you think that we do?

If we do, one idea is to take the coin_range, block_number, ... and an included data (bad name for another parameter😅) and insert these as bound_variables into some template.

But, I am still not sure if this allows the good feature of the original plasma spec of deploying new predicates once live. So, maybe we still include a property, but one which changes some "implication scope" (like a variable scope) used in verifyImplication. Perhaps this is a generalization of the predicate address whitelist? I'm not sure.

Hope this makes sense! Maybe there is a better solution or I am not realizing something and it is not an attack 😊

[syuhei176]

Thank you for replying! There are certainly a problem that I did not notice 😅

If we do, one idea is to take the coin_range, block_number, ... and an included data (bad name for another parameter😅) and insert these as bound_variables into some template.

I and @tkmct discussed about that. If we understood the problem correctly IsDeprecated should pass the state_update as a arg of state_update.property.predicate.

Pseudo code

IsDeprecated(state_update) := state_update.property.decider(state_update)

In this way, I guess a malicious challenger can't deprecate an exit by the claim with different range.
Is our understanding correct?

And one thing I forgot is RemoveOutdatedExit. Maybe we should add this condition in exit claim.

Not(
  There exists checkpoint such that intersect(checkpoint, state_update.coin_range) and checkpoint.block_number > block_number)