STARK Recursion / Avihu Mordechai Levy

EthPrague 2022 · June 2022 · 19:47

Avihu Mordechai Levy explains STARK recursion at ETHPrague 2022, the technique of proving the validity of other STARK proofs inside a new proof. He presents it in the context of StarkNet, a validity rollup, also known as a ZK rollup, on Ethereum, where recursive proving lets many computations be compressed into a single proof.

Speakers

Topics

From EthPrague 2022, hosted by ETHPrague.

Transcript

foreign [Music] yeah hi everyone can you hear me well great so I'm a view I'm head of product at starkware I'm very happy to be here today and talk about recursion um on a personal note I started to work at starkware actually from here from paper Hab in police I spent my almost my first year in Stockwell working from there so for me it's uh

very nice to be here and give this talk today um okay I only have 20 minutes and there will be no question time because there is something right after that so if you have any questions feel free to come to me after and ask I do want to try and present in just 19 minutes what is recursion and basically it's going to there I'm going to separate it to three or four parts I'm going to talk about a little bit about the background because well you need to know something to understand what's happening in this talk but it's not so much and then I'm going to explain what is recursion why do we want recursion and at the end if I have time I'm going

to touch a little bit on what is the timeline when are we going to see recursion in production for Starks okay cool um so what you should know is basically this is like a short and not comprehensive list but I'm actually I I'm going to touch very briefly on the first three points and the first point is like nice to have if you know what starting is great if you don't that's very that that's pity and you should come to me after and I will fit you with all the details great so a little bit about uh Starks proofs and Cairo basically the concept that the concept that you need to be familiar

with is that there is an ability to take every computation with uh that takes time T to execute and generate the proof uh for this computation and the entities that generate the proofs we normally call it the prover there is also a separate entity which is called the verifier and the verifier only takes log T time to verify the correctness of the computation if you get a proof what Cairo the pro the programming language I mentioned earlier what chiro enables is basically to take any logic any computation and have it written in a way that it can be efficiently proven okay great so this is like very um

simple heuristic of how Cairo Works um you want you want your program to be proven you write your program in Cairo then you have approver on the left side uh she's running the Cairo program on some input let's say input X you can think of the input basically as a list of transactions most of the time and the program being something that takes those transactions and does something with them on the state and eventually it outputs Y and the verifier basically wants to know that running this Cairo program on some out input really generate the output Y and that's basically how you should conceptually think on what's Happening Here okay great okay I this is something I must explain and most of the people are probably not

familiar with so we have approver that a special prover machine that we call sharp sharp is like a shared prover right and what sharp knows to do very well is to take Cairo programs that are not necessarily similar for in this example I I took Stark X immutable Stark X rare and Stark net from the proverb perspective those are all completely different programs they don't they can be with completely different Cairo code he can still take all of those with different transactions for each so when you see her job and I'm not going to get too much into that but when you see her job every job is basically a program in a set of transactions you can

take different programs with different set of transactions and prove in a single proof proof all of them together and verify it on ethereum in one proof in one well it's not one but one proof several transactions okay so conceptually and also in practice sharp takes different program unite them to a single proof okay and that's what you need to know about Sharp great okay so now I can start talking about recursion are you familiar with these uh I guess some people are familiar so basically admit I haven't seen this particular chapter for a while but the basic idea that you see in the picture this is from a TV show named Rick and Morty and the guy that top is Rick and he's driving a

spaceshift a spaceship sorry and he has a in this particular episode is a engine is broken so he has to go inside his engine and it turns out that he created basically a completely a full Universe just to generate energy for his engine so when he goes inside he finds out that this universe that he created that well they were too lazy to run everything to create the energy for his engine so they created another universe that created the energy to run whatever they need for him to run his engine and you can imagine that this universe are also they're also being lazy so they created Another Universe yeah you understand

where I'm going okay so actually this kind kind of reminded me what you're going to see with Stark recursion so if you don't want to take anything else you can always go back to Rick and Morty that's what I do sometimes it will be good for you to refresh your memory okay so I want to explain in a couple of sentences what is recursion right because you know recursion probably from programming or maybe from other uh areas of life but I want to explain what is recursion when it comes to Starks and proofs right so what you all if you know prove some before this is what you're normally used to there is a program doesn't matter what it is can be Stark net or anything else and up until now what you're used to is that we generate the proof for the

