Introduction

ZoKrates is a toolbox for zkSNARKs on Ethereum. It helps you use verifiable computation in your DApp, from the specification of your program in a high level language to generating proofs of computation to verifying those proofs in Solidity.

Background on zkSNARKs

Zero-knowledge proofs (ZKPs) are a family of probabilistic protocols, first described by Goldwasser, Micali and Rackoff in 1985.

One particular family of ZKPs is described as zero-knowledge Succinct Non-interactive ARguments of Knowledge, a.k.a. zkSNARKs. zkSNARKs are the most widely used zero-knowledge protocols, with the anonymous cryptocurrency Zcash and the smart-contract platform Ethereum among the notable early adopters.

For further details we refer the reader to some introductory material provided by the community: [1], [2], [3].

Motivation

Ethereum runs computations on all nodes of the network, resulting in high costs, limits in complexity, and low privacy. zkSNARKs have been enabling to only verify computations on-chain for a fraction of the cost of running them, but are hard to grasp and work with.

ZoKrates bridges this gap. It helps you create off-chain programs and link them to the Ethereum blockchain, expanding the possibilities for your DApp.

License

ZoKrates is released under the GNU Lesser General Public License v3.

Getting Started

Installation

Online IDEs

To get a feel of the language, try the ZoKrates playgound.

To experiment with creating SNARKs and verifying them in the EVM, check out the ZoKrates plugin in the Remix online IDE.

One-line installation

We provide one-line installation for Linux, MacOS and FreeBSD:

curl -LSfs get.zokrat.es | sh

From source

You can build ZoKrates from source with the following commands:

git clone https://github.com/ZoKrates/ZoKrates
cd ZoKrates
export ZOKRATES_STDLIB=$PWD/zokrates_stdlib/stdlib
cargo build -p zokrates_cli --release
cd target/release

Docker

ZoKrates is available on Dockerhub.

docker run -ti zokrates/zokrates /bin/bash

From there on, you can use the zokrates CLI.

Hello ZoKrates!

First, create the text-file root.zok and implement your program. In this example, we will prove knowledge of the square root a of a number b:

def main(private field a, field b) {
    assert(a * a == b);
    return;
}

Some observations:

  • The keyword field is the basic type we use, which is an element of a given prime field.
  • The keyword private signals that we do not want to reveal this input, but still prove that we know its value.

Then run the different phases of the protocol:

# compile
zokrates compile -i root.zok
# perform the setup phase
zokrates setup
# execute the program
zokrates compute-witness -a 337 113569
# generate a proof of computation
zokrates generate-proof
# export a solidity verifier
zokrates export-verifier
# or verify natively
zokrates verify

The CLI commands are explained in more detail in the CLI reference.

Programming Concepts

Variables

Variables can have any name which does not start with a number. Variables are mutable, and always passed by value to functions.

Declaration

Variables need to be declared to be used. Declaration and definition are always combined, so that undefined variables do not exist.

def main() {
    // declare and define `my_variable`
    field mut my_variable = 2;
    // redefine `my_variable`
    my_variable = 3;
    return;
}

Mutability

Variables are immutable by default. In order to declare a mutable variable, the mut keyword is used.

def main() {
    field a = 42;
    // a = 43; <- not allowed, as `a` is immutable
    field mut b = 42;
    b = 43; // ok
    return;
}

Shadowing

Shadowing is allowed.

def main() -> field {
    field a = 2;
    field a = 3; // shadowing
    for u32 i in 0..5 {
        bool a = true; // shadowing
    }
    // `a` is the variable declared before the loop
    return a;
}

Scope

Function

Functions have their own scope

def foo() -> field {
    // return myGlobal; <- not allowed
    return 42;
}

def main() -> field {
    field myGlobal = 42;
    return foo();
}

For-loop

For-loops have their own scope

def main() -> u32 {
    u32 mut a = 0;
    for u32 i in 0..5 {
        a = a + i;
    }
    // return i; <- not allowed
    return a;
}

Types

ZoKrates currently exposes two primitive types and two complex types:

Primitive Types

field

This is the most basic type in ZoKrates, and it represents a field element with positive integer values in [0, p - 1] where p is a (large) prime number.

As an example, p is set to 21888242871839275222246405745257275088548364400416034343698204186575808495617 when working with the ALT_BN128 curve supported by Ethereum.

While field values mostly behave like unsigned integers, one should keep in mind that they overflow at p and not some power of 2, so that we have:

def main() {
    field pMinusOne = 21888242871839275222246405745257275088548364400416034343698204186575808495616;
    assert(0 - 1 == pMinusOne);
    return;
}

Note that division in the finite field behaves differently than in the case of integers. For field elements, the division operation multiplies the numerator with the denominator's inverse field element. The results coincide with integer divisions for cases with remainder 0, but differ otherwise.

bool

Booleans are available in ZoKrates. When a boolean is used as a parameter of the main function, the program is constrained to only accept 0 or 1 for that parameter. A boolean can be asserted to be true using an assert(bool) statement.

u8/u16/u32/u64

Unsigned integers represent positive numbers of the interval [0, 2 ** bitwidth), where bitwidth is specified in the type's name, e.g., 32 bits in the case of u32. Their arithmetics are defined modulo 2 ** bitwidth.

Internally, they use a binary encoding, which makes them particularly efficient for implementing programs that operate on that binary representation, e.g., the SHA256 hash function.

Similarly to booleans, unsigned integer inputs of the main function only accept values of the appropriate range.

The division operation calculates the standard floor division for integers. The % operand can be used to obtain the remainder.

Numeric inference

In the case of decimal literals like 42, the compiler tries to find the appropriate type (field, u8, u16, u32 or u64) depending on the context. If it cannot converge to a single option, an error is returned. This means that there is no default type for decimal literals.

All operations between literals have the semantics of the inferred type.

def main() {
    // `255` is inferred to `255f`, and the addition happens between field elements
    assert(255 + 1f == 256);

    // `255` is inferred to `255u8`, and the addition happens between u8
    // This causes an overflow
    assert(255 + 1u8 == 0);

    return;
}

Complex Types

ZoKrates provides two complex types: arrays and structs.

Arrays

ZoKrates supports static arrays, i.e., whose length needs to be known at compile time. For more details on generic array sizes, see constant generics Arrays can contain elements of any type and have arbitrary dimensions.

The following example code shows examples of how to use arrays:

def main() -> field {
    field[3] mut a = [1, 2, 3]; // initialize a field array with field values
    a[2] = 4;               // set a member to a value
    field[4] b = [42; 4];   // initialize an array of 4 values all equal to 42
    field[4] c = [...a, 4]; // initialize an array copying values from `a`, followed by 4
    field[2] d = a[1..3];   // initialize an array copying a slice from `a`
    bool[3] e = [true, true || false, true]; // initialize a boolean array
    u32 SIZE = 3;
    field[SIZE] f = [1, 2, 3]; // initialize a field array with a size that's a compile-time constant
    return a[0] + b[1] + c[2];
}

Declaration and Initialization

An array is defined by appending [] to a type literal representing the type of the array's elements.

Initialization always needs to happen in the same statement as a declaration, unless the array is declared within a function's signature.

For initialization, a list of comma-separated values is provided within brackets [].

ZoKrates offers a special shorthand syntax to initialize an array with a constant value: [value; repetitions]

The following code provides examples for declaration and initialization:

field[3] a = [1, 2, 3]; // initialize a field array with field values
bool[13] b = [false; 13]; // initialize a bool array with value false

Multidimensional Arrays

As an array can contain any type of elements, it can contain arrays again. There is a special syntax to declare such multi-dimensional arrays, i.e., arrays of arrays. To declare an array of an inner array, i.e., and an array of elements of a type, prepend brackets [size] to the declaration of the inner array. In summary, this leads to the following scheme for array declarations: data_type[size of 1st dimension][size of 2nd dimension]. Consider the following example:

def main() -> field {
    // Array of two elements of array of 3 elements
    field[2][3] a = [[1, 2, 3],[4, 5, 6]];

    field[3] b = a[0]; // should be [1, 2, 3]

    // allowed access [0..2][0..3]
    return a[1][2];
}

Spreads and Slices

ZoKrates provides some syntactic sugar to retrieve subsets of arrays.

Spreads

The spread operator ... applied to an array copies the elements of the existing array. This can be used to conveniently compose new arrays, as shown in the following example:

field[3] a = [1, 2, 3];
field[4] c = [...a, 4]; // initialize an array copying values from `a`, followed by 4
Slices

An array can also be assigned to by creating a copy of a subset of an existing array. This operation is called slicing, and the following example shows how to slice in ZoKrates:

field[3] a = [1, 2, 3];
field[2] b = a[1..3];   // initialize an array copying a slice from `a`

Tuples

A tuple is a composite datatype representing a numbered collection of values. The following code shows an example of how to use tuples.

def main() -> bool {
    (field[2], bool) mut v = ([1, 2], true);
    v.0 = [42, 43];
    return v.1;
}

In tuple types and values, the trailing comma is optional, unless the tuple contains a single element, in which case it is mandatory.

Structs

A struct is a composite datatype representing a named collection of values. Structs can be generic over constants, in order to wrap arrays of generic size. For more details on generic array sizes, see constant generics. The contained variables can be of any type.

The following code shows an example of how to use structs.

struct Bar<N> {
    field[N] c;
    bool d;
}

struct Foo<P> {
    Bar<P> a;
    bool b;
}

def main() -> Foo<2> {
    Foo<2>[2] mut f = [Foo { a: Bar { c: [0, 0], d: false }, b: true}, Foo { a: Bar {c: [0, 0], d: false}, b: true }];
    f[0].a.c = [42, 43];
    return f[0];
}

Definition

Before a struct data type can be used, it needs to be defined. A struct definition starts with the struct keyword followed by a name. Afterwards, a new-line separated list of variables is declared in curly braces {}. For example:

struct Point {
    field x;
    field y;
}

Note that two struct definitions with the same members still introduce two entirely different types. For example, they cannot be compared with each other.

Declaration and Initialization

Initialization of a variable of a struct type always needs to happen in the same statement as a declaration, unless the struct-typed variable is declared within a function's signature.

The following example shows declaration and initialization of a variable of the Point struct type:

struct Point {
    field x;
    field y;
}

def main() -> Point {
    Point p = Point { x: 1, y: 0 };
    return p;
}

Assignment

The variables within a struct instance, the so called members, can be accessed through the . operator as shown in the following extended example:

struct Point {
    field x;
    field y;
}

def main(field a) -> Point {
    Point mut p = Point { x: 1, y: 0 };
    p.x = a;
    p.y = p.x;
    return p;
}

Type aliases

Type aliases can be defined for any existing type. This can be useful for readability, or to specialize generic types.

Note that type aliases are just syntactic sugar: in the type system, a type and its alias are exactly equivalent. For example, they can be compared.

type MyField = field;

type Rectangle<L, W> = bool[L][W];

type Square<S> = Rectangle<S, S>;

def main() {
    MyField f = 42;
    Rectangle<2, 2> r = [[true; 2]; 2];
    Square<2> s = r;
    return;
}

Operators

The following table lists the precedence and associativity of all operators. Operators are listed top to bottom, in ascending precedence. Operators in the same cell have the same precedence. Operators are binary, unless the syntax is provided.

Operator Description field u8/u16 u32/u64 bool Associativity
**
Power 1     Left
+x
-x
!x
Positive
Negative
Negation


 


 
 
Right
*
/
%
Multiplication
Division
Remainder


 


 
 
 
Left
+
-
Addition
Subtraction
  Left
<<
>>
Left shift
Right shift
  2   Left
& Bitwise AND     Left
| Bitwise OR     Left
^ Bitwise XOR     Left
>=
>
<=
<
Greater or equal
Greater
Lower or equal
Lower
3   Left
!=
==
Not Equal
Equal
Left
&& Boolean AND     Left
|| Boolean OR     Left
c ? x : y

if c { x } else { y }
Conditional expression Right
1

The exponent must be a compile-time constant of type u32

2

The right operand must be a compile time constant of type u32

3

If neither of the operands can be determined to be a compile-time constant, then we have a restriction: for the check a < b, if the field prime p is represented on N bits, |a - b| must fit in N - 2 bits. Failing to respect this condition will lead to a runtime error.

Control Flow

ZoKrates provides a single thread of execution with a few flow constructs.

Function calls

Function calls help make programs clear and modular.

Arguments are passed by value.

Function parameters can be declared as mutable to allow for mutation within the function's body. However, mutable function arguments are still passed by value, so the original value can never be mutated.

def incr(field mut a) -> field {
    a = a + 1;
    return a;
}

def main() {
    field x = 1;
    field res = incr(x);
    assert(x == 1); // x has not changed
    return;
}

Generic parameters, if any, must be compile-time constants. They are inferred by the compiler if that is possible, but can also be provided explicitly.

def foo<N, P>() -> field[P] {
    return [42; P];
}

def main() -> field[2] {
    // `P` is inferred from the declaration of `res`, while `N` is provided explicitly
    field[2] res = foo::<3, _>();
    return res;
}

Conditional expressions

A conditional expression allows you to branch your code depending on a boolean condition.

def main(field x) -> field {
    field y = if x + 2 == 3 { 1 } else { 5 };
    return y;
}

The conditional expression can also be written using a ternary operator:

def main(field x) -> field {
    field y = x + 2 == 3 ? 1 : 5;
    return y;
}

There are two important caveats when it comes to conditional expressions. Before we go into them, let's define two concepts:

  • for an execution of the program, an executed branch is a branch which has to be paid for when executing the program, generating proofs, etc.
  • for an execution of the program, a logically executed branch is a branch which is "chosen" by the condition of an if-expression. This is the more intuitive notion of execution, and there is only one for each if-expression.

Now the two caveats:

  • Both branches are always executed. No short-circuiting happens based on the value of the condition. Therefore, the complexity of a program in terms of the number of constraints it compiles down to is the sum of the cost of all branches.
def cheap(field x) -> field {
    return x + 1;
}

def expensive(field x) -> field {
    return x**1000;
}

def main(field x) -> field {
    return if x == 1 {
        cheap(x)
    } else {
        expensive(x) // both branches executed
    };
}
  • An unsatisfied constraint inside any branch will make the whole execution fail, even if this branch is not logically executed. Also, the compiler itself inserts assertions which can fail. This can lead to unexpected results:
def main(field x) -> field {
    return if x == 0 {
        0
    } else {
        1 / x // executed even for x := 0, which leads to the execution failing
    };
}

The reason for these caveats is that the program is compiled down to an arithmetic circuit. This construct does not support jumping to a branch depending on a condition as you could do on traditional architectures. Instead, all branches are inlined as if they were printed on a circuit board.

For loops

For loops are available with the following syntax:

def main() -> u32 {
    u32 mut res = 0;
    for u32 i in 0..4 {
        for u32 j in i..5 {
            res = res + i;
        }
    }
    return res;
}

The bounds have to be constant at compile-time, therefore they cannot depend on execution inputs. They can depend on generic parameters. The range is half-open, meaning it is bounded inclusively below and exclusively above. The range start..end contains all values within start <= x < end. The range is empty if start >= end.

For loops are only syntactic sugar for repeating a block of statements many times. No condition of the type index < max is being checked at run-time after each iteration. Instead, at compile-time, the index is incremented and the block is executed again. Therefore, assigning to the loop index does not have any influence on the number of iterations performed and is considered bad practice.

