Skip to content

Commit

Permalink
chore(docs): updating docs to match new recursion interfacee (#4187)
Browse files Browse the repository at this point in the history
# Description

This PR documents the new recursion interface.

## Problem\*

Resolves #4139 
Resolves AztecProtocol/dev-rel#148

## Summary\*

- Removes the usage of `aggregation object` while retaining the mention
that recursive proofs are actually aggregation of proofs
- Removes the mention to add the size of public inputs to the proof, as
they are now separate
- Removes some leftover explainer in the `verify_proof` reference

## Additional Context

`noir-examples` is actually not working with this new interface, as I'm
blocked by a weird issue where proofs give me my dear friend
`unreachable`

Will debug that next week with @TomAFrench but I think we're good to
push the docs for now.

---------

Co-authored-by: Cat McGee <[email protected]>
  • Loading branch information
signorecello and catmcgee authored Jan 30, 2024
1 parent 0205d3b commit f4de6ee
Show file tree
Hide file tree
Showing 6 changed files with 64 additions and 120 deletions.
23 changes: 11 additions & 12 deletions docs/docs/explainers/explainer-recursion.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,13 @@ keywords:
"Optimizing Computational Resources",
"Improving Efficiency",
"Verification Key",
"Aggregation Objects",
"Aggregation",
"Recursive zkSNARK schemes",
"PLONK",
"Proving and Verification Keys"
]
sidebar_position: 1
pagination_next: how_to/how-to-recursion
---

In programming, we tend to think of recursion as something calling itself. A classic example would be the calculation of the factorial of a number:
Expand Down Expand Up @@ -64,7 +65,7 @@ So, they use zero-knowledge proofs. Alice tries to guess Bob's number, and Bob w

This ZK proof can go on a smart contract, revealing the winner and even giving prizes. However, this means every turn needs to be verified on-chain. This incurs some cost and waiting time that may simply make the game too expensive or time-consuming to be worth it.

As a solution, Alice proposes the following: "what if Bob generates his proof, and instead of sending it on-chain, I verify it *within* my own proof before playing my own turn?".
As a solution, Alice proposes the following: "what if Bob generates his proof, and instead of sending it on-chain, I verify it *within* my own proof before playing my own turn?".

She can then generate a proof that she verified his proof, and so on.

Expand Down Expand Up @@ -116,25 +117,19 @@ As you can see in the [recursion reference](noir/standard_library/recursion.md),
- The Verification Key of the circuit that generated the proof
- A hash of this verification key, as it's needed for some backends
- The public inputs for the proof
- The input aggregation object

It also returns the `output aggregation object`. These aggregation objects can be confusing at times, so let's dive in a little bit.

### Aggregation objects
:::info

Recursive zkSNARK schemes do not necessarily "verify a proof" in the sense that you expect a true or false to be spit out by the verifier. Rather an aggregation object is built over the public inputs.

In the case of PLONK the recursive aggregation object is two G1 points (expressed as 16 witness values). The final verifier (in our case this is most often the smart contract verifier) has to be aware of this aggregation object to execute a pairing and check the validity of these points.

So, taking the example of Alice and Bob and their guessing game:

- Alice makes her guess. Her proof is *not* recursive: it doesn't verify any proof within it! It's just a standard `assert(x != y)` circuit
- Bob verifies Alice's proof and makes his own guess. In this circuit, he is verifying a proof, so it needs to output an `aggregation object`: he is generating a recursive proof!
- Alice verifies Bob's *recursive proof*, and uses Bob's `output aggregation object` as the `input aggregation object` in her proof... Which in turn, generates another `output aggregation object`.
- Bob verifies Alice's proof and makes his own guess. In this circuit, he doesn't exactly *prove* the verification of Alice's proof. Instead, he *aggregates* his proof to Alice's proof. The actual verification is done when the full proof is verified, for example when using `nargo verify` or through the verifier smart contract.

