zkSummit - Circom and Snarkjs - Jordi Baylina (Iden3)

Transcript

well hello everybody i'm gonna i'm george by lena from idol 3 and i'm going to talk today about two tools one is called circum and another is not Jes silcone is my need to build circuits to be used in zero knowledge and aznar Jes is an independent implementation of the zika snarks protocol fully rated in in in javascript so let's start well here i have an introduction i'm sure that most of you are ready now what does zero knowledge if you are in this place but just to just to focus you know it's like we have a silk read sometimes it's called a stuntman or a terminus T

program but have an input have an output input can be private or public no put and array is that you execute that that program your ticket that deterministic program sometimes this program can be understand I'd like to understand it very much as an electronic circuit so that you have inputs either electrical input signals and then you have an source and some you know some combinations and you have an opposite they are not really electrical signals and they are not in an either binary but it works very much like what that way and array it's quite quite easy there is that we just execute a circuit and then we proof that which cuted that circuit but without revealing neither the inputs nor the internal signals we just prove

that we executed a circuit in a way that the output and the public inputs were that specific okay that's the zero knowledge the zero knowledge proof of course the proof must be okay and and and another characteristics but that's area so yes that's what we want to prove but how we write those circuits what are those programs well so I told you there is let's start with a very very simple circuit this is an electronic circuit it's a NAND gate okay here you can see for example the truth the truth table so depending on the input of the signals

you have a specific output the interesting thing is that this input can be converted to a constraint system so here we have only three signals and whatever output we have here we need to find as 1 and s2 that follows this signal you see that if s1 or s2 it's equal 1 then 1 minus 1 is 0 so s3 is 0 is this case of here and if s1 or s2 is 0 then 1 minus 0 is 1 and then this this feature and this is the this is the constraint ok so how would we write this circuit in circle here we have the single implementation we see here that we define a template is

: we define the signals in this case we have as 1 as 2 and s 3 s 1 and s 2 are inputs s 3 is output and we just here we just assign s 3 to 1 minus s 1 s 2 ok so this would be and of course this is just a template and then here we instantiate that template that would be a minimal signal and a mini more like a hello world of a circuit okay as you see but this is a very trivial probably so very useless circuit but it would be a circle okay and you see here very little bit we you start you see here what's the taste of a circle how you write this what else can you do in in silicon silicon is

mainly a DSL a DSL language so that is that you can build circuits in a bottom down so you do a you have a like a big secret that's decomposed in the smaller circuits the smaller circuits are the compost and the smaller and smaller smaller and then you have all the hierarchy of the Silk witted at the end you go to the wire the same way very much the same way that when you design electronics that you are just putting small circuits together to make bigger circuits then you end up building whatever Silkwood you want to build hash functions and anything you can imagine out of there okay so here how it works well here of course the you have the system of equations here we have five signals the system of equations is well

here's the first name this is a second man okay and and here are this distance which is must must feed this is what we are proving we are proving that we know all the signals that so we'd be given some in this case s2 s4 and s5 we know s3 honest one that fulfills this constraint system that's mainly what we are proving in us so how do we do this yeah well we have this template this is the same one that we had in the last slide well we changed the names here we have input a input B the output and then we have the output and here we see how we compensate that so here we have the scene the signals - well three inputs one output and one that's just an

intermediate signal is this s3 okay we define also as one as private in this case here we instantiate the two templates of this none and then we just connect the signals then we just connect the signals there we just assign so as one goes to G 1 dot a as - 2 G 2 1 dot B here G 1 the output of G 1 goes to the a input of G 2 s 3 goes to the B input of G 2 and the output goes the output of G 2 goes to s 5 you see here a normal DSL not normal way to connect and now we get create a bigger a composite but from Diaz can be as we can get another bigger one and we

can we can connect and we can generate this composition okay so this is very good it's bad so it's a good way to design it's very different but it's just the people that can from the like the electric engineers it's quite common to design circuit this way so ok let's go to a more another more useful circuit this case as I told you here in in these circuits the inputs are are here should be binary okay but internally all the circuits we work in the field the field is a some number between zero R Prime and the prime

number close to 2 to the 50 so with 256 bits so it's our big big numbers so here I'm sure that we are able to find in this constraint systems some signals that are neither 0 nor 1 so that they are not binary that may be fulfill this circuit and that's not what we really want so it in many cases when we work to really work with binary circuits there is one important circuit that mainly what it does is come it converts a field number to binary inputs so what we do while of course you see that the binarization so if you b0 is

