Nargo producing proofs which cannot be verified.

[TomAFrench]

Description

Aim

I'm attempting to create a function which when given a value in the range 0..64, will return a bit mask with the bit at that position and all subsequent bits turned on, i.e. f(0) -> 0xfffffffffffffff, f(1) -> 0x3fffffffffffffff, f(63) -> 0x0000000000000001

Expected behavior

To start with, lets create a bitmap which only contains the bit at the given position for which we use the below function:

fn main(bit_position: Field) -> pub u64 {

  // We cannot perform bitshifts with non-comptime values so the most efficient way to do this is with a lookup table.
  let bit_masks: [comptime u64; 64] = [
    0x8000000000000000, 0x4000000000000000, 0x2000000000000000, 0x1000000000000000,
    0x0800000000000000, 0x0400000000000000, 0x0200000000000000, 0x0100000000000000,
    0x0080000000000000, 0x0040000000000000, 0x0020000000000000, 0x0010000000000000,
    0x0008000000000000, 0x0004000000000000, 0x0002000000000000, 0x0001000000000000,
    0x0000800000000000, 0x0000400000000000, 0x0000200000000000, 0x0000100000000000,
    0x0000080000000000, 0x0000040000000000, 0x0000020000000000, 0x0000010000000000,
    0x0000008000000000, 0x0000004000000000, 0x0000002000000000, 0x0000001000000000,
    0x0000000800000000, 0x0000000400000000, 0x0000000200000000, 0x0000000100000000,
    0x0000000080000000, 0x0000000040000000, 0x0000000020000000, 0x0000000010000000,
    0x0000000008000000, 0x0000000004000000, 0x0000000002000000, 0x0000000001000000,
    0x0000000000800000, 0x0000000000400000, 0x0000000000200000, 0x0000000000100000,
    0x0000000000080000, 0x0000000000040000, 0x0000000000020000, 0x0000000000010000,
    0x0000000000008000, 0x0000000000004000, 0x0000000000002000, 0x0000000000001000,
    0x0000000000000800, 0x0000000000000400, 0x0000000000000200, 0x0000000000000100,
    0x0000000000000080, 0x0000000000000040, 0x0000000000000020, 0x0000000000000010,
    0x0000000000000008, 0x0000000000000004, 0x0000000000000002, 0x0000000000000001
  ];

  let mut bit_mask: u64 = 0;
  // We need to loop through here to be able to perform an array access with non-comptime index
  for j in 0..64 {
    if j == bit_position {
      bit_mask = bit_masks[j];
    }
  };

  bit_mask
}

This circuit works as expected. Given a value for bit_position, I can prove the return value is the corresponding entry in the array. To get the function we want we then just need to swap the return value out for 2 * bit_mask - 1. This is slightly wrong as we'll get an overflow if bit_position = 0 but we can ignore that for now (we can always adjust the for-loop range to avoid pulling out this value and not pass bit_position = 0).

Bug

# Prover.toml
bit_position = 63
return = 1

If I swap out the return value for 2 * bit_mask - 1 and attempt to prove the circuit with the simplest case of just turning on the last bit in the u64 with the Prover.toml file above, the nargo prove step works as expected but if I try to verify the produced proof then I get the output below.

$ nargo verify test
verifier deserialise : 1583310ns ~0seconds
creating verifier : 140295069ns ~0seconds
verifying proof : 1443116ns ~0seconds
Proof verified : false

Unless I'm making a really silly mistake somewhere I don't see how this could happen. In the first circuit we can prove that for bit_position = 63 results in bit_mask == 1. 2*1 - 1 = 1 so we should be able to create a valid proof for the provided inputs but we can't.

To reproduce

1. Create a noir project with the above snippet
2. Convince yourself that it proves/verifies correctly
3. Swap out the return value for 2 * bit_mask - 1
4. Run nargo prove and nargo verify using the sample Prover.toml below.

Environment

• OS: Ubuntu

For nargo users

• noir-lang/noir commit cloned: 0070622
• Proving backend
  • default
    • Clang: 10.0.0-4ubuntu1
  • wasm-base

Additional context

You might be wondering why I don't just update the bitmaps in the array rather than doing 2 * bit_mask - 1, I actually need both bitmasks.

[TomAFrench]

I just checked this with my old implementation (below) and I get the same behaviour.

fn main(bit_position: u64) -> pub u64 {

  let mut bit_mask: u64 = 1;
  for j in 0..64 {
    if (j as u64) > bit_position {
      bit_mask = bit_mask * 2;
    }
  };

  bit_mask
}

