ZK13: Almost Linear Time Permutation Check - Jessica Chen (New York University)

Transcript

[Music] Um, thanks for everyone for coming. Today I'll be talking about a way to do almost linear time permutation check. This is joint work with Bendic Bones and Zachary Dafano at NYU. So let's start by looking at the definition of permutation check. It states that given polomials f and g their outputs are permutations of each other. if and only if there exists a polomial sigma mapping between the same a boolean hyper cube of the same dimension such that f of sigma of x is equal to g ofx over the boolean hyper cube. So let's look at in a quick

example throughout this talk I will use mu to represent the dimension of the boolean hyper cube we're working with and n equals to 2 to the mu to represent the number of elements in the permutation. So suppose mu is equal to two and therefore n is equal to four and suppose we're given f such that its outputs over the building hyper cube are 77 96 91 and 28. Now we're also given g with outputs 96 28 97 and 77 uh sorry 91 and 77 over the boolean hyper cube. We can see that the blocks of the same color uh hold the same values. So f and g are indeed permutations of each other. This

implies that there exists a permutation polomial sigma which maps from the indices on the g table to the corresponding indices uh of the same color blocks on the f table such that f of sigma is equal to g uh on all four of these indices. Okay. So that is the basic permutation check formulation. There is also a closely related formulation called the prescribed permutation check for which we need to prove that the equality holds for a specific permutation polomial sigma.

This requires proving that a provided permutation polomial actually maps to zeros and ones. Uh and this can be done by using an additional sum check on top of the proving scheme for the basic permutation check. We will not have time to go into the details of this today. So for today we will only focus on the basic permutation check assuming the permutation polinomial sigma is precomputed and committed to. Okay. Why do we care about permutation check? Well perm check is at the heart of proof systems in circuits particularly we need to prove the correctness of wiring. In other words the prover needs to show that the inputs to each gate are indeed the outputs of the correct gates from the previous

layer. This is proved using permutation check with a premputed uh permutation polomial. So the wiring or the permutation polomial is committed to as part of the circuit description and then we perform a perm check to show that the inputs and outputs of the gates are consistent with the committed wiring. Besides circuits, perm check also has applications in memory checking where we prove all the reads and writes are consistent. In the classic offline memory checking idea, we compile the list of reads and writes by doing read before write and write after read. And in the end, we do a perm check to prove that the initial state and the read list together is a permutation of the right

list and the final state. Permutation check is also highly related to lookup arguments. Here we have the basic permutation check formulation and all we need to change to turn this into a a formulation for lookups is to replace the sigma with a lookup polomial row that now maps from one hyper cube to another hyper cube of different dimension. Then in a formulation f will represent the lookup table and g will represent the witness vector. Lookup arguments are also used for proving machine computations. For example, jolt used lasso and proves for deep thought used

logup. So how was a permutation check previously done? Well, the most common way is to reduce it to a univari product check will prove that the product of f ofx plus a random value is equal to the product of g of x plus a random value over the boolean hyper cube. This is equivalent to saying that a product of these fractions is equal to one. When the product check is instantiated, the variable is replaced by some random challenge r. The product check requires linear commitments and has a soundness error of n over the field size. Well, this is because to prove it, we need to commit to all n

partial products and show correct composition and equivalence. What this means is that uh let's call the k partial product pp of k. It is the product of the these fractions from x equal to all zeros to x equal to k. And the prover will use a zero test to show that the nth partial product is one and every intermediate partial product is indeed the previous partial product times the k fraction. Notice that because the random challenge R is field size which means lambda bits the partial products are also lambda bit long. So committing to them and is expensive and can be wasteful because we always need to commit to a total

of we always need to commit to a total of n lambda bit elements. Even if the the outputs of f and g which comprise a witness is much smaller than lambda bit lambda is required to be at least 256 under discrete logarithm assumption and at least 120 in hashbased systems. So for example, say all the table entries, the outputs of FNG are only 32-bit long, but we are using a 256-bit field. Then committing to these partial products incurs an eight times overhead. There was work in 2020 called Quorks which also reduces perm check to

product check but uses multilinear polomials instead of univari ones. And in 2022, Haboc introduced an alternative way uh largely known as logup to perform permutation check by using the logarithm derivatives of product check. However, in all of these works, the linear wasteful commitment cost and the n over field size soundness error persist. A quick note that a previously mentioned wasteful uh commitment cost can be saved by using GKR because GKR allows us to only commit to the inputs and outputs and not any of the intermediate values.

However, using GKR requires log and rounds of sum. This leads to worse verifier time, worse proof size and worse soundness and is certainly too large to be put on the blockchain. Moreover, GKR is expensive for recursion and parallelism. Um, and there is also a recent attack against the fear shmeirre soundness of convoluted GKR circuit which even though it does not break the affforementioned solutions to permutation check still cautions against applying fashionir to deep GKR circuits. Okay. So what did we manage to achieve? I'll introduce a way to perform permutation check using only two rounds of sum check. We have better soundness

