Add GKR implementation of Grand Product lookups

[andrewmilson]

This change is 

[andrewmilson]

• Add eval order and interpolate to SecureEvaluation #794
• Add MLE eval constraints #742
• Add eq evals constraints #741
• Add benchmarks for GKR lookups #673
• Implement LogupOps for SIMD backend #641
• Implement GrandProductOps for SIMD backend #640
• Implement GkrOps for SIMD backend #630
• Implement MleOps for SIMD backend #629
• Add GKR implementation of Logup lookups #623
• Add GKR implementation of Grand Product lookups #620 👈
• Implement GkrOps for CPU backend #621
• Add batch GKR prover and verifier #581
• Rename CPU* structs to Cpu* to conform to Rust's naming convention #617
• Remove AVX backend #616
• Convert wide_fibbonacci AVX backend example to SIMD backend #615
• Update CI to test Wasm simd128, avx2 and aarch64 neon #614
• Fix CirclePointIndex bug in debug mode for 32-bit archs #613
• Change opt-level in benchmarks script #612
• Add benchmarks for SIMD m31 #611
• Add benchmarks for SIMD merkle #610
• dev

This stack of pull requests is managed by Graphite. Learn more about stacking.

Join @andrewmilson and the rest of your teammates on Graphite

[codecov-commenter]

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]

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.

[spapinistarkware]

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]

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.

[spapinistarkware]

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?

[spapinistarkware]

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]

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

[spapinistarkware]

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])`.

[andrewmilson]

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]

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?

[spapinistarkware]

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])

[spapinistarkware]

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]

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