Multiset checks with multiplicities and LogUp

This note picks up where the previous one on multiset checks left off. The main motivation for this note is to support a variation on multiset checks where we can encode how many times we expect an element to show up in the set (i.e. the multiplicity) without having that element showing up that many times. Specifically, the multiset check with multiplicities equation is

i=1n1j=1k(αaij)maij=i=1n1j=1k(αbij)mbij

For example, if

ma23=2, then the term
(αa23)
in the equation is repeated twice:
(αa23)(αa23)
. Hence, the value
a23
would appear once in the
{aij}
multiset, but would need to appear twice in the
{bij}
multiset (or equivalently, only once, but with an associated multiplicity of
2
). Note also that setting a multiplicity value to
maij=0
has the effect of "turning off" the associated
(αaij)
term.

This is especially useful for range checks, which the Miden VM docs have a good introduction about.

The problem with multiplicities

Adding multiplicities creates challenges when implementing the new equation in STARKs, as it makes the running product column discussed in the previous note no longer viable. Specifically, the transition constraint for the running product column

p would need to be:

p[i+1]=p[i]×j=1k(αaij)maij(αbij)mbij.

The right-hand side equation is not a polynomial, since both

maij appears in the exponent position, and is itself a polynomial (and similarly for
mbij
). LogUp was designed to solve that problem.

LogUp

The core idea of LogUp is relatively simple. It involves applying the logarithm to both sides of the multiset check with multiplicities equation, followed by a derivative.

Note that the logarithm and the derivative are concepts defined over the real numbers. The paper goes into the formalism of how to formally think about these operations over finite fields, which we will take for granted in this note.

Start with the multiset check with multiplicities equation,

i=1n1j=1k(αaij)maij=i=1n1j=1k(αbij)mbij,

apply the logarithm to both sides (and a few logarithm rules),

logi=1n1j=1k(αaij)maij=logi=1n1j=1k(αbij)mbiji=1n1j=1klog((αaij)maij)=i=1n1j=1klog((αbij)mbij)i=1n1j=1kmaijlog(αaij)=i=1n1j=1kmbijlog(αbij),

and then apply the derivative to both sides (where

x will stand for the "current" and "next" row, the inputs to
aij
and
bij
)

ddxi=1n1j=1kmaijlog(αaij)=ddxi=1n1j=1kmbijlog(αbij)i=1n1j=1kmaijddxlog(αaij)=i=1n1j=1kmbijddxlog(αbij)i=1n1j=1kmaij(αaij)=i=1n1j=1kmbij(αbij).

And that's it! The final form of the LogUp equation is

i=1n1j=1kmaij(αaij)=i=1n1j=1kmbij(αbij)

Implementing LogUp in STARKs

LogUp in STARKs is going to look very similar to standard multiset checks: we will implement a running sum auxiliary column instead of a running product. Let's see how that would work. But first, we need to rearrange the LogUp equation slightly by subtracting the right-hand side on both sides:

i=1n1j=1kmaij(αaij)i=1n1j=1kmbij(αbij)=0i=1n1(j=1kmaij(αaij)mbij(αbij))=0

Our running sum column

s is going to be built similarly to the running product column for multiset checks. The first row will always contain
0
, and each new row will start with the previous row's value, add
j=1kmaij(αaij)
, and subtract
j=1kmbij(αbij)
:

Row
s
1 0
2
j=1kma0jαa0jmb0jαb0j
3
i=12j=1kmaij(αaij)mbij(αbij)
4
i=13j=1kmaij(αaij)mbij(αbij)
n1
i=1n2j=1kmaij(αaij)mbij(αbij)
n
i=1n1j=1kmaij(αaij)mbij(αbij)

Boundary constraints

In the boundary constraints, we make sure that the first and last row of

s contain
0
:

s[1]=s[n]=0

Transition constraint

Then, the transition constraint needs to ensure that every row

i (except the last) is built by taking the value in the previous row, add in
j=1kmaij(αaij)
, and subtract out
j=1kmbij(αbij)
:

s[i+1]=s[i]+(j=1kmaij(αaij))(j=1kmbij(αbij)).

However, the current form is not a valid polynomial expression. We need to rearrange the equation so that we remove the division operations for equivalent multiplications:

s[i+1](j=1kαaij)(j=1kαbij)=s[i](j=1kαaij)(j=1kαbij)+j=1kmaijej(αaie)e=1k(αbie)j=1kmbijej(αbie)e=1k(αaie)

This equation is a little difficult to parse, but it is simply the result of multiplying out all the denominators on both sides. For example, if

k=1, then the equation would look like:

s[i+1](αai0)(αbi0)=s[i](αai0)(αbi0)+mai0(αbi0)mbi0(αai0)

Ultimately, the running sum column implementing LogUp achieved what the running product column could not: a polynomial transition constraint.

Transition constraint degree

LogUp is a good choice for use cases that can't do without representing multiplicities. However, as we'll see, we pay with a higher transition constraint degree. Specifically, the transition constraint degree is the maximum of

1+j=1k(degaij+degbij),j,degmaij+ejdegaie+e=1kdegbie,andj,degmbij+ejdegbie+e=1kdegaie.

The biggest difference with the running product column transition constraint degree (other than the fact that we now have multiplicities) is that now the degree of the

aij's and the
bij
's add together.

Hence, the rule of thumb is that between a standard multiset check and LogUp, prefer to use a standard multiset check when possible to lower the transition constraint degree.