Groth16 Batch Verification

\gdef\delim#1#2#3{\mathopen{}\mathclose{\left#1 #2 \right#3}} \gdef\p#1{\delim({#1})} \gdef\set#1{\delim\{{#1}\}} \gdef\e{\operatorname{e}} \gdef\g{\mathrm{g}} \gdef\Z{\mathrm{Z}} \gdef\U{\mathrm{U}} \gdef\V{\mathrm{V}} \gdef\W{\mathrm{W}} \gdef\k#1{\mathbf{#1}} \gdef\F{\mathbb{F}} \gdef\G{\mathbb{G}} \gdef\ga#1{\delim[{#1}]_1} \gdef\gb#1{\delim[{#1}]_2}

Introduction

Constraints

Recall Groth16. For a given circuit with n variables, m constraints and p public inputs we encode the circuit as 3⋅n+1 polynomials \U_i, \V_i, \W_i, \Z ∈ \F[X] each with m terms (i.e. degree m-1). A witness x ∈\F^n is correct if for some H(X) ∈ \F[X] it satisfies

\p{\sum_{i∈[0,n)} x_i ⋅ \U_i(X)} ⋅ \p{\sum_{i∈[0,n)} x_i ⋅ \V_i(X)} = \p{\sum_{i∈[0,n)} x_i ⋅ \W_i(X)} + H(X) ⋅\Z(X)

For a given circuit and setup we have \ga{α}, \gb{β}, L_i, \gb{γ}, \ga{δ}.

Consider a proof (x_i, A, B, C). To verify it we check

0 = \e\p{A, B} - \e\p{\ga{α}, \gb{β}} - \e\p{\sum_{i∈[0,p)}x_i⋅L_i, \gb{γ}} - \e\p{C, \gb{δ}}

Linear combinations

Consider many proofs (x_{ij}, A_j, B_j, C_j). Take a random linear product of verifications with r_j ∈ \F.

\begin{aligned} 0 &= \sum_j r_j⋅ \p{\e\p{A_j, B_j} -\e\p{\ga{α}, \gb{β}} - \e\p{\sum_{i∈[0,p)}x_{ij}⋅L_i, \gb{γ}} - \e\p{C_j, \gb{δ}} }\\ &= \sum_j r_j⋅ \e\p{A_j, B_j} - \e\p{\sum_j r_j⋅\ga{α}, \gb{β}}- \e\p{\sum_{i∈[0,p)}\p{\sum_j x_{ij}⋅r_j}⋅L_i, \gb{γ}} - \e\p{\sum_j r_j⋅C_j, \gb{δ}} \end{aligned}

The problem is \sum_j r_j⋅ \e\p{A_j, B_j} is not computable in \G_1, \G_2 but requires operations in \G_3.

If we simply forced the sum inside we'd get many cross terms:

\begin{aligned} \e\p{\sum_j r_j⋅ A_j, \sum_j r_j⋅ B_j} &= \sum_i \sum_j r_i⋅ r_j⋅ \e\p{A_i, B_j} \end{aligned}

Snarkpack solves this using a target inner pairing product (TIPP) protocol to provide the verifier with \sum_j r_j⋅ \e\p{A_j, B_j} and proof that it was constructed correctly.

Attempt at alternative

What if instead we embrace the cross terms and try to make it work?

\begin{aligned} \e\p{\sum_j r^j⋅ A_j, \sum_j s_j⋅ B_j} &= \sum_i \sum_j r^i⋅ s_j⋅ \e\p{A_i, B_j} \end{aligned}

Poor man's snarkpack

We can also simply not aggregate the \e{A,B} pair:

\begin{aligned} \sum_j \e\p{r^j⋅ A_j, B_j} &= \e\p{\sum_j r^j⋅\ga{α}, \gb{β}} + \e\p{\sum_{i∈[0,p)}\p{\sum_j x_{ij}⋅r^j}⋅L_i, \gb{γ}} + \e\p{\sum_j r^j⋅C_j, \gb{δ}} \end{aligned}

