# Build a constraint system, prover and verifier using OpenZKP Stark by Remco Bloemen (Devcon5)

- Speakers: [Remco Bloemen](https://streameth.org/speakers/remco-bloemen)
- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 30:17
- Topics: blockchain, smart contracts, distributed ledger, ethereum
- Watch: https://streameth.org/watch/yt-WxW1IEUWFHY
- YouTube: https://www.youtube.com/watch?v=WxW1IEUWFHY

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/5/build-a-constraint-system-prover-and-verifier-using-openzkp-stark

There are great tools and tutorials for R1CS proof systems (aka Snarks) but not much is known about programming Starks. Starks have a much more complex constraint language, but in return you can achieve a much better performance.
In this workshop we will
* learn about the mathematical underpinnings of Stark proofs,
* use 0x's OpenZKP library to generate and verify proofs, and
* implement a Stark constraint system.


Speaker(s): Remco Bloemen
Skill level: advanced
Track: Security
Keywords: technical

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

[Applause] welcome everyone to the open zkp worship we're always showing the starting computation that we recently announced so it's building in rust that anyone wants to go to I really recommend that you get through these commands right now because it will download the relative to the line principles and even the conference Wi-Fi you might wanna do this now I'll keep this tech stuff in every single slide so you don't have to remember ever cut it down last numbers just don't wait while I'm talking so [Music] come onto the upper right corner also I'm assuming that if you're coding along you're familiar with rust if not you'll be fine just listening so what is the zero knowledge protocol essentially you have a thing that is a claim which you can prove given some additional information call a witness or a private income or to secret and that results in a proof that is used to be much smaller than the actual thing that you're proving so smaller than a witness and you can verify this thing so you can if you have a claim and you have a proof you can verify it you can make sure that indeed any witness exists that satisfies this claim I'll give an example now the particular kind of chrome that we implement here is a start this is a protocol family developed by elephants and make you only observe near Goldberg and father in particular elements asan has been a hero in this field as he has been working on this for a long while and high-quality protocol variants and implementations of this particular protocol family are made by start work so you shout out to them for all the amazing work they've done in this field open start is an independent and partial implementation of the specific start variant used in the startx them so why stars stocks have some very interesting and unique qualities they have no trusted setup they require only elementary mark because of their simplicity they've had very good proof or in verifier performance they have small proves not fighting not as tiny as the proof you can get using bearing cryptography constructions but this comes with a Gabi they have a unique but completely different constraint system from everything you are used to and this makes them so interesting so study and play around so quick over to you of how these things and to prove that the program has executed on some input data you create a computational trace of the program's execution and you lay out this trace in a thick tape now this trace also contains your privately so this table is sort of secret but we want to have a prove and binds you to this particular trait and in starts we do this by creating several equations which you will evaluate over the traced able to prove that the disk array will be even explicitly say simulated but it will not only need to do that hey every next row effort every next row needs to contain to someone we've used two rows more and so on or you can say that it needs to be equal to a particular value so big slightly big scariest I don't worry they'll go to a bit byte what we're gonna do is fibonacci so quite the nest notation people not she is you have a and B but the initialized a with one we initialized B with on this case not one but some secret value right this is going to be our private equity and then we just iterate we update a and B with the previous be value and a plus B so this is a standard Fibonacci sequence and then we return a for some index so if we have this function and we run it we can do through Bonacci the 200 value starting with secret value 42 and you'll end up with a large number in this starts with one one nine now we want to create a zero knowledge claim on this by the way I'm saying zero knowledge but actually the implementation we have is a broad erasing and I'll see rich have a detail so we went to claim that we know some number and I'm not gonna tell you that it's 42 is such that if we compute the Fibonacci sequence on this and take the 200 value we get this big number so this is going to be our public claim all right so let's go through the steps the first thing we need to do is create a computational trace so we run this people not cheat program and we write down at each step what the values of a and B are so in the first row a is 1 and B is our secret value 42 because we're calling it with index 207 42 so a is 1 B is 42 and then we go into those 11 so for I in 0 to index we get a equals B so the next day is a PBS B and you can see that this happens everywhere and the new B is the sum of the previous table so this value here is 1 plus 42 what stream same here and this goes on until we made the road 200 and then we get our eight number that we want to demonstrate now if you look at this trace you can sort of see that there are four simple rules that capture the entire nature of the problem that would find cream and these rules are written down here there they are the so-called constraints they come in two basic kinds called boundary constraints and repeating constraints Adamo constraints are the first we need to have the first column being one but only for row zero so this value here needs to be one then we have another boundary constraint similar to that one that says that the first column needs to be our big outcome but only on road 200 so this value needs to be our big and then we need to demonstrate that it actually executed is the dilute here so we need that for each row the first column is equal to the previous row the second element is should have been 1 here so here of that and this holds for each row in this table so this is a repeating constraint similarly the second column or the next row is the sum of the two columns in the previous row so this value for some of these difficulties now these are four simple rules but if you think about it this captures everything that is intended with this plane so if you if you haven't raced it that satisfies these constraints you've shown the display place so now we've reduced our problem from this thing here to this thing here we still have a major trade secret but that's part of the star protocol but in order to do that we need to do a couple more iterations on what these constraints look like and the next thing we need to do is we need to tell them into multi bright mysteries so instead of having equalities we need to create expressions that are 0 whenever they hold that easy whenever you have an equality sign just replace it with a minus so this thing needs to be 0 on row 0 it's only 0 when this thing is 1 same here this thing needs to be 0 on world 200 you just subtract the value and then it'll be 0 same thing for us needing to have these two values equal you just subtract them and again what we need to have the sum we just subtract it left hand the expression from the right hand expression ok so now we've done that we have changed our constraints such that they are expressions that are 0 whenever the constraint volts now we didn't need to do a next trick the reasons for this trigger kind of mathematical and I don't have the time to go into the details of exactly why it is the way it is but if we have a constraint where we want I equals some value we need to multiply this by a thing 1 over X minus Omega to the power Omega is a constant and similarly if we want a repeating constraint we need to multiply this thing with this expression here when you do that you get this system it looks complicated but it's really just these things multiplied by these things and that's pretty much it what you need to do in order to create a constraint system for the people that's you start so let's show you now what it looks like if implemented using or vibrations so is anyone trying to code along now this makes sense so yeah I'm hoping you've got it to the point where you can do the build release and you managed to download [Music] so I build it here now so what we do is we take the ckp start package and we just import everything we also employed the prime field that again to this what a great example it doesn't really matter those are values but but if you're working with these systems in like practical applications you need to know that every operation happens in some large prime field applications so the first thing we do is we create a struts that represents our plane in this case the greatest article tonight she claimed it has the index which in the example is 200 it has the secret value which was this very large number that behind and so he has neat public Valeo didn't complain large numbers and now we implement two trails on let's start the provable so what do we need to do you need to create a table or this thing like we said so what I already have here is we have the Stars itself which is here we have our secret value which is here twenty South were to trace table so for mathematical reasons the tri-state will always needs to have a power of two sighs so we'll just round index up to the next power of two don't worry we'll still get brother two hundred out of it we just need to compute two hundred into the safe rows and we create race table with this size into the columns so let's initialize it we start with adding almost what we need to hi the second column B or C value and then we have mark for loop where we update each that was sort of the first one was they both lead all by minus 1 to 1 and the second value or Y value was equal to hit some talk louder yes then semantics so if you're not familiar with us you can ignore the under sons and diplomas there just to satisfy the Bordeaux checker let's see what's happening little line where we say that the value equals that's pretty the value that we want to play doctor and is larger still yeah here just the programming like this interesting so yes let's print the value at if I trying to clean there we go okay and we have already playing here so let's go to the main function so we created our playing index to wonder and we think that the value is this is just a hexadecimal will be large number the claim of those secret is 42 regular playing store which you can see here and let's just for test who claims on each race and see if indeed one row 200 we get the value and yes we get the value that is the same as this one so we implemented by trace table correctly so that's the trade stable now the second thing we need to do is we need to implement the constraint expressions for that we have a little genome oppression expression is important we need to again have a number of rows that this is power of 2 so we rounded up the next one here I've prepared those two expressions that do one off and repeated constraints so we can just need create a new constraint object from expressions we give the size of a trace table which is n by two we give a seed which in this we're not really using and now I know the sector where I just can just enter these expressions so does anyone remember or constraints there you go the first one was the first row and the first column needs to be in constant value quantity and this needs to hold for the first row so we say on row zero and for second constraint very similar to the first one except that we now need to have it match or claims invalid and we need to have it on the row that be plain so like this so I choose the Southern gentleman [Music] I'm sorry so this is actually this is an i plus you but so it means that on on the role of set zero versus pro upset so this where it like this now it have the repeating on the strain but before you go ahead the on row and every row of functions and omega are those um just for every table or are they specific to this example they would work for every table the technical thing that happens is that omega is a root of unity of size of the trace table and a particular prime field that we have as roots feud is the only of powers of two which is why these have a power of two is a stable name but this these three lines here you can essentially copy-paste in in any constraint system and I should know because if you go to any X you see here that we do I and I plus 1 so the I plus is sort of implicit here in this case we have I plus 0 I plus 0 which matches what we're doing here this is like I plus 0 and this is either 0 the actual did the number 200 itself comes into this on world expression that's where the 200 is implying it becomes a little bit more clearer with the repeating constraints so the first one will do is the pokemons strength we'll do a trace and here we want I plus one so we say one year and zero and we need to subtract Trey's zero comma one so one row down and coma zero - same room whole month and we want this on every row and then there is one more repeating strength that we have and in fact this is the constraint whether it's on or it's all about because this is the one that I should be implements that you will not see there is this sort of like boiler plate and plumbing and this is the line that says that it is the sum of the next row first column is the sum of the previous row both columns there we go here right right yes so next row second column sum of previous row okay let's see it runs [Music] I expected missing parentheses successful people not see proof in 32 it opens it gets better the crew size grows logarithmically so-called larger and larger examples it's significantly better now I'll show you what what exactly happened here so we're creating now an instance of this people massive flame of yet with the values that we want to prove we have our secret value that we want to hide we created proof by saying play monkey act dog proof with our secret and unwrap as a technicality here for trust error handling they basically throws an error in anything fails then we can compare this proof - it's like binary representation we can show that it's about 32 kilobytes and what we can also do is we can do plain thought verify and give it the proof and make sure it's okay and I mean print valid which you see here what we can also do is create an incorrect thing so let's take the same index and let's not change the value to something completely different and if we take a wrong plane and try to verify it using this proof it will actually print invalid so so much for the life coding part in contusion so we started this open CPU project to experiment and learn and study different root systems like I said we're currently having only a very partial implementation one of the things we would like to implement next from the start proof protocol is having constraints that span offsets different from one leg right now we have constraints between rows between one row in the next if you want to do interesting things you really need to have offsets that are more complicated than one row in the next you want to be able to reference multiple rows back for example we want to add many more examples that is we have for example an implementation of the mimsy hash function we are working on technology proposal for proof of data availability we are working on the example from Aneta labs where they do a verifiable tool a function using MC so that's a lot of fun we're working on or we won't be working on evn fairly minor contract so that you can not only like right now we can verify your proof in rust our rest code base compiles to webassembly so we already have verifiers in the browser we also managed to verify it inside of the substrate note so any like webassembly enabled 2.0 blockchains will be able to verify the exposure one thing you noticed in this language right now is it feels really low level like we're literally writing the assembly language that those brain systems and what you want is a higher-level language where you just write the program in moralistic Python s language that I showed and then demo automatically generate the logic put a trace table a little spaces for you that's an interesting field to explore performance is pretty decent but still has room for so that's something we can work on and we're interested in implementing all sorts of crazy new serie knowledge proof protocols that have been released over the past couple of months a lot of them have a meaningful equivalent that is very similar to Starks in the sense that you have transparency and yet no trusted said you use polynomial commitment schemes so you can look into Aurora I'm Marlene plumb fractal etc and we're trying to do is there is a nice community within the theorem block chain of people researching this and our hope is that by contributing this and inviting owners to contribute to us we look at an exchange of ideas and help each other move this field forward yes so what about Annie do we have the distinct it is not legally hey in this case yeah absolutely none because you can just compute Fibonacci reversed the other thing I briefly mentioned it what one of the things we don't have right now is perfect server knowledge you need to you need to implement a couple more things to get them so right now we don't have enough zero knowledge we just have Cygnus which means that your proof only grows logarithmically in the size of the fact that it would instantly and he became protector proof or we should do you can check the food and you can I just do not young rhythm and and check that it block that way I know it's more efficient so is this instrument it's it's logarithmic in the original in the number yes yeah yeah here for example gonna like this seed straight somewhere what was that for yes so what you want is to initialize the proof with the shared information between the approver and the verifier so if I'm creating a prove and I'm giving it to you ideally it would improve security is all are you all on knowledge we have in common what's encoded in there so what you could do is take a hash of your claim put it in there and then it prove is more constraints cryptographically to be for that particular so adds to security by committing you to this particular instance of the problem like I get back to my motivational shirt so suppose I do people actually did something else yes so again what can people do by this you know the study but yeah so this these two things to this question the first is yes it's okay so the guarantee that you get is that the verifier will not be able to learn anything more and can be learned from the public input and if on paper by somebody other absolutely yeah that is that is a proof done by elements person at all I know but what do you what do you your proof you think they yeah which is essentially what happens in in the Fibonacci example because you know the output is just defined buddy by the secret values so you can just compute it backwards it's not hard algebra I hate to do this but you can also do is just like iterate through all the values if you know that there is only a small set of them and this is why the is really important to know what the exact truth is and the exact thing is you cannot learn anything more than you can already learn from the claim itself if the claim contains your private into it or something that allows you to derive the private input then you have no zero knowledge guarantees so this is something to keep in mind if you want to use these things for is your actual zero knowledge and privacy be careful about what you put in the public input because you might be able to derive the private input from this if you're not careful another big room are going to make is that right now we don't have perfect your knowledge we only have sickness in the system that we have so like the system we have is not soon at the moment for any hard privacy requirements but again contributions of weapons though so something that you could committee group with this is that given the output being a hash function it was verified that there was an input that did get a rate that actually we have an example of a machine Ashley image you can see you can find it in the repo [Applause]