ZK10: Varuna: Flexible zkSNARKs for generalized R1CS - Victor Sint Nicolaas

Transcript

Thank you. Do I have a clicker? Is that this thing? Nice. Uh thank you all for joining. Uh I'd love to talk with you about some of the work that we've done on the proof system of Aleo. Uh yeah, one of the big sponsors of this conference, which gave a very inspirational talk at the beginning of the day. I'm going to rewatch that. Um I am a protocol engineer at Aleo, and this is joint work with a number of other researchers mentioned here.

Alireza, Mary Maller, Michael Little in the audience if we have some questions for him later. And uh Petrus as well. Um Veruna is kind of a derivative of the Marlin proof system. Question for the audience. Who here has heard of Marlin? Cool. Who has like high-level decent understanding of how Marlin works? Cool. So, we're going to do a little bit of an intro, and I cannot go into like too much mathematical details. Also, I don't have time for that. But, I hope to give some kind of an impression of how we took our existing proof system and still, yeah, try to push the most performance out of it as possible.

Because we're hitting mainnet in, yeah, a couple months from now. So, there's no room anymore to re-architect everything. But, we have certain design criteria for what we want our proof system to do. We want very fast verification, very small proof size, and uh yeah, let's see how we get those properties. In the end, I'll also talk briefly about different constraint systems and how we can, yeah, kind of express all the constraints that we want also within a Marlin world. So, just to set the stage, what am I talking about when I'm talking about these proof systems?

We've seen many variations of this. I'll do my own. We have a prover and verifier, and the prover wants to prove knowledge of some theorem to the verifier by sending a number of messages, or if we compress them using polynomial commitment schemes, uh a single message at the end. Um what are the building blocks that these proofs are made of? Uh in our setting, specifically an interactive oracle proof and a polynomial commitment scheme. So, the interactive oracle proof uh allows us to represent a constraint system as polynomials, as you have maybe seen 20 times now in different talks.

And the polynomial commitment scheme allows us to um yeah, prove that this constraint system actually holds in a non-interactive way. Now, the one thing that I did not define yet is what is this constraint system? Uh an example that has been widely widely used as a constraint system is the rank one constraint system, where we define whatever computation you want to prove, whether it's your identity or your software program, and we're going to split that up into only addition and multiplication gates.

When preparing for this talk, I was actually very curious about the history of R1CS. So, I did what every good modern knowledge worker does. I went to ChatGPT and asked, "When was the first time when we started using R1CS?" If anybody has a good answer to this, I'd be very curious to hear it. And ChatGPT pointed me towards a paper from 2008 by Groth and Sahai, where they used quadratic relations between polynomials for the first time. And yeah, this is a very similar structure to R1CS. But anyway, we're using it now all over the place.

And uh yeah, it's an NP-complete language, so it can express a wide variety of statements. What does this R1CS thing actually look like? Well, there's three matrices, A, B, and C, of dimension R * C, which is my personal notation of saying we have a number of rows and we have a number of columns. Then we also have a vector Z, which is also called the witness vector or the assignment vector of uh degree C. So, that equals the number of columns. It's pretty abstract still, so let's create an example. Let's say we have a very very very tiny program of three variables, and I want to prove to you that I have knowledge of some

variables where variable one multiplied by variable two equals variable three. So, this is what the R1CS would look like for that. Um each matrix is going to have as many columns as there are variables. This is the same for all three matrices. Um and then we need to represent in these three matrices um which variables we're going to choose. So, for the A matrix, we're going to choose variable one once. For the B matrix, variable two once. And for the C matrix, variable three once.

And as you can see, something to keep in mind is that even though we have nine entries in this one row, in this one constraint, um there are only three non-zero entries. So, the non-zero entries might be a tiny fraction of actually the entire R1CS matrices. Uh one more definition to also keep in mind, I'm going to talk about assigned matrices later, and that happens when we kind of multiply the witness vector Z, or sometimes it's also called W, uh with these um R1CS matrices. So, if I say I'm going to actually instantiate these variables with real values, so 2 * 3 = 6 for example, then we would essentially get three