original program and then we verify the proof in a verify program and that's that's how things works in the normal life and that's how things works today sharp takes computation generator proof send it to the verifier own chain but the very fire program is a program by itself it's a program by its by its own right so the same way that you can prove any other program you can also prove a verify a program and basically when you prove a verifier program you don't prove directly the original program you prove the verification of the proof of the original program right take a take a

second take a two or three seconds okay have it great and then you can verify the verification instead of verifying the original proof of the program you can verify that you verify the program and of course you can also prove that you verify the verification and so on okay so that's that's that's fantastic and that's very cool and we do things because they're cool but but then the question is okay so why why do we want to use recursion what are the reasons that we want to do something crazy like that okay I'm gonna skip that um so here's a clue about the motivation so the clue is that if you have a

program that take these steps then proving it takes roughly also two steps but if you already proven this proof then proving the verifier only Tech log steps which is much in most of the times it's much much much much shorter to prove once you have it and it's like compared to the original proof of the original program right so here is something I can do and I'm going to explain it in a second okay this was a clue um it's okay the first thing that you want to do recursion for is basically dramatically reduce the gas cost and increase the proof capacity as we have

today on chain so why is it why is it like this well today um you can imagine you take a program a program can be Stark in it and it gets many many transactions right so you collect those transactions and at some point you take you took the largest machine on Amazon AWS or gcp and you can only push yay many transactions and that's it because after that the the machine run out of memory run out of core you can't you can't push larger uh computation inside you can't have more transaction in single proof so if you have 10 000 transactions let's say that means that an approved verification cost 5 million guys then it puts you a limit on how low

can you go with every transaction right because you know the tent you can put up to 10 000 transactions in 5 million guys which is amazing but that's your limit and we want to do better we want to do sometimes 20 000 transactions we want to do 100 000 transactions so then this is a place where recursion can actually help because if before all you could fit is program a with these steps then now you can use this scheme prove every program separately but then prove the verification of those programs and two times log T is most of the time way smaller than T so now you could you can push two like you could double Your Capacity meaning pay half the gas cost

in the best case right and still use a single proof on chain and it goes further right it doesn't have to be two programs you can also do it for four different programs and you can increase your capacity by four times and basically it goes on and on and on right because this can be nested this can be a tree of arbitrary size almost so this enables us practically to take the gas costs to be like infinitely small and the proof capacity to be extremely high so that's very very cool and this is by itself already why we would like to have recursion but there are a few more things and I really wish that I would have more than

nine extra minutes to talk about the other things but I don't so you're gonna have to come later um but I do want to mention a few more things latency you remember that I introduced sharp a few moments ago so imagine that in in real life those jobs they're not coming at the same time you wait for transactions in immutable you wait for transaction in severe you wait for transactions on starknet and at some point mutable is saying okay we have enough transactions we want it to Unchained so the same their job and so where comes later and start net comes later so in practice what is happening is that you wait and wait and wait and wait for enough transactions to fill up enough jobs before you start proving and

when you do start proving today it's a huge proof that takes hours to proof right so overall you get latency from two places one is you wait for transactions and the other one is that you wait for a single huge proof to be proven and that's going to improve dramatically with recursion because now let's say that immune we are waiting we are all waiting we like to wait and then we have job zero arrived from immutable and instead of waiting we can just prove it so RJ here stands for recursive job basically we took the original job from immutable we didn't wait for other jobs to arrive and we proved it and because

we proved it we do the same for uh the job from swear but now we can just take two proofs two basically proofs with the verifier program and unite them and prove them all together right so we didn't wait for the for the job for Stark to arrive we already proved the jobs from immutable and swear and we do the same with starting a job and by the time we have all three jobs ready to be sent we already have them proven so we got two things one we don't have to wait for the line of transactions to be fulfilled anymore we can prove things as they arrive and two the proving itself is faster because it doesn't necessarily have to be on a single huge machine it can be splitted to many many many machines that take