This should trivially work and save 75% of the pairings, at the cost of \F and \G_1 operations.

Poor man's turbo

The aggregator computes

\begin{aligned} C &= \sum_j r^j ⋅ C_j \\ \end{aligned}

The verifier checks

\begin{aligned} \sum_j \e\p{r^j⋅ A_j, B_j} &= \e\p{\p{\sum_j r^j}⋅\ga{α}, \gb{β}} + \e\p{\sum_{i∈[0,p)}\p{\sum_j x_{ij}⋅r^j}⋅L_i, \gb{γ}} + \e\p{C, \gb{δ}} \end{aligned}

This requires 2⋅(n-1) times \mathsf{Add}_{\F}, p⋅n times \mathsf{Mul}_{\F}, n+p+1 times \mathsf{Mul}_{\G_1} and n+3 times \mathsf{Pair}.

This construction preserves completeness and zero-knowledge, but does it preserve soundness?

Note. If this works it could also be applied to SnarkPack.

Attempted Soundness Proof

As before, but now with additional formal parameters r_j.

\begin{aligned} \sum_j r^j⋅ A_j⋅ B_j &= \sum_j r^j⋅α⋅β + \sum_j r^j ⋅\sum_{i∈[0,p)} x_{ij}⋅\p{β⋅\U_i​(τ)+α⋅\V_i​(τ)+\W_i​(τ)} +C⋅δ \end{aligned}

where we have multiple A, B values

\begin{aligned} A_j &= A_{τj}(τ) + A_{αj}(τ)⋅α + A_{βj}(τ)⋅β + A_{δj} ⋅ δ + A_{γj} ⋅ γ + A_{Zj}(τ)⋅{\footnotesize \frac{\Z(τ)}{δ}} \\[0.5em] &\phantom{=}+ \sum_{i∈[0,p)} A_{ij}⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} + \sum_{i∈[p,m)} A_{ij}⋅ {\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} } \\[2em] B_j &= B_{τj}(τ) + B_{βj}⋅β + B_{δj} ⋅ δ + B_{γj} ⋅ γ \\[0.2em] \end{aligned}

The aggregator constructs a C while having knowledge of the r_j:

\begin{aligned} C &= C_τ(r, τ) + C_α(r, τ)⋅α + C_β(r,τ)⋅β + C_δ(r) ⋅ δ + C_γ(r) ⋅ γ + C_Z(r,τ)⋅{\footnotesize \frac{\Z(τ)}{δ}} \\[0.5em] &\phantom{=}+ \sum_{i∈[0,p)} C_i(r)⋅{\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{γ}} + \sum_{i∈[p,m)} C_i(r)⋅ {\footnotesize \frac{β ⋅ \U_i(τ) + α ⋅ \V_i(τ) + \W_i(τ)}{δ} } \end{aligned}

Where each function f(r, τ) can is of the form f_0(r) + f_1(r)⋅τ + f_2(r)⋅τ^2+⋯.

The steps where the RHS is constant factor on r and are much the same as before:

\begin{aligned} A_{αj}(τ) ⋅ B_{βj} &= 1 &\hspace{2em}&\p{α⋅β⋅τ^i⋅r^j} \\ A_{βj}(τ) ⋅ B_{βj} &= 0 &\hspace{2em}&\p{β^2⋅τ^i⋅r^j} \\ A_{αj}(τ) ⋅ B_{γj} &= 0 &\hspace{2em}&\p{α⋅γ⋅τ^i⋅r^j} \\ &\hspace{0.7em}⋮ \end{aligned}

So we again get

\begin{aligned} A_j &= A_{τj}(τ) + A_{αj}⋅α + A_{δj} ⋅ δ \\ B_j &= B_{τj}(τ) + A_{αj}^{-1} ⋅ β + B_{δj} ⋅ δ \end{aligned}

Looking at monomials

