Beyond the Johnson Bound: A Path to Smaller Post-Quantum SNARKs

Transcript

[music] [music] Good morning everyone. Welcome to our workshop beyond the Johnson bound. This is going to be an introduction to the Athereum proximity prize. There's some really interesting mathematics. We're going to be explaining everything from scratch. So you don't have to have any background information on the Ethereum proximity prize. We're going to explain everything. So, um, if you're familiar with Ethereum Proximity Prize, this is going to be a little bit of a recap, but you might learn something new. So, yeah.

So, what are the goals of this workshop? Uh, the goals of this workshop are to build the foundations required to understand the Ethereum proximity prize. You're going to understand how solving the Ethereum Foundation proximity prize can lead to smaller postquantum snarks. And at the end we'll also explain at a very high level the recent mathematical progress made related to the Ethereum proximity price. All right. So what are we going to cover today? We are going to cover coding theory terminology and mathematics.

We're going to explain what the Johnson bound is because that's the name of our presentation beyond the Johnson bound. We're going to cover mutual correlated agreements, MCA, and we're going to cover the $1 million Ethereum Foundation Proximity Prize. We will explain how solving the Ethereum Proximity Prize will lead to smaller postquantum snark proofs. We will briefly at the end summarize latest research results related to proximity gaps and also explain what in the world better codes is. if you've heard of it. Uh it's this auto research competition and its relationship to the Ethereum proximity prize. Awesome. So, how is this even related to Ethereum? So, Ethereum is

migrating to hashbased snark cryptography. This is the lean Ethereum protocol initiative. So the goal is to make these hashbased snark proofs as small as mathematically provably possible because smaller proofs means a more performant blockchain because literally when you're creating a proof and you have to send it over the wire over the internet the smaller the proof is um you have like more bandwidth. So it's just a more [clears throat] just more performance of the blockchain and also to achieve a fully formally verified stack there needs to be no reliance on mathematical conjectures. So we want small proofs but we need to have proven security.

So that's how this is all related to Ethereum. Okay. So we have some workshop materials. This is just our GitHub. we have was all these definitions because we start at the very beginning with basic stuff but as we progress uh we don't want you get lost uh with some of the terminology so this is just to uh keep that all those ter like terms and stuff in your mind uh and we'll have this QR code throughout u the workshop okay so since we're talking about hashbased snarks we need to talk about the basics of read Solomon codes. So what in the world are read Solomon codes? So read Solomon codes are a class of error

correcting codes. So at a very very high level this is what they allow you to do. So say you have some message m of k symbols you can encode it into a code word of n [snorts] symbols. You send it across the wire. It can get corrupted. That's okay because then our recipient of the message can still recover the original message. So at a very high level, this is what reads solen codes allow you to do. So first example of where read solen codes are even used.

They're used in some forms of communication. So let's say Alice wants to send some message over the wire. It's a lossy wire. She can overencode it. Just some bit flips. That's okay. Bob can still decode. So essentially you can recover corrupt data during transmission. It's also used in data storage. So let's say Alice wants to encode some data. She saves it on a DVD, CD, whatever. That's okay because if it gets scratched, she can still recover that data. So you can recover data by overencoding it. And also it's used in hashbased snarks for proving computation. So let's say you have some computation some function f

ofx you can run the computation generate your trace which is just like all the intermediate steps of this execution of this program f ofx then you can encode it into a polomial we'll explain all this um so you have now your polomial you can prove certain things about this polomial that the trace follows certain rules and then you do some more things at the end um so that the verifier can quickly and succinctly verify that this computation was done correctly. So you can verify the result of computation without having to do the computation again.

Okay, so concretely let's go through a very basic example here. So let's send the word hello to our friend over the wire. So literally the word hello and we know the the wire is lossy. So we don't want to like accidentally send the word hell to our friend cuz then it's you know that would not be good. Uh so we can turn this into asky for example. So this is just this vector of numbers and we can find the polomial which when evaluated at this this leads to these numbers.

Then we can over encode. So we evaluate this polomial at more points. So now we have this larger vector of numbers and this is literally just the evaluations of this polinomial. Then we can send this over the wire. Some points get corrupted. That's okay because our friend can still decode and we'll explain sort of how that works later on. Okay. So now let's get a little bit more mathematical here. So this and again this is starting from the very beginning like we're starting from the very beginning. Um don't worry we'll we'll get past these very beginning stage definitions.

Okay, so we got to start with what in the world a finite field is. So a finite field denoted FQ is a field containing a number a finite number of elements where addition subtraction multiplication and division by non-zero elements is defined. The number of elements must be a prime power where Q is equal to P to the power of M where P is a prime number and M is greater than or equal to 1 and is an integer. So concretely f finite field f7 you can do arithmetic over this field. For example, if you want to do six plus one in this finite field, the arithmetic wraps around. So at a very high level, you can do arithmetic over the finite field. Okay,

cool. Next definition, domain. What is a domain? So domain with this curly L it is a set of distinct elements from a finite field at which a polinomial is evaluated. So every single element in this domain is an element in the finite field. Cool. What is a vector? A vector is an ordered list of n field elements. So in the context of read solomment codes these are evaluations of a polomial concretely.

So yeah notation here is v_sub_1 v2 v to the n where f to the n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n n is the length of this vector and q is the size of the finite field. And concretely if we have this polomial x^2 we plug in the points of this evaluation domain to this polomial and since it is a finite field f7 this is the evaluation um our vector. So this is the resulting vector. Length of the vector is six over the finite field f7. So things are happening modulo this finite field.

Okay. So now we're going to get deeper into read solomment code mathematics and Andre is going to explain some definitions. Yeah. Hello. Uh yeah I will cover read Solomon code. Uh so read solmon code is a set of the all vectors obtained by evalation of polomial degree less than k over field f at evolution d l. So you can see here that L C is a Ritzelman code at F is the finite field. L is the valuation demand and K is the dimension of the code and C L C is a set of the all valid code words.

Yeah, we can visualize element code here. So uh the setup here is F3 the spinate field. L is evolation domain in case the dimension of the code and at the left side we can see all the polomials that um generated infinite field F3 and then we basically encode these polomials into the code words using this evaluation MNL. So what is a code word? code word is a vector that belong to the set of the code word C and the word is a vector of the finite field elements that may not or may belong to the code C. So the key

key distinctions here is every code word is a word but not every word is a code word. Uh the code rate code rate is defined by Greek letter raw. So basically you divide the number of message coefficients into number of elements in the code words. So yeah you can see here two examples. The first one rate five over seven. So in the green in the green line the gray area you see that number of message coefficients and uh if you sum up gray and green area so you will get the number of elements of the code word. And uh the second uh example is 5

/ 10. So yeah you get uh you have a k is the number of coefficients. [snorts] So in gray area you have the number of message coefficients. And if you sum up gray area and green area you get uh code word lengths. Uh next I will briefly define smooth evaluation domain. So why it's important? It's used extensively in uh FFT algorithms to evaluate polomial efficiently. It's also used widely in snarks in the proof system like FRI for example. So I define it as L. So whereas omega is element of the finite field

whose powers first return to one after exactly n steps and n is often as a power of two. You can see here example of a smooth domain. Here I define it as L. And you can see here the size of the evaluation domain is 8 which is power of two. And we have a following setup here. We have finite field f F17 which is omega= to 2 and n equals to 8. And you can see here in the bottom that um exactly after eight steps two and the power of eight evaluate to one modulus 17.

So and we can have a quick quiz here. So you can basically don't raise your hand just you can mentally check that you uh understood this topic correctly. So uh there is a ritzelman code encodes five symbol into 11 symbol and what is the code rate? So I can wait like 10 seconds. So uh yeah and the answer the correct answer is B is 5 over 11. Uh and the next quiz is uh if k equals to 5 stay constant by n doubles from 11 to 22 what happens to the read solommon code rate? And you can see here on the top there are like some formulas to help

with this quiz. So you can think about it uh 10 seconds. So and the correct answer is rate halves. So next I will cover measuring error between vectors. So you can see here on the slide two vectors C and V they disagree exactly in two positions that marked in red. So I define absolute Hamming distance here that is number of positions that these vectors disagree which equals to two and the relative Hamming distance it's delta. So it's basically absolute Hamming distance divided by the vector

length which is 2 over 7 uh seven in this case. So next I will cover a hamming balls and decod ready. So in this slide you can see this circle which is basically this humming ball. So I define it salmon code in the right area. So yeah and uh uh also um basically all the dots within this circle are basically belongs to the Ritzolmon code large C and given some code word Y over length N defined over finite field FQ and the goal here is efficiently find all nearby code wordss

uh to Y within some radius delta. Uh so and uh if we set the radius to 1 minus code rate over two I recall that code rate is equals to k / n. So and uh we can find at most one code word within this unique decoding radius that is close to y. You can see here that is c1. So in this example you can see the polomial P which is equals to X. So we can encode this polomial to the original code word C and this code word actually

transmitted over the wire and getting corrupted. So you can see this uh last two position and corrupted code words they disagree in with original code word. So and you can see here on the bottom we can compute a relative hemming distance and this is would be uh approximately 28% and it it lies within this green unique decoding area. So it means that one can recover the original code word unamiguously. So if we increase the radius up to Johnson radius which is defined over RJ 1 minus square root of the code rate. So

we can all we can return all nearby code words to Y. So you can see here in this example that there are C1, C, C C2 and C3 there are code word that basically close to Y and there is a Johnson bound guarantee here that for Y the number of valid code words within the Johnson radius of Y is polomally bounded. It's important to understand. So and if we increase the radius beyond the Johnson up to capacity so this guarantee no longer applies although the small list can exist and if we go beyond the capacity so to find all nearby code words

to y would require exponential time. Uh quick recap here. So we have the smallest radio this is unique decoding radius. So we can find at most one codeboard that close to y and uh if we increase the radius to Johnson radius we can find polomial number of nearby code wordss and we if we go beyond the Johnson bound. So this guarantee that uh the all finding all nearby code words will be polinomial binding no longer applies and if we go beyond the capacity uh the number of all nearby code wordss

would be exponential and we have also quick quiz here. So yeah, you can basically prove that you mentally grasp the topic. So the rate raw 1 / 4 the approximate Johnson error radius is so you can have a at the top you can have a hint that's Johnson radius is computed is 1 / square root of the code rate and there um the correct answer is C it's 50% sent.

Next, Alex will talk about mutual created agreement. Awesome. Okay. So, mutual correlated agreement. But first, before we talk about mutual correlated agreements, we need to define some things. Okay. So, the first thing that we need to define is what an agreement set is. So, we have two vectors. We have a word and we have a code word C. And an agreement set is just the evaluation points where a word and a code word agree. So in this case, it's just the these green squares here.

So the set S is you can see. Okay. So yeah, it's the these points. So 1 3 4 6 7 8. And this is the set S. Every single element in the set S is an element in the domain L. And there's this notation called restriction notation which is this. So if you this is like the mathematical way of saying that these green squares of code word C are equal to the green squares of word U. So you can say U restricted by S is equal to C restrict by S. And this notation pops up in the later slides.

Okay. So agreement set S. So the next concept to grasp is S delta closeness. Okay. So S delta closeness is essentially the same concept as the agreement set except the size of the set S needs to be sufficiently large. And all this means is that the size of the set S needs to be greater than or equal to 1us delta * n. And in this case so we have two places where these were these vectors do not agree. So these gray areas so their absolute Hamming distance is two. They differ at two positions.

Their relative distance is 2 / 8, the length of the vector. That simplifies to 1/4. So 1 - 1/4 * 8, which is the length, is equal to 6. So six green squares, it's the size of the set S. And so it is a sufficiently large set S. And it's important. So we can say the word U is S delta close to the code word C. But we can also say that the word U is S delta close to large C.

And probably should have made this a different uh letter like U or something or yeah different uh code word um definition here. But it's also you can say it's S delta close to the entire read Solomon code. So the set of all vectors. Okay. So next concept is a random linear combination. So say we have two code words f and g and we can do f plus alpha [snorts] * g where alpha is randomly sampled from the finite field. This is a random linear combination. So, and if F and G are both code words,

