result of shr differs in acir and brillig

[jewelofchaos9]

Aim

I'm trying to find differences between Brillig and ACIR execution results using fuzzing.

Expected Behavior

Same results for brillig and acir execution

Bug

Noir program

fn main(x: u64, y: u8) -> pub u64 {
  (x >> y)
}

with Prover.toml:

"x" = "16746359216597577687"
"y" = "65"

nargo execute -> Failed to solve program: 'Cannot satisfy constraint'

nargo debug:

[noir] Circuit witness successfully solved
[noir] Circuit output: Field(0)

To Reproduce

1. noir_version = 1.0.0-beta.1+bd33bebb6ed6c0192cd2a44e6a25e7b52ead04e1
2. nargo project with provided code and prover
3. in acir nargo execute
4. in brillig nargo debug and press n until Execution finished

Workaround

None

Workaround Description

No response

Additional Context

No response

Project Impact

None

Blocker Context

No response

Nargo Version

1.0.0-beta.1+bd33bebb6ed6c0192cd2a44e6a25e7b52ead04e1

NoirJS Version

No response

Proving Backend Tooling & Version

No response

Would you like to submit a PR for this Issue?

None

Support Needs

No response

[asterite]

Debugging this I found that this is only an issue when shifting right with an unknown value, and that value ends up being greater than the bit size of the target type.

For example, given this program:

fn main(x: u8) -> pub u8 {
    (1 >> x)
}

it works fine if Prover.toml has x = 8, but it fails if x = 9.

If we change the program to (1 >> 9) than that's optimized away to zero.

To clarify, we always want >> to give zero on "underflow".

To compute lhs >> rhs we do lhs / rhs^2. To do that we first compute rhs^2 by first casting rhs to Field, then casting rhs^2 back to the type of lhs to perform the division. The problem is that rhs^2 might exceed the range of valid values for that type.

In the example above, 2^9 is 512 and that doesn't fit in u8. At some points this is range-checked and it fails.

(for some reason it doesn't fail for 2^8=256 which would exceed the maximum value 🤔)

I'll try to limit the pow value to the maximum allowed, somehow, without using if.