[vezenovm]

I am unable to reproduce this bug on the Noir master branch or the specific commit listed in the issue.

When using the correct inputs I generate a proof and then I get a verify true upon running nargo verify. When I changed the Prover.toml to incorrect inputs and ran nargo prove I got constraints not all satisfied as I expected. I tried with the input you provided and also

# Prover.toml
bit_position = 62
return = 2

for which I still got Proof verified: true.

@guipublic @jfecher would you be able to try and reproduce this bug?

[TomAFrench]

I just tried again and could reproduce on 44872e2. Just to make sure there's no miscommunication, the issue only arises if you change the return value from bit_mask to 2*bit_mask-1, if you just run the snippets above then you'll get the behaviour you described.

// This produces valid proofs
fn main(bit_position: u64) -> pub u64 {

  let mut bit_mask: u64 = 1;
  for j in 0..64 {
    if (j as u64) > bit_position {
      bit_mask = bit_mask * 2;
    }
  };

  bit_mask
}

// This produces invalid proofs
fn main(bit_position: u64) -> pub u64 {

  let mut bit_mask: u64 = 1;
  for j in 0..64 {
    if (j as u64) > bit_position {
      bit_mask = bit_mask * 2;
    }
  };

  2 * bit_mask - 1
}

[vezenovm]

Thank you for clarifying as there was a miscommunication. I was able to produce false proofs. This does look like a bug.

[guipublic]

I guess this issue is the same as #358

[vezenovm]

It looks as though this issue could be related to how we are handling bit decomposition and range constraints when solving a circuit. If we change the code snippets provided to use Field types for the bit masks we get the expected false proof. For the snippet below nargo will still generate a proof for false proofs (which points to something being incorrect with the PWG), however, we get the expected true or false for the correct respective prover inputs.

fn main(bit_position: Field) -> pub u64 {

  // We cannot perform bitshifts with non-comptime values so the most efficient way to do this is with a lookup table.
  let bit_masks: [comptime Field; 64] = [
    0x8000000000000000, 0x4000000000000000, 0x2000000000000000, 0x1000000000000000,
    0x0800000000000000, 0x0400000000000000, 0x0200000000000000, 0x0100000000000000,
    0x0080000000000000, 0x0040000000000000, 0x0020000000000000, 0x0010000000000000,
    0x0008000000000000, 0x0004000000000000, 0x0002000000000000, 0x0001000000000000,
    0x0000800000000000, 0x0000400000000000, 0x0000200000000000, 0x0000100000000000,
    0x0000080000000000, 0x0000040000000000, 0x0000020000000000, 0x0000010000000000,
    0x0000008000000000, 0x0000004000000000, 0x0000002000000000, 0x0000001000000000,
    0x0000000800000000, 0x0000000400000000, 0x0000000200000000, 0x0000000100000000,
    0x0000000080000000, 0x0000000040000000, 0x0000000020000000, 0x0000000010000000,
    0x0000000008000000, 0x0000000004000000, 0x0000000002000000, 0x0000000001000000,
    0x0000000000800000, 0x0000000000400000, 0x0000000000200000, 0x0000000000100000,
    0x0000000000080000, 0x0000000000040000, 0x0000000000020000, 0x0000000000010000,
    0x0000000000008000, 0x0000000000004000, 0x0000000000002000, 0x0000000000001000,
    0x0000000000000800, 0x0000000000000400, 0x0000000000000200, 0x0000000000000100,
    0x0000000000000080, 0x0000000000000040, 0x0000000000000020, 0x0000000000000010,
    0x0000000000000008, 0x0000000000000004, 0x0000000000000002, 0x0000000000000001
  ];

  let mut bit_mask: Field = 0;
  // We need to loop through here to be able to perform an array access with non-comptime index
  for j in 0..64 {
    if j == bit_position {
      bit_mask = bit_masks[j];
    }
  };

  (2 * bit_mask - 1) as u64
}

While the same snippet in the original post where we use u64 for the bit mask will cause this issue of invalid proofs being produced. The same behavior was seen with these snippets:

// This produces valid proofs
fn main(bit_position: u64) -> pub u64 {

  let mut bit_mask: Field = 1;
  for j in 0..64 {
    if (j as u64) > bit_position {
      bit_mask = bit_mask * 2;
    }
  };

  (2 * bit_mask - 1) as u64
}