H alpha is always going to be a code word. And this is the definition of why read Solomon codes are linear because any random linear combination of F and G, if they're code words, H alpha will always be a code word. So, let's run through a quick example here. So these two vectors both code words elements of the set C and this is their corresponding polinomials and we can do this random linear combination which is say that randomly we picked two for alpha and this is the resulting vector uh 1 412 and this is a valid code word and this is the corresponding polinomial when we did the

random linear combination. Okay, so I think we have everything required to understand mutual correlated agreement. Okay, so in the previous slide we were talking about if F and G are valid code words. But in this case, let's just say that F and G are not valid code words. They they can be, but maybe not. So they're just vectors. So and we sample alpha at random here. So and then this resulting result of this h alpha the result of the random linear combination it is s delta close to u. So meaning that it agrees on these green squares with u. We can say it's s delta close to u and it's also s delta close to the set

of all possible code words in this read solment code. And the question that mutual correlated agreement is asking is MCA is a question. This is very important. It's kind of difficult to understand like when I was first like thinking about this is like okay it's actually a question and the question it's asking is if H alpha is S delta close to U are F and G also S delta close to C. So essentially we're asking if H alpha is S delta close to U are F and G also S delta close to U0 and U1 and in this case they are and great so

that's this is good like and for most of the time we we want MCA like this is stronger security bounds in snarks so we want MCA so in this case so uh for a random alpha if h alpha as S delta close to C are F and G also S as delta close to C but this doesn't happen all the time and that's what we're going to cover next. So sometimes this does not happen and this is called an MCA error event in this case. So h alpha is s delta close to u but f and g are not s delta close to some code words u0 and u1.

Okay so in this case h alpha agrees with all of c but f and g only agree on a smaller set and again this is this uh restriction notation. So there does not exist u0 u1 which are elements of c such that f restricted by s is equal to u restricted by s and g restricted by s is equal to u1 by s. Okay. And and the main intuition here is the larger delta is the smaller s can be. So the size of the set s so as delta gets larger the size of the set can get smaller.

Okay. So as delta goes up, S can be smaller. This means there's fewer positions to match and the probability of an MCA error event goes up. Okay, so this is a really stupid slide. I was explaining this to my fiance and she was like got so tired of me like explaining MCA and all this crap. So I was like um she's like it reminds me of this like Instagram really stupid like AI swap content with these fruits or whatever. So, and I was like actually think like maybe actually you're right. This is kind of MCA. You can say it's uh related to this AI slop where okay, this strawberry woman is sort of like maybe a code word F. And the banana is not a

code word. It's just a vector. Okay. And this the banana baby is H alpha. And this guy is like a valid code word and we're just okay and us by looking at this image we're like the verifier and we're trying to check okay is this banana baby is it the result is f are f and g valid code words. That's essentially MCA. I know this is not mathematical but just to kind of wake you guys up after that technical explanation. Okay. So why is this even important? Why is it important to know the probability of MCA and measure it exactly? Um and the reason why is because it's used in fry and were which are components of proving systems

and they use random linear combinations to test lowderee polomials. So if we have better proven MCA bounds this limits the probability of a cheating prover. So when you're generating a proof [snorts] like we don't want someone to be able to prove something that they should not be able to prove. And if we have better MCA bounds, this means that we can catch this. So essentially, better bounds means potentially fewer queries, which means smaller proofs at the same security level. Okay. All right. So now I think you have everything you need to know to understand the $1 million Ethereum proximity prize, and Andre is going to walk you through that right

now. >> Yeah. Uh guys, if you solve this challenge, so you will get $1 million from Ethereum Foundation and you you will getting the friends forever with um cryptography professor of Tom Stanford, Dan Bonet and Ethereum researchers. So yeah, basically you can visit this website to learn more about this proximity price. So and uh basically it consists over like two problems we cover in this lecture. The first problem the grand MCA challenge. So uh we are given a rit solomon code word c here over some smooth evaluation domain l and the code has a constant rate which is means it

can be one of 1 / 2 or 1 / 4 1 / 8 or 1 / 6 etc. And for a given small epsilon star which is set to 2 in the power of minus 128 we have to identify the largest delta such as MCA error at this code C at this distance delta is negligible. So basically we have to keep this MCA error very small.

