ZK14 - SNARKs for Integers with Low Overhead - Lucas Xia (NYU)

Transcript

So, today I'm going to be presenting a new construction for SNARKs for integers. And in particular, this is going to be with low overhead. And then I'll more properly define what SNARKs for integers is and also what low overhead is. But yeah. So, I'm going to skip over what a SNARK is. Hopefully, everyone knows what that is by now. Um but to recap some of the applications that we might want to use a SNARK for, like for example, you can prove RSA verification, hash functions, you know, CPU executions, SNARK recursion, or some combination of these.

And when we think about what happens when we, you know, start with an application that might be in some sort of like program form, and um for a SNARK, we need to be able to arithmetize that into a circuit format. And I want to point out in particular that a lot of these SNARK constructions involve picking a specific field F. Right? Usually, this is due to some cryptographic reason. There's other reasons for this, but some F is chosen. Um and usually, this has prime size or characteristic.

So, why did I want to point this out? Well, the question is like how do you write these programs, like these RSA verifications or hash functions, in such a way that is, you know, in this particular field encoding? So, how do we do this step without blowing up the circuit size? Right? That's the non-native arithmetic problem. Um and this is kind of like a very prevalent problem that a lot of applications run into. And one approach that people have used in the past, um and I'm going to classify them under what I call circuit tricks.

This is like basically trying to optimize the circuit to use less constraints, right? So, there's a lot of these like limb decomposition tricks where you sort of take each limb and multiply it individually. Um, there's like usages of the Chinese remainder theorem to try to like use smaller modulus. Um, and there's like a whole bunch of tricks like these. Um, unfortunately, a lot of these can sort of encounter similar issues, okay? And most of these issues are from a lot of the sort of intermediate costs that come from like limb-by-limb decomposition. You need to have like intermediate sort of values that come from each limb product.

Um, and this sort of directly translates into a large commitment overhead, right? If your circuit is like a 100x or 1,000x what it should be, then you're going to be committing to and doing like large cryptographic operations for 100x, 1,000x what you, you know, theoretically could could do. And maybe more importantly, this often leads um, these circuit tricks often lead to like high complexity. And it pushes sort of the burden on the circuit writers.

And in particular, this leads to soundness bugs or other kinds of bugs. Um, and here's one example. Not trying to shout out my former employer, but um, they paid out a bug of like $500,000 uh, due to some non-native arithmetic um, bug that they had. So, today I want to sort of lead you away from these sort of like circuit tricks into maybe a more natural encoding of things. So, today I'm going to talk about like things in the frame of R1CS. Hopefully, people are familiar with this. This is just a way to sort of write circuits and it has this form of like AZ * BZ is CZ.

Right, and here's an example circuit where we're doing this limb by limb sort of product. Um However, like what if we had like a more natural way of encoding these? Okay, so here is the R1CS relation written in a maybe more natural way, right? We have this like mods and quotients thing. And now you can imagine like if you want to do a modular uh multiplication, you know, you can just like write this as like one constraint now, right? So like sort of the the quotient is eating up a lot of the complexity.

But if you want to multiply val1 and val2, you get result um which is the, you know, result mod n. And this is like one constraint, right? It's like very clean. Like you don't have to do any sort of like limb decomposition into sort of recombining the limbs and all that. However, it comes with a caveat. Um where previously we could use a field we can't really use a field here, and why? If we do this over a field, like the quotients always has a solution pretty much, right? So like if we had an incorrect equation um we could sort of fix it. Like a malicious prover could like solve for quotients

and and prove something that's incorrect. Um And a natural way of preventing this is to prove things over the integers instead, right? Because over the integers there's no inverses besides one and negative one, right? You can't just prove two is equal to four because you can't invert two. Um Right, so that that's sort of like the motivation for why we we might want to prove over something that's not a field, like the integers. So that leads me into this sort of recent paradigm um SNARKs for integers. And here I'm going to give a overview of sort of the the history of it, the very recent history. So, the first work in 2024 is Groth16.

They gave a construction for SNARKs for integers. Um but the problem with it is that it was based on DARK. Um and the the bad part here is that it uses like these groups of unknown order. And in in practice, groups of unknown order are extremely inefficient because they usually involve uh like several thousand bits, like fields of several thousand bits. Um and you don't want to be doing a lot of operations with several thousand bits, you know, repeatedly. Um in a follow-up work called Zinc, they built a a PCS that that's based on breakdown.

