Type bound error when instantiating signed integers at negative boundary

[Savio-Sou]

Aim

Instantiate signed integers at but not exceeding their negative type boundaries.

Expected Behavior

E.g. given i8's boundary goes from -128 to 127, both of the following examples should work:

1. Adding a value up to the type boundary:

fn main() {
    let x : i8 = -127;
    let y : i8 = -1;
    x + y;
}

2. Instantiating variable at boundary:

fn main() {
    let x : i8 = -128;
}

Bug

Proving (1) works.

While attempting to prove (2) gave:

% nargo prove
error: 2⁷ does not fit within the type bounds for i8
┌─ ~/src/main.nr:13:19
│
│     let x : i8 = -128;
│                   ---
│
= Call stack:
  ...

This seems to only happen at the negative boundary, but not on the positive side.

Installation Method

Binary

Nargo Version

(Nightly)

nargo version = 0.18.0 noirc version = 0.18.0+a0985412594c5cbd35551afc7e94cb444723adb0 (git version hash: a098541, is dirty: false)

Additional Context

Discovered while drafting examples in #3393.

Would you like to submit a PR for this Issue?

No

Support Needs

No response

[Savio-Sou]

Assigning P-LOW under the assumption that this is a minor bug that does not affect a lot of users.

Please vote with emojis if your project is affected by this bug.

[jfecher]

This seems to only happen at the negative boundary, but not on the positive side.

This is because the integer isn't -128, it is 128 which you then take the negative of. Since 128 doesn't fit within an i8 you get an error explaining so (note the error message says 2^7, not (-2)^7).

We can add negative integer literals to fix this, I just wanted to explain the reason for this error.

[guipublic]

I have been looking into this and to add to Jake's comment, we translate -128 into 0-128. The expression 0-128 is invalid because it uses 128, although the original expression -128 is valid.
I tried to fix this by interpreting negative integers during ssa codegen but it is not satisfactory as -(-128) becomes -128. So I also agree that we need negative integer literals.