Merge pull request #1931 from o1-labs/feature/declare-proofs

Introduce recursive proofs from within ZkPrograms

Author: mitschabaude

CHANGELOG.md

@@ -22,6 +22,10 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 ### Added
 
 - `ZkProgram` to support non-pure provable types as inputs and outputs https://github.com/o1-labs/o1js/pull/1828
+- API for recursively proving a ZkProgram method from within another https://github.com/o1-labs/o1js/pull/1931
+  - `let recursive = Experimental.Recursive(program);`
+  - `recursive.<methodName>(...args): Promise<PublicOutput>`
+  - This also works within the same program, as long as the return value is type-annotated
 - Add `enforceTransactionLimits` parameter on Network https://github.com/o1-labs/o1js/issues/1910
 - Method for optional types to assert none https://github.com/o1-labs/o1js/pull/1922
 - Increased maximum supported amount of methods in a `SmartContract` or `ZkProgram` to 30. https://github.com/o1-labs/o1js/pull/1918
@@ -34,6 +38,8 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 ## [2.1.0](https://github.com/o1-labs/o1js/compare/b04520d...e1bac02) - 2024-11-13
 
+### Added
+
 - Support secp256r1 in elliptic curve and ECDSA gadgets https://github.com/o1-labs/o1js/pull/1885
 
 ### Fixed

run-ci-tests.sh

@@ -9,6 +9,7 @@ case $TEST_TYPE in
   ./run src/examples/zkapps/reducer/reducer-composite.ts --bundle
   ./run src/examples/zkapps/composability.ts --bundle
   ./run src/tests/fake-proof.ts
+  ./run src/tests/inductive-proofs-internal.ts --bundle
   ./run tests/vk-regression/diverse-zk-program-run.ts --bundle
   ;;
 

src/bindings

@@ -148,6 +148,7 @@ import * as OffchainState_ from './lib/mina/actions/offchain-state.js';
 import * as BatchReducer_ from './lib/mina/actions/batch-reducer.js';
 import { Actionable } from './lib/mina/actions/offchain-state-serialization.js';
 import { InferProvable } from './lib/provable/types/struct.js';
