Try   HackMD

A simple multivariate AIR argument inspired by SuperSpartan

We will consider the following basic version of AIR. Let

F be a finite field and let
FF[X0,,X2C1]
be a constraint polynomial. An AIR witness for this instance is a table of
C
columns
z0,,zC1
of size
n=2v
such that for all
i=0,,n2
,
F(z0[i],,zC1[i],z0[i+1],,zC1[i+1])=0.

Multi-columns CCS (MCCCS)

CCS is a constraint system introduced in [STW23][1] that generalizes common constraint systems such as R1CS, AIR, and Plonk. A CCS structure is given by

  • Matrices
    M0,,Mt1Fm×n
    .
  • Multisets
    S0,,Sq1
    with elements in
    {0,,t1}
    .
  • Constants
    c0,,cq1F
    .

A witness is a vector

zFn such that[2]
i=0q1cijSiMjz=0.

We introduce a generalization, MCCCS, of CCS where the witness is structured as a table of

C columns. The additional information required is

  • A function
    c:{0,,t1}{0,,C1}
    assigning a column to each matrix.

A witness is then a table of

C columns
z0,,zC1Fn
such that
i=0q1cijSiMjzc(j)=0.

It is easy to see that MCCCS is equivalent to CCS by flattening/unflattening the columns.

Proving system for MCCCS

The SuperSpartan proving system can easily be modified to accommodate MCCCS. The only difference is that the prover commits to all MLE

Z~j(X) of the columns and then equation (14) in [STW23] becomes
0=a{0,1}logmeq~(τ,a)i=0q1cijSi(y{0,1}lognM~j(a,y)Z~c(j)(y)),

which can be proved with multiple calls to the sumcheck protocol.

AIR as a MCCCS

The AIR arithmetization is shown to be a special case of CCS in [STW23]. We show here that AIR can also be seen as a MCCCS with a very simple transformation.

Consider the AIR constraint polynomial

FF[X0,,X2C1], let
S0,,Sq1
be multisets with values in
{0,,2C1}
representing the monomials of
F
, and let
c0,,cq1
be the coefficients of these monomials, i.e.,
F(X0,,X2C1)=i=0q1cijSiXj.

Let

In1 be the identity matrix of size
n1
, let
A0
be the
n×n
matrix
A0=[In1000]

and let
A1
be the
n×n
matrix
A1=[0In100]

Note that for
A0
and
A1
the last row is only used for padding so that the matrix is square.

Finally, let

t=2C,
Mj=Aj/C
, and
c(j)=j mod C
. Then the MCCCS with these parameters is equivalent to the original AIR.

Example

If

C=2 and
F=X0X12X22X1X3
, the MCCCS constraint will be
A0z0A0z1A0z1A1z02A0z1A1z1=0.

Proving system for AIR

The MLE of the matrices

A0 and
A1
are simple. We have
A0[i,j]=eq(i,j)eq(i,n1)eq(j,n1)

and

A1[i,j]=next(i,j), where
next(i,j)=eq(i+1,j)
is defined in Section 5.1 of [STW23]. Therefore the MLE of
A0
is
A0~(x,y)=eq~(x,y)eq~(x,n1)eq~(y,n1)

which can be evaluated in time
O(v=logn)
, and the MLE of
A1
is
A1~(x,y)=next~(x,y)

which can also be evaluated in time
O(v)
, as shown in Theorem 2 of [SWT23]. See also below for a description of
next~
.

Therefore, oracle access to

A0~ and
A1~
is not required by the verifier.

Cyclic constraints

Some versions of AIR use cyclic constraints, i.e., the constraint polynomial also vanishes at

i=n1:
F(z0[n1],,zC1[n1],z0[0],,zC1[0])=0.

The MCCCS for AIR can be adapted to support this by using the matrices
A0=In=[In1001]

and
A1=[0In110].

The MLE of these matrices can also be computed in time

O(v) using the following identites
A0~(x,y)=eq~(x,y)

and
A1~(x,y)=next~(x,y)+eq~(x,n1)eq~(y,0).

Handling public inputs

AIR is often used to arithmetize an execution trace. For example, zkVMs often have the structure of an AIR where the first row contains the input of the program and the last row contains the output. Each other row represents a cycle in the zkVM.

For this reason, we might want (parts of) the first and last rows to be public inputs in the proving system. This can be achieved in the proving system for MCCCS as follows.

