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

Implement numeric generics #620

Merged
merged 19 commits into from
Jan 31, 2023
Merged

Implement numeric generics #620

merged 19 commits into from
Jan 31, 2023

Conversation

jfecher
Copy link
Contributor

@jfecher jfecher commented Jan 5, 2023

Related issue(s)

Provides a workaround for #606 but does not resolve it

Description

Summary of changes

Allow generics to be used in array length types. For example, this allows

fn id<N>(array: [Field; N]) -> [Field; N] {
    array
}

Structs can also be parameterized over array lengths:

struct Foo<N> {
    limbs: [u64; N],
}

Some basic math on constants and globals (using +, -, *, and /) is also supported, although we do not officially support math on non-constants like N above. Supporting arithmetic on variables like N would require non-trivial unification and evaluation support on symbolic expressions.

Test additions / changes

Added test numeric_generics

Checklist

  • I have tested the changes locally.
  • I have formatted the changes with Prettier and/or cargo fmt with default settings.
  • I have linked this PR to the issue(s) that it resolves.
  • I have reviewed the changes on GitHub, line by line.
  • I have ensured all changes are covered in the description.

Additional context

Some care was taken to avoid naming this feature "const generics" even though it is effectively quite similar to rust's const generics feature. Avoiding this name lets us:

  1. Be more clear that we may not support the exact same feature set rust supports here, while also allowing us room in the future to expand or branch off in a different direction.
  2. Avoid a confusing name to newcomers. Particularly the const keyword being co-opted for compile-time evaluated expressions rather than just constants is confusing. This feature is also not called comptime generics in noir as we do not currently allow comptime variables within these generics. This is because comptime variables can be passed in as function arguments and allowing for these to be referenced would require something closer to dependent types.

@jfecher
Copy link
Contributor Author

jfecher commented Jan 5, 2023

Note that this PR seems to have found a new bug in either the SSA pass or acir gen - likely with regards to array handling or generic arrays now being allowed within structs. The error is currently occurring while running the new numeric_generics test. I need to do some more investigation on whether we should wait to merge or if the error should be fixed separately in a later PR and we should edit the test in the meantime. At the time of writing, this PR currently does not introduce any changes in noirc_evaluator.

Edit: I think it is a separate bug, perhaps more related to the sum(id(...)) function calls. I've swapped out the test with a slightly modified example from the bug report and it is proving and verifying correctly.

@jfecher
Copy link
Contributor Author

jfecher commented Jan 6, 2023

Fixed the bug in the global_consts test.
It is also worth mentioning this PR officially removes support for the use of local variables within array length types. This was never officially supported to begin with and was only possible via a bug that allowed it if the local was initialized to an integer.

In the future we can look into changing it to officially allow this rule but it impacts name resolution which will be greatly changed once the higher order functions PR is merged so I'd like to avoid these conflicts for now.

@jfecher jfecher requested review from guipublic and vezenovm January 9, 2023 16:04
Copy link
Contributor

@vezenovm vezenovm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this PR looks good. Just had a coupe minor questions

crates/noirc_frontend/src/hir_def/types.rs Outdated Show resolved Hide resolved
crates/noirc_frontend/src/hir_def/types.rs Outdated Show resolved Hide resolved
vezenovm
vezenovm previously approved these changes Jan 10, 2023
@jfecher
Copy link
Contributor Author

jfecher commented Jan 10, 2023

Added a commit fixing a bug where the previous representation of TypeExpression did not have a variant for NamedGenerics. This meant it was possible to have code which bound over named generics because it treated them wrongly as rebindable TypeVariables.
This meant the compiler previously accepted

fn bad_id<N, M>(a: [Field; N]) -> [Field; M] { a }

and now it correctly errors.

@jfecher
Copy link
Contributor Author

jfecher commented Jan 12, 2023

Alright, I've added support for parsing numeric generic expressions within the normal generic brackets <> as well. This likely should have been included from the start but I was worried how messy it would be to duplicate the expression parser. The final solution I landed on was adding a boolean parameter to parse_expression_with_precedence to indicate whether it should parse a normal expression or only the restricted syntax valid within type expressions. Other expression functions like term are still partially duplicated, though with most choices removed.

@jfecher jfecher mentioned this pull request Jan 12, 2023
5 tasks
@okuyiga
Copy link

okuyiga commented Jan 13, 2023

