Try   HackMD

LogUp-GKR: The Air constraints

Recall from the previous article that running GKR on the LogUp circuit leaves us with the claims

f~0(ρ),,f~m1(ρ), for some randomly sampled
ρFlogn
. We will be proving these claims in Air.

Rather than proving

m separate claims, we will instead prove the random linear combination of these claims:

σ=j=0m1αjf~j(ρ)

for randomly sampled

αjF,
0j<m
.

Finally, let

g be the generator of a cyclic group
G
of size
n
, where
GF
.

Conventions

Let

iF. Then, we will use
i
to denote the bit decomposition of
i
. For example, if
i=4
, then
i=(0,0,1)
. Note that when representing bit decompositions, the least significant bit comes first, and the most significant bit comes last.

Given the trace length

n, let
μ=log2n
.

The columns

We will first re-arrange the equation to better reflect how we will be proving

σ.

σ=j=0m1αjf~j(ρ)=j=0m1αjx{0,1}μeq(x,ρ)fj(x)=x{0,1}μeq(x,ρ)j=0m1αjfj(x)

We will use 2 auxiliary columns, called

l and
s
, to prove
σ
. We will also refer to the
l
column as the "Lagrange kernel" column.

The Lagrange kernel column

Recall that the

eq polynomial is defined as

eq(x,ρ)=k=0μ1(1xk)(1ρk)+xkρk

for

xFμ and
ρFμ
.

Then, at row

i, the Lagrange kernel column will store
eq(i,ρ)
. For example, if
μ=3
, then the column would be constructed as

l
(1ρ0)(1ρ1)(1ρ2)
ρ0(1ρ1)(1ρ2)
(1ρ0)ρ1(1ρ2)
ρ0ρ1(1ρ2)
(1ρ0)(1ρ1)ρ2
ρ0(1ρ1)ρ2
(1ρ0)ρ1ρ2
ρ0ρ1ρ2

The
s
column

The

s column is defined as implementing a running sum of

x{0,1}μeq(x,ρ)j=0m1αjfj(x).

As we will see in later sections, since the Lagrange kernel column stores the expression

eq(x,ρ), the transition constraint for the
s
column will refer to
l
.

Additionally, we need to remove

iσn from row
i
to make the constraints work, as we will see in the last section.

For example, if

μ=3, then the column would be constructed as

s
σ8+l(0)j=0m1αjfj(0)
2σ8+i=01l(i)j=0m1αjfj(i)
3σ8+i=02l(i)j=0m1αjfj(i)
4σ8+i=03l(i)j=0m1αjfj(i)
5σ8+i=04l(i)j=0m1αjfj(i)
6σ8+i=05l(i)j=0m1αjfj(i)
7σ8+i=06l(i)j=0m1αjfj(i)
0

Notice that the last row of the

s column contains
0
. Hence, by now we can see the whole picture of how
l
and
s
work together to prove
σ
. The sum that defines
σ
is built row by row in
s
, which uses the values in the Lagrange kernel column. The last row of the
s
column contains
σ
, which will be ensured using a boundary constraint.

Next, we will look at the constraints that ensure

l and
s
are well constructed.

The constraints

We will first define the Lagrange kernel column constraints, followed by the

s column constraints.

The Lagrange kernel constraints

The Lagrange kernel constraints are unusual in that the number of transition constraints varies with the length of the trace. Also, the transition constraints rely on more rows than only the typical "current" and "next" rows. We will first the constraints, and follow up with an example that provides an intuition for why the constraints make sense.

The boundary constraints simply check that the first row is constructed correctly:

l(0)=eq(0,ρ)

As for the transition constraints, for each

κ{1,,μ},

ρμκl(x)(1ρμκ)l(g2μκ)=0

holds on the first

2κ1 roots of unity. In other words, the transition constraint divisor is
x2κ1
.

It's probably not immediately clear why these transition constraints make sense, and hence we will give an example where

μ=3 (i.e. the trace length
n=8
).

Example

To ensure that

l is properly built, we need the transition constraints to enforce the following 8 equations:

l(0)=eq(0,ρ)=(1ρ2)(1ρ1)(1ρ0)l(1)=eq(1,ρ)=(1ρ2)(1ρ1)ρ0l(2)=eq(2,ρ)=(1ρ2)ρ1(1ρ0)l(3)=eq(3,ρ)=(1ρ2)ρ1ρ0l(4)=eq(4,ρ)=ρ2(1ρ1)(1ρ0)l(5)=eq(5,ρ)=ρ2(1ρ1)ρ0l(6)=eq(6,ρ)=ρ2ρ1(1ρ0)l(7)=eq(7,ρ)=ρ2ρ1ρ0

The first equation is enforced using a boundary constraint. Hence, we will then explore how the 3 transition constraints enforce these remaining 7 equations.

Notice that we can rewrite the 7 equations in terms of one another:

l(1)=ρ01ρ0l(0)

l(3)=ρ01ρ0l(2)

l(5)=ρ01ρ0l(4)

l(7)=ρ01ρ0l(6)

l(2)=ρ11ρ1l(0)

l(6)=ρ11ρ1l(4)

l(4)=ρ21ρ2l(0)

Note that there are more than one way to write these constraints; any two rows can be written in terms of one another if their index differs by 1 bit (i.e. they have a Hamming distance of 1). We chose this way specifically to serve the rest of the argument.

Recall the following key identity used in STARKs:

xn1=i=0n1(xgi).

To make a long story short, if the enforcement domain of a transition constraint is

xn1, then the transition constraint applies to the domain points
{g0,g1,...,gn1}
.

Note that the use of varying length enforcement domains is the key idea that enables us to enforce the

n equations using
logn
transition constraints.

As a reminder the transition constraint formula is as follows (rewritten slightly for readability). For

κ{1,...,μ},

l(g2μκx)=ρμκ1ρμκl(x)

for

x{g0,...,g2κ1}.

Let's build our intuition of why this works by going back to our

μ=3 example. We have 3 constraints over the following domains:

κ=1{g0},κ=2{g0,g4},κ=3{g0,g2,g4,g6}

Let's now evaluate the transition constraint formula for

κ=1, where the enforcement domain is
{g0}
. If we plug in to the formula
x=g0
and
κ=1
, we get

l(4)=ρ21ρ2l(0)

Notice that this is the 7th equation defined previously!

For

κ=2, the enforcement domain is
{g0,g4}
. If we plug
x=g0
and
κ=2
in the formula, we get

l(2)=ρ11ρ1l(0)

and with

x=g4, we get

l(6)=ρ11ρ1l(4)

our 5th and 6th equations!

For

κ=2, the enforcement domain is
{g0,g2,g4,g6}
; we leave it as an exercise to show that we recover the remaining 4 equations.

The
s
column constraints

The

s column has no boundary constraint - everything is encoded in the transition constraint. As for the transition constraint, it is unlike traditional transition constraints in that its enforcement domain is the entire
G
. That is, we can think of the transition constraint as "wrapping around" from
gn1
back to
g0
.

The transition constraint is as follows:

s(i)=s(i1)σn+j=0m1αjfj(i)

If we look back at how the

s column was built, you should verify that the constraint holds over all pairs subsequent rows. Specifically, referring back to the example
s
column
, you should verify that

s(0)=s(7)σn+j=0m1αjfj(0)

Conclusion

This article is the conclusion of the book! Hopefully, you are now better equipped to understand how to offload the proving of LogUp to GKR.

If you've spotted a mistake, or something still isn't clear, please drop a comment directly in the note, or DM me on X. I will be happy to rework parts of the book.