Getting Started with zkSnarks on ZoKrates

With zkSnarks, an untrusted party can prove possession of certain information, e.g. a secret key, without revealing that information.

Succinct Zero-Knowledge proofs (zkSnarks) are proving to be one of the most promising frameworks for enhancing privacy and scalability in the blockchain space.

Projects like Zcash are using this technology to shield transactions and make payments anonymous (rather than pseudonymous). Other projects such as Coda are paving the way for trustless light clients by using recursive snark proofs to dramatically reduce the number of state verifications blockchain clients have to perform when coming online. For Ethereum, proposals like RollUp or Plasma Snapp indicate how snarks can be used to increase the number of transactions by at least a factor of 20.

In this tutorial, we will demonstrate how to write a zero-knowledge proof using the ZoKrates framework. We will learn how to verify the correctness of our computation on the Ethereum blockchain and how to improve the efficiency of our proof.

In this instance, we will prove that we know the only non-prime number in the following list without revealing the number itself or its factorization to anyone (thus making it zero-knowledge):

[179426333, 181327921, 198492781, 533001793, 334216237]

Traditionally, snarks have been written using NP complete arithmetic circuits and finding a valid assignment on them. From a usability standpoint, this can be compared to writing assembly code in traditional machine programming. ZoKrates provides a higher level programming language (something like C in the same metaphor) which compiles down to the underlying constraint system and thus allows programmers to write snarks much closer to how they are used to programming.

We won’t cover the mathematical foundation of zkSnarks in this tutorial. While not required, you can learn more about them in Vitalik’s trilogy (part 1, part 2, part 3) or Christian Reitwiessner’s explanation. For a more basic, intuitive guide to zkSnarks check out this article.

Ready? Let’s go!

1. Install ZoKrates: To start off we need to install the ZoKrates framework. ZoKrates runs best inside a Docker container. The repository comes with a Docker configuration which will install all required dependencies for you. If you haven’t already, you can download Docker here. Next, clone or download ZoKrates from the github repository. Inside the ZoKrates folder run the following commands to start the docker container.

docker build -t zokrates_tutorial . 
mkdir code
docker run -v $PWD/code:/home/zokrates/ZoKrates/target/debug/code -ti zokrates_tutorial /bin/bash
cd ZoKrates/target/debug/

Inside the docker container, you are now in the folder containing the ZoKrates executable. You should also see a folder called code which is synced with the code/ folder we created inside the ZoKrates folder on the host machine (not the docker container) in the second command above.

You should be able to create and edit files in that folder using any editor on your host machine and changes will be reflected inside the docker container (from where you will execute the zokrates commands).

Let’s try creating a file called prime.code on the host machine inside the code folder. After saving it, it will also show up in the docker container:

zokrates@06db6c6c230d:~/ZoKrates/target/debug$ ls -a code
. .. prime.code

2. Write the snark program: Next we will write the program. Later on, we will run it locally and then eventually verify on the blockchain that we have indeed run its code. The proof we want to provide is:

Given a list of 5 numbers, one of which is not prime, we know which one is the non prime number, without revealing it.

Our snark is going to take the 5 numbers as a public input, which will be visible to both the prover and verifier. In order to show one of them is not prime, the prover will have to provide two non-trivial factors p,q where p*q is equal to one of the elements.

However, the prover does not want to reveal the factorization, since this would make it trivial for the verifier to calculate the non-prime. Therefore, we will provide the factors p and q as a private input (not visible to the verifier).

The main method signature (inside prime.code) therefore looks as follows:

// c0-c4 — candidates in the list, one of which not prime
// p, q — non-trivial factors for the non-prime candidate
def main(field c0, field c1, field c2, field c3, field c4, private field p, private field q) -> (field): 
  // TODO actual logic 
  return 1

Just like in traditional programming, there is an infinite number of ways that we can write the logic for this problem. Different approaches are going to compile down to a different number of instructions (called constraints in the case of snarks) and will affect the time and memory it takes to create proofs.

One simple approach would be to check for every input c0-c4, if it is equal to the product of p and q and if so increment a counter. We will also need to assert that p and q are non-trivial (e.g. 179426333 * 1 is not a valid factorization of 179426333).