vectors of 2 0 0, 0 3 0, and 0 0 6. And if you want to like prove more constraints, or going to have a giant ZK VM at some point then obviously we can keep adding more rows, add more variables to prove. So, the proof system Marlin, the one that I'm talking about, specifically cares about optimizing having a constant verifier time, extremely fast, constant proof size, very small, and a universal setup. So, in order to get these benefits, we only had to do a setup once a number of years ago. Aleo has been around for 4 years now. I think these setup happened one or two years ago if I'm correct.

And we can keep using this for a large number of circuits and computations going forward. Now, many of the other proof systems that were presented today and that you read about have very awesome properties that maybe excel at some other dimensions, but often they're going to have a trade-off with some of the three that I care about here. So, yeah, just take that into account. In the end, I think many people agree there's not going to be one ZK-SNARK to rule them all, but for our setting, this really works. And why do we want these three properties? Because we have a blockchain and yeah, the idea when Aleo was designed 4 years ago using the base on the work of Zexe

zero-knowledge execution was to build a very scalable, very private blockchain that makes the most use of zero-knowledge proofs. So, instead of actually sending transaction through the network, everybody only sends proofs of transactions, and we want the state of the blockchain to just grow yeah, as slowly as possible. And for all the nodes in the network to be able to verify all the proofs extremely fast as well. Maybe one more criteria that we also really care about is simplicity and production readiness. So, yeah, there are certain custom proof systems that might be able to achieve these criteria, but maybe also introduce

extra complexity. So, this is why I do think that the work from Lasso and Jolt is very exciting that maybe it'll be able to standardize a lot of the lower level stuff, including a lot of the higher level stuff, and we only have to do a lot of work interpreting the middle layer. So, as a polynomial commitment scheme, we use KZG, and we use specifically univariate KZG because this is the one with the best proof time, sorry, proof size and verifier time. And the interactive article proof is kind of the main innovation that was introduced in the Marlin paper.

If you want to go more into detail, I can highly recommend these papers. I'll give you a high-level rundown of the strategy which we're pursuing. It's going to be three steps. First step, let's assume that the prover or sorry, let's assume that the verifier that we have three polynomials, ZA, ZB, and ZC. And that these represent the assigned matrices. So, that's what I mentioned before. That was if we want to do the computation 2 * 3 = 6, then the first polynomial on some subgroup in a univariate domain is going to evaluate to 200. The second polynomial ZB is

going to evaluate to 030, and the third one is going to evaluate to 006 on this small domain. If we assume that we have access to these polynomials, we can very efficiently check that this indeed equals to zero in some domain by giving to the verifier something called the quotient polynomial. In the second step, we're no longer going to assume that we actually have these polynomials. The prover is going to have to prove to the verifier actually these assigned matrices is a multiplication of the assignment vector which evaluates to 2, 3, and six. And the three different uh uh matrix uh matrix matrices. So, the second step, we

obviously would have to do three times for the three different R1CS matrices. Um how does the verifier get access to the Z polynomial? Very easy, using a polynomial commitment. How does the verifier get access to the matrix polynomial? Very difficult because matrices can grow pretty big. And if you would do uh a polynomial commitment of the matrix, or if you would represent the matrix as a polynomial, then that polynomial is growing the is going to grow in the degree of the number of constraints and the number of variables.

So, this quadratic blow-up can get pretty nasty at some scale. So, one of the main main innovations of Marlin is that they introduce some kind of preprocessing. And there is a third step where actually the prover is going to prove to the verifier, my matrix polynomial is some linear combination of these preprocessed polynomial. It's also why in the title of the Marlin paper, it uses the word preprocessing. They call it holography, very cool word. Uh because they kind of project the two-dimensional matrix into a one-dimensional vector of only the nonzero entries.

So, remember that I talked before about the nonzero entries? There were only three of them in total. So, actually instead of representing the three matrices as three joint polynomials, we're going to end up with nine degree one polynomials. So, yeah. It's asymptotically a lot better. And this is also what we use in production. So, we first have to make some kind of proving keys. We represent the polynomials. Uh we represent these matrices in a more succinct way. And using that extra preprocessed information, uh yeah, the verifier is going to have a much better time verifying everything. And the prover is going to have a better time proving everything.

And the prover time that we end up with is bounded by the degree R, the number of rows, and the degree K, which is the number of non-zero entries in these matrices. A lot of math. So, that is Marlin. So, how where do we go from here? What techniques do we have in the back to kind of improve this particular proof system without yeah, relinquishing or getting rid of these benefits that we talked about in the beginning? Well, we've been working with a number of co-authors on something called Veruna, flexible ZK-SNARKs for generalized R1CS.

