Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Integer type value checking and integer type casts not working #3227

Closed
tsujp opened this issue Oct 20, 2023 · 3 comments · Fixed by #3236
Closed

Integer type value checking and integer type casts not working #3227

tsujp opened this issue Oct 20, 2023 · 3 comments · Fixed by #3236
Labels
bug Something isn't working

Comments

@tsujp
Copy link
Contributor

tsujp commented Oct 20, 2023

Aim

I am trying to define a function which takes a 6-bit integer u6 and further does stuff (not relevant) with it. I noticed that even if I define such a function, e.g. foo(var: u6), that input which is clearly not 6-bits in size is allowed foo(9999999999999999999).

This lead me to adding range checking on the input, however I believe that in the past attempting to invoke foo this way would result in an error. Anyway, range checking:

fn foo(alpha: BitboardIndex) {
    let beta: u6 = alpha as u6;
    println(f"Alpha (untouched): {alpha}  /  Beta: {beta}");

    // This always INCORRECTLY passes because invalid input for `alpha` of type
    //   larger than 6-bit is range constrained down to the modulo of the input
    //   value and the input-parameters-type's maximum value.
    // So an input of 0x93 here will result in `alpha` of 0x13 (0x93 % 0x40 = 0x13).
    assert(0 <= beta & beta <= 63);
}

The above function foo's assertion will always pass. Even if called with values above 6-bit.

While not shown in the println output for foo if I define a function bar:

fn bar(alpha: Field) {
    let beta: u6 = alpha as u6;
    println(f"Alpha (untouched): {alpha}  /  Beta: {beta}");

    assert(0 <= beta & beta <= 63);
}

You can see (when run) that beta becomes equal to the last nibble of the constrained value given to bar and since 2^4 will always be within closed range 0 - 63 the assertion always passes.

For input values which are already valid println shows the values correctly.

I feel like this wasn't the case in the past. Calling foo or bar with an incorrect value (as known at compile-time since these are static) should be an error, no? If not then range constraints feel useless within code however apparently will result in a proof failing verification. Although given the nature of the range constraining here I imagine it is possible to be VERY unlucky and somehow result in a valid value still which passes proof verification?

Expected Behavior

  1. Obvious (statically inferable) invalid input to functions should result in a compiler error the same as mismatched types do.
  2. If not, range checking should not produce unexpected results and such casting should result in invalid values or consistent values (e.g. always 0 and not the last nibble of the input).

Bug

Nargo version:

nargo 0.16.0 (git version hash: c4faf3a0a40eea1ee02e11dfe08b48c6b4438bbf, is dirty: false)

Command:

$ nargo test --show-output

Sources:

Nargo.toml

[package]
name = 'foo_bar'
authors = ["Jordan Ellis Coppard <$(printf 'amMrZ2l0QHd6Lmh0Cg==' | base64 -d)>"]
compiler_version = '0.16.0'
type = 'lib'

[dependencies]
use dep::std::println;

type BitboardIndex = u6;

fn foo(alpha: BitboardIndex) {
    let beta: u6 = alpha as u6;
    println(f"Alpha (untouched): {alpha}  /  Beta: {beta}");

    // This always INCORRECTLY passes because invalid input for `alpha` of type
    //   larger than 6-bit is range constrained down to the last hex-digit of
    //   the invalid input.
    assert(0 <= beta & beta <= 63);
}


fn bar(alpha: Field) {
    let beta: u6 = alpha as u6;
    println(f"Alpha (untouched): {alpha}  /  Beta: {beta}");

    assert(0 <= beta & beta <= 63);
}


#[test]
fn test() {
    println(f""); // Fix missing newline after Nargo test-name output.

    println(f"Foo tests ----------------------------------------------------");

    foo(
        0x39, // Within 6-bits (decimal 63).
    );

    foo(
        0x40 // NOT within 6-bits (decimal 64).
    );

    // Obviously both are much larger than 6-bits.
    foo(0x85);
    foo(0x8c3defb1edb984fe2ac71c71c7);
        
    println(f"Bar tests ----------------------------------------------------");

    bar(
        0x39, // Within 6-bits (decimal 63).
    );

    bar(
        0x40 // NOT within 6-bits (decimal 64).
    );

    // Obviously both are much larger than 6-bits.
    bar(0x85);
    bar(0x8c3defb1edb984fe2ac71c71c7);
}

To Reproduce

  1. Use nargo version as described above.
  2. Paste source code as described above.
  3. Run command as described above.

Installation Method

Compiled from source

Nargo Version

nargo 0.16.0 (git version hash: c4faf3a, is dirty: false)

Additional Context

No response

Would you like to submit a PR for this Issue?

Maybe

Support Needs

No response

@tsujp tsujp added the bug Something isn't working label Oct 20, 2023
@tsujp
Copy link
Contributor Author

tsujp commented Oct 20, 2023

Amending function bar to this results in correct range checking:

fn bar(alpha: Field) {
    let beta: u6 = alpha as u6;
    println(f"Alpha (untouched): {alpha}  /  Beta: {beta}");

    assert((alpha == beta as Field) & 0 <= beta & beta <= 63);
    //     ^^^^^^^^^^^^^^^^^^^^^^^^^^
}

@tsujp
Copy link
Contributor Author

tsujp commented Oct 20, 2023

As an aside, hex literals will cause the assertion to always fail:

assert((alpha == beta as Field) & 0 <= beta & beta < 0x40);
                                                   ^^^^^^

@jfecher
Copy link
Contributor

jfecher commented Oct 20, 2023

Hmm looks like we're missing an error ensuring an integer constant is within the range of its inferred type

jfecher added a commit that referenced this issue Oct 20, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
Archived in project
Development

Successfully merging a pull request may close this issue.

2 participants