Preconditions #207

mitschabaude · 2022-05-26T12:00:52Z

Closes Account / network precondition RFC #179
Adds example of using the new API: https://github.com/o1-labs/snarkyjs/blob/dab7ed9aa93fe95fb88f1b184195de252046704c/src/examples/simple_zkapp.ts#L39
Adds a method for checking deep equality of two party subtypes (where "party subtype" is defined very broadly to be future-proof): 5bf05cd. This is used to check if the user manually modified a precondition, which counts as explicitly constraining the value, to avoid the error that we throw when it's not constrained.

TODOs:

change integration test so that it tests fetching from the graphql URI, and uses preconditions, and ideally is broken up into zkapps that test different features
investigate broken prover and decide if it should be fixed as part of this issue
some precondition fields aren't implemented yet because the logic to parse them from an encoded string is missing. this could be done here or in a follow-up PR

mitschabaude

Some comments to make review easier:

mitschabaude · 2022-06-07T09:05:48Z

src/lib/fetch.ts

@@ -218,34 +245,6 @@ function stringifyAccount(account: FlexibleAccount): FetchedAccount {
  };
 }

-async function checkResponseStatus(


this code block was just moved to the bottom of the file. I often move unimportant / helper-type code to the bottom, and the exported API / most important parts to the top, because I think this makes code more readable

mitschabaude · 2022-06-07T09:07:18Z

src/lib/fetch.ts

@@ -317,6 +347,163 @@ function addCachedAccountInternal(
  };
 }