\begin{aligned} \sum_j r^j ⋅ A_{αj} ⋅ B_{τj}(τ) &= \sum_j \sum_{i∈[0,p)} r^j⋅x_{ij} ⋅ \V_i(τ) + \sum_{i∈[p,m)} C_i(r) ⋅ \V_i(τ) &\hspace{2em}&\p{α⋅τ^i⋅r^j} \\ \sum_j r^j ⋅ A_{αj}^{-1} ⋅ A_{τj}(τ) &= \sum_j \sum_{i∈[0,p)} r^j⋅x_{ij} ⋅ \U_i(τ) + \sum_{i∈[p,m)} C_i(r) ⋅ \U_i(τ) &\hspace{2em}&\p{β⋅τ^i⋅r^j} \end{aligned}

Defining

\hat x_i =\begin{cases} \sum_j r^j ⋅ x_{ij} & i∈[0,p) \\ C_i(r) & i∈[p,m) \end{cases}

we can rewrite these as

\begin{aligned} \sum_j r^j ⋅ A_{αj} ⋅ B_{τj}(τ) &= \sum_{i∈[0,m)} \hat x_i ⋅ \V_i(τ) \\ \sum_j r^j ⋅ A_{αj}^{-1} ⋅ A_{τj}(τ) &= \sum_{i∈[0,m)} \hat x_i ⋅ \U_i(τ) \end{aligned}

Finally looking at the monomials in τ^i⋅r^j:

$$ \begin{aligned} \sum_j r^j ⋅ A_{τj}(τ) ⋅ B_{τj}(τ) &= \sum_j r^j ⋅\sum_{i∈[0,p)} x_{ij}⋅\W_i​(τ)

• \sum_{i∈[p,m)} C_i(r)⋅\W_i(τ)
• C_Z(r,τ)⋅\Z(τ) \end{aligned} $$

Simplifiying using \hat x

$$ \begin{aligned} \sum_j r^j ⋅ A_{τj}(τ) ⋅ B_{τj}(τ) &= \sum_{i∈[0,p)} \hat x_i⋅\W_i​(τ)

• C_Z(r,τ)⋅\Z(τ) \end{aligned} $$

Looking at the left hand side:

\begin{aligned} \sum_j r^j ⋅ A_{τj}(τ) ⋅ B_{τj}(τ) &= \end{aligned}

Assume for the moment \U_i, \V_i, \W_i are all linearly independent Then

\begin{aligned} \sum_j r^j ⋅ A_{αj} ⋅ B_{τj}(τ) &= \sum_j \sum_{i∈[0,p)} r^j⋅x_{ij} ⋅ \V_i(τ) + \sum_{i∈[p,m)} C_i(r) ⋅ \V_i(τ) &\hspace{2em}&\p{α⋅τ^i⋅r^j} \\ \sum_j r^j ⋅ A_{αj}^{-1} ⋅ A_{τj}(τ) &= \sum_j \sum_{i∈[0,p)} r^j⋅x_{ij} ⋅ \U_i(τ) + \sum_{i∈[p,m)} C_i(r) ⋅ \U_i(τ) &\hspace{2em}&\p{β⋅τ^i⋅r^j} \end{aligned}

We are looking for

\sum_{j∈[0,k)} r^j⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \U_i(X)} ⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \V_i(X)} = \sum_{\substack{i∈[0,n)\\j∈[0,k)}} r^j ⋅ x_{ij} ⋅ \W_i(X) + \sum_j r^j ⋅ H_j(X) ⋅\Z(X)

Question. Can we define H(X) = \sum_j r^j ⋅ H(X) and forgo breaking it down?

\sum_{j∈[0,k)} r^j⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \U_i(X)} ⋅ \p{\sum_{i∈[0,n)} x_{ij} ⋅ \V_i(X)} = \sum_{\substack{i∈[0,n)\\j∈[0,k)}} r^j ⋅ x_{ij} ⋅ \W_i(X) + H(X) ⋅\Z(X)