AirScript: Arithmetization for zk-STARKs, with Bobbin

so some of that is going to be a little bit redundant but there's going to be a mostly new stuff so kind of the quick outline of the talk so the first I want to discuss a wreck mutilation whether they specifically so we have a lot of this potential with the zero knowledge proof technologies and they really wonderful but the question is how do we translate the programs that we kind of use in a daily basis into those type of things that can be used to generate proofs for those programs and this is what the estimate ization is about then I'm going to talk about a little bit about how Starks work very quickly just to show an overview where there is a mutation fits and lastly there is enough time I'll show the quick example of how you can write a program an error script that can be verified or for which you can generate the proof using Starks so let's jump in so the first thing to kind of think about is how we can think about computations and there are really two ways to think about computations in general and those the circuit computations and machine computations and the difference between the two is that and if the first one can be represented as an arithmetic circuit we can think about it almost like a electronic circuit as well where you have some inputs you have gates and the inputs propagate through those gates and then you get an output this is different from the machine computation approach where you have kind of a state of a computation you apply transition function to the computation and you apply it many times and every time you apply the transition function your state changes and that kind of defines your computation so those are the two approaches and there are different ways to hypnotize those two approaches the first one is our ones here so that's a very well-defined constraint system that you can translate computation into and for machine computation that's called err or algebraic intermediate representation now there are different benefits and trade-offs associate with them I've listed a couple here but for 1cs it's fairly easy to take a general computation translate it into our one CS it's fairly easy to compose different computations for machine computations because they can be represented using a succinct transition function usually you can give them much more efficient for specific time of computation water of generating proofs and verifying groups and you know there are different types of languages used to write for those constraint system so like first you write in a given language and then you translate into like let's say r1 CSO air and there are quite a few languages for circuit computations those largest circle Socrates the new month recently came out of the sink and machine crepitations there is really air script in their assembly and their kind of languages that are tied together and this is what I've been working on primarily and air assembly translates into or air script can get compiled into your assembly and that's good and gets executed to generate the proof and then just to say where they're used so most of the snark constants the constructs that people usually talk about use are 1cs constraints Starks are one of the exceptions that use air constraints in theory it is possible to use air constraints without the proving system but nobody really does that in practice so this is kind of the lay of the land and let's dive into the what exactly is air and what are the concepts behind it because I think there are like basically five concepts that once you understand them it's fairly easy understand what's going on so the first concept is the computation state you can think about this as a set of registers that have a value at a given point in time it's in a way similar to how like let's say CPU has a set of registers that have you know different values stored in them and this is kind of a state of a computation the given point and time the next concept is execution trace so if we take those states and record them at every point in time we'll get an execution trace so you can think about it as a two dimensional matrix where at you know a row in the matrix represent a point in time of a computation and the column represents a given register so the next concept is a transition function so the transition function takes a state and outputs the next state of the computation and kind of for this to work for air to be efficient you have to apply the same function from one state to another so it's the same function that gets applied every time and you get their execution trace and the next concept is transition constraints this is also a function that gets applies to two consecutive states so you basically fit in two states and you get a set of values out of it and the computations considered to be valid if all of those values is 0 and the last concept is boundary constraints and basically I allow you to specify what is the value of a computation or given register at a given point in time in reality transition constraints and boundary constraints are really the same thing just I think it makes logical sense to separate them and think about them differently okay to dive into the execution trace a bit more so this is kind of how the execution trace would look like or at least how I described it but I actually kind of simplified it a little bit so there is actually two parts to the execution traces that you can kind of conceptually separate there is the die set of dynamic registers that get built up by the transition function but there is also a set of static registers that you can define using some simple representation as an example you can think of like let's say a cyclic rate register that gets a set of values repeated all over and over again you don't really need a transition function to describe it you can describe it using a simple polynomial for example another example is kind of a nice holy register where the values get inserted at the given point in time and you don't really care about what the values in between are and those are also very easy to describe using polynomials now these are two concepts and you know if you start combining them in different ways they're actually pretty powerful allow you to do a lot of different things and there are some kind of considerations so first thing we need to have our traces execution traces for efficiency reasons have to be a power of two you know we can make the your registers public or private and you know fields have to have higher orders ruling it it's like special type of fields a lot of fields have that property but not all not all fields so it's something to be aware of now transition function now to update based on our kind of separation between static and dynamic registers now in previously I only use dynamic registers so in this case you know a transition function takes a set of dynamic registers and a set of static registers and outputs the next state of the static or dynamic registers actually and you know it might have seem like it's a very limit like transition function is a very limited way to describe a computation because it's the same function that gets applied over and over again but you can actually use a concept of arithmetic switching where you can define kind of two separate functions and when let's say one of the registers is zero you know this function will get executed but when let's see this K 0 register is 1 this function gets executed so you can actually kind of extend this and have many different functions get execute it and they get switched based on values of other registers that's actually very powerful we can describe pretty much any computation using this approach and some considerations so you can use all it metric operations like divisions multiplications and so forth within transition function you have to keep in mind what the degree of the function is because it's important for efficiency reason the higher the degree the longer it will you know take to ingenuity the proof and the bigger the proof size would be and the way you can you know keep keep your eye on degrees that you want to minimize the number of multiplications or reuse the number of multiplications between registers or raising and given register to some power and the other thing I kind of skipped over the consular transition function can actually be even more powerful where you don't have to take two consecutive or one state you can take multiple states for example and Fibonacci sequence is a good example of that where the next state of the sequence depends on a two previous state not only on one previous state and just to dive a bit more into the transition constraints now again it takes the two states of the dynamic trace and state of the static trace and then outputs this transition transition constraints frequently transition constraints could be just something as simple as you take the current state apply transition function to it and subtract it from the next state and that will give you all zeros if you know for certain types of transitions but it can actually make it much more complicated you can apply different constraints beasts you know of what kind of information you want to fit into them and this this is the way to kind of sometimes reduce the degree or get a bit more sophisticated and some of the considerations for constraints is that you can't really use division very easily but it's very easy to emulate it the degree of the transition constraints it could be different from a degree of transition function you don't have to have the same degree and actually the degree of the transition constraints is what is important that you degree of a transition function doesn't matter as much as some actually doesn't matter at all what matters for the computational efficiency or crew generation efficiency and so forth is the degree of the transition constraints and again the concept of long-range constraints where you can take more than just two consecutive states I'm kind of skipping over for the sake of simplicity here okay so with this let's kind of get into the start specifically and talk about a bit how start who generation process works so every computation starts with a set of inputs you run those inputs through a transition function and you get your execution trace the next step is to apply the transition constraints to this execution trace and you get your constraint evaluations and then once you get them you do something called you compose those constraints into a single polynomial using random linear combination and lastly you use the Fry protocol to kind of prove the low degree of that polynomial and I'm skipping over a bunch of different steps here but this is kind of the high level process of you know how things work out and the way to think about these steps as well is that the first two steps a computation specific meaning they depend on the specific computation that you are trying to generate the proof for but the last two steps are computation agnostic meaning it doesn't really matter what computation you're running the last two steps are always you know kind of the same and within kind of the work at time doing the first two steps are handled by this err script language and the last two steps there is a gen Stark library that allows you to give an error script that allows you to generate proofs and verify those proofs for the computations and the purpose of the heirs of air script languages there are really three main goals the first one is it describes the logic of how you generate the execution trees it describes the logic of how to evaluate transition strains and it also provides a logic of how you interpret different inputs that if you didn't do it and kind of the actual toolchain model of how this works is that you have your inter script source it gets compiled into air assembly and then this gen start proven very far it can interpret air assembler to generate proofs and verify proofs in the future I hope that more people will kind of try to build other languages that I can think of to compile into air assembly and then build other provers and very fires that can run off of air assembly to verify in January proofs now let's dive into an example of how you could use air script so we're gonna do it on an example of a very simple computation it's called MinC computation how many people have heard about mi MC before okay so my MC is basically nearly trivial computation but it could be used to kind of generate a hash or it could be used as a simple hash function because if you repeat many times it's very difficult to kind of roll it back and figure out what's going on so the computation is self described but by this simple formula so we have kind of a value with cubed and we had some constant to it and we repeat this over and over again so in the context of arithmetician like we can say this is our current state this is our some constant that we're going to be adding to the current state and that could change from one step to another but it changes in a predictable way and this is going to be our next state so a fairly simple so we really have just one dynamic register that you know the single value that changes like you can think about it as an execution trace with a single column and we have one static register that actually going to be another column within the execution trace now how would this work out so let's generate an execution trace for this so let's say we start with a value 3 that's going to be our input we can have a single static register that going to repeat this you know simple cycle 1 2 3 4 over and over in the execution trace we're going to run the computation for 64 steps and we're going to use a field in which we do computations but one thing I probably should have mentioned is all there is medic operations Historics happen in the finite field so in this case the finite field has this modulus basically it's kind of like modular arithmetic you literally think they can do use by the modulus or divided by the modulus so this is how the execution trace is going to look like you can see we have our static register K 0 here and it just repeats the sequence of 1 2 3 4 1 2 3 4 [Music] 4 64 steps and then you see our dynamic register over there so because our input is 3 it starts with a value 3 and you can see like the first time we apply the transition function what it does it it cubes 3 and add 1 to it so we get 28 the the second time at cubes 28 and add 2 to it and you get you know 21 9 5 4 and it runs until then until it gets that for 0 1 2 and so forth number and as a very last step so this is our execution trace and this is the computation that we generated a trace for so in a context of gel dark library or first of all let's talk about air script so how would you describe this using air script and this is the entire code that you need to describe this computation using air script and I'll explain what it does so the first thing that we do is that we declare our start and we say that it's going to work over this field the second thing that we do is we define our static register so we say this you know round constant is going to be the name of our static register and just going to repeat the cycle of 1 2 3 4 over and over again the next thing we say is that we're going to have a single input which is going to be a single field element so because our computation just takes one input at a time that's what it's going to be and then we define our transition functions so here's a bit more kind of things to explain here so the first thing we say that our transition function is going to work with only one dynamic register and we're gonna repeat this cycle or this loop for every start value that gets passed in so we could pass in just the 3 or we could pass in like an array of values and for each of those it will run this computation the first thing it will do is initialize the execution trace put the 3 like if you think about the trace that actually before it would put the 3 as the first value in the execution trace and then it's going to repeat this like run this formula for 63 more times so 64 total calculations and in this case like our zero is actually an implicit variable that refers to the first register in the trees we only have one register so it's going to just have a single column so basically take our current state cubed add round constant and that's going to be the output of the computation and then the last thing is our transition constraints they are very simple in this case you just take the current state of the computation apply transition function to it and compare it to the next state and in this case M a dollar sign n is kind of implicit variable that refers to the next state of the computation so we basically say if we take the current state which is dollar sign R 0 apply transition to it it should equal to the next state and if that holds that means that our constraints have been satisfied all right so how do you run this example what say using Java Script so this is the code the entire code that you need to run this example in generate and verify proof for it so the first thing we do is let's assume that the script variable here has that script that I showed on the previous slides so we say instantiate script and I generates a stark object this dark object then can be used to generate and verify proofs so the next thing that we need to do before we can generate a proof we need to define some assertions what what statements do we make about the computation so in this case we're saying that register 0 at step 0 should be be equal to 3 and register 0 at step 64 should be equal to that value so computation would be valid if the register those two registers have those values or this register those two steps has those values and then the next thing that we do is we just generate proof and we pass this 3 as our initial value so basically what what it says if you execute this MinC computation for 64 steps and you start with the value 3 you should generate an execution trace that will align satisfy these two assertions and then no we can verify this assertions against the proof that gets generated in the previous state and of course in this case the proof will pass because we have generate and verified exactly the same proof but you can think about Siri lysing this proof and sending it to somebody else and they can verify that you ran that computation done it correctly now of course this is a trivial computation it doesn't do a lot of things but you can think about different types of computations that they can prove in the same way like a pre-image of hash function or that you verify the digital signature or something even much more complex so you can write air script so like for example there are air scripts that verify member membership in the miracle tree or verify a digital signature like it's nor signature and things like that so and this is my talk so any questions [Applause]