// c0-c4 — candidates in the list, one of which not prime
// p, q — non-trivial factors for the non-prime candidate
def main(field c0, field c1, field c2, field c3, field c4, private field p, private field q) -> (field): 
  // Assert p,q are non trivial 
  0 == if 1 < p then 0 else 1 fi 
  0 == if 1 < q then 0 else 1 fi
 
  // Count how many candidates can be factored into p, q 
  field nonPrime = 0 
  nonPrime = nonPrime + if p * q == c0 then 1 else 0 fi 
  nonPrime = nonPrime + if p * q == c1 then 1 else 0 fi 
  nonPrime = nonPrime + if p * q == c2 then 1 else 0 fi 
  nonPrime = nonPrime + if p * q == c3 then 1 else 0 fi 
  nonPrime = nonPrime + if p * q == c4 then 1 else 0 fi
  return nonPrime

ZoKrates’ syntax might be a bit confusing at first sight. There are two basic types of statements: assignments (lines 10–15) and assertions (lines 6–7).

Conditional if statements have to be written into a single line (like ternaries in other languages) and return different values for the then and else case.

To write more complex multi-line branches, the code can be pulled into its own method and invoked from inside the ternary. Here’s an example of what that might look like:

def f(field p) -> (field): 
  field valid = 0 
  // more logic 
  return valid
def main(field condition, field p, field q) -> (field)
  field result = if cond == 1 then f(p) else f(q) fi 
  return result

Also, there is currently no support for statically sized arrays. This would allow specifying candidates as field[5] and using a for-loop instead of repeating line 11 five times. The ZoKrates team is actively working on adding support for arrays.

Even today this abstraction is much more convenient than writing R1CS constraints manually as it makes it easier to compose a program of reusable components.

An extended list of supported syntax constructs can be taken from the example folder in their github repository.

There are two ways in which the program could return the information that p and q divide exactly one number. One way would be to assert that nonPrime == 1. Assertions lead to runtime errors if false and thus the program would not be able to generate any output if given the wrong input. Even if we were to change Zokrates’ solver to continue proving after failed assertions, we would eventually not be able to verify the proof later.

The other option (which we have chosen here) is to simply return the nonPrime count. When verifying the computation, we can specify the expected output parameters (1 in this case). The verifier would only pass if the actual output matches the expected output.

3. Compiling the program: Before we can run the computation with actual data, we need to compile the code above. From the docker container, run:

./zokrates compile -i code/prime.code

The last line of the output displays the number of constraints of our compiled code (~1600 in our case). As a rule of thumb, a single machine with 32GB memory and a modern processor can prove a computation of up to about 10 million constraints in ~30 minutes. Research on how to parallelize execution on a cluster of machines and solving up to 2 billion constraints in 30 minutes exists, however, that framework is not compatible with ZoKrates at the moment. Parallelization and memory requirements aside, we cannot verify computations with more than 2^28 (~268 million) constraints on Ethereum due to requirements on the underlying elliptic curve.

Let’s see if we can reduce the number of constraints that our very simple program compiles to. Commenting out the triviality check (line 6,7) we see that our resulting program only contains ~80 constraints. The reason for this is that inequality checks are very expensive operations in the underlying constraint system. The two numbers are split into their bit-representation which have to be verified (sum of all bits multiplied with their power of 2 equals the original number) and then each bit is compared from least-significant to most-significant. This results in a large number of constraints.

We should be able to express the triviality check without inequality operators by inverting the condition into:

// Assert p,q are non trivial 
0 == if 1 == p then 1 else 0 fi 
0 == if 1 == q then 1 else 0 fi

Compiling the program again now leads to ~110 constraints, saving more than 90%.

Yet, even with further optimization, programs written with ZoKrates are likely to be slightly more expensive than manually written arithmetic circuits (just like manual assembly is usually more efficient than compiled code).

This is why some expensive functions (such as hash functions) may be handwritten and included in ZoKrates through so-called ‘gadgets’ (cf. this Zokrates example for sha256).

EDIT: Snark arithmetic is done in a finite field (all results are taken modulo a large prime number P ~2²⁵⁴). As Vitalik correctly pointed out in his comment below, we need to also check that p*q does not overflow that prime. Otherwise, e.g. with P=7, we would be able to pass factors like 2 * 6 = 12 = 5 mod 7, and make it look like 5 was not prime. Thus, we need to also add the constraints p < sqrt(P) and q < sqrt(P) to our snark program.

