Definition of M3

Including tables, constraints, flushing rules and channels

Here, we define M3 at a reasonable level of rigor, targeting a thorough conceptual understanding of what its instances look like. Throughout, we work with the binary datatypes we've already discussed.

Basic Objects

A M3 instance consists of various objects, which interact.

Channels

A channel is simply an abstract, stateful bidirectional "receptacle" of data, which features a fixed width and type signature. That is, each channel exposes two methods, "push" and "pull". These methods have identical signatures; that is, both take a single tuple, with a fixed number of components, which themselves each have prescribed bit-widths. The tuple arity and type signature a channel features are durable, permanent properties of that channel.

Finally, a channel either is or isn't balanced at any given time. To be balanced entails simply that its pushes exactly match its pulls. That is, the respective multisets of its pushed and pulled elements (i.e., ignoring order, but counting multiplicity) are equal.

For example, a channel with the following table of accumulated pushes and pulls:

Pushes	Pulls
`(0xd9de, 0x86cd91f4)`	`(0xd9de, 0x86cd91f4)`
`(0xd9de, 0x86cd91f4)`	`(0xbd8f, 0x00000000)`
`(0xd9de, 0x0000d9de)`	`(0xd9de, 0x86cd91f4)`
`(0xbd8f, 0x00000000)`	`(0xd9de, 0x0000d9de)`

would be balanced. But if we changed any single character in this table, the channel would become unbalanced—as it likewise would if we, say, added an element to the left-hand side (but not the right).

Tables and constraints

A table is what it sounds like—an ordered list of rows, each with a fixed width and fixed cell-types. Indeed, like channels, M3 tables also have prescribed "signatures", fixed once and for all by the instance specification. Each table has a fixed number of columns; each column is itself of a fixed type (one of the tower field heights).

Moreover, to each table is associated a plurality of polynomial constraints. Each constraint is a multivariate polynomial with as many variables as the table has columns. The polynomial's field of definition will itself be a tower-subfield.

A table is said to satisfy its constraints when each of its constraint polynomials vanishes identically on the table's rows. That is, for each of the table's constraint polynomials, for each row of the table, the polynomial, evaluated on the row, outputs 0.

For example, we can write down a table with three columns, $John$ , $Mary$ , and $Fred$ , of types $\mathcal{T}_4$ , $\mathcal{T}_5$ , and $\mathcal{T}_5$ , respectively. We are moreover going to impose the algebraic constraint whereby

\begin{equation*}John \cdot Mary = Fred.\end{equation*}

Here is an example of our table, populated with a few rows (which satisfy the constraint):

John ( $\mathcal{T}_4$ )	Mary ( $\mathcal{T}_5$ )	Fred ( $\mathcal{T}_5$ )
`0xd9de`	`0x5dd09445`	`0x86cd91f4`
`0xd9de`	`0x5dd09445`	`0x86cd91f4`
`0xd9de`	`0x00000001`	`0x0000d9de`
`0xbd8f`	`0x00000000`	`0x00000000`

The rough intuition is that the prover won't have direct access to the instance's channels. He will, on the other hand, have direct access to its tables, in the sense that the prover will be at liberty to populate the tables arbitrarily—subject, of course, to the requirement whereby the rows it appends satisfy their tables' constraints.

Flushing rules

Intuitively, flushing rules "wire" tables into channels. They can also be called "routing rules". Each flushing rule dictates that a particular set of columns—themselves either transparent, committed or virtual columns, all associated with a single table—should be bundled into tuples, and pushed or pulled (as the case may be) into a particular channel. The intuition is that our tables will get "flushed" into our channels, and the flushing rules tell us how.

More precisely, each flushing rule specifies:

An ordered sequence of columns, all drawn (either explicitly or virtually derived) from a single table.
A channel.
A direction (push or pull).

Sanity check. In order for this to typecheck, the "tuple type" represented by the flushing rule's column subset must match the tuple type of the channel. That is, both its width (number of components) and its component types must match.

For example, a flushing rule might say that

The tuple $(John, Fred)$ should be pushed to the above channel.

Note that this typechecks; indeed, our channel above expects tuples of type $(\mathcal{T}_4, \mathcal{T}_5)$ . Indeed, by looking back at the example channel state written down above, you will see that that channel's pushes are exactly what would come out of this flushing rule.

Note that we could have also defined a flushing rule involving virtual columns. For example, we could have declared that:

The tuple $(g \cdot Mary + John, Fred)$ should be pulled from the above channel.

Here, $g \in \mathcal{T}_4$ is some fixed, constant field element. The linear combination $g \cdot Mary + John$ is a perfectly good virtual column, based on the above table, and is fair game to use in flushing rules.

On the other hand, the flushing rule

The tuple $(John, Mary, Fred)$ should be pushed to the above channel.

wouldn't make sense / typecheck, since there would be too many components for the channel (3, instead of 2).

Boundary conditions

Finally, we will in general want to allow the "preseeding" of channels with statement-dependent data. The idea here is that before populate the tables and apply the flushing rules, we initialize the channels with some statement-dependent initial state. What this means is that we will take certain values and "manually" push or pull them directly to certain channels. An example of this can be seen in our M3 example, where the verifier started things off by pushing 3,135 (the statement) and pulling 1 (a null / terminal value).

There is a further slight subtlety. Even standard flushing rules, which do involve tables, can either involve "statement" columns—which capture the what prover is trying to show in the first place—or "witness" columns, which are merely auxiliary, and serve only to cause the instance's channels to balance. For example, in Lasso, the lookup table $T$ and the looked-up column $U$ are "statement columns", while the read counts $R$ and the final counts $F$ are "witness columns".

Instances and Attempts

We will use the term M3 instance to refer to a general specification of channels, tables, flushing rules, and boundary conditions. An instance describes how many channels there are (and what their type signatures are), how many tables there are (and what their type signatures are), what the flushing rules are, and finally how channels should be pre-seeded using statement-dependent data.

For example, an instance might declare that there be two channels, one of type $(\mathcal{T}_0, \mathcal{T}_3, \mathcal{T}_4)$ and the other of type $(\mathcal{T}_4, \mathcal{T}_5)$ , and two tables, one of type $(\mathcal{T}_4, \mathcal{T}_5, \mathcal{T}_5)$ , and one of type $(\mathcal{T}_0, \mathcal{T}_3)$ . These tables might be respectively constrained by the polynomials $X_0 \cdot X_1 = X_2$ and $X_0^3 = X_1$ , say. It might finally declare that the first two columns of its first table be pushed to its second channel, and that table's first and third columns be pulled from it, as well as that both columns of its second table and the first column of its first table be pushed to its first channel. Finally, it might pre-push the statement—of type $(\mathcal{T}_0, \mathcal{T}_3, \mathcal{T}_4)$ —to its first channel, and pre-pull (0x0, 0x00, 0x0000).

Of course, this makes no sense, but it's merely an example of what an M3 instance specification might look like. We'll see "real" examples soon.

We will distinguish between instances, defined above, and attempts. An attempt at an M3 instance is a particular value for the statement, as well as an actual population of the instance's tables with appropriately-typed values.

Satisfaction

We're finally ready to say what it means for an attempt to satisfy an instance. To define satisfaction, we will go through the following algorithm.

All of the instance's channels begin in the empty state.
If called for by the instance specification, certain channels are prepopulated with the appropriate statement-dependent data.
All of the attempt's tables are flushed into the instance's channels, per the instance's flushing rules.
The attempt satisfies the instance if all of the instance's channels are now balanced.

This completes our definition of M3 in the abstract. Soon, we will see various real-life examples.

Push or Pull?

We end this section by remarking on the directionality of channels. Thus far, the terms "pushing" and "pulling" have been arbitrary, and could have been freely reversed throughout. As it happens in practice, these directions matter, and cannot in general be interchanged. Roughly, "pushing" a tuple to a channel corresponds to "registering it as a new, pending, unresolved liability". In contrast, "pulling" a tuple from a channel corresponds to "declaring it as stricken, accounted for and resolved". In practice, M3 instances tend to operate by allowing the prover to pull large claims, but only if he simultaneously pushes various smaller claims, whose collective truth moreover implies the large claim. Indeed, this was more-or-less the pattern visible in our toy example.