binary so b 0 2 to the 0 plus B 1 2 to the 1 plus B 2 to the 2 2 must be equal to F ok that's the first constraint that must fulfill these ok and the second constraint is that that is that the outputs must be binary how we do that well we add this constraint for each of the output signals in this case is V 0 times V 0 minus V 1 this constraint can only be fulfilled if B 0 is either 0 or 1 if B 0 is not neither 0 nor 1 then this system will never fulfill ok so here so here is mainly how we build how we do that in circum well easy that

the thing is that ok we have an input itself we have three outputs here I want to show here that circum works perfectly with a race actually work with multiple dimension of rice so in this case we have three outputs given array and then here we construct here in this case we construct these these constraints in this case is the second line of here so for 3 times B dot a equal V dot I minus 1 equal equal equal zero this equal what you live here is you are adding a constraint okay and the last constraint here we do it here okay so it's B 0 plus 2 times V 1 plus 4 times V 2 must be

equal to must be equal to F okay and here you will see a special operator that's an arrow but just with a single line arrow in this case what we are doing is we are assigning like by hand the what's the real value or that should go to V V I in this case is f as life is lifestyle this this line the difference between this and normal and a normal assignment like this is that this adds like a this adds our constraint in this case for example here this it assigns the this value to s 3 plus at a constraint that s 3 must be equal to do

this with a single arrow with a single arrow with a single arrow we just assign the the value but we are not adding the constraint in general when when we are we can split between the assignment that the witness calculation and then the constraint into different into different into different lines this so mainly is a double arrow is equivalent to a single arrow to an assignment and a single a single equity why is that well mainly circum it has like two rounds when it compiles it have like two runs in general the first one it constructs the constraints system and the second round

it generates the code to compute all these intermediary circuits so it's actually it does it generates the code that computes all that brands are synced with the doujin that generates the winner the generates all the intermediary Terminator signals so this this so this the secret is executed like two times one to generator constraints and then is that when you generate the Khan are calculating the witness here it says how you put how you calculate the the signals how you calculate these intermediary signals okay so let's go to a more interesting one here imagine that

we want to generate a create a library of you know for Janet for any number of binary and here is what we call with them that's why we use parametric templates we can generate a set of set of templates that are parametric in this case the parameter is the number of output bits okay so here you see that the this in the template we can define an end so in this can define different parameters in this case is just n and of course we have input F the output have n okay and of course the loop is ends and here the interesting part and here is that we define this body about LS so

it's like this is linear combination one but that I start with zero and this because it this this work so it will be different when it computes the the constraint system and when it compute when it's cut is used to calculate the the code for generating the the witness in the when I'm computing the constraint system when I am adding flc1 x lb y Y what I'm adding is this to the to the linear combination so I'm not really adding I am just joining together in the in the in this face of generating the of generating the constraints but

when I'm computing the when I'm computing the the the the witness then here is execute the way this is I just says that LLC 1 must be equal to F so it does actually does nothing because what it counts is this one okay so you see it here is just a general a generic way of creating circuits okay the same as the same that yeah okay let's go for let's say another more complex system machine that we want to do a binary other okay and we want to add binary binary your parents but I can

have like em operands and each or parent have n n n bits okay so I want to have imagined that a 64 number binary bit plus 64 number bit plus a 64 number bit so I want to do a 3 politician of how would I do this in in silicon well here first of all is we need to understand what are the constraints that I'm building here the first one is actually what there others does well here you see that the number of outputs is not n is n plus C because you know you have like a chorus if you have two two operands we will have one bit of curry but if you

have three four five opens the the number of carries will be will be higher okay so here is the constraint system here mainly this is the first operand put it so the first operand with in a binary so putting just starting with the winery's this is the second operand you have all the operands and this must be equal to the output okay and finally for each output we also force that our binary with this system we add or everything all together okay so let's write that in in in circle here is well here this is the bin sum here you see that there's been some have two

parameters n which is the whole white is the operon M is how many operands we want white okay and here we calculate the variable that's call and out is mainly it's how many outputs should be and here to calculate that I define a function a function that's called and it's okay here what I pass is how many bits how many bits have a okay here is what I'm asking here is how many beats has the maximum number that I can add these are the maximum number for each operand is two to the N minus one and because there are operands this is like the maximum number so what I'm doing is how many beats have these