+import { Recursive as Recursive_ } from './lib/proof-system/recursive.js';
 export { Experimental };
 
 const Experimental_ = {
@@ -162,6 +163,8 @@ const Experimental_ = {
 namespace Experimental {
   export let memoizeWitness = Experimental_.memoizeWitness;
 
+  export let Recursive = Recursive_;
+
   // indexed merkle map
   export let IndexedMerkleMap = Experimental_.IndexedMerkleMap;
   export type IndexedMerkleMap = IndexedMerkleMapBase;

src/index.ts

@@ -655,7 +655,6 @@ type LazyProof = {
   kind: 'lazy-proof';
   methodName: string;
   args: any[];
-  previousProofs: Pickles.Proof[];
   ZkappClass: typeof SmartContract;
   memoized: { fields: Field[]; aux: any[] }[];
   blindingValue: Field;
@@ -2116,14 +2115,7 @@ async function addProof(
 
 async function createZkappProof(
   prover: Pickles.Prover,
-  {
-    methodName,
-    args,
-    previousProofs,
-    ZkappClass,
-    memoized,
-    blindingValue,
-  }: LazyProof,
+  { methodName, args, ZkappClass, memoized, blindingValue }: LazyProof,
   { transaction, accountUpdate, index }: ZkappProverData
 ): Promise<Proof<ZkappPublicInput, Empty>> {
   let publicInput = accountUpdate.toPublicInput(transaction);
@@ -2141,7 +2133,7 @@ async function createZkappProof(
         blindingValue,
       });
       try {
-        return await prover(publicInputFields, MlArray.to(previousProofs));
+        return await prover(publicInputFields);
       } catch (err) {
         console.error(`Error when proving ${ZkappClass.name}.${methodName}()`);
         throw err;
@@ -2151,7 +2143,7 @@ async function createZkappProof(
     }
   );
 
-  let maxProofsVerified = ZkappClass._maxProofsVerified!;
+  let maxProofsVerified = await ZkappClass.getMaxProofsVerified();
   const Proof = ZkappClass.Proof();
   return new Proof({
     publicInput,

src/lib/mina/account-update.ts

@@ -44,13 +44,13 @@ import {
 import {
   analyzeMethod,
   compileProgram,
+  computeMaxProofsVerified,
   Empty,
-  getPreviousProofsForProver,
   MethodInterface,
   sortMethodArguments,
   VerificationKey,
 } from '../proof-system/zkprogram.js';
-import { Proof } from '../proof-system/proof.js';
+import { Proof, ProofClass } from '../proof-system/proof.js';
 import { PublicKey } from '../provable/crypto/signature.js';
 import {
   InternalStateType,
@@ -154,11 +154,6 @@ function method<K extends string, T extends SmartContract>(
   // FIXME: overriding a method implies pushing a separate method entry here, yielding two entries with the same name
   // this should only be changed once we no longer share the _methods array with the parent class (otherwise a subclass declaration messes up the parent class)
   ZkappClass._methods.push(methodEntry);
-  ZkappClass._maxProofsVerified ??= 0;
-  ZkappClass._maxProofsVerified = Math.max(
-    ZkappClass._maxProofsVerified,
-    methodEntry.numberOfProofs
-  ) as 0 | 1 | 2;
   let func = descriptor.value as AsyncFunction;
   descriptor.value = wrapMethod(func, ZkappClass, internalMethodEntry);
 }
@@ -341,8 +336,6 @@ function wrapMethod(
               {
                 methodName: methodIntf.methodName,
                 args: clonedArgs,
-                // proofs actually don't have to be cloned
-                previousProofs: getPreviousProofsForProver(actualArgs),
                 ZkappClass,
                 memoized,
                 blindingValue,
@@ -433,7 +426,6 @@ function wrapMethod(
             {
               methodName: methodIntf.methodName,
               args: constantArgs,
-              previousProofs: getPreviousProofsForProver(constantArgs),
               ZkappClass,
               memoized,
               blindingValue: constantBlindingValue,
@@ -593,10 +585,10 @@ class SmartContract extends SmartContractBase {
       rows: number;
       digest: string;
       gates: Gate[];
+      proofs: ProofClass[];
     }
   >; // keyed by method name
   static _provers?: Pickles.Prover[];
-  static _maxProofsVerified?: 0 | 1 | 2;
   static _verificationKey?: { data: string; hash: Field };
 
   /**
@@ -644,6 +636,7 @@ class SmartContract extends SmartContractBase {
     forceRecompile = false,
   } = {}) {
     let methodIntfs = this._methods ?? [];
+    let methodKeys = methodIntfs.map(({ methodName }) => methodName);
     let methods = methodIntfs.map(({ methodName }) => {
       return async (
         publicInput: unknown,
@@ -657,13 +650,15 @@ class SmartContract extends SmartContractBase {
     });
     // run methods once to get information that we need already at compile time
     let methodsMeta = await this.analyzeMethods();
-    let gates = methodIntfs.map((intf) => methodsMeta[intf.methodName].gates);
+    let gates = methodKeys.map((k) => methodsMeta[k].gates);
+    let proofs = methodKeys.map((k) => methodsMeta[k].proofs);
     let { verificationKey, provers, verify } = await compileProgram({
       publicInputType: ZkappPublicInput,
       publicOutputType: Empty,
       methodIntfs,
       methods,
       gates,
+      proofs,
       proofSystemTag: this,
       cache,
       forceRecompile,
@@ -689,6 +684,17 @@ class SmartContract extends SmartContractBase {
     return hash.toBigInt().toString(16);
   }
 
+  /**
+   * The maximum number of proofs that are verified by any of the zkApp methods.
+   * This is an internal parameter needed by the proof system.
+   */
+  static async getMaxProofsVerified() {
+    let methodData = await this.analyzeMethods();
+    return computeMaxProofsVerified(
+      Object.values(methodData).map((d) => d.proofs.length)
+    );
+  }
+
   /**
    * Deploys a {@link SmartContract}.
    *
@@ -1189,7 +1195,7 @@ super.init();
       try {
         for (let methodIntf of methodIntfs) {
           let accountUpdate: AccountUpdate;
-          let { rows, digest, gates, summary } = await analyzeMethod(
+          let { rows, digest, gates, summary, proofs } = await analyzeMethod(
             ZkappPublicInput,
             methodIntf,
             async (publicInput, publicKey, tokenId, ...args) => {
@@ -1207,6 +1213,7 @@ super.init();
             rows,
             digest,
             gates,
+            proofs,
           };
           if (printSummary) console.log(methodIntf.methodName, summary());
         }

src/lib/mina/zkapp.ts

@@ -54,7 +54,6 @@ it('pickles rule creation', async () => {
   expect(methodIntf).toEqual({
     methodName: 'main',
     args: [EmptyProof, Bool],
-    numberOfProofs: 1,
   });
 
   // store compiled tag
@@ -67,7 +66,8 @@ it('pickles rule creation', async () => {
     main as AnyFunction,
     { name: 'mock' },
     methodIntf,
-    []
+    [],
+    [EmptyProof]
   );
 
   await equivalentAsync(
@@ -133,7 +133,6 @@ it('pickles rule creation: nested proof', async () => {
   expect(methodIntf).toEqual({
     methodName: 'main',
     args: [NestedProof2],
-    numberOfProofs: 2,
   });
 
   // store compiled tag
@@ -146,7 +145,8 @@ it('pickles rule creation: nested proof', async () => {
     main as AnyFunction,
     { name: 'mock' },
     methodIntf,
-    []
+    [],
+    [EmptyProof, EmptyProof]
   );
 
   let dummy = await EmptyProof.dummy(Field(0), undefined, 0);

src/lib/proof-system/proof-system.unit-test.ts

@@ -16,15 +16,18 @@ import type { Provable } from '../provable/provable.js';
 import { assert } from '../util/assert.js';
 import { Unconstrained } from '../provable/types/unconstrained.js';
 import { ProvableType } from '../provable/types/provable-intf.js';
+import { ZkProgramContext } from './zkprogram-context.js';
 
 // public API
-export { ProofBase, Proof, DynamicProof };
+export { ProofBase, Proof, DynamicProof, ProofClass };
 
 // internal API
 export { dummyProof, extractProofs, extractProofTypes, type ProofValue };
 
 type MaxProofs = 0 | 1 | 2;
 
+type ProofClass = Subclass<typeof ProofBase>;
+
 class ProofBase<Input = any, Output = any> {
   static publicInputType: FlexibleProvable<any> = undefined as any;
   static publicOutputType: FlexibleProvable<any> = undefined as any;
@@ -40,6 +43,27 @@ class ProofBase<Input = any, Output = any> {
   maxProofsVerified: 0 | 1 | 2;
   shouldVerify = Bool(false);
 
+  /**
+   * To verify a recursive proof inside a ZkProgram method, it has to be "declared" as part of
+   * the method. This is done by calling `declare()` on the proof.
+   *
+   * Note: `declare()` is a low-level method that most users will not have to call directly.
+   * For proofs that are inputs to the ZkProgram, it is done automatically.
+   *
+   * You can think of declaring a proof as a similar step as witnessing a variable, which introduces
+   * that variable to the circuit. Declaring a proof will tell Pickles to add the additional constraints
+   * for recursive proof verification.
+   *
+   * Similar to `Provable.witness()`, `declare()` is a no-op when run outside ZkProgram compilation or proving.
+   * It returns `false` in that case, and `true` if the proof was actually declared.
+   */
+  declare() {
+    if (!ZkProgramContext.has()) return false;
+    const ProofClass = this.constructor as Subclass<typeof ProofBase>;
+    ZkProgramContext.declareProof({ ProofClass, proofInstance: this });
+    return true;
+  }
+
   toJSON(): JsonProof {
     let fields = this.publicFields();
     return {