Add #[recursive] proof artifact generation to nargo prove

[Savio-Sou]

Problem

The #[recursive] attribute was introduced, but Nargo does not currently do anything special with it to ease recursive proof developer experience.

Happy Case

Running nargo prove on a Noir program with the #[recursive] flag generates, in addition to the usual .proof file, a TOML file containing information that matches with verify_proof's expected inputs (i.e. verification_key, proof...).

This helps users to more easily compose custom prover input TOML files for recursively verifying such programs in other Noir programs.

Project Impact

Nice-to-have

Impact Context

The vlayer team would like to prove their big and recursive programs (preferably on Nargo).

Proving on Nargo gets them the proof but not recursive proof artifacts.

Proving with NoirJS gets them the recursive proof artifacts but not the proof (as the program exceeds WASM's memory limit).

Workaround

Yes

Workaround Description

Generate recursive proof artifacts with NoirJS, then mix-and-match with Nargo.

If this Issue isn't too tricky to resolve, however, it would make devs' lives considerably easier.

UPDATE:
Script for generating recursive proof artifacts on CLI using bb binary: #4336 (comment)

Additional Context

No response

Would you like to submit a PR for this Issue?

None

Support Needs

No response

[Savio-Sou]

Forgot about the AztecProtocol/aztec-packages#4221 works; @vezenovm is this relevant in spite of the is_recursive flag removal initiative?

[TomAFrench]

I don't think we're ever really going to have a "one click" method of generating a proof and then generating another proof which verifies it.

The current status is that we can generate proofs which are easily verified inside of a snark with the #[recursive] attribute. We can also verify these proofs on the CLI in the same way as "normal" proofs.

The two main hurdles after that to reach what I think this issue is asking for are:

1. We need a generic way to convert the returned proof into a format which nargo can feed into another proof.

i.e. this shouldn't result in hardcoding to bb specifics.

2. We need to be able to compose these recursive proofs in arbitrary conditions.

This is the real showstopper imo.

Assume that we tackle the first issue, we could write some logic so that we generate a proof and then split that up into fields (a la. generateRecursiveProofArtifacts). The next question is then how to make those available to the program which is verifying this proof.

This is kinda fine (but not great) if we're verifying a single proof in that circuit, maybe we declare some canonical argument names which correspond to a proof and we can pipe those through. But what happens then if the outer program aggregates 2 proofs, or 3, etc.?

This basically boils down to data plumbing but if I'm writing a system of zk proofs which interact with each other, I think that it's reasonable to expect me to write a shell script which handles this.

[Savio-Sou]

Very reasonable. We should shoot for (1) but agree that (2) won't be necessary now that we are moving to the use of #[recursive] (overlooked when creating the Issue).

Updated the original issue.

[vezenovm]

We could have that a circuit marked with #[recursive] attribute automatically spits out a proof and vkey in the format that the backend expects for recursive proofs.

This may have some developer footguns with regards to serializing to/from the normal byte format and the recursive format. For example, in the bberg case, we want a list of field elements as inputs to a recursive circuit, but verifying that circuit with nargo uses just the normal proof byte format. A backend would then need to not only be able to serialize into the recursive format but deserialize into the normal proof format as well. This would require a bit more exploration on how to make generating these artifacts backend agnostic.

[Savio-Sou]

We could have that a circuit marked with #[recursive] attribute automatically spits out a proof and vkey in the format that the backend expects for recursive proofs.

If this is relatively easy to do with barretenberg, shall we get this in to resolve this Issue and improve devs' lives first and spin up another Issue for longer-term serialization improvement?

[vezenovm]

If this is relatively easy to do with barretenberg, shall we get this in to resolve this Issue and improve devs' lives first and spin up another Issue for longer-term serialization improvement?

We would need the serialization to enable people to use nargo verify on circuits marked with #[recursive]. So it would be a dev ex improvement for supplying the recursive artifacts to another circuit but a regression in devs ability to prove/verify outside of the circuit.

[Savio-Sou]

Could we make nargo prove spits out both:

1. "Normal" proof verifiable by nargo verify (i.e. what we already do), and
2. Proof artifacts useful for feeding into verify_proof (i.e. what barretenberg already has APIs for)

when proving a program marked with #[recursive]?

It'll take up more disk space by "duplicating" proofs, sure, but should be justifiable as a quick regression-less DevEx improvement.

[vezenovm]

Could we not have nargo prove spits out both:

Yeah that could be a good compromise. A backend could just deal with multiple proof and/or vkey formats. I would need to look into how this would play into the existing nargo API.

[Savio-Sou]

spits out both

If that makes barretenberg prove twice (or require additional work to avoid so), we could also approach it by adding a nargo prove --recursive-artifacts flag, where:

1. nargo prove --> generates "normal" proof
2. nargo prove --recursive-artifacts --> generates proof artifacts

And the dev could choose which route to opt for without doubling proving times.

Let me know if that's preferred, happy to update the original Issue accordingly.

[vezenovm]

nargo prove --recursive-artifacts

This type of flag is what we would like to avoid. It is why we moved away from a is-recursive flag to putting an attribute on the circuit.

I need to check the nargo interface but worst case the backend should be able to read and discern between multiple proof formats. Definitely can avoid proving twice, and reading multiple proofs isn't that bad as they are small (at least in the bberg case).

[Savio-Sou]

Tom further shared that we could actually gather the recursion artifacts with barretenberg on CLI today by running a few commands on the barretenberg binary. He will share an example with how-tos, which should be a sufficient stop-gap solution for the community.

Hence we can skip the compromised approach discussed in the few comments above and go straight for a generalized interface to resolve this Issue (e.g. requiring proving backends to expose an API to generate all artifacts it needs to perform recursion). This would help minimize breaking changes and upgrade frictions for Noir devs in between.

[TomAFrench]

Took at look at implementing this in pure bash

#!/usr/bin/env bash
set -eu

PROJECT_PATH=$1

# Note this assumes you're using the `assert_statement_recursive` project currently.
ARTIFACT_FILE=$PROJECT_PATH/target/assert_statement_recursive.json
PROOF_FILE=$PROJECT_PATH/proofs/assert_statement_recursive.proof
BB=~/.nargo/backends/acvm-backend-barretenberg/backend_binary

jq -r '.bytecode' $ARTIFACT_FILE | base64 -d > acir.tmp
$BB write_vk -b acir.tmp -o vk.tmp
$BB vk_as_fields -k vk.tmp -o vk_fields.tmp


VK_HASH=$(jq -r '.[0]' vk_fields.tmp) 
echo "vk_hash = $VK_HASH" > temp.toml

VK_AS_FIELDS=$(jq -r '.[1:]' vk_fields.tmp) 
echo "vk_as_fields = $VK_AS_FIELDS" >> temp.toml

base64 -d $PROOF_FILE > proof.tmp

$BB proof_as_fields -k vk.tmp -p proof.tmp -o proof_as_fields.tmp

rm acir.tmp
rm vk_fields.tmp
rm vk.tmp

Main trouble I'm running into is that we're storing a proof with public inputs stripped off in the proofs directory whereas bb expects to have the correct number of public inputs attached to it. We could attach dummy public inputs here and then strip them off again but it looks like we have unnecessary friction here.

[vezenovm]

Main trouble I'm running into is that we're storing a proof with public inputs stripped off in the proofs directory whereas bb expects to have the correct number of public inputs attached to it. We could attach dummy public inputs here and then strip them off again but it looks like we have unnecessary friction here.

Maybe we can write a small tool for this and we just call the binary in Rust. We actually do a bash file for generating recursive artifacts here in the acir tests, however, it does prove using bb due to this friction.

[akonior]

I attempted to use this script, and one modification was necessary: instead of converting the proof from base64 to binary format, I had to convert a string saved in hexadecimal format to binary format. Additionally, I appended public input values at the end. I am including a link to a GitHub gist for future reference.

[Savio-Sou]

Moving towards #4960.