This is the second part in our series about the math behind STARKs (first part here), and it is the first of two posts about arithmetization.
By the time you complete this post, you should have a good idea of what execution trace and polynomial constraints are, and how a Computational Integrity statement gets transformed into these. We will start with a simple example of a supermarket receipt, and move on to a slightly more complex one, that of Collatz sequences, that relates to a well-known open problem in number theory. We will assume basic familiarity with polynomials over finite fields, and binary representations of integers.
STARK in Broad Strokes
The goal of the STARK protocol is to verify computations succinctly and transparently. The first step in STARK is called arithmetization, and it is the translation (often referred to as ‘reduction’) of the problem of verifying a computation to the problem of checking that a certain polynomial, which can be evaluated efficiently on the verifier’s side (this is the ‘succinctly’ part), is of low degree. Arithmetization is useful since it enables the use of tools from the realm of Error Correction Codes that efficiently test low degree-ness. However, arithmetization itself only translates a Computational Integrity statement into a polynomial, setting the scene for the next phase in STARK, which is another interactive protocol that involves a prover that attempts to convince a verifier that the polynomial is indeed of low degree. The verifier is convinced that the polynomial is of low degree if and only if the original computation is correct (except for an infinitesimally small probability). In the last step of STARK, the interactive protocol is transformed into a single non-interactive proof, that can be posted to a blockchain and publicly verified by anyone.
Arithmetization itself is composed of two steps: the first is generating an execution trace and polynomial constraints, the second is transforming these two objects into a single low-degree polynomial. In terms of prover-verifier interaction, what really goes on is that the prover and the verifier agree on what the polynomial constraints are in advance. The prover then generates an execution trace, and in the subsequent interaction, the prover tries to convince the verifier that the polynomial constraints are satisfied over this execution trace, unseen by the verifier.
Recap — Computational Integrity Statements
In the previous post we discussed the notion of a Computational Integrity (CI) statement, the claim that the output of a certain computation is correct, from an abstract standpoint. Let’s take a look at a concrete example for a CI statement: the total sum we should pay at the supermarket was computed correctly. The conventional proof for this particular statement is the receipt. Typically, the items in the receipt are listed with their prices, and the total sum is indicated at the bottom, like so:
For simplicity — we only consider this to be a statement that the summation is correct. To see whether this CI statement holds, one can go over the list — not skipping any item — to compute the total sum, and check it against the number at the bottom of the receipt. This is a very naive example, but we’ll use it further down this article to demonstrate the idea of succinct testability.
Arithmetization
The first step of arithmetization is to take some CI statement (such as “the fifth transaction in block 7218290 is correct”), and translate it into formal algebraic language. This serves two purposes: 1) it defines the claim succinctly in an unambiguous way, and 2) it embeds the claim in an algebraic domain. This embedding is what allows the second step of arithmetization, which reduces the CI statement to a claim about the degree of a specific polynomial.
The algebraic representation that we use has two main components: 1) an execution trace, and 2) a set of polynomial constraints. The execution trace is a table that represents the steps of the underlying computation, where each row represents a single step. The set of polynomial constraints is constructed such that all of them are satisfied if and only if the trace represents a valid computation. While the execution trace may be very long, we will work with a succinct set of polynomial constraints.
Execution Trace
The type of execution trace that we’re looking to generate must have the special trait of being succinctly testable — each row can be verified relying only on rows that are close to it in the trace, and the same verification procedure is applied to each pair of rows. This trait directly affects the size of the proof. To exemplify what we mean by being succinctly testable, let’s go back to the supermarket receipt, and add another column for the running total:
This simple addition allows us to verify each row individually, given its previous row.
We can, for example, examine these two rows:
and be convinced that this particular step of the computation (i.e. the number 16.41) is correct since 12.96+3.45=16.41. Notice that the same constraint is applied to each pair of rows. This is what we mean by succinct constraints.
Polynomial Constraints
Let’s rewrite the supermarket receipt (with the running total) in the form of a table:
Denote the value of the cell in the i-th row and j-th column by Ai,j (we’ll denote subscript that way since Medium does not support LaTeX). We can now rephrase the correctness conditions as this set of polynomial constraints:
These are linear polynomial constraints in Ai,j. If the set of polynomial constraints we use are of high degree, this has an adverse effect on the proof length and the time it takes to generate it. Consequently, linear constraints are the best we can hope for. Notice that (2) is really a single constraint applied multiple times, and the whole size of the set is independent of the length of the receipt.
In sum, we took a CI problem of verifying a supermarket receipt, and transformed it into a succinctly testable execution trace, and a corresponding set of polynomial constraints that hold if and only if the total sum in the original receipt is correct.
Let’s see a more complex example.
Collatz Conjecture
In 1937, a German mathematician named Lothar Collatz presented a conjecture in the field of number theory. At first glance this conjecture might seem merely a cute math puzzle, but in fact it is a hard open problem in number theory. It caught the attention of many mathematicians over the years, and acquired a lot of synonyms (e.g., the 3n + 1 conjecture, the Ulam conjecture, Kakutani’s problem and many more). Paul Erdős once said about this conjecture: “Mathematics may not be ready for such problems”.
A Collatz sequence starts with any positive integer, where each subsequent element in the sequence is obtained from the previous one as follows:
- If the previous element is even: divide it by 2.
- If the previous element is odd and greater than 1: multiply it by 3 and add 1.
- If the previous element is 1, stop.
Let’s consider a simple example where the initial term is 52:
52 -> 26 -> 13 -> 40 -> 20 -> 10 -> 5 -> 16 -> 8 -> 4 -> 2 -> 1.
Collatz Conjecture: for any positive integer we start with, the sequence always reaches 1.
Unfortunately, resolving the Collatz Conjecture is beyond the scope of this blog post. Instead, we will consider the problem of verifying a computation that checks the conjecture for a particular starting integer.
The Collatz Sequence Execution Trace
The CI statement is: “A Collatz sequence that starts with 52, ends with 1 after 11 iterations”.
Let A be the execution trace of the sequence’s computation. The i-th row, denoted by Ai, represents the i-th number in the sequence. All numbers are represented as binary strings, to make it easier to express the odd/even condition with polynomials. Ai,j equals to the j-th least significant bit of the i-th number of the sequence. For example, A0=001011: the first term is 52, its binary representation is 110100 and then we reverse the bits’ order (bit reversal order simplifies indexing in the polynomial constraints notation).
Here is the execution trace of the above Collatz sequence that starts with 52:
Note that here the trace has 6 columns because 6 bits are enough to represent even the largest number in the sequence. Had we started the sequence with 51, the next number would have been 154, so the trace of such a sequence would have required at least 8 columns.
The Collatz Sequence Polynomial Constraints
Recall that the polynomial constraints we are looking for are such that all of them are satisfied if and only if the trace A describes the given Collatz sequence (starting with 52, ending with 1, and the transition from any two consecutive rows is done correctly). In our example, the trace A is of size 6x12, i.e., it represents a Collatz sequence of 12 6-bit numbers. The set of polynomial constraints are the following (n=12, m=6):
Let’s go over each of the constraints. The first three are straightforward:
(1) holds if and only if the first row is a binary representation of 52.
(2) holds if and only if the last row is a binary representation of 1.
(3) holds if and only if the trace contains only bits (a number is equal to its square if and only if it is either 0 or 1).
The fourth set of constraints defines the heart of the succinct computation of the sequence, i.e., the connection between every two consecutive rows. The ability to express computational constraints as a recurring pattern of local constraints (i.e. succinctness), is fundamental to the verifier being exponentially faster than a naive replay of the computation.
Let’s examine the constraints themselves carefully.
For any i<n-1, denote:
Hence, for each i<n-1, we get the following constraint:
Ai,0 is the least significant bit of the i-th number, which determines its parity as an integer, so this constraint describes the Collatz sequence rule.
To sum up, all constraints are satisfied if and only if the trace represents a valid computation of a Collatz sequence.
Note that any Collatz sequence of length n, can be represented using a trace of size n*m where m is the maximum number of bits in the representation of a number in the sequence, and the corresponding polynomial constraints are modified accordingly. Note that the polynomial constraints do not grow with n and m, but remain simple and concise.
Given a specific first term for a Collatz sequence, a simple computer program can output the execution trace and the polynomial constraints.
Conclusion
In this post we covered the first step in arithmetization of CI statements.
We have seen how a CI statement about a Collatz sequence can be transformed into an execution trace and a succinctly-described set of polynomial constraints. Similar methods can be used to transform any computation, and in general, any CI statement can be translated into this form. The details, however, matter a great deal. While there are many ways in which an execution trace (and a set of polynomial constraints) may describe a specific computation, only a handful of them result in a small STARK proof which can be constructed efficiently. Much of the effort in StarkWare is devoted to designing reductions that lead to good polynomial constraints, which we call AIR (Algebraic Intermediate Representation), as much of the performance of our systems depends on it.
In the next post we’ll cover the second step in arithmetization — transforming the execution trace and the polynomial constraints into a single polynomial, one that is guaranteed to be of low degree, if and only if the original computation is correct.
Kineret Segal & Shir Peled
StarkWare
