Hash-based zkSNARKs

Transcript

[Applause] Okay, so we started with the foundations uh for Son and we're kind of working our way up the stack. His next uh talk is going to be from Jako also on foundations the proximity gaps uh conjectures that that we're and results that we're relying on. Hi guys. So I'm J. I'm a researcher at PFL and today I'm going to be focusing on the other side of the stack which is the ashbased snarks. So Antonia has very helpfully like been telling us about the

ashbased part. I'm going to be telling you about the other part. But first I'm going to just kind of go a bit back tell you about the story of ashbased ns how are they constructed and then some of the open question that I often in this workshop we can make some progress on. And so I made like a very like arbitrary like uh graph. This is like kind of started from as far as I can remember. So you know at the bottom we start having like the initial elliptic curb base scheme GST and KZG and then we're going to have like a a progression of scenarios going to come. So this is time on the side. So what is the y- axis? Well it's just arbitrary goodness. I'm taking a

playbook of like the old company. So this doesn't mean anything but I need the number to go up for the slide to actually work. So okay so we had like uh after that we started having BCS. So this was the definition of IOP and in 2016 we had gross 16. Then we had few more things like bulletproof and IAX. In 2018 we started having fries darks and aurora. So this was like when like ashbased n really kind of like took their stride and came into mainstream. In 2019 we had something which is called the cam explosion of snarks. So this year a lot of stuff happened. Uh a lot of the system went on and then we

continue with plus uh we had breakdown flunk flong Germany flu you know Labrador you know baseballs be h you know frainister like liatron up to the end and you can see that like that uh what I have over here is the green ones are like all the snark kind of like which are bash functions and you can see that uh this trend is going up because I made the graph that way also there's more and more green on these things at the same time there's been like industrial adop adoption which has continued like there's been like started like from like the dcash which is really

the pioneers in the industrial development and adoption of snarks and there were things like polygons of starware but then you know 2023 give or take it was when DKVM started like appearing you know and then we also had a camera explosion of ZKVM and this kind of like furthers my point because most of these ends up being ash based so it seemed like that at least from the industrial and like the richer things ashbased nar tend to have like a very good track record there are things that change there are very exciting development in like latis based things now which I'm really excited about but as a good pet the ashbased nar they tend to have like a good record so let me tell you how these things are

built and like uh one of the things which I'm really blessed is that okay so this is like the marketing part don't worry about it but you know and then the nice thing about touch base is that you you get like a lot of benefit compared to like public key secure cryptography secure like snarks so you get transparent setup you know the field operations are much more are much cheaper so for example this is something I run on my laptop on like committing into a large vector of field elements between like ashbased and elliptic curves. It's not really a fair benchmark because there are lies them light and benchmarks is one of those. Uh but the good thing is like the the

performance that we can get is something is something quite nice. So how do we build these things? One of the very nice things of ashbased narks is that they admit a very like clean separation between the part which is the cryptographic and the part which is information theoretical. So essentially every ashbased narc is either explicitly or implicitly obtained by something called the bcs transformation. So you start with something which is uh fully information theoretical that is an IOP.

So uh how many people here are familiar with IOP and PCP just to double check. Okay, good. Perfect. So roughly this is like interactive protocol between approver and a verifier in which the verifier the approver can send like long messages. Think of this to be as large as a weakness maybe you know few megabytes but the verifier is not required to actually read them in full. It just can like make few queries to them. So you can just read a few location over there. Then you take this uh you take this information object you know in the world that we live in we don't have oracles we don't have any of this kind of stuff and then you compile it with that cryptography the one that Anton has been

telling you about to get something which is actually a cryptographic object with simness so this is how you do it this is cores of like book this beautiful keynote illustration and you can think of it that the when you compile it you end up getting an argument which depends like linearly in the number of queries and logarithmically in the like size of the oracles. So for typical settings so say 2 to the 26 like proof length and like 400 queries you end up getting something small in the order of t or like few hundred kilobytes. So this is how you get you boot such things.

