recursive proofs for the rest of us! - Mohammad Jahanara

foreign [Music] thank you for coming everyone so my presentation today is about recursive proofs and it's titled recursive proofs for the rest of us by the intention that I'm going to give you an overview of what this technology do what you can use it for I mean building your applications here at the Hakata and uh a little bit about the different constructions that are out there more I'm going to be focusing more on family familiarizing you with the ideas and you know the vocabulary but if you have questions and anybody is curious about the details and we have time for questions at the end so please do ask questions okay let's get this started let's start from you know reminding you what is this zero knowledge business about so meet Ali Zamba Ali Samba are two nerds with trust issues Alice wants to convince Bob that she knows some w we call it witness Mustafa such that the function f of x of w is equal to some y okay so x y f all of them are public everybody knows them but W I see that and we want to do two things Alice wants to make sure W is kept secret and Bob doesn't have much time he's a bit dumb and slow and we have to make the verification as easy as possible so you already know a lot of applications that use you know this technology like ZK roll ups you know all of the different games like Dark Forest that use this technology I'm just setting the terminology for you here okay we want a few good properties out of these and we actually can get these properties with constructions that we know and love today first one is privacy okay again we call it zero analysis as well W must get Prime must be kept perfect you can think about this as you know some part of the input or trace of the execution something like that is kept pregnant sometimes because we really mean to keep it private sometimes because there is no need to share it the second part is integrity of the computation we want to make sure that you know if Alice is claiming I executed this function and this is the result we can trust Alice's claim if we do the verification and the last part is you want this you know proof to be quick to verify very short because again Bob is a slow in our you know real world most of the time Bob is the ethereum mainnet and Alice is you know some big super computer or sequencer or proverb that generates probes sometimes situation is a little bit different we get to that too okay I'm going to be using these boxes to show the functions like there is a function f inside the purple box which is the prover and the inputs go into the function and Y is the output of function but we get the proof Pi out of the prover okay and this is the first component this is what Alice executes so the proverb generates a proof Pi Pi is very short and we also have another component executed by Bob the component that's supposed to be very cheap and easy to run we call it the verifier and it gets you know the statement which is you know X and Y and also the proof and spits out accept of reject you know depending on if the proof is satisfying or okay two important points uh the first one is the computation has to be expressed as some sort of circuit for those of you who have seen it before it has to be a arithmetic circuit defined over finite field basically we cannot just write python code or solidity code and expect it to be you know proved there might be tools that do this for us but at some level it has to be translated into something called an arithmetic circuit and these arithmetic circuits can do only arithmetics over some finite field and this is going to be important during the talk so that's why I'm mentioning it now in particular that field is you know some called the scalar field of some electrical function but if you don't know this stuff this doesn't matter you can follow the talk that's why the second thing that I want to emphasize is most of the time the verification of the proofs has an expensive part like there is a part that's the bottleneck of verification okay and that part especially on the proofs that we deal with on ethereal magnets are you know something called a pairing check again we are using this you know finite fields that are obtained from some elliptic curves and some elliptic curves provide this nice thing called the painting and most of the constructions that are efficient and have you know short proof size rely on pairings and we have to do a pairing check to make sure you know the proofs are valid so the verifier does a pairing check to think about it conceptually if this stuff is new for you the pairing check is just checking some you know element a times some constant is equal to another element times another constant and digital elements A and B belong to some field okay this is a very simplified version of the pairing tape this is enough if you want to follow the thought great now now that we are all set let's get to the recursion business okay so the main topic is recursive probes and recursive proofs are basically proofs about other proofs what does that mean imagine we have a you know computation part of this computation is verifying some other proof is correct and then maybe we have other stuff to do as well like maybe we were doing some competition for a while now and we generated for the pro approved for the computation so far like maybe it's a computation that takes ages to run and I'm someone who were you know responsible for doing this competition I worked on this competition for 30 years and now I want to pass it along to the next person I have a proof that okay this is the proof for the completion computation so far this is the result now you carry on and the new person is going to first verify what I have done so far and then keep doing other stuff right so in the picture here I drew a green you know rectangle this is supposed to be the verifier remember we had a verifier function that was you know used by Bob or maybe it's a smart contract ethereum mainnet usually that verifies the proof is correct right so we have a component that that does the verification but now it's done inside another circuit like maybe we executed some other circuit there is a result and we created a proof for the execution of that circuit okay but this is a bit tricky now because we want to do the verification inside a new circuit okay and we do some other competition as well so to summarize what does this new proof Pi Prime says it says two things first it says I know a proof Pi for the you know competition that was done before like some f and that proof is accepted by the verify like this green box accepts the proof for the computation so far and also after some new stuff let's call them F Prime and this is the new result y Prime okay so what is good about this thing the good thing is you can fit more things like more computation more data on the same proof like imagine you have tons of data you cannot process it all at once for reasons we are going to talk about but intuitively you can think about it like if you have an Ever growing data like the ethereum chain itself and you want to do some computation about that and prove that that prove that that computation was correct you cannot expect it to be you know practical as the chain grows and grows and grows that's just one scenario uh and what is the overhead like okay we want to put more computation and data inside the proof but what what is the cost that we are paying the cost is overhead of you know executing these verifiers each time we want to you know pass along approve from some money to someone else and add more stuff to it we have to incur the overhead of verification of what what has been done so far let's get a bit deeper into what is good about this stuff so we can do two main things with this you know technology first one is compression and the second one is composition so what do I mean by compression I mean you know taking large proofs and making it small for instance polygon ZK Hermes how does that work inside they have efficient proof system in the sense that the approver runs very fast but it uses a component called fry it's a polynomial commitment scheme that's very fast to execute but it generates humongous you know proofs if you want to post that proof directly on mainnet you have to pay a lot of money and gas what they do is that they wrap their proof inside another proof and then it's short but this is not specific to them this is the idea that you can use in many different scenarios imagine you have a circuit if you know about plug circuits for instance and your circuit has many columns each column and the commitment to each column has to be part of the final proof so the more columns you have the log the larger is your proof but it's easier to design circuits with more columns so what you can do you can use as many columns as you want but then wrap your proof in another final proof that just does the verification of the first move and if the verifier circuit is small meaning that it has few columns then your final proof is as well which is nice so this is the first thing we can do with compression another thing we can do with compression is more about you know the size of the competition or data we are handling as I mentioned we can have scenarios in which we have a lot of data or a lot of computation and circuits are kind of limited in nature like they are limited by two things maybe you have a computer that has limited memory which is always the case like you have a limited time and you can't do the proof all at once like maybe you want to generate a proof for terabytes update okay that does that's just not possible because you know you are the proof generation process consumes uh that much you know memory you have to keep all keep all those stuff in memory because you have to generate commitments to this you know data and you know run ffts on stuff with the same size so that's not visible and maybe your you know data you're talking about is ever growing it's growing and growing and growing like you want to claim something about ethereum's chain so the idea here is we break the original computation into steps one scenario you can you know think about we do this like you want to do you want to execute a smart contract and generate a proof for it it's not proofer one way to approach this is to break the execution of the smart contract into op codes and you know recursively execute each up code and verify the proof for the execution so far and go on like that versus looking at all the up codes all at once and generating a proof all at once so what is the trade-off here the trade-off here is basically we trade memory with compute like we spend less memory at each step but we get to spend more time on this and you know incur the overhead cost of verification and at each step right but sometimes it's just not practical to do it at one go so we have to do this or sometimes maybe we are willing to pay more in compute one example of you know this is maybe we want to make a light client a ZK enabled like client for ethereum or a fast sync for ethereum and one thing that you know we have to do when we sync with network or you know we create a lite client we have to verify that the blocks are valid like the content of the block is valid like the signatures are valid execution is random stuff like that and one approach is for each block we send the proof that the block was executed correctly and everything inside the black is valid but we can go one step further and that's it that's you know generating a proof for the whole chain up until some point that the whole chain is valid suppose we want to do this if we recreate the proof for the whole chain whenever we have a new Block it's going to be very painful and costly but if you use this recursion Technique we just verify the proof up until the no last block prove the new block and now we have a proof for the whole thing again the second item is more fun and more relevant to you know building dabs and you know games and stuff like that so pay attention so what does composition mean it means that it means that you know the prover is going to show knowledge of something that he doesn't really know more precisely we initial proving that okay there is some W that I know but I'm not sharing with you that has this nice property claiming that somebody else knows a w that they didn't share with me but it's correct like it satisfies some you know stuff and I'm going to claim more things about that I'm going to give you an example and it's it's going to become clear think about the partial information gaps like poker when you're playing poker let me go want to step back think about partial information games and by personal information I mean any game that you know some player knows something that others don't know like there is something about a state of the game that only I know there is something about the state of the game that only you know like many games like poker Counter Strike whatever you don't know where I am in the map when we are playing countersect or you are not supposed to know at least when we are implementing these games in a decentralized fashion it gets tricky really quick because we want to enforce that play players you know change the state of the game correctly like if you are implementing counters Counter-Strike in a decentralized fashion you don't want to let me jump from one place in the map to another place you want to make sure I'm taking the steps right but on the other hand you don't want to me revealing where I am at the in the map okay so there is a simple trick like I hash where I am in the map and each time I take a step I open the hash as a witness like in the circuit as this W hidden W and then take a step update the pre-mage and take a new hash and give you the new hash something like that it's easy to do but it entails recursive probes because each time you have to verify the proof of the previous hash I give you and then I have to verify the proof of previous slash I give you and then updated something it this is the case when you're dealing with any partial information game and many games like many massive multiplayer online games like Dark Forest uh a poker implementation decentralized Counter-Strike serverless decentralized all these games involve this so this is a very powerful tool another example which is you know very practical is some you know about zikaish so zcash enables people transacting without revealing who they are sending their money to and who they got the money from stuff like that so abstractly think about that if you want to enable that on a roll up what what should we do so basically the goal is the roll up operator is not going to be able to tell who's sending money to whom right so it entails two steps if you're doing a transaction you have to create a proof for correctness of your transaction that you're changing the state of the chain correctly without revealing the addresses involved and you send that proof to the rollup operator we still want to get the scalability of stuff right so the roll-up operator is going to recursively verify all these proofs and create a new proof set okay there is a block there are these transactions that are proofs are not you know normal ethereum transactions I verified all of them and they are correct and this is the new state and this is something that you might you might have heard about is called zkzk roll up basically having a zcash as a roll-up in ethereal and the applications are you know endless if you start thinking about social applications like there is this one called it does that uh that gives you the the distance you have from italic without revealing the social tree like if I'm five steps away from italic and I know you I can give you a proof that you are six steps away from vitalik but you don't get to know what is my path to italic or what's the social structure here and stuff like that and how we do that we first verify that my proof is correct and then add a proof that okay I attest that you are my friend something like that again it's a very powerful primitive okay now we know about variable water snark proofs we talked about you know what is a recursive proves and what are accuracy proofs and what the why we care about it now I want to talk about constructions with you and this part is intended to be you know very newcomer friendly so I hope I can give you a at least a little bit of idea what's going on behind the scene so the most naive way to do this stuff is the way I was describing so far and that's implementing a verifier in circuit like we have a verifier function it was supposed to be implemented in solidity maybe on mainnet or no in code like rust or python or whatever let's let's Implement that as a circuit let's arithmetize that and put it inside the circuit maybe we have other stuff in the circuit as well but that's part of the circuit and voila we have a you know recursive we have enough technology to do recursive probes because now verifier verifies whatever we have and we can do more stuff so this is very architecturally simple clearly because it's easy to understand easy to analyze in terms of security the problem is it's very costly the overhead is a lot especially if we do it naively and I'm going to tell you why is that there are two reasons for this you know large overhead the first one is we have to deal with something called non-native arithmetics non-native field arithmetic arithmetics and the second one is often we have to do this pairing check I mentioned at the beginning in circuit which is a very costly operation so what is non-native arithmetics in one slide so elliptic curves they they're defined over two you know finite Fields first one is base field normally shown as FP and the other one is scalar field normally shown as fq you can think about this you know finite Fields as doing a regular Mass operations modulo p and Q like FP is mod P fq is mudq yeah in the simple case and the thing is when we are doing the arithmetic operations inside the circuit with doing those operations over F Cube so everything is done mod Q okay but the proofs the proofs are not P like they live in FP and if we want to argue about proofs inside the circuit then we have to do arithmetics over FPU sorry FP but using the fq elements so you see you have to do some simulations like it's like when you implement big num and you know C plus plus or stuff like that you have to do some things like breaking yourself into Limbs and you know doing the multiplications very carefully doing the carrier stuff like that so even arithmetics becomes non-trivial so for that reason and we call it a non-native arithmetics because we have to do arithmetic over certain field but we get to have access to another field okay so that that adds a little bit of overhead but there are tools out there that help you to do it you don't have to implement it like if you're using circum there is a circum pairing library and circum bigint library and if you're using Halo 2 there is a wrong Halo 2 so there are tools for available for you to do it the second an idea you know to you know get away from doing this you know non-native stuff is using something called cycle of leptic Curves so you don't have to use the same elliptic curve each time you're generating a proof you can switch your elliptic curve from time to time and the idea is if you have a curve with parameters p and Q like the base field is p and the you know scalar field skill if you have another field with the alternating parameters like q and P then each time you want to talk about something in FP you just alternate to that curve and one of the main contributions of zcash people is creating a pairing friendly cycle of peptic curves called Palace and Vista the problem is we cannot use that on ethereal because an ethereum we only have this one curve called bn254 and bn254 is the only curve that's supported as a pre-compiled other curves if you want to do them we have to implement the solidity code and that's very costly it's not worth it but the problem is people proven mathematically that there is no uh efficient parently you know cycle up electric curves for bn254 so there's no hope this approach is kind of that's going to work for us on ethereum I have two more you know ideas which are you know based up the works that came out in last two years the first one is something called proof accumulation so we want to do some recursion maybe we want to do a hundred steps of recursion to prove something recurs on it recurs on it recurs on it and at the very end we want to post the final proof on mainnet to be verified by some smart contract okay the core idea is maybe we delay the hard work to the very end and remember what was the hard work it was this pairing Checker stuff right and if you do that and if we do recursion for many steps many iterations we kind of get to amortize the cost of you know that one time heavy because over all the steps and kind of it makes sense now so the idea is we accumulate probes which I'm going to hint at a little bit in the next slide so we accumulate proof somehow somehow combine all the proofs okay and we verified that this accumulation is done correctly so we have to do some verification in circuit but it's not a full start verification it's just a verification that the accumulation is done correctly so the verification is much smaller now like maybe just 10 20 of the original like the costs of verifying the whole star okay and on top of that we never do the hard work in circuit like I told you at the very end we have to do this bearing check but we do it in a smart contract on Elbow so it never happens the hard work never happens in circuit which is very nice uh so I'm going to quickly go over this slide because we don't have time so the idea is we use this tree called random linear combinations we combine all the you know pairing checks with random coefficients and then just do the pairing check for the combination of all of them and you can prove that very high probability if the final one checks out all of them would have checked out the other idea is statement folding this one is a little bit different in the sense that it happens a little bit sooner in the life cycle of the proofs in accumulation we have to generate proofs for each step and then we accumulate right but in a statement folding the idea is we don't even generate the proofs at the level of statements we accumulate the statements and then we get to generate a Fool Proof when we accumulated all the statements okay so the core idea is very similar we want to delay the hard work as much as possible but because we do it a bit a bit earlier in the life cycle of the proofs we get to do more saving and this is very new like these ideas came out maybe uh mid-2022 so this is very new and Yep this is my final slide so basically in circuit verifiers proofs leave their full life cycle and we pay all the cost accumulation schemes we get to avoid the verification until very end and a statement faulting we don't generate the proofs at all like we do just hit some proofs but generate full proofs at all until we accumulate we folded all the statements so that's that's all what you can do now so I want to encourage you to use you know these ideas of recursive proofs think about them come up with ideas how you can make personal information Games Social applications that you know somehow exploit this power of recursive probes the other thing you can do many of these you know ideas came out very recently and there are not good implementations or some of them don't have any implementation so you can go out there and you know find which one you like more and start contributing to them and the last item is there's a lot more to learn here I'm happy to talk to any of you if you want to pointers to more resources and learn and just educate others thanks a lot [Applause] there's still maybe libraries and or things for you know Jan equals so there are certainly many Tools in particular I mentioned the circum pairing and circum big end and around Halo 2 these are libraries that you can use to implement in circuit verifiers or in circuit you know accumulation verifiers or folding verifiers stuff like that um but there are tools that you know do the whole process for you but on the top of my mind I don't have them but please talk to me later okay oh yeah I mean absolutely yeah yeah that's a very good question so uh the way the way we generate the proofs is that we most of the time use kcg commitments and kcg commitments works like this like we take something and put it in exponent like in the elliptic curves and when we do that we move from a group to another group like and uh like another one field to another field so the commitments are you know in this other field like and that that's why you know the LLP points are pairs of uh points on base field like FP and you have to deal with them when you're dealing with the proof so that's why and you can't really get away from that like that's part of every Construction