Remember to familiarize yourself with our math conventions.
A "multiset check" checks the equality of two multisets (i.e. sets where multiple copies of the same element are allowed). Multiset checks are also called "permutation checks", because equivalently, they check whether a list is a permutation of another list. In the context of STARK-based zk-VMs, these multisets are derived from the trace.
For example, column 1 and column 2 could be the two multisets of interest, in which case running a multiset check would ensure that the values in column 1 are the same values as in column 2, potentially rearranged. Or, \(\mathrm{column_1} \cup \mathrm{column}_2\) could be the first multiset, while \(\mathrm{column_3} \cup \mathrm{column}_4\) could be the second multiset. However, as we'll see in the next section, the elements in the multisets don't actually need to live explicitly in the trace.
Before we discuss how to implement a multiset check, we should first give a proper definition of how our multisets are defined.
There are multiple possible definitions, and each different definition will influence how the multiset check is implemented. In this note, we will focus on the definition used in the Miden VM.
A first take at a definition of an element of a multiset is:
\[ a_x = f(c_1(x), \dots, c_m(x), c_1(\omega x), \dots, c_m(\omega x)), \]
where \(f\) is a polynomial, \(x \in \mathbb{H}\), and as usual \(\omega\) is our domain generator. Recall that when \(x \in \mathbb{H}\) (that is, when \(x\) represents a trace row), \(\omega x\) represents the next row after \(x\).
Put simply, the elements of the multisets as defined as a polynomial over any given trace row and the next. It is no accident that this is the same form as an AIR transition constraint: ultimately the transition constraints will be implementing the multiset check, and they must be able to represent the elements of the multiset.
For example, this definition allows elements of the first set \(\{a_i\}_{i=1}^n\) to be defined as \(c_0(x) + 2 c_1(x) + 4 c_2(x) + 8 c_3(x)\). If columns \(c_0, \dots, c_3\) are also constrained to be \(0\) or \(1\), then the \(\{a_i\}_{i=1}^n\) would correspond to the element "made up" of the bits in those columns. To put it concretely, if \(c_0(5) = 1, c_1(5) = 0, c_2(5) = 0, c_3(5) = 1\), then \(a_5 = 9\).
After we introduce so-called "auxiliary columns" and their corresponding "auxiliary constraints", we will generalize the current definition slightly, but the general idea will remain the same.
We are now ready to discuss the core idea behind how multiset checks will be proved. The next section will use this core idea to then show how multiset checks are implemented in STARKs.
Let our two multisets be \(\{a_i\}_{i=1}^k\) and \(\{b_i\}_{i=1}^k\), where \(k\) is any integer. The core idea is the following: build 2 polynomials, one for each multiset, where the roots of each polynomial is their respective multiset. Then, check for equality of those 2 polynomials. Due to how the polynomials were defined, if both polynomials are equal, then the multisets are also equal; and if the polynomials are not equal, then the multisets also are not equal.
Concretely, we define the 2 polynomials are defined as:
\[ p_a(x) = \prod_{i=1}^k (x - a_i) \]
and
\[ p_b(x) = \prod_{i=1}^k (x - b_i) \]
Then, multiset equality \(\{a_i\}_{i=1}^k = \{b_i\}_{i=1}^k\) is equivalent to polynomial equality
\[ \prod_{i=1}^k (x - a_i) = \prod_{i=1}^k (x - b_i) \]
We will give the short argument for why this polynomial equality is equivalent to the multiset equality \(\{a_i\}_{i=1}^k = \{b_i\}_{i=1}^k\). For polynomials over finite fields, monic polynomials such as \(p_a\) and \(p_b\) (i.e. highest degree coefficient is 1) have a unique factorization. That is, if 2 polynomials are different, then their factorization is different. This is analogous to how primes work for the integers: every integer has a unique factorization in terms of prime numbers. Notice as well that each factor of \(p_a\) or \(p_b\) uniquely identifies its corresponding root (i.e. \((x - a_i)\) identifies with \(a_i\)). Hence, \(p_a\) and \(p_b\) identify with their roots: that is, \(p_a = p_b\) if and only if \(\{a_i\}_{i=1}^k = \{b_i\}_{i=1}^k\). For more information about the theorems behind these claims, refer to this Wikipedia article section (or this more in-depth article).
Hence, we reduced the problem of checking for equality of multisets to the problem of checking for polynomial equality. By the Schwartz-Zippel lemma, we can (probabilistically) check for equality of polynomials by evaluating both polynomials at a random point \(\alpha \in \mathbb{F}\), and checking for equality:
\[ \prod_{i=1}^k (\alpha - a_i) = \prod_{i=1}^k (\alpha - b_i) \]
And so we have our general recipe for (probabilistically) checking if 2 multisets are equal: sample a random point, shift every element of the multisets by that point, and check that the (shifted) points of both multisets multiplied together are equal.
In the section Definition of a multiset in STARKs, we saw how multiset elements are defined in STARKs. In the previous section, we saw how to transform the problem of multiset equality to polynomial equality. In this section, we will put both together: how to prove multiset equality between multisets made up of elements derived from the trace.
First though, we will rewrite slightly the equality check from last section, from:
\[ \prod_{i=1}^k (\alpha - a_i) = \prod_{i=1}^k (\alpha - b_i) \]
to
\[ \prod_{i=1}^{n-1} \prod_{j=1}^k (\alpha - a_{ij}) = \prod_{i=1}^{n-1} \prod_{j=1}^k (\alpha - b_{ij}) \]
Notice now that \(i\) goes from \(1\) to \(n-1\) (the trace length minus the last row), and \(j\) goes from \(1\) to \(k\), where \(k\) is any integer. In words, we made explicit the row \(i\) at which each element comes from, and we say that there are \(k\) elements produced at each row.
Remember that \(a_{ij}\) and \(b_{ij}\) (for \(1 \le j \le k\)) are polynomials of row \(i\) and \(i+1\). Hence \(i\) goes from 1 to \(n-1\) instead of from \(1\) to \(n\). This is the first major consequence of our definition of \(a_{ij}\) and \(b_{ij}\): the last row alone of the main trace cannot generate any multiset element. As a result, in the Miden VM, we ensure that the last instruction executed is always HALT, which is guaranteed to never generate any multiset element.
Note: if a row only actually has 1 element to add to the multiset (or any number less than \(k\)), then the other \(k-1\) polynomials for that row can simply evaluate to \(0\). How that works in practice is that we have \(k\) polynomial expressions \(\hat{a}_{j}, 1 \le j \le k\) for the multiset \(a\) and \(k\) polynomial expressions \(\hat{b}_{j}, 1 \le j \le k\) for the multiset \(b\) that we apply at every row. \(\hat{a}_{j}\) and \(\hat{b}_{j}\) are of the form
\[ \begin{align} \hat{a}_{j} &= \mathrm{flag}_{a_j} \times a_{j} \\ \hat{b}_{j} &= \mathrm{flag}_{b_j} \times b_{j}, \end{align} \]where \(\mathrm{flag}_{a_j}\) and \(\mathrm{flag}_{b_j}\) are polynomials that act as "if statements". That is, over the trace domain they evaluate to 1 if \(a_j\) and \(b_j\) need to be activated, and 0 otherwise. And then \(a_j\) and \(b_j\) are the polynomials that encode what we actually want to add to their corresponding multisets.
To make this a little bit more concrete, in the context of a zk-VM, certain CPU instructions will need to add items to the \(a\) multiset, while other instructions will need to add items to the \(b\) multiset. Then, the flag polynomials \(\mathrm{flag}_{a_j}\) returns 1 if we're currently executing one of the instructions that generate multiset element \(a_j\), and 0 otherwise (and similarly for \(\mathrm{flag}_{b_j}\)).
We are now finally ready to look into how to implement the multiset check equation in a STARK. One final small adjustment to make to our equation is simply to bring everything on the left side by dividing both sides by the right side:
\[ \prod_{i=1}^{n-1} \prod_{j=1}^k \frac{\alpha - a_{ij}}{\alpha - b_{ij}} = 1 \]
We will implement this equation using a single "running product" column \(p\), where row \(i\) contains the product up to row \(i\). That is:
| Row | \(p\) |
|---|---|
| 1 | 1 |
| 2 | \(\prod_{j=1}^k \frac{\alpha - a_{0j}}{\alpha - b_{0j}}\) |
| 3 | \(\prod_{i=1}^{2} \prod_{j=1}^k \frac{\alpha - a_{ij}}{\alpha - b_{ij}}\) |
| 4 | \(\prod_{i=1}^{3} \prod_{j=1}^k \frac{\alpha - a_{ij}}{\alpha - b_{ij}}\) |
| \(\dots\) | \(\dots\) |
| \(n-1\) | \(\prod_{i=1}^{n-2} \prod_{j=1}^k \frac{\alpha - a_{ij}}{\alpha - b_{ij}}\) |
| \(n\) | \(\prod_{i=1}^{n-1} \prod_{j=1}^k \frac{\alpha - a_{ij}}{\alpha - b_{ij}}\) |
Before we continue any further, let's address the elephant in the room: \(\alpha\) is a randomly generated value, but AIR constraints don't have access to random values. We'll fully address this problem in the next section, where we introduce auxiliary columns that are designed to solve this problem. For now, we'll leave it as: the running product column is an auxiliary column, which has access to any number of random values that it needs.
Next, we discuss the boundary and transition constraints that ensure that the row is built as described.
The boundary constraints only need to ensure that the first and last row contain \(1\):
\[ p[1] = p[n] = 1 \]
Then, the transition constraint needs to ensure that every row \(i\) (except the last) is built by taking the value in the previous row, multiply in \(\prod_{j=1}^k \alpha - a_{ij}\), and divide out \(\prod_{j=1}^k \alpha - b_{ij}\):
\[ p[i+1] = p[i] \times \prod_{j=1}^k \frac{\alpha - a_{ij}}{\alpha - b_{ij}}. \]
However, we need to rearrange the previous equation, which is not a proper polynomial equation. Equivalently,
\[ (p[i+1] \times \prod_{j=1}^k \alpha - b_{ij}) - (p[i] \times \prod_{j=1}^k \alpha - a_{ij}) = 0 \]
We end this section with an analysis of the transition constraint degree, which plays a very important role in understanding the motivation behind LogUp-GKR. Formally, the transition constraint degree is the maximum of
\[ 1 + \sum_{j=1}^k \deg b_{ij}, \]
and
\[ 1 + \sum_{j=1}^k \deg a_{ij}. \]
In words, at a given row \(i\), the degrees of the polynomial expressions \(a_{ij}\) add (and similarly for \(b_{ij}\)). Hence, the "more complex" the multiset check, the higher the transition constraint degree. To put this in perspective, in the Miden VM, we currently limit the degree of all constraints to be \(9\) or less. Hence, this will end up being limiting, and be a main motivation for using LogUp-GKR. We will return to this concern after we've gone over LogUp in the next article.
As an aside, we can always reduce the degree of any \(a_{ij}\) or \(b_{ij}\) polynomial by adding a column in our main trace, where each of its row values are defined as \(\mathrm{col}[i] = a_{ij}\). Then, the degree of \(a_{ij}\) can be brought down to \(1\) by simply returning the value in this new column. However, adding a new column isn't free and incurs new costs on the prover. Whether or not a new column should be added for a given \(a_{ij}\) or \(b_{ij}\) is then a judgment call to be made by the VM designer.
Auxiliary columns are columns which can be built using values that were randomly generated. Equivalently, the boundary and transition constraints also have access to this randomness. This section only aims to give a short introduction to auxiliary columns.
The term "auxiliary" is the one used by Winterfell. Unfortunately, the same concept might be called differently elsewhere. For example, Plonky3 uses the term "permutation" instead.
To support auxiliary columns, we need to extend the STARK protocol slightly:
At the beginning of this note, we gave the following definition for multiset elements:
\[ a_x = f(c_1(x), \dots, c_m(x), c_1(\omega x), \dots, c_m(\omega x)). \]
However, in the last section, we learned that about auxiliary columns, and how their boundary and transition constraints can have access to any number of random values. It turns out that it can be useful to allow elements of multisets to be built using random values.
Specifically, let \(\psi = [\psi_0, \dots, \psi_{\mu - 1}]\) be a vector of \(\mu\) random values. We can then expand the definition of \(a_x\) to:
\[ a_x = f(\psi, c_1(x), \dots, c_m(x), c_1(\omega x), \dots, c_m(\omega x)). \]
This can be especially useful to reduce the degree of the transition constraint by taking a random linear combination of multiset elements. For example, say that each row generates 2 multiset elements for \(a\), and the same 2 for \(b\):
\[ \begin{align} a_{x0} &= c_0(x) \\ a_{x1} &= c_1(x) \\ b_{x0} &= c_0(x) \\ b_{x1} &= c_1(x) \\ \end{align} \]
This would mean that the transition constraint degree would be \(3\). What we can do is define the following instead:
\[ \begin{align} a_{x} &= \psi_0 c_0(x) + \psi_1 c_1(x) \\ b_{x} &= \psi_0 c_0(x) + \psi_1 c_1(x) \\ \end{align} \]
Then, columns \(c_0\) and \(c_1\) are properly include in the multiset checks, but we've reduced the transition constraint degree down to \(2\)! This is the basis of virtual tables in the Miden VM.
-
Any changes
Be notified of any changes
-
Mention me
Be notified of mention me
-
Unsubscribe
Subscribe