Unifying Succinct Arguments

Transcript

Yeah, ready to go? Cool. Hey everyone, welcome back from lunch. I'm Nico. I'm going to be talking about unifying succinct arguments. >> [snorts] >> And this is sort of the image that I sent to Justin sort of pitch like what the talk is about. I don't know if you're familiar with this like this analogy of the blind men and the elephant. They're all trying to figure out what it is and depending on what they touch, they see something else. So my claim is we're doing this right now with succinct arguments. The white I'm going to use the whiteboards in a minute. So yeah.

But don't worry, there's not that much important content on the slides. >> [snorts] >> So yeah, my claim is we're doing the same with succinct arguments. Some people talk about I don't know matrix vector products in Ligero or univariate polynomials in Fry or multilinear as in War or in Sum Check. At the end of the day, it's all the same. Wait, I'm going to use those in a minute. >> [laughter] >> Thanks. So [snorts] there's many works that point to this idea. This is not you know, I'm not the first one to say this. The main one is algebraic reductions of knowledge which itself is based or takes inspiration from the Sum Check arguments.

Bisford will tell you we're interleaving Fry and Sum Check. I'm saying you're all just doing the same thing. Zook is like the zero knowledge IOPPs. Has like a War Ligero unification. Again, same protocol. IPA Sum Check connections as well. Cool. So let's get started with unifying all these. The first observation is that we're always using objects and we're having protocols that have recursive structure. So let's do a bit of audience participation. Apparently that's good.

>> [laughter] >> Maybe let's start with like if anyone is familiar with some of the protocols I showed earlier, can you tell me like what's their sort of recursive step that's happening in them. Yeah. Yeah, so some check we have like these um polynomials and we'll reduce it to like one fewer variables, right? I don't know if people can read what I'm writing, but cool.

Um there's degree bounds on these polynomials. We can work with multilinear as whatever. Um any other? Fry yeah cool. Yeah, even odd, so even odd is a good description cuz you're working with univariates of degree less than D and you get to univariates of degree like D over 2. But you can also just describe this as any other folding factor. You don't have to do even and odd, you can do like low and high. Um you can just describe this as words that live in F to the N and words that live in F to the N over 2.

Cool. >> IPA bulletproof? >> IPA, yep, same thing. Uh they do low and high parts, right? >> Uh >> I think. I'm seeing some nods from people who worked on IPA, so I'll take it as a yes. Um cool. We can also have the Garo, I guess. It's it's a nice one to add in. I don't have any matrix stuff here. We have a N by N matrix and we eventually reduce to just a length N vector. Cool. So the language to unify all these is using modules and tensor products of those modules and that comes from the algebraic reductions of knowledge paper.

So why modules? Well, we have objects that can be added together. Like we're always working with things that can be added together. Um so in that sense a group would be enough cuz you know, they get scaled by integers. However, some of our arguments use uh challenges from extension fields. And so in that case, integers is not enough to represent these challenges. Um so if I need extension fields, I need sort of the next layer of abstraction after group, I need a module. >> It also helps in the sense that you can instantiate various linear codes, additive codes, and codes from module codes.

>> Yes, correct. Correct. Yeah, yeah. Uh well, we'll get there. >> [laughter] >> Like that that works. Um the other question is like why tensor products of modules? And by that I mean this idea that uh we can start with this one. A polynomial in n variables is actually a polynomial in n minus one variables as coefficients. And then we have a polynomial in just like one variable.

Right? So a n varied polynomial is a univariate polynomial in this variable where the coefficients are n minus one varied polynomials. Cool. Um and this is like the the tensor product. I am not really going to do a lesson on like modules and and tensor products, but hopefully these things make sense. Um we can keep working through these examples. Yeah it. Um univariate polynomials is going to look very much like this where univariates of degree less than d are actually isomorphic to

degree d over two tensor degree d over two. Yeah. >> [snorts] >> Um and we can do the same with a matrix, but I I I hope you can trust after the n n by n is isomorphic to fn tensor fn. Which means an n by n matrix can be seen as a collection of n rows put together or a collection of n columns put together. Like this operation is always put together. Like means put together.