Assertions

Any boolean can be asserted to be true using the assert function.

def main() {
    assert(1f + 1f == 2f);
    return;
}

If any assertion fails, execution stops as no valid proof could be generated from it.

Constants

Constants must be globally defined outside all other scopes by using a const keyword. Constants can be set only to a constant expression.

const field PRIME = 31;

def main() -> field {
    return PRIME;
}

The value of a constant can't be changed through reassignment, and it can't be redeclared.

Constants must be explicitly typed. One can reference other constants inside the expression, as long as the referenced constant is already defined.

const field ONE = 1;
const field TWO = ONE + ONE;

def main() -> field {
    return TWO;
}

The naming convention for constants are similar to that of variables. All characters in a constant name are usually in uppercase.

Functions

Functions are declared using the def keyword. A function's signature has to be explicitly provided. Its arguments are type annotated, just like variables, and, if the function returns a value, the return type must be specified after an arrow ->.

A function has to be declared at the top level before it is called.

def foo(field a, field b) -> field {
    return a + b;
}

def main() -> field {
    return foo(1, 2);
}

A function can be generic over any number of values of type u32.

def foo<N>() -> field[N] {
    return [42; N];
}

def main() -> field[2] {
    field[2] res = foo();
    return res;
}

The generic parameters can be provided explicitly, especially when they cannot be inferred.

// a function to sum the N first powers of a field element
def sum_powers<N>(field a) -> field {
    field mut res = 0;
    for u32 i in 0..N {
        res = res + a ** i;
    }
    return res;
}

def main(field a) -> field {
    // call `sum_powers` providing the explicit generic parameter `N := 5`
    return sum_powers::<5>(a);
}

If the return type of a function is the empty tuple (), the return type as well as the return statement can be omitted.

def main() {}

Generics

ZoKrates supports code that is generic over constants of the u32 type. No specific keyword is used: the compiler determines if the generic parameters are indeed constant at compile time. Here's an example of generic code in ZoKrates:

def sum<N>(field[N] a) -> field {
    field mut res = 0;
    for u32 i in 0..N {
        res = res + a[i];
    }
    return res;
}

def main(field[3] a) -> field {
    return sum(a);
}

Imports

You can separate your code into multiple ZoKrates files using import statements to import symbols, ignoring the .zok extension of the imported file.

Import syntax

Symbol selection

The preferred way to import a symbol is by module and name:

from "./path/to/my/module" import MySymbol;

// `MySymbol` is now in scope.

To import multiple symbols with a single import statement, separate the symbols names with commas:

from "./path/to/my/module" import MySymbol, MyOtherSymbol;

Aliasing

The as keyword enables renaming symbols:

from "./path/to/my/module" import MySymbol as MyAlias;

// `MySymbol` is now in scope under the alias MyAlias.

Legacy

The legacy way to import a symbol is by only specifying a module:

import "./path/to/my/module";

In this case, the name of the symbol is assumed to be main and the alias is assumed to be the module's filename so that the above is equivalent to

from "./path/to/my/module" import main as module;

// `main` is now in scope under the alias `module`.

Note that this legacy method is likely to become deprecated, so it is recommended to use the preferred way instead.

Symbols

Three types of symbols can be imported

Functions

Functions are imported by name. If many functions have the same name but different signatures, all of them get imported, and which one to use in a particular call is inferred.

User-defined types

User-defined types declared with the struct keyword are imported by name.

Constants

Constants declared with the const keyword are imported by name.

Relative Imports

You can import a resource in the same folder directly, like this:

from "./mycode" import foo;

Imports up the file-system tree are supported:

from "../../../mycode" import foo;

Absolute Imports

Absolute imports don't start with ./ or ../ in the path and are used to import components from the ZoKrates standard library. Please check the according section for more details.

Comments

Inline comments

Inline (single-line) comments allow narrative on only one line at a time. Single-line comments can begin in any column of a given line and end at a new line or carriage return. Inline comments can be added with double-slashes.

def main() -> field {
    field a = 42; // this is an end of line comment
    // this is a full line comment
    return a;
}

Multi-line comments

Multi-line comments have one or more lines of narrative within a set of comment delimiters. The /* delimiter marks the beginning of the comment, and the */ marks the end. Any content between those delimiters is considered a comment.

/*
    This is a multi-line comment
    written in more than just one line.
*/
def main() -> field {
    return 42;
}

Macros

ZoKrates currently exposes a single macro:

#pragma curve $CURVE

The effect of this macro is to abort compilation if this file is being compiled for a curve different from $CURVE.

Logging

ZoKrates supports a command to log messages during execution in the interpreter.

The values of expressions can be checked and basic string interpolation is supported:

struct Foo {
    field[3] a;
    bool b;
}

def main(Foo x, field y) {
    log("x is {}, y is {}", x, y);
    return;
}

By default, logs get removed during compilation. In order to include them in the compiled program, the --debug flag has to be enabled.

Assembly

ZoKrates allows developers to define constraints through assembly blocks. Assembly blocks are considered unsafe, as safety and correctness of the resulting arithmetic circuit is in the hands of the developer. Usage of assembly is recommended only in optimization efforts for experienced developers to minimize constraint count of an arithmetic circuit.

The usage of assembly blocks in ZoKrates is experimental. In particular, while assembly blocks help minimise constraint count in some cases, they currently can at the same time lead to larger compiler output and slower witness generation.

Writing assembly

All constraints must be enclosed within an asm block. In an assembly block we can do the following:

  1. Assign to a witness variable using <--
  2. Define a constraint using ===

Assigning a value, in general, should be combined with adding a constraint:

def main(field a, field b) -> field {
    field mut c = 0;
    field mut invb = 0;
    asm {
        invb <-- b == 0 ? 0 : 1 / b;
        invb * b === 1;
        c <-- invb * a;
        a === b * c;
    }
    return c;
}

Note that operator <-- is used for unconstrained assignment and can be easily misused. This operator does not generate constraints, which could result in unconstrained variables in the constraint system.

Unconstrained assignment <-- allows assignment to variables with complex types. The type must consist of field elements only (eg. field[3]):

field[3] mut c = [0; 3];
asm {
    c <-- [2, 2, 4];
    c[0] * c[1] === c[2];
}

In some cases we can combine the witness assignment and constraint generation with the <== operator (constrained assignment):

asm {
    c <== 1 - a*b;
}

which is equivalent to:

asm {
    c <-- 1 - a*b;
    c === 1 - a*b;
}

In the case of constrained assignment <==, both sides of the statement have to be of type field.

A constraint can contain arithmetic expressions that are built using multiplication, addition, and other variables or field values. Only quadratic expressions are allowed to be included in constraints. Non-quadratic expressions or usage of other arithmetic operators like division or power are not allowed as constraints, but can be used in the witness assignment expression.

The following code is not allowed:

asm {
    d === a*b*c;
}

as the constraint d === a*b*c is not quadratic.

In some cases, ZoKrates will apply minor transformations on the defined constraints in order to meet the correct format:

asm {
    x * (x - 1) === 0;
}

will be transformed to:

asm {
    x === x * x;
}

Type casting

Assembly is a low-level part of the compiler which does not have type safety. In some cases we might want to do zero-cost conversions between field and bool type.

field_to_bool_unsafe

This call is unsafe because it is the responsibility of the user to constrain the field input:

from "EMBED" import field_to_bool_unsafe;

def main(field x) -> bool {
    // we constrain `x` to be 0 or 1
    asm {
        x * (x - 1) === 0;
    }
    // we can convert `x` to `bool` afterwards, as we constrained it properly
    // if we failed to constrain `x` to `0` or `1`, the call to `field_to_bool_unsafe` introduces undefined behavior
    // `field_to_bool_unsafe` call does not produce any extra constraints
    bool out = field_to_bool_unsafe(x);
    return out;
}