Does this PR contemplate support for numeric generics in implementations. I'm working on a bigint library and am particularly interested in support for something like this

struct BigInt<N> {
    limbs : [u32; N],
}

impl BigInt<N> {
    fn mul(self, other : BigInt<N>) -> BigInt<N * 2> {
        // ...
    }
}

Also this

fn loop_example<N>() -> Field {
    let mut sum = 0;
    for i in 0..N {
        sum = sum + i;
    }
    sum
}

@jfecher
Copy link
Contributor Author

jfecher commented Jan 13, 2023

Does this PR contemplate support for numeric generics in implementations?

Unfortunately not, impls currently do not support generics on the impl at all. This is planned though, and once generics on impls are supported numeric generics should come naturally with that. As for your specific examples I'll break them down a bit on what is supported and what is not:

// Structs generic over unsigned integer numerals will be entirely supported as of this PR
struct BigInt<N> {
    limbs : [u32; N],
}

// Generics on impls are not currently supported, but are planned for a later date
impl BigInt<N> {

    // Arithmetic on generic parameters (N here) is currently unsupported officially.
    // This PR provides the beginnings of support for them but offering full support would
    // require full unification support for these which would require a symbolic expression solver.
    // I'd like to experiment with expanding support for this in the future but this feature may be
    // unnecessary if Noir ever gets true array slice types `[T]` with no hidden size parameter.
    fn mul(self, other : BigInt<N>) -> BigInt<N * 2> {
        // ...
    }
}

fn loop_example<N>() -> Field {
    let mut sum = 0;
    
    // Using numeric generics as expressions themselves is also not supported. You can accomplish
    // something similar however by passing in N as a comptime Field parameter instead. If you have an
    // array type parameterized over N you can also extract it into a comptime Field via std::array::len.
    // I may work on making numeric generics directly useable within expressions eventually but it is
    // admittedly not the highest of priorities since there are workarounds present.
    for i in 0..N {
        sum = sum + i;
    }
    sum
}

Copy link
Contributor

@guipublic guipublic left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems that there are a lot of similar code and I am wondering if we could not try to unify somehow comptime and numeric generics in a new type which gets to become evaluated after monomorphisation?
I believe this new type would not be restricted to u64 and could be another integer size or fieldelement (of course it will be u64 is used for array len).
If you think it is a good idea but it would be a significant change, we should do it in a separate PR.
If you think it is a bad idea, we can forget about it.

crates/noirc_frontend/src/hir_def/types.rs Outdated Show resolved Hide resolved
@jfecher
Copy link
Contributor Author

jfecher commented Jan 30, 2023

Just added a commit removing the experimental feature of allowing arithmetic on generic integers like N+1 in fn grow_array<N>(array: [Field; N]) -> [Field; N+1] { ... }. This requires a full symbolic arithmetic solver if we truly want to support it.
It was originally added in this PR as an experiment and not officially supported, but users may run into it and file bugs when it was not as well supported as they hoped, so it has been removed from this PR for safety.
In the future, I think functions like grow_array would be better written via unsized slice/Vec types as encoding increasingly more information in types would naturally lead to dependent types which is not a goal of noir.

Copy link
Contributor

@guipublic guipublic left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's OK for me, I agree that trying to do more has some implications so it's a good first step for now.

@jfecher jfecher merged commit a484e28 into master Jan 31, 2023
@jfecher jfecher deleted the jf/impl-const-generics branch January 31, 2023 15:19
TomAFrench added a commit that referenced this pull request Feb 3, 2023
* master:
  Rename methods that use `conditionalize` to be more descriptive (#739)
  feat(noir)!:  Returned values are no longer required by the prover (#731)
  chore: explicit versions for dependencies (#727)
  chore: readability improvements (#726)
  feat(nargo): include short git commit in cli version output (#721)
  Remove print to console for named proofs in `nargo prove` (#718)
  chore: clean up serde-related dependencies (#722)
  Handle out-of-bound errors in CSE (#471) (#673)
  Remove unused dependencies and only use workspace inheritance on shared deps (#671)
  feat(std_lib)!: modulus bits/bytes methods, and to_bits -> to_le_bits (#697)
  Implement numeric generics (#620)
  Review some TODO in SSA (#698)
  Replace `toml_map_to_field` and `toml_remap` with traits to map between `InputValue`s and `TomlTypes` (#677)
  Apply witness visibility on a parameter level rather than witness level (#712)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants