Interactive AIR Arithmetization

But first, we quickly remind the reader that the Starknet STARK protocol allows a prover to convince a verifier that an AIR (Algebraic Intermediate Representation) arithmetization is satisfied by their witness. This is generally augmented to also include a public input, usually via a public memory extension.

AIR is essentially two things:

1. an indexed table representing the execution trace of a run, where columns can be seen as registers and the rows the values they take as one steps through a program. The table takes values when a prover tries to prove an execution.
2. a list of fixed constraints that are agreed on.

The indexing of the table is chosen as the elements of the smallest subgroup of power $2$ that can index the table.

Furthermore, the columns of a table can be grouped, which allows the prover to fill the table group by group, using challenges from the verifier in-between. This is useful in order to perform an interactive arithmetization where parts of the encoded circuit need verifier randomness to be computed.

We give the example of two "original" columns and one "interaction" column, indexed using the multiplicative subgroup of the 16-th roots of unity:

The first phase of the Starknet STARK protocol is to iteratively construct the trace tables (what we previously called interactive arithmetization). The prover sends commitments to parts of the table, and receives verifier challenges in between.

• TODO: we should make this part agnostic to Cairo though.

Composition Polynomial

The role of the verifier is now to verify constraints of the form of polynomials on the trace column polynomials, applied on a domain (a list of all the indexes on which the constraint applies).

As with our example above, we can imagine a list of constraints $C_i(x)$ that need to vanish on a list of associated domains described by their domain polynomials $D_i(x)$.

By definition, this can be reduced to checking that you can write each $C_i$ as $C_i(x)=D_i(x)·q(x)$ for some quotient polynomial $q(x)$ of degree $deg(C_i)-deg(D_i)$.

While protocols based on polynomial commitments like KZG would commit to the quotient polynomial and then prove the relation $C_i(x)=D_i(x)·q(x)$ at a random point (using Schwartz-Zippel), the Starknet STARK protocol uses a different approach: it uses a FRI check to prove that the commitment to the evaluations of $q(x)=\frac{C_i(x)}{D_i(x)}$ correctly represents a polynomial of low degree.

As such, the role of the verifier is to verify that all the quotient polynomials associated with all the constraints exist and are of low-degree.

TODO: define low-degree better

As we want to avoid having to go through many FRI checks, the verifier sends a challenge $\alpha$ which the prover can use to aggregate all of the constraint quotient polynomials into a composition polynomial $h(x):={\sum }_{i=0}\frac{C_i(x)}{D_i(x)}·{\alpha }^i$.

This composition polynomial is quite big, so the prover provides a commitment to chunks or columns of the composition polynomials, interpreting $h$ as $h(x)={\sum }_i{h}_i(x)x^i$.

Finally, to allow the verifier to check that $h$ has correctly been committed, Schwartz-Zippel is used with a random verifier challenge called the "oods point". Specifically, the verifier evaluates the following and check that they match:

• the left-hand side ${\sum }_{i=0}\frac{C_i(\text{oods\_point})}{D_i(\text{oods\_point})}·{\alpha }^i$
• the right-hand side $h_0(\text{oods\_point})+h_1(\text{oods\_point})·\text{oods\_point}$

Of course, the verifier cannot evaluate both sides without the help of the prover! The left-hand side involves evaluations of the trace polynomials at the oods point (and potentially shifted oods points), and the right-hand side involves evaluations of the composition column polynomials at the oods point as well.

As such, the prover sends the needed evaluations to the verifier so that the verifier can perform the check. (These evaluations are often referred to as the "mask" values.)

Notice that this "oods check" cannot happen in the domain used to index the trace polynomials. This is because the left-hand side involves divisions by domain polynomials $D_i(\text{oods\_point})$, which might lead to divisions by zero.

This is why the oods point is called "out-of-domain sampling". Although nothing special is done when sampling this point, but the probability that it ends up in the trace domain is very low.

TODO: explain what parts does the term "DEEP" refer to in this protocol.

Aggregation and FRI Proof

The verifier now has to:

1. Perform a FRI check on $h_0(x)+x{h}_1(x)$ (which will verify the original prover claim that the trace polynomials satisfy the constraints).
2. Verify all the evaluations that were sent, the prover and the verifier can use FRI-PCS for that, as described in the FRI-PCS section of the Starknet FRI Verifier specification.

TODO: the second point also should have the effect of proving that the commitments to the trace column polynomials are correct (as they will also act as FRI checks)

