ETHLondonUK: How Does A STARK Proof System Work, with Michael Riabzev

everybody who's been here in the earlier session that they had today okay not everybody but who's familiar with proof systems okay so this talk now starts with an introduction to prove systems something that I did this morning as well and then continues story just and that continues with diving into the start protocol it would be a bit less engineering like and there would be some mathematical stuff here but before that I will just tell you that you should concentrate because there might be some tricky ideas that it's not trivial to to conceive okay so shortly I started introduced in the morning we are start where we are building an exchange with diversify us of custodial exchange allowing high throughput of transactions creep cryptographic proof system in high level is something that its input can be a predicate a predicate described with any program for example a Python program a C or whatever that given an input returns true or false and it can be compiled using systems like star to approver in a verifier such that the prover can receive an input that satisfies the predicate it can generate a proof to show that this predicate it knows the valid predicate and the very fair can read this proof and be sure that the prover indeed knew this such a predicate I'll do a general simple example for those who don't really have the intuition to what can be done with that so computational integrity is one example for this we can think about the following scenario we usually send benchmarks on works to the cloud and we hope the cloud will reply honestly with results technically the cloud provider has the ability to do anything they want to tamper with the result that they returned to us using computers computational integrity we can think about the predicate it's just something that can verify that when executing the program I want to render with the input I give I get the result I really want the cloud provider really suggests is the result of the execution so I'll divert to describe the features of the decay stark proof system so the K stands for zero knowledge which means that when someone sees the proof they cannot know anything about the witness the satisfying witness scalability it means that very fine such a proof scales logarithmically with the time that it's a takes to compute to execute the predicate for example in the case of the cloud provider it could be the case I actually offload a big workload to this cloud provider something that would take them a lot of time to compute something that I would not be able to compute in reasonable time on my laptop but the verification of the proof would take me milliseconds and I can be sure that they cannot lie to me or give any false result transparent means that there is no need in any trust that set up that reading this proof of sufficient like a mathematical proof to make sure that everything is okay and you don't have to trust any other party argument not knowledge it means that looking at the fact that the approver can generate a proof says that the proof actually knows a witness that is fine this predicate what I will focus mostly on this talk is about the scalability feature which is the main feature that start provides okay so this protocol just like any other protocols it's kind of an agreement of an agreement between two parties in this case the prover in the verifier and many times it's very comfortable to think about protocols like protocol stacks like the tcp/ip stack are you familiar with the TCP stack yes okay so that's good so we will see something which is a similar to the TCP stack so there is the application layer in the application layer we have a statement on the side of the verifier and we have a statement in the witness on the side of the prover the prover has to know some special witness not not in all cases for example in execution it's not in all cases but it could be the case that they provide the prover a program and they prove to me that they know something that I don't know of how to satisfy this program an example for such an interesting predicate a program that takes two inputs verifies they two are different hashes them with chateaux and then verifies they're the output are the same technically satisfying this predicate means knowledge of collision of chateaux so somebody could generate a proof of knowledge for satisfaction of such predicate put her on the website and if it's a thorough knowledge proved then everybody would know they know a collision to shut to but nobody would get in information about the data itself it would not leak so this is the statement something very easy to talk about it's something very standard in computer science what we do when we want to construct a stark proof we move from a statement to some kind of a localized format of the statement in high-level you can think of it as executing the prover can execute the predicate and what the very further - it can locally verify the trace it can just access two consecutive lines of the trace and verified our consistent assuming for example we're an honest Pacific architecture the intel architecture then it's very easy to look at all the old estate of all the registers and to see that when we are in one state we move correctly to the other state and other thing is direct mutilation and mutilation is just taking all the things that we had before the trace and the way to verify two consecutive lies in the trace and to make it algebraic there is not much intuition now of why would we want to do something like that but hopefully by the end of this presentation you'll get intuition of why would we would we want to arithmetics this localize the language and we after that what we do we do low degree testing again not much of intuition right now but hopefully we will get some by the end of this language and we do a realisation of the entire model using the merkel commitment trees is anybody our everybody here familiar with miracle trees is anybody in not familiar with miracle trees okay so in a way the start protocol is actually a very simple protocol is not something complex what it does it just it based on two pretty complex ideas one of them it's very computer science like idea of programs execution traces that programmers are usually feel comfortable with but not most of the people in the world feel comfortable with them the other set of ideas are more algebraic ideas talking about polynomials allowed and load the greenness this is something that mathematician might feel comfortable with and most of the people in the world don't feel comfortable with and what we do in stark we just merge the two ideas and build on top of them to provide a proof system okay we will just now scan all the reductions in the protocols but not in the but not in the consecutive order of what's going on here who will start with going from an application to a localized a statement to a localized test we will see what is the issue there and there in order to find a solution we will jump to the end to something that intuitively can find a solution and we will do this man in the middle technique finally a understanding what the start protocol is so in localization the prover the predicate is compelled to a prover in the very first approve er given a witness can generate an execution trace and now the verifier can choose randomly a two consecutive lines from the trace and verify if there are consistent given the architecture executing this program but the issue is assuming the prover is volition assuming the approval is the Amazon and I'm running some program that they really want to cheat on they really want me to think the result in something else for example I want to know if I want to invest in Azure Amazon and they want me to invest in Amazon so what would be their probability of cheating how hard it would be for them to cheat me in this case anybody something interactive here somebody wants to guess it depends on the length of the problem so assume the program is very long million of lines million of lines in the trace exactly they only have to cheat once it's it is sufficient to find a single line and to make it completely independent from the previous line in the case of a trace of length a million the probability of me choosing this line would be one from a million it's it's not very sound so I wouldn't use this system so we have here an issue that what we want to do is to verify for all constraints for all pair pair of consecutive lines something is satisfied and in this standard way it's not very sound so this is the reason why we're going to the algebraic world and now we will get the intuition of how algebra can help us in this case if somebody is familiar I can fate is related to error correction correction codes okay so we are jumping down to the last layer of low-degree testing and the realization and we will start with a story in the story we have Alice Alice is the manager we have Bob who is very busy and we have Charlie with the coder so Alice asked Bob to do some computation Alice provides Bob with a list of numbers and she wants Bob to computer square root the issue is that there are many numbers there - - the 50 numbers it's a lot of work and Bob is very busy so Bob calls and Bob what Alice gives Bob she doesn't give him to the 50 numbers she just gives him a miracle root of those numbers that Bob can use to download them from BitTorrent you familiar with BitTorrent do you know how when you get a slice of of a file how you verify that if this is indeed consistent with what you want to download it's actually miracle drills you verify that the ratings are consistent with the miracle root this is the hash that you use when you want to download something in Victorian so Bo can download the file on BitTorrent but what was very busy doesn't even have time to download from BitTorrent what Bob does Bob asks Charlie - helping charlie is a great coder and you can solve this issue Charlie can write a script to solve this issue the issue is that Charlie sometimes does mistakes and it could be the case that Charlie has a bug and Bob really want this job to be done correctly he doesn't want any any issues with with the result so bob has to verify Charlie's work then I in solution for Bob to verify each other's work is just to go over to to to the 50 years old the Charlie would provide him and to compute they're squares but it's a lot of work and Bob is very busy as you can see his name okay so now Bob thought about an idea and I apologize there is not much intuition to what is going to happen now but please try to follow it would be this kind of mathematical argument that it's pretty easy to follow it line after line but in the end there is something that one have to just wrap the head around there are some interesting ideas that just need to you need to think about them so i really suggest to concentrate on it now so Bob thinks intuitively that maybe those numbers are values of a polynomial not every set of numbers are values of polynomial you can always do interpolation over values like right so Bob tells to Charlie the file that Alice one gave of numbers think of them as the values of a polynomial that the the polynomial on I is actually the ice number in their file now you can do interpolation and get the coefficients of this polynomial you have now a formal fact a functional polynomial and the degree of this polynomial is at most 2 to the 50 it's limited by 2050 this is this is how interpolation works and what Bob asked Charlie as well is don't give me explicitly the list of result do the same for the results as well once you have the result the square roots of the numbers then think of them as values of a polynomial over the same exit over the same domain and just just give those coefficient not explicitly to me we will see exactly what will happen with them but think about the coefficients of this polynomial the those are the daughter is valued on this domain and this polynomial is again of the great most - to the 50 because it's an interpolation of 2 to the 50 numbers so the observation in this case the important observation is that if we think of the polynomial Q which is G minus P Square it has to funny vanish over the domain both polynomials were interpolated on right it has to be zero for any X under 2 to the 50 starting of zero right is that ok and what is the degree of this polynomial so this polynomial is the linear combination of two polynomials one of them is of degree 2 to the 50 the other one is the degree to vice 2 to the 50 so 2 to the 51 okay so there are some easily the polynomial of degree at most 2 to the 51 is this ok are there any questions meanwhile okay so we have an algebraic fact algebraic fact a polynomial vanishes on some point if you know only if we can factor it we can factor this root out so if R is the root of Q then we can think of Q as multiplication of a polynomial B by the polynomial the simple polynomial with the root are X minus R and the degree of B is smaller by one from the degree of Q does it make sense anything no doesn't make sense it's okay okay and by induction because we know that Q should vanish in case Charlie was did the work correctly you should vanish over this entire domain then by induction we can see that Q can be factored as the product of some polynomial B of small enough degree and the minimal polynomial vanishes over this domain okay this is this is the important idea that we will use so this is those are the facts and this is the construction that we have and now we see what is the test Bob will apply on Charlie's results Bob will simply draw a random number from the domain 0 to 2 to the 60 and we'll ask Charlie to evaluate the polynomials Charlie computed over the point R and verify that Jean R minus P in our square equals Ben are we Charlie should compute it well multiplied by this polynomial vanishing on the domain okay so because of our construction in case a Charlie did a good job Bob is always satisfied right right but what if Charlie failed what if Charlie had some kind of a bug something didn't work right in this case when we look at this equation on both sides of this equation we have polynomials of degree at most two to the 51 right and if this is not exactly the same polynomial then they can agree on it most two to the 51 points because think about their difference if we subtract the two sides we have here a polynomial of the great pass to to the 51 here polynomial of degree at most two to 51 their difference with the polynomial of degree at most two to the 51 and if it's not zero it can have at most two to the 51 roots so they can agree on at most two thousand 51 points but Charlie each others are from a much bigger domain the two to the 60 options so the probability of Charlie choosing by mistake a value that satisfies this equation in in case this is not always satisfied is at most one over 500 okay which is okay to catch a bug with probability 1 over 500 it sorry took to be cheated not to catch a bug with probability 1 over 500 it's great it means that you catch a bug with probability 499 over 500 this is really good and if Bob wants to be more sure about this test Bob can choose another R and to do it again and the probability of Bob not finding the error will go down exponentially okay till now we talked about the case that Charlie is trustworthy but he might do a mistake so it was a way to verify Charlie did everything correctly but what if charlie is malicious what if charlie is actually kind of lazy and it tries to it tries just to cheetah that it really did the job in this case we will use the Burkle trees so we will ask Charlie to commit on both the real values that we know the miracle tree of them and the low-degree extension with some commitment and to do the same for all the polynomials for all the polynomials evaluating them on the domain 0 to 2 to the 60 the domain that Bob will be asking on and after Charlie does this a commitment with Merkel trees only then Bob will decide on what value you want - he wants to query and will query all those polynomials and verify they are consistent with the route charlie provided ahead using Merkle trees just eliminates the ability of Charlie being adaptive because without them if Charlie's malicious it's very easy to give values of GP and be satisfying this equation you just give some random numbers and set the last one to be whatever it's it's an equation that is easy to satisfy if you don't really commit to polynomials but this requires Charlie to commit to polynomials but there is another problem here what if the polynomials the evaluation Charlie committed on here are not low degree all of our soundness here was based on the fact they must be low degree so this is were low degree testing comes to low degree testing allows a sixteenth verifier to look at some enormous evaluation not to read all of it but to sample parts of it and to engage in a protocol with approver that eventually the very fair can be satisfied and know that this evaluation describes the polynomial of low degree this is what what we actually need here I think this was the hardest part any question before I go on to the rest of the construction so yeah so it seems that all the computational theory and proof system somehow eventually reduce to low degree testing and so I don't know it seems that initially in the late 80s they started with this approach and it seems to be going well and I'm not aware of something that they took a completely different direction okay so we looked at the reduction from application to localization and we look at reduction from low degree testing to realization and we will just continue to do meet-in-the-middle until we get into stark so remember in localization we said that the prover generates trace and execution trace and the very fair just verifies to two consecutive lines in distress and you can think of the way the very first asset using some validation circuit an example of a validation circuit if we'll take talking here about the Intel Architecture the validation circuit could be just the circuit of the CPU verifying that the next line is consistent with the execution of the CPU on the current line this is an example but in the end those are all circuits so our motivation is actually taking this circuit that verifies consistency between two consecutive lines and making a polynomial out of it ok this is a very simple example of assuming polynomial that receives bit because we start from a circuit that is a boolean circuit but actually a lot of more interesting constructions do stuff that are above this and look at the full field elements and some more complex encoding which bobbins we'll be talking about it in 430 so why do we want to make this circuit into a polynomial because of Bob's idea that we've seen a few minutes ago this circuit the cue circuit is very similar to Bob's idea of defining Q polynomial having some constraint and checking that it is satisfied on all on all parts of the trace on all part on all numbers so here we are making this Q polynomial and we are using it to verify that every two consecutive lines of the trés satisfy this polynomial meaning it satisfied the circuit all the or the CPU architecture and as I said this is a very naive technique a bobbin we'll be talking about more interesting techniques to do this I admit evasion okay so we cover all the parts and we will just rub them all together to see what stark is so in order to get in to start protocol both sides need to agree on some arithmetician of the constraint of the circuit of the architecture they want to execute the prover should compute the execution trace and it coded in an algebraic way that can be verified with this art mutilation of the circuit with the polynomial and in the end we are just using the technique that Bob used with Charlie to verify that every two consecutive lines in this execution trace indeed satisfy this constraint polynomial or the circuit so now we covered everything and I hope it provided you more intuition to what Stark is thank you