ZK11: Folding, Codes and Linear Algebra - Alex Evans

Transcript

[Music] it's a it's a real pleasure to be at a zik summit in Athens no less at the planetarium I was reflecting this morning that this is a particularly good choice of venue among other things because it's a sober reminder to crypto projects the world over that the name space of the cosmos is fully saturated there are no more uh celestial bodies or phenomena for you to name your projects after they have all been taken uh so please keep that in mind when you're starting something new the second reason is this is perhaps at

least when I was growing up here in Athens this was the primary place for Middle School field trips I think I went on three I changed middle schools a couple times so they they start you over again which I hope serves as a great inspiration for the aspiration of today talk which is Simplicity and in that context what I want to do is I want to share what I hope is a parsimonious framework for understanding succinct proofs and protocols this is not the most General such framework that we could come up with but just the simplest one that can nonetheless allow you to do a little bit of damage the idea here is of course succin proofs and protocols you take

something very big very hard to verify potentially cosmically interesting and reduce it to something simple and pedestrian uh with a little bit of Randomness and incurring some soundness error along the way so we're going to try to describe why that thing is even a reasonable thing to do in the first place using just a little bit of linear algebra a smattering of error correcting codes and perhaps a little bit of basic probability some notation is going to be introduced in a smattering throughout but that's going to be the core idea and to start with oh and I should say this is part partly joint work with my colleague German jerus who co-authored a paper with called U er um zero knowledge proofs and linear algebra which we call

the end of last year I think we have I might have a QR Link at the end and the there's a separate sessions I forget like CK study sessions or whatever it was with gearmo where he presents that whole thing as a course this is a condensed version of that we're going to go over some of the basic results in that paper just the notation and the framework and then as a treat for all of you we're going to do something that's not in the paper that's somewhat new okay so we're going to start out with Frameworks and we're going to ask what is a good framework and I'll let you be the judg as whether this is a good framework or not it is an attempt at a good framework and hopefully a good framework can you utilize a simple set of tools to nonetheless explain a lot of

interesting things and I'd say broadly in cinc proofs we have two types of Frameworks ones that are super General and describe almost all protocols at a very high level of abstraction and general reductions therein these are more recent and are now starting to become more popular in some papers that have been coming out more recently they are nonetheless mostly blunt they're work at a level of abstraction that's very high you can't easily use them to prove things or construct new types of systems or protocols and then there's like application specific things which you can use in constructing proofs of soundness of whatever protocol you create or creating protocols and the like so this is going to be somewhere in the middle okay and we're going to get into it we're going to hopefully just

create a library these things produce a little bit of notation and then see how these things could compose potentially in interesting ways to create new types of succinct proofs and protocols so hopefully as a positive side effect of that we can understand why intuitively succinct proofs work and potentially use them to do new and interesting things which I'll try to do something moderately new and interesting in the second half of this presentation but hopefully not straying too far from the goal of simplicity okay so at a high level I'm going to go over a basic protocol that everybody should be familiar with which is going to be the polinomial zero check this is ubiquitous we use it all the time we

basically do that in linear combinations that's the punchline of this throughout ZK so we're going to go through that we're going to introduce the notation and the framework that we have in the context of an example as opposed to in the abstract and then we're going to start doing some damage with something a little bit more interesting which is going to involve some work by I see Ben diamond and Jim Posen this paper on logarithmic Randomness we're going to try to replicate at least a big part of that proof with what seems to be a slightly better sound and that's going to be uh thanks to minro who got a really good generalization of it so okay so let's start polinomial zero check we all know and love we're going to start with a field we're going to define a polinomial over that field over a

certain degree bound and then we're going to say that if we evaluate that polinomial at a uniformly randomly chosen point in the field and that evalues to zero then we can infer with probability that the polom itself is the zero polom this is pedestrian I'll pause for a second but everybody should be familiar with this by now and so what we're going to do is we're just going to rewrite this using the first thing we're going to introduce is probabilistic implications and we're just going to say in the standard way that F of R so F evaluated R equals z implies with soundness error at most P that f is identically the zero polinomial okay and the soundness this p is just given Again by the degree Bound in the standard way we we all know in

