Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] Predicate Notation Version 2 #41

Closed
syuhei176 opened this issue Jul 10, 2019 · 3 comments
Closed

[WIP] Predicate Notation Version 2 #41

syuhei176 opened this issue Jul 10, 2019 · 3 comments
Labels

Comments

@syuhei176
Copy link
Member

@syuhei176 syuhei176 commented Jul 10, 2019

Overview

Derived from #31

What problem can be solved

The problem can be solved is same as the previous version, but this version is more general.

It's hard to explain new predicate each time is created. Researchers need very high context background to understand the behavior of deprecation logic in the discussion. ex) plasma.build We define the notation for predicates to define and share a new predicate quickly and correctly.

How does it work in detail

Dispute scheme and deprecation logic

  • The dispute scheme is to prove the validity of state.
  • The deprecation logic is to prove deprecation of state.
dispution(state, deprecation logic).

Theorem

dispution(deprecationA(state) and deprecationB(state)) = dispution(deprecationA(state)) or dispution(deprecationB(state))
dispution(deprecationA(state) or deprecationB(state)) = dispution(deprecationA(state)) and dispution(deprecationB(state))

Examples

Fee predicate

This formula defamation stands for that fee transfer predicate can be split into fee predicate and ownership predicate.

predicate(proveFee(state) and proveDeprecation(state))
= predicate(proveFee(state)) or predicate(proveDeprecation(state))
1. predicate(proveFee(state) and proveDeprecation(state))
  1. means one predicate has the deprecation logic which is combined from proveFee and proveDeprecation.
2. predicate(proveFee(state)) or predicate(proveDeprecation(state))
  1. means that two exits run at the same time and if at least one exit succeed the whole state should be exitable.

Simple swap predicate

predicate(proveDeprecation(state) and (proveInclusion(state.correspondent) or confirmation(state.correspondent))) or predicate(proveInclusion(state.correspondent) and confirmation(state.correspondent))
= predicate(proveDeprecation(state)) or predicate(proveInclusion(state.correspondent) and confirmation(state.correspondent))
= predicate(proveDeprecation(state)) or predicate(proveInclusion(state.correspondent)) or predicate(confirmation(state.correspondent))

Payment channel predicate

predicate(proveClose(openState)) and channel(deprecation(openState))

Dex predicate

predicate(proveDeprecation(state)) or (predicate(finalizeExit(state.correspondent)) and predicate(proveDeprecation(state.correspondent)))

What topic to research next

@weili-go

This comment has been minimized.

Copy link

@weili-go weili-go commented Jul 23, 2019

This is too abstract, can't resonate, can you give some simple examples?

@syuhei176

This comment has been minimized.

Copy link
Member Author

@syuhei176 syuhei176 commented Jul 23, 2019

@weili-go Hi!

This issue was out of dated.
We will use OVM and predicate 2.0 notation described in these articles and we'll also make examples.
https://medium.com/plasma-group/introducing-the-ovm-db253287af50
https://hackmd.io/@aTTDQ4GiRVyyce6trnsfpg/S1yGmXVxB

ps: We'll write a blog post about our development direction in this week.

@syuhei176 syuhei176 closed this Jul 23, 2019
@weili-go

This comment has been minimized.

Copy link

@weili-go weili-go commented Jul 23, 2019

Very nice.
Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.