+async function fetchLastBlock(graphqlEndpoint = defaultGraphqlEndpoint) {


this provides the logic to get the network precondition. we fetch the bestChain, which returns a list of blocks, and take the network state from the last of them. is this OK @bkase?

We can do it in one graphql call — bestChain optionally takes a parameter for the number to pull and goes through a happy path if you put 1 there (executes much faster), so we should add that! Then you can skip the query for the block at a specific height.

very nice, I did that and it became much faster!

mitschabaude · 2022-06-07T09:08:13Z

src/lib/fetch.ts

+  },
+}: FetchedBlock): NetworkValue {
+  return {
+    snarkedLedgerHash: Field.zero, // TODO


some of the network preconditions are not implemented yet, because we lack the logic for parsing these hashes into Fields

Can you make accessing the unimplemented parts of network/account preconditions throw an error instead of silently using the wrong value? This will certainly confuse people I think if we don’t do this.

done 👍🏻

mitschabaude · 2022-06-07T09:13:10Z

src/lib/fetch.ts

@@ -380,3 +567,31 @@ async function makeGraphqlRequest(
    return [undefined, inferError(error)] as [undefined, FetchError];
  }
 }
+
+async function checkResponseStatus(


code moved here from the top of the file

mitschabaude · 2022-06-07T09:18:18Z

src/lib/global-context.ts

  inProver,
  inCompile,
  inCheckedComputation,
 };

+// per-smart-contract context for transaction construction
+type ExecutionState = {


this code was moved here from zkapp.ts. this continues two themes:

breaking apart zkapp.ts because it was too big

doing book-keeping with WeakMap instead of secret properties on public-facing objects

mitschabaude · 2022-06-07T09:29:54Z

src/lib/precondition.ts

+}
+
+function assertPreconditionInvariants(party: Party) {
+  let context = getPreconditionContextExn(party);


this is the function that throws an error if the user used .get() on a account / network field, without explicitly adding a precondition. calling get would have added an entry to context.read. adding a precondition would have added an entry to context.constrained.

mitschabaude · 2022-06-07T09:32:26Z

src/snarky.d.ts

+  /**
+   * The constant [[`Bool`]] that is `true`.
+   */
+  static true: Bool;


I added Bool.true and Bool.false, because in the end it won the community vote :D

mitschabaude · 2022-06-07T09:36:24Z

src/lib/int.ts

  @prop value: Field;
  static NUM_BITS = 64;
+  type = 'UInt64' as const;


I added this field to UInt64, to make the type conform to the interface { value: Field; type: "UInt64" }, which is used to signify UInt64s in the autogenerated party types.
the intention is to make the UInt64 interface distinct from the UInt32 one, to get advanced types in precondition.tsto work. this also fixes a couple of bug sources, where UInt32 could be passed into functions that expected UIn64 and vice versa

Can we use a phantom type here instead of actually polluting the object at runtime? https://dev.to/busypeoples/notes-on-typescript-phantom-types-kg9 You can put the type parameter on the interface to avoid people having to see it when they use Uint64 .

See below, I think I solved it nicely

mitschabaude · 2022-06-07T09:37:24Z

src/lib/int.ts


  constructor(value: Field) {
    super();
    this.value = value;
+    // TODO type breaks Circuit.if for some reason
+    delete (this as any).type;


we actually can't keep the .type property on the class instance.. it's just for typescript

mitschabaude · 2022-06-07T09:47:35Z

src/lib/party.ts

+    this.isSelf = isSelf;
+  }
+
+  static clone(party: Party) {


Before adding this, Partys were just cloned with cloneCircuitValue directly. I changed it because the new account and network fields aren't safely clone-able, due to how they use closures / are attached to a party instance. This new cloning will lose precondition-related metadata attached to a party (i.e. which account / network fields were accessed / constrained). this seems appropriate, because cloning a party also doesn't magically add it to the current transaction

bkase

I don’t know if I believe in the WeakMap over storing secret things on the object.
The benefit is you can easily see everything associated with that entity by looking at the class. When there are WeakMap’s floating around, you have to know where to look to find the extra associated data.

Also, popular and well-thought-out libraries do this (like React), so I don’t think it’s controversial.

What is your reason for reaching for weakmaps here?

If we do end up sticking with WeakMaps, having just one for all the secret things at least mitigates the “hard to find” associated data problem a bit. Rather than one for each kind of associated datum.

bkase · 2022-06-07T14:21:00Z

src/lib/fetch.ts

@@ -317,6 +347,163 @@ function addCachedAccountInternal(
  };
 }

+async function fetchLastBlock(graphqlEndpoint = defaultGraphqlEndpoint) {


We can do it in one graphql call — bestChain optionally takes a parameter for the number to pull and goes through a happy path if you put 1 there (executes much faster), so we should add that! Then you can skip the query for the block at a specific height.

bkase · 2022-06-07T14:23:16Z

src/lib/fetch.ts

+  }
+}`;
+
+type FetchedBlock = {


I look forward to the day when we autogenerate this like we did with transaction. Unfortunately, today is not that day. This is good for now.

bkase · 2022-06-07T14:24:59Z

src/lib/fetch.ts

+  },
+}: FetchedBlock): NetworkValue {
+  return {
+    snarkedLedgerHash: Field.zero, // TODO


Can you make accessing the unimplemented parts of network/account preconditions throw an error instead of silently using the wrong value? This will certainly confuse people I think if we don’t do this.

bkase · 2022-06-07T14:31:29Z

src/lib/int.ts

  @prop value: Field;
  static NUM_BITS = 64;
+  type = 'UInt64' as const;


bkase · 2022-06-07T14:35:11Z

src/lib/int.ts

  @prop value: Field;
  static NUM_BITS = 64;
+  type = 'UInt64' as const;


Can we use a phantom type here instead of actually polluting the object at runtime? https://dev.to/busypeoples/notes-on-typescript-phantom-types-kg9 You can put the type parameter on the interface to avoid people having to see it when they use Uint64 .

bkase · 2022-06-07T14:45:42Z

src/lib/precondition.ts

+  | OptionLayout<BaseLayout>
+  | BaseLayout;
+
+// TS magic for computing flattened precondition types


These types are awesome haha, reminds me of doing this kind of stuff when I was doing web things at Pinterest

bkase · 2022-06-07T14:48:05Z

src/lib/precondition.ts

+}
+
+// helper. getPath({a: {b: 'x'}}, 'a.b') === 'x'
+// TODO: would be awesome to type this


microsoft/TypeScript#12290 😉 (no need to do this now unless you feel an itch for cleanliness)

bkase · 2022-06-07T14:48:47Z

src/snarky.d.ts

+  /**
+   * The constant [[`Bool`]] that is `true`.
+   */
+  static true: Bool;


bkase · 2022-06-07T14:51:10Z

src/snarky/parties-leaves.ts

@@ -12,8 +12,8 @@ export {

 export { toJson, toJsonLeafTypes, toFields, toFieldsLeafTypes };

-type UInt64 = { value: Field };
-type UInt32 = { value: Field };
+type UInt64 = { value: Field; type: 'UInt64' };


Ah I think I solved it with phantom types cleanly:

type FieldLike<N> = { value: Field } type UInt64 = FieldLike<{type: 'UInt64'}>

Unfortunately doesn't seem to solve my use case.. I need UInt64 to not extend UInt32 and vice versa.

I tried the following snippet:

type FieldLike<N> = { value: Field }; type UInt64 = FieldLike<{ type: 'UInt64' }>; type UInt32 = FieldLike<{ type: 'UInt32' }>; type X = UInt32 extends UInt64 ? 'not working' : 'it works!';

For me, X is of type "not working"..

I think the original solution can be improved by making the type prop optional:

type UInt64 = { value: Field; type?: 'UInt64' }; type UInt32 = { value: Field; type?: 'UInt32' };

that way, they don't extend each other and we can just instantiate them without the type field at runtime.

it's still not perfect because the type field shows up in intellisense

That's weird that they extend each other, shows that I do not understand typescript's type system enough.

I think this is good with them optional -- since it appears in intellisense can you use some kind of prefix so people know to avoid it: like _type or $type (I'm not sure if we have a standard for this yet)

bkase · 2022-06-07T14:51:48Z

src/lib/int.ts

  @prop value: Field;
  static NUM_BITS = 64;
+  type = 'UInt64' as const;


See below, I think I solved it nicely

mitschabaude · 2022-06-08T07:43:59Z

I don’t know if I believe in the WeakMap over storing secret things on the object. (...) Also, popular and well-thought-out libraries do this (like React), so I don’t think it’s controversial.

Ok, this is good feedback. I might have overreached with the intention to remove all secret props. Specifically, I'm not sure if I can defend the move of SmartContract._executionState to a weakmap, because that prop mainly gets used internally by the SmartContract class. In that case, I guess it's more natural to make it a private class field, so it's removed from the TS type / doesn't pollute intelli-sense, but is accessible to the class that uses it.

What is your reason for reaching for weakmaps here?

If we do end up sticking with WeakMaps, having just one for all the secret things at least mitigates the “hard to find” associated data problem a bit. Rather than one for each kind of associated datum.

I do think there are cases where weakmaps are better than extra class props, and it's also better to not have them in one place.

For example, the precondition.ts module stores metadata associated with each Party instance in a weakmap. I like the weakmap approach for that because it makes the metadata book-keeping be localized to the module that is concerned with it - precondition.ts. Keeping modules encapsulated helps with understanding and maintaining the code. In this case, seeing a map of precondition-related metadata being initialized on the Party class in party.ts would be more confusing, because there's no other code in party.ts related to that metadata; and when trying to understand the precondition.ts code, it would be confusing that we don't see where that metadata is initialized. It would mix concerns of the Party class with concerns of the precondition module, and the downside is increased code complexity.

An alternative would be to secretly set a property (party as any)._preconditionData = ... inside precondition.ts, but I think this is just not as clean and not as well-typed as maintaining a weakmap for that data. It breaks the "contract" that Party defines, and forces us to use as any whenever we deal with the secret property.

The same reasoning applies for the @state logic that's now encapsulated in state.ts. We used to store _states and _layout() fields on SmartContract subclasses from inside the @state logic. I think it's strictly less confusing and more maintainable now that we have a state-related weakmap inside state.ts, and not mess with the SmartContracts from that module.

Since only precondition.ts / state.ts ever need to be concerned with their respective metadata, I don't see the value of having a central weakmap which combines their stuff. Also, the keys and values of that centralized weakmap would be a mix of completely different things if we do that, which would make accurate typing much harder.

TL;DR, I think both of those weakmaps help with encapsulation, code clarity and strict typing.

@bkase, what do you think of a middle-ground approach where we don't try to avoid private props in principle, but we use weakmaps if a module wants to associate data with objects that originate in a different module? I would revert the _executionState weakmap in that case.

Proof verification

bkase · 2022-06-08T21:55:07Z

Renaming the type? to _type? (or something) + refactoring that WeakMap for executionState and then I'll approve 💯

`@state` refactor

mitschabaude added 19 commits May 26, 2022 18:21

expose verification of tx proofs

d1d982a

start writing precondition logic

a1c97d7

start adding .get() for account fields

6aa176f

move executionstate off of smart contract

e55897e

add method to check equality of two snarky types

5bf05cd

add account field to Party, adapt party cloning

bdf4c96

error when getting account fields w/o constraining

36a9beb

fix alternate way of signing tx

2dc2deb

implement assertions on account preconditions

9cc14dd

don't hard-code range conditions

d8adf47

better error message on missing account fields

571b5a8

add logic to fetch protocol state at best tip

e80ddea

renaming

2e2c4e6

compute precondition class type more intelligently

30c42da

implement this.network

d6170d9

make Types.{UInt32, UInt64} distuingishable

8294ec3

unify this.account impl with this.network

2370bc7

make type invariants more local

8c171d0

parse fetched preconditions into compatible type

38b8444

mitschabaude mentioned this pull request Jun 1, 2022

Consolidate preconditions MinaProtocol/mina#11096 #206

Merged

mitschabaude added 4 commits June 3, 2022 10:00

add more stuff to Bool

0225489

plug in fetching of network state

631f93a

allow precondition.get() outside transaction

0f110aa

add method to simple_zkapp that uses preconditions

dab7ed9

mitschabaude marked this pull request as ready for review June 3, 2022 10:16

mitschabaude added 5 commits June 3, 2022 16:18

Merge branch 'main' into feature/preconditions

ad8dd5f

Merge branch 'main' into feature/verify-proofs

08c3517

fix serve:web script

975baca

don't modify function.name, not supported well

187ea84

add missing methods to worker_spec; fixes proving

440e92b

mitschabaude commented Jun 7, 2022

View reviewed changes

mitschabaude requested a review from bkase June 7, 2022 09:50

mitschabaude added 2 commits June 7, 2022 14:32

Merge branch 'main' into feature/verify-proofs

902462c

clean variable cache to avoid messing up circuits

60999a7

bkase requested changes Jun 7, 2022

View reviewed changes

check that precondition works in a proof

6d4fbdd

mitschabaude added 12 commits June 8, 2022 11:21

tweak uint types

6a8a176

fetch network state more efficiently

0a62267

throw when accessing unimplemented precondition

2f0d293

fix: properly clean up if precondition check fails

72ef4f1

add unimplemented preconditions

3db29f1

build fixes

22def5c

fix ts linting in .test files

3f497cb

add timestamp to unimplemented preconditions

68dc9ac

add precondition unit tests

899d14c

remove unused imports

d104558

update bindings

118401c

Merge pull request #208 from o1-labs/feature/verify-proofs

8774937

Proof verification

mitschabaude added 3 commits June 8, 2022 23:59

Merge pull request #235 from o1-labs/feature/preconditions-refactor

6b2073f

`@state` refactor

address pr comments

3562b3c

Merge branch 'main' into feature/preconditions

0d67182

bkase approved these changes Jun 9, 2022

View reviewed changes

mitschabaude mentioned this pull request Jun 9, 2022

Finish unimplemented preconditions #240

Closed

3 tasks

mitschabaude added 2 commits June 9, 2022 08:54

clean up bindings

adf7bc9

update bindings

92d2308

mitschabaude merged commit e992c87 into feature/preconditions-refactor Jun 9, 2022

mitschabaude mentioned this pull request Jun 9, 2022

Preconditions 2 #241

Merged

mitschabaude deleted the feature/preconditions branch June 30, 2022 07:52

Preconditions #207

Preconditions #207

Conversation

mitschabaude commented May 26, 2022 • edited by ymekuria Loading

mitschabaude left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bkase left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mitschabaude Jun 8, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mitschabaude commented Jun 8, 2022 • edited Loading

bkase commented Jun 8, 2022

mitschabaude commented May 26, 2022 •

edited by ymekuria

Loading

mitschabaude left a comment •

edited

Loading

mitschabaude Jun 8, 2022 •

edited

Loading

mitschabaude commented Jun 8, 2022 •

edited

Loading