Proving phase fails for operations on negative literals

[Jurarpereurs]

Aim

If you do some operations over a negative literal, e.g., 2 * -1, the proving phase would complain that some constraints are not satisfied. This is unexpected, since 2 * -1 is just -2, which is a valid literal.

Consider the following example:

let t: u32 =  2 * -1;

The proving phase would complain that the following constraints are not satisfied:

error: Unsatisfied constraint
  ┌─ /home/Jurarpereurs/noir/src/main.nr:5:19
  │
5 │     let t: u32 =  2 * -1;
  │                   ------ Constraint failed

Error: could not satisfy all constraints

Location:
    crates/nargo_cli/src/cli/mod.rs:74:5

If you explicitly cast the negative literal to the target type, the proving phase still fails:

let t: u32 =  2 * (-1 as u32);

If you directly assign the negative literal to the target type, the proving phase would succeed:

let t: u32 =  -2;

Expected Behavior

The proving phase should succeed for all the three cases.

let t: u32 =  2 * -1;
let t: u32 =  2 * (-1 as u32);
let t: u32 =  -2;

Bug

The proving phase throws an error message for the line:

let t: u32 =  2 * -1;

with the error message as:

error: Unsatisfied constraint
  ┌─ /home/Jurarpereurs/noir/src/main.nr:5:19
  │
5 │     let t: u32 =  2 * -1;          // This one fails
  │                   ------ Constraint failed

Error: could not satisfy all constraints

Location:
    crates/nargo_cli/src/cli/mod.rs:74:5

To Reproduce

Save the following code into src/main.nr:

use dep::std;

fn main() {
    let t: u32 = -2;               // This one succeeds
    let t: u32 =  2 * -1;          // This one fails
    // let t: u32 =  2 * (-1 as u32); // This one also fails
    std::println(t);
}

Then run the following command:

nargo prove p

Installation Method

Binary

Nargo Version

nargo 0.9.0 (git version hash: 6acc242, is dirty: false)

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response

[jfecher]

Probably related to #2045

[Jurarpereurs]

I just quickly checked the latest version of Noir, and found that this issue hasn't been correctly fixed yet. Although the compiler doesn't complain about the 2 * -1 operation, it somehow throws an error on a simple statement as let a: u32 = -1. To reproduce, please refer to the issue #2045, and you will find the compiler would throw an error that piece of code with the following message:

error: u8 cannot be used in a unary operation