-
Notifications
You must be signed in to change notification settings - Fork 141
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
Preconditions #207
Merged
mitschabaude
merged 50 commits into
feature/preconditions-refactor
from
feature/preconditions
Jun 9, 2022
+8,988
−1,690,806
Merged
Preconditions #207
Changes from 1 commit
Commits
Show all changes
50 commits
Select commit
Hold shift + click to select a range
d1d982a
expose verification of tx proofs
mitschabaude a1c97d7
start writing precondition logic
mitschabaude 6aa176f
start adding .get() for account fields
mitschabaude e55897e
move executionstate off of smart contract
mitschabaude 5bf05cd
add method to check equality of two snarky types
mitschabaude bdf4c96
add `account` field to Party, adapt party cloning
mitschabaude 36a9beb
error when getting account fields w/o constraining
mitschabaude 2dc2deb
fix alternate way of signing tx
mitschabaude 9cc14dd
implement assertions on account preconditions
mitschabaude d8adf47
don't hard-code range conditions
mitschabaude 571b5a8
better error message on missing account fields
mitschabaude e80ddea
add logic to fetch protocol state at best tip
mitschabaude 2e2c4e6
renaming
mitschabaude 30c42da
compute precondition class type more intelligently
mitschabaude d6170d9
implement this.network
mitschabaude 8294ec3
make Types.{UInt32, UInt64} distuingishable
mitschabaude 2370bc7
unify this.account impl with this.network
mitschabaude 8c171d0
make type invariants more local
mitschabaude 38b8444
parse fetched preconditions into compatible type
mitschabaude 0225489
add more stuff to Bool
mitschabaude 631f93a
plug in fetching of network state
mitschabaude 0f110aa
allow precondition.get() outside transaction
mitschabaude dab7ed9
add method to simple_zkapp that uses preconditions
mitschabaude ad8dd5f
Merge branch 'main' into feature/preconditions
mitschabaude 08c3517
Merge branch 'main' into feature/verify-proofs
mitschabaude 975baca
fix serve:web script
mitschabaude 187ea84
don't modify function.name, not supported well
mitschabaude 440e92b
add missing methods to worker_spec; fixes proving
mitschabaude 5df9800
Merge pull request #231 from o1-labs/fix/zkapps-web-main
mitschabaude 960c0e9
Merge branch 'feature/preconditions-refactor' into feature/preconditions
mitschabaude 902462c
Merge branch 'main' into feature/verify-proofs
mitschabaude 60999a7
clean variable cache to avoid messing up circuits
mitschabaude 6d4fbdd
check that precondition works in a proof
mitschabaude 6a8a176
tweak uint types
mitschabaude 0a62267
fetch network state more efficiently
mitschabaude 2f0d293
throw when accessing unimplemented precondition
mitschabaude 72ef4f1
fix: properly clean up if precondition check fails
mitschabaude 3db29f1
add unimplemented preconditions
mitschabaude 22def5c
build fixes
mitschabaude 3f497cb
fix ts linting in .test files
mitschabaude 68dc9ac
add timestamp to unimplemented preconditions
mitschabaude 899d14c
add precondition unit tests
mitschabaude d104558
remove unused imports
mitschabaude 118401c
update bindings
mitschabaude 8774937
Merge pull request #208 from o1-labs/feature/verify-proofs
mitschabaude 6b2073f
Merge pull request #235 from o1-labs/feature/preconditions-refactor
mitschabaude 3562b3c
address pr comments
mitschabaude 0d67182
Merge branch 'main' into feature/preconditions
mitschabaude adf7bc9
clean up bindings
mitschabaude 92d2308
update bindings
mitschabaude File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
unify this.account impl with this.network
- Loading branch information
commit 2370bc7e9d736a0442e9c6c3be8e197a2339ff0a
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,11 @@ | ||
import { Circuit, AsFieldElements, Bool, Field, jsLayout } from '../snarky'; | ||
import { | ||
Circuit, | ||
AsFieldElements, | ||
Bool, | ||
Field, | ||
jsLayout, | ||
Types, | ||
} from '../snarky'; | ||
import { circuitValueEquals } from './circuit_value'; | ||
import { PublicKey } from './signature'; | ||
import * as Mina from './mina'; | ||
|
@@ -14,6 +21,9 @@ function preconditions(party: Party, isSelf: boolean) { | |
return { account: Account(party), network: Network(party) }; | ||
} | ||
|
||
// note: please keep the two precondition implementations separate | ||
// so we can add customized fields easily | ||
|
||
function Network(party: Party): Network { | ||
// TODO there should be a less error-prone way of typing js layout | ||
// e.g. separate keys list and value object, so that we can access by key | ||
|
@@ -23,6 +33,15 @@ function Network(party: Party): Network { | |
return preconditionClass(layout, `network`, party, context); | ||
} | ||
|
||
function Account(party: Party): Account { | ||
// TODO there should be a less error-prone way of typing js layout | ||
// e.g. separate keys list and value object, so that we can access by key | ||
let layout = (jsLayout as any).Party.layout[0].value.layout[9].value.layout[1] | ||
.value as Layout; | ||
let context = getPreconditionContextExn(party); | ||
return preconditionClass(layout, `account`, party, context); | ||
} | ||
|
||
function preconditionClass( | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this function is recursive! it produces all the |
||
layout: Layout, | ||
baseKey: any, | ||
|
@@ -80,7 +99,7 @@ function preconditionSubclass< | |
get() { | ||
read.add(longKey); | ||
return (vars[longKey] ?? | ||
(vars[longKey] = getVariable(longKey, fieldType))) as U; | ||
(vars[longKey] = getVariable(party, longKey, fieldType))) as U; | ||
}, | ||
assertEquals(value: U) { | ||
constrained.add(longKey); | ||
|
@@ -105,98 +124,26 @@ function preconditionSubclass< | |
} | ||
|
||
function getVariable<K extends LongKey, U extends FlatPreconditionValue[K]>( | ||
party: Party, | ||
longKey: K, | ||
fieldType: AsFieldElements<U> | ||
): U { | ||
throw Error('todo'); | ||
} | ||
|
||
type AccountPrecondition = Omit<Preconditions['account'], 'state'>; | ||
type AccountKey = keyof AccountPrecondition; | ||
type AccountValueType = PreconditionBaseTypes<AccountPrecondition>; | ||
type Account = PreconditionClassType<AccountPrecondition>; | ||
|
||
function Account(party: Party): Account { | ||
let address = party.body.publicKey; | ||
let { read, vars, constrained } = getPreconditionContextExn(party); | ||
|
||
function precondition<K extends AccountKey>( | ||
path: K, | ||
fieldType: AsFieldElements<AccountValueType[K]> | ||
) { | ||
let longPath = `account.${path}` as const; | ||
return { | ||
get(): AccountValueType[K] { | ||
read.add(longPath); | ||
return (vars[longPath] ?? | ||
(vars[longPath] = getAccountFieldExn( | ||
address, | ||
path, | ||
fieldType | ||
) as FlatPreconditionValue[typeof longPath])) as AccountValueType[K]; | ||
}, | ||
assertEquals(value: AccountValueType[K]) { | ||
constrained.add(longPath); | ||
let property = getPath( | ||
party.body.preconditions, | ||
longPath | ||
) as AccountPrecondition[K]; | ||
if ('isSome' in property) { | ||
property.isSome = Bool(true); | ||
property.value = value as any; | ||
} else if ('lower' in property) { | ||
property.lower = value as any; | ||
property.upper = value as any; | ||
} else { | ||
party.body.preconditions.account[path] = value as any; | ||
} | ||
}, | ||
assertNothing() { | ||
constrained.add(longPath); | ||
}, | ||
}; | ||
} | ||
let [accountOrNetwork, ...rest] = longKey.split('.'); | ||
let key = rest.join('.'); | ||
|
||
function rangePrecondition<K extends 'nonce' | 'balance'>( | ||
path: K, | ||
fieldType: AsFieldElements<AccountValueType[K]> | ||
) { | ||
let longPath = `account.${path}` as const; | ||
return { | ||
...precondition(path, fieldType), | ||
assertBetween(lower: AccountValueType[K], upper: AccountValueType[K]) { | ||
constrained.add(longPath); | ||
let property = getPath( | ||
party.body.preconditions, | ||
longPath | ||
) as AccountPrecondition[K]; | ||
property.lower = lower; | ||
property.upper = upper; | ||
}, | ||
}; | ||
if (accountOrNetwork === 'account') { | ||
let address = party.body.publicKey; | ||
return getAccountFieldExn<any>(address, key, fieldType); | ||
} | ||
|
||
return { | ||
balance: rangePrecondition('balance', UInt64), | ||
nonce: rangePrecondition('nonce', UInt32), | ||
// TODO: OK how we read this from delegateAccount? | ||
delegate: precondition('delegate', PublicKey), | ||
// TODO: no graphql field yet | ||
provedState: precondition('provedState', Bool), | ||
// TODO: figure out serialization | ||
receiptChainHash: precondition('receiptChainHash', Field), | ||
// TODO: OK how we read this from sequenceEvents? | ||
sequenceState: precondition('sequenceState', Field), | ||
// TODO: should we add state? then we should change the structure on `Fetch.Account` which is stupid anyway | ||
// then can just use circuitArray(Field, 8) as the type | ||
}; | ||
throw Error('todo'); | ||
} | ||
|
||
function getAccountFieldExn<K extends keyof AccountValueType>( | ||
address: PublicKey, | ||
key: K, | ||
fieldType: AsFieldElements<AccountValueType[K]> | ||
) { | ||
): AccountValueType[K] { | ||
type Value = AccountValueType[K]; | ||
let inProver = GlobalContext.inProver(); | ||
if (!GlobalContext.inCompile()) { | ||
|
@@ -205,7 +152,7 @@ function getAccountFieldExn<K extends keyof AccountValueType>( | |
throw Error( | ||
`Could not get \`${key}\` on account with public key ${address.toBase58()}. The property may not be available on this account.` | ||
); | ||
let field = account[key] as Value; | ||
let field = account[key] as any as Value; | ||
// in prover, create a new witness with the state values | ||
// outside, just return the state values | ||
return inProver ? Circuit.witness(fieldType, () => field) : field; | ||
|
@@ -271,29 +218,40 @@ const preconditionContexts = new WeakMap<Party, PreconditionContext>(); | |
|
||
// exported types | ||
|
||
// TODO actually fetch network preconditions | ||
type NetworkPrecondition = Preconditions['network']; | ||
type Network = PreconditionClassType<NetworkPrecondition>; | ||
|
||
// TODO: OK how we read delegate from delegateAccount? | ||
// TODO: no graphql field for provedState yet | ||
// TODO: figure out serialization of receiptChainHash | ||
// TODO: OK how we read sequenceState from sequenceEvents? | ||
// TODO: should we add account.state? then we should change the structure on `Fetch.Account` which is stupid anyway | ||
// then can just use circuitArray(Field, 8) as the type | ||
type AccountPrecondition = Omit<Preconditions['account'], 'state'>; | ||
type AccountValueType = PreconditionBaseTypes<AccountPrecondition>; | ||
type Account = PreconditionClassType<AccountPrecondition>; | ||
|
||
type PreconditionBaseTypes<T> = { | ||
[K in keyof T]: T[K] extends RangeCondition<infer U> | ||
? U | ||
? BasicToFull<U> | ||
: T[K] extends FlaggedOptionCondition<infer U> | ||
? U | ||
? BasicToFull<U> | ||
: T[K] extends AsFieldElements<infer U> | ||
? U | ||
? BasicToFull<U> | ||
: PreconditionBaseTypes<T[K]>; | ||
}; | ||
|
||
type PreconditionSubclassType<U> = { | ||
get(): U; | ||
assertEquals(value: U): void; | ||
get(): BasicToFull<U>; | ||
assertEquals(value: BasicToFull<U>): void; | ||
assertNothing(): void; | ||
}; | ||
|
||
type PreconditionClassType<T> = { | ||
[K in keyof T]: T[K] extends RangeCondition<infer U> | ||
? PreconditionSubclassType<U> & { | ||
assertBetween(lower: U, upper: U): void; | ||
assertBetween(lower: BasicToFull<U>, upper: BasicToFull<U>): void; | ||
} | ||
: T[K] extends FlaggedOptionCondition<infer U> | ||
? PreconditionSubclassType<U> | ||
|
@@ -302,6 +260,16 @@ type PreconditionClassType<T> = { | |
: PreconditionClassType<T[K]>; | ||
}; | ||
|
||
type BasicToFull<K> = K extends Types.UInt32 | ||
? UInt32 | ||
: K extends Types.UInt64 | ||
? UInt64 | ||
: K extends Field | ||
? Field | ||
: K extends Bool | ||
? Bool | ||
: never; | ||
|
||
// layout types | ||
|
||
type BaseLayout = { type: 'UInt64' | 'UInt32' | 'Field' | 'Bool' }; | ||
|
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this file is the most important part of this PR. it will be hard to review without local access to see the types, because it contains quite a bit of advanced typing. the goal of doing this advanced typing was to derive everything from OCaml-generated code, and not introduce another hard-coded layer