Add batch GKR prover and verifier

[andrewmilson]

This change is 

[codecov-commenter]

Codecov Report

Attention: Patch coverage is 14.15094% with 273 lines in your changes missing coverage. Please review.

Project coverage is 89.80%. Comparing base (6b29913) to head (30790f2).

Files	Patch %	Lines
crates/prover/src/core/lookups/gkr_prover.rs	0.00%	146 Missing ⚠️
crates/prover/src/core/lookups/gkr_verifier.rs	0.00%	124 Missing ⚠️
crates/prover/src/core/lookups/utils.rs	93.18%	3 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##              dev     #581      +/-   ##
==========================================
- Coverage   92.40%   89.80%   -2.60%     
==========================================
  Files          69       71       +2     
  Lines        9030     9337     +307     
  Branches     9030     9337     +307     
==========================================
+ Hits         8344     8385      +41     
- Misses        614      880     +266     
  Partials       72       72              

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

[spapinistarkware]

Reviewed all commit messages.
Reviewable status: 0 of 4 files reviewed, 2 unresolved discussions (waiting on @andrewmilson and @shaharsamocha7)

---

src/core/lookups/gkr.rs line 81 at r1 (raw file):

    ///
    /// [`sumcheck::prove_batch()`]: crate::core::lookups::sumcheck::prove_batch
    fn into_sumcheck_oracle(

How about something like this?
"Represents this GKR layer evaluation as a multivariate polynomial which uses the previous GKR layer as input."

Suggestion:

into_multivariate_poly

---

src/core/lookups/gkr.rs line 83 at r1 (raw file):

    fn into_sumcheck_oracle(
        self,
        lambda: SecureField,

doc

Code quote:

lambda: SecureField,

[andrewmilson]

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

---

src/core/lookups/gkr.rs line 81 at r1 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

How about something like this?
"Represents this GKR layer evaluation as a multivariate polynomial which uses the previous GKR layer as input."

Sounds good but I think "Represents the next GKR layer as a multivariate polynomial which uses this GKR layer as input." might be more accurate. WDYT?

---

src/core/lookups/gkr.rs line 83 at r1 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

doc

Updated. WDYT?

[spapinistarkware]

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

---

crates/prover/src/core/lookups/gkr.rs line 232 at r4 (raw file):

/// the OOD point. These evaluations are not checked by this function - hence partial verification.
pub fn partially_verify_batch(
    circuit_unit_by_component: Vec<&dyn GkrBinaryCircuitUnit>,

Why does this assume a binary circuit, and the prove does not? (Gets a GkrLayer)

---

src/core/lookups/gkr.rs line 81 at r1 (raw file):

Previously, andrewmilson (Andrew Milson) wrote…

Sounds good but I think "Represents the next GKR layer as a multivariate polynomial which uses this GKR layer as input." might be more accurate. WDYT?

sg.

[shaharsamocha7]

Reviewed 4 of 6 files at r4, all commit messages.
Reviewable status: 4 of 6 files reviewed, 5 unresolved discussions (waiting on @andrewmilson)

---

crates/prover/src/core/lookups/utils.rs line 178 at r4 (raw file):

    assert_eq!(x.len(), y.len());
    zip(x, y)
        .map(|(&xi, &wi)| xi * wi + (F::one() - xi) * (F::one() - wi))

Suggestion:

    zip(x, y)
        .map(|(&xi, &yi)| xi * yi + (F::one() - yi) * (F::one() - yi))

---

crates/prover/src/core/lookups/gkr.rs line 21 at r4 (raw file):

pub trait GkrOps: MleOps<SecureField> {
    /// Returns the evaluations of [`eq(x, y)`] for all values of `x = (x_0, ..., x_{n-1})` where
    /// `x_0 = 0` and `x_1, ..., x_{n-1}` in `{0, 1}`.

Consider writing the comment as follow, not sure if it's better

Suggestion:

    /// Returns the evaluations of [`eq(x, y)`] for all the boolean hypercube points of the form `x = (0, x_1, ..., x_{n-1})`.

---

crates/prover/src/core/lookups/gkr.rs line 43 at r4 (raw file):

        let y = y.to_vec();
        let evals = B::gen_eq_evals(&y);
        assert_eq!(evals.len(), 1 << y.len().saturating_sub(1));

Why do you need this assert?

Code quote:

        assert_eq!(evals.len(), 1 << y.len().saturating_sub(1));

[shaharsamocha7]

Reviewable status: 4 of 6 files reviewed, 6 unresolved discussions (waiting on @andrewmilson)

---

crates/prover/src/core/lookups/gkr.rs line 76 at r4 (raw file):

    ///
    /// Layers can contain multiple columns `c_0, ..., c_{n-1}` with multivariate polynomial `g_i`
    /// representing `c_i` in the next layer. These polynomials must must be combined with `lambda`

Duplicate

Suggestion:

These polynomial must be combined with `lambda`

[andrewmilson]

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

---

crates/prover/src/core/lookups/utils.rs line 178 at r4 (raw file):

    assert_eq!(x.len(), y.len());
    zip(x, y)
        .map(|(&xi, &wi)| xi * wi + (F::one() - xi) * (F::one() - wi))

Done.

---

crates/prover/src/core/lookups/gkr.rs line 43 at r4 (raw file):

Previously, shaharsamocha7 wrote…

Why do you need this assert?

Just a sanity check to make sure the backend returns the expected amount of evaluations

---

crates/prover/src/core/lookups/gkr.rs line 76 at r4 (raw file):

Previously, shaharsamocha7 wrote…

Duplicate

Done.

---

crates/prover/src/core/lookups/gkr.rs line 232 at r4 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

Why does this assume a binary circuit, and the prove does not? (Gets a GkrLayer)

Changed GkrLayer to GkrBinaryLayer

[andrewmilson]

• 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

[andrewmilson]

Reviewable status: 3 of 9 files reviewed, 4 unresolved discussions (waiting on @andrewmilson, @shaharsamocha7, and @spapinistarkware)

---

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

Previously, spapinistarkware (Shahar Papini) wrote…

Not sure this name should appear in the interface. If you add error cases in the future, it will break the naming. Maybe make it an enum with a single variant instead?

I think it's just as problematic. Still a breaking change if other enum variants are added in the future

[shaharsamocha7]

Reviewed 1 of 6 files at r4, 1 of 1 files at r6, 1 of 2 files at r8, 1 of 3 files at r10, 1 of 2 files at r11, all commit messages.
Reviewable status: 8 of 9 files reviewed, 3 unresolved discussions (waiting on @andrewmilson and @spapinistarkware)

---

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

pub trait GkrOps: MleOps<SecureField> {
    /// Returns evaluations `eq(x, y) * v` for all `x` in `{0, 1}^n`.

Does it return in regular order?

Code quote:

/// Returns evaluations `eq(x, y) * v` for all `x` in `{0, 1}^n`.

---

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

pub trait GkrBinaryGate {
    /// Returns the output row after applying the gate to the provided input rows.
    fn eval(&self, row0: &[SecureField], row1: &[SecureField]) -> Vec<SecureField>;

Why does the inputs called row?

Code quote:

fn eval(&self, row0: &[SecureField], row1: &[SecureField]) -> Vec<SecureField>;

[shaharsamocha7]

Reviewable status: 8 of 9 files reviewed, 4 unresolved discussions (waiting on @andrewmilson and @spapinistarkware)

---

crates/prover/src/core/lookups/gkr.rs line 519 at r11 (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(

Remove from this pr as discussed.

Code quote:

pub fn correct_sum_as_poly_in_first_variable(

[shaharsamocha7]

Reviewed 3 of 6 files at r12, all commit messages.
Reviewable status: 8 of 11 files reviewed, 6 unresolved discussions (waiting on @andrewmilson and @spapinistarkware)

---

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

pub trait GkrOps: MleOps<SecureField> {
    /// Returns evaluations `eq(x, y) * v` for all `x` in `{0, 1}^n`.

Does it return in regular order?

Code quote:

    /// Returns evaluations `eq(x, y) * v` for all `x` in `{0, 1}^n`.

---

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

    fn is_output_layer(&self) -> bool {
        self.n_variables() == 0
    }

Does it assumes that we only have one output?

Code quote:

    fn is_output_layer(&self) -> bool {
        self.n_variables() == 0
    }

---

crates/prover/src/core/lookups/utils.rs line 173 at r12 (raw file):

/// Returns `v_0 + alpha * v_1 + ... + alpha^(n-1) * v_{n-1}`.
pub fn random_linear_combination(v: &[SecureField], alpha: SecureField) -> SecureField {

Can you check if we already have this util func somewhere in the code?

Code quote:

random_linear_combination

[andrewmilson]

Reviewable status: 8 of 11 files reviewed, 5 unresolved discussions (waiting on @andrewmilson, @shaharsamocha7, and @spapinistarkware)

---

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

Previously, shaharsamocha7 wrote…

Does it return in regular order?

Mle stores values in bit-reversed order

---

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

Previously, shaharsamocha7 wrote…

Does it assumes that we only have one output?

Yes, assumes each column has a single value since it's just for lookups

---

crates/prover/src/core/lookups/utils.rs line 173 at r12 (raw file):

Previously, shaharsamocha7 wrote…

Can you check if we already have this util func somewhere in the code?

Couldn't find an existing function for it

---

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

Previously, shaharsamocha7 wrote…

Why does the inputs called row?

Updated to take mask

---

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

Previously, shaharsamocha7 wrote…

Remove from this pr as discussed.

Done.

[shaharsamocha7]

Reviewable status: 8 of 11 files reviewed, 3 unresolved discussions (waiting on @andrewmilson and @spapinistarkware)

---

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

Previously, andrewmilson (Andrew Milson) wrote…

Mle stores values in bit-reversed order

consider to document here.

---

crates/prover/src/core/lookups/utils.rs line 173 at r12 (raw file):

Previously, andrewmilson (Andrew Milson) wrote…

Couldn't find an existing function for it

you have that one:

stwo/crates/prover/src/core/utils.rs

Line 92 in 9259c07

pub fn shifted_secure_combination(

[spapinistarkware]

Reviewed 1 of 1 files at r6, all commit messages.
Reviewable status: 8 of 11 files reviewed, 6 unresolved discussions (waiting on @andrewmilson)

---

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

impl<B: GkrOps> EqEvals<B> {
    pub fn new(y: &[SecureField]) -> Self {

When calling new, it is clear that there is a significant amount of work being done. Rename it to something that does convey that

Code quote:

new

---

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

/// [LogUp]: https://eprint.iacr.org/2023/1284.pdf
pub enum Layer<B: GkrOps> {
    _LogUp(B),

Why Does it have a B value? Sounds a bit weird

Code quote:

B

---

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

/// A multivariate polynomial expressed in the multilinear poly columns of a [`Layer`].
pub enum GkrMultivariatePolyOracle {

Is this different than the Layer enum? Can they ever diverge?

[spapinistarkware]

Reviewed 1 of 6 files at r12.
Reviewable status: 9 of 11 files reviewed, 6 unresolved discussions (waiting on @andrewmilson)

[spapinistarkware]

Reviewable status: 9 of 11 files reviewed, 9 unresolved discussions (waiting on @andrewmilson)

---

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

pub struct NotConstantPolyError;

// GKR algorithm: <https://people.cs.georgetown.edu/jthaler/ProofsArgsAndZK.pdf> (page 64)

Add a doc about soundness assumptions.
For example, the input layer have been committed to the channel.

---

crates/prover/src/core/lookups/gkr_verifier.rs line 170 at r12 (raw file):

///
/// [Thaler13]: https://eprint.iacr.org/2013/351.pdf
pub enum Gate {

It's the third time we have this enum. Do they need to be separated?

---

crates/prover/src/core/lookups/gkr_verifier.rs line 188 at r12 (raw file):

impl From<InvalidNumMaskColumnsError> for GkrError {
    fn from(_: InvalidNumMaskColumnsError) -> Self {
        Self::MalformedProof

This is losing information, right? Perhaps we want to keep it?

[spapinistarkware]

Reviewable status: 9 of 11 files reviewed, 9 unresolved discussions (waiting on @andrewmilson)

---

crates/prover/src/core/lookups/gkr_verifier.rs line 188 at r12 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

This is losing information, right? Perhaps we want to keep it?

I mean, perhaps encapsulate this type inside GkrError

[spapinistarkware]

Reviewed 3 of 6 files at r4, 1 of 2 files at r8, 5 of 6 files at r12.
Reviewable status: all files reviewed, 8 unresolved discussions (waiting on @andrewmilson)

[andrewmilson]

Reviewable status: 8 of 11 files reviewed, 7 unresolved discussions (waiting on @shaharsamocha7 and @spapinistarkware)

---

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

Previously, spapinistarkware (Shahar Papini) wrote…

When calling new, it is clear that there is a significant amount of work being done. Rename it to something that does convey that

Done.

---

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

Previously, spapinistarkware (Shahar Papini) wrote…

Why Does it have a B value? Sounds a bit weird

Just using it as a B value placeholder so the compiler doesn't complain.
Implementation is fixed in the next PR.

---

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

Previously, spapinistarkware (Shahar Papini) wrote…

Is this different than the Layer enum? Can they ever diverge?

Updated

---

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

Previously, spapinistarkware (Shahar Papini) wrote…

Add a doc about soundness assumptions.
For example, the input layer have been committed to the channel.

Added. WDYT?

---

crates/prover/src/core/lookups/gkr_verifier.rs line 170 at r12 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

It's the third time we have this enum. Do they need to be separated?

Only two now. Layer is for the prover, Gate is is for the verifier

---

crates/prover/src/core/lookups/gkr_verifier.rs line 188 at r12 (raw file):

Previously, spapinistarkware (Shahar Papini) wrote…

I mean, perhaps encapsulate this type inside GkrError

Updated.

---

crates/prover/src/core/lookups/utils.rs line 173 at r12 (raw file):

Previously, shaharsamocha7 wrote…

you have that one:

stwo/crates/prover/src/core/utils.rs

Line 92 in 9259c07

pub fn shifted_secure_combination(

It's a bit more than a random linear combination as it involves alpha and z. Also doesn't use SecureField

[spapinistarkware]

Reviewed 2 of 3 files at r13, all commit messages.
Reviewable status: 10 of 11 files reviewed, all discussions resolved (waiting on @andrewmilson)

[spapinistarkware]

Reviewed 1 of 3 files at r13.
Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @andrewmilson)

[spapinistarkware]

Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @andrewmilson)