And the first main improvement is that we can expand the number of constraints that we can represent. Instead of being just R1CS constraints, where we flatten our computation to only addition and multiplication gates, we can now represent custom constraints, lookup arguments, or let's say that I have not three matrices, but 100 matrices. Because for particular gadgets, for proving particular statements, they actually there are efficiency benefits to be gained from this. If anybody is curious to look yeah, at a gadget which takes this to the extreme, the Sinsemilla hash function from Zcash, they use like I think six custom gates of like pretty

high degree up to seven. So, it's pretty fascinating and maybe we'll integrate that at some point. So, in the first step, we're going to say we want to prove that some polynomial equals zero. Which could be the R1 linear combination of R1CS, but it could also be yeah, any other combination of assigned matrices, vectors. Second step stays the same. For any number of matrices that we have, we need to prove that they the assignment matrix equals the assignment times the matrix. And the third step stays the same as well.

And yeah, I guess minor but interesting technical detail is that the three steps are kind of more modularized and completely separated. So, the first step scales with the degree of constraints, the second step with the number of variables, and the third step still with the number of non-zero entries. But, there's more. This custom constraints yeah, it's really about more programmability so to say and for very specific gadgets, we can gain more scalability.

But, we want to gain more yeah, a better prover time for like any statement so to say. And the trick that we use to achieve that is by using every cryptographer's favorite trick, linear combinations. And it's really a simple if the circuits are the same, what we can do is just yeah, multiply the polynomial in step one by a random challenge. We aggregate those all up. And this really gives us very, very good scaling because we only have to do the first step basically for all the different uh uh circuits or for all the different statements. And step two and step three,

because we're using exactly the same computation which we're representing, uh can stay the same. So, as a concrete example, it's a little bit small here, but for a single proof here, I'm taking 50 milliseconds. And if I'm doing 32 proofs, it's going to be only three around 300 milliseconds. So, that's a five times improvement or if I want to make that sound more exciting, 500% improvement. And it is pretty significant. Um something to take into account there as well is that uh yeah, hidden in the Zcash paper, we also want to support some kind of delegation where if the proof is really big, then the prover could potentially

delegate this to other people. There's a number of people in the Aleo ecosystem working on this, so that if you're on your phone and you want to make some kind of proof that you could delegate it out. And the fact that all these statements can be batched together really allows delegable proving to be done a lot faster for a very large amount of statements for potentially also different parties. Um there's one more level of batching that we can do. The last level of batching was very similar to a paper called A Plonk. Um but we also want to support batching for circuits of different sizes.

And there's one extra technicality that comes into this. Um if we have completely different circuits, we do actually have to do all the three steps for the different circuits, but we can yeah, kind of batch together all the different operations. And we need to introduce something called as a valuer. Uh we need to introduce a selector polynomial. So that um if the polynomial representing the constraints from one circuit live in a small domain because maybe they only have like 10 uh constraints and the polynomial of a different uh circuits consists of like a hundred uh degree a hundred, then we

actually need to kind of lift the smaller polynomial and represent it as a bigger polynomial. And what this gives us is that if you want to batch uh multiple you want to prove 10 statements together where the statements are of different sizes, then effectively we can drop the cost of the smaller circuit because the like the thing that kind of determines the cost of these proofs is the degree uh of these polynomials. So the smaller circuits is far away and yeah, this is really nice.

And there's one more extra uh that we recently have been like tinkering about. It's not in the code base actually. But the interesting thing is that the first step grows with the degree of the matrix. So if we have a million constraints, it's going to be very big. What we could theoretically do is cut up those R1CS matrices and pretend that they are thinner R1CS matrices with less constraints, but we're going to have more of them.

And turns out we can make this interesting trade-off between proof size and prover time whereby we can double the speed or we can just increase the speed of the prover by growing our proof size. Now obviously in the beginning I said we don't want to have a very big proof size with a proof system. So we might gain a little bit of benefit from this, but you can also see that if we're going to have a 1 GB proof size, probably by that time you want to use a different proof system. And then final topic that I wanted to talk about is how do we want to represent our constraints in a yeah kind of fashion that is reusable, that allows us to formally verify those constraints, that

