Skip to content

The Rest

The univariate skip's positive rounds

As of the end of the univariate skip, the parties have obtained an updated sum claim S0≔g(s′)S_0 \coloneqq g(s'). Moreover, the prover has locally specialized his rectangular multilinears t^0,…,t^n−1\widehat{t}_0, \ldots , \widehat{t}_{n - 1}. That is, for each t^i\widehat{t}_i, using the verifier's univariate challenge s′s', the prover has specialised t^i(Y,X0,…,Xℓ−k−1)\widehat{t}_i(Y, X_0, \ldots , X_{\ell - k - 1}) to t^i(s′,X0,…,Xℓ−k−1)\widehat{t}_i(s', X_0, \ldots , X_{\ell - k - 1}). This latter polynomial—in fact, it's a multilinear!—requires just 2ℓ−k2^{\ell - k} values to represent, as opposed to the 2ℓ2^\ell we started with.

Moreover, the claim we're interested in checking is simply that:

S0=?∑v∈BℓC^(s′,v0,…,vℓ−k−1)⋅δD(s′,s)⋅eq~(v,r).\begin{equation*}S_0 \stackrel{?}= \sum_{v \in \mathcal{B}_\ell} \widehat{C}(s', v_0, \ldots , v_{\ell - k - 1}) \cdot \delta_D(s', s) \cdot \widetilde{\texttt{eq}}(v, r).\end{equation*}

This is mechanically identical to a normal, rectangular sumcheck claim, pertaining now to the ℓ−k\ell - k-variate multilinears t^i(s′,X0,…,Xℓ−k−1)\widehat{t}_i(s', X_0, \ldots , X_{\ell - k - 1}) and the usual composition polynomial c(Z0,…,Zn−1)c(Z_0, \ldots , Z_{n - 1}). The prover and verifier may thus process it accordingly, by running the sumcheck protocol for ℓ−k\ell - k rounds.

The End

By proceeding in this way for ℓ−k\ell - k rounds, the prover and verifier may reduce their initial claim to an evaluation claim of the form Sℓ−k=?C^(s′,r0′,…,rℓ−k−1′)⋅δD(s′,s)⋅eq~(r′,r)S_{\ell - k} \stackrel{?}= \widehat{C}(s', r'_0, \ldots , r'_{\ell - k - 1}) \cdot \delta_D(s', s) \cdot \widetilde{\texttt{eq}}(r', r), for some point r′∈Tτℓ−kr' \in \mathcal{T}_\tau^{\ell - k} sampled during the course of the standard sumcheck. Of course, the verifier may locally evaluate δD(s′,s)⋅eq~(r′,r)\delta_D(s', s) \cdot \widetilde{\texttt{eq}}(r', r) himself. It thus remains for the verifier to learn C^(s′,r0′,…,rℓ−k−1′)\widehat{C}(s', r'_0, \ldots , r'_{\ell - k - 1}); to do this, it suffices in turn for the verifier to learn the individual evaluations t^i(s′,r0′,…,rℓ−k−1′)\widehat{t}_i(s', r'_0, \ldots , r'_{\ell - k - 1}) for each input index i∈{0,…,n−1}i \in \{0, \ldots , n - 1\}—indeed, assuming reliable access to these evaluations, the verifier can just apply the composition polynomial c(Z0,…,Zn−1)c(Z_0, \ldots , Z_{n - 1}) upon them to learn the desired thing C^(s′,r0′,…,rℓ−k−1′)\widehat{C}(s', r'_0, \ldots , r'_{\ell - k - 1}).

Where this gets tricky is that our evaluation claims on the initial input polynomials are rectangular, not standard. That is, if we instead needed to evaluate the standard cube-shaped multilinears ti(X0,…,Xℓ−1)t_i(X_0, \ldots , X_{\ell - 1}) at some point, we would be fine—we would just feed the relevant claims directly into our PCS. As it stands, we rather need to evaluate the rectangularized small-field multilinears t^i(Y,X0,…,Xℓ−k−1)\widehat{t}_i(Y, X_0, \ldots , X_{\ell - k - 1}), namely at the point (s′,r0′,…,rℓ−k−1′)(s', r'_0, \ldots , r'_{\ell - k - 1}).

There are a couple ways to proceed from this point. Here, we sketch one, which is currently implemented in Binius. The idea is to express the desired, rectangularized evaluations t^i(s′,r0′,…,rℓ−k−1′)\hat{t}_i(s', r'_0, \ldots , r'_{\ell - k - 1}) in terms of statements about the underlying, standard multilinears tit_i:

t^i(s′,r0′,…,rℓ−k−1′)=∑u∈BkδD({u},s′)⋅ti(u0,…,uk−1,r0′,…,rℓ−k−1′).\begin{equation*}\hat{t}_i(s', r'_0, \ldots , r'_{\ell - k - 1}) = \sum_{u \in \mathcal{B}_k} \delta_D(\{u\}, s') \cdot t_i(u_0, \ldots , u_{k - 1}, r'_0, \ldots , r'_{\ell - k - 1}).\end{equation*}

Indeed, this identity holds essentially by definition of the rectangularizations t^i\hat{t}_i.

The next step is to observe that the above thing can be sumchecked! That is, the parties may run a kk-round sumcheck on the kk-variate product of multilinears

(X0,…,Xk−1)↦δD,s′(X0,…,Xk−1)⋅ti(X0,…,Xk−1,r0′,…,rℓ−k−1′);\begin{equation*}(X_0, \ldots , X_{k - 1}) \mapsto \delta_{D, s'}(X_0, \ldots , X_{k - 1}) \cdot t_i(X_0, \ldots , X_{k - 1}, r'_0, \ldots , r'_{\ell - k - 1});\end{equation*}

here, δD,s′(X0,…,Xk−1)\delta_{D, s'}(X_0, \ldots , X_{k - 1}) is the multilinear which, for each cube point u∈Bku \in \mathcal{B}_k, sends u↦δD({u},s′)u \mapsto \delta_D(\{u\}, s'). (This is a perfectly good multilinear; we have specified it by giving its table of values on the cube.)

Indeed, by running the above sumcheck, the verifier may reduce the desired evaluation claim to two further claims—namely of the form δD,s′(r0′′,…,rk−1′′)\delta_{D, s'}(r''_0, \ldots , r''_{k - 1}) and ti(r0′′,…,rk−1′′,r0′,…,rℓ−k−1′)t_i(r''_0, \ldots , r''_{k - 1}, r'_0, \ldots , r'_{\ell - k - 1}), for some point r′′∈Tτkr'' \in \mathcal{T}_\tau^k sampled during this sumcheck. By biting the bullet and expending Θ(2k)\Theta(2^k) work, the verifier may evaluate δD(r′′,s′)\delta_D(r'', s') itself locally; at this point, it remains just to learn ti(r0′′,…,rk−1′′,r0′,…,rℓ−k−1′)t_i(r''_0, \ldots , r''_{k - 1}, r'_0, \ldots , r'_{\ell - k - 1}). This is just a standard cube-shaped evaluation claim on a committed multilinear, so at this point we're done.