// This produces invalid proofs
fn main(bit_position: u64) -> pub u64 {

  let mut bit_mask: u64 = 1;
  for j in 0..64 {
    if (j as u64) > bit_position {
      bit_mask = bit_mask * 2;
    }
  };

  2 * bit_mask - 1
}

[Fantoni0]

I am facing the same problem. Is this still an outgoing issue?
Nargo produces a proof that cannot later verify.

I think the proof is valid, since if I change any parameter in Prover.toml , nargo complaints about not satisfying all the constraints.

[vezenovm]

This issue has not yet been solved. Are you doing something similar to the code snippet above? Is it possible to post what you are working on here?

[Fantoni0]

A merkle proof based only in Pedersen hash.

use dep::std;
fn main(
    public_key: [Field; 2],
    index: Field,
    merkle_path: [Field; 3],
    merkle_root : pub Field,
) -> pub Field {

// Compute leaf
let leaf = std::hash::pedersen(public_key);

let is_member = std::merkle::check_membership(merkle_root, leaf[0] , index, merkle_path);
constrain is_member == 1;

merkle_root
}

[vezenovm]

And with which Prover.toml do you produce a false proof? I have not seen this with the merkle proofs so this is surprising. But it is most likely a related issue.

[Fantoni0]

With this configuration, let me know if you can replicate the issue.

public_key = ["0x0ba51a3fd0f698edf85d1a55056c9455184ffcf5bcad55ff12f5c7add823ed82", "0x2a68c3e25eaf46478c6820fc885a65b12241c8c10a9d9153cd4058cdf0d1aaed"]
index = "1"
merkle_path = ["0x125814ef721abadfee11d76feed2b096edacb999d3fc71fea94e5a1ef1f2bf78",
    "0x14ff5b0c5e2d284a2d15d9c0b7cec6ebc1a8a5f95642e8604e4e3b74ec499cb2",
    "0x187769436d5bab97500f1b0f301fb1b94913154e979a66b28d70b739199fa31a"]
merkle_root = "0x0e1801493bdf93b75e8f3e1b9c0b679d1da475ef1c5529b21938ed4ae9b7bb41"
return = "0x0e1801493bdf93b75e8f3e1b9c0b679d1da475ef1c5529b21938ed4ae9b7bb41"

[TomAFrench]

Confirming that this is still an issue for me as well when building on 673249f when using Fields or integers.

[vezenovm]

// This produces valid proofs
fn main(bit_position: u64) -> pub u64 {

let mut bit_mask: Field = 1;
for j in 0..64 {
if (j as u64) > bit_position {
bit_mask = bit_mask * 2;
}
};

(2 * bit_mask - 1) as u64
}

@TomAFrench This is giving false proofs for you?

[TomAFrench]

I get no difference between both implementations.

I've been using nargo execute to query the actual return value returned by the circuit and it seems to be correct if we don't provide an expected return value. If we do provide a return value however then the circuit repeats that value back to us.

Potentially the issue is that ACVM tries to write to the return value's witness, sees that it's already got a value and so doesn't write anything but doesn't check that the existing value matches the value it was going to write?

I've changed the circuit to have a public input and an explicit constrain and can create false proofs so it's not a return value specific issue.

[TomAFrench]

Probably worth checking after #731

[TomAFrench]

I'm going to close this issue as I can only create valid proofs now so this is fixed as far as I'm aware.

@Fantoni0 I've run your example and can verify a proof with the return value you specified. Please feel free to reopen if you still run into the issue on a current version of Nargo/Noir.

[Fantoni0]

@TomAFrench
I am using the latest release v0.1.1 and I am still not able to verify the proof. Neither in my example or #358 .
Nargo 0.1.1 (git:0c16089) returns false when I run nargo verify p.

[guipublic]

Probably worth checking after #731

As you said it is not a return value issue, so #731 cannot be the fix.

[kevaundray]

Tracking issue : #1252

[kevaundray]

@TomAFrench what is the status of this issue?

[TomAFrench]

This is almost certainly fixed at this point as the backend related code has completely changed since I opened this. I'll check and close this tonight though.

[Fantoni0]

I have tried the new nargo version (0.7.1) on #358 as it's easy and fast to verify.
The verifier now does not state that the result is false, it simply ends its execution with no error message or any kind of output. Is this the expected behavior?

[vezenovm]

The verifier now does not state that the result is false, it simply ends its execution with no error message or any kind of output. Is this the expected behavior?

Yes this is the expected functionality. We decided to follow the unix methodology that no output == no problems. If you see output it means there has been an error

[TomAFrench]

Thanks @Fantoni0! I'm going to close this issue as resolved in this case.