maximum numbers and well here what I'm doing is mainly I'm just trying you know it's just I'm starting to zero one and so I'm adding a bit adding a big that any beta when this is gets higher than and then I stop okay so I have here input signals of M and N and C is here the the the multi-dimensional alright and then I have an output of the number of outputs that I generated before okay and then what I'm being is well here is for this is for for the first this for mainly for I'm calculating for the first side the left side of the constraints is called left left in this is what I'm

doing is just adding for each operand and for each I'm putting this side okay in the end up in the here in the other side I'm calculating all the output and here is the inequality so here is the constraint so here we go stroke all that and then of course for our outputs I just put I just put that constrain it's where that's been binary so all this constraint and then of course I need to calculate the outputs by hand so I'm adding this so I'm just calculating what's the alene that the width of this alein so you see here with not many lines of code you can do a quite complex binary circuit quite complex binary circuit okay okay let's

go to the next example the other interesting thing is baby job baby job or job job in the in the case of snarks but in here we're working very much in the first version in BA in theorem well it's just a normal little curve that have the property that the field the order of the field of that works in the Corp is exactly the order of the curve that we are working so there is that when we are are multiplying or adding in this formula we can do it in the same circuit so this is so here it's just a multiplication that's not a multiplication that's normal addition so creating these formulas in a circuit are very easy and

are they are very cheap in constraints and these allows this is a secure curve so it is allows to what to do anything a lot of cryptographic elements inside the curve okay for example you know signatory schemas hash schemas and many other many other things okay so how would you do you add in the curve here you have X 1 a 1 X 2 is a 2 and here I just calculate with the formulas I just calculate X out and white out you can see that you have 1 2 3 4 5 & 6 constraints with a single full addition of an elliptic curve which is quite

optimal for for that but you see that writing that in silicon is is quite trivial ok so it's not it's just multiplying and calculating them all together ok here what I want to present here we have a circle it needs a little bit of documentation if you go inside but here in silicon we have implemented with a lot of components of red you know Vinnie fields and binary converters or the baby hop ad networks and Montgomery you know baby the baby hop while this this kind of course can can be interchanged between the Edwards of

Montgomery and and it saves a lot I think Montgomery instead of 6 constraints these are half only 3 but you cannot add the zeros and you have to take in account in that but depending what you are doing it's convenient to change the Montgomery do a lot of operations and then change back to Edwards and all that stuff we can have the other a VDS a implementation the Patterson implementation than in c7 which is not sure if it's there safe or not but they are also implemented in these we have all the sparse miracle tree implementation here are for verification inclusion and exclusion verification and also all insert and delete it's for insert that they'll update and delete proofs insert

as parts marquetry they are all implemented there or sort of comparative comparators logic operators even there is a sha-256 features there and many more that we are writing on there so well this is like a it has been very much used to also to to improve and to test that circum is a good way for writing components in a zero in a in this context and silicone connects very much with snark Jas not Jas well as I told you is an independent implementation of the sickest North's protocol it supports the classical pine

pine ochio schema but also the growth 16 which is much more optimal okay it's pulling writing in JavaScript I know that javascript is not well it's the worst you know is the pro is the worst language to write anything about in cryptography but the nice thing that it works in the browser quite well and right now we are we're talking later but we are rewriting that everything awesome so the it's quite optimal well it's fully browser compatible which is cool so of course it's a flew absolutely open source and party ball and it's very easy to use no we are going to do a demo it's an NPM library so you can create your programs and that generate the prove

that test prove that verifies the proof in a normal in JavaScript so in note or abroad you know in a browser so that's like the cool thing of snark Jas okay so let's do a ok I've explained that or so let's see how it works so I'm going to do it's just a small demonstration here you see that well to install them I already have in started in my Computers while you install us on normal as a normal inside as a normal JavaScript NPM package okay well I'm gonna create a directory okay I'm going to create a program in this case is I'm

just creating a program it's a multiplier mainly you see here that's very easy program you know two inputs one output and then the output is just the multiplication of Amb this well you can understand you know that factoring two numbers is not it's quite difficult so there is that you prove that you know the in this case they are private so you would prove that you have two numbers that when you multiply them together you gives you of course this is not a practical circuit because we here we are not working with natural numbers we're working with the field numbers so I can if I have a I can just find the inverse and find the other that multiplies that

so if this is not a working program so then working problem is just an example of how you would do it for this is a single a single circuit okay so you here what you are proving is that you know two numbers and when you multiply them in in the model lose this this this big prime number it gives this number okay so we already have the circuit there it's called here while we created here is multiplier but circum so no the next thing that I'm going to do is I'm gonna where I'm going to well I'm going to compile that here well I just compile it I'm just okay the input is silk um and