part partially smaller jobs and run them in parallel so if you want to imagine how it looks in sharp in the general case there is a algorithm that takes jobs that are waiting on the Queue recursively proving them if you find still recursive jobs you United them and so on and so forth this is just one potential outcome it doesn't have to be that way it really depends when the job's arrived but I'm not going to get into it now okay this is another topic that I'm really touching um in a minute or two but I think we can you just about this I can probably talk an hour um so this is basically the general idea of layer three

um I like to picture it and also in my in my head it looks like this so I don't know why but the base layer for me sits in the top and you're never going to see it including not in my slide because nobody agrees for me to put it that way but I can put it in a picture so for me it's like starting it all the way down basically that the general idea of layer 3 is to say well we run things on Stark net and that's great but sometimes for whatever reason in the world you want to have your own environment you want to have your own Uh custom Stark net you want to have your own static system maybe you have a different VM and you don't want to relate to the way that star gets to

Stark net VMS are created maybe you have a ZK evm system that you care about maybe you have I don't know what I took orbit VM as an example maybe you have your own whatever MEPS or or whatever VM that you can think of so what you can do is you can write your VM in Cairo whatever Implement your VM State machine in Cairo and then use the using the Cairo verifier that we already wrote for the recursion you can deploy the cover verifier on stack that we will actually do it for you um probably soon you can use this card verifier to prove any such environment separately so you can have your own personal environment within starknet it has all kind of benefits you pay even

less than Stark net you control the environment yourself you can have a different VM you can even imagine a world where all each one of those there are three has like completely different smart contract system but they can interact with each other and it's much much cheaper to know it than doing it from layer 2 on ethereum so I know it's not maybe it's not gonna be as clear as I see it right now but take a moment think about it this is like you can put in different environments with different VMS and different state machines on top of starknet and you can prove them and they can communicate with each other can I have ZK VM smart contracts talking with some customs Target smart contrast over starknet can be very cool

um what else I wanted to mention so I have four minutes I'm gonna attach this in a very like yeah let's do it so this is actually something pretty cool that I think most people don't understand yet um normally at least in Starks uh there is some complexity in the verifier this complexity comes because in Starks the verifier has to know the program in some way it has has to know whatever is proving so the Stark verifier of Cairo has to know the Cairo VM um constraints and we want to do things more efficient which means to in to present more constraints for example people are

saying we want to approve ketchak very efficiently then we are introducing a ketchup building a catcher constraints that goes to the verifier and that makes over time the verifier complex and expensive and we don't want that nobody wants that with recursion you can actually say well you want to add complex built-ins complex restrictions to prove things faster but you don't want to come to over complex Your solution very far that's fine prove everything that you wanted is complex on a higher level of recursion and then just use this verifier to prove it but the solution verifier will never need to be aware of those because the intermediate

step will not use them and I don't know like it it just it helps so much in the in that you can now do very over complex things on on our side you can prove things much more efficiently but the solitary verifier is not going to be to get hard and sometimes you yeah you can keep it very very simple that's basically what I want to say about it um you can do proof compression which is very very cool so basically the idea to if you have already several proofs that you generated over time for example proofs for liability of Stark net or the validity of Bitcoin or any China and now you you had like approved every hour let's say then if until now you just end

up with having like 100 proofs or whatever it is per day that you had to download and rerun now you can unite them to a single proof all the time which is I think very useful Okay one minute to talk about when so I the reason I'm actually giving this talk it's not like well if you think about recursion some concept that people have been talking about and sometimes implemented for specific use cases already in the past the reason I'm talking about it is that recursion is now very very close to production you know in Stark net and starkic systems it basically means the very far is out there uh sharp knows already how to run with recursion it's actually running

own shop environment that basically mimics production and I expected in a month or two we are going to see recursion uh running on General computation that includes darknet and Stark X and maybe other programs who knows running in production which is very very cool and it's gonna it's gonna present you changes for the good um so you should be aware and yeah that's it that's what I want to say thank you very much [Applause] so there's time for maybe I know we've gone over now I'm sorry okay thank you very much Abby thank you

foreign