potentially allows us to reuse all the formal verification across projects as well. This is a big topic that we've been thinking about because yeah, we are going into production soon and we cannot yeah safety is really important for us. We spend a lot of time and effort into this formal verification formal verification. And yet we also want to support the cool things that Plonk-like systems have regarding custom gates. The problem is I've heard a lot of complaints already in the last couple hours about all the different Halo 2 libraries that exist right now and all the different ways that we can describe custom gates. So is there a way that we can find some unified way

to represent these? Some of this formal verification work has been done by the way by the Caster Institute. So, if anybody is interested to yeah, learn more about how that's done, do check them out. I'm going to rush through this cuz I have a couple more minutes, but I want to briefly explain how do we express custom constraints in our proof system. So, above you see R1CS. As I mentioned all the way in the beginning with three matrices and assignment vector and we want this linear combination to equate to zero. A popular construction or formula that was I think came out this year and of last year.

It's customizable constraint systems where basically they say instead of doing three matrices, let's have as many matrices as we want and we want some linear combination between these matrices to equal to zero. And this actually allows you to yeah, express your computation not just in addition and multiplication gates, but a lot of different like type of arithmetic gates. We have a different construction which we call generalized R1CS, which is extremely similar because mathematically it's actually the same. Um and we also have a larger number of matrices and we want to have some local predicate that equals to zero or that holds over these matrices.

And you might wonder why different name and why a different construction? Because we've already been yeah, tinkering on this for a while before CCS came out and I think it's actually very logical name because it pays homage to the fact that the lowest common denominator or the primitives that we use are still R1CS matrices. We still have these sets of constraints kind of. We can just combine them in different ways to gain more expressivity. Um instead of using all these little indices, we can also discard them just for simplicity for now and say we're going to iterate over sets of matrices and then yeah, looks a little bit cleaner.

So I'll very briefly mention how these two kind of notations compare and yeah, I'd be very excited to discuss with anyone afterwards on yeah, what the right notations are. Like what could basically help us gain the best insight into making these systems. So R1CS for example is very simple in both for CCS we describe these A, B and C matrices and how they relate to each other AB minus C. In generalized R1CS we would separately indicate okay, we have a certain vector of matrices assigned witness matrices the first one, second one and the third one and then we have some local

predicate that we want to hold AB minus C equals zero. So far so good. What happens if we want to have expressed two different constraints then CCS becomes a little bit hairy actually. Because these matrices suddenly have to be subdivided into other matrices but it kind of works and in our scenario I think it's a little bit cleaner notation because we say okay, we have four matrices and we want some local predicate to hold over the first three and another local predicate to hold over the fourth matrix. For example, this one does AB minus C equals zero R1CS plus D squared equals zero for some other matrix.

The biggest difference is perhaps when we add lookups into the equation literally because CCS is not directly supported in the appendix of the paper they say actually if you want to have lookups go into CCS plus and for some set of the witness vector we want to guarantee that these witnesses or sorry, these entries are in the table. So we're kind of expanding the definition there and it means that we can't use CCS in a black box way whereas within our definition, we can because if we say we want some assigned matrix to be included in a table, we can just

indicate that there is one matrix and that this local predicate holds for that particular matrix. So this little A here is our assigned matrix and the rest is basically the logarithmic derivative base local argument from Havoc. So I think that covered yeah. Not everything but a good part of the construction that we built. And yeah, I'm still figuring out trying to wrap my head around how to also look into recent work from Havoc and other author.

How would you express GKR based subcomponents into these customizable constraints? How do you translate from multivariate to univariate polynomials? There is a mapping but yeah, can you maybe express that in a clean way? And yeah, I'm really looking forward to straightening that out over the next year and yeah, making kind of a clear documentation standard on how we can use these constraints. Thank you. Thank you so much. And we have a few minutes for questions.

Does anyone have questions? I should add that all of this like everything people are doing here is open source so in the corner is the library where all of this lives, SnarkVM. Did you invent your own .r1cs file format or did you use someone else's? I mean you can't export our .r1cs so we don't even have a file format. We do have some kind of abstraction over it which you're welcome to learn if you want to.

Any other questions? Can we get some proof of life? Some woos. All right.