ZoKrates – A Toolbox for zkSNARKs on Ethereum

Hi. So, um my name is Jacob Eberhardt, and I work at the Information Systems Engineering Group at TU Berlin in Germany, and I'm here today to talk about uh Socrates, which is a toolbox for CK-SNARKs on Ethereum. So, let's first look at how transaction processing works in traditional blockchain networks. As you can see on the left, the transaction is sent to the network. It that then gets validated at the first node and is then broadcast to the other nodes, and at some point it gets included into some block after someone solved the proof-of-work problem.

Now, imagine if we had a system like on the right side, where a transaction is sent to the nodes in a network, but instead of directly being validated on chain, they get forwarded to a third party, the yellow box here, and that's where the transaction processing happens. After the processing off chain is done, the result is written back to the blockchain, and on chain it is verified to be correct. Only that verification will then happen redundantly and not the transaction processing itself. So, what would be gained through that? One thing would be scalability.

If the verification is cheaper than redoing or uh executing the transaction in the first place, if you only have to do the verification on chain, then you can increase throughput. Also, there is no such thing as a block gas limit that comes into play here because there is no need to circumvent the halting problem. A second aspect is that private information that gets used on that external node can, if we use the right tools, be kept private and they do not have to be published to the blockchain network, which is also what we not have at the moment. So, what are the approaches for that? We've heard an excellent talk by Jason earlier about Truebit is one such approach where you gain scalability by off-chain computations and then there's a verification game um played on chain and with that you gain scalability.

Another approach is a non-interactive zero-knowledge proofs. Uh in that case, you additionally have zero knowledge. That means the private information you use during your processing on that external node, they are not um revealed to the network. Okay, so what could those uh non-interactive zero-knowledge proofs be? One um yeah, proven mechanism is CK-SNARKs.

I think many of you are aware of that technology and it stands for uh zero-knowledge succinct non-interactive arguments of knowledge. And here are um several key properties of CK-SNARKs. So, the proofs are short and non-interactive. That essentially means you can simply take a proof generated by a prover send it over the network to a verifier and without further communication, it can then be verified. Also, we have a zero-knowledge property.

That means some information that goes into the processing um is not revealed to the network later on. Um verification cost, and that's a big one, is independent of the computational complexity of the initial computation. So, no matter how complex your computation is, the cost of verifying a proof is always the same. Okay, so that's a a key aspect. Now, a little inconvenience is that to specify um computations in a way that you can do zero-knowledge proofs on, you have to think in an abstraction that's not very convenient to most developers.

So, for example, you can specify computations as arithmetic circuits or rank-1 constraint systems. Of course, you can do it, but it's just not convenient to do, and that's what, yeah, impacts um usability negatively. Uh let's take a brief look at the process of using zk-SNARKs before we move on to the tool itself uh because it's necessary background. So, um here on the left, we have a circuit or a rank-1 constraint system that encodes a computation. In that case, uh we just multiply two numbers and uh demand that that equals another number.

And for example, RSA encryption uses uh a different uh a similar um construction. Um from that circuit or rank-1 constraint system, the first step is a so-called setup phase, which is needed to um arrive at the proving key and a verification key that are then later on needed in the proving process. So, this setup has to be performed once for a circuit or uh rank-1 constraint system, and then it can be reused over and over again. Um on the right side here, you see the verification process. Based on the proving key, a prover could, for example, um first find the solution for the problem at hand, and then generate a proof that it correctly executed that computation and found the solution.

and the cool thing is it could optionally supply all the information that went into the processing, but it could also keep some of the information to itself. In that example here, the prover only supplies set, which is the result of the multiplication and not the factors themselves that went into it. And the verifier can then check the correctness of the computation without redoing it. And that is much cheaper that verification process than the the proving process and with that the execution of the computation itself in the first place. Um Socrates.

So, with Byzantium, Ethereum added three new precompiles that enable CK Snark verification on chain. So, we have elliptic curve addition, scalar multiplication, and a so-called pairing check. But, the big question is how do we use that? And that's where Socrates comes in. So, the vision of this tool box is to provide a usable abstraction um and tooling to support CK Snarks on Ethereum to actually make them usable.

The goal is to support the complete process from program code specification to on-chain verification of the execution of that program code. It's supposed to seamlessly integrate with Ethereum and how it does that we'll see in a minute. Um Socrates comprises several things. One is a domain-specific high-level language that allows you to specify your computation in a more abstract way than arithmetic circuits or rank-1 constraint systems, which are inconvenient. Then, we have a compiler, which transforms these programs into provable constraint systems.

And then there's support for the different phases we need to go through with uh CK Snarks. So, the setup phase, finding a solution to our constraint system, uh which is the witness computation, the proof generation itself, and then we can also, using the tool, export a Solidity smart contract that can then be used to verify the computation on chain. Let's briefly look, um at the language. So, the language at this point is pretty close to the constraint system, but provides some more convenient abstractions to specify circuits. So, the data type we have is prime field elements.