Yeah. So there's a beautiful book which I have uh by contract I have to plug every time I make this slide. You're welcome. Way to check in the mail as usual. Yes. But what we're going to what I particularly focus on is the IOP because one of the beautiful things about a bas is that this compilation process is by now very well understood very well documented and like there's a you know on that we're very confident on. So as long the function is is in a good spot which Antonio assured me it is then we are like we can focus all our attention on the IOP side and this is quite interesting because this is a purely information theoretical you can forget

everything about cryptography and just focus on the IOP sorry and IOPS they roughly can be decomposed in like two different steps uh a front which roughly what happens is that you send some redundant encoding of the witness under an error correcting code of some sort. For our case, we're going to be read Solomon and then we're going to have like a back end which does something called approximity test. So approximate test effectively like looks at this redundant encoding touches it in a few places and somewhat magically this is enough to guarantee some of the

properties that the encoding needs to have. So why have I uh made this slide? Well because the point I want to get across is that IOPS and efficiency of snark is almost fundamentally intertwined with the code. like the really like coding theory and snarks end up having like a very nice dance together like what we by now we know how to construct IOPS with the stigience is almost entirely determined by the code that we have so with no other factor train and for your intuition yeah the yes so the the front end kind of tells you what the IOP can prove and then the efficiency is in large part determined

by like the the test that you have underneath. And just to give you like kind of like the parameters of interest that you should think about like you know what codes we want to use like so code will have like very well and very well studied coding theory theoretic like properties particular minimum distance. This is like the distance between two code words in the code. The rate this is like how much redundancy the code gives you. and then encoding time and the uh the minimum distance almost directly translate to verifier efficiency. So code with larger separation between code words will give you leave you a better verifier.

Rate translate directly to how many ashes the prover needs to make and encoding time also translate to prover time because the prover will have to encode the dam witness. So this is kind of like how what you should think about for the for the things and for most schemes and what I we want to focus on for the proximity price we like resolon code and this is not just an arbitrary choice resolon code in a certain sense informationally they achieve some optimal things so they are like max code so they achieve the optimal tradeoff between the rate and the and the and the distance so between the number of proverses and the and the verifier efficiency

was so encoding is an FFT which theoretically this is not optimal but turns out we're really good at doing it in this surprisingly maybe like I think it's the second most optimized algorithm after matrix multiplication >> by arbit my arbitrary matrix and the third part is that they have great proficient test right like this was already shown by fry like rich solomon course has like a lot of structure that you can use to leverage and to and to test proximity to. So they kind of like they're a very natural choice for this stack. They're not the only like choice but they're a very natural choice.

Okay. So this is kind of anatomy like what I want to focus on this workshop is something which Justin has been talking about this proximity price and this is going to be what underlies the security of basically all the ashbased IOPS that I've shown in the previous slide and the property that we're going to be caring about really is something called cored agreement. So uh what's correct agreement? So there are many many notions of it. So I'm going to kind of like go through the the various one of them. And so the setting is that you have like a bunch of like uh a bunch of like vectors. So you're given some vectors. You cannot read them in in

their entirety. And you know we are in the business of like doing succinct arguments. So there's only one thing that we actually know how to do which is like try to go from many things that you're you're interested about to a single one. So what we're interested about about these things is that we would like this to be guaranteed to be close to a code. So ideally I would want to check that all of them are read Solomon codes but in reality I cannot really read all of them. So I kind of just want to get some proximity version of it and the only way that we know to reduce from like many things to a single one is by taking a random combination. So what will happen is that the verifier will just sample some scalar arise and then

we'll ask the prover to tell us what is the combination of of the previous code words on the on that. So as you see you're kind of like shrinking the problem size by a bit. Now the whole area of correct agreement correg is about like figuring out what happened if I tell you that this part is close to a code. What does this imply about the init the the initial things? So my uh my initial condition will be that we we say like okay with itability over this choice of randomness we know that this f asterisk is close to the code.

What does this tell us about the original things that I care about? So this is kind of like you know you can think of this that in these three locations uh the the thing agrees with the code in reality this that should be more than three but that's maybe I'm sorry like okay so agreement is something that we knew from a long time tells you that if the initial last thing is close to the code then all the individual things will be close to the code. So this is what uh this is kind of like the setting that you have.