>> [snorts] >> Um the next thing is the right hand side can have a basis. Like univariate polynomials we can have monomial basis or Lagrange basis. Um for matrices we can have unit vectors as our basis. Um yeah. Cool. >> [snorts] >> So this is all Coda polynomial Parno. Um or like that's how they use it. And it's great. However, they have a section about recovering SumCheck and they say this. Uh the tensor reduction transcript inherently contains more structural information which must be thrown out to recover the SumCheck protocol transcript.

Which is sad cuz it means like okay, we don't have a correspondence between their nice abstract description and SumCheck. Uh I disagree with this and we're going to see like why this is the case. Okay, the second observation is that all our protocols always prove the same relation. Actually, >> [snorts] >> I think I have it up here. It's the pre-image relation. Like of a linear map. So I have U as a linear map, W is my witness, V is the image. So uh polynomial evaluation is a linear map. Linear uh sorry, univariate or uh multilinear.

Uh sum over the hypercube is a linear map. Um I think that's it. Encoding with a linear code is a linear map. Interleaved codes, yada yada. Cool. Um So actually that's one of the things I want people to remember from this. Tell us what linear map you're proving. Don't just tell me I'm doing SumCheck. Please tell me the linear map I care about is this one. Um what happens when we plug in sort of actually all this stuff, like this tensor decomposition of the modules we care about, in this case W, into our uh pre-image relation.

Um first I need to introduce what it means for a linear map to also have a tensor decomposition. Um and in this case, if you have a map, you know, like F tensor G applied, let's say, to like the left part of a witness and the right part of a witness >> [snorts] >> is going to be equals to F W L tensor uh G W right. Right.

We just need to make sure that F is a linear map for like, you know, whatever module we had on the on the left. G is a linear map for whatever we have on the right. And then, yeah, that's just And this tensor operation now is in whatever target like we had. So, sum over the hypercube. Okay. So, in this talk I'm going to stay in this special case, but this is actually very much like a subset of all the homomorphisms. And very special subset. Um the theory extends for other ones.

The other thing I'm using up in this slide is I'm talking about like a public basis for the module. So, by that I mean like we have here the unit varied basis, the Lagrange basis. It doesn't matter which one you use. Cool. So, we can take our U of W equals V, plug in the things from above and we get to sort of yeah, this equation. What I did here is just what I did on the whiteboard, right? Like I I the sum out cuz it's a linear map. And then I put the U primes on the W parts and the U double prime on the delta part.

The nice thing is we have the split between what's private and public and that already sort of tells us how we're going to do our protocols. The prover is going to send the private part untrusted. The verifier is going to check everything else and then we're going to batch check this uh private part. So, we're ready to describe our reduction of knowledge. This is again called the Polian Parno sort of like a bit uh cleaned up, let's say. So, we have our input statement. The first phase is a split phase. The prover sends, you know, these like private part that we saw just a second ago.

The verifier makes this assertion untrusted. And then we have a folding phase where we're going to take a challenge C. We're going to run it through some generator, so think of this is like powers of C or uh you know, like the log randomness that they use in um I think Bitlis it was. Not here. Um and then we take linear combinations of our instance and linear combinations of our witness. And that's it. We're done. We now have a new statement which is maybe you're not Does this show? Or Okay cool.

Still not? Yeah. >> [laughter] >> Okay. [gasps] Um There we go. Ta-da! It's like open the curtains on the Um I'll pause here for a second because I want the intuition here to make sense. Maybe it'll make more sense once we start looking at concrete like protocols. Uh the plan for the rest of the talk is to look at how this is sum check. Um But yeah.

The idea is our relationship was just this equation with the U prime of WI. The prover tells us don't worry about this, I'll do it for you, and then we batch all of them. And the saving comes from like batching. Notice that at the end we're working with W prime, which is a combination of the W's, so we've like we shed off one layer of um yeah, complexity, I guess. Cool. Nope, that's not what I need. This way I need.

All right, so little checkpoint, this is our abstract reduction of knowledge. It's one round of these like log round arguments, or it's Ligero, if you want. Um But there should be questions still, like does this actually map to sum check? What about hash based PCS's? This is what we're all using in the room. How do we recurse? So I've showed you like how to go from input to output, I've removed one layer. How do we keep going? Um and how do we prove knowledge on this? Like can we prove knowledge on this at this layer of abstraction, or do we have to go and instantiate U, instantiate all our objects?

