Introduce recursive proofs from within ZkPrograms

[mitschabaude]

This PR enables to "declare" a recursively verified proof from within a ZkProgram method. Thus, recursive proofs no longer need to be inputs to the method, and therefore can be abstracted away much more easily.

bindings: o1-labs/o1js-bindings#318

The new low-level way of introducing a proof that hasn't been passed as method argument is as follows:

let proof = await Provable.witnessAsync(MyProof, async () => { /* generate and return proof */  });
proof.declare();
// ... use the proof as if it had been a method argument ...

New Recursion API

see UPDATE below for final version of this API

On top of this, I added an even more pleasant API, which you can use in the typical case where the ZkProgram that produces the inner proof is in scope. For this, assume the proof in question is supposed to come from a method innerProgram.run(). Then, the entire logic above is now encapsulated inside the new property innerProgram.proveRecursively.run():

// inside outer zkprogram method
let output = await innerProgram.proveRecursively.run(...inputs);

note: this expects the inputs (public and private) as arguments and returns the public output -- which is the natural way to think of calling a method.

Internally, we make sure that the inner proof's public input matches what the outer circuit passed in.

Caveats: of course we can't make any statement about the private inputs, because the inner proof inherently doesn't reveal those. so the private inputs must be understood only as hints to the recursive proving. Similarly, the inner proof doesn't guarantee the particular method that was called on the inner program: as usual with recursive proofs, all of the methods can produce it.

An e2e example, that I added to CI and also manually ran in the browser, is at src/tests/inductive-proofs-internal.ts

UPDATE: after discussions, the API was changed to live separately from ZkProgram:

let inner = ZkProgram({ ..., methods: { run: ... });
let innerRecursive = Experimental.Recursive(program);

// inside another -- or even the same -- program:
let output = await innerRecursive.run(...inputs);

[mitschabaude]

@Trivo25 this is ready for review.

In a follow-up PR, I also want to add a conditional version: proveRecursivelyIf(), to cover the common use case of implementing base case and recursive case within the same method.

This, in turn, would enable us to simplify the offchain state API, by handling the recursive settling proof internally. @45930 do you think that should be done?

[mitschabaude]

this is the implementation of the new recursive proving API

[mitschabaude]

instead of collecting all proofs inside this function as before, we get them from the new global context ZkProgramContext, which is also written to by Proof.declare()

[mitschabaude]

I worked a bit on types in this file to reduce the amount of as any, in particular it's nice to have this final sanity check that the returned program matches the output type. for that, I had to put a boolean into program.proofsEnabled which we overwrite later with Object.defineProperty()

[mitschabaude]

the added logic here comes from the bindings, see o1-labs/o1js-bindings#318

[mitschabaude]

⚠️ Update: This is not ready for review yet ⚠️

I forgot to declare the internally declared proofs to pickles in the top level of picklesRuleFromFunction(). so, Pickles doesn't currently add any proof verification logic, and the "recursive proofs" work even if we use dummy proofs.

To fix this, I'll need to refactor a bit to find out the proofs prior to calling pickledRuleFromFunction(). Luckily this should be possible without extra overhead, because we're already calling analyzeMethods() up front to determine the gates, and in that step we'll also be able to count the declared proofs.

Because this caught me by surprise and seems like a dangerous footgun, I'm going to add runtime check that the number of dynamically returned proofs to be verified matches the number that was determined at compile time.

[Trivo25]

I will let the others be the judge if we want to express the API this way or if this is too confusing. I wonder if we can/should type this method in a certain way so its only available when its called in the correct context (within another program), and not in the plain native verison to avoid confusion

[mitschabaude]

one note: proveRecursively doesn't return you a proof (just the proof output), and it's therefore hard to confuse with the plain proving API.

like, if you need a proof, you'll figure out quickly that this API doesn't give you what you want.

(if you don't care about a proof, then it's fine to use this API outside a circuit, because it does run the method.. will just take very long due to the internal proving)

[45930]

But for the example, I wouldn't understand how to use this. .recursiveProvers seems slightly better, at least because it sounds like it may return an object. It still sounds like .recursiveProvers.baseCase() will return a proof, so potentially .recursiveProverFunctions is the most natural sounding.

I think there's an asterisk to this which is that zkprogram is still a very opaque API that people don't have an intuitive sense for, so I think we can only be so intuitive with the naming anyways.

[mitschabaude]

yeah so it's not self-documenting I agree, but as you say, few things about zkprogram are.

which IMO just means it needs documentation! that documentation will be simpler than the existing docs, because the API is simpler to use.

compare, for example, what you currently have to do to define the Proof class that belongs to a recursively verified program, i.e. ZkProgram.Proof(). It's documented nowhere (in fact, our current docs show an API that doesn't even exist). Will be easier in the new API because you don't even have to define that proof class!

[45930]

I'm not sure how I feel about the proposed API change. It is quite clean, but also hides a lot of detail, and perhaps makes it easier to write programs with accidental or intentional exploits. It seems to move the opposite direction of our new API design, which is more explicit and verbose. Since it's optional for developers, I don't feel strongly that we shouldn't release it.

I also don't love new APIs that are out ahead of the documentation. That's the state of where we are now, so I wouldn't block this release on that. But I intend to get to the point where I would block such a release for that reason in the future.

[mitschabaude]

@45930 @Trivo25 If you're uncomfortable with introducing a different API out of the blue -- it would probably also work as a wrapper around ZkProgram. Something like this would produce less of an irreversible change:

let program = ZkProgram(...);

let programRecursive = Experimental.Recursive(program);

// inside other program method
let output = await programRecursive.run(...inputs);

Personally I think the API is awesome as is and would be easier to use and find on ZkProgram directly, but I don't want it to block the main addition of this PR, internal proof declaring, which is much more important.

[mitschabaude]

Note: I pushed one more commit f591f02 which emerged as a necessary fix in zksecurity/mina-credentials#86 when running internal proofs with proofsEnabled = false.

Also, by experience on zksecurity/mina-credentials#86, I can now say that proof declaring works well in a complicated, real-world circuit.
Also worth mentioning, there are scenarios where I couldn't use .proveRecursively but had to use manual proof witnessing: when I wanted to pick the particular recursive method based on the remaining size of proof inputs

[45930]

it would probably also work as a wrapper around ZkProgram

I would feel more comfortable with this experimental wrapper. Given that you've modified this PR a couple times already, it seems likely that more changes will eventually be needed. That way we can also give you the functionality you want, but have more time internally to get comfortable with these changes and think about how they fit into the v2 API changes.

@mitschabaude

@Trivo25 would you also be ok with merging these changes as an experimental function?

[Trivo25]

I think we should go for the wrapper and potentially move the functionality into zkProgram natively some time in the future

[mitschabaude]

cool, I'll push a refactor sometime soon

[mitschabaude]

@Trivo25 @45930 I moved Recursive outside ZkProgram!

[mitschabaude]

All I Want For Christmas Is getting my PR merged 🎄 🎅🏻 🎄 🎁 🎄

[45930]