And this is sort of like a mitigation to the original problem because based on breakdown, you know, you're not working over groups of order of unknown order. It's like a hash-based scheme, right? So, uh they solved the problem of like trying to get your commitment overhead low. So, like the prover cost is a lot lower in Zinc. However, their verifier cost is um prohibitively high. Like breakdown introduces like the square root size proof size and verifier cost. And they're also they end up being linear in like the number of bits of your witness, which in practice just translates to something that's just like unusable for the verification.

So, in a more recent work that's also concurrent with ours, they sort of try to solve this problem by making the PCS more agnostic. All right. So, we want to be able to use any of the new fun like PCSs that people are constructing. And in particular, their requirement is that they they need the characteristic of the field to be exponential size. So, like while it's still while it's agnostic, there's still like a requirement here. And maybe the the more important part is here is that um their witness needs to be in bit form, so it introduces a lot more commitment overheaded here.

Um but they do solve the the verifier problem in their you know, logarithmic. And today I want to present our work, which is sort of the best of all these worlds. First of all, like the characteristic of the field only needs to be lambda squared size, like O lambda squared. No long like no longer an exponential size. And we'll see this later uh when I show the parameters. The commitment overhead is also um like optimal in terms of like multiplicative overhead. We only introduce a sublinear amount of extra commitment.

And lastly, we maintain um the logarithmic complexity of the verifier. So this is sort of a summary of of what we're achieving. Yeah. Mhm. Yeah, sorry. I I meant the commitment over commitment overhead as outside of just the witness. So you do you still have to commit to the witness. I'm just saying beyond the witness in terms of extra commitments.

So actually, we commit to the the witness in limb form if you're worried about that. Oh, so you're So the range check. Yeah, so the range check might introduce overheads depending on which range check you use. Right, but if you use a range check that doesn't have commitment overhead, you know, it's not going to cost anything extra. Okay. Yeah. Okay, so back to the the thing that we're trying to achieve, right? We have this modular um RNCs. And we're trying to do this over the integers right?

So, the main trick that pretty much everyone has used is the power of randomness. And essentially what this means is that instead of proving over the integers, we can instead maybe try to prove over a randomly selected prime P. Okay, so why is this great? So, one uh if something is true over the integers, then obviously it's going to be true mod a random prime, right? But the even better thing is that in the reverse direction if you prove something is true over this random prime it ends up being true that it's also true of the integers.

Um you know, with high probability. And the intuition for this is that uh for example, if I'm malicious if I'm a malicious prover and I'm trying to prove that 10 is 25 then this only works if I pick the prime to be three and five and sort of any other prime I would be trying to prove a wrong thing. Okay, so the soundness of of going from the bottom to the top is is almost one. It's like as long as you don't pick one of those few sort of bad random primes. Okay, great. So, now the problem is how do we prove over this random prime?

Okay? Um and this might not be um that easy to do like yeah, we'll figure it out. Okay? So, so let's think about how we construct a SNARK, right? So the the standard recipe for this is to build like a PIOP and a PCS. So, if we think about the PIOP, right? We need to build this PIOP for our NCS over a random prime P now. Okay? And it turns out that a lot of these PIOPs that sort of exist like Spartan or you know, Hyperplonk for a different arithmetization, they already kind of work over this. And and the reason why is like if you just think about like what Spartan does, it does like a bunch of sum checks.

And here we're just doing sum checks over FP instead of the original the original field FQ. All right so so these sum checks just like work as they're supposed to. And there's not really any issues here. Um because we don't have like a strict requirement on what P needs to be, right? So the other part of this is that we need a polynomial commitment scheme, right? And the problem here is that it needs to be relative to this random prime P. So why is this a why is this an issue?

Like the core issue here is that P is sampled after commitment, right? We've committed to the witness. We need to now open it mod a random prime. And if you think about how normal polynomial commitments work, they open to like mod their chosen field, right? Like they open a field element in FQ, not FP. So to illustrate this point a little a little bit more, I'm going to sort of define what a PCS is again. And here we're going to only work with multilinear PCSs. This ends up being kind of important for our construction, but people are very happy with multilinears.

Um so again, there's like a setup and there's a commitment phase uh or commitment algorithm, and this, you know, generates a commitment. And in general, like Z is committed to in some FQ, right? Like the field FQ is chosen during one of these two phases. Like in the KZG, it might be in the setup. In a lot of hash-based schemes, you're picking the field, you know, when you pick the code. Um but yeah, like pretty much all PCSs will pick this FQ during one of these two phases. And then lastly, we have this like evaluation function, which generates the proof of opening this polynomial.

