Discussion on the sumcheck protocol

[marvin.jones]

Sumcheck can be applied in the instance that you’re referring. Though, you’ll need c to be selected by the verifier (or with Fiat-Shamir based on w, a, b).

I’m not sure why this would require 4 instances of sumcheck. A single instance of sumcheck could be applied to the polynomial \tilde{beta}_x(r)\cdot (\tilde{w}(x) - (\tilde{a}(x) - \tilde{b}(x)))\cdot \tilde{c}(x).

KZG would be separate from an instance of GKR. GKR answers a question concerning field elements with the language of field elements (and related polynomials). KZG as a polynomial commitment translates a question concerning polynomials to elliptic curves (pairings specifically). The question proposed would be more ‘simply’ answered that way though.

If there’s a specific objective you have in mind that requires sumcheck or GKR, I might be able to provide additional insight.

[zkLisa]

@marvin.jones

Sumcheck can be applied in the instance that you’re referring. Though, you’ll need c to be selected by the verifier (or with Fiat-Shamir based on w, a, b).

You mean selected as in, it should be public?

@marvin.jones

I’m not sure why this would require 4 instances of sumcheck. A single instance of sumcheck could be applied to the polynomial \tilde{beta}_x(r)\cdot (\tilde{w}(x) - (\tilde{a}(x) - \tilde{b}(x)))\cdot \tilde{c}(x).

If you’re going from the field domain to the Boolean domain, then you would need to prove some consistency for each vector, right?

@marvin.jones

If there’s a specific objective you have in mind that requires sumcheck or GKR, I might be able to provide additional insight.

How do proof systems based on GKR and sumcheck usually handle inequalities or range constraints on values? Are there some common tricks?

For example, to enforce:
a \leq z \leq b, this could be encoded as: z - a \geq 0 and b - z \geq 0.
The first step would be to prove the subtraction, and then ensure that the MSB of the difference is 0 (the last step could be easily done ig). Initialising GKR seems to be an overkill for a few values.

Ad far as I see, one could do this with R1CS, but there’s probably ways to avoid that.

[marvin.jones]

Blockquote[quote=“zkLisa, post:22, topic:401, full:true”]
You mean selected as in, it should be public? [/quote]

Usually, sumcheck assumes the original polynomial is public. Though, it is not actually necessary for w, a and b to be known. If z(x) = w(x) - (a(x) - b(x)) is public then Fiat-Shamir heuristic could be applied on this.

Blockquote[quote=“zkLisa, post:22, topic:401, full:true”]
If you’re going from the field domain to the Boolean domain, then you would need to prove some consistency for each vector, right? [/quote]

I think the only use Boolean domain is used is for entry specification. A bit of context for how I’m thinking about this in case it differs from your thoughts:

• We have some vector z = w- (a-b) with n entries.
• Each entry of z can be specified as a binary string of length \log(n).
• This gives an implicit polynomial over Binary domain \{0,1\}^{\log(n)} with outputs to a field \mathbb{F}.
• Sumcheck is applied to the multilinear extension \tilde{z}: \mathbb{F}^{\log{n}} \rightarrow \mathbb{F}.
  For this, no consistency is necessary as \{0,1\} is a subset of \mathbb{F} and our polynomial \tilde{z} matches with z on the points that sumcheck cares about.

Blockquote[quote=“zkLisa, post:22, topic:401, full:true”]
How do proof systems based on GKR and sumcheck usually handle inequalities or range constraints on values? Are there some common tricks? [/quote]

The way you want to think about this question isn’t “how does GKR (or any proof system) handle this” but rather “how would an arithmetic circuit represent this”.

To represent inequalities or range constraints on a value, we can use three equalities from Bulletproofs (page 17). - Bulletproofs shows how to construct a specialize proof system using inner product argument. We only need equation 37 for an arithmetic circuit:

• {\bf{a}_R} = {\bf{a}_L} - {\bf{1}}^n; each entry is of the form {\bf{a}_R}[i] = {\bf{a}_L}[i]-1.
• {\bf{a}_L} \circ {\bf{a}_R} = {\bf{0}}^n (hadamard product) shows {\bf{a}_L}[i] \cdot {\bf{a}_R}[i] = 0 for every n.
  These two constraints force {\bf{a}}_L to have entries in \{0,1\}.