Say we want the first element of column

zi to be public. Instead of committing to the MLE of the full column, the prover commits to the MLE of
zi=(0 zi[1..])
, the same column with the first element set to 0. Then, the verifier can compute the value
Z~i(ry)
using the relation
Z~i(ry)=Z~i(ry)+zi[0]χ0(ry),

where
χ0
is the 0-th Lagrange basis multilinear polynomial, which can be evaluated in
O(v)
.

A similar modification can be used to make the last row public.

When the constraint is an arithmetic circuit

In applications, the constraint polynomial

F(X0,,X2C1) is rarely given in sum-of-monomials form. Most of the time, it is given as an arithmetic circuit. The circuit representation can be much more efficient than the sum-of-monomials representation. For example,
F(X0,,X2C1)=(X0++X2C1)2

takes
2C1
additions and
1
multiplication to evaluate as an arithmetic circuit, but is a sum of
2C2+C
monomials. So the (MC)CCS representation can be very inefficient, especially when the number of columns in the AIR is large.

However, it is easy to generalize (MC)CCS to work with arithmetic circuits. Let

C be an arithmetic circuit[3] with
t
inputs
x0,,xt1
and
1
output
C(x0,,xt1)
. Then, we can modify the CCS constraint equation to be
C(M0z,,Mt1z)=0,

where the circuit is evaluated on the
t
vectors entrywise.

As in the SuperSpartan proving system for CCS, it is easy to see that (except with negligible probability) this constraint is equivalent to

0=a{0,1}logmeq~(τ,a)C(u0,,ut1), with ui=y{0,1}lognMi~(a,y)Z~(y),
where
τFlogm
is a random vector. This can be proved using an instantiation of the sumcheck protocol for the inner sum, as well as
t
instantiations of the sumcheck protocol for the values
ui
.

next~
and higher order shifts

The function

next~(x,y) is described in section 5.1 of [STW23]. It is based on the following algorithm to check that
y=x+1
using little-endian bit decomposition.

Let

xk=0 be the first
0
bit of
x
, so that the little-endian bit decomposition of
x
is
x=110xk+1xv1.
Then
y=x+1
if and only if
yi=0
for
i<k
,
yk=1
, and
xi=yi
for all
i>k
, i.e.,
y=001xk+1xv1.

We can check this with the multilinear polynomial
gk(x,y)=(i=0k1xi(1yi))(1xk)yk eq~(xk+1,yk+1)eq~(xv1,yv1).

The big product checks that the first bits of
x
are
1
and those of
y
are
0
, the term
(1xk)yk
checks that
xk=0
and
yk=1
, and the
eq~
terms check that the remaining bits are equal.

Then we simply have

next~(x,y)=k=0v1gk(x,y).
Note that if
x=2v1
has all
1
bits, then
next~(x,y)=0
for all
y
since the
1xk
term is
0
for all
k
. Finally, note that
g0(x,y)
can be computed in time
O(v)
and that
gk+1(x,y)
can be computed in time
O(1)
given
gk(x,y)
using
gk+1(x,y)=gk(x,y)xk(1yk)(1xk+1)yk+1xk1(1yk1)(1xk)yk eq~(xk+1,yk+1).

Therefore,
next~(x,y)
can be computed in time
O(v)
.

It can sometimes be useful to consider higher order shifts, that is constraints of the form

F(z0[i],,zC1[i],z0[i+s],,zC1[i+s])=0,
where
s>1
. The above argument can be adapted for this case by using the modified function
nexts(i,j)=eq(i+s,j)
. We will only consider the case where
s=2e
, but the general case can also be done (I think).

To check

y=x+2e, we observe that it is equivalent to checking that the first
e
bits of
x
and
y
are equal and that the remaining bits satisfy the
next
relation. That is,
next~s(x,y)=eq~(x0,y0)eq~(xe1,ye1) next~(xe,,xv1,ye,,yv1),

which can also be computed in time
O(v)
.


  1. Customizable constraint systems for succinct arguments, Srinath Setty and Justin Thaler and Riad Wahby, eprint.iacr.org/2023/552. ↩︎

  2. Disregarding public inputs for now. ↩︎

  3. Here we consider usual arithmetic circuits over the field

    F with binary addition and multiplication gates, as well as unary gates for multiplication by a constant:
    {gc}cF
    with
    gc(x)=cx
    . ↩︎