# How does one use a SNARK for something (DSL's/toolsets)

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2018-10-07
- Duration: 20:25
- Watch: https://streameth.org/watch/yt-lQ7tpus_zZ8
- YouTube: https://www.youtube.com/watch?v=lQ7tpus_zZ8

## Description

Speaker: Jacob Eberhardt

The Devcon3 ZK breakout sessions are sponsored by the Zcash Company.

## Transcript

[Music] hello everyone great to be here my name is Jakob rahat and I work at to Berlin in the information systems engineering group and we've heard such great oxido which brought the setup phase to the next level I think which will make it in the future hopefully feasible to run your own setup for your own circuit with that bring CK snarks actually to the practice so you can use it so what we did with the silk resist project is to see what we can do with the new pre composite on the theorem how we can use them to actually do something useful in the network and it's currently a research prototype but we can already do some things so the end goal is to have a nice domain-specific language and some tooling to actually be able to use narcs and I want to show you some of that today so I won't go into detail about a circuit test toolbox because I did talk on Wednesday already but just as a quick wrap-up so the vision is to provide a usable abstraction and tooling for CK starks that integrates nicely with a theorem and it's supposed to support the full process that means from specifying your program code up to the point where you validate the execution of that code or the correctness of the execution of that code on the blockchain in sir knowledge so what does a feature at the moment at the moment it's a domain-specific higher-level language not terribly powerful yet I'm talking to people about what the feature should be how we can extend it and what makes sense at the moment it's still quite limited and the compiler which transforms these conditions into constraint systems we can use to do proofs on also it provides some support with setup phase at this point this is a trusted set up and that's why I'm so excited to hear about the efforts by the sea guys to make a distributed setup face actually usable because I think then we could actually make applications use this technology so that's like really cool I'm really excited I hope this works well in the future and brings them to developers as fast as possible it also the tool also helps to generate witnesses and with that to find solutions for your constraint system generally proof and export solidity smart contracts so you will actually be able to check the proofs on the plot chain so the language I covered in my other talks so just briefly the the primary data type you have is prime field elements so think of positive numbers that are larger than smaller than one huge prime number and of course you can simulate binary circuits with that which is just not very efficient because you only use one and zero instead of a larger set and you have mperatures statements you have assertions you have loops conditionals and functions which allow you to structure code nicely but there's no recursion at that point that would be doable with things like tiny RAM which is really cool concept but the proofs just seem to be a bit too expansive for applications at this point so what's the process how do you use silk row tests this is based on the command-line interface the slide you're seeing here so you have high level code and then you compile that to a constraint system basically and then based on that constraint system you can find the solution for that constraint system based on either private or public inputs you decide which part of that you make public so that's the witness computation and then it supports at this point only a local trusted setup I hope there will be some distributed process in the future supported that allow you to generate a verification key and a proven key these are a circuit specific so you do that once for one computation you specified up here basically and then you can export that very few key into a solidity smart contract which will then allow you to check the proofs on the blockchain the proofs you can then actually check with that is approves your generated by using a witness a solution for your constraint system satisfying variable assignment together with the proving key and based on that you can generate a proof which shows that you valuated your constraint system correctly and with that executed your program correctly but also you can provide or publish part of the inputs you used your public inputs but you can also keep part of that private so you don't have to reveal it to the public who of you has seen Christian talk the Christians talk in the morning okay that's a lot very good so Christian introduced the pseudo Co example and what I want to do in this workshop session is to show you how you can specify a pseudo code checker in that language and how you can actually then check whether someone found a solution for your pseudo code system on the theorem so let's do that so here we have a given solution I just copied that from Christian I didn't find it myself so the question now is how can we use Socrates to prove we know a solution to the pseudo crew system without revealing it to the public so essentially we want to show that there is a solution for a given system and how can we verify that on chain okay so first we need to model our problem a little bit so we have a Sudoku a mini Sudoku and it consists of sub squares and I've used letters for them so we have sub square a B C and D and then we just number all variables to build that kind of matrix structure and then we have to define the validity conditions for a pseudo system so what would that be first we have to guarantee that values are in 1 2 3 4 in this set so other values are not allowed then we have to make sure that we have unique values in rows and columns and in sub squares so each of these values can occur or has to occur exactly once in each sub square column and row so how do we put that down as conditions so first define a validate input function and this returns zero if the value is in one two three or four it does it by multiplication and then we assert that's condition down here that all inputs satisfy that condition so that we actually only have one two three four in our system then we need a uniqueness check so we need to compare all the elements with each other and with that make sure that that there's no duplicate entries in either rows columns or sub squares so that's the conditions we have to check for entries and then we put that together we define one global counter and that constraint or in that in that system and then we check these conditions these checks return zero if they're all different so we just do that for a sub squares we do it for rows we do it for columns and in the end we assert that the counter is zero and if the counter is zero in the end we know for sure that the Sudoku has or that the inputs we had were a valid solution for our pseudo ku possible so one more thing here what we have given as our task is to solve this puzzle here on the left side what we have also is our internal modeling structure how we model that in the code and now we have to specify which of these points are given so we kind of have to say okay this is the possible we have to solve and we do that by specifying input parameters in our main functions that are later the public inputs that become public together with proof and in that case we have a 2-1 for example this entry is three because that's what we see in this system here so that's how we specify that part and then for the solution we have private inputs 2 1 4 4 1 3 1 2 1 3 that's a solution I showed earlier right that's just how you fill out the others to come up with a valid solution and now I want to do something that's always discouraged when giving talks I want to do a live demo so I'll have to put this down I hope you can still hear me I'll just give it a try if not you let me know wow that's that's awesome thank you unfortunately I can't see right here but I'll look over there and all that it works yeah okay I just tried to turn mirroring on real quick if I can find my mouse yeah sorry about that okay here we go I'm added okay can you read this is this okay all right okay we should be fine now so okay what we have here oh let me remove this really quick so we have a clean directory state so what we have here is our pseudocode checker right that's just the set of conditions we have and I just showed you that on the slide set and then we have the Socrates to which we will now use moving on so what we do first is we compile these yeah these this program in two set of conditions so we simply do circuit us compile and give it an input file and that's a pseudo cout checker code and it writes it to another file that the out codes to human readable one so we can say see it's a set of human readable equations that are as expressive as a rank one constraint system but that's not too important for now so we we we compiled it basically what we can do now is we can find a witness for this problem so we essentially need to find a satisfying variable assignment for this set of constraints I just showed you and we have to do it so we can later find a proof so I do circuit us compute witness and I have to provide the arguments which I showed you for the arguments of the main function here and I prepared it a little bit so it's faster okay so now we have the public inputs but the private inputs we need to specify them still and here we can do that interactively so the other parts of private solution what we actually fill in the pseudocode possible that is what we now have to space if I so I'll just type in what we had in the solution before so field a 1/1 was a 2 then we had a 1 then a 4 a 4 again 1 3 1 2 1 3 I will not make a mistake now but believe me if I would have made a mistake this will trash and show me an error okay but it would just take too much time so I immediately immediately put in private inputs that satisfy the constraint system so what we have now here is a file that contains a witness and as you can see that's just a variable assignment for all of these variables we use in our constraint system before ok because that's how we model equality checks because for equality checks we asked that there is a witness x by some input is 1 so there is inverse element and that's in it's it's inverse element so that's what we calculate internally and that's why there is those huge numbers and in the system ok ok so now what we have is we have a solution to our constraint system and we have the constraint system but we have not done a setup phase yet so that's what we have to do next and because we do not have good distributed setup yet we do local trusted setup so we do circuit test and set up and that gives us a verification key and approving key we can see that and files but what's interesting now we can use a tool to actually generate a solidity smart contract out of the verification key that we can afterwards use to verify the computation on chain so let's do that we do Socrates or what's the command oh I show you another nice feature you can have a command line overview here so it's export there and then if you get a smart contract the solidity smart contract that does then all the necessary checks to yeah validate the solution on chain so what we do now I have already deployed that to the robson test network so I uploaded the code so you see I'm not cheating here so this is actually the smart contract we just generated only that it uses a different verification key and here I already did some transactions but what I want to do now and I use the remix IDE for that is I bind that contract that's already deployed to the smart contract I have in here so I can conveniently use their interface to invoke the smart contract and then I can here generate a proof based on the witness and the proving key I already had and then I get that down here and I already have it prepared here in a way where the output is formatted nicely and can be directly pasted into the solidity web IDE so I will just paste this down here and my new instance instance and say verify transactions that may take one second no madam asked will ask me whether I'm ok with this transaction so I say all right I want to do it let's go on Rob stone and then we can check the verification contract in case we're still yeah so we have a pending transaction here now and we'll have to wait for it to be mined for just a second it usually happens quite quickly and Rob soon okay so it's might now let's look into it Bart was it wrong okay let me go back sorry oh here it is okay sorry about that okay and here we can go to the event logs and check the message so the event was issued that the transaction was successfully verified so what we did now is we actually checked on chain that we provided a valid solution to the Sudoku puzzle [Applause] [Music] what what's maybe interesting to note here it was quite expensive though so it cost 1.8 million gasps so that's quite a lot on the main net that would mean you could currently do six validations in in one block so as six verifications in in one block and why is that I'm gonna go back to the slides that real quick okay so what happens thank you very much we we generated the proof using the circuit test tool and that proof has eight elliptic curve points at least with the current C case and our construction we use as I learned today it could become even less and then the public inputs and they are used in the verification smart contract to check the conditions and for that you need five pairing checks for elliptic curve additions and depending on the inputs the number of public inputs you have to generate the customer vacation key there several elliptic curve multiplications so that's there are the new precompiled contracts that were introduced with byzantium and this is currently quite expensive but maybe there will be better constructions that make it even cheaper to verify those proofs on chain so to sum it up you can check out the source code and I'm happy for contributions I think regarding the domain-specific language we're we're at an early stage right so it's working but we would need efficient implementations of hash functions so we can do good commitments and as Sean pointed out there might be some other challenges we need to talk a tackle so we're in contract there and also an integration of a distributed set of phase will of course be key for adaption adoption on the network so you can actually prove things to third parties and in that case with a Sudoku example only I could deploy that thing and trust the proves that someone sends to me because I did the setup and I know I forgot the toxic waste involved I could not convince a third party of that at that point so there's some work to do please talk to me if your interest in that and thank you very much [Music]