• \langle {\bf{a_L}}, {\bf{2}}^n\rangle = {\bf{a}_L}[0] + {\bf{a}}_L[1]\cdot 2 + \cdots+{\bf{a}_L}[n-1]2^{n-1} = v; shows {\bf{a}}_L is a 2-adic representation of v.

Since v can be expressed this way, then we know 0 \leq v \leq 2^n. These three constraints can be used to form a R1CS circuit. Thus, GKR can be applied.

Cuproofs takes this style construction and applies it to v \in [a,b].

[zkLisa]

@marvin.jones

Usually, sumcheck assumes the original polynomial is public. Though, it is not actually necessary for w, a and b to be known. If z(x) = w(x) - (a(x) - b(x)) is public then Fiat-Shamir heuristic could be applied on this.

Ah, I see! My thought process was something like this:
Private inputs: w,a,b
Public inputs: c (and it is known to be 1^n, otherwise the sumcheck will fail even when w,a,b are “correct”)

@marvin.jones

I think the only use Boolean domain is used is for entry specification. A bit of context for how I’m thinking about this in case it differs from your thoughts:

I was looking at proving that (a-b) equals to w. And considering the example you gave to show that the sumcheck equation I initially proposed won’t work:

Consider the vectors: w= (3,2), a = (5,7) and b = (3,4). Of course, w \neq a-b = (2,3).

I thought of taking e.g w= (3,2) decomposing it to w_{bit}= (011, 010) proving that you decomposed it right, and then applying:

@zkLisa

\begin{align} 0 &= \sum_{x \in \{0,1\}^{\log n}} \widetilde{\beta}_x(r) \cdot \Big(( \widetilde{w}(x) - (\widetilde{a}(x) - \widetilde{b}(x))) \cdot \widetilde{c}(x)\Big) , \end{align}

So, the output of e.g., \widetilde{a}(x) is just 0/1 basically and not any field member. This would technically prove that \exists a and \exists b s.t a-b = w. And also these “constrains” still hold:

1. Private inputs: w,a,b
2. Public inputs: c (and it is known to be 1^n, otherwise the sumcheck will fail even when w,a,b are “correct”)

But ofc applying your exact example in this equation won’t work bc w \neq a-b = (2,3).

@marvin.jones

we can use three equalities from Bulletproofs (page 17).

Thank you! I’ll look into that.

@marvin.jones

These three constraints can be used to form a R1CS circuit.

I thought we should always try to minimize the size of the R1CS representation. e.g., by using bit-decomposition but they blow up the circuit size, so sometimes being able to express and prove computation via a sumcheck instance is nice. I saw it in the zkPoT paper I mentioned a while ago.

@marvin.jones

Cuproofs takes this style construction and applies it to v \in [a,b].

Thank you again! I’ll see what they’re up to.

[marvin.jones]

@zkLisa

@marvin.jones

Usually, sumcheck assumes the original polynomial is public. Though, it is not actually necessary for w, a and b to be known. If z(x) = w(x) - (a(x) - b(x)) is public then Fiat-Shamir heuristic could be applied on this.

Ah, I see! My thought process was something like this:
Private inputs: w,a,b
Public inputs: c (and it is known to be 1^n, otherwise the sumcheck will fail even when w,a,b are “correct”)

Sumcheck in this application would retain correctness. But this application would lack soundness. As my counterexample demonstrated.

@zkLisa

@marvin.jones

I think the only use Boolean domain is used is for entry specification. A bit of context for how I’m thinking about this in case it differs from your thoughts:

I was looking at proving that (a-b) equals to w. And considering the example you gave to show that the sumcheck equation I initially proposed won’t work:

Consider the vectors: w= (3,2), a = (5,7) and b = (3,4). Of course, w \neq a-b = (2,3).

I thought of taking e.g w= (3,2) decomposing it to w_{bit}= (011, 010) proving that you decomposed it right, and then applying:

@zkLisa

\begin{align} 0 &= \sum_{x \in \{0,1\}^{\log n}} \widetilde{\beta}_x(r) \cdot \Big(( \widetilde{w}(x) - (\widetilde{a}(x) - \widetilde{b}(x))) \cdot \widetilde{c}(x)\Big) , \end{align}

