Nargo fails to verify the proof (repro attached)

[LogvinovLeon]

Aim

I would like to be able to generate a proof and then verify it

Expected Behavior

Nargo verify succeeds after

Bug

Nargo verfiy fails

To Reproduce

1. Install nargo 0.24.0. noirup --version 0.24.0
2. git clone [email protected]:vlayer-xyz/nargo-verify-repro.git
3. cd nargo-verify-repro
4. nargo prove
5. nargo verify - Fails

Project Impact

Blocker

Impact Context

It's a blocker because nargo generates proofs that are invalid.

Workaround

None

Workaround Description

No response

Additional Context

No response

Installation Method

Binary (noirup default)

Nargo Version

noirc version = 0.24.0+df04ce9d72581416665e7e420d188d61d6cdc529

NoirJS Version

No response

Would you like to submit a PR for this Issue?

None

Support Needs

No response

[TomAFrench]

I can reproduce this on master

[vezenovm]

@LogvinovLeon Would you be able to link the repo in the issue so we don't have to go searching for it?

[LogvinovLeon]

It is linked in the repro steps, but here is the link one more time: [email protected]:vlayer-xyz/nargo-verify-repro.git
Or http version: https://github.com/vlayer-xyz/nargo-verify-repro

[LogvinovLeon]

Here is it's contents inline:

global number = 14194126;
global hash = 0;

global block_header_partial = BlockHeaderPartial { number, hash};

struct BlockHeaderPartial {
    number: Field,
    hash: Field,
}

fn main(block_no: pub Field) -> pub BlockHeaderPartial {
    let block_header_partial = get_header_unconstrained(block_no);
    assert(block_header_partial.number == block_no);
    block_header_partial
}

unconstrained fn get_header_unconstrained(block_no: Field) -> BlockHeaderPartial {
    block_header_partial
}

[LogvinovLeon]

Is there any workaround around this? This is making it impossible for us to enable all assertions we want on our system and therefore - the proofs we're generating do not satisfy soundness. So for us - we can't fix our critical security vulnerability before this is fixed. (although we're not live yet).

Also - the optics on this are pretty bad as it's not an issue in noir-js or solidity but core nargo.

[guipublic]

I have been able to reproduce this with an even smaller example:

fn main(block_no: pub Field) -> pub [Field;2] {
   [block_no, 0]
}

The next step for me is to reproduce it within a Barretenberg test case, which I have not been able to do yet.

[vezenovm]

@guipublic The basic reproduction looks like we are returning the same input witness as output, so I tried adding a distinct keyword.

fn main(block_no: pub Field) -> distinct pub [Field;2] {
   [block_no, 0]
}

This successfully proves and verifies for me. Adding distinct to the program output @LogvinovLeon posted above also successfully verified for me. For now this is the workaround @LogvinovLeon.

This verify false is still deceiving though and we should improve this handling of duplicate inputs/outputs. @guipublic This should help for a barretenberg test case as well.