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

fix: SSA typing for loop bounds #4290

Closed
wants to merge 1 commit into from

Conversation

sirasistant
Copy link
Contributor

@sirasistant sirasistant commented Feb 7, 2024

Description

Problem*

Partial work towards #4275

Summary*

The frontend is not enforcing typing on loop bounds in some cases:

fn loop_from<N, K>(_arr: [Field; N], _another: [Field; K]) -> u32 {
    let mut acc = 0;
    // N and K are type Field but the iterator is u32
    for i in N..K {
        acc += i;
    }
    acc
}

fn main() -> pub u32 {
    loop_from([0; 10], [0; 20])
}

This PR casts the types of the bounds at the SSA level with the iterator type but we might want to enforce this in the frontend instead. I think the mismatch only happens on generic bounds so it might be painful to fix.

Additional Context

Documentation*

Check one:

  • No documentation needed.
  • Documentation included in this PR.
  • [Exceptional Case] Documentation to be submitted in a separate PR.

PR Checklist*

  • I have tested the changes locally.
  • I have formatted the changes with Prettier and/or cargo fmt on default settings.

Copy link
Contributor

@jfecher jfecher left a comment

Choose a reason for hiding this comment

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

The frontend does unify the type for loop bounds. The issue is related to #4118 where the frontend does not actually have a type for "any integer except Field." Once that PR is fixed & merged this issue should be fixed as well.

@sirasistant
Copy link
Contributor Author

Thanks Jake! Will it also fix a case like this one?:

  fn bit_mul<N>(self, bits: [u1; N], p: Point) -> Point {
            let mut out = Point::zero();
            
            for i in 0..N {
                out = self.add(
                    self.add(out, out),
                    if(bits[N - i - 1] == 0) {Point::zero()} else {p});
            }

            out
        }

Where the N is not only used in the end range, but also in bits[N - i - 1] ? I think I'm seeing mismatched types in the loop end range but also in the binary operations to compute the bits index

@sirasistant
Copy link
Contributor Author

Oh, I think your message in that PR addresses exactly that

github-merge-queue bot pushed a commit that referenced this pull request Feb 13, 2024
# Description

Add a new `TypeVariableKind` specifically for Integers: until this PR,
`IntegerOrField` is used.

## Problem\*

May resolve #3639,
#4290

## Summary\*

Adds the new `TypeVariableKind`
- [x] Unify
- [x] Test
- [ ] Docs

## Additional Context



## Documentation\*

Check one:
- [ ] No documentation needed.
- [x] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.

---------

Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
Co-authored-by: jfecher <jake@aztecprotocol.com>
@sirasistant
Copy link
Contributor Author

sirasistant commented Feb 14, 2024

@jfecher @michaeljklein just tested on master after #4118 was merged and we still have different types in the example in the description:

Types of loop: index Numeric(Unsigned { bit_size: 32 }), start Numeric(NativeField), end Numeric(NativeField)

@jfecher
Copy link
Contributor

jfecher commented Feb 14, 2024

@sirasistant yep, sorry that is expected. We decided to split that PR into one that adds the new type variable kind, and then another later PR to use the new type variable kind in for loops and bitwise operations. I'll update this thread when the second PR is up

@jfecher
Copy link
Contributor

jfecher commented Feb 14, 2024

@sirasistant #4376 should fix the issue

@sirasistant
Copy link
Contributor Author

fixed in #4386

github-merge-queue bot pushed a commit that referenced this pull request Feb 15, 2024
# Description

## Problem\*

Resolves #4290 

## Summary\*

Previously, the monomorphizer would assume all numeric generics were
Fields, but this was not necessarily true.

## Additional Context



## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.
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.

2 participants