4. Running the code: Now, that we have compiled the program, we need to execute it. That is computing a satisfying variable assignment (called witness) for the underlying constraint system given a set of public and private inputs. To do this, we pass the public and private input we want to test with into compute-witness command

./zokrates compute-witness -a 1 1 1 1 4 2 2

With c0-c4 being 1, 1, 1, 1, 4 and with private inputs 2 and 2, this program returns 1 (cf. ~out_0 1 in the output), since one candidate (c4) is divisible by p and q. You can try running the program with different parameters

./zokrates compute-witness -a 1 2 4 4 5 2 2
./zokrates compute-witness -a 1 1 1 1 4 2 3
./zokrates compute-witness -a 1 1 1 1 5 5 1

The latter two should fail since in the second example 2, 3 are not the factoring of any candidates and example three is a trivial factorization. Note that compute-witness runs the version of the code that was most recently compiled by default. Don’t forget to recompile your code if you are making changes to the .code file.

5. Setting up the verifier: To prove the execution of our program, we need to create a smart contract which can verify our proofs. To do so we need to run:

./zokrates setup && ./zokrates export-verifier && cat verifier.sol

This will create a verifier.sol smart contract in our current directory. This smart contract is tied to the code we have previously compiled. Any changes to the underlying code will require us to rerun the setup and export a new verifier. The verifier contract needs to be deployed on the Ethereum chain.

A simple way of doing this is using the Remix web editor. You will also need a wallet (e.g. MetaMask) with some free test ether on the Ropsten network (which you can get here). Paste the content of verifier.sol into the Remix editor. On the right side, choose the “Run” tab, select the Verifier contract (instead of Pairing) and click “Create”. Sign the transaction with MetaMask and wait for it to go through.

Now that you have deployed the verifier contract anyone could run the code you compiled locally on their machine and prove to you that they did without revealing the private inputs to you.

Note: During setup, we generate some parameters that are commonly referred to as toxic waste. If these parameters are not removed (which ZoKrates does by default) a person gaining access to them could create arbitrary proofs without actually running the code, thereby breaking the security of snarks. For this reason, it’s important that the party setting up the verifier has no incentive in cheating or that the setup happens through a secure multi-party computation, e.g. as in the case of the Zcash ceremony.

6. Generating and verifying the proof: Let’s look at the list of larger numbers from above:

[179426333, 181327921, 198492781, 533001793, 334216237]

Can you find the only non-prime number (e.g. using Wolfram Alpha)? Once found, recreate a witness using

./zokrates compute-witness -a 179426333 181327921 198492781 533001793 334216237 <p> <q>

This witness is a satisfying assignment of the underlying constraint system which was generated during compilation. That means, for each constraint, the witness contains one element with a value fulfilling this constraint. As the number of constraints increases, the witness can easily become very large. In order to make proofs succinct, we have to turn this long list into a concise commitment. This is done with:

./zokrates generate-proof

Again, for the underlying math, we refer to the literature mentioned at the beginning of the post.

To verify your computation using the smart contract deployed in the step above we need to copy the last part of the output of the generate-proof command to the remix editor (while converting it into proper json). ZoKrates is working on printing json directly in the proof-generation step to make this step less tedious.

For now, we need to convert G1Point(x,y) to [x,y], G2Point([x1, y1],[x2, y2]) becomes [[x1, y1],[x2, y2]] and all hex values are escaped with quotes. We can easily get this format by piping the generated proof into sed:

./zokrates generate-proof | sed ‘/Point/!d;s/.*Point(\(.*\));/[\1],/g;s/\(0x[0–9a-f]*\)/”\1"/g;’ | awk ‘{a=a s $0;s=” “}END{print a}’

We also need to add the public input values (omit the private ones) and the expected output value (1) as a last argument to the list. The converted proof from the example above would look like this:

In Remix, paste this string into the verifyTx text field under your deployed contract and click verifyTx. Sign the transaction and once confirmed you should see a verification event in the detail logs:

You (or whoever else submitted this proof) has now proven that they ran the program we compiled above with input 179426333, 181327921, 198492781, 533001793, 334216237 and two secret parameters for which the program returned 1.

The tutorial is based on this GitHub commit of Zokrates. The project is under active development, therefore the syntax or other steps in this tutorial might change slightly.

Many thanks to Eric Gorski, Thibaut Schaeffer, Tobias Schubotz, Ben Smith, Anton Shtylman, Alexander Herrmann, and Nadja Beneš.