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

Add GKR implementation of Grand Product lookups #620

Merged

Conversation

andrewmilson
Copy link
Contributor

@andrewmilson andrewmilson commented May 8, 2024

This change is Reviewable

@codecov-commenter
Copy link

codecov-commenter commented May 8, 2024

Codecov Report

Attention: Patch coverage is 92.79279% with 16 lines in your changes missing coverage. Please review.

Project coverage is 92.51%. Comparing base (2c6cbfd) to head (2980f55).
Report is 3 commits behind head on dev.

Files Patch % Lines
crates/prover/src/core/lookups/gkr_prover.rs 90.69% 8 Missing ⚠️
crates/prover/src/core/lookups/gkr_verifier.rs 92.64% 2 Missing and 3 partials ⚠️
crates/prover/src/core/backend/cpu/lookups/gkr.rs 95.52% 2 Missing and 1 partial ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##              dev     #620      +/-   ##
==========================================
+ Coverage   90.20%   92.51%   +2.31%     
==========================================
  Files          81       82       +1     
  Lines       10354    10908     +554     
  Branches    10354    10908     +554     
==========================================
+ Hits         9340    10092     +752     
+ Misses        930      721     -209     
- Partials       84       95      +11     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@andrewmilson andrewmilson changed the base branch from andrew/dev/lookups/gkr to 05-08-Implement_GkrOps_for_CPU_backend May 8, 2024 16:46
Base automatically changed from 05-08-Implement_GkrOps_for_CPU_backend to dev June 20, 2024 15:01
@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch 2 times, most recently from b375f43 to ca61e80 Compare June 22, 2024 19:05
Copy link
Contributor Author

@andrewmilson andrewmilson left a comment

Choose a reason for hiding this comment

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

Reviewable status: 1 of 12 files reviewed, 4 unresolved discussions (waiting on @shaharsamocha7 and @spapinistarkware)


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 32 at r3 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

n_variables or n_vars

Done.


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 35 at r3 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

What's this? Rename or doc.

Done.


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 51 at r3 (raw file):

                    let rhs0 = input_layer[(n_terms + i) * 2];
                    let rhs1 = input_layer[(n_terms + i) * 2 + 1];

Done.


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 54 at r3 (raw file):

                    let product2 = (rhs0.double() - lhs0) * (rhs1.double() - lhs1);
                    let product0 = lhs0 * lhs1;

Done.

@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch from ca61e80 to 789c3c9 Compare June 22, 2024 19:09
@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch from 789c3c9 to 9fbd265 Compare June 25, 2024 02:20
Copy link
Collaborator

@spapinistarkware spapinistarkware left a comment

Choose a reason for hiding this comment

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

Reviewable status: 1 of 12 files reviewed, 4 unresolved discussions (waiting on @andrewmilson and @shaharsamocha7)


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 30 at r5 (raw file):

    ) -> UnivariatePoly<SecureField> {
        let n_variables = h.n_variables();
        let n_terms = 1 << n_variables.saturating_sub(1);

Does this function work when n_variables == 0?

Code quote:

n_variables.saturating_sub(1)

crates/prover/src/core/backend/cpu/lookups/gkr.rs line 57 at r5 (raw file):

}