Cool. So like I said, the rest is not going to be about instantiating sum check as this. Do you have any questions at this point before we keep going? No nice. >> Can I ask a question in advance? >> Yes. >> Cuz I was otherwise asking about 10 minutes. So we're going to say, you know, kind of everything Oh sorry. Uh so I say you know, we're basically going to say, you know, everything is kind of sum check and and so on. And I think I have a some notion of this that's, you know, Adam's paper, just to say that it was sort of a case of the same thing. And and I think it makes sense, and I know like if you, you know, a lot of this framework is also what Kwang has been working on in in our claim, and so I

have some familiarity with that. I think the interesting question is also then we can say everything is sum check, but then we also know that, you know, once people actually implement stuff and try to make it faster that use case they still diverge in some way. And you just need to seems to be can we take this view of everything as a sum check and also want to translate that into how do I refine my sum check for my use case? >> Yeah, actually I want to move away from everything is a sum check and that I don't think sum check means much. I think everything is a split and fold argument. Except yeah, things with quotients are different and quotients we ignore that's why I say like log round arguments.

So yeah, rather than everything is a sum check I'd rather say everything is a divide and conquer or split and fold argument for the pre-image relation. What I care about is the specific linear map. And for that linear map or for the specific modules you're going to choose you will have more or less efficient algorithms to implement things like decomposing. So one thing >> That's what I have in the Aquiring switch actually. >> Okay, nice. >> I have a generic ring switch and you just have to specify the embedding that you want and then the trickiness actually comes from then when you need to map it to different notions of soundness. So I have the same ring switch that works for Hatchi and for Binyas but then for Hatchi you have code in twice special soundness and the trickiness is how to manage that

hierarchy of soundness definitions. >> And same when you go from I don't know like sum check which is very simple soundness definition to proximity like proof of proximity you also now have like it's slightly different notion. Yeah. >> [snorts] >> One question and I'm not sure maybe you're going to cover this but I'm curious how this would extend to higher degree sum checks. >> We haven't even said anything about the degree right? Um When I split my N varied polynomial actually I should have written degrees. Let's say I had degree D in every variable.

Like I have degree strictly less than D on both. My sum check will have here like my basis will be of size D. So when I split when I Sorry, I'm using N here. Yeah, N is the the size of the basis of, you know, your right-hand side. So, this is already like a degree N sum check. Uh what was I going to say? Yeah, to your question, one big thing is depending on how you choose your modules and how you split them, you might have to do FFTs. Right? Like, if I take a univariate polynomial and I split the >> The thing is you even have to specify

the algebra. >> Yeah. Yeah. Cool. So, now we're going to see why uh sum check actually works. >> [snorts] [laughter] >> And I have about 2 minutes, 3 minutes. Yeah, it's not going to it's not going to happen. Um All right. Sum check, we usually see it as the prover and verifier have a polynomial P. So, that's part of the instance. They both have it. Um there's a target sum sigma. And then there's no real witness because the prover has like P as the witness.

What I want to advocate for is actually P is also the witness. And the linear map we care about is the map that takes P to P and P to sigma. So, the map is actually the map like ID and sum over the hypercube. Now, I need to show you that these are decomposable, like I said earlier. Um so, the identity function will be decomposable, right? I just take identity on each side of my tensor product. That's fine. So, we're going to call this like ID tensor ID.

>> [snorts] >> And the sum is a bit trickier, but I think I have it written on slide. And for the sake of time, I'm just going to flash it to you. Um the idea being you express your polynomial as coefficients in your basis. Uh the sum over the hypercube you can split. And then if you manipulate the sum, you actually recover the sum over the hypercube of each coefficient tensor product the sum over the hypercube of your basis. And in this case I'm using the monomial basis. I didn't have to.

But I can. >> [snorts] >> Happy to walk through this later, but for the sake of time I think we can keep going. Um the question I might have is like okay, usually in sumcheck the prover is going to send like a univariate polynomial. And right now everything I'm describing is not that at all cuz if I'm saying you send left part of the homomorphism of the coefficients and I said this was my map, then you'd expect to see a polynomial being sent like the coefficients and their sums.