the output is just a JSON which is just a compiled version so we will see the constraints and an info and all that stuff for example I can see the info of this circuit here we see that well the silk with half just it's a very small circle but have four wires one constraint to provide pivot inputs and one output okay so that's the one thing here you see that I pass the compilot version of this the other thing that I can do is for example I can print the constraints that it generated this the the compiler okay so here it just generated one constraint

that says a times B equals well minus C equals zero so the - can well mine well here is a with a negative so the negative cut this side can go to the other side and this might not be this - cause this is because it it goes this constraint systems that go with a standard format it's a linear combination of the signals times the linear combination of the other signals - linear combinations - the signals equals zero and this is many times okay so this is put in the in the system but here you can see all individual in all the constraints this is good for for debugging and see what generate the code okay so next step well we need to here

within a normal in a real silk with here we would run we already have the secret we will run that trusted that that trust is wrapped okay so here's a multi-party ceremony this is like another story in this case what we are doing is a trusted setup in my computer so it's not really address the setup is you have to have to trust yourself but for testing everything it works it works okay or it could work even if isn't if you wanna so I can compile a circuit then you can and give you the trusted setup to you and you can prove to me so for individual proofs it also would work okay so here let's see what it does there is a long line see if I don't

forget okay what did this of course is a setup the input is the the output of the compiler the silk with that I want to generate the trusted set up for it generates this is the it generates two files one is the proving here and the verification key the proving key is all the information that you need to generate proofs and the verification key is all the information you need to verify that proofs okay and in this case I'm also specifying the the protocol de Graaf about the graph 16 okay that's the protocol that that that that I'm using okay so right now if we see what we have here well we have the of course the circuit we have the the circuit compiler

and then the private the the proving key and the verification key okay so now we can start creating proofs okay but the first you know five minutes only okay okay okay I'm going fast okay generate I'm going to generate the proofs first to generate the proof first I to generate the proof first I need to create I need to execute the circuit so I put a just create a file with the inputs of the circuit okay then I calculate the winners or if you want you run the circuit so with those inputs

here you see as an input as an input calculator witness to the silk weight you get the input and then the output is the witness if you see there are the output here we see all the internal signals that generated so mainly what I did now is I just run this circuit and generate all these signals in here okay and now with this weakness I know I can generate the proof okay so to generate the proof generate the proof of course I pass the

witness I press a proving key and it generates the proof plus the public which is just a subset of the signals with only the public keys if I see the public it just have the 33 but I already have the proof if I see the proof here here is all the the points that actually makes the the proof okay I know that I have the proof for example I can't verify I can verify that proof in this case it's okay here it's verify you pass the verification key you pass the proof you

pass the public input that's what you really want to verify and then it says that's of course that's that's okay okay now let's go a little bit further okay the other thing that I can do here is generate just in this case its generator solidity version of the prover okay so I can do for example cat very fire okay here it's a full very fire okay so what I'm gonna do here so let me see if I'm ever see if I couldn't paste and I'm going to go to

remix okay so I'm going to put all that to here okay compile well it's for 25 I already have it set up okay so I just generate the verifier okay and I'm running in in in this case I'm running in in rinkeby okay so I'm just gonna deploy it let's see if it not takes pretty much let me just go with a higher price case so I'm deploying this contract here let's see if it if it does not take all along oh this is the old one here is it's already

deployed okay so no I should try and I should call the verify if you see the very fire of a proof here where if I prove here I see is this the proof on the input you see here is the proof on the input okay but to generate all these parameters in it's not GS I can do it so I have a special option just to generate this so these are the parameters but especially here what I see I put here is generate call with the proof that I want to really prove and the public is so I just put all the calling all the calling parameters so if I couldn't paste this okay you can go directly to the remix

and paste here so if I verify the proof it says okay so proof for example if I change any number for example instead of here let's put 20 to verify the proof it those false okay so I just generated a full circuit created through the setup I generated the proof I deployed a contract I verified it oh gee so that's very much little bit how this Tool Works so I think I'm running [Applause] so here just to finish is the current status of what we are doing in item 3 on

this snark so we are working very much in optimizing so we are working a lot in optimizing optimizing all this is not jst and we're possibly so we can generate proofs from the from the system very fast we have the also working with a GPU of demising and so on and we are also working in silicon just to to generate bigger circuits and to optimizing a lot and that's it that's I don't know if we have time for questions but thank you if we're light so we can we can we can talk we can talk whenever you you want ok [Applause]