plasma-group / ovm Goto Github PK
View Code? Open in Web Editor NEWOVM specs & contracts
OVM specs & contracts
Let me introduce Plasma claims which we are working on, for collaboration!
There are two claims for Plasma, checkpoint claim and exit 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.
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.
IncludedAtBlock(block_number, state_update)
in exit claim showing Not(IncludedAtBlock(block_number, state_update)).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.
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.
{
decider: ForAllSuchThatDecider,
input: {
quantifier: LessThanQuantifier,
quantifierParameters: b,
propertyFactory: (blockNumber) => {
return FooDecider(blockNumber)
}
}
}
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
}
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
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
}
}
I'm looking for appropriate solution for this. these are my very rough ideas but I have no concrete solutions yet.
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)
}
}
contract LessThanQuantifier {
quantify(_parameters: ExitableQuantifierParameters, _toQuantify: Property, _implicationProofElement: ImplicationProofElement) {
let bb = _parameters.innerProperty.reduce(_toQuantify)
assert(bb < _parameters.upperBound)
}
}
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:
FTR if it was possible to deploy contracts via Rust/WASM and not Solidity/JS that would be a dream come true... just saying :)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.