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.