The problem is that you know, we can't work with this standard algorithm anymore, right? This opens Z of R is equal to Y mod Q. Um we actually need something of this form, right? We need we need a function called mod eval that actually opens mod P. Okay. So, our protocol, which we're calling the integer evaluation protocol, solves this goal. So, to reiterate, we need to um like given this multilinear polynomial F with little n variables committed to an FQ, we want to prove a mod P evaluation.

Um our protocol does something actually slightly harder. So, we actually prove an integer evaluation. Um and the reason why this is harder is that like you know, once you have an integer evaluation, you just get the mod P evaluation by default, right? You can just take it mod P. Um but that's the difference in our protocol. And I'm going to keep a running example. So, we have uh little n to be 20. We have this bound on F, which I'll talk about a little bit later, but it's 32 bits.

Lambda being 128, P being 128 bits. And we have R, the challenge, being sampled from ZP. And we have this multilinear polynomial F. Okay? So, let's consider maybe like a straw man case. So, what if Q is like really, really big? Okay? Then, if we just evaluate the polynomial like in its normal eval function, right? That just sort of gives us the integer evaluation, right? If nothing overflows, like we can just like take the evaluation uh mod Q, and since it's not bigger than Q, it's just also the integer evaluation.

Right? And that's like so like are we done? Right? Like if Q is large enough, then we're done, right? Um we're not done. Not done yet. The problem here is that like even in our example, if you think about how big this evaluation is, right? There's 2 to the n terms. Each one has like this coefficient and also the EQ polynomial. And if you think about how big this sum is, it's quite large, right? There's this EQ, which is like the challenge raised to the little n the power.

Um so there's this P to the n term. And based on the parameters that I set, you know, this already is like humongous. It's 2,600 bits. Right? So we can't pick Q to be 2,600 bits unless you want something to be really inefficient, which defeats the whole point. But, you know, this gives us a new goal to achieve. If we can reduce the norm in some way enough, then like we can just use the original eval function to open things mod like over the integers, you know, as long as things don't overflow Q.

So, our first idea is to use the Chinese remainder theorem. And the reason why the Chinese remainder theorem Well, I Let me explain what it is first. So the Chinese remainder theorem basically says that you can prove something like over a large modulus over the integers and it's equivalent to proving it over a bunch of small prime moduli. So for example, like if you want to prove something is equivalent mod 30, you can also prove it just mod 2, mod 3, and 5. Right? And that sort of implies that it's also equivalent mod 30.

And the power of CRT here is that it actually helps us drastically reduce the norm. And the reason is that if we think about things mod this smaller moduli MI, right? We can take everything mod MI. So the evaluation point can also be taken mod MI. And in our example, that's really powerful because let's say MI is like 2 to the 30 bits now. We have a bunch of like these 230 2 to the 30 bit um MIs. Now our evaluation is only based on MI instead of P, right?

Um and in the example that's only 650 bits. So it's like way better than what we had before. Um but it's still not good enough. Um but it it is way better. Okay. So one question is like how many MIs do we need right for the CRT? So in in normally like normally as I said before, you need the product of the MIs to be bigger than the integer evaluation. So in our case that ends up being 900 in this example, which is pretty high. However, we can again use the power randomness if we sample these MIs randomly.

Um this gives a lot gives us a lot of power, right? Then like you end up only needing like a logarithmic amount of them. In our example that ends up being less than 10. So yeah, so instead of a 900 X and sort of like prover cost, it's it's something more manageable. It's like less than 10. Okay. So to Yeah, so this is like where we are right now at 650 bits. Our second idea is to partially evaluate, right? So what I mean by partially evaluate is that instead of evaluating all N variables, what if we just only did like some of them at a time?

So here I'm evaluating the last K variables, right? And the reason why this is great is because if you look at the top expression, there's this like 2 to the N MI to the N term, and that's sort of killing us, right? Because N is 20, uh you know, it like blows it up a lot. If we just partially evaluate it, right? Then it's only based on K. Um and K is a parameter that we can sort of pick. Right? So let's say we've picked K to be seven. Then the the norm of this even like partial evaluation is already like a manageable number.

Um it's only 250 bits and already a lot of these PCSs use 250-bit primes, right? Elliptic curve ones, even hash-based ones can use 256-bit primes. So, this is already good enough. Um but the first thing is that we can pick K to be even smaller. So, this is how we get uh the the the PCSs that use like 64-bit primes, this is how we um allow for those. Uh but the other thing to note here is that this partially evaluated polynomial is also kind of like exponentially smaller in K, right? So, like once you partially evaluate K variables,

