Unreachable Error when calling std::verify_proof() multiple times in recursion circuit

[tuhoag]

Aim

I am trying to write a rollup circuit that can verify proofs from many sub circuits. Then, the rollup circuit needs to call std::verify_proof() multiple times to verify proofs from sub circuits. However, I got the Unreachble Runtime Error when generating the proof of the rollup circuit.

Moreover, I tried to generate the solidity verifier of the rollup circuit and deploy it using Remix (Default network). However, I got the error PUBLIC_INPUT_COUNT_INVALID.

I executed the repositories in macOS Sonoma 14.3.1 with Apple M3 Pro (12 cores).

Expected Behavior

The rollup circuit must be able to generate the rollup proof.

Bug

Generating proof from the rollup circuit in NoirJS raises the RuntimeError: unreachable.

To Reproduce

To reproduce the error, you can use the following two repositories:

• Noir using Node.js (Typescript) that compiles circuits using nargo: https://github.com/tuhoag/noir-typescript
  • Execute ts-node src/index.ts
• Noir using Hardhat (Typescript) that compiles circuits using noir_wasm: https://github.com/tuhoag/noir-examples
  • Execute npx hardhat run scripts/test_recursive_proofs.ts

Project Impact

Blocker

Impact Context

This feature is required in my project since the rollup circuit must verify more than one proof to reduce the verification cost.

Workaround

None

Workaround Description

No response

Additional Context

No response

Installation Method

Binary (noirup default)

Nargo Version

nargo version = 0.23.0
noirc version = 0.23.0+5be9f9d7e2f39ca228df10e5a530474af0331704
(git version hash: 5be9f9d, is dirty: false)

NoirJS Version

0.23.0

Would you like to submit a PR for this Issue?

Maybe

Support Needs

No response

[Savio-Sou]

Thanks for submitting the Issue!

The PUBLIC_INPUT_COUNT_INVALID error seems like a different problem. It'd be great if you could create a separate Issue for it, so the team could follow up in parallel.

Meanwhile, would you be able to copy the full unreachable error call stacks you got? It'd be a very helpful easy reference.

[tuhoag]

The error call stack is not very useful for my case. It is the stack:
Error [RuntimeError]: unreachable
at wasm://wasm/0177a776:wasm-function[14557]:0x58d9a8
at wasm://wasm/0177a776:wasm-function[175]:0x242d6
at wasm://wasm/0177a776:wasm-function[178]:0x2449e
at wasm://wasm/0177a776:wasm-function[6282]:0x2921ba
at wasm://wasm/0177a776:wasm-function[6281]:0x292165
at wasm://wasm/0177a776:wasm-function[6280]:0x292121
at wasm://wasm/0177a776:wasm-function[5700]:0x1e1149
at wasm://wasm/0177a776:wasm-function[5672]:0x1e0005
at wasm://wasm/0177a776:wasm-function[5654]:0x1ded1f
at wasm://wasm/0177a776:wasm-function[3298]:0x1a2561

[Savio-Sou]

Thank you. Is that the full stack trace though? As in do you have the option to expand it further.

Separately, is it right to assume the same circuit works on Nargo, just not on NoirJS?

[tuhoag]

Hi, the recursion circuit is executed successfully with nargo. Only NoirJS raises errors.
NoirJS only shows the stack I described.

[n4ru]

Hi, the recursion circuit is executed successfully with nargo. Only NoirJS raises errors. NoirJS only shows the stack I described.

Were you able to verify in Nargo? I am experiencing this same issue for the same reason, but my circuit also fails to verify in Nargo - though it will prove with Nargo and creates the intermediate proof in NoirJS.

[tuhoag]

Yes, I have the same issue. Proving with nargo is ok but verification is also fail. The error is: Failed to verify proof proofPath.

[Savio-Sou]

FWIW nargo prove and nargo verify works on the double_verify_proof test case, which also has two verify_proofs 🤔

Steps ran:

1. noirup -v 0.25.0
2. git clone https://github.com/noir-lang/noir.git
3. cd noir/test_programs/execution_success/double_verify_proof
4. nargo prove
5. nargo verify

@n4ru / @tuhoag could you upload the Prover.toml file for reproduction? It'd be easier for our engineers if we could first confirm if there is / what is the problem in Nargo first, then move on to NoirJS.

[n4ru]

After spending the majority of my day debugging this, I'm no longer convinced Nargo has any issues, but I cannot even get one verify_proof to run on the latest version of NoirJS, even when compiling with noir_wasm.

However, the noir-examples recursion repo DOES work with a single verify_proof, and gives unreachable with two.

I'm at a loss here and have nearly lost track of my test cases. I've tried just about every combination of #[recursive], one verify, two verifies, compiling with Nargo, compiling with noir_wasm, and even though it obviously works in some cases (like the noir-examples), I cannot figure out what is causing it to fail in others. Since nargo succeeds with identical input (as far as I can tell) and NoirJS still throw unreachable when done twice in a row on the same proof, I assume there is a real issue with NoirJS somewhere.

Could it be related to circuit size? I vaguely recall someone else mentioning a similar issue with bigger circuits in NoirJS, even though they were below the maximum wasm constraint size, but it wouldn't explain why one verify would fail in one case and succeed in the other, since the inner circuit size shouldn't be relevant when verifying a single inner proof (?).

😮‍💨

[signorecello]

Hey we're on it, hold on my friend!

[tuhoag]

FWIW nargo prove and nargo verify works on the double_verify_proof test case, which also has two verify_proofs 🤔

Steps ran:

1. noirup -v 0.25.0
2. git clone https://github.com/noir-lang/noir.git
3. cd noir/test_programs/execution_success/double_verify_proof
4. nargo prove
5. nargo verify

@n4ru / @tuhoag could you upload the Prover.toml file for reproduction? It'd be easier for our engineers if we could first confirm if there is / what is the problem in Nargo first, then move on to NoirJS.

Hi, I updated the Prover.toml. I tested it again today and the verification is correct. Maybe I made some mistakes yesterday. However, noirjs cannot be run. I think the main problem is due to the limitation of WASM. When the memory is more than 4GB, it would crash. I think it is better if Noir has another API in rust/go to tackle this issue. In my project, I have to develop a wrapper to interact with Nargo instead of using NoirJS.

[manylov]

I've made repo with the same issue:
https://github.com/manylov/noir-25-recursive-issue

[tsujp]

I'm also blocked by this. Occurs on 0.25.0, 0.26.0 and a0f7474ae6bd74132efdb945d2eb2383f3913cce (at the time of writing the current HEAD).

For the following circuit with EITHER call to aggregate_proof commented out it works fine. With both uncommented it errors when, from NoirJS, generateProof is called on said circuit.

use dep::std::verify_proof as aggregate_proof;

fn main(
    public_left: [Field; 22],
    public_right: [Field; 22],
    proof_left: [Field; 93],
    proof_right: [Field; 93],
    vk: [Field; 114],
    vk_hash: Field,
) {
    // Aggregate left proof.
    aggregate_proof(
        vk.as_slice(),
        proof_left.as_slice(),
        public_left.as_slice(),
        vk_hash,
    );

    // Aggregate right proof.
    aggregate_proof(
        vk.as_slice(),
        proof_right.as_slice(),
        public_right.as_slice(),
        vk_hash,
    );
}

Error trace:

53 |                     this.logger(str2)
54 |                     if (str2.startsWith('WARNING:')) {
55 |                         this.logger(new Error().stack)
56 |                     }
57 |                 },
58 |                 get_data: (keyAddr, outBufAddr) => {
     ^
RuntimeError: Unreachable code should not be executed (evaluating 'this.exports()[name](...args)')
      at <?>.wasm-function[18106] (native:1:1)
      at <?>.wasm-function[197] (native:1:1)
      at <?>.wasm-function[192] (native:1:1)
      at <?>.wasm-function[155] (native:1:1)
      at 155 (native:1:1)
      at call (/Users/tsujp/programming/~aztec/tikan/node_modules/@aztec/bb.js/dest/node/barretenberg_wasm/barretenberg_wasm_base/index.js:58:34)
      at callWasmExport (/Users/tsujp/programming/~aztec/tikan/node_modules/@aztec/bb.js/dest/node/barretenberg_wasm/barretenberg_wasm_main/index.js:85:14)
      at callback (/Users/tsujp/programming/~aztec/tikan/node_modules/comlink/dist/umd/comlink.js:109:52)
      at l (/Users/tsujp/programming/~aztec/tikan/node_modules/@aztec/bb.js/dest/node/barretenberg_wasm/helpers/node/node_endpoint.js:11:21)

[tsujp]

Ah, @Savio-Sou you mentioned here a ~500k circuit size. The circuit I posted above is 526338 gates which is indeed over 2^19.

[n4ru]

If your circuit is >2^19, currently your only option is to use a combination of nargo and barretenberg directly to generate a proof.

However, you can use said proofs via a single verify_proof in a circuit that itself is under the limit and compatible with NoirJS.

[Savio-Sou]

The circuit I posted above is 526338 gates which is indeed over 2^19.

Yes @tsujp it seems like the number of public inputs in your example exceeded what the WASM memory limit could hold.

The basically identical double_verify_proof test case with one public input is sized at 519,537 gates, marginally below 2^19 (i.e. 524,288).

[Savio-Sou]

Intermediary update on Noir v0.31.0 and bb v0.41.0:

On further debugging, we've found that with the proving backend barretenberg:

• double_verify_proof that simply verifies two normal proofs within is below WASM's 2^19 constraint limit
• double_verify_nested_proof that verifies two recursive proofs within is beyond WASM's 2^19 constraint limit; the linked code results in 536302 constraints to be exact

At some point changes resulted in the test case to creep beyond the 2^19 limit, causing verification of two recursive proofs in one (that is by extension compressing proofs in the binary tree manner >2 levels) to not currently work in JS.

This is hence a barretenberg issue (not of a problem inherent to Noir) and is logged accordingly as AztecProtocol/aztec-packages#6672.

A way to circumvent the WASM memory limit would be to gather the recursive proof artifacts and engage in the entire workflow in CLI; kudos to @akonior for creating a script to make things easier here: #4336 (comment)

In the meantime, the barretenberg team is coming up possible solutions for the problem; will circle back when there is further update 🙏

[Savio-Sou]

Informational update:

The barretenberg team has been working on getting the UltraHonk version of barretenberg to work with Noir: https://github.com/AztecProtocol/barretenberg/milestone/9, which might resolve the Issue here in one go. To confirm once the integration completes.

[Savio-Sou]

Early access steps of how to prove and verify Noir programs with UltraHonk are available here: https://github.com/AztecProtocol/aztec-packages/blob/86afa81d744bcf0c3ffd732663a24234b26e8aa8/barretenberg/cpp/src/barretenberg/bb/readme.md#usage-with-ultrahonk#usage-with-ultrahonk

If you come across bugs and bumps, the team is welcoming feedback there!