fn process_grand_product_sum(

Also, I'd like to doc somewhere that the GrandProduct layer poly is. Maybe at the enum definition.

P(x) = Inp(x,0) * Inp(x,1)

Suggestion:

/// Evaluates the sum of a grand product layer poly over a hypercube.
fn eval_grand_product_sum(

crates/prover/src/core/backend/cpu/lookups/gkr.rs line 58 at r5 (raw file):

fn process_grand_product_sum(
    eval_at_0: &mut SecureField,

Why get them as mut instead of return them? You are passing zeros.

@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch from 9fbd265 to 0cc0d79 Compare June 26, 2024 14:33
Copy link
Contributor Author

@andrewmilson andrewmilson left a comment

Choose a reason for hiding this comment

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

Reviewable status: 1 of 12 files reviewed, 4 unresolved discussions (waiting on @shaharsamocha7 and @spapinistarkware)


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 30 at r5 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

Does this function work when n_variables == 0?

It doesn't, thanks. Changed it to panic.


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 58 at r5 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

Why get them as mut instead of return them? You are passing zeros.

Done.

Copy link
Collaborator

@spapinistarkware spapinistarkware left a comment

Choose a reason for hiding this comment

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

Reviewed 1 of 2 files at r4, all commit messages.
Reviewable status: 2 of 12 files reviewed, 2 unresolved discussions (waiting on @andrewmilson and @shaharsamocha7)


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 45 at r7 (raw file):

        // 1. `sum_x eq(({0}^|r|, 0, x), y) * F(r, t, x)`
        // 2. `sum_x eq((r,       t, x), y) * F(r, t, x)`
        {

Why is this in a block?

Copy link
Collaborator

@spapinistarkware spapinistarkware left a comment

Choose a reason for hiding this comment

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

Reviewable status: 2 of 12 files reviewed, 3 unresolved discussions (waiting on @andrewmilson and @shaharsamocha7)


crates/prover/src/core/lookups/gkr_prover.rs line 391 at r7 (raw file):

/// * `k` is zero or greater than the length of `y`.
/// * `z_0` is zero.
pub fn correct_sum_as_poly_in_first_variable(

I think this function is kind of convoluted with respect to what it actually needs to do.
Here is my reasoning.

We evaluated f(0) and f(2) - the inputs.
We want to compute r(t) = f(t) * eq(t,z)/eq(0,z) / eq(0, y)
(I think this explicit formulat would also help the docs).

eq(0,y) is a const, call it a.
eq(t,z)/eq(0,z) =
(tz+(1-t)(1-z))/(1-z) =
1-t+tz/(1-z)=
1 - t(1 - z/(1-z))=
1 - t(2 - 1/(1-z))=
1-bt

We get that r(t) = f(t) * (1-bt) / a.
Also,
r(0) = f(0) / a
r(1) = claim - r(0)
r(2) = f(2)(1-2b) / a
r(1/b) = 0

Interpolate these.

@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch from 0cc0d79 to f8ff1d6 Compare July 8, 2024 04:43
Copy link
Contributor Author

@andrewmilson andrewmilson left a comment

Choose a reason for hiding this comment

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

Reviewable status: 1 of 12 files reviewed, 2 unresolved discussions (waiting on @shaharsamocha7 and @spapinistarkware)


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 57 at r5 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

Also, I'd like to doc somewhere that the GrandProduct layer poly is. Maybe at the enum definition.

P(x) = Inp(x,0) * Inp(x,1)

Done. Added to GkrMultivariatePolyOracle


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 45 at r7 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

Why is this in a block?

I added the block just to indicate the doc is for the whole block not the first multiplication

@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch 3 times, most recently from c3cede8 to bdac672 Compare July 11, 2024 14:40
Copy link
Collaborator

@spapinistarkware spapinistarkware left a comment

Choose a reason for hiding this comment

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

Reviewed 1 of 1 files at r10.
Reviewable status: 2 of 12 files reviewed, 3 unresolved discussions (waiting on @andrewmilson and @shaharsamocha7)


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 44 at r10 (raw file):

        // Corrects the difference between two univariate sums in `t`:
        // 1. `sum_x eq(({0}^|r|, 0, x), y) * F(r, t, x)`
        // 2. `sum_x eq((r,       t, x), y) * F(r, t, x)`

Does this actually refer to the whole block? Because from what I understood, correct_sum_as_poly_in_first_variable actually "lowers" the width of the eq.

Code quote:

        // Corrects the difference between two univariate sums in `t`:
        // 1. `sum_x eq(({0}^|r|, 0, x), y) * F(r, t, x)`
        // 2. `sum_x eq((r,       t, x), y) * F(r, t, x)`

crates/prover/src/core/lookups/gkr_prover.rs line 388 at r10 (raw file):

}

/// Computes `r(t) = sum_x eq((t, x), z) * p(t, x)` from evaluations of

I think inlining z is clearer

Suggestion:

`r(t) = sum_x eq((t, x), y[-k:]) * p(t, x)`

crates/prover/src/core/lookups/gkr_prover.rs line 407 at r10 (raw file):

    // We evaluated `f(0)` and `f(2)` - the inputs.
    // We want to compute `r(t) = f(t) * eq(t, z0) / eq(0, z0) / eq(0, y_{0:k})`.

It does seem redundant to split /eq(0, y[n-k]) and /eq(0, y_[:n-k]). We divide by both. Can we just divide by eq(0, y_[:n-k+1]) instead? And just write
eq(t,z0) = t * z0 + (1 - t)(1 - z0) = 1-z0 - t(1-2z0)

That might be more straight forward.

Suggestion:

// We want to compute `r(t) = f(t) * eq(t, y[n-k]) / eq(0, y[n-k]) / eq(0, y_[:n-k])`.

Copy link
Contributor Author

@andrewmilson andrewmilson left a comment

Choose a reason for hiding this comment

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

Reviewable status: 2 of 12 files reviewed, 3 unresolved discussions (waiting on @shaharsamocha7 and @spapinistarkware)


crates/prover/src/core/lookups/gkr_prover.rs line 407 at r10 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

It does seem redundant to split /eq(0, y[n-k]) and /eq(0, y_[:n-k]). We divide by both. Can we just divide by eq(0, y_[:n-k+1]) instead? And just write
eq(t,z0) = t * z0 + (1 - t)(1 - z0) = 1-z0 - t(1-2z0)

That might be more straight forward.

Don't we also need to do a division to find the value of t that makes r(t) = 0

@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch 3 times, most recently from aebb34a to 2980f55 Compare July 14, 2024 14:30
Copy link
Contributor Author

@andrewmilson andrewmilson left a comment

Choose a reason for hiding this comment

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

Reviewable status: 1 of 12 files reviewed, 3 unresolved discussions (waiting on @shaharsamocha7 and @spapinistarkware)


crates/prover/src/core/backend/cpu/lookups/gkr.rs line 44 at r10 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

Does this actually refer to the whole block? Because from what I understood, correct_sum_as_poly_in_first_variable actually "lowers" the width of the eq.

My bad, that was a typo. Removed.


crates/prover/src/core/lookups/gkr_prover.rs line 388 at r10 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

I think inlining z is clearer

Done.


crates/prover/src/core/lookups/gkr_prover.rs line 407 at r10 (raw file):

Previously, andrewmilson (Andrew Milson) wrote…

Don't we also need to do a division to find the value of t that makes r(t) = 0

Updated WDYT?

Copy link
Collaborator

@spapinistarkware spapinistarkware left a comment

Choose a reason for hiding this comment

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

Reviewed 1 of 2 files at r11, all commit messages.
Reviewable status: 2 of 12 files reviewed, 1 unresolved discussion (waiting on @andrewmilson and @shaharsamocha7)


crates/prover/src/core/lookups/gkr_prover.rs line 407 at r11 (raw file):

    // We evaluated `f(0)` and `f(2)` - the inputs.
    // We want to compute `r(t) = f(t) * eq(t, y[n - k]) / eq(0, y[:n - k + 1])`.

Amazing, super clear to me.


crates/prover/src/core/lookups/gkr_prover.rs line 410 at r11 (raw file):

    let a_const = eq(&vec![SecureField::zero(); n - k + 1], &y[..n - k + 1]).inverse();

    //    0 = eq(t, y[n - k])

Suggestion:

//    Find the additional root of r(t), by finding the root of eq(t, y[n - k])
//    0 = eq(t, y[n - k])

Copy link
Collaborator

@spapinistarkware spapinistarkware left a comment

Choose a reason for hiding this comment

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

:lgtm:

Reviewed 6 of 10 files at r2, 2 of 3 files at r3, 1 of 2 files at r8, 1 of 2 files at r11.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @andrewmilson and @shaharsamocha7)

@andrewmilson andrewmilson force-pushed the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch from 2980f55 to 35e313d Compare July 15, 2024 13:02
Copy link
Contributor Author

@andrewmilson andrewmilson left a comment

Choose a reason for hiding this comment

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

Reviewable status: 11 of 12 files reviewed, 1 unresolved discussion (waiting on @shaharsamocha7 and @spapinistarkware)


crates/prover/src/core/lookups/gkr_prover.rs line 391 at r7 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

I think this function is kind of convoluted with respect to what it actually needs to do.
Here is my reasoning.

We evaluated f(0) and f(2) - the inputs.
We want to compute r(t) = f(t) * eq(t,z)/eq(0,z) / eq(0, y)
(I think this explicit formulat would also help the docs).

eq(0,y) is a const, call it a.
eq(t,z)/eq(0,z) =
(tz+(1-t)(1-z))/(1-z) =
1-t+tz/(1-z)=
1 - t(1 - z/(1-z))=
1 - t(2 - 1/(1-z))=
1-bt

We get that r(t) = f(t) * (1-bt) / a.
Also,
r(0) = f(0) / a
r(1) = claim - r(0)
r(2) = f(2)(1-2b) / a
r(1/b) = 0

Interpolate these.

Done


crates/prover/src/core/lookups/gkr_prover.rs line 407 at r11 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

Amazing, super clear to me.

Great, thanks for the feedback


crates/prover/src/core/lookups/gkr_prover.rs line 410 at r11 (raw file):

    let a_const = eq(&vec![SecureField::zero(); n - k + 1], &y[..n - k + 1]).inverse();

    //    0 = eq(t, y[n - k])

Done

@andrewmilson andrewmilson merged commit 437ea59 into dev Jul 15, 2024
13 of 14 checks passed
@andrewmilson andrewmilson deleted the 05-08-Add_GKR_implementation_of_Grand_Product_lookups branch July 15, 2024 13:36
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.

None yet

3 participants