love okay so now we're going to rewrite this a little bit more and we're just going to introduce a little bit of linear algebra it's going to say the same thing we're not going to do anything new or interesting thing here so we're going to start with the generator Matrix with the rolon code or B Matrix we're going to pick a random row index by R of that Matrix and then we're going to take this product of gr transpose X we're going to say that that is essentially equal to F of R it's sort of by definition and then we're going to check that that gpose R of X which is the coefficient Vector of the polinomial just going to take the coefficients and put them in a vector and then multiply by gr transpose we're going to check that that is equal to zero and again

with probability with soundest error at most P we're going to infer that the coefficients are zero this is equivalent to saying that the polinomial is zero so so far we've taken step one we've taken it into probabilistic implications step two we've done something very basic and trivial which is we've just re written it not involving the esoteric properties of polinomial or anything just rewriting in basic linear algebra again I'll pause you as a little bit of math on this slide but it's very basic okay so why do this I think the first thing is you can ideally start to utilize the composition of these implications to prove potentially more interesting things this is not a remarkably interesting thing that I'll do here but I'll just give you a basic example we can chain two probabilistic

implications to say something a little bit more complicated than the single VAR po case so let's take a coefficient Matrix of aari polinomial with degree bound n minus one in each of the two variables and then we're going to take two rows randomly indexed by R and RP Prime respectively of the generator Matrix and we're going to do the standard Matrix Vector product so we're going to first multiply by gr that Matrix and then by gr transpose and we're going to check that that thing is zero which is going to imply that the middle thing here is equal to zero again with soundness error at most p and then which in turn is going to imply that the entire Matrix is zero now these

probabilities will sum across these two implications in the worst case which is going to give us our standard swi zipple bound we do actually have in the paper and this is not to put on slides at a conference certainly not at the end of a conference a slight tightening of what we're usually we usually use in the sort zle Lemma that's an appendix in the paper if people are interested in checking that out Okay so we've done nothing interesting or new at this point we've just introduced new notation and that's just going to be useful now in moving on to something that's a little bit closer to The Cutting Edge of the field no pun intended we will prove a hopefully slightly tighter version of the result of logarithmic Randomness by diamond and

Posen this is so we're going to start with a Subspace with distance D and we're back in code l so what we're going to refer to as distance D here is just going to be the minimum disagreement between let's say two code two code words in a code okay and then we're going to define the distance of a matrix with two k columns two to the K columns as just take a matrix I probably should have had a slide with the definition here so just take take a matrix X and take a take another Matrix y whose columns all lie in the Subspace and consider that difference of some any Matrix X and Y okay and take the closest one of those

for example and just say what is the minimum number of so what is the number of sort of zero nonzero rows right so the columns we transposed it so normally you see it in the code words are in rows I see you struggling with that one we just transpor it like it just makes the linear algebra a little bit easier so so take the The Columns right and subtract out the ones where the columns are entirely contained in the space and then consider the non-zero row so if like two columns right are not in that then that would just be counted once right so two columns differ at that same Index right that's just going to be counted once okay so that's going to be the notion of distance of the Matrix to the Subspace and the rewriting of the basic result is

going to be that we're going to take this Matrix Vector product of this Matrix x with this tensor product y r okay so notice again this is a logarithmic number of random elements we have two to the K columns we have K of these random entries and this Matrix Vector proba is going to be a sufficient witness such that we can make the implication that if the distance of that to the Subspace given this this this proximity parameter Q Which is less than D over3 again with soundest error at most P implies that the original Matrix was close to the Subspace and we're going to do it with what seems to be a slightly better bound than well we gain a bit here it's not very significant but slightly better than what we've seen in the paper so far okay so this is a

