Recursion Pt 1 #245

mitschabaude · 2022-06-13T15:50:21Z

Closes Recursion / Proof Composition #247
RFC: Recursion / proof composition RFC #89
This has reduced scope compared to the original goal, to make review easier: It only adds the necessary machinery for merging proofs, and makes it fully work for SmartContracts. That is, smart contracts can now verify their own proofs as well as proofs from other smart contracts
What this PR doesn't do is add an interface to create non-smart-contract proofs. Implementation-wise, this will be only a small addition, which was left for later because it turned out to be an orthogonal change.

This reverts commit 6846bb9.

mitschabaude

Added some comments to aid review:

mitschabaude · 2022-06-16T14:26:06Z

src/examples/simple_zkapp_with_proof.ts

@@ -0,0 +1,129 @@
+import {


This file tests the additions of this PR!

mitschabaude · 2022-06-16T14:29:57Z

src/lib/circuit_value.ts

+
+// TODO properly type this at the interface
+// create recursive type that describes JSON-like structures of circuit types
+function circuitValue<T>(typeObj: any): AsFieldElements<T> {


helper function which provides functionality equivalent to CircuitValue, but is less brittle, doesn't require decorators and can be applied in situations where a circuit value should be created from a plain JS object
i.e.

let MyCircuitValue = circuitValue({ a: Group, b: Bool, c: [Field, Field] });

is equivalent to (but is more precisely typed than)

class MyCircuitValue extends CircuitValue { @prop a: Group; @prop b: Bool; @arrayProp(Field, 2) c: Field[]; constructor(a: Group, b: Bool, c: Field[]) { this.a = a; this.b = b; this.c = c; } }

circuitValue is only used in one place right now but I want to explore further usage, for example to simplify non-decorator ways of specifying circuit inputs

Yeah I think we should move towards the more precise typed versions of things with generics in general.

mitschabaude · 2022-06-16T14:35:15Z

src/lib/mina.ts

@@ -43,7 +45,7 @@ interface Transaction {
  toJSON(): string;
  toGraphqlQuery(): string;
  sign(additionialKeys?: PrivateKey[]): Transaction;
-  prove(): Promise<Transaction>;
+  prove(): Promise<(Proof<ZkappStatement> | undefined)[]>;


only breaking change: tx.prove now returns a list of proofs (one for each party, undefined for parties without proofs) instead of the transaction itself. (Because it was async, returning the transaction wasn't very useful for chaining anyway)

mitschabaude · 2022-06-16T14:36:42Z

src/lib/proof_system.ts

-): any {}
+class Proof<T> {
+  static publicInputType: AsFieldElements<any> = undefined as any;
+  static tag: () => { name: string } = () => {


the new Proof class needs a tag to identify the compiled SmartContract that this proof belongs to

mitschabaude · 2022-06-16T14:39:42Z

src/snarky.d.ts

 }

 declare interface AsFieldElements<T> {
  toFields(x: T): Field[];
  ofFields(x: Field[]): T;
  sizeInFields(): number;
-  check?: (x: T) => void;
+  check(x: T): void;


I made this change to facilitate inferring <T> from and AsFieldElements<T>.
That every circuit type has a check method is now also enforced by Circuit.witness.
@imeckler had mentioned that he should've made check required instead of optional, so I went with that; it makes for simpler types and less special-casing.
This change has minor repercussions throughout the code base

It would have been better if this change was made separately.

Yeah you're right. It was made to enable some typing that I intended to add in this PR, but ended up saving for the next PR.

mitschabaude · 2022-06-16T14:40:07Z

src/snarky.d.ts

-  static sizeInFields(): number;
-}
+// TODO: Add this when OCaml bindings are implemented:
+// declare class EndoScalar {


removed this because it didn't actually exist!

mitschabaude · 2022-06-16T14:40:55Z

src/snarky/wrapper.node.js

-    await Promise.all(global.wasm_workers.map((worker) => worker.terminate()));
-    process.exit(0);
-  }
+  process.exit(0);


shutdown as previously implemented failed to always shut down.. so I just made it exit the node process directly

mrmr1993 · 2022-06-16T14:55:50Z

src/lib/zkapp.ts

-        methodName,
-        (...args: unknown[]) => (instance[methodName] as any)(...args),
-        witnessArgs
+        // TODO: it's problematic that this refers to the instance that was passed in during compile


=> arrow functions should be considered dangerous! If you write function() { ... } instead, you get the this dispatched by call/apply/the method's owner/global object.

fixed 9f60ff4

mrmr1993 · 2022-06-16T14:59:31Z

src/snarky.d.ts

-    verify: (statement: Statement, proof: unknown) => Promise<boolean>;
+  compile: (
+    rules: Pickles.Rule[],
+    statementSize: number


To quote this comment from the Mina-side PR:

Getting the user to manually pass the size of the public input seems error-prone at best, and can lead to under-constrained circuits at worst. Is there not a cleaner way?

I know, for example, that we keep a size_in_field_elements in each Typ.t on the OCaml side. This also has the benefit of not forcing the user to handle an array of field elements when they actually want a structured public input.

I understand the objection. This is not intended as a user-facing API though, it's internal functionality.
That Pickles ends up being exported from snarkyjs is an unintentional side effect of exporting * from this file.
I propose to fix this by removing it from the exports. OK?
(It's a good idea anyway to reduce unintentional exporting from snarkyjs)

I propose to fix this by removing it from the exports. OK?

Sgtm

fixed! e7d69ba

mrmr1993 · 2022-06-16T15:03:35Z

src/snarky.d.ts

 }

 declare interface AsFieldElements<T> {
  toFields(x: T): Field[];
  ofFields(x: Field[]): T;
  sizeInFields(): number;
-  check?: (x: T) => void;
+  check(x: T): void;


It would have been better if this change was made separately.

bkase · 2022-06-27T09:45:03Z

src/lib/circuit_value.ts

+
+// TODO properly type this at the interface
+// create recursive type that describes JSON-like structures of circuit types
+function circuitValue<T>(typeObj: any): AsFieldElements<T> {


Yeah I think we should move towards the more precise typed versions of things with generics in general.

bkase · 2022-06-27T09:45:35Z

src/lib/circuit_value.ts

@@ -278,6 +288,64 @@ function circuitMain(
 }

 let primitives = new Set(['Field', 'Bool', 'Scalar', 'Group']);
+let complexTypes = new Set(['object', 'function']);
+
+// TODO properly type this at the interface


Can you add a todo for unit tests here too?

mitschabaude mentioned this pull request Jun 13, 2022

SnarkyJS proof recursion MinaProtocol/mina#11268

Merged

mitschabaude added 24 commits June 15, 2022 11:00

add helper to create circuit value types

1e80f45

type tweaks to infer int types from their class

7431588

start work on Proof

64a113d

fix source of errors

4decb76

add todo comment

229c0c6

return proofs from tx.prove()

5c6bd86

add TS example which does proving

df77c35

remove unused argument to pickles main

797efa0

fix circuitValue

85576f0

fix circuitValue pt 2

48d908b

implement self proving for smart contracts

6bcf4d1

test self proving in example

46a6fa8

add some potential types for multi-circuit

6846bb9

add useful script for Mina + snarkyjs development

6fea744

fix Pickles types and make self proving work

a61a3bc

Merge branch 'main' into feature/recursion

bdc106b

implement merging proofs from other zkapps

7b14792

errors when trying to merge > 2 proofs

80401ad

make example merge proofs from other zkapps

ae5ff37

fix typedoc

e8fc3a7

check proof verification

576f094

fix shutdown

783e9fb

Revert "add some potential types for multi-circuit"

d227d46

This reverts commit 6846bb9.

Merge branch 'main' into feature/recursion

bd9a768

mitschabaude marked this pull request as ready for review June 16, 2022 14:11

mitschabaude changed the title ~~Recursion~~ Recursion Pt 1 Jun 16, 2022

mitschabaude requested review from MartinMinkov and mimoo June 16, 2022 14:12

mitschabaude commented Jun 16, 2022

View reviewed changes

mrmr1993 reviewed Jun 16, 2022

View reviewed changes

mitschabaude added 2 commits June 16, 2022 22:38

consistently use publicInput

a20cbd9

fix stale SmartContract instance in prover

9f60ff4

mitschabaude removed the request for review from mimoo June 16, 2022 20:45

don't export * from snarky.d.ts

e7d69ba

This was referenced Jun 20, 2022

Recursion, Pt 2 #250

Merged

Update bindings for recursion #251

Merged

bkase approved these changes Jun 27, 2022

View reviewed changes

mitschabaude added 3 commits June 27, 2022 12:38

add TODO

004b509

Merge branch 'main' into feature/recursion

8c9cce6

fix: can't use Bool.true yet

a220a8b

mitschabaude merged commit 0cae7ba into main Jun 27, 2022

mitschabaude deleted the feature/recursion branch June 27, 2022 11:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Recursion Pt 1 #245

Recursion Pt 1 #245

mitschabaude commented Jun 13, 2022 •

edited

mitschabaude left a comment

mitschabaude Jun 16, 2022

mitschabaude Jun 16, 2022

bkase Jun 27, 2022

mitschabaude Jun 16, 2022

mitschabaude Jun 16, 2022

mitschabaude Jun 16, 2022

mrmr1993 Jun 16, 2022

mitschabaude Jun 16, 2022

mitschabaude Jun 16, 2022

mitschabaude Jun 16, 2022

mrmr1993 Jun 16, 2022

mitschabaude Jun 16, 2022

mrmr1993 Jun 16, 2022

mitschabaude Jun 16, 2022

mrmr1993 Jun 16, 2022

mitschabaude Jun 16, 2022

mrmr1993 Jun 16, 2022

bkase Jun 27, 2022

bkase Jun 27, 2022

Recursion Pt 1 #245

Recursion Pt 1 #245

Conversation

mitschabaude commented Jun 13, 2022 • edited

mitschabaude 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

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 commented Jun 13, 2022 •

edited