The coefficients we can not do because it's redundant information with our instance. This I still need to convince you like that sigma sorry, that the univariate H is actually all these sums all these VIs. And that's this slide. If I actually take, you know, the sum of the VIs so this is the expression the verifier is checking. Again, manipulating the sums um I'm just expanding B for the case zero and the case one.

You actually see we now have a polynomial here evaluated at zero and a polynomial evaluated at one. So this tells us immediately actually H is the polynomial defined up there at the right. Um and when V is checking H of zero plus H of one equals the target sum it's doing this operation. Um it's in a sense like sumcheck sort of is unaware of its own magic and says send a univariate polynomial without realizing what I care about is actually send the underlying sums or the smaller instances.

>> [snorts] >> Okay. Anything else I want to say about this? I don't think so. Ah, yes, one last thing. I used the monomial basis as well for H, but I don't have to. And that's also why sometimes you won't see like if you look at H um in a different basis to the basis used to decompose, it's not going to look like they're sums of your coefficients. But that's fine, you're still defining the same polynomial. >> [snorts] >> Okay, back here I've explained three and four.

Okay, now the next thing is when we get here, we don't say Okay the we take the the sums of H, well, we take H of R usually in sumcheck, right? H of R is this as long as H was in like the right basis and we've used generator to be that basis as well. Um what happens to you know, uh fixing one variable? You know, we take our polynomial P of X and we actually set one of the variables to be R.

So it's what happens here with the witness. And it's actually what's happening on this part of the instance. And that's the hardest part of sumcheck. How does the verifier check this succinctly? And this is actually what we differ. Sumcheck says, "I'm not going to check it. I'm going to keep recursing and at the end I need to do one polynomial evaluation." That's what that evaluation is. It's these checks these linear combination checks deferred all the way down. And so there you have it. Sumcheck actually is this thing repeated over and over again.

Um we can do more than that if I find the clicker. Oh, there. Enough with sum check, hash-based PCS. Same thing, but instead of the identity function, I actually have a code, like an error-correcting code. Um, and why do I want to do this? Because instead of having the polynomial evaluation at the end or checking my output instance, the code allows me to do just spot checks. And that's like sort of the the fundamental reason why we use error-correcting codes.

Um, so your hash-based PCS is just an encoded sum check. That's it. End of story. The difficulty is I said, "Ah, I need you to have this like magic structure." And not all codes will have this. Reed-Solomon codes have this. And once you shed off one layer, it still has it. And that's why like the first IOPPs we had, like Fry, have Reed-Solomon codes. That's where the magic is. Um, an interleaved code also has that magic in that U' prime is any code, and on this side you'll have, you know, like whatever basis uh, you're interleaving with. Like you These are the unit vectors, you know, like first, second, third.

>> Wait, wait, wait, is this every interleaved code or like >> Every interleaved code. Interleaved means I have a code and then I put it at the top, I put it below, below below below. Yeah. The only problem is once I've shed one layer of this, I'm left with this U' prime which might not be magically structured, and this is where we do code switching. So actually we can have a more generic thing. Here we could talk about like map switching. And maybe that's something to consider. Um, and that's it. And we also do code switching with Reed-Solomon codes sometimes for performance, and that's what like Stir and Word do.

Um, and that's it. That covers all our hash-based proofs pretty much, except the ones that use tensor codes, and that's like something I need to check on. Cool. I think I'm above time easily. Oh, no, at time. Beautiful. That's enough for a little recap. So, all these protocols I mentioned, we've described them with multilinear polynomials, univariate polynomials, blah blah blah. Actually, we can just talk about modules and tensor products to express this recursive structure.

We always are arguing the pre-image of a linear map. And if we want to do more than that, like something like Spartan, I think we actually reduce degree two to degree one using this, and then degree one to truth using this again. Uh these are all split and fold reductions. The design decisions, once you have this template, is okay, what modules do I use? And you're going to choose things where you have like fast uh algorithms to compute them. You have to choose your generator, and that's going to also change things. Um and the big question is, how does the verifier in enforce this like output instance thing? So, with sum check, we defer to the end, and we have still an expensive computation.