than previous permutation checks. Our soundness error is only poly log n over the field size. The commitment cost uh is the cost of committing to the witness plus the opening cost of the polomial commitments. So we do require using polomial commitment schemes with sublinear opening cost such as kh or dory. The total number of field operations done by the prover is asymtoic to n log log n uh hence the title almost linear time. The verifier cost and the proof size are both logarithmic and the resulting permutation check can be used to replace any existing permutation check and can also be extended to

lookups. All right, now let's dive into the details of our solution. In 2022, Hyperplunk introduced a way to reduce permutation check to sum check but has undesired proof cost. We will start from that. So first let's look at the naive formulation of permutation check. We observe that this term on the left is quadratic. So we can move it out of f by using a simple multilinear extension. And since sigma is a permutation, sigma is injective and therefore invertible. So it is equivalent to writing eqx comma sigma of inverse of y. Now observe that the left side of the

equality is degree mu in x and the right side is also degree mu in x. Since they are both multilinear in x then they must be the same polomial if they agree over the entire boolean hyper cube. This implies we can apply short zipple to test whether the left and the right hand side are the same polomial by using a random challenge alpha. Okay, so we can run some check to do this. The problem with efficiency is that this EQ term here is a big product of mu bitwise

eqs which means it is degree mu in each bit of y and the sum check costs all n times log squar n field multiplications. This is where hyperplong stopped in 2022 and we will continue. So our idea is that take the first round of sum check for example. We could compute all the possible polomials EQ can take on. So suppose we call them EQ1 EQ2 etc. We can flip the sum. So instead of summing over instead of summing up the f polomials

within each bucket of e sorry so instead of summing up um in this fashion we can sum up each f polomial within each bucket of eq and then multiply with the corresponding eqi. Then the number of field multiplications only depend on the total number of buckets. So the total number by the total number of buckets I mean the total number of distinct polomials EQ can take on and the degree of each eqi. This trick would be great if the total number of buckets is sublinear. So let's look at how many

buckets there actually are. Observe that the sigma inverse in the first round of sum check must be among one of the four polomials. It can be zero or one or y or one minus y and that's it because it is degree one in capital y and it maps to zero or one. This implies that eq has 4 to the mu which is n squared total possibilities.

Well, unfortunately, this is obviously way too many buckets to work with uh because there are too many terms in the EQ product. It would be great if the product has fewer things. So, it say if the product only has P things, then the EQ only has four to the P possibilities. The solution then intuitively is to break the computation into chunks. Right now we have mu things multiplied together to yield this EQ term. We can break the big product into partial products each with fewer terms. So say we break them into L chunks. Then we multiply the terms the

mu over L terms in the first chunk into some middle value which we call mid one comma Y. And we do the same for all L chunks. So we have mid 2 comma y all the way to mid l comma y. Then we will multiply all the l chance together to yield the same eq term we had before. Since each mid is a product of only mu over l terms, they only have four to the mu over l possibilities in the first round of sum check.

So how many chunks do we actually need? What should the value of L be? Well, observe that as small as L equals to 3 already achieve sublinear number of buckets in the first round of sum check because 4 to the mu over 3 is equal to n to the 2/3. But unfortunately the solution is not that simple because the number of possible polomials sigma can take on increases exponentially with each sum check round. Specifically there are four to the k in the kth round which implies 4 to the k * mu over l for each chunk.

So after careful computation which I will skip today we found that we need l to be at least four log mu and hence the lo login factors in our proofer cost to put together we will use a mini two-layer GKR circuit to prove permutation check applying the bucketing trick in the process. The first layer computes the equivalence of the basic per permutation check except that um we buck um we put them into chunks instead of computing the entire uh eq product with mu terms. The second layer computes every mid for every y and the boolean hyper cube and every uh chunk. So for J

from one to L, each mid is a multilinear extension of the J's chunk, which means it's a product of mu over L terms. The resulting number of field operations is asymtoically and log n. Our solution can be extended to lockups lookups quite easily. But the challenge in applying the same trick to lookups is that the lookup polomial rule is not injective. which means we cannot simply write eqx comma row inverse of y like we did with sigma previously. So what we ended up doing is first we'll add an outer eq for x uh where t is the random challenge and then

essentially flip the summations and use a pseudo inverse. So instead of iterating over every Y in the hyper cube, we'll iterate over the images of RO and sum up all corresponding X that maps to the image. We'll run the naive sum check for the outer sum over Y and then apply apply the two-layer GKR trick with bucketing for the rest. The asymtoic cost is also on the order of N log N. So uh there are a few future directions. First of all obviously is to get the proveral cost down to actually linear field operations with very small constants while preserving soundness

verifier cost and proof size. As I was preparing these slides last week, we actually came up with a way um but puts extra restrictions on the PCS choice. We will also work on implementation and benchmarks and our paper will be out on errint soon. Thank you.