zkSessions: Thibaut Schaeffer on ZoKrates

Transcript

so hello everyone i'm going to be talking about socrates which is a toolbox for zero knowledge proofs on ethereum and elsewhere um so first of all i wanna just just give a bit of context so the project was started at the university of berlin and we now have the support of the ethereum foundation which i think in this context gives us a bit different positioning to the extent that we're not building a particular snark application on any particular system or rather we're trying to have this toolbox that gives easy access to zika snacks for developers so that leads into our design principles

so this is one one consequence of of that approach which is that we're maybe more conservative in terms of the um the proof systems that we support so we currently support r1cs without the planck extensions for example um also we do not develop our own back end instead we reuse back ends from existing implementations when it comes to the language design we really go for a very high language high level language with very high level constructs and abstractions but we want these abstractions to be zero cost as much as possible and that's why we rely on heavy use of

optimizations inside the compiler um so in terms of using socrates where would you run socrates so first in terms of the the compiler part um societies is available as a cli tool we can also if you want to try it out try it in the mix ethereum ide where you can find uh as oct's plugin so you can play around and you can generate proofs and verify them directly in the browser and in the evm of remix in terms of the schemes so as i said we mostly support the pre-processing snacks such as the one used by the

version of zcash graph 16 and we're working on including modern as well in order to have a universal stock that doesn't require a setup for each circuit for the proving aspect so we rely on the libraries such as lipstick bellman and arc and we support a wide range of curves as well finally for the verifier so you can run your verifier in the evm the way to do that is to compile a program and then you can generate a verifier which is going to be a solidity contract that you can then deploy to an ethereum

chain and send your proofs to for them to be verified you can also verify this proofs in the cli itself as well as in javascript with the circuits.js library so now to go a bit more in detail in the language itself and what i meant by high level language i here have a piece of code which is part of our implementation of the chat to 56 hash function completely in the language and here there's a lot of things happening but i want to focus on two particular things that we added recently so maybe some of you who are familiar with socrates already haven't seen those

features yet the first one is relatively simple is the fact that we now support constants so you have this four constants uh value which is part of the chat 256 specification and that is used here as the the default value for this current variable the second one is something that those of you who are familiar with rust maybe saw that was added recently to rust is the concept of constant generics um and you can see this in the declaration of the function so you can see here shot 256 of k and then this a is used inside the

signature of the function effectively what it means is that this function is generic over the size of the message that you want to pass to it so you can pass a message of arbitrary size this size has to be known at compile time hence the word constant generic and then this is going to influence the number of shower rounds that you are going to run in this loop below finally there is one concept that i want to focus a bit more on and that's something that alex talked about in his in his presentation that was really great that he did that um is the concept of uh of branches in in stocks and that's something that

can be can be really confusing for people who are not familiar with the lower level concepts behind snarks which are arithmetic circuits which you can think of as basically electronic circuits um so branching is confusing in snarks for two reasons the first thing that's confusing is the cost of branching um so here in the spain function we branch depending on this variable b and we either return the yes function or we return the no function however what happens behind the scenes is that both branches are first executed

and then the result of the execution is assigned to the result conditionally what this means is that in terms of the costs and number of constraints and the number of constraints is basically bottom line in terms of complexity of the of the circuit you're not going to pay only for the branch that you're executing you're going to pay for both branches and that's going to be both at the setup phase and at the proof generation phase so that's that's one thing that's confusing there's a second thing that's that's for me even more confusing is the concept of uh the the behavior itself of the brand the branching in the case where

one of the branches panics um so here i'm just going to look at this little algorithm and basically we take a boolean b then depending on the value of b we go in in the yes function and in the less function we assert that b is true but here the condition was true anyway so this should this should succeed and basically this whole program should just return b however what happens is that since we compute both branches if i run this program with the value true for b the first branch is going to be okay but i'm also executing the second branch the second branch as has an assert not b but b is true

therefore this is going to fail so when when the the input is true this program fails when the input is false it also fails pretty opposite reason so you end up with a program that looks like it's the identity function but it actually never you will not be able to generate a proof that will be accepted by the verifier this is something that we just released a new experimental feature on um which basically only activates the constraints that are inside your branches if those branches are being executed in the intuitive sense so only if the branches are the ones chosen by the value of the condition

in that if statement there's like this one cave yet here is that contrary to the other abstractions that i talked about earlier this abstraction is not zero costs because you need to basically encode these things in constraints themselves and encoding a conditional assertion is more expensive than encoding just your assertion itself um however we think that there's a there's a range of applications where this is useful um and so that's something that we currently provide behind a flag but that we hopefully will make uh more and more available in the future so yeah and it's also a feature that we we would really love to hear feedback on and that we're still optimizing in terms

of cost finally i just want to go quickly into the what's coming soon the main direction that we're going is first supporting recursive proofs so we already support the curves from the zix protocol so we already have a way to generate those proofs we only have the part missing which is which is verifying the proof inside the host curve uh and that's something that we are working on now and that we want to also uh provide in the toolbox second is using marlin as i described this uh proof standard still based on r1cs but that does not

have a circuit specific uh setup phase and um i mean trusted setup place and and and and finally we also work on having a simplified project configuration so as you maybe know from other projects you have this little tool that helps you with having a config file for your project etc and put your parameters there which is something we also want to to support um so feel free to check out our documentation which reach out to us on getter check out our github and uh yeah i'm happy to answer questions if there's any any time left hey so i don't think we have very much

time but there were questions here maybe i'll just ask the first one and you can go answer the others by chat sure so matthias asked and i i'm going to say it right this time sorry about the earlier question and and not saying that right um yes can you overwrite a variable that lies outside the scope of the if else statement um so we don't have if else statements we have if else expressions um so your expressions currently we don't have blocks as expressions so there's basically no syntactic way to express that so you would call a function and the function would have its own scope cool