With hash-based PCS, we have uh spot checks. In FRI, it's these correlated spot checks. In Ligero, you have just one round of spot checks. Um in like Bulletproofs IPA or lattices, you have homomorphic commitments. So, actually, you can just add the commitments together. What I didn't cover is what happens when you doesn't have this magical structure. So, it's this structure, but with a sum. This what happens in inner product arguments. This is why you get cross terms. And if you want to chat about it more, I can happily.

What I skipped over is the soundness proof, but I can tell you now it relies on the properties of you and the properties of your generator. And I didn't give a proper description of a PCS, but from the point that you have like a binding function and a polynomial evaluation, you have a PCS. That's it. And paper coming soon. Hopefully formal verification with it. And hopefully this is now a fact for you to take with you. Thank you very much. >> [applause] >> Happy to take questions if we have time.

I don't know who's the the time master. Cool. Oh no, no questions. >> There's um >> [laughter] >> There's There's a cute trick in in some check where instead of the verifier verifying at every step, it uses this relation to omit one of the values sent. Does that also generalize? >> Yeah, absolutely. Um Let's see. Where do I have it? So here the verifier has to take this combination. Uh sorry, no. Has to check this.

If um this is known, you can keep one of these unknown. And as long as like this tensor is invertible, easily invertible, then you can like, you know, manipulate this to have to isolate one of these VIs on one side and recover it. So yeah, that does generalize. You do need your tensoring operation to be invertible. Yeah. Oh, that it's invertible? No. It's When you're working with a field or a field extension, it is. Yeah, exactly. Or if you're working with rings, then not invertible.

But that's fine. It's just the trick of I can avoid sending one VI multiply. I don't know if it's a big saving or not. Can you Yes, if you work over fields and your like tensor product is multiplication in the field, then it's invertible. Yeah. Do you want a microphone or yeah? >> Do you have to have a property of this >> Yeah.

>> zero divisors >> Okay, sorry. Can you say the first question again? >> I believe from from what I understood the theory the tensor product being associated amounts to the univariate skip >> Yes, absolutely. >> And what about modules over rings with zero divisors? >> Yeah. So just for the univariate skip actually something I wanted to mention. It's really nice. It actually says what we're saying here is your first decomposition is very important because that's when you start introducing challenges. So you could decide to decompose with more than one variable here or you can decompose with higher degrees.

So that's yeah, the univariate skip. or or wacky AG codes absolutely. Although the AG code is more about this. It's the the preimage or oh no. Okay. Okay. Yeah. Cool. Then then that is that. Rings with zero divisors you might have issues. Yeah. So the sound is depends actually I lied in that I said it depends on you. It depends on the generator. It also depends on what ring you're working in.

>> So does this sort of picture suggest that say tricks you come up with for some checks should be able to be pulled across a different >> Yeah. >> Cool. >> Absolutely. This is why so maybe I should have motivated to the talk to begin with but if you're doing formal verification do this, you know, and then formalize the tricks one by one. If you're writing algorithms and you found cool tricks in one area well check if through this they translate somewhere else. It might be that your trick is specific to the module and the decomposition you're working with or it might be that it's general. So, like Remco Remco was asking when can I or can I not get rid of one of the VIs when this tensor ring is invertible?

Yeah. >> Um Uh one of the uh features of this presentation is the linearity property. Now, the pre-image under a linear map, uh have you thought about different kinds of relations keeping the linear structure of the module? >> Um So, different kinds of relations, you mean like higher degree relations? Yeah. So, the algebraic reductions of knowledge paper talk about this. Like, how do we do bilinear relations with this tool? And the trick is you take your bilinear relation, you reduce it to a linear relation using this.

And then, again, you run a linear relation using this. Which I think is more of a general thing of what we're doing when we're taking, you know, R1CS, reducing it to polynomial commitment scheme, and then evaluating the polynomial is that degree two to degree one to truth. I think that might be the general formulation. We also have like these lin IOPs that we reduce to commitments with linear queries. I think it's the same >> Okay. >> elephant we're touching again. >> [laughter] >> Like >> bilinear map stuff in FHE. >> Sorry? >> Does this apply to the bilinear map stuff in FHE?

>> Uh FHE, I don't know. Bilinear maps, I think yes, in that Kate upon Parno again in that paper I keep referencing have that. So, it should. Yeah. Cool. Then I'll see you there. Thank you very much. >> [applause]