Introduce recursive proofs from within ZkPrograms

CHANGELOG.md

@@ -17,20 +17,19 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 ## [Unreleased](https://github.com/o1-labs/o1js/compare/e1bac02...HEAD)
 
-
 ### Added
 
+- API for recursively proving a ZkProgram method from within another https://github.com/o1-labs/o1js/pull/1931
+  - `program.proveRecursively.<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
 
 ### Fixed
 
 - Compiling stuck in the browser for recursive zkprograms https://github.com/o1-labs/o1js/pull/1906
 - Error message in `rangeCheck16` gadget https://github.com/o1-labs/o1js/pull/1920
 
-### Added
-
-- Method for optional types to assert none https://github.com/o1-labs/o1js/pull/1922
-
 ## [2.1.0](https://github.com/o1-labs/o1js/compare/b04520d...e1bac02) - 2024-11-13
 
 ### Added

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/lib/proof-system/proof.ts

@@ -12,6 +12,7 @@ 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 };
@@ -36,6 +37,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 Proof = this.constructor as Subclass<typeof ProofBase>;
+    ZkProgramContext.declareProof({ Proof, proof: this });
+    return true;
+  }
+
   toJSON(): JsonProof {
     let fields = this.publicFields();
     return {

src/lib/proof-system/workers.ts

@@ -1,4 +1,4 @@
-export { workers, setNumberOfWorkers };
+export { workers, setNumberOfWorkers, WithThreadPool };
 
 const workers = {
   numWorkers: undefined as number | undefined,
@@ -15,3 +15,68 @@ const workers = {
 const setNumberOfWorkers = (numWorkers: number) => {
   workers.numWorkers = numWorkers;
 };
+
+type ThreadPoolState =
+  | { type: 'none' }
+  | { type: 'initializing'; initPromise: Promise<void> }
+  | { type: 'running' }
+  | { type: 'exiting'; exitPromise: Promise<void> };
+
+function WithThreadPool({
+  initThreadPool,
+  exitThreadPool,
+}: {
+  initThreadPool: () => Promise<void>;
+  exitThreadPool: () => Promise<void>;
+}) {
+  // state machine to enable calling multiple functions that need a thread pool at once
+  let state: ThreadPoolState = { type: 'none' };
+  let isNeededBy = 0;
+
+  return async function withThreadPool<T>(run: () => Promise<T>): Promise<T> {
+    isNeededBy++;
+    // none, exiting -> initializing
+    switch (state.type) {
+      case 'none': {
+        let initPromise = initThreadPool();
+        state = { type: 'initializing', initPromise };
+        break;
+      }
+      case 'initializing':
+      case 'running':
+        break;
+      case 'exiting': {
+        let initPromise = state.exitPromise.then(initThreadPool);
+        state = { type: 'initializing', initPromise };
+        break;
+      }
+    }
+    // initializing -> running
+    if (state.type === 'initializing') await state.initPromise;
+    state = { type: 'running' };
+
+    let result: T;
+    try {
+      result = await run();
+    } finally {
+      // running -> exiting IF we don't need to run longer
+      isNeededBy--;
+
+      if (state.type !== 'running') {
+        throw Error('bug in ThreadPool state machine');
+      }
+
+      if (isNeededBy < 1) {
+        let exitPromise = exitThreadPool();
+        state = { type: 'exiting', exitPromise };
+
+        // exiting -> none IF we didn't move exiting -> initializing
+        await exitPromise;
+        if (state.type === 'exiting') {
+          state = { type: 'none' };
+        }
+      }
+    }
+    return result;
+  };
+}

src/lib/proof-system/zkprogram-context.ts

@@ -0,0 +1,29 @@
+import { Context } from '../util/global-context.js';
+import type { Subclass } from '../util/types.js';
+import type { ProofBase } from './proof.js';
+
+export { ZkProgramContext, DeclaredProof };
+
+type DeclaredProof = {
+  Proof: Subclass<typeof ProofBase<any, any>>;
+  proof: ProofBase<any, any>;
+};
+type ZkProgramContext = {
+  proofs: DeclaredProof[];
+};
+let context = Context.create<ZkProgramContext>();
+
+const ZkProgramContext = {
+  enter() {
+    return context.enter({ proofs: [] });
+  },
+  leave: context.leave,
+  has: context.has,
+
+  declareProof(proof: DeclaredProof) {
+    context.get().proofs.push(proof);
+  },
+  getDeclaredProofs() {
+    return context.get().proofs;
+  },
+};