So, the output of e.g., \widetilde{a}(x) is just 0/1 basically and not any field member. This would technically prove that \exists a and \exists b s.t a-b = w. And also these “constrains” still hold:

1. Private inputs: w,a,b
2. Public inputs: c (and it is known to be 1^n, otherwise the sumcheck will fail even when w,a,b are “correct”)

But ofc applying your exact example in this equation won’t work bc w \neq a-b = (2,3).

Usually, \tilde{a} denotes a polynomial extension of vector a. To assume that vector a is binary, you’d need the first two constraints from Bulletproofs (a \circ b = 0 and b = a - 1). However, a polynomial extension of a would not be restricted to just 0/1.

@zkLisa

@marvin.jones

These three constraints can be used to form a R1CS circuit.

I thought we should always try to minimize the size of the R1CS representation. e.g., by using bit-decomposition but they blow up the circuit size, so sometimes being able to express and prove computation via a sumcheck instance is nice. I saw it in the zkPoT paper I mentioned a while ago.

GKR is used for proving circuit satisfiability which usually is R1CS (for GKR). It is good to minimize circuit size but depending on the problem this can be restrictive. For certain applications, it can be best to design an application specific argument. E.g., Bulletproofs’ paper develops a range proof specific protocol before later using similar techniques for R1CS. Most (modern) proof systems are designed to be universal which requires the flexibility to accept a general arithmetic circuit.

[zkLisa]

So, as far as I can see, in range proofs you are kinda restricted to using an arithmetic circuit anyway.

Why not use this approach instead:
To check if a private x is in the public range [a,b]:

1. Define l as l = x-a
2. Define u as u = b-x
3. Prove that x-a equals l with GKR (two input and one subtraction gate, gate of a is probably like a public constant gate). Basically run a GKR on l= x - a.
4. Prove that b-x equals u with GKR (two input and one subtraction gate, gate of b is probably like a public constant gate)). Basically run a GKR on u = b - x.
5. Provide bit-decompositions and sign bits of l and u and prove them with sumcheck using the method you gave an overview of:

@marvin.jones

Roughly, speaking. There’s a vector z. Each component of z has a binary representation in the matrix Z and bit sign z_{sgn} that are claimed to be binary. To prove that they are binary.

• A challenge \alpha is applied to ensure that the z_{sgn}(1-z_{sgn}) and Z(1-Z) terms do not cleverly cancel out.
• r_y and r_x are used in \beta function (defined in the definition of MLE in the paper).
  Equation 3 demonstrates that Z and z_{sgn} are binary.
  Equation 4 is used to show that Z and z_{sgn} correlate to the vector z in the claimed manner. This is the very rough idea.

6. Check if the sign bit of the l and u is 0 by running something like this:
   0 = \sum_{x \in \{0,1\}^{\log n}} \widetilde{\beta}_x(r) \cdot \widetilde{l}_{\mathrm{Sign}}(x).

Wouldn’t this suffice to show that a \geq x \geq b by a restructure x-a\geq 0 and b-x \geq 0 ? The original GKR is not zero-knowledge but we can consider Virgo++, I guess.

But I feel like I am terribly missing something here since I haven’t seen this method before.

Edit: Idk if this is stupid, but could we avoid running a GKR on l = x-a and just run a sumcheck on l = x + (-a) instead? So, by consider the negation of a.

[marvin.jones]

The gates for 1 and 2 could be compiled into a single circuit. This would enable a single proof to be generated to attest to the correctness of l and u.

This approach seemingly works, but it raises a critical question. If the arithmetic is being done over a finite field, positive/negative is ‘skewed.’ Afterall, -x = p-x in \mathbb{F}_p.

This means that you’ll need some strange bound concerns when shifting to bit-decomposition representation. E.g., for any x in \mathbb{F}_p we can find representations of l and u that would ‘appear positive.’ Thus rendering the real constraint that you want with l and u ineffective; the sign bits lose some context.

If arithmetic is not restricted to a finite field; then you need to have a large bound to ensure overflow does not occur. I think this would result in a check like l, u \in [0, 2^n]. This could be done with an IPA style argument rather than sumcheck…

Cuproof gets around this issue by using theory from Quadratic Forms (Lagrange’s sum of four squares). This provides a clear representation for non-negative integers without restriction to \mathbb{F}_p.

