From a89c8cd37a230a191526778d89e21b8ec9fc4f54 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 28 Nov 2024 16:31:38 +0100 Subject: [PATCH 1/9] implement conditional recursion --- src/lib/proof-system/zkprogram.ts | 100 +++++++++++++++++++++++++----- 1 file changed, 86 insertions(+), 14 deletions(-) diff --git a/src/lib/proof-system/zkprogram.ts b/src/lib/proof-system/zkprogram.ts index 2cb0222b3..9c88ac64e 100644 --- a/src/lib/proof-system/zkprogram.ts +++ b/src/lib/proof-system/zkprogram.ts @@ -55,6 +55,7 @@ import { emptyWitness } from '../provable/types/util.js'; import { InferValue } from '../../bindings/lib/provable-generic.js'; import { DeclaredProof, ZkProgramContext } from './zkprogram-context.js'; import { mapObject, mapToObject, zip } from '../util/arrays.js'; +import { Bool } from '../provable/bool.js'; // public API export { @@ -246,6 +247,13 @@ function ZkProgram< PrivateInputs[I] >; }; + proveRecursivelyIf: { + [I in keyof Config['methods']]: ConditionalRecursiveProver< + InferProvableOrUndefined>, + InferProvableOrVoid>, + PrivateInputs[I] + >; + }; proofsEnabled: boolean; setProofsEnabled(proofsEnabled: boolean): void; } & { @@ -468,11 +476,30 @@ function ZkProgram< let regularRecursiveProvers = mapObject(regularProvers, (prover, key) => { return async function proveRecursively_( + conditionAndConfig: Bool | { condition: Bool; domainLog2?: number }, publicInput: PublicInput, ...args: TupleToInstances ) { + let condition = + conditionAndConfig instanceof Bool + ? conditionAndConfig + : conditionAndConfig.condition; + // create the base proof in a witness block let proof = await Provable.witnessAsync(SelfProof, async () => { + let cond = condition.toBoolean(); + if (!cond) { + let publicOutput = ProvableType.synthesize(publicOutputType); + return SelfProof.dummy( + publicInput, + publicOutput, + maxProofsVerified, + conditionAndConfig instanceof Bool + ? undefined + : conditionAndConfig.domainLog2 + ); + } + // move method args to constants let constInput = Provable.toConstant(publicInputType, publicInput); let constArgs = zip(args, methods[key].privateInputs).map( @@ -489,26 +516,55 @@ function ZkProgram< // declare and verify the proof, and return its public output proof.declare(); - proof.verify(); + proof.verifyIf(condition); return proof.publicOutput; }; }); - type RecursiveProver_ = RecursiveProver< - PublicInput, - PublicOutput, - PrivateInputs[K] - >; + type RecursiveProvers = { - [K in MethodKey]: RecursiveProver_; + [K in MethodKey]: RecursiveProver< + PublicInput, + PublicOutput, + PrivateInputs[K] + >; }; - let proveRecursively: RecursiveProvers = mapToObject(methodKeys, (key) => { - if (publicInputType === Undefined || publicInputType === Void) { - return ((...args: any) => - regularRecursiveProvers[key](undefined as any, ...args)) as any; - } else { - return regularRecursiveProvers[key] as any; + type ConditionalRecursiveProvers = { + [K in MethodKey]: ConditionalRecursiveProver< + PublicInput, + PublicOutput, + PrivateInputs[K] + >; + }; + + let proveRecursively: RecursiveProvers = mapObject( + regularRecursiveProvers, + (prover): RecursiveProvers[MethodKey] => { + if (!hasPublicInput) { + return ((...args: any) => + prover(new Bool(true), undefined as any, ...args)) as any; + } else { + return ((pi: PublicInput, ...args: any) => + prover(new Bool(true), pi, ...args)) as any; + } } - }); + ); + let proveRecursivelyIf: ConditionalRecursiveProvers = mapObject( + regularRecursiveProvers, + (prover): ConditionalRecursiveProvers[MethodKey] => { + if (!hasPublicInput) { + return (( + condition: Bool | { condition: Bool; domainLog2?: number }, + ...args: any + ) => prover(condition, undefined as any, ...args)) as any; + } else { + return (( + condition: Bool | { condition: Bool; domainLog2?: number }, + pi: PublicInput, + ...args: any + ) => prover(condition, pi, ...args)) as any; + } + } + ); async function digest() { let methodsMeta = await analyzeMethods(); @@ -546,6 +602,7 @@ function ZkProgram< }, proveRecursively, + proveRecursivelyIf, }, provers ); @@ -1162,6 +1219,21 @@ type RecursiveProver< ...args: TupleToInstances ) => Promise; +type ConditionalRecursiveProver< + PublicInput, + PublicOutput, + Args extends Tuple +> = PublicInput extends undefined + ? ( + condition: Bool | { condition: Bool; domainLog2?: number }, + ...args: TupleToInstances + ) => Promise + : ( + condition: Bool | { condition: Bool; domainLog2?: number }, + publicInput: PublicInput, + ...args: TupleToInstances + ) => Promise; + type ProvableOrUndefined = A extends undefined ? typeof Undefined : ToProvable; From 4a902400f8b8bde106b9f08595962e9a7f8c0fcf Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 28 Nov 2024 16:32:49 +0100 Subject: [PATCH 2/9] self-recursive hash chain example --- src/examples/zkprogram/hash-chain.ts | 59 ++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 src/examples/zkprogram/hash-chain.ts diff --git a/src/examples/zkprogram/hash-chain.ts b/src/examples/zkprogram/hash-chain.ts new file mode 100644 index 000000000..3032e9007 --- /dev/null +++ b/src/examples/zkprogram/hash-chain.ts @@ -0,0 +1,59 @@ +/** + * This shows how to prove a preimage of an arbitrarily long chain of hashes using ZkProgram, i.e. + * "I know x such that hash^n(x) = y". + * + * We implement this as a self-recursive ZkProgram, using `proveRecursivelyIf()` + */ +import { assert, Bool, Field, Poseidon, Provable, ZkProgram } from 'o1js'; + +const HASHES_PER_PROOF = 30; + +const hashChain = ZkProgram({ + name: 'hash-chain', + publicInput: Field, + publicOutput: Field, + + methods: { + chain: { + privateInputs: [Field], + + async method(x: Field, n: Field) { + Provable.log('hashChain (start method)', n); + let y = x; + let k = Field(0); + let reachedN = Bool(false); + + for (let i = 0; i < HASHES_PER_PROOF; i++) { + reachedN = k.equals(n); + y = Provable.if(reachedN, y, Poseidon.hash([y])); + k = Provable.if(reachedN, n, k.add(1)); + } + + // we have y = hash^k(x) + // now do z = hash^(n-k)(y) = hash^n(x) by calling this method recursively + // except if we have k = n, then ignore the output and use y + let z: Field = await hashChain.proveRecursivelyIf.chain( + reachedN.not(), + y, + n.sub(k) + ); + z = Provable.if(reachedN, y, z); + Provable.log('hashChain (start proving)', n); + return { publicOutput: z }; + }, + }, + }, +}); + +await hashChain.compile(); + +let n = 100; +let x = Field.random(); + +let { proof } = await hashChain.chain(x, Field(n)); + +assert(await hashChain.verify(proof), 'Proof invalid'); + +// check that the output is correct +let z = Array.from({ length: n }, () => 0).reduce((y) => Poseidon.hash([y]), x); +proof.publicOutput.assertEquals(z, 'Output is incorrect'); From aa90a40ef207d143cc08693e36f1cd8d4201d674 Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 28 Nov 2024 16:43:50 +0100 Subject: [PATCH 3/9] changelog --- CHANGELOG.md | 3 ++- src/examples/zkprogram/hash-chain.ts | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 159d68def..bc1747b58 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -19,8 +19,9 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm ### Added -- API for recursively proving a ZkProgram method from within another https://github.com/o1-labs/o1js/pull/1931 +- APIs for recursively proving a ZkProgram method from within another https://github.com/o1-labs/o1js/pull/1931 https://github.com/o1-labs/o1js/pull/1932 - `program.proveRecursively.(...args): Promise` + - `program.proveRecursivelyIf.(condition, ...args): Promise` - 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 diff --git a/src/examples/zkprogram/hash-chain.ts b/src/examples/zkprogram/hash-chain.ts index 3032e9007..28071db53 100644 --- a/src/examples/zkprogram/hash-chain.ts +++ b/src/examples/zkprogram/hash-chain.ts @@ -57,3 +57,5 @@ assert(await hashChain.verify(proof), 'Proof invalid'); // check that the output is correct let z = Array.from({ length: n }, () => 0).reduce((y) => Poseidon.hash([y]), x); proof.publicOutput.assertEquals(z, 'Output is incorrect'); + +console.log('Finished hash chain proof'); From 72eba8a1850c18944507781cdec0d3754ad45edb Mon Sep 17 00:00:00 2001 From: Gregor Date: Thu, 28 Nov 2024 16:57:20 +0100 Subject: [PATCH 4/9] make n also a public input --- src/examples/zkprogram/hash-chain.ts | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/src/examples/zkprogram/hash-chain.ts b/src/examples/zkprogram/hash-chain.ts index 28071db53..b009602e3 100644 --- a/src/examples/zkprogram/hash-chain.ts +++ b/src/examples/zkprogram/hash-chain.ts @@ -1,23 +1,33 @@ /** - * This shows how to prove a preimage of an arbitrarily long chain of hashes using ZkProgram, i.e. - * "I know x such that hash^n(x) = y". + * This shows how to prove an arbitrarily long chain of hashes using ZkProgram, i.e. + * `hash^n(x) = y`. * * We implement this as a self-recursive ZkProgram, using `proveRecursivelyIf()` */ -import { assert, Bool, Field, Poseidon, Provable, ZkProgram } from 'o1js'; +import { + assert, + Bool, + Field, + Poseidon, + Provable, + Struct, + ZkProgram, +} from 'o1js'; const HASHES_PER_PROOF = 30; +class HashChainSpec extends Struct({ x: Field, n: Field }) {} + const hashChain = ZkProgram({ name: 'hash-chain', - publicInput: Field, + publicInput: HashChainSpec, publicOutput: Field, methods: { chain: { - privateInputs: [Field], + privateInputs: [], - async method(x: Field, n: Field) { + async method({ x, n }: HashChainSpec) { Provable.log('hashChain (start method)', n); let y = x; let k = Field(0); @@ -34,8 +44,7 @@ const hashChain = ZkProgram({ // except if we have k = n, then ignore the output and use y let z: Field = await hashChain.proveRecursivelyIf.chain( reachedN.not(), - y, - n.sub(k) + { x: y, n: n.sub(k) } ); z = Provable.if(reachedN, y, z); Provable.log('hashChain (start proving)', n); @@ -50,7 +59,7 @@ await hashChain.compile(); let n = 100; let x = Field.random(); -let { proof } = await hashChain.chain(x, Field(n)); +let { proof } = await hashChain.chain({ x, n: Field(n) }); assert(await hashChain.verify(proof), 'Proof invalid'); From d383fe0504c70d5eb81ea89bd7914193a9538c38 Mon Sep 17 00:00:00 2001 From: Gregor Date: Fri, 29 Nov 2024 15:46:58 +0100 Subject: [PATCH 5/9] fixup --- src/lib/proof-system/zkprogram.ts | 1 + 1 file changed, 1 insertion(+) diff --git a/src/lib/proof-system/zkprogram.ts b/src/lib/proof-system/zkprogram.ts index 31d8f42cf..c39d39e55 100644 --- a/src/lib/proof-system/zkprogram.ts +++ b/src/lib/proof-system/zkprogram.ts @@ -502,6 +502,7 @@ function ZkProgram< let cond = condition.toBoolean(); if (!cond) { let publicOutput = ProvableType.synthesize(publicOutputType); + let maxProofsVerified = compileOutput?.maxProofsVerified!; return SelfProof.dummy( publicInput, publicOutput, From 1a903d0b610ac94f8c08a46455cf8234b00f4952 Mon Sep 17 00:00:00 2001 From: Gregor Date: Tue, 17 Dec 2024 17:04:27 +0100 Subject: [PATCH 6/9] add back recursive conditional provers --- src/lib/proof-system/recursive.ts | 102 ++++++++++++++++++++++++------ 1 file changed, 82 insertions(+), 20 deletions(-) diff --git a/src/lib/proof-system/recursive.ts b/src/lib/proof-system/recursive.ts index 23dbd4186..d23ae101a 100644 --- a/src/lib/proof-system/recursive.ts +++ b/src/lib/proof-system/recursive.ts @@ -5,6 +5,7 @@ import { Tuple } from '../util/types.js'; import { Proof } from './proof.js'; import { mapObject, mapToObject, zip } from '../util/arrays.js'; import { Undefined, Void } from './zkprogram.js'; +import { Bool } from '../provable/bool.js'; export { Recursive }; @@ -38,7 +39,13 @@ function Recursive< InferProvable, InferProvable, PrivateInputs[Key] - >; + > & { + if: ConditionalRecursiveProver< + InferProvable, + InferProvable, + PrivateInputs[Key] + >; + }; } { type PublicInput = InferProvable; type PublicOutput = InferProvable; @@ -62,11 +69,17 @@ function Recursive< let methodKeys: MethodKey[] = Object.keys(methods); - let regularRecursiveProvers = mapObject(zkprogram, (prover, key) => { + let regularRecursiveProvers = mapToObject(methodKeys, (key) => { return async function proveRecursively_( + conditionAndConfig: Bool | { condition: Bool; domainLog2?: number }, publicInput: PublicInput, ...args: TupleToInstances - ) { + ): Promise { + let condition = + conditionAndConfig instanceof Bool + ? conditionAndConfig + : conditionAndConfig.condition; + // create the base proof in a witness block let proof = await Provable.witnessAsync(SelfProof, async () => { // move method args to constants @@ -77,6 +90,24 @@ function Recursive< let constArgs = zip(args, privateInputs[key]).map(([arg, type]) => Provable.toConstant(type, arg) ); + + if (!condition.toBoolean()) { + let publicOutput: PublicOutput = + ProvableType.synthesize(publicOutputType); + let maxProofsVerified: 0 | 1 | 2 = + (await zkprogram.maxProofsVerified()) as any; // TODO + return SelfProof.dummy( + publicInput, + publicOutput, + maxProofsVerified, + conditionAndConfig instanceof Bool + ? undefined + : conditionAndConfig.domainLog2 + ); + } + + let prover = zkprogram[key]; + if (hasPublicInput) { let { proof } = await prover(constInput, ...constArgs); return proof; @@ -93,32 +124,48 @@ function Recursive< // declare and verify the proof, and return its public output proof.declare(); - proof.verify(); + proof.verifyIf(condition); return proof.publicOutput; }; }); - type RecursiveProver_ = RecursiveProver< - PublicInput, - PublicOutput, - PrivateInputs[K] - >; - type RecursiveProvers = { - [K in MethodKey]: RecursiveProver_; - }; - let proveRecursively: RecursiveProvers = mapToObject( - methodKeys, - (key: MethodKey) => { + return mapObject( + regularRecursiveProvers, + ( + prover + ): RecursiveProver & { + if: ConditionalRecursiveProver< + PublicInput, + PublicOutput, + PrivateInputs[MethodKey] + >; + } => { if (!hasPublicInput) { - return ((...args: any) => - regularRecursiveProvers[key](undefined as any, ...args)) as any; + return Object.assign( + ((...args: any) => + prover(new Bool(true), undefined as any, ...args)) as any, + { + if: ( + condition: Bool | { condition: Bool; domainLog2?: number }, + ...args: any + ) => prover(condition, undefined as any, ...args), + } + ); } else { - return regularRecursiveProvers[key] as any; + return Object.assign( + ((pi: PublicInput, ...args: any) => + prover(new Bool(true), pi, ...args)) as any, + { + if: ( + condition: Bool | { condition: Bool; domainLog2?: number }, + pi: PublicInput, + ...args: any + ) => prover(condition, pi, ...args), + } + ); } } ); - - return proveRecursively; } type RecursiveProver< @@ -132,6 +179,21 @@ type RecursiveProver< ...args: TupleToInstances ) => Promise; +type ConditionalRecursiveProver< + PublicInput, + PublicOutput, + Args extends Tuple +> = PublicInput extends undefined + ? ( + condition: Bool | { condition: Bool; domainLog2?: number }, + ...args: TupleToInstances + ) => Promise + : ( + condition: Bool | { condition: Bool; domainLog2?: number }, + publicInput: PublicInput, + ...args: TupleToInstances + ) => Promise; + type TupleToInstances = { [I in keyof T]: InferProvable; }; From bff1f194591142744a3c3cc6d55715d0974fcfaa Mon Sep 17 00:00:00 2001 From: Gregor Date: Tue, 17 Dec 2024 17:10:15 +0100 Subject: [PATCH 7/9] fix after merging other pr --- src/lib/proof-system/recursive.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/proof-system/recursive.ts b/src/lib/proof-system/recursive.ts index d23ae101a..bdc6f1031 100644 --- a/src/lib/proof-system/recursive.ts +++ b/src/lib/proof-system/recursive.ts @@ -26,6 +26,7 @@ function Recursive< ...args: any ) => Promise<{ publicOutput: InferProvable }>; }; + maxProofsVerified: () => Promise<0 | 1 | 2>; } & { [Key in keyof PrivateInputs]: (...args: any) => Promise<{ proof: Proof< @@ -94,8 +95,7 @@ function Recursive< if (!condition.toBoolean()) { let publicOutput: PublicOutput = ProvableType.synthesize(publicOutputType); - let maxProofsVerified: 0 | 1 | 2 = - (await zkprogram.maxProofsVerified()) as any; // TODO + let maxProofsVerified = await zkprogram.maxProofsVerified(); return SelfProof.dummy( publicInput, publicOutput, From 6890754b2040c205e67a0898bdec3a306356aa83 Mon Sep 17 00:00:00 2001 From: Gregor Date: Tue, 17 Dec 2024 17:10:24 +0100 Subject: [PATCH 8/9] adapt hash chain example --- src/examples/zkprogram/hash-chain.ts | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/examples/zkprogram/hash-chain.ts b/src/examples/zkprogram/hash-chain.ts index b009602e3..53bc574cf 100644 --- a/src/examples/zkprogram/hash-chain.ts +++ b/src/examples/zkprogram/hash-chain.ts @@ -7,6 +7,7 @@ import { assert, Bool, + Experimental, Field, Poseidon, Provable, @@ -42,10 +43,10 @@ const hashChain = ZkProgram({ // we have y = hash^k(x) // now do z = hash^(n-k)(y) = hash^n(x) by calling this method recursively // except if we have k = n, then ignore the output and use y - let z: Field = await hashChain.proveRecursivelyIf.chain( - reachedN.not(), - { x: y, n: n.sub(k) } - ); + let z: Field = await hashChainRecursive.chain.if(reachedN.not(), { + x: y, + n: n.sub(k), + }); z = Provable.if(reachedN, y, z); Provable.log('hashChain (start proving)', n); return { publicOutput: z }; @@ -53,6 +54,7 @@ const hashChain = ZkProgram({ }, }, }); +let hashChainRecursive = Experimental.Recursive(hashChain); await hashChain.compile(); From 8383bb67450ebad9f88ab3fc07ba415799df39ed Mon Sep 17 00:00:00 2001 From: Gregor Date: Wed, 8 Jan 2025 08:21:13 +0100 Subject: [PATCH 9/9] prune imports and changelog fix --- CHANGELOG.md | 2 +- src/lib/proof-system/zkprogram.ts | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6cf58f4d7..8c3f662cb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,7 +25,7 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm - APIs for recursively proving a ZkProgram method from within another https://github.com/o1-labs/o1js/pull/1931 https://github.com/o1-labs/o1js/pull/1932 - `let recursive = Experimental.Recursive(program);` - `recursive.(...args): Promise` - - `recursive..if.(condition, ...args): Promise` + - `recursive..if(condition, ...args): Promise` - 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 diff --git a/src/lib/proof-system/zkprogram.ts b/src/lib/proof-system/zkprogram.ts index 766f7b03f..01c04322c 100644 --- a/src/lib/proof-system/zkprogram.ts +++ b/src/lib/proof-system/zkprogram.ts @@ -30,7 +30,6 @@ import { unsetSrsCache, } from '../../bindings/crypto/bindings/srs.js'; import { - ProvablePure, ProvableType, ProvableTypePure, ToProvable, @@ -55,8 +54,7 @@ import { import { emptyWitness } from '../provable/types/util.js'; import { InferValue } from '../../bindings/lib/provable-generic.js'; import { DeclaredProof, ZkProgramContext } from './zkprogram-context.js'; -import { mapObject, mapToObject, zip } from '../util/arrays.js'; -import { Bool } from '../provable/bool.js'; +import { mapObject, mapToObject } from '../util/arrays.js'; // public API export {