One should notice that when Bob generates his first proof, he has no input aggregation object. Because he is not verifying an recursive proof, he has no `input aggregation object`. In this case, he may use zeros instead.
We can imagine recursive proofs a [relay race](https://en.wikipedia.org/wiki/Relay_race). The first runner doesn't have to receive the baton from anyone else, as he/she already starts with it. But when his/her turn is over, the next runner needs to receive it, run a bit more, and pass it along. Even though every runner could theoretically verify the baton mid-run (why not? 🏃🔍), only at the end of the race does the referee verify that the whole race is valid.

We can imagine the `aggregation object` as the baton in a [relay race](https://en.wikipedia.org/wiki/Relay_race). The first runner doesn't have to receive the baton from anyone else, as he/she already starts with it. But when his/her turn is over, the next runner needs to receive it, run a bit more, and pass it along. Even though every runner could theoretically verify the baton mid-run (why not? 🏃🔍), only at the end of the race does the referee verify that the whole race is valid.
:::

## Some architecture

Expand Down Expand Up @@ -175,3 +170,7 @@ In this example, a regulator could verify that taxes were paid for a specific pu
At the time of writing, verifying recursive proofs is surprisingly fast. This is because most of the time is spent on generating the verification key that will be used to generate the next proof. So you are able to cache the verification key and reuse it later.

Currently, Noir JS packages don't expose the functionality of loading proving and verification keys, but that feature exists in the underlying `bb.js` package.

## How can I try it

Learn more about using recursion in Nargo and NoirJS in the [how-to guide](../how_to/how-to-recursion.md) and see a full example in [noir-examples](https://github.com/noir-lang/noir-examples).
21 changes: 8 additions & 13 deletions docs/docs/how_to/how-to-recursion.md
Original file line number Diff line number Diff line change
Expand Up @@ -108,11 +108,7 @@ This call takes the public inputs and the proof, but also the public inputs coun

:::info

The `proofAsFields` has a constant size `[Field; 93]`. However, currently the backend doesn't remove the public inputs from the proof when converting it.

This means that if your `main` circuit has two public inputs, then you should also modify the recursive circuit to accept a proof with the public inputs appended. This means that in our example, since `y` is a public input, our `proofAsFields` is of type `[Field; 94]`.

Verification keys in Barretenberg are always of size 114.
The `proofAsFields` has a constant size `[Field; 93]` and verification keys in Barretenberg are always `[Field; 114]`.

:::

Expand All @@ -136,32 +132,31 @@ const recursiveInputs = {
proof: proofAsFields, // array of length 93 + size of public inputs
publicInputs: [mainInput.y], // using the example above, where `y` is the only public input
key_hash: vkHash,
input_aggregation_object: Array(16).fill(0) // this circuit is verifying a non-recursive proof, so there's no input aggregation object: just use zero
}

const { witness, returnValue } = noir.execute(recursiveInputs) // we're executing the recursive circuit now!
const { proof, publicInputs } = backend.generateFinalProof(witness)
const verified = backend.verifyFinalProof({ proof, publicInputs })
```

You can obviously chain this proof into another proof. In fact, if you're using recursive proofs, you're probably interested of using them this way! In that case, you should keep in mind the `returnValue`, as it will contain the `input_aggregation_object` for the next proof.
You can obviously chain this proof into another proof. In fact, if you're using recursive proofs, you're probably interested of using them this way!

:::tip

Managing circuits and "who does what" can be confusing. To make sure your naming is consistent, you can keep them in an object. For example:

```js
const circuits = {
main: mainJSON,
recursive: recursiveJSON
main: mainJSON,
recursive: recursiveJSON
}
const backends = {
main: new BarretenbergBackend(circuits.main),
recursive: new BarretenbergBackend(circuits.recursive)
main: new BarretenbergBackend(circuits.main),
recursive: new BarretenbergBackend(circuits.recursive)
}
const noir_programs = {
main: new Noir(circuits.main, backends.main),
recursive: new Noir(circuits.recursive, backends.recursive)
main: new Noir(circuits.main, backends.main),
recursive: new Noir(circuits.recursive, backends.recursive)
}
```

Expand Down
48 changes: 13 additions & 35 deletions docs/docs/noir/standard_library/recursion.md
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
---
title: Recursive Proofs
description: Learn about how to write recursive proofs in Noir.
keywords: [recursion, recursive proofs, verification_key, aggregation object, verify_proof]
keywords: [recursion, recursive proofs, verification_key, verify_proof]
---

Noir supports recursively verifying proofs, meaning you verify the proof of a Noir program in another Noir program. This enables creating proofs of arbitrary size by doing step-wise verification of smaller components of a large proof.

The `verify_proof` function takes a verification key, proof and public inputs for a zk program, as well as a key hash and an input aggregation object. The key hash is used to check the validity of the verification key and the input aggregation object is required by some proving systems. The `verify_proof` function returns an output aggregation object that can then be fed into future iterations of the proof verification if required.
Read [the explainer on recursion](../../explainers/explainer-recursion.md) to know more about this function and the [guide on how to use it.](../../how_to/how-to-recursion.md)

```rust
#[foreign(verify_proof)]
fn verify_proof(_verification_key : [Field], _proof : [Field], _public_input : Field, _key_hash : Field, _input_aggregation_object : [Field]) -> [Field] {}
fn verify_proof(_verification_key : [Field], _proof : [Field], _public_input : Field, _key_hash : Field) {}
```

:::info
Expand All @@ -26,36 +26,29 @@ use dep::std;

fn main(
verification_key : [Field; 114],
proof : [Field; 94],
proof : [Field; 93],
public_inputs : [Field; 1],
key_hash : Field,
input_aggregation_object : [Field; 16],
proof_b : [Field; 94],
) -> pub [Field; 16] {
let output_aggregation_object_a = std::verify_proof(
proof_b : [Field; 93],
) {
std::verify_proof(
verification_key.as_slice(),
proof.as_slice(),
public_inputs.as_slice(),
key_hash,
input_aggregation_object
key_hash
);

let output_aggregation_object = std::verify_proof(
std::verify_proof(
verification_key.as_slice(),
proof_b.as_slice(),
public_inputs.as_slice(),
key_hash,
output_aggregation_object_a
key_hash
);

let mut output = [0; 16];
for i in 0..16 {
output[i] = output_aggregation_object[i];
}
output
}
```

You can see a full example of recursive proofs in [this example recursion demo repo](https://github.com/noir-lang/noir-examples/tree/master/recursion).

## Parameters

### `verification_key`
Expand All @@ -68,23 +61,8 @@ The proof for the zk program that is being verified.

### `public_inputs`

These represent the public inputs of the proof we are verifying. They should be checked against in the circuit after construction of a new aggregation state.
These represent the public inputs of the proof we are verifying.

### `key_hash`

A key hash is used to check the validity of the verification key. The circuit implementing this opcode can use this hash to ensure that the key provided to the circuit matches the key produced by the circuit creator.

### `input_aggregation_object`

An aggregation object is blob of data that the top-level verifier must run some proof system specific algorithm on to complete verification. The size is proof system specific and will be set by the backend integrating this opcode. The input aggregation object is only not `None` when we are verifying a previous recursive aggregation in the current circuit. If this is the first recursive aggregation there is no input aggregation object. It is left to the backend to determine how to handle when there is no input aggregation object.

## Return value

### `output_aggregation_object`

This is the result of a recursive aggregation and is what will be fed into the next verifier.
The next verifier can either perform a final verification (returning true or false) or perform another recursive aggregation where this output aggregation object will be the input aggregation object of the next recursive aggregation.

## Example

You can see an example of how to do recursive proofs in [this example recursion demo repo](https://github.com/noir-lang/noir-examples/tree/master/recursion).
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,13 @@ keywords:
"Optimizing Computational Resources",
"Improving Efficiency",
"Verification Key",
"Aggregation Objects",
"Aggregation",
"Recursive zkSNARK schemes",
"PLONK",
"Proving and Verification Keys"
]
sidebar_position: 1
pagination_next: how_to/how-to-recursion
---

In programming, we tend to think of recursion as something calling itself. A classic example would be the calculation of the factorial of a number:
Expand Down Expand Up @@ -64,7 +65,7 @@ So, they use zero-knowledge proofs. Alice tries to guess Bob's number, and Bob w

This ZK proof can go on a smart contract, revealing the winner and even giving prizes. However, this means every turn needs to be verified on-chain. This incurs some cost and waiting time that may simply make the game too expensive or time-consuming to be worth it.

As a solution, Alice proposes the following: "what if Bob generates his proof, and instead of sending it on-chain, I verify it *within* my own proof before playing my own turn?".
As a solution, Alice proposes the following: "what if Bob generates his proof, and instead of sending it on-chain, I verify it *within* my own proof before playing my own turn?".

She can then generate a proof that she verified his proof, and so on.

Expand Down Expand Up @@ -116,25 +117,19 @@ As you can see in the [recursion reference](noir/standard_library/recursion.md),
- The Verification Key of the circuit that generated the proof
- A hash of this verification key, as it's needed for some backends
- The public inputs for the proof
- The input aggregation object

It also returns the `output aggregation object`. These aggregation objects can be confusing at times, so let's dive in a little bit.

### Aggregation objects
:::info

Recursive zkSNARK schemes do not necessarily "verify a proof" in the sense that you expect a true or false to be spit out by the verifier. Rather an aggregation object is built over the public inputs.

In the case of PLONK the recursive aggregation object is two G1 points (expressed as 16 witness values). The final verifier (in our case this is most often the smart contract verifier) has to be aware of this aggregation object to execute a pairing and check the validity of these points.

So, taking the example of Alice and Bob and their guessing game:

- Alice makes her guess. Her proof is *not* recursive: it doesn't verify any proof within it! It's just a standard `assert(x != y)` circuit
- Bob verifies Alice's proof and makes his own guess. In this circuit, he is verifying a proof, so it needs to output an `aggregation object`: he is generating a recursive proof!
- Alice verifies Bob's *recursive proof*, and uses Bob's `output aggregation object` as the `input aggregation object` in her proof... Which in turn, generates another `output aggregation object`.
- Bob verifies Alice's proof and makes his own guess. In this circuit, he doesn't exactly *prove* the verification of Alice's proof. Instead, he *aggregates* his proof to Alice's proof. The actual verification is done when the full proof is verified, for example when using `nargo verify` or through the verifier smart contract.

One should notice that when Bob generates his first proof, he has no input aggregation object. Because he is not verifying an recursive proof, he has no `input aggregation object`. In this case, he may use zeros instead.
We can imagine recursive proofs a [relay race](https://en.wikipedia.org/wiki/Relay_race). The first runner doesn't have to receive the baton from anyone else, as he/she already starts with it. But when his/her turn is over, the next runner needs to receive it, run a bit more, and pass it along. Even though every runner could theoretically verify the baton mid-run (why not? 🏃🔍), only at the end of the race does the referee verify that the whole race is valid.

We can imagine the `aggregation object` as the baton in a [relay race](https://en.wikipedia.org/wiki/Relay_race). The first runner doesn't have to receive the baton from anyone else, as he/she already starts with it. But when his/her turn is over, the next runner needs to receive it, run a bit more, and pass it along. Even though every runner could theoretically verify the baton mid-run (why not? 🏃🔍), only at the end of the race does the referee verify that the whole race is valid.
:::

## Some architecture

Expand Down Expand Up @@ -175,3 +170,7 @@ In this example, a regulator could verify that taxes were paid for a specific pu
At the time of writing, verifying recursive proofs is surprisingly fast. This is because most of the time is spent on generating the verification key that will be used to generate the next proof. So you are able to cache the verification key and reuse it later.

Currently, Noir JS packages don't expose the functionality of loading proving and verification keys, but that feature exists in the underlying `bb.js` package.

## How can I try it

Learn more about using recursion in Nargo and NoirJS in the [how-to guide](../how_to/how-to-recursion.md) and see a full example in [noir-examples](https://github.com/noir-lang/noir-examples).
21 changes: 8 additions & 13 deletions docs/versioned_docs/version-v0.23.0/how_to/how-to-recursion.md
Original file line number Diff line number Diff line change
Expand Up @@ -108,11 +108,7 @@ This call takes the public inputs and the proof, but also the public inputs coun

:::info

The `proofAsFields` has a constant size `[Field; 93]`. However, currently the backend doesn't remove the public inputs from the proof when converting it.

This means that if your `main` circuit has two public inputs, then you should also modify the recursive circuit to accept a proof with the public inputs appended. This means that in our example, since `y` is a public input, our `proofAsFields` is of type `[Field; 94]`.

Verification keys in Barretenberg are always of size 114.
The `proofAsFields` has a constant size `[Field; 93]` and verification keys in Barretenberg are always `[Field; 114]`.

:::

Expand All @@ -136,32 +132,31 @@ const recursiveInputs = {
proof: proofAsFields, // array of length 93 + size of public inputs
publicInputs: [mainInput.y], // using the example above, where `y` is the only public input
key_hash: vkHash,
input_aggregation_object: Array(16).fill(0) // this circuit is verifying a non-recursive proof, so there's no input aggregation object: just use zero
}

const { witness, returnValue } = noir.execute(recursiveInputs) // we're executing the recursive circuit now!
const { proof, publicInputs } = backend.generateFinalProof(witness)
const verified = backend.verifyFinalProof({ proof, publicInputs })
```

You can obviously chain this proof into another proof. In fact, if you're using recursive proofs, you're probably interested of using them this way! In that case, you should keep in mind the `returnValue`, as it will contain the `input_aggregation_object` for the next proof.
You can obviously chain this proof into another proof. In fact, if you're using recursive proofs, you're probably interested of using them this way!

:::tip

Managing circuits and "who does what" can be confusing. To make sure your naming is consistent, you can keep them in an object. For example:

```js
const circuits = {
main: mainJSON,
recursive: recursiveJSON
main: mainJSON,
recursive: recursiveJSON
}
const backends = {
main: new BarretenbergBackend(circuits.main),
recursive: new BarretenbergBackend(circuits.recursive)
main: new BarretenbergBackend(circuits.main),
recursive: new BarretenbergBackend(circuits.recursive)
}
const noir_programs = {
main: new Noir(circuits.main, backends.main),
recursive: new Noir(circuits.recursive, backends.recursive)
main: new Noir(circuits.main, backends.main),
recursive: new Noir(circuits.recursive, backends.recursive)
}
```

Expand Down
Loading

0 comments on commit f4de6ee

Please sign in to comment.