You can just think of these as positive numbers smaller than a huge prime number. So, essentially, think of it as positive numbers. Then we have imperative statements, which is the abstraction most of you should be used to when programming. Um we have assertions, we have loops, we have conditionals, and we have functions which allow you to structure your code and keep it a bit less redundant. So, let's look at an example here, um for n choose k, or a binomial coefficient.

The upper function here computes the factorial. We'll not look at that in detail, because it's just not important. What's more interesting here is the lower part, is the main function. As you can see, the main function here takes two arguments, n and k. And then there's a return statement.

Now, in Socrates, um the arguments of the main function and the value of the return statement are public. That means, when you prove that computation, you use that code to prove the correct execution execution of that code, n, k, and the return value become public. If you do not want that to happen, if you want to keep that private, that information, you can simply not list that at as arguments, but still use the variables in the processing, as we do here. And then, when you supply the proof and the inputs, um n and k do not appear in there, and all the person verifying that thing would know is that you computed the binomial coefficient and what the result was, but n and k will not be known. Let's look at the user perspective and the command line interface that Circom provides you.

So, you start with high-level code. You write that high-level code and it get gets compiled to a set of conditions or also called flattened code. Based on that, you can then find a veriful um a valid variable assignment for that code, which is basically a solution to your program. And that's called a witness. So, you can use the tool to find solutions for your programs, and it also supports you with a setup phase, so you can use the tool to compute a verification key and a proving key, which you will need later on.

Based on the verification key, you can derive a solidity smart contract, deploy it to the network, and then verify proofs that were generated with the proving key that came out of the same setup phase. And to generate a proof, there is that generate proof um yeah, command, which takes the given witness that you computed previously, and the proving key, and together you generate a proof that can then be um verified by the smart contract you created beforehand. The internal architecture of the tool looks like this. So, we start with um code in that domain-specific language, and that goes into a portal uh portal is then flattened, and then you have an interpreter, which computes solution to the program. Here, you can decide which part of the solution will become publicly available and which part will remain private.

So, here you have the control. And then after that we do just some format conversions to um yeah, to um interface with the libsnark library, which we use for the um zk-snark operations themselves. Then there's a contract exporter, which can be used to um export Solidity smart contracts to verify proofs. Okay. Um the on-chain proof um verification looks like this.

So, on the left side here we have what the Socrates tool generated is a a proof. It consists of eight elliptic curve points and inputs. On the other side we have um a verification contract, which we also generated, and that contains a verification key. Seven elliptic curve point uh is what that is made up of. And then there's a verify function, which uses the new precompiles that came with Byzantium to um yeah, check the validity of the proof and also make sure that the inputs were correct.

At the moment a verification like that costs round about 1.6 million gas, so actually a lot. Um that means on the Ropsten testnet we can do four in one block. On the mainnet it's currently six in one block. Uh the gas cost varies a bit with the amount of input parameters we um we give with the proof, but the main cost is um constant and and rather high.

Um a couple of challenges and outlook of how we want to proceed with Socrates, what would be cool in the future. So, I think for the language to be more usable, more convenient, we would want additional types. So, for example, Boolean types. Everything um you can do with Boolean types can be done now, but it's just not as convenient to do it on prime field elements. And then some um integers that have a binary representation internally.

Um what's very important, and that's basically implementation work ahead of us, is uh domain-specific library with important functions. So, next thing we need, in my opinion, is a hash function so we can do commitments in circuits. And then signature encryption, that would be nice to have. Also, we want to look at integration of other front ends that can also be used to arrive at rank one constraint systems, for example, Buffet. Um a generic ZK-Snark challenge that is not specific to Socrates, but rather yeah, always comes up when speaking about ZK-Snarks is the trusted setup phase.

So, if you supply a verification smart contract and you want to verify something someone else proves to you, and you're the only one to be convinced, you don't have any problem. You run the setup, and you know that you did it correctly, and thus you can trust the proof, and you know that the person proving to you cannot fake proofs because you were in control of the setup. But if you want to use these proofs to um also to third parties, other parties observing these proofs on on the blockchain, um then they would have to trust you with the setup phase. So, what would be great if we could eliminate some of that trust by integrating a distributed setup phase. Um it just would have to become a bit more efficient than it was in the um Zcash multi-party computation protocol, for example, which they employed to do their uh trusted setup.

So, I think we'll hear more about that on um Friday in the CK-SNARK breakout session, hopefully. Okay, so the code is open source. It's available on GitHub. You're all welcome to try it out. I'm happy to receive your feedback.

Uh keep in mind it's a proof-of-concept and a research prototype at this place. We're actively developing it, and we're always happy for people who want to contribute to the further development. You can also contact me by email, and I want to give um credits to Christian Reitwiessner, who always provided very valuable feedback and input in discussions, and also to Dennis Kügler, who contributed a lot to the existing implementation. Thank you very much.