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

chore(ssa refactor): patch unsigned division and shift right algorithms #1528

Closed
wants to merge 4 commits into from

Conversation

kevaundray
Copy link
Contributor

Description

Previously unsigned division and Shr were using field division. Since we now have euclidean division, we can patch those algorithms to return the quotient

Problem*

Resolves

Summary*

This PR sets out to

Example

Before:


After:


Documentation

  • This PR requires documentation updates when merged.

    • I will submit a noir-lang/docs PR.
    • I will request for and support Dev Rel's help in documenting this PR.

Additional Context

PR Checklist*

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

@kevaundray kevaundray changed the base branch from master to kw/add-modulo June 3, 2023 19:09
@kevaundray
Copy link
Contributor Author

One issue is the fact that we are not capturing the bit size for constants, so (x as u32) >> 7 will try to check the bit size for x and see that it is 32, but then it will crash because we do not assign a bit size to 7

@kevaundray
Copy link
Contributor Author

Seems we are not entirely handling the shr and shl properly, due to the SSA not including an explicit cast for the results of shifts if its the same type.

Take the following code:

fn main(x : Field)  {
    let z = (x as u32) >> 4;
    let t = (x as u32) << 4;
    let r = ((t as u32) >> 8);
    assert(z == r);
}

It will translate to:

After Mem2Reg:
fn main f1 {
  b0(v0: Field):
    v1 = cast v0 as u32
    v3 = shr v1, u32 4
    v4 = cast v0 as u32
    v5 = shl v4, u32 4
    v7 = shr v5, u32 8
    v8 = eq v3, v7
    constrain v8
    return unit 0
}

Notice that although the original code has 3 casts, the ssa code only has two. In particular, there is no cast v5 as u32 instruction. Thats because the shl will return a type of u32, so technically v5 is already a u32.

One can verify this by checking the following program:

fn main(x : Field)  {
    let z = (x as u32) >> 4;
    let t = (x as u32) << 4;
    let r = ((t as u64) >> 8);
    assert(z as u64 == r);
}

Which will be converted to:

After Mem2Reg:
fn main f1 {
  b0(v0: Field):
    v1 = cast v0 as u32
    v3 = shr v1, u32 4
    v4 = cast v0 as u32
    v5 = shl v4, u32 4
    v6 = cast v5 as u64
    v8 = shr v6, u64 8
    v9 = cast v3 as u64
    v10 = eq v9, v8
    constrain v10
    return unit 0
}

@kevaundray
Copy link
Contributor Author

Going to make this reliant on #1530 since we introduce types from ssa ir which then allows us to get the bit size from the parameter

@jfecher
Copy link
Contributor

jfecher commented Jun 5, 2023

Right, as far as the SSA is concerned, t is already a u32 in the first example so there is no need to cast it again. This is related to #1487 not being implemented

Base automatically changed from kw/add-modulo to master June 6, 2023 14:15
@kevaundray
Copy link
Contributor Author

This is now outdated

@kevaundray kevaundray closed this Jun 22, 2023
@TomAFrench TomAFrench deleted the kw/patch-unsinged-division branch November 20, 2024 12:01
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