particularly interesting result not only because we love to Shi allano our investors and all the time it's a really well-written paper you should read it it is also one of the fastest breakdown like schemes and the main reason for that is is that you can view this x yr product as a partial evaluation of a multilinear polinomial which lets you merge the query the the commitment and query phases of breakdown SL Leo like protocols it's also the original beus paper uses this as the a the core they do some cool things with packing and so forth it's not necessary that you use the really cool data structure and beus that was presented earlier today with this particular framework but I think still the fastest prover of for beius is using this so maybe Max that fastest Pro

period uh is using this abstraction so we think it's particularly interesting and happens to be a more recent and slightly more involved result to hopefully demonstrate that you can do cool things by just chaining implications together okay so we're going to start with something that is due to Min sitting over there who got the who got the J we got it for D over4 and he was able to generalize it all the way up to D over3 for the proximity parameters so we're going to take two matrices and we're going to take this linear combination with these coefficients given by again these R Prime and 1 minus r Prime which again R is uniformly R Prim is uniformly randomly drawn from the field right and we're going to check that that thing is Q close to the the vector space to the

Subspace and then we're going to say with soundest error at most P that the Matrix whose columns consist of X1 X2 is also close to the Subspace and we're going to do that with this bound we are not going to prove this here this is sort of you have to do this in the old fashioned way you have to sit down like you did with pencil and paper and prove it and we make no claims that probabilistic implications will suddenly solve that for you you still have to do a little bit of math okay so now we're going to take that result and just by using a little bit of induction and hopefully just chaining a couple of these implications together do all the rest of the work and again this is what we're trying to prove which was from the previous slide that this Matrix

Vector product if we check that then the Matrix is close to the Subspace and we're good and we're going to do it of course by induction so first we're going to start by sort of unrolling this tensor product I'm going to take that very last entry and separate out we're going to call this everything all the K the tensor product all the way up to K minus one uh y Tilda and then we're just going to take that final thing and tensor that's just this is just definitions of The Chronic product okay we haven't done anything and so given that these things two these two things are equal their distance is of course the same to the Subspace and then this is the inductive hypothesis so we're going to say very clear like this is we're just going to

say we're going to test the thing on the just as we did before on the inside with the last value so again this is just the the left hand side here is just the right hand side of the previous one the inductive hypothesis that implies with soundus er no larger than kus1 Q +1 over the size of the field that the this linear combination on the right is itself close to V and of course that is simply the basic step that we had in the previous slide so we're done and you just need to go and sum across all the k random values and of course you get the claim bound of k q + 1 over the size of the field I'm going to pause here I I want

to see the look of comprehension specifically on your face and then I'll move on seems espe assing yeah yeah we should go over that separately that it's actually really nice it's pretty simple too we can go over it okay so this is the punch line I think this is what we set out to prove I I think what's nice about it is you can chain these probabilistic implications really nicely together and they work very nicely the proof itself is like page and a half you put everything together it's including the basic step it's like a page and a half which is really nice the notation is really clean and simple and it intuitively maybe this induction step gives you an indication as to why this tensor code thing is the right thing is you're taking these

linear you're basically taking these matrices and folding the columns at every step right so it's like fry maybe folds that way and you're folding this way or something so hopefully that gives at least some indication to someone that a framework like this that's not the most abstract but still is sort of sharp enough to go in and prove some results is an interesting one and hopefully allows us to clean up and simplify notation compactify notation of things that we already know and maybe even do some slightly new things like we did today so uh Min thank you for the contributions to the Bas of proof and thank you everyone it's all open up to questions uh thanks Alex I I'm wondering

how does this translate down to the formalisms of probability like the the aums can you write this implication as a statement that the probability of this and that is bounded by this and do the properties that you're using such as I I'm guessing transitivity or whatever translate down to the axum of probability for example I'm wondering like what is your probability space all these things is this in the paper yeah yeah we we don't TR we don't like have like a sample space and like Define a filtration or whatever over it like it's very very basic probability that you need you're just think of it as just normal logical statements like contrapositive whatever you want to do and chaining together logical implications okay and just now imp

posing soundness error on top of that right there's like apparently another we had never seen we kind of made this up right cuz we that the way this came up is we were writing some of these proofs out on a whiteboard and in our office and we just started rewriting them in this way because first of all take less space and it was nice and so it just also felt like a good way of doing proofs but you can chain them together and compose them and you can also take Contra so forth and just the probabilities would either negate or they would sum like you can take a union bound and so forth sometimes you would want something sharper than that right like for instance here we just at the end we just summed everything together right which turns out to be fine yeah because in in cryptography as you may

know like there's often the problem of if I if I go a little bit too high level and I I use probabilities and implications for example if the number of implication steps is dependent on the execution for example it's like a polinomial of the whatever security parameter then it actually doesn't really work out right so you need to be very careful of what I'm doing here that's right that's right that's right you don't you don't get to avoid that okay yeah then then oh wait there's somebody in the back too okay so we'll we'll take both yeah so the uh the key result which is the in the background yeah so that's exactly the same as the one in Ben paper right so that is exact basically exactly the

same same so the Improvement is just the two right it's just the two Factor yeah yeah yeah and Ben is very good at math so we should we should go back and triple check it just to make sure yeah thank you yeah so it's uh Q Plus one divided by the field side yeah yeah cool thanks there you go I is this on yes it is uh yeah and by the way um you you shouldn't under sell getting rid of that factor of two it's actually in in the most recent version It's stated as like a would be nice right like kind of conjecture essentially like can can you get rid of that factor of two so that's actually pretty good if if if if you can maybe we just add it to the

paper something yeah yeah um but yeah I I was just going to follow up on this I mean to me it's it's pretty clear how you make this precise grounded in probability Theory you basically say that the the locus of the parameter space where the leftand thing is true and the right hand thing is not true right namely where the implication fails that that Locus would be bounded in size by something and then when you do the chaining it's kind of clear that you're taking a union of these locai right and and of course you can take a union bound there and then you just add them so to me it's pretty reasonably evident like how to unroll this formalism into something that right is that fair yeah

exactly and far better stated than me as always does it work yeah so thanks for the talk so I fully agree like uh I mean all the proof systems are typically built uh by by an IOP where you have all the random reductions uh seems to me like if you when it comes to linear algebra that might be maybe a good uh generalizing framework for General linear codes but it seems to me just or did you ever think of like a complimenting picture that uh is more Centric to algebraic geometry codes you know even even the example

with the vont Matrix and so on it can be all uh again played down to schal simple uh in the appropriate setting not claiming exactly in that way but uh so it seems to me like there is a lot of potential of uniformization of all different struct let's stay for a second just with Univar snarks or the IOP there's a lot of potential of uh of unification in terms of the algebraic objects you use on which you do SCH simple personally I'm not but this is just my personal taste I'm not so much a big fan of linear

algebra uh CU what you often lose is the connection look even at at at ffd based encoders uh you could like bold you could write it down you know uh with all Define your F what do they call it follow followable code yeah and I have a funny story about that what you in my opinion it's just a personal opinion might might be wrong here is uh you can do foldable codes that's just as a generalization of with Solon codes to some algebraic geometry codes including fras like additive ffd codes and so on just long questions short did you ever think of like a complementary

unifying framework in the sense of uh the algebraic codes or the GE algebraic objects yes so in this case we so a few things one is generally speaking the abstraction of linear algebra is you can explain to an undergraduate and so forth so in this setting funny enough actually with with uh bfold the thing that we have described so we have in our paper sort of a pro a basic proof of fry using just these probabilistic implications and it turns out that actually the thing we used was itself based which fil builts very nicely and you can do it in that framew now could you go a level higher in abstraction actually where most of the things break down is that we

end up just working in code based things in general right and so the higher level abstractions that we've been mostly curious about have been can you have like a module theoretic generalization for example the stuff that we have here which turns out to be similar to some other work in terms of more General codes and constructions there in any linear code would fit naturally inside of the framework right because you can describe it simply as you take a generator Matrix and multiply it by a vector right H thanks uh it seems to me exactly you know but that's that's my personal opinion so once you move away from the algebraic picture to generator Matrix you lose a lot of uh background

information so potentially but it turns out to be sufficient to prove things that are useful in field so the question is like how much machinery and abstraction do you need to prove the things that you want to prove agreed on that and what is the barrier to entry for somebody coming in to utilize because it's ites the idea of the proof no you have super like write a high level program in assembly yeah yeah that's danger that's right that's right and I so I would argue that's that's assembly right it's like what is the minimum set of things that I actually need to do something and and by the way I totally agree with you I think there are there's Frameworks at multiple layers of abstraction that are interesting I think there's like ones that are like super abstract now and you

can't use to do anything and then there's ones that I just need to come up with a new framework every time I'm looking at a new system even though the tricks are overlapping every single time to come up with my proof and uh I'm not I'm not that good in order to be able to have to figure it out every single time and you can reuse a lot of the same trick because it's basically the same that the punchline is it's all the same stuff almost every single time at least pertaining to these codes thank you yeah but I think that would be a very interesting generalization we should chat about it I think it's you make a really good point do we have any other questions we have time for a couple more take is it's a full room so don't

be shy yes they are shy more okay we have a few minutes for your just a side question you were mentioning uh you you did write down proof of fry exactly probability probabilistic redu reduction chain you also take into account The Joint query oh sorry you take into account The Joint query joint query like you like the classical fry not like stir where it's more easy to work round by round from round to round you know CL uh the classical fry where you just have the commit phase and then you jointly query all all the committed

to or oracles yeah yeah so you don't have it's not like commit and then query in the and next round is again commit independent queries and so on yeah we just sum in our case I I can pull I can show you the proof but we just yeah the queries are correlated in that case I I don't I I missed the stir talk this morning so I don't know how to compare the two that's the only version of that we consider is one where they're exactly correlated I think in their case you have to your queries are like you're switching domains at every point I mean St seems to be much simpler I'm just asking because I was doing hard you know really understanding the right form of

framework for I mean first of all reading a proof in in the proximity gaps paper from uh uh you know what the soundness proof of fry you know because of the joint query it's not that easy as usual and you have to be very careful in in writing down what is the relation you reduce by each folding step uh because you have to always take into account the whole history and and and how it correlates in some sense so so I was just wondering if if you had it yeah we have a naive one you might need all of that stuff to get a to look to be honest with you to get a tight version ofy our version of fry is pedagogically

interesting we think right so we don't get a great bound necessarily so you might need to consider sort of that adaptive Behavior across you're quering just once and so forth in Practical protocols right so what we have is can you explain to somebody pick somebody off the street that knows algebra and say hey uh let me show you take take a take a Subspace and consider a recursive substructure right where you can sort essentially exactly what bfold realizes that you can generalize this idea fry to a broader code when you you consider that you can decompose the spect okay so so so you sense and then we just sum across and then it follows the bounds I guarantee you the bound is terrible but

but it is at least for me it was great to work out a proof of because I I I read the I read the proximity gaps papers and so forth and just the machinery and work that needs to go into it I pull out half my hair and I don't follow I suspect that is a shared thing there are people that are obviously far smarter like yourself that have actually done damage with these things so um but that that's that's the objective anyway I can show it to you maybe we can strengthen it without getting too far down the rabbit hole of uh that original proof but my guess is you might need a little bit more Machinery to get something fully tight here just happen to be really nice I think you can get something tight just very nicely because it just fits directly into the

abstraction you're already working in this code setting you're already dealing with these subspaces fry is a little bit more involved at least to my eye yeah I agree thanks yeah hi can you just uh can you just show the inaction step really quick yeah by the way I do need to jump to the main stage um so I can show it to you maybe offline yeah I can um but thank you took longer thank you everybody I'm sorry for that let's catch up after