zkSummit - Zk0x02 - Towards friendlier SNARKs with ZoKrates - Thibaut Schaeffer (Zokrates)

Transcript

[Music] hi everyone I'm timoshev today I'm going to be talking about Socrates so giving kind of a general introduction for those of you who are not familiar with the tool and also kind of talk about some of the concepts and ideas we've been working on recently again yeah check out the episode that's going to come out soon with zero knowledge podcasts I should be a good one so the first I should mention Socrates would start it was started in a tu Berlin and we're proud to have had

the support of the etherium foundation since the start so with that out of the way let's jump right into it so one way we like to think about it is that in the blockchain space since Bitcoin we've basically seen two main trends one trend is towards more generality with a theorem and smart contracts and everyone can write whatever they want and you have all this freedom and privacy on the other side with Z cache with kind of more private systems what we think Socrates is that by combining those two aspects we're likely to bring more

innovation into the space and to let developers come up with the actual interesting use cases so we really want to be up there on the right on this graph however if you look at Z cache there's amazing systems being built at Z cash however for the average developer it's still really really hard to get started with as you know it's proofs because the abstractions are being used are very very low level and very close to what you would be doing with a an actual circuit board where actually would want something a little bit more high level and developer friendly to get started so we want to enable developers to write

privacy-preserving applications and maybe I can kind of give a quick overview of what that could be even though of course the use cases will be found by the developers eventually so in general approving facts and private data is something that that you can do with those systems in particular proving membership in a Merkle tree Sheila token schemes schemes such as desi cash scheme as well commitment schemes and finally maybe another type of use case that we were also looking at which is not directly linked to privacy itself but it's compression so taking for example a number of proofs that were generated

like like normal using other tools and kind of take those proofs that input and then compress them to have one single sixteen proof that kind of sums up all those proofs as input and we have some some project who are using Socrates to do that for more on the applications we have a panel this afternoon that's that will go more into what people are actually building with those systems so given all those applications the space is especially the etherium community thought oh that would be great to be able to use those tools however there requires some cryptographic primitives

that are quite specific and for this familiar with theorem only theorem you can only use this EVM the virtual machine and actually implementing those primitives on the under on the EVM was really really costly in terms of gas so last September last year there was a hard work in a theorem which introduced three whiskey three new primitives and in the form of pre compiles where we call pre-compose which are basically primitives that you can call from the EVM but that can be much more complex and for which you pay just a fraction of the cost because they're not executed on the virtual machine itself but they're executed natively on the host so you kind of have a huge savings

on that and this primitives were elliptic curve operations on LPN which is the curve that's currently used in NZ cash so including paring checks and paring checks are known for being kind of the underlying cryptographic tool necessary to use the current zero knowledge systems such as the one used by Z cash so that was added into etherium making it possible for anyone to go and start doing the real knowledge proofs on the theorem however that did not really happen because they were just introduced as this very very low-level primitive but there was no way anyone

could actually take that and actually build something on top because it was so low level you didn't even have this room the proofing system you just had this very kind of basic primitive so yeah here's some tools to go and use them it's actually not that easy so that's where though queries comes in and what we actually built is a domain-specific language where you can define your computation your privacy-preserving computation so arielle talked about like public inputs and private inputs that's something you can define directly in a Socrates program so here we have the main function and the main function has inputs the first input is private which means that when you're going to generate

proofs this value a will not be revealed and has also public input so the value H will be revealed and in this case what we're doing in this program is proving that we know the preimage of a given hash so you kind of feed your secret preimage a and you feed the public hash h and then you basically return one if the hash of a is equal to the public hash and then you have some hash function that you can define in Socrates as well and so on so trying to have this very like high-level abstraction for people to build on so what it looks like in general is a

whole pipeline of tools so starting from the domain-specific language we have tools to Jen to actually run a setup phase similar to one run in Z cache which generates two different things one thing is approver and the prover is basically a piece of software that will be run let's say on the client of the prover or whoever wants to use the application so in the cache that could be someone wanting to spend some coins and that's something that's completely independent from any blockchain it's just a piece of software that lets you generate proofs and the other piece of software that we generate in the other

