Skip to content

Commit

Permalink
chore: Add #[recursive] Explainer to Documentation (#4399)
Browse files Browse the repository at this point in the history
# Description

## Problem

Step towards [#4392](#4392)

The documentation for Recursive Proofs was lacking information on the
newly introduced `#[recursive]` attribute, which is crucial for
understanding how to mark circuits for recursive proof generation.

## Summary

This pull request updates the Recursive Proofs documentation page to
include a comprehensive section on the `#[recursive]` attribute. It
explains the attribute's purpose, how it should be used, and provides an
example demonstrating its application within a circuit definition.

## Additional Context

The introduction of the `#[recursive]` attribute simplifies the process
of designating circuits for recursive proofs, eliminating the need for
manual flagging in the tooling infrastructure.

## Documentation

- [ ] No documentation needed.
- [x] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.

---------

Co-authored-by: Savio <[email protected]>
  • Loading branch information
paulallensuxs and Savio-Sou authored Feb 22, 2024
1 parent e382921 commit ceb8001
Show file tree
Hide file tree
Showing 2 changed files with 40 additions and 0 deletions.
20 changes: 20 additions & 0 deletions docs/docs/noir/standard_library/recursion.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,26 @@ Noir supports recursively verifying proofs, meaning you verify the proof of a No

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)

## The `#[recursive]` Attribute

In Noir, the `#[recursive]` attribute is used to indicate that a circuit is designed for recursive proof generation. When applied, it informs the compiler and the tooling that the circuit should be compiled in a way that makes its proofs suitable for recursive verification. This attribute eliminates the need for manual flagging of recursion at the tooling level, streamlining the proof generation process for recursive circuits.

### Example usage with `#[recursive]`

```rust
#[recursive]
fn main(x: Field, y: pub Field) {
assert(x == y, "x and y are not equal");
}

// This marks the circuit as recursion-friendly and indicates that proofs generated from this circuit
// are intended for recursive verification.
```

By incorporating this attribute directly in the circuit's definition, tooling like Nargo and NoirJS can automatically execute recursive-specific duties for Noir programs (e.g. recursive-friendly proof artifact generation) without additional flags or configurations.

## Verifying Recursive Proofs

```rust
#[foreign(verify_proof)]
fn verify_proof(_verification_key : [Field], _proof : [Field], _public_input : Field, _key_hash : Field) {}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,26 @@ Noir supports recursively verifying proofs, meaning you verify the proof of a No

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)

## The `#[recursive]` Attribute

In Noir, the `#[recursive]` attribute is used to indicate that a circuit is designed for recursive proof generation. When applied, it informs the compiler and the tooling that the circuit should be compiled in a way that makes its proofs suitable for recursive verification. This attribute eliminates the need for manual flagging of recursion at the tooling level, streamlining the proof generation process for recursive circuits.

### Example usage with `#[recursive]`

```rust
#[recursive]
fn main(x: Field, y: pub Field) {
assert(x == y, "x and y are not equal");
}

// This marks the circuit as recursion-friendly and indicates that proofs generated from this circuit
// are intended for recursive verification.
```

By incorporating this attribute directly in the circuit's definition, tooling like Nargo and NoirJS can automatically execute recursive-specific duties for Noir programs (e.g. recursive-friendly proof artifact generation) without additional flags or configurations.

## Verifying Recursive Proofs

```rust
#[foreign(verify_proof)]
fn verify_proof(_verification_key : [Field], _proof : [Field], _public_input : Field, _key_hash : Field) {}
Expand Down

0 comments on commit ceb8001

Please sign in to comment.