So it turns out that this is not is useful but it's not too useful. So we need some strengthening of it to get like very efficient IOPS and one strengthening is that of correct agreement. It is that not only they agree with the code but they will also agree on the same strike. So this is kind of like the picture that correct agreement gives you and this kind of makes sense because if you have like things which agree with the code in the same place then they will also you know agree you know when you sum them they kind of like the errors do not uh do not disappear and you know of course if you are in the same world we are actually in this setting and this is strengthening still which is of mutual creative agreement which is basically that uh the strike in

which the uh the final final code word agrees with the code is the same in which they in the the final code word agree with the code. So these are the three flavors of of coral agreement and yeah like all of the all of the ashbased narcs that I was telling you about in some way rely on some property of this of this uh kind. Okay. So what is the proximity price? So the proximity price is initiative that we have to like try to uh to understand what actually holds about uh this problem. So as I said before we have a blessing we have a blessing in a space word in that uh security is information

theoretical. So for the previous property that I can like that I show you before in some particular settings we're able to prove like very good bounds or not so good bounds uh that tells you that security all unconditionally for desire. Unfortunately, these are not the settings in which a lot of these systems are deployed to get like to per to get performance to a a good level. People use conjectures in order to actually um estimate what the behavior of this uh combination does.

These these conjectures they like kind of like partially battle tested in the sense that nobody has been able to break them but they connect to some very beautiful questioning theory. So what the opportunity price is about is kind of is formalizing these conjectures and putting it out to the world for actually to prove like at the conjecture will give you at least a twice improvement in like recursion speed for example and there's a lot of questions you have to do which I hope that in the workshop we're able to uh to to address. So this very like uh on from like the the least technical to the most technical. So I

think everybody can contribute. So there's like the uh the bike shedding like we which is basically we're going to be putting out uh the Ethereum foundation is going to be putting out a million dollars for this problem. So this is going to attract a lot of attention and you know the number is probably intentionally suggestive of like the clay problem. So the millennium problem which create like a lot of like attention. So in order to like uh not lose our faith we need to be very careful on how we like um we evaluate and like we check submissions. We want to figure out you know many questions like should we require formally verified solutions? Is the use of AI attested in

the in the solution? all of these kind of like more like administrative things. So this is like just figuring out the condition of the price. Then there's like the theory part. So even like stating these conjectures in a way that are like possible to prove and not trivial to disprove is not trivial. So here we need to find like the the right formulation. There's I've already started like uh with some survey of like the literature to figure out what is known about all these problems but there's more to do.

There's like a lot of like interesting like uh papers to like look down to figure out exactly what are the status of the art. You know there are some question about whether we want to like state them as like very like mathematical uh problems or we want to target more concrete like improvement of the protocols. There are like other things which are interesting you know for like setting of like ashum could be of interesting. So for example there's this factor of seven maybe six on like previous work uh that if we you know even just improving this bound which is much simpler than improving the conjecture but still very hard is a very interesting open

question. So there's like a lot of interesting like directions on what we want to formalize, what we want to actually prioritize and hope the research actually goes towards. Uh so yeah, so this is the proximity prize. I think we'll have a session tomorrow. Well, one today, one tomorrow and another one maybe. I'm not exactly sure. The other thing which I'm interested on when I'm here is the performance award. So I think will be talking about this in a bit. But you know, so this is a war and there's like, you know, one of the goals that we want to get is this is getting the the line in Justin's like

slides below the other line. And um I think like this is a good opportunity to also try to figure out what what kind of improvements we can do on the lean application part. uh you know one one thing I'm kind of excited about is this concept of sigma IOPS that we had introduced when we were doing work that I think could help us with dignity for example. So this is something that we can also try to uh to jam about. So yeah this is like my two focus for the workshop. So one of them is like really trying to get as much as possible uh as much progress as possible in proing the price on formalizing the

conjecture trying to give intuition on what the things seeing what's possible to prove and what's not and trying to get like as many decisions out as possible and the other one on trying to optimize work performance as much as possible. >> Thank you. [Applause] >> Thank you for a great talk. Uh I have a question. So can these conjectures can be meaningfully formulated for some small parameters so that we can kind of test them or find the solution by exhaustive search or something?