target is a verifier typically and what we built is that our verifier is actually a piece of solidity code that you can deploy directly to a blockchain so that end-to-end you could have someone generating a proof on the client for example proving that they are above 18 and then sending this proof to a smart contract and a smart contract you just take this proof to say okay this is valid and do some access control based on that so this is a kind of use case that we're looking at currently so great we have this disturbing at this I love a language so we can start writing all our programs in it and everything will be

fine so that's basically what we did so we wrote as seen in the previous example we we wrote we implemented in the hash function especially the sha-256 compression function so just one round of sector 56 and here's how it went so as you can see our implementation has our kind of naive implementation has 250,000 constraints and in the case of of those systems the more constraints you have the less efficient your your system is because if you have a lot of constraints it's going to take a lot of time for the prove her to generate the proof and for

the set up as well to be executed whereas lips nor gadgets which is the kind of light the kind of library that most developers use currently has an implementation of shadow physics in just twenty seven thousand constraints so of course our implementation is very naive and we could have more optimizations but our approach is to say oh we have this great implementation already why not just try and kind of import that into Socrates and see how we can kind of interoperate between between those two so our goal is going to be to find kind of a common language between those two tools kind of Socrates and other tools

such as lip snark so we looked at what good candidates we could have for this kind of interoperability between the different tools and you can see it as Socrates and the little gadgets kind of standing on top of this common obstruction which is basically arithmetic circuits and art Matic circuits can be represented in this form called R 1 CS or went Rank 1 constraint systems which is actually pretty simple it's just a list of so-called constraints and each constraint is sort of a an equation like this where you can have one multiplication so here W times this kind of product and so only one

let's say on the left and a no multiplication on the right and then the elements that you multiply need to be only linear combinations so like is some factors of your variables right so you in terms of art mistake take circuits you can think of it as a circuit that has plus gates and and multiplication gates and in this case what each variable is it I live in a prime field which is basically a field that has which whose size is a prime at a very big prime right so this this is a very simple abstraction and it say ok let's let's use that we just take the let's

norwich just compile it to our once yes take that feed it into Socrates and there we go we have our twenty seven thousand constraints hash function so when we did our implementation of sha-256 we were basically very close to our once yes saying okay would create a first constraint and we said some some of the values some of their variables some values and then in the next constraint we can reuse some of the variables and say okay this is another constraint and then by going through all the constraints you can find a solution to this system right so just looking at our once yes you can actually write complete programs however if we look at something that we want to do which is turning a

number into its bit representation and that's something that's really useful especially in the case of sha-256 because child 256 is based on bits so you actually yeah you absolutely need to have a way to kind of represent bits in to implement this algorithm and it turns out that if you want to take a number which is living in this kind of prime field so it's just like an integer and you want from that to output the bits that represent this number and imagine you only have this abstraction that we had before which is just a bunch of constrains there are just multiplication and additions actually it's going to be really really hard if you just has those

have those tools to go from a number to its bit representation but here we can see what's actually being used in the systems in order to have efficient circuits and it's the following is to say instead of executing the kind of bit decomposition in the circuit I'm going to have this first line with with the kind of hash tag there where I just set two new variables c1 and c2 to being the result right so it's really easy like off the circuit to find a bit Robinson representation of a

number and then this is not enough right if I just come up with two values then I could come up with anything and then I could I could even put like five and and and for which which wouldn't make sense so then the important thing is to then once I have the result of the computation I need to have a bunch of constraints that make sure that this result is actually correct so in this case if I come up with c1 and c2 which are the bit representation of C then I need to check three things I need to check that C is actually equal to c1 times 1 plus c2 times 2 right and that's actually just one constraint it kind of

it it works in our current abstraction of just being one constraint in the system and then I also need to check that c1 and c2 are actually either 0 1 right because I want to make sure that those are actually bits so to do that we use this trick where you just make sure that the square of the number is equal to the number because 0 times 0 is 0 1 times 1 is 1 and there's no the number that satisfies this equation in the prime field so the kind of general idea is to say ok we have this computation but actually a lot of the times it's way more efficient to do the computation of

the circuit and then just verify the computation in the circuit and that's what we're doing here where we can do bit decomposition is your three constraints and if you have more bits it actually scales linearly right so this is something that was not capturing the are ones yes are once yes just told you that those are the lines that those are pretty much what Arwen's yes is but our one CS doesn't give you this and of the way to solve the system and that's something that we also need to carry if we want to interrupt rate between different systems right so from that we came up with this very simple abstraction where you have basically two just two things and circuits one thing is assertions and assertions

you can think of them as being the exact same thing as ah once yes is just a bunch of constraints a bunch of equations that need to hold and you have solvers which are ways for someone running the program to find actually which values to set to the variables before they can check the constraints and those two things are necessary so that we can kind of take advantage of all the the power of the like the Shatford six lips Tariq implementation [Music] so we kind of took that approach and applied it to sha-256 and this is what we ended up with we have basic here's oka dysfunction which is a wrapper

around the shot if it's a clip snark so the way it works is that sha-256 in our case takes 512 inputs I have one too many here so it takes your inputs and then you have this solver so nothing happens on the circuit itself but the solver just takes the whole constraint system for sha-256 in limbs dark and just sets every single variable of the system to what it should be right so based on your inputs it sets all the variables like all the intermediate variables there's actually twenty-seven

thousand variables and sets them to some values and then that's something that's executed in lip snark so from Socrates we actually do a call to lip start to say hey what's the solution to this big constraint system for for those inputs and lip starts going to give give us okay those are all the values in it you have but then again that's not enough so we need to add all the constraints and again those constraints we can get them from this nor because lips mark has the whole circuit and then we can just verify those constraints and in the end we just return whatever is a subset of all the intermediate variables is our actual output in this case the 256 bits so we

have this in in so kittens kind of first step that that we took in this direction but we actually want to go further to actually have a real way for systems to interpret interoperate and for the r-1 CS part for the constraints part this is actually really easy because it's just a bunch of constraints but in this case when we did our sha-256 integration we were still calling from lips from from zouk it is to lip start to get the salute the witness to get the solution to the system and it would be actually great if if you could actually get the solution to a system without having a lips mark

at all so the idea would be to instead export front lips nor with Miss generation this kind of silver bit and kind of have that alongside the constraint system so that you could directly import and have the the witness generation in included so what we experimented with so of course the lips not solvers which I described earlier inside Socrates we also have solvers that are being used inside a language in some cases to to to kind of resolve the constraint system and they're written in rust and one idea we have is to use webassembly in order for all the different tools to compile their solvers so that then you

just need to have a web assembly runtime so that you can run the solvers for your system and that doesn't have any security implications because the whole security every system relies on two constraints and not on the witness narration so having something that's really really portable here makes makes sense to us that's that's something we're looking at as well so in terms of the kind of next steps that we're looking at so having more stuff on interoperability making it easier for the systems to interoperate too so that we don't have to re-implement sha in every single tool box when in stay we

can share those implementations we also working on a type system so we have two main reasons why we're working on type system so in region of Socrates there's only one type which is field elements but this can be very cumbersome for developers work with especially if you're talking about a hash function then you have like 256 outputs that sorry easy to work with so the first kind of type that we would want to have is kind of static erase so that you can actually Enzo Curtis have this array which represent a number of values and then this gets compiled down to the actual filaments and there's the second use case where the type system is going to be really interesting is for safety

itself so when you're talking about bits you always need to make sure that whatever variables represent a bit so in this case the c1 and the c2 here all of this only makes sense if c1 and c2 are 0 or 1 and that's something that we we're looking at enforcing in the type system itself so that if in Socrates you allocate a bit then it's going to automatically make sure that this bit is always 0 1 all the way through in your program finally integrated with other backends is something we're looking at so currently we have we target aetherium with a specific proof system and a

specific curve but there is no reason why we couldn't just take vocalist and target a different curve or a different proof system as long as it's based on the are ones yes abstraction um then just a quick wishlist for the ecosystem at large because we start having people working on those tools and and some stuff that I that we think could be interesting for space so first there's this tool called bellman which is the library developed by C cache which does both kind of circuit generation and also proving and that's something that is really interesting for us for many

