Add recursion opcode

[kevaundray]

Problem

The ability to verify a program in another program is one feature which modern programming languages have. As with all opcodes, this can be done in the frontend using the arithmetic opcode, however it will be in-efficient and there are ways in which the proving system can do it in a more optimal way. One of these is delaying the pairing computation until verification, so it is not computed inside of the circuit.

Proposed solution

An alternative

Lets first discuss an alternative which may eventually deprecate the strategy we will go with now.

The idea is to look at what parts of the verification algorithms we really need to delegate to the proving system. In the case that the proving system uses KZG we would only create a pairings opcode and the frontend will efficiently compute the rest. An example of a frontend would be Noir. It is the case that there are other components in the verification algorithm that are expensive like big integer arithmetic and this solution would hinge on us having enough opcodes such that they cover the possible usecases such as big integer.

The reason to not go with this strategy right now is because we would need to do a survey of the known proving systems and figure out what components we really need to delegate to the proving system.

The advantages of this strategy is that you more of the code is implemented in the frontend or in the acvm-stdlib, making it less opaque.

Proposed solution

To implement a VERIFY_PROOF opcode which will take a proof, public inputs and a verification key. It will then return true to indicate whether the proof is successful and false to indicate whether the proof is not successful.

Structures

This will be a new black box function, where the function definition will be:

FuncDefinition {
           name : "verify_proof",
           input_size: InputSize::Variable,
           output_size: OutputSize(1),
},

The input_size will be the concatenation of the verification key, proof and public inputs. The input size is variable for two reasons:

• The public inputs can vary depending on the circuit.
• (Not ideal) we don't specify what proving system we are verifying a proof for, so this recursion opcode can be used to verify plonk/groth16/bulletproofs for example. This is not ideal because if a frontend changes the backend but does not change the proof, then they will encounter a failing proof.

For the latter point, we could introduce an opcode for each proof system that we can recurse on though this is not an ideal solution because each time we add a backend which is supported, we would then need to add an opcode.

Alternatives considered

No response

Additional context

No response

Submission Checklist

• [X] Once I hit submit, I will assign this issue to the Project Board with the appropriate tags.

[kevaundray]

Note: We have been trying to get to a stage where all opcodes can be executed by the vm. This is not the case right now since pedersen hashing is hard to implement in rust, so we ask the backend to supply the implementation.

Adding this opcode will make this the case again, since we cannot know if proof verification was successful in the partial witness generator without verifying it.

We could somewhat alleviate this by adding a verify_proof_true opcode that returns nothing and then just assuming that it passes. A user would only know if the proof failed after proof verification.

[zac-williamson]

Suggestion: we change FuncDefinition to

FuncDefinition {
           name : "verify_proof",
           input_size: InputSize::Variable,
           output_size: OutputSize::Variable,
},

"Recursive Verification" is a misleading term and should better be considered "Recursive Aggregation". All recursion schemes I am aware of do not fully verify a proof, but instead spit out an "AggregationObject" on public inputs.

The AggregationObject contains a blob of data that the top-level verifier needs to run some proof-system-specific algorithm on to complete verification.

For example, in UltraPlonk this is two G1 points that must be fed into a pairing (our smart contract handles this already).

For Halo2 the AggregationObject is a vector of G1 points whose size is the log of the circuit size.

I would propose that the output of the Recursion ACIR opcode is the following:

1. A true/false flag (this cannot be fully verified until the aggregation object is checked, but this can be used by an honest Prover to signal to the ACVM that an error should be thrown)
2. A hash of the verification key (for cases where the circuit being verified is one-of-many, the hash can be used to determine which key was used)
3. The AggregationObject (size is proof-system specific)

[kevaundray]

Suggestion: we change FuncDefinition to

FuncDefinition {
           name : "verify_proof",
           input_size: InputSize::Variable,
           output_size: OutputSize::Variable,
},

"Recursive Verification" is a misleading term and should better be considered "Recursive Aggregation". All recursion schemes I am aware of do not fully verify a proof, but instead spit out an "AggregationObject" on public inputs.

The AggregationObject contains a blob of data that the top-level verifier needs to run some proof-system-specific algorithm on to complete verification.

For example, in UltraPlonk this is two G1 points that must be fed into a pairing (our smart contract handles this already).

For Halo2 the AggregationObject is a vector of G1 points whose size is the log of the circuit size.

I would propose that the output of the Recursion ACIR opcode is the following:

1. A true/false flag (this cannot be fully verified until the aggregation object is checked, but this can be used by an honest Prover to signal to the ACVM that an error should be thrown)
2. A hash of the verification key (for cases where the circuit being verified is one-of-many, the hash can be used to determine which key was used)
3. The AggregationObject (size is proof-system specific)

That's a good point re Aggregation obejct.

1. Re true/false flag, the elements in the opcode should only be related to circuit construction -- a true/false flag seems to be a prover value that is never checked by the verifier.
2. How would this be used in a circuit?
3. Yep this makes sense!