We will consider the following basic version of AIR. Let be a finite field and let be a constraint polynomial. An AIR witness for this instance is a table of columns of size such that for all ,
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
A witness is a vector such that[2]
We introduce a generalization, MCCCS, of CCS where the witness is structured as a table of columns. The additional information required is
A witness is then a table of columns such that
It is easy to see that MCCCS is equivalent to CCS by flattening/unflattening the columns.
The SuperSpartan proving system can easily be modified to accommodate MCCCS. The only difference is that the prover commits to all MLE of the columns and then equation (14) in [STW23] becomes
which can be proved with multiple calls to the sumcheck protocol.
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 , let be multisets with values in representing the monomials of , and let be the coefficients of these monomials, i.e.,
Let be the identity matrix of size , let be the
matrix
and let be the matrix
Note that for and the last row is only used for padding so that the matrix is square.
Finally, let , , and . Then the MCCCS with these parameters is equivalent to the original AIR.
If and , the MCCCS constraint will be
The MLE of the matrices and are simple. We have
and
where is defined in Section 5.1 of [STW23]. Therefore the MLE of is
which can be evaluated in time , and the MLE of is
which can also be evaluated in time , as shown in Theorem 2 of [SWT23]. See also below for a description of .
Therefore, oracle access to and is not required by the verifier.
Some versions of AIR use cyclic constraints, i.e., the constraint polynomial also vanishes at :
The MCCCS for AIR can be adapted to support this by using the matrices
and
The MLE of these matrices can also be computed in time using the following identites
and
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 to be public. Instead of committing to the MLE of the full column, the prover commits to the MLE of , the same column with the first element set to 0. Then, the verifier can compute the value using the relation
where is the 0-th Lagrange basis multilinear polynomial, which can be evaluated in .
A similar modification can be used to make the last row public.
In applications, the constraint polynomial 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,
takes additions and multiplication to evaluate as an arithmetic circuit, but is a sum of 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 be an arithmetic circuit[3] with inputs and output . Then, we can modify the CCS constraint equation to be
where the circuit is evaluated on the 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
where is a random vector. This can be proved using an instantiation of the sumcheck protocol for the inner sum, as well as instantiations of the sumcheck protocol for the values .
The function is described in section 5.1 of [STW23]. It is based on the following algorithm to check that using little-endian bit decomposition.
Let be the first bit of , so that the little-endian bit decomposition of is Then if and only if for , , and for all , i.e.,
We can check this with the multilinear polynomial
The big product checks that the first bits of are and those of are , the term checks that and , and the terms check that the remaining bits are equal.
Then we simply have
Note that if has all bits, then for all since the term is for all . Finally, note that can be computed in time and that can be computed in time given using
Therefore, can be computed in time .
It can sometimes be useful to consider higher order shifts, that is constraints of the form
where . The above argument can be adapted for this case by using the modified function . We will only consider the case where , but the general case can also be done (I think).
To check , we observe that it is equivalent to checking that the first bits of and are equal and that the remaining bits satisfy the relation. That is,
which can also be computed in time .
Customizable constraint systems for succinct arguments, Srinath Setty and Justin Thaler and Riad Wahby, eprint.iacr.org/2023/552. ↩︎
Disregarding public inputs for now. ↩︎
Here we consider usual arithmetic circuits over the field with binary addition and multiplication gates, as well as unary gates for multiplication by a constant: with . ↩︎