Uh yeah. So this is the MCA grand MCA challenge. What does solving the proximity price get us actually? So essentially it will get us like two things. Uh firstly uh smaller proofs for proof system based on Ritzelmon codes for example like FRI and the second there's no reliance on mathematical conesture. So we'll build provable system instead of conjecture based and uh the end goal of Ethereum foundation basically to formally verify the entire stack and then next uh Alex will cover result

beyond the Johnson bound. Yeah. So there was this bombshell paper that came out in September and this was published by Dao Kamir and and thou um and these results were inspired by the better codes auto research competition which I'll explain later. And so if you were a submitter to better codes you actually got cited in this paper. So like I I was I was reading this paper and I see my GitHub handle cited in this paper and I'm like what in the world?

like this is some like alien level math and I'm like cited here is kind of crazy but so essentially they were able to so better codes pushed the probability of MCA um keeping MCA constant but push delta larger past Johnson bound but this is for a fixed parameter set and this paper generalized this to all read Solomon code parameters um when the finite field is sufficiently charge and so essentially remember I was talking about that agreement agreement threshold so like the percentage of the agreement set and they were able to prove um like reduce the agreement threshold

but keeping the rate the same essentially and so there was this improvement so like the reduction in the agreement set um you they were able to reduce the agreement set but keep the rate the same and this is like some honest like alien level mathematics like uh like these hidden derivatives And we we wanted to explain this in this presentation but it was like we just didn't have time to digest all the mathematics here yet. Um so yeah so what did this paper actually lead to? So it actually led to performance improvements in in ZKVMs. So Proofkit had an 11% reduction in their proof size. ZISK had a 4.6% uh reduction in proof size and Lambda had about 4.8% reduction in proof size. Yeah. So what is this Ethereum

research foundation um like this Ethereum foundation auto research competition called better codes. So essentially better codes is asking this question about MCA. How large how big can we make delta such that the probability of MCA stays really really low and but it's for a fixed uh parameter. So for this very large finite field uh koala bear prime um you know this large domain and it uses interle resolment code essentially the same as just regular read solment code with some slight differences um and so this orange line here is like pushing the soundness bound above Johnson. So this is like zero Johnson bounds and

this is like pushing proven soundness above Johnson. And the blue line is essentially proving that it is not safe at a certain size delta. It's proven to not be safe. So that's essentially what the better codes competition is. Um yeah. So how can you contribute to better codes? So I would honestly just like recommend understanding the problem. So I've been like really nerding out about MCA and Ethereum Proximity Prize for at least the past six months. And I had a bunch of like lean for proofs that I was like before even better codes came out. I was like like told my agent let's just write let's formalize all this stuff related to reselling codes. Um and I was just like writing my own like hackmd

documents to this. And when better codes came out I just told my agent I was like okay take these lean four proofs that I already have plus all these like hackmds that I've written and let's just attack this problem like you know. So I'd say first step is understand the problem, explore the proofs and then you just set your agent loose but give it a direction like you once you've kind of understood the problem you'll have slightly more intuition where you can direct your agent. Um so yeah and this applies to all these auto research competitions. If you go to Yukon uh research um this there's many different auto research competitions. This is just one one of them. So yeah, so this is the last slide in our presentation. If you

want to continue to build intuition with MCA, we built like this website where you like have these, you know, vectors, you can change alpha and see where the MCA error event happens to kind of just build some more intuition with this. Um, so yeah, thank thank you so much everyone. Thank you DevCon. Um, if you want to reach out, these are X uh accounts and if if you have any questions, we'd be happy to answer them now. There any questions regarding MCA read Solomon codes results past Johnson bound?

uh the results are actually generalized. So it's um this paper essentially took inspiration from the auto research competition better codes and they cited everyone that submitted proofs but they generalized it to all parameters of um except for binary fields I think is different but yeah so like it's there's a definition here of like sufficiently large uh finite field f and they generalize that to all those parameters. So this is for all read solen code parameters.

>> Yes. >> Yeah. >> Yeah. We still need to dig into this honestly like this is um some really interesting stuff. Any more questions? No questions. Let's say [music]