ZoKrates Reference

The reference covers the details of the ZoKrates toolbox beyond the ZoKrates language.

Command Line Tool

ZoKrates provides a command line interface. You can see an overview of the available subcommands by running

zokrates

You can get help about a particular subcommand with --help, for example:

zokrates compile --help

Performing a trusted setup using a multi-party computation protocol (MPC)

The zk-SNARK schemes supported by ZoKrates require a trusted setup. This procedure must be run to generate the proving and verification keys. This procedure generates some data often referred to as "toxic waste" which can be used to create fake proofs which will be accepted by the verifier. The entity running the trusted setup is trusted to delete this toxic waste. Using an MPC protocol, we can run the trusted setup in a decentralized way, so that this responsibility is shared among all participants of the setup. If at least one participant is honest and deletes their part of the toxic waste, then no fake proofs can be created by anyone. This section of the book describes the steps to perform a trusted setup for the Groth16 scheme.

Pre-requisites

The trusted setup is done in two steps. The first step, also known as "phase 1", does not depend on the program and is called Powers of Tau. The second step is called "phase 2" and is circuit-specific, so it should be done separately for each different program. The Ethereum community runs a phase 1 setup called Perpetual Powers of Tau, whose output we can use. Therefore, we only need to run phase 2 of the setup.

Compiling a circuit

We will start this tutorial by using ZoKrates to compile a basic program. First, we create a new file named program.zok with the following content:

def main(private field a, private field b) -> field {
    return a * b;
}

We compile the program using the compile command.

zokrates compile -i program.zok -o circuit

Initializing a phase 2 ceremony

We then initialize a phase 2 ceremony with the following command:

$ zokrates mpc init -i circuit -o mpc.params -r ./phase1radix2m2

Initializing MPC...
Parameters written to `mpc.params`

Using the -r flag, we pass a path to the file which contains the parameters for our circuit with depth 2^n (phase1radix2m{n}). The parameters for various circuit depths can be computed using the phase2-bn254 utility by picking the latest response from the Perpetual Powers of Tau and following the instructions in the mentioned repositories.

Making a contribution

In this example, we will conduct a ceremony that has 3 participants: Alice, Bob, and Charlie. Participants will run the contributions in sequential order, managed by the coordinator (us).

Firstly, our initial mpc.params file is given to Alice who runs the following command:

$ zokrates mpc contribute -i mpc.params -o alice.params -e "alice 1"

Contributing to `mpc.params`...
The BLAKE2b hash of your contribution is:

        4ebf1359 416fbc42 31af6476 9173cb33 
        32b8c2f9 475d143a 25634a5c e461eb67 
        5f7738b1 6478a020 7ec9d365 9170bca6 
        154b31df d307b78e ca0c025f 59c5a7fb

Your contribution has been written to `alice.params`

Alice must give some randomness to the contribution, which is done by the -e flag.

Examples of entropy sources:

  • /dev/urandom from one or more devices
  • The most recent block hash
  • Randomly mashing keys on the keyboard

Secondly, the output file alice.params is sent to Bob who runs his contribution:

$ zokrates mpc contribute -i alice.params -o bob.params -e "bob 2"

Contributing to `alice.params`...
The BLAKE2b hash of your contribution is:

        1a4e0d17 449b00ec f31d2072 59bc173c
        f30f6dbd 78c81921 869091a8 e40f454e
        8c8d72e8 395bf044 cd777842 b6ab1d88
        9e24cf7f 7d88b473 2190fb0c 730fb6fc

Your contribution has been written to `bob.params`

Thirdly, with the same procedure as above, Charlie makes his contribution on top of Bob's:

$ zokrates mpc contribute -i bob.params -o charlie.params -e "charlie 3"

Contributing to `bob.params`...
The BLAKE2b hash of your contribution is:

        46dc6c01 ec778382 93b333b2 116a4bfb
        a9aca5dd eb6945f1 cbe07cda 6ffb3ffd 
        cf4e4736 62fe2339 166d5b87 db392ca6
        d2e87e36 92cc8f0e e618298f c3f7caf1

Your contribution has been written to `charlie.params`

Applying a random beacon

To finalize the ceremony, we can apply a random beacon to get the final parameters:

$ zokrates mpc beacon -i charlie.params -o final.params -h b94d27b9934d3e08a52e52d7da7dabfac484efe37a5380ee9088f7ace2efcde9 -n 10

Creating a beacon RNG
0: b94d27b9934d3e08a52e52d7da7dabfac484efe37a5380ee9088f7ace2efcde9
1: bc62d4b80d9e36da29c16c5d4d9f11731f36052c72401a76c23c0fb5a9b74423
2: 76dfcb21a877aaeba06b3269d08dc2ed1d38c62ffec132800b46e94b14f72938
...removed for brevity
1022: dd842dc43d9ac5c6dff74cca18405123761d17edd36724b092ef57c237b31291
1023: a11c8a03c22e9c31c037aa0085c061ba8dd19a3f599314570702eeef1baacd79
Final result of beacon: ef8faec4fc31faf341f368084b82d267d380992e905c923a179e0717ce39708d

Contributing to `charlie.params`...
The BLAKE2b hash of your contribution is: 

        83d67a6f 935fc4d0 5733ebed d43f2074 
        5425b105 9a32a315 a790668a f5a1f021 
        66f840e2 e6a5d441 38593163 5b86df09 
        a00f352e 2ad2a88b ede07886 2134b889

Your contribution has been written to `final.params`

The random beacon is the 2^n iteration of SHA256 over the hash evaluated on some high entropy and publicly available data. Possible sources of data could be:

  • The closing value of the stock market on a certain date
  • The output of a selected set of national lotteries
  • The value of a block at a particular height in one or more blockchains
  • League of Entropy (drand)

Verifying contributions

At any point in the ceremony we can verify contributions by running the following command:

$ zokrates mpc verify -i final.params -c circuit -r ./phase1radix2m2

Verifying contributions...

Transcript contains 4 contributions:
0: 4ebf1359416fbc4231af64769173cb3332b8c2f9475d143a25634a5ce461eb675f7738b16478a0207ec9d3659170bca6154b31dfd307b78eca0c025f59c5a7fb
1: 1a4e0d17449b00ecf31d207259bc173cf30f6dbd78c81921869091a8e40f454e8c8d72e8395bf044cd777842b6ab1d889e24cf7f7d88b4732190fb0c730fb6fc
2: 46dc6c01ec77838293b333b2116a4bfba9aca5ddeb6945f1cbe07cda6ffb3ffdcf4e473662fe2339166d5b87db392ca6d2e87e3692cc8f0ee618298fc3f7caf1
3: 83d67a6f935fc4d05733ebedd43f20745425b1059a32a315a790668af5a1f02166f840e2e6a5d441385931635b86df09a00f352e2ad2a88bede078862134b889

Contributions verified

Exporting keys

Once the ceremony is finalized, we can export the keys and use them to generate proofs and verify them.

# export keys from final parameters (proving and verification key)
zokrates mpc export -i final.params

# use the keys to generate proofs and verify
zokrates compute-witness -i circuit -a 123456789 987654321 --verbose
zokrates generate-proof -i circuit -b bellman
zokrates verify -b bellman

Conclusion

The secure generation of parameters for zk-SNARKs is a crucial step in the trustworthiness of the resulting proof system. The security of the ceremony relies entirely on the fact that at least one participant needs to securely delete their "toxic waste" for the resulting parameters to be generated honestly. Opening the ceremony to a large number of participants reduces the probability that the resulting parameters are dishonest. Once the ceremony is finalized, we can generate a verifier smart contract by using the keys we obtained through the trusted setup ceremony. At this point, we can safely deploy the contract and verify proofs on-chain.

Standard library