Response to edit:
All of this is complex and there’s not a one right approach. Each method has strange tradeoffs and then there’s just whatever tools you tend to use.
Sumcheck could be applied to the MLE of l - (x + (-a)) (I think this is what you meant). Though, you’ll have to make sure to use challenges generated from Fiat-Shamir to ensure that the Prover cannot exploit a rearrangement of vector entries from l and x+(-a).

[zkLisa]

@marvin.jones

The gates for 1 and 2 could be compiled into a single circuit. This would enable a single proof to be generated to attest to the correctness of l and u.

This approach seemingly works, but it raises a critical question. If the arithmetic is being done over a finite field, positive/negative is ‘skewed.’ Afterall, -x = p-x in \mathbb{F}_p.

This means that you’ll need some strange bound concerns when shifting to bit-decomposition representation. E.g., for any x in \mathbb{F}_p we can find representations of l and u that would ‘appear positive.’ Thus rendering the real constraint that you want with l and u ineffective; the sign bits lose some context.

Yes, all arithmetic is performed over a finite field \mathbb{F}_p. In order for bit-decompositions and sign bits to be well-defined, I guess we make the following assumptions:

1. Any value z that is subject to a bit-decomposition must satisfy 0 \leq z < 2^q with 2^q < p. This prob. ensures that the binary representation of z is unique in \mathbb{F}_p.

2. When a sign bit is used, we assume -2^{q-1} \leq z < 2^{q-1}
   again with 2^q < p, so that each z has a unique signed binary representation. And then this resolves ambiguities such as -x \equiv p - x \pmod{p}.

3. Comparisons of the form z \geq 0 are interpreted with respect to these bounded integer intervals, not modulo p?

So, all of these things are not explicitly written in this paper:

zkPoT

E.g check their Integer arithmetic and comparison and Sumcheck for binary operations subsubsections. So, I guess you they didn’t prove ranges defined in the 3 assumptions I mentioned, but just assumed they hold.

btw I am referring to this paper often, bc I remember more of it since I read it a few times more throughly.

[marvin.jones]

I’m not sure whether I’ve read all of ZKPoT (if so, it’s been awhile). So, there might be a subtle situation that by passes the modulo issue for ranges.

As long as the following conditions hold:

• Distances within your interval are less than 2^q; b-a < 2^q
• 2^q < p/2

Then overflow is avoided. These conditions do not need to be checked by your circuit provided these are public parameters. If a,b are private (and q is public), then additional constraints are needed.

[zkLisa]

@marvin.jones

All of this is complex and there’s not a one right approach. Each method has strange tradeoffs and then there’s just whatever tools you tend to use.

But for simple arguments like l = x - a, Virgo++ (the zk GKR) is too heavy.

Be aware my question might be beyond stupid here:

@marvin.jones

Sumcheck could be applied to the MLE of l - (x + (-a)) (I think this is what you meant). Though, you’ll have to make sure to use challenges generated from Fiat-Shamir to ensure that the Prover cannot exploit a rearrangement of vector entries from l and x+(-a).

I meant a statement like “I know a l s.t when you sum up x and -a, you obtain l”. Let’s denote the negation of a with a_{neg}:

\begin{align} \widetilde{l}(r) &= \sum_{i \in \{0,1\}^{\log n}} \widetilde{\beta}_i(r) \cdot (\widetilde{x}(i) + \tilde{a}_{neg}(i)) \end{align}

But, I guess then one would need to prove that a was negated correctly if planning to keep it private.

But that seems to be equivalent to literally:

\begin{align} \widetilde{l}(r) &= \sum_{i \in \{0,1\}^{\log n}} \widetilde{\beta}_i(r) \cdot (\widetilde{x}(i) - \tilde{a}(i)) \end{align}

So no need for negation at all ig

[marvin.jones]

Agreed, but the main issue is that the sum from the Sumcheck version only handles the entries in the vector. Assuming that \tilde{\beta}_i is evaluation point r is selected by the Verifier (after \tilde{x}, \tilde{a} have been committed to), the Prover should not be able to manipulate the sum in Sumcheck by the “re-arranging” coefficients example provided earlier.

Sumcheck can be used to do this, but you’d need to have a related proof that l was correctly formed. This results in either multiple separate proofs or potentially a ‘bloated’ R1CS circuit.

[zkLisa]

Thank you so much for your insights!!!