>> Yes. Yes. In fact they can be done and Antonio has written a script for that for this already. So this is something that I won't talk more in the jump part. So conjectures when we're talking about for example the clay institute they tend to come like when possible with extensive numerical like analysis and experiment that kind of suggest that this conjecture end up holding water. So I think for these conjectures uh there is something that we can do for like very small parameter we can start brute force searching. So one thing that I think will be very good for the forum prize would be like to also have like um a lot of experiment which suggest that the conjecture that we believe actually

all true for like small parameters >> for like boundaries on small parameters >> or boundies on small parameters. Yes, that's the other option. >> Yeah. Yeah. Absolutely. >> Uh I just have a very uh basic question. Um if the conjecture is true, does that solve any other open conjectures that exist in coding theory? Do we know what that um looks like from the perspective of just how difficult this problem ends up being? I know there used to be I think three or four years ago that start um Starkware had um based some of their security analysis on another conjecture like do we know what it looks like from the the sort of like conjecture flowchart like do we have any work on that? So yes so there is like uh there

are some different kind of conjecture for example the one that starore was uh using is something called the toy problem conjecture so the conjecture that we target is strictly weaker than the toy problem problem but still enough for what we care about weaker okay incomparable actually because the the toy problem targets correct we will be targeting mutual which is stronger than correlated but the toy problem ask for an error which is very very small while we're kind of fine with larger errors. So the two things are incomparable. So one thing to note is that all these proximity gap conjectures they're kind of like very endemic to the proof system field. Like if you look at the wider

coding theory literature these are problems which are not studied in as much detail. the one as part of the conjecture we actually going to be touching one of these coding to edit problems because we actually need some property on list coding. So this is the probably that I give you like uh you know I give you some word and I want to estimate how many uh code words are close to this word. So this is a very well studied problem in like uh in coding theory for like been open for like 20 years in the parameter setting that we care about and we know some connection between the proximity gaps and the and the list the coding but they tend to be very lofty. So they don't they don't doesn't really tell us much.

So like there is some gut feeling that these two things are related but even just understanding how they're related is still something which is open to follow when you're You mean the conductor? >> I'm talking about the conjecture about like the uh the re Solomon code up to capacity. Yes. Exactly. Yeah. Have a bounded list. Yeah. >> That reminded me a little bit. >> Exactly. Exactly. No, they're very related. You kind of need both of them for the security of this system. Uh without an algebraic decoder, we just need a combinatorial analysis.

There's been recent progress on this kind of conjecture like we know that for randomly puncture resolment codes we actually have this property up to capacity but for like the the code that we care about the explicit uh read solommon codes we currently don't have any techniques for it so it's like a you know a very interesting problem in my opinion hey so maybe more of a comment not exactly a question but I just want to comment that there is a world where the conjecture is false but the stark that we build is still secure. So the conjecture is mathematical information theoretic right but let's say you talked about list

decoding it still could be that it's computationally hard you know to enumerate this list of functions or to find the counter example for the proximity gaps and so even if the conjecture is false could be that the schemes we build under assuming the conjecture are still secure and I guess that would be hard for the prize like if you want to somebody can bring a efficient attack not just prove that it's yeah I totally agree like it can happen this is the one of the world that we can live in I hope it didn't like uh yeah in that case so yeah like my personal opinion on this

and we can chat a bit more during the jam is that um like we have this blessing in ash's world that we can be information theoretically and so Even though there might not be an efficient computational attack, I would still be kind of feel kind of une there's an efficient informationical attack. So it is possible. Uh but I really hope it's not the case. >> General, last question. Uh I saw a screenshot where there's some sort of survey with Dan. Um is that paper out? >> Uh no, no, we are uh still writing it.

Uh I have like a GitHub link at the moment uh that I can share with people. >> Okay, perfect. >> Yeah, the EF Millennial one. Yeah. >> Oh, the millennial one. Okay, perfect. >> Yeah, but it's still like Yeah, I think the last time I touched it, so I need to uh Yeah. Yeah, there's a lot of work to be done there. >> Perfect. Thank you, Jakobo. Thank you, I think we're going to break out for five minutes for coffee. Uh we're running a little bit behind schedule, so we'll make it a quick break.