there's two to the K less terms. Um and then that like the norm also blows up slightly, but but only linear in K. All right, so this new polynomial is actually a lot smaller. Um so, it helps us like maybe if we iterate on this, you know, we can work with something a lot smaller. Um but there's a problem here, right? So, once we've partially evaluated, the norm is already kind of like as big as Q or it's like much larger than before. So, like you can't just continue partially evaluating, right? That would That would blow up the norm again. Um so we we've come up with an idea. It's kind of a simple idea where we decompose

Oh. Too far. Where we decompose Let me go back. the polynomial into its like mod MI remainder and quotient. So, this is kind of like a the most natural idea you can come up with, right? We only care about the evaluation mod MI. And we're just sort of splitting it into its remainder and quotient form. And the important thing to note here is that like f of like the partial value of f and a agree mod mi. So, why is this great? We can just recursively iterate on a of x now.

And remember a of x has a small norm, right? Because we've taken out anything bigger than mi. Okay. So, let's say we just continue doing like the partial evaluation stuff. Eventually, we get down to a base case. Here it's just simple, you know, if there's less than k variables. Now, we can just evaluate it directly, right? And get the get the result. Um and we need to check that it's equal to the claimed evaluation mod m. Um so, that that part is simple. So, this is like a brief sort of big picture view at our protocol. We have this m different or like a bunch of different mis that we're evaluating over, and then

we're repeatedly, recursively partially evaluating and decomposing until we get down to one thing. So, it's worth noting here that like a lot of the extra commitment overhead happens, you know, below the initial witness, so we're committing to these polynomials. But as I said, they're like exponentially smaller in k. Right? So, the sum of them actually isn't isn't too big. And we can see that in the next slide. So, here are some like parameters that we've calculated that work for our scheme. Um the first three rows in the left side are for different choices of k. So, like when k is a little bit smaller, you know, we have we need less little ms or like m mis, uh but the commitment cost is a little

higher. But we can select a k such that you know, the commitment cost is like basically negligible um at the cost of more field work. So, s here is what? s is the number of small moduli, like MIs, that we needed for the CRT. So, where that matters is on the right side, the the amount of field work that the prover does is linear in in S. Wait, just a quick question. So, this SM is actually SM by some tropical numbers. So, we don't have S subchecks.

There are S subchecks, yeah. Wait, what do you mean? There will be S different subchecks, no? Uh there's no subchecks here. >> They're just evaluations. Yeah, it's just evaluations. Yeah. Yeah. Um and the other thing I want to point out is that if you make Q really small, so our scheme works by by picking like an even smaller K. Um but the problem here is that now the the partial evaluations are like a little bit bigger, so we need to commit to more stuff here. So, in this case it's like 16x the original witness size.

Um and other important parts here, like the prover size and verifier work are also pretty small. Um and I here I want to tie a couple of loose ends here. I'm going to hand wave a little bit. Um there's a couple of things, right? One, we need to actually commit to integers, as I said before. And the second is that we need to actually support the the low norm F. Like remember in the example I had F to be less than 2 to 32. Fortunately, both of these are solved by the same method, which is by limb splitting. And this is like a you know, common solution.

And the reason why limb splitting isn't too bad, so I made the the relation a a lot uglier, but um don't be scared by it. It's really just like we've added this structured limb vector in, and we're sort of like multiplying multiplying it out with the limbs. Um and the reason why this is like not too bad is if we use like a sumcheck based PIP, it ends up being just like a few more variables in the sum itself, right? Like we can multiply out the limbs with the limb polynomial in the sum tricks itself, and it won't cost us like really that much more cuz it's so structured.

Okay. And that brings us basically to the end, you know, we construct a SNARK for integers as low prover overhead. It compiles from sort of any PCS, and it maintains a fast verifier that's logarithmic. And this is great because, you know, it gives us sort of a method to approach non-native arithmetic that's more and more natural and like maybe less bug prone. Okay, thank you. >> [applause] >> Okay, let's take only one question.

Do you have some concrete like performance examples? Uh we're still in the middle of implementing, which is unfortunately why the the paper isn't on ePrint Yeah. >> Okay. Yeah, I was about to ask if it was on ePrint as well. Yeah, sorry. Yeah, unfortunately it's not yet, but we're hoping it'll be on like soon, like really soon. Yeah. Yep. Thanks a lot. Really cool work. Thank you very much. We're going to switch to the >> [applause] >> Thanks, Lucas.