reasons one of them being that it's based on rust and we're also building a rust another thing is that they use the concept of streaming the constraint so that you can't you have actually reduced memory usage compared to other proofing tools the kind of the drawback of bellman is that it is developed inside Z cache so it's very focused on the Z cache use cases so it only supports one curve it only supports one proof system so if we can have bellman as a kind of community tool that people build on and add more proof systems and more curves there's already some people interested in adding the Albion curve to bellman which would be awesome as well then in terms of the curves himself

embracing BLS 12 381 could be super interesting as well that's something we're also looking at but in terms of the support currently it's pre restricted to the kind of Z cache community so it would be great to have more implementation of BLS 12 381 and that's something that the etherium foundation is also interested in so if you're interested in porting BLS 1281 to a different language just reach out I can I can help on that also having more developers because there's so much stuff to do like it's pretty much kind of open territory now so we have interesting topics if you if you want to work on these things and yeah it's just so much to do and finally sharing I

think is something that's really important because right now the community kind of benefits of all the great work that the lip Stark people have been doing and the Z cash people have been doing on bellman but we could use more sharing like events like today or the kind of Z con conference in Montreal also meetups so I'm also looking at ways that people can connect more and share their experience with the system so that we can build best practices and have actual you skis out there so that's all for me you can join this afternoon we have a panel on the uski system themselves and also definitely check out the tool and

come talk to me if you have any kind of disagreement on anything I said I'm definitely interested to hear your perspective thank you [Applause] so I think if there's any questions I'm gonna be running around with the mic cool thanks for a great talk so two questions first you mentioned the sha-256 so it's ready now it can be used yeah we have we have two implementation one is zouk this native implementation which is not efficient and we have a integration with lip snark that you can use I can kind of

show you how to use it it's not on master yet but it's available ready cool and second question is you mentioned the types which can be boolean in the future but not currently your only support the the fields so the operators are also just arithmetic circuits so I don't have logical operators is the correct so I I have to implement logical operators myself with arithmetic all stuff at the moment is the case but once we have types you would definitely have gore and all those operators I see can you estimate the ETA for this that's something we're working on now we want to want to be sure we get it right but it should be this year thank you so my question is on the

trusted set up you said you can make the trusted SEP set up in Socrates but if I set up the trusted set up but it's not really trusted so could you use the zk z cash trusted set up for the example so that's something that would be very interest interesting to do that some something we don't have at the moment we only have the centralized set up there are some use cases which work with a centralized set up especially if you're doing to set up in your your the verifier so in some cases it's okay to have the Stratus trusted set up but if you're interested to work on having a more decentralized set up in zocalo

that's definitely something we we would support and yeah definitely any other questions oh hi thanks for the talk do you have any ideas for eath Berlin projects like sighs like hackathons high's projects that we could attempt to do with Socrates sure there is one proposal for a project which is more about Socrates itself to integrate Socrates with remix so that's more on the kind of developer tool side of things in terms of a kind of toy project that you could use that you could do

during a hackathon yeah I think you could already use kind of has fun to see what you can do it with hash functions and in general and I know there's some people from neurosis and in the room that also have some very interesting ideas so maybe kind of connect with them and and also this afternoon we're going to have this panel so maybe we'll have some ideas I've said that hi thanks for the dog in the context of verifying merkel proofs what needs to be added on socrates to be able to do the verification efficiently and ideally we could do the proof generation for multiple proofs in one

like recursive set up thing um do you mean recursive snarks I I have heard of the name but I'm not sure if that's what you would want ideally a way to make marked multiple medical proofs of inclusion in one proof okay um I don't see anything that would prevent you from doing that based on a hash function so you could take a hash function in Socrates and then implement the miracle tree on top of that and then use that so I think you could you could do it today and we have people who did similar stuff okay if there aren't any more questions we can take okay won't give you one more

but then we can take a little break before Howard Wu comes up and talks about Disick in UVM there is a precompiled contract where these trusted set up based on Z cash trust asset is that correct so your trusted set up is not based on the curve it's based on the circuit and in this case each developer comes up with the circuit so typically you would do the trusted set up so whoever sets up the smart kind of verifier does the sort of justice set up but what about the EVM precompiled contract oh the precompile contract is only for the pairing checks okay and the pairing checks are used in the process of verifying a proof but they don't they don't have any trusted set up it's okay

it's just you see cryptography okay thanks cool cool thanks a lot you so [Applause]