Mathematizing M3 Instances

Converting M3 instances into mathematical claims

As we've argued, M3 is a flexible abstraction that lets us formulate and capture computational problems. On the other hand, M3 is only as useful as it is amenable to actual cryptographic treatment. How do we solve M3 problems, once we've formulated them? Much of this entire site section will be devoted to this very problem.

In this page, we discuss the first step in this process: translating M3 instances into mathematical claims to begin with. Those claims will then get fed in as inputs to our cryptographic reductions. We haven't yet explained those reductions, of course. This page is thus more like a "bridge" between our arithmetization section and this blueprint. We will generally be tying ideas from M3 to mathematical techniques contained throughout this section, pointing in advance to those sections before we arrive at them.

Mathematizing the Attempt

Here, we explain how to re-express the prover's M3 attempt satisfaction in mathematical terms. We take for granted here the full definition of M3.

Tables

As we will see shortly, columns in a table and multilinear polynomials are one and the same thing. We can thus freely view the prover's tables as sequences of multilinear polynomials. We will ultimately ask the prover to commit to these columns before the proof kicks off.

Constraints

Our constraints were already defined to be polynomials acting row-wise on our tables. These are mathematical objects in their own right.

Thus, it is not hard to mathematically formulate the condition whereby the prover's tables satisfy their constraints. We fix a particular table, populated during a prover attempt in such a way that it has $2^\ell$ rows, let's say. We write $t_0, \ldots t_{n - 1}$ for this table's columns, suitably reinterpreted as multilinears; here, each $t_i(X_0, \ldots , X_{\ell - 1})$ is an $\ell$ -variate multilinear over an appropriate field (i.e., the field of definition of the relevant column). Finally, we write $c_0, \ldots , c_{m - 1}$ for the table's constraints. Each of these is a $n$ -variate polynomial, defined over the indeterminates $Z_0, \ldots , Z_{n - 1}$ , say. The table's satisfaction of its constraints amounts to the condition whereby, for each constraint $j \in \{0, \ldots , m - 1\}$ , the $\ell$ -variate composition polynomial

\begin{equation*}C_j(t_0(X_0, \ldots , X_{\ell - 1}), \ldots, t_{n - 1}(X_0, \ldots , X_{\ell - 1}))\end{equation*}

vanishes identically on the cube $\mathcal{B}_\ell$ .

This is precisely the condition that the zerocheck is designed to process. That is, that protocol reduces vanishing claims like this into evaluation claims, amenable to our cryptographic techniques.

Channel balancing

Channels, under the hood, are essentially pairs of dueling multisets. A multiset is a list of elements, in which the unique items are counted, as is the number of times each item appears (its multiplicity), but the order of the elements is not counted.

To check whether any given channel balances, then, it's enough to simply running a multiset-check. As we explain in our reductions section, we know exactly how to evaluate these checks—or more precisely, how to reduce them to grand-product claims, themselves amenable to our GKR-based grand-product argument.

Flushing rules

The catch is that the particular multisets involved in each channel-balancing check will not—in almost all interesting cases—be simple committed multilinears. Rather, they will be populated by flushing rules. Indeed, in general, each multiset at hand will contain not just elements but tuples; moreover, it will have "received" its tuples from many different sources, at the hands of many different flushing rules. That is, in general, many different flushing rules will contribute elements to each given, particular multiset (by pushing or pulling to that multiset's channel, as the case may be).

In our section on virtual polynomials, we describe these ideas at length. That is, we describe how one can flush not just committed columns, but "virtual" columns which derive from these in arbitrary ways. One can also assemble aggregate multisets, which accrue members from many different virtual columns.

Stepping Back

In each of the above steps, we reduced the relevant M3 component to a cryptographic problem, treatable using our tools for those problems. The point though is that, after those reductions themselves are fully unwound, the work will be succinct for the verifier, and efficient (say, quasilinear) for the prover. This means that we can use M3 as our "lingua franca"—that is, as the top-level arithmetization language in which we capture our problems—assured all the while that we will be able to efficiently evaluate its instances.