In order to avoid running multiple instances of the FRI protocol, the FRI Aggregation technique is used as described in the Aggregating Multiple FRI Proofs section of the Starknet FRI Verifier specification. The verifier sends a challenge called oods_alpha which is used to aggregate all of the first layer of the previously discussed FRI proofs.

Finally, the FRI protocol is run as described in the Starknet FRI Verifier specification.

AIR Arithmetization Dependency

While this specification was written with Cairo in mind, it should be usable with any AIR arithmetization that can be verified using the STARK protocol.

A protocol that wants to use this specification should provide the following:

interactive arithmetization. A description of the interactive arithmetization step, which should include in what order the different tables are committed and what verifier challenges are sent in-between.

eval_composition_polynomial. A function that takes all of the commitments, all of the evaluations, and a number of Merkle tree witnesses sent by the prover and produces an evaluation of the composition polynomial at the oods point. (This evaluation will depend heavily on the number of trace columns and the constraints of the given AIR arithmetization.) The function is expected to verify any decommitment (via the Merkle tree witnesses) that it uses.

eval_oods_polynomial. A function that takes all of the commitments, all of the evaluations, and a number of Merkle tree witnesses sent by the prover and produces a list of evaluations of the first layer polynomial of the FRI check at a list of queried points. The function is expected to verify any decommitment (via the Merkle tree witnesses) that it uses.

We refer to the Merkle Tree Polynomial Commitments specification on how to verify decommitments.

Protocol constants

STARKNET_PRIME = 3618502788666131213697322783095070105623107215331596699973092056135872020481. The Starknet prime ($2^{251}+17·2^{192}+1$).

FIELD_GENERATOR = 3. The generator for the main multiplicative subgroup of the Starknet field. This is also used as coset factor to produce the coset used in the first layer's evaluation.

Channel

See the Channel specification for more details.

FRI

See the Starknet FRI Verifier specification.

Specifically, we expose the following functions:

• fri_commit
• fri_verify_initial
• fri_verify_step
• fri_verify_final

as well as the two objects FriVerificationStateConstant, FriVerificationStateVariable defined in that specification.

Domains and Commitments

Commitments to all the polynomials, before the FRI protocol, are done on evaluations of polynomials in the evaluation domain as defined in the Domains and Commitments section of the Starknet FRI Verifier specification.

Commitments to all the polynomials, before the FRI protocol, are done using table commitments as described in the Table Commitments section of the Merkle Tree Polynomial Commitments specification.

• For trace polynomials in the interactive arithmetization phase, the tables committed into the leaves represent the evaluations of each of the trace columns at the same point.
• For composition column polynomials in the composition polynomial phase, the tables committed into the leaves represent the evaluations of each of the composition columns at the same point.

STARK commit

The goal of the STARK commit is to process all of the commitments produced by the prover during the protocol (including the FRI commitments), as well as produce the verifier challenges.

1. Interactive arithmetization to absorb the execution trace tables:
   1. Absorb the original table with the channel.
   2. Sample the interaction challenges (e.g. z and alpha for the memory check argument (different alpha called memory_alpha to distinguish it from the alpha used to aggregate the different constraints into the composition polynomial)).
   3. Absorb the interaction table with the channel.
2. Produce the aggregation of the constraint quotient polynomials as the composition polynomial:
   1. Sample the alpha challenge ("composition_alpha") to aggregate all the constraint quotient polynomials (caches the powers of alpha into "traces_coefficients").
   2. Absorb the composition columns (the $h_i$ in $h(x)={\sum }_i{h}_i{x}^i$) with the channel.
   3. Sample the oods point (interaction_after_composition).
   4. Absorb all evaluations with the channel.
   5. Verify that the composition polynomial is correct by checking that its evaluation at the oods point is correct using some of the evaluations ${\sum }_j\frac{C_j(\text{oods\_point})}{D_j(\text{odds\_point})}={\sum }_i{h}_i(\text{oods\_point})\times {\text{oods\_point}}^i$.
      1. The right-hand side can be computed directly using the evaluations sent by the prover
      2. The left-hand side has to be computed using the eval_composition_polynomial function defined in the AIR Arithmetization Dependency section.
3. Produce a challenge to aggregate all FRI checks and run the FRI protocol:
   1. Sample the oods_alpha challenge with the channel.
   2. Call fri_commit.

STARK verify

The goal of STARK verify is to verify evaluation queries (by checking that evaluations exist in the committed polynomials) and the FRI queries (by running the FRI verification).

To do this, we simply call the fri_verify_initial function contained in the FRI specification and give it the values computed by eval_oods_polynomial (as defined in the AIR Arithmetization Dependency section) as first evaluations associated with the queried points. It should return two FRI objects.