ZoKrates comes with a number of reusable components in the form of a Standard Library. In order to import it as described in the imports section, the $ZOKRATES_STDLIB environment variable must be set to the stdlib folder.

The full ZoKrates Standard Library can be found here.

Hashes

SHA256

We provide an implementation of the SHA256 function from the SHA-2 family of secure hash functions 1. The hash functions of the SHA-2 family are considered to be pseudorandom.

SHA256 is available in Ethereum as a pre-compiled contract and thus a hash function that is cheap to evaluate in the EVM. However, the implementation inside a circuit is comparatively expensive, as it is defined for binary in- and outputs and heavily relies on bit manipulation.

Pedersen Hashes

The pedersen hash function is inspired by a commitment scheme published by Pedersen 2. This hash function’s security is based on the discrete logarithm problem. Pedersen-hashes cannot be assumed to be pseudorandom and should therefore not be used where a hash function serves as a random oracle.

In the EVM, operations on the BabyJubJub curve are not natively supported. Therefore, Pedersen hashes are expensive to evaluate on-chain and should be avoided.

By definition, the Pedersen hash function has a fixed-length binary input and outputs a group element, i.e., a point on the BabyJubJub elliptic curve in our case.

MiMC

The MiMC hash function was designed by using the MiMC-Feistel permutation 3 over a prime field in a sponge construction 4 to arrive at a secure and efficiently provable hash function. The construction is based on established hash function design principles from symmetric cryptography but is still novel and should thus be used cautiously. MiMC hashes are considered to be pseudorandom.

Due to its native use of prime field arithmetics, MiMC hash functions are efficient in circuits. At the same time, they can be evaluated by the EVM with comparatively little overhead.

The MiMC hash function maps from field elements to field elements; applying the function to its output again does not introduce overhead for packing/unpacking.

Elliptic curve cryptography

Thanks to the existence of BabyJubJub, an efficient elliptic curve embedded in ALT_BN128, we provide tools to perform elliptic curve operations such as:

  • Point operations
  • Proving knowledge of a private EdDSA key
  • Proving validity of an EdDSA signature

Check out this python repository for tooling, for example to generate EdDSA signatures to then check in a SNARK.

Utils

Packing / Unpacking

As some operations require their input to be provided in the form of bits, we provide tools to convert back and forth between field elements and their bit representations.

Casts

Helpers to convert between types representing binary data.

Multiplexer

Optimised tools to branch inside circuits.

1

P. FIPS. “180-4 FEDERAL INFORMATION PROCESSING STANDARDS PUBLICA- TION”. In: Secure Hash Standard (SHS), National Institute of Standards and Technology (2012).

2

T. P. Pedersen. “Non-interactive and information-theoretic secure verifiable secret shar- ing”. In: Annual International Cryptology Conference. Springer. 1991, pp. 129–140.

3

M. Albrecht, L. Grassi, C. Rechberger, A. Roy, and T. Tiessen. “MiMC: Efficient en- cryption and cryptographic hashing with minimal multiplicative complexity”. In: In- ternational Conference on the Theory and Application of Cryptology and Information Security. Springer. 2016, pp. 191–219.

4

G. Bertoni, J. Daemen, M. Peeters, and G. Van Assche. “On the indifferentiability of the sponge construction”. In: Annual International Conference on the Theory and Applica- tions of Cryptographic Techniques. Springer. 2008, pp. 181–197.

Proving schemes

Curves

Proving schemes supported by ZoKrates require a pairing-friendly elliptic curve. The options are the following:

Curve CLI flag Supported by Ethereum
ALT_BN128 --curve bn128 Yes (EIP-196, EIP-197)
BLS12_381 --curve bls12_381 No (EIP-2537)
BLS12_377 --curve bls12_377 No (EIP-2539)
BW6_761 --curve bw6_761 No (EIP-3026)

Default: ALT_BN128

When not using the default, the CLI flag has to be provided for the following commands:

  • universal-setup
  • compile
  • export-verifier
  • verify

Schemes

ZoKrates supports different proving schemes. We identify the schemes by the reference to the paper that introduced them. Currently the options available are:

Scheme CLI flag Curves Universal
G16 --proving-scheme g16 ALTBN_128, BLS12_381 No
GM17 --proving-scheme gm17 ALTBN_128, BLS12_381, BLS12_377, BW6_761 No
Marlin --proving-scheme marlin ALTBN_128, BLS12_381, BLS12_377, BW6_761 Yes

All schemes have a circuit-specific setup phase called setup. Universal schemes also feature a preliminary, circuit-agnostic step called universal-setup. The advantage of universal schemes is that only the universal-setup step requires trust, so that it can be run a single time and reused trustlessly for many programs.

Default: G16, except for universal-setup for which the default is Marlin

When not using the default, the CLI flag has to be provided for the following commands:

  • universal-setup
  • setup
  • export-verifier
  • generate-proof
  • verify

Supporting backends

ZoKrates supports multiple backends. The options are the following:

Backend CLI flag Proving schemes Curves
Bellman --backend bellman G16 ALTBN_128, BLS12_381
Ark --backend ark G16, GM17, MARLIN ALTBN_128, BLS12_381, BLS12_377, BW6_761

Default: ark

When not using the default, the CLI flag has to be provided for the following commands:

  • universal-setup
  • setup
  • generate-proof
  • verify

G16 malleability

When using G16, developers should pay attention to the fact that an attacker, seeing a valid proof, can very easily generate a different but still valid proof. Therefore, depending on the use case, making sure on chain that the same proof cannot be submitted twice may not be enough to guarantee that attackers cannot replay proofs. Mechanisms to solve this issue include:

  • signed proofs
  • nullifiers
  • usage of an ethereum address as a public input to the program
  • usage of non-malleable schemes such as GM17

Verification

Passed to the verifier contract, a proof can be checked. For example, using web3, a call would look like the following:

const accounts = await web3.eth.getAccounts();
const address = '0x456...'; // verifier contract address

let verifier = new web3.eth.Contract(abi, address, {
    from: accounts[0], // default from address
    gasPrice: '20000000000000'; // default gas price in wei
});

let result = await verifier.methods
    .verifyTx(proof.proof, proof.inputs)
    .call({ from: accounts[0] });

ZIR

ZIR is the intermediate representation ZoKrates uses to represent programs. It is close to R1CS but still encapsulates witness generation.

Note that ZIR is still in development and can change without notice.

Serialisation

ZIR programs are serialised with the following format:

Fields Length in bytes Description
Magic 4 ZOK in ASCII, right-padded by 0: 0x5a4f4b00
Version 4 This format's version, as a big endian number: 0x00000001
Field size 4 The first 4 bytes of sha256(FIELD_MODULUS): 0xb4f7b5bd for bn128 for example
Program n The bincode-encoded program

Display

When generating R1CS constraints, very large numbers are often used, which can make reading ZIR hard for humans. To mitigate this, ZIR applies an isomorphism when displaying field elements: they are shown as members of the interval [- (p - 1)/2, (p - 1)/2]. In other words, the following mapping is used:

  • elements in [0, (p - 1)/2] map to themselves
  • elements in [(p + 1)/2, p - 1] map to themselves minus p

Therefore, instead of writing p - 1 as:

21888242871839275222246405745257275088548364400416034343698204186575808495616

... in ZIR, we simply write:

-1

ZoKrates ABI

In order to interact programmatically with compiled ZoKrates programs, ZoKrates supports passing arguments using an ABI.

To illustrate this, we'll use the following example program:

struct Bar {
    field a;
}

struct Foo {
    u8 a;
    Bar b;
}

def main(Foo foo, bool[2] bar, field num) -> field {
    return 42;
}

ABI specification

When compiling a program, an ABI specification is generated and describes the interface of the program.

In this example, the ABI specification is:

{
   "inputs":[
      {
         "name":"foo",
         "public":true,
         "type":"struct",
         "components":{
            "name":"Foo",
            "members":[
               {
                  "name":"a",
                  "type":"u8"
               },
               {
                  "name":"b",
                  "type":"struct",
                  "components":{
                     "name":"Bar",
                     "members":[
                        {
                           "name":"a",
                           "type":"field"
                        }
                     ]
                  }
               }
            ]
         }
      },
      {
         "name":"bar",
         "public":true,
         "type":"array",
         "components":{
            "size":2,
            "type":"bool"
         }
      },
      {
         "name":"num",
         "public":true,
         "type":"field"
      }
   ],
   "output": {
     "type":"field"
   }
}

ABI input format

When executing a program, arguments can be passed as a JSON object of the following form:

[
   {
      "a":"0x2a",
      "b":{
         "a":"42"
      }
   },
   [
      true,
      false
   ],
   "42"
]

Note the following:

  • Field elements are passed as JSON strings in order to support arbitrary large numbers
  • Unsigned integers are passed as JSON strings containing their hexadecimal representation
  • Structs are passed as JSON objects, ignoring the struct name

zokrates.js

JavaScript bindings for ZoKrates.

npm install zokrates-js

Importing

ES modules

import { initialize } from "zokrates-js";

CommonJS

let { initialize } = await import("zokrates-js");

CDN

<script src="https://unpkg.com/zokrates-js@latest/umd.min.js"></script>
<script>
  zokrates.initialize().then((zokratesProvider) => {
    /* ... */
  });
</script>

Example

initialize().then((zokratesProvider) => {
  const source = "def main(private field a) -> field { return a * a; }";

  // compilation
  const artifacts = zokratesProvider.compile(source);

  // computation
  const { witness, output } = zokratesProvider.computeWitness(artifacts, ["2"]);

  // run setup
  const keypair = zokratesProvider.setup(artifacts.program);

  // generate proof
  const proof = zokratesProvider.generateProof(
    artifacts.program,
    witness,
    keypair.pk
  );

  // export solidity verifier
  const verifier = zokratesProvider.exportSolidityVerifier(keypair.vk);

  // or verify off-chain
  const isVerified = zokratesProvider.verify(keypair.vk, proof);
});

API

initialize()

Returns an initialized ZoKratesProvider as a promise.

initialize().then((zokratesProvider) => {
  // call api functions here
});

Returns: Promise<ZoKratesProvider>

withOptions(options)

Returns a ZoKratesProvider configured with given options.

initialize().then((defaultProvider) => {
  let zokratesProvider = defaultProvider.withOptions({
    backend: "ark",
    curve: "bls12_381",
    scheme: "g16",
  });
  // ...
});

Options:

  • backend - Backend (options: ark | bellman, default: ark)
  • curve - Elliptic curve (options: bn128 | bls12_381 | bls12_377 | bw6_761, default: bn128)
  • scheme - Proving scheme (options: g16 | gm17 | marlin, default: g16)

Returns: ZoKratesProvider

compile(source[, options])

Compiles source code into ZoKrates internal representation of arithmetic circuits.

Parameters:

  • source - Source code to compile
  • options - Compilation options

Returns: CompilationArtifacts

Examples:

Compilation:

const artifacts = zokratesProvider.compile("def main() { return; }");

Compilation with custom options:

const source = "...";
const options = {
  location: "main.zok", // location of the root module
  resolveCallback: (currentLocation, importLocation) => {
    console.log(currentLocation + " is importing " + importLocation);
    return {
      source: "def main() { return; }",
      location: importLocation,
    };
  },
};
const artifacts = zokratesProvider.compile(source, options);

Note: The resolveCallback function is used to resolve dependencies. This callback receives the current module location and the import location of the module which is being imported. The callback must synchronously return either an error, null or a valid ResolverResult object like shown in the example above. A simple file system resolver in a node environment can be implemented as follows:

import fs from "fs";
import path from "path";

const fileSystemResolver = (from, to) => {
  const location = path.resolve(path.dirname(path.resolve(from)), to);
  const source = fs.readFileSync(location).toString();
  return { source, location };
};
computeWitness(artifacts, args[, options])

Computes a valid assignment of the variables, which include the results of the computation.

Parameters:

  • artifacts - Compilation artifacts
  • args - Array of arguments (eg. ["1", "2", true])
  • options - Computation options

Returns: ComputationResult

Example:

const code = "def main(private field a) -> field { return a * a; }";
const artifacts = zokratesProvider.compile(code);

const { witness, output } = zokratesProvider.computeWitness(artifacts, ["2"]);

console.log(witness); // Resulting witness which can be used to generate a proof
console.log(output); // Computation output: "4"
setup(program[, entropy])

Generates a trusted setup for the compiled program.

Parameters:

  • program - Compiled program
  • entropy - User provided randomness (optional)

Returns: SetupKeypair

universalSetup(size[, entropy])

Performs the universal phase of a trusted setup. Only available for the marlin scheme.

Parameters:

  • size - Size of the trusted setup passed as an exponent. For example, 8 for 2**8.
  • entropy - User provided randomness (optional)

Returns: Uint8Array

setupWithSrs(srs, program)

Generates a trusted setup with universal public parameters for the compiled program. Only available for marlin scheme.

Parameters:

  • srs - Universal public parameters from the universal setup phase
  • program - Compiled program

Returns: SetupKeypair

generateProof(program, witness, provingKey[, entropy])

Generates a proof for a computation of the compiled program.

Parameters:

  • program - Compiled program
  • witness - Witness (valid assignment of the variables) from the computation result
  • provingKey - Proving key from the setup keypair
  • entropy - User provided randomness (optional)

Returns: Proof

verify(verificationKey, proof)

Verifies the generated proof.

Parameters:

  • verificationKey - Verification key from the setup keypair
  • proof - Generated proof

Returns: boolean

exportSolidityVerifier(verificationKey)

Generates a Solidity contract which contains the generated verification key and a public function to verify proofs of computation of the compiled program.

Parameters:

  • verificationKey - Verification key from the setup keypair

Returns: string

utils.formatProof(proof)

Formats the proof into an array of field elements that are compatible as input to the generated solidity contract

Parameters:

  • proof - Generated proof

Returns: array

Experimental features

ZoKrates supports some experimental features.

Nova

ZoKrates supports the nova proof system using the bellperson backend. Nova is accessed with the subcommand nova.

API

To use Nova, programs must have the following signature, for any types State and StepInput:

def main(public State state, private StepInput step_input) -> State

Then, using Nova lets the user prove many steps of this program, given an initial state.

For example:

def main(public field sum, private field element) -> field {
    return sum + element;
}

We compile this program using the Pallas curve:

zokrates compile -i sum.zok --curve pallas

Then we can prove three iterations as follows:

echo "\"0\"" > init.json
echo "[\"1\", \"7\", \"42\"]" > steps.json
zokrates nova prove

The proof created at proof.json proves the statement 0 + 1 + 7 + 42 == 50.

We can extend it by running more steps, for example with the same intermediate inputs:

zokrates nova prove --continue

The proof updated at proof.json proves the statement 50 + (0 + 1 + 7 + 42) == 100.

Once we're done, we compress the proof to a compressed snark:

zokrates nova compress

Finally, we can verify this proof

zokrates nova verify

Limitations

  • The step circuit must be compiled with --curve pallas
  • The resulting recursive proof cannot currently be verified on the EVM

ZoKrates Examples

This section covers examples of using the ZoKrates programming language.

Tutorial: A SNARK Powered RNG

Prerequisites

Make sure you have followed the instructions in the Getting Started chapter and are able to run the "Hello World" example described there.

Description of the problem

Alice and Bob want to bet on the result of a series of coin tosses. To do so, they need to generate a series of random bits. They proceed as follows:

  1. Each of them commits to a 512 bit value. Let’s call this value the preimage. They publish the hash of the preimage.
  2. Each time they need a new random value, they reveal one bit from their preimage, and agree that the new random value is the result of XORing these two bits, so that neither of them can control the output.

Note that we are making a few assumptions here:

  1. They make sure they do not use all 512 bits of their preimage, as the more they reveal, the easier it gets for the other to brute-force their preimage.
  2. They need a way to be convinced that the bit the other revealed is indeed part of their preimage.

In this tutorial you learn how to use Zokrates and zero knowledge proofs to reveal a single bit from the preimage of a hash value.

Commit to a preimage

The first step is for Alice and Bob to each come up with a preimage value and calculate the hash to commit to it. There are many ways to calculate a hash, but here we use Zokrates.

Create this file under the name get_hash.zok:

import "hashes/sha256/512bit" as sha256;

def main(u32[16] hashMe) -> u32[8] {
    u32[8] h = sha256(hashMe[0..8], hashMe[8..16]);
    return h;
}

Compile the program to a form that is usable for zero knowledge proofs. This command writes the binary to get_hash. You can see a textual representation, somewhat analogous to assembler coming from a compiler, at get_hash.ztf created by the inspect command.

zokrates compile -i get_hash.zok -o get_hash && zokrates inspect -i get_hash

The input to the Zokrates program is sixteen 32 bit values, each in decimal. specify those values to get a hash. For example, to calculate the hash of 0x00000000000000010000000200000003000000040000000500000006... use this command:

zokrates compute-witness --verbose -i get_hash -a 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15

The result is:

Computing witness...

Witness:

["3592665057","2164530888","1223339564","3041196771","2006723467","2963045520","3851824201","3453903005"]

Pick your own value and store it somewhere.

Detailed explanation

This line imports a Zokrates function from the standard library. You can see the specific function we are importing here. It will be called sha256.

import "hashes/sha256/512bit" as sha256;

This is the main function. The input (u32[16]) is an array of sixteen values, each an unsigned 32-bit integer (a number between (0) and (2^{32} - 1)). As you have seen above, you specify these numbers using the -a command line parameter. The total number of input bits is 32 × 16 = 512.

The output is u32[8], a 32 × 8 = 256 bit value.

def main(u32[16] hashMe) -> u32[8] {

This line does several things. First, u32[8] h defines a variable called h, whose type is an array of eight 32-bit unsigned integers. This variable is initialized using sha256, the function we imported from the standard library. The sha256 function expects to get two arrays of eight values each, so we use a slice .. to divide hashMe into two arrays.

    u32[8] h = sha256(hashMe[0..8], hashMe[8..16]);

Finally, return h to the caller to display the hash.

    return h;

Reveal a single bit

The next step is to reveal a single bit.

Use this program, reveal_bit.zok:

import "hashes/sha256/512bit" as sha256;
import "utils/casts/u32_to_bits" as u32_to_bits;

// Reveal a bit from a 512 bit value, and return it with the corresponding hash
// for that value.
//
// WARNING, once enough bits have been revealed it is possible to brute force
// the remaining preimage bits.
def main(private u32[16] preimage, u32 bitNum) -> (u32[8], bool) {
    // Convert the preimage to bits
    bool[512] mut preimageBits = [false; 512];
    for u32 i in 0..16 {
        bool[32] val = u32_to_bits(preimage[i]);
        for u32 bit in 0..32 {
            preimageBits[i*32 + bit] = val[bit];
        }
    }
    return (sha256(preimage[0..8], preimage[8..16]), preimageBits[bitNum]);
}

Compile and run as you did the previous program:

zokrates compile -i reveal_bit.zok -o reveal_bit
zokrates compute-witness --verbose -i reveal_bit -a 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 510

The output should be similar to:

Witness:

["3592665057","2164530888","1223339564","3041196771","2006723467","2963045520","3851824201","3453903005","1"]

Detailed explanation

This line imports a function that converts a u32 value to an array of 32 booleans. There are cast functions to convert u8s, u16s, and u32s to boolean arrays and back again, you can see them here.

import "utils/casts/u32_to_bits" as u32_to_bits;

The preimage is declared private so it won't be revealed by the zero knowledge proof.

A Zokrates function can return multiple values. In this case, it returns the hash and a boolean which is the value of the bit being revealed.

    // Convert the preimage to bits

To find the value of the bit being revealed, we convert the entire preimage into bits and access it at the index bitNum. The first line defines an array of 512 boolean values (bool[512]) called preimageBits. It is initialized to an array of 512 false values. The syntax [<value>; <number>] initializes the an array of <number> copies of <value>. It is necessary to include it here because a Zokrates variable must be initialized when it is declared.

    bool[512] mut preimageBits = [false; 512];
    for u32 i in 0..16 {

This is a for loop. For loops have to have an index of type u32, and their bounds need to be known at compile time. In this case, we go over each of the sixteen 32 bit words.

        bool[32] val = u32_to_bits(preimage[i]);

The function we imported, u32_to_bits, converts a u32 value to an array of bits.

        for u32 bit in 0..32 {

The inner loop copies the bits from val to preimageBits, the bit array for the preimage.

            preimageBits[i*32 + bit] = val[bit];
        }
    }
    return (sha256(preimage[0..8], preimage[8..16]), preimageBits[bitNum]);

To return multiple values, separate them by commas.


Actually using zero knowledge proofs

The reveal_bit.zok program reveals a bit from the preimage, but who runs it?

  1. If Alice runs the program, she can feed it her secret preimage and receive the correct result. However, when she sends the output there is no reason for Bob to trust that she is providing the correct output.
  2. If Bob runs the program, he does not have Alice's secret preimage. If Alice discloses her secret preimage, Bob can know the value of all the bits.

Therefore, we need to have Alice run the program and produce the output, but produce it in such a way Bob will know it is the correct output. This is what Zero Knowledge Proofs give us.

Set up the environment

Create two separate directories, alice and bob. You will perform the actions of Alice in the alice directory, and the actions of Bob in the bob directory.

Bob's setup stage

Compile reveal_bit.zok and create the proving and verification keys.

zokrates compile -i reveal_bit.zok -o reveal_bit
zokrates setup -i reveal_bit

Copy the file proving.key to Alice's directory.

Alice reveals a bit

Alice should compile reveal_bit.zok independently to make sure it doesn't disclose information she wants to keep secret.

zokrates compile -i reveal_bit.zok -o reveal_bit

Next, Alice creates the witness file with the values of all the parameters in the program. Using this witness, Bob's proving.key, and the compiled program she generates the actual proof.

zokrates compute-witness --verbose -i reveal_bit -a 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 510
zokrates generate-proof -i reveal_bit

The proof is created in the file proof.json. Copy this file to Bob's directory.

Bob accepts the proof

Finally, Bob verifies the proof:

zokrates verify

As a sanity check, modify any of the values in proof.json and see that the verification fails.

Connecting to Ethereum

So far, Alice and Bob calculated the random bit between themselves. However, it is often useful to have the values published on the blockchain. To do this, Bob creates a Solidity program:

zokrates export-verifier

The Solidity program is called verifier.sol.

Here are the instructions to use this program when using Truffle and Ganache. We'll assume they are installed, and the Ganache blockchain is running.

  1. Create a new project with truffle init and copy verify.sol to the subdirectory contracts.

  2. Identify the version of Solidity used by verifier.sol:

    grep solidity contracts/verifier.sol
    
  3. Edit truffle-config.js:

    • Change module.exports.compilers.solc.version to the version required by verifier.sol.
    • Uncomment modules.exports.networks.development. Make sure you delete the comma after the definition.
  4. Compile the contract.

    truffle compile
    
  5. Start the Truffle console. The rest of this procedure is done in the JavaScript prompt inside that console.

    truffle console
    
  6. Deploy the Verifier contract.

    contract = await Verifier.new()
    
  7. Read the content of proof.json.

    proof = JSON.parse(fs.readFileSync("path/to/your/proof.json"))
    
  8. Verify the proof. Check that you get the result true.

    await contract.verifyTx(proof.proof.a, proof.proof.b, proof.proof.c, proof.inputs)
    
  9. Pretend to be Alice and try to cheat. Create cheat which flips the result bit.

    cheat = [...proof.inputs]
    cheat[cheat.length-1] = cheat[cheat.length-1].replace(/[01]$/, cheat[cheat.length-1][65] == '1' ? '0': '1')
    
  10. As Bob, try to verify a cheating proof, and check that it fails.

      await contract.verifyTx(proof.proof.a, proof.proof.b, proof.proof.c, cheat)
    

Conclusion

At this point you should know how to use Zokrates to create zero knowledge proofs and verify them from the command line. You should also be able to publish a verifier to a blockchain, generate proofs from the command line, and submit them using JavaScript.


Original version of this tutorial by Ori Pomerantz qbzzt1@gmail.com

Tutorial: Proving knowledge of a hash preimage

Let's jump into ZoKrates by working through a hands-on project together!

We'll implement an operation that's very typical in blockchain use-cases: proving knowledge of the preimage for a given hash digest. In particular, we'll show how ZoKrates and the Ethereum blockchain can be used to allow a prover, let's call her Peggy, to demonstrate beyond any reasonable doubt to a verifier, let's call him Victor, that she knows a hash preimage for a digest chosen by Victor, without revealing what the preimage is.

Pre-requisites

Make sure you have followed the instructions in the Getting Started chapter and are able to run the "Hello World" example described there.

Computing a Hash using ZoKrates

We will start this tutorial by using ZoKrates to compute the hash for an arbitrarily chosen preimage, being the number 5 in this example.

First, we create a new file named hashexample.zok with the following content:

import "hashes/sha256/512bitPacked" as sha256packed;

def main(private field a, private field b, private field c, private field d) -> field[2] {
    field[2] h = sha256packed([a, b, c, d]);
    return h;
}

The first line imports the sha256packed function from the ZoKrates standard library.

sha256packed is a SHA256 implementation that is optimized for the use in the ZoKrates DSL. Here is how it works: We want to pass 512 bits of input to SHA256. However, a field value can only hold 254 bits due to the size of the underlying prime field we are using. As a consequence, we use four field elements, each one encoding 128 bits, to represent our input. The four elements are then concatenated in ZoKrates and passed to SHA256. Given that the resulting hash is 256 bit long, we split it in two and return each value as a 128 bit number.

In case you are interested in an example that is fully compliant with existing SHA256 implementations in Python or Solidity, you can have a look at this blog post.

Our code is really just using the sha256packed, returning the computed hash.

Having our problem described in ZoKrates' DSL, we can now continue using ZoKrates for the rest of our workflow.

First, we compile the program into an arithmetic circuit using the compile command.

zokrates compile -i hashexample.zok

As a next step we can create a witness file using the following command:

zokrates compute-witness -a 0 0 0 5 --verbose

Using the flag -a we pass arguments to the program. Recall that our goal is to compute the hash for the number 5. Consequently we set a, b and c to 0 and d to 5.

Still here? Great! At this point we can check the return values. We should see the following output:

Witness: 
["263561599766550617289250058199814760685","65303172752238645975888084098459749904"]

By concatenating the outputs as 128 bit numbers, we arrive at the following value as the hash for our selected pre-image : 0xc6481e22c5ff4164af680b8cfaa5e8ed3120eeff89c4f307c4a6faaae059ce10

Prove knowledge of pre-image

For now, we have seen that we can compute a hash using ZoKrates.

Let's recall our goal: Peggy wants to prove that she knows a preimage for a digest chosen by Victor, without revealing what the preimage is. Without loss of generality, let's now assume that Victor chooses the digest to be the one we found in our example above.

To make it work, the two parties have to follow their roles in the protocol:

First, Victor has to specify what hash he is interested in. Therefore, we have to adjust the zkSNARK circuit, compiled by ZoKrates, such that in addition to computing the digest, it also validates it against the digest of interest, provided by Victor. This leads to the following update for hashexample.zok:

import "hashes/sha256/512bitPacked" as sha256packed;

def main(private field a, private field b, private field c, private field d) {
    field[2] h = sha256packed([a, b, c, d]);
    assert(h[0] == 263561599766550617289250058199814760685);
    assert(h[1] == 65303172752238645975888084098459749904);
    return;
}

Note that we now compare the result of sha256packed with the hard-coded correct solution defined by Victor. The lines which we added are treated as assertions: the verifier will not accept a proof where these constraints were not satisfied. Clearly, this program only returns 1 if all of the computed bits are equal.

So, having defined the program, Victor is now ready to compile the code:

zokrates compile -i hashexample.zok

Based on that Victor can run the setup phase and export a verifier smart contract as a Solidity file:

zokrates setup
zokrates export-verifier

setup creates a verification.key file and a proving.key file. Victor gives the proving key to Peggy.

export-verifier creates a verifier.sol contract that contains our verification key and a function verifyTx. Victor deploys this smart contract to the Ethereum network.

Peggy provides the correct pre-image as an argument to the program.

zokrates compute-witness -a 0 0 0 5

Finally, Peggy can run the command to construct the proof:

zokrates generate-proof

As the inputs were declared as private in the program, they do not appear in the proof thanks to the zero-knowledge property of the protocol.

ZoKrates creates a file, proof.json, consisting of the three elliptic curve points that make up the zkSNARKs proof. The verifyTx function in the smart contract deployed by Victor accepts these three values, along with an array of public inputs. The array of public inputs consists of:

  • any public inputs to the main function, declared without the private keyword
  • the return values of the ZoKrates function

In the example we're considering, all inputs are private and there is a single return value of 1, hence Peggy has to define her public input array as follows: [1].

Peggy can then submit her proof by calling verifyTx.

Victor monitors the verification smart contract for the return value of Peggy's transaction. As soon as he observes a transaction from Peggy's public address with a true return value, he can be sure that she has a valid pre-image for the hash he set in the smart contract.

Conclusion

At this point, you've successfully ran you first zkSNARK on the Ethereum blockchain. Congratulations!

Remember that in this example only two parties were involved. This special case makes it easy to deal with the trust assumptions of zkSNARKs: only Victor was interested in verifying the claim by Peggy, hence he can trust his execution of the setup phase.

In general, multiple parties may be interested in verifying the correctness of Peggy's statement. For example, in the zero-knowledge based cryptocurrency Zcash, each node needs to be able to validate the correctness of transactions. In order to generalize the setup phase to these multi-party use-cases a tricky process, commonly referred to as "trusted setup" or "ceremony" needs to be conducted.

ZoKrates would welcome ideas to add support for such ceremonies!

A ZK Magic Square in the browser

Testing

Unit tests

In ZoKrates, unit tests comprise of

  • internal tests for all zokrates crates
  • compilation tests for all examples in zokrates_cli/examples. These tests only ensure that the examples compile.
  • compilation + witness-computation tests. These tests compile the test cases, compute a witness and compare the result with a pre-defined expected result. Such test cases exist for
    • The zokrates_core crate in zokrates_core_test/tests
    • The zokrates_stdlib crate in zokrates_stdlib/tests

Unit tests can be executed with the following command:

cargo test --release

Integration tests

Integration tests are excluded from cargo test by default. They are defined in the zokrates_cli crate in integration.rs and use the test cases specified in zokrates_cli/tests/code.

Integration tests can then be run with the following command:

cargo test --release -- --ignored

If you want to run unit and integrations tests together, run the following command:

cargo test --release & cargo test --release -- --ignored