1
0
Fork 0
mirror of synced 2025-09-24 04:40:05 +00:00

restructure, amend tutorial

This commit is contained in:
schaeff 2018-10-26 16:31:46 +02:00
parent 8de54f5979
commit 7ad49a45a5
12 changed files with 250 additions and 250 deletions

View file

@ -3,11 +3,17 @@
- [Introduction](./introduction.md)
- [Getting Started](./gettingstarted.md)
- [Proofing a Hash Pre-Image](./sha256example.md)
- [ZoKrates Programming Concepts](./concepts.md)
- [Programming Concepts](./concepts.md)
- [Variables](./concepts/variables.md)
- [Types](./concepts/types.md)
- [Functions](./concepts/functions.md)
- [Control flow](./concepts/control_flow.md)
- [Comments](./concepts/comments.md)
- [ZoKrates Reference](reference/index.md)
- [Reference](reference/index.md)
- [Grammar](reference/grammar.md)
- [CLI](reference/cli.md)
- [Verification](reference/verification.md)
- [Tutorial: Proof of preimage](./sha256example.md)

View file

@ -1,184 +1 @@
# ZoKrates Programming Concepts
## Variables
Variables can have any name which does not start with a number. Underscores are not allowed in variable names.
## Types
ZoKrates currently exposes three types:
### `field`
This is the most basic type in ZoKrates, and it represents a positive integer between `0` and `p - 1`, where `p` is a (large) prime number.
The prime `p` is set to `21888242871839275222246405745257275088548364400416034343698204186575808495616` as imposed by the pairing curve supported by Ethereum.
While `field` values mostly behave like unsigned integers, there are some things to keep in mind:
- They overflow at p and not some power of 2 and underflow at 0, so that we have:
```zokrates
def main() -> (field):
field p_minus_one = 21888242871839275222246405745257275088548364400416034343698204186575808495616
0 - 1 == p_minus_one
return 1
```
### `bool`
ZoKrates has limited support for booleans, to the extent that they can only be used as the condition in `if ... else ... endif` expressions.
You can use them for equality checks, inequality checks and inequality checks between `field` values.
Note that while equality checks are cheap, inequality checks should be use wisely as they are orders of magnitude more expensive.
### `field[n]`
Static arrays of `field` can be instantiated with a constant size, and their elements can be accessed and updated:
```zokrates
def main() -> (field):
field[3] a = [1, 2, 3]
a[2] = 4
return a[0] + a[2]
```
## Comments
Comments can be added with double-slashes.
```zokrates
def main() -> (field):
field a = 42 // this is an end of line comment
// this is a full line comment
return a
```
## Functions
A function has to be declared at the top level before it is called.
```zokrates
def foo() -> (field):
return 1
def bar() -> (field):
return foo()
```
A function's signature has to be explicitely provided.
Functions can return many values simply by providing them as a comma-separated list.
```zokrates
def main() -> (field, field[3]):
return 1, [2, 3, 4]
```
### Inference
When defining a variable as the return value of a function, types are optional:
```zokrates
def foo() -> (field, field):
return 21, 42
def main() -> (field):
a, b = foo()
return 1
```
If there is an ambiguity, providing the types of some of the assigned variables is necessary.
```zokrates
def foo() -> (field, field[3]):
return 1, [2, 3, 4]
def foo() -> (field, field):
return 1, 2
def main() -> (field):
a, field[3] b = foo()
return 1
```
## Control Flow
ZoKrates provide a single thread of execution with two control flow constructs.
### Function calls
Function calls can help make programs clearer and more modular. However, using function calls is not always zero-cost, so deep call chains should be avoided.
Arguments are always passed by value, so that no side effects inside the callee will be visible to the caller.
```zokrates
def incr(field a) -> (field)
a = a + 1
return 1
def main() -> (field):
field x = 1
field res = incr(x)
x == 1 // x has not changed
return 1
```
### For loops
For loops are available with the following syntax:
```zokrates
def main() -> (field):
field res = 0
for field i in 0..4 do
res = res + i
endfor
return res
```
The bounds have to be known at compile time, so only constants are allowed.
For loops have define their own scope.
## Standard library
ZoKrates comes with a number of reusable components. For now, these components are:
### sha256
```zokrates
import "LIBSNARK/sha256"
```
A function that takes 512 field elements as inputs, checks that they are all bits, and returns their sha256 hash as 256 field elements.
### sha256compression
```zokrates
import "LIBSNARK/sha256compression"
```
A function that takes 512 field elements as inputs, checks that they are all bits, and returns the result of applying the sha256 compression function on them. The difference with `sha256` is that no padding is added at the end of the message, which makes it more efficient but also less compatible with Solidity.
### sha256packed
```zokrates
import "LIBSNARK/sha256packed"
```
A function that takes 2 field elements as inputs, unpacks each of them to 254 bits (big endian), pads each of them to 256 bits on the left, concatenates them and applies sha256. It then removes the two most significant bits and returns the rest as one field element. The rationale is that one `field` value can only hold 254 bits due to the size of `p`.
### pack254
```zokrates
import "PACKING/pack254"
```
Packs 254 field elements as one.
### unpack254
```zokrates
import "PACKING/unpack254"
```
Unpacks a field element to 254 field elements.
# Programming Concepts

View file

@ -0,0 +1,10 @@
## Comments
Comments can be added with double-slashes.
```zokrates
def main() -> (field):
field a = 42 // this is an end of line comment
// this is a full line comment
return a
```

View file

@ -0,0 +1,37 @@
## Control Flow
ZoKrates provide a single thread of execution with two control flow constructs.
### Function calls
Function calls can help make programs clearer and more modular. However, using function calls is not always zero-cost, so deep call chains should be avoided.
Arguments are passed by value.
```zokrates
def incr(field a) -> (field)
a = a + 1
return 1
def main() -> (field):
field x = 1
field res = incr(x)
x == 1 // x has not changed
return 1
```
### For loops
For loops are available with the following syntax:
```zokrates
def main() -> (field):
field res = 0
for field i in 0..4 do
res = res + i
endfor
return res
```
The bounds have to be known at compile time, so only constants are allowed.
For-loops define their own scope.

View file

@ -0,0 +1,46 @@
## Functions
A function has to be declared at the top level before it is called.
```zokrates
def foo() -> (field):
return 1
def bar() -> (field):
return foo()
```
A function's signature has to be explicitely provided.
Functions can return many values by providing them as a comma-separated list.
```zokrates
def main() -> (field, field[3]):
return 1, [2, 3, 4]
```
### Inference
When defining a variable as the return value of a function, types are optional:
```zokrates
def foo() -> (field, field):
return 21, 42
def main() -> (field):
a, b = foo()
return 1
```
If there is an ambiguity, providing the types of some of the assigned variables is necessary.
```zokrates
def foo() -> (field, field[3]):
return 1, [2, 3, 4]
def foo() -> (field, field):
return 1, 2
def main() -> (field):
a, field[3] b = foo()
return 1
```

View file

@ -0,0 +1,43 @@
## Standard library
ZoKrates comes with a number of reusable components. For now, these components are:
### sha256
```zokrates
import "LIBSNARK/sha256"
```
A function that takes 512 field elements as inputs, checks that they are all bits, and returns their sha256 hash as 256 field elements.
### sha256compression
```zokrates
import "LIBSNARK/sha256compression"
```
A function that takes 512 field elements as inputs, checks that they are all bits, and returns the result of applying the sha256 compression function on them. The difference with `sha256` is that no padding is added at the end of the message, which makes it more efficient but also less compatible with Solidity.
### sha256packed
```zokrates
import "LIBSNARK/sha256packed"
```
A function that takes 4 field elements as inputs, unpacks each of them to 128 bits (big endian), concatenates them and applies sha256. It then returns two field elements, each representing 128 bits of the result.
### pack128
```zokrates
import "PACKING/pack128"
```
Packs 128 field elements as one.
### unpack128
```zokrates
import "PACKING/unpack128"
```
Unpacks a field element to 128 field elements.

View file

@ -0,0 +1,37 @@
## Types
ZoKrates currently exposes three types:
### `field`
This is the most basic type in ZoKrates, and it represents a positive integer between `0` and `p - 1`, where `p` is a (large) prime number.
The prime `p` is set to `21888242871839275222246405745257275088548364400416034343698204186575808495616` as imposed by the pairing 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 and underflow at 0, so that we have:
```zokrates
def main() -> (field):
field p_minus_one = 21888242871839275222246405745257275088548364400416034343698204186575808495616
0 - 1 == p_minus_one
return 1
```
### `bool`
ZoKrates has limited support for booleans, to the extent that they can only be used as the condition in `if ... else ... endif` expressions.
You can use them for equality checks, inequality checks and inequality checks between `field` values.
Note that while equality checks are cheap, inequality checks should be use wisely as they are orders of magnitude more expensive.
### `field[n]`
Static arrays of `field` can be instantiated with a constant size, and their elements can be accessed and updated:
```zokrates
def main() -> (field):
field[3] a = [1, 2, 3]
a[2] = 4
return a[0] + a[2]
```

View file

@ -0,0 +1,4 @@
## Variables
Variables can have any name which does not start with a number. Underscores are not allowed in variable names.
Variables are mutable, and always passed by values to functions.

View file

@ -2,15 +2,19 @@
## Installation
### Docker
Using Docker is currently the recommended way to get started with ZoKrates.
```bash
docker run -ti zokrates/zokrates /bin/bash
```
Now you should be dropped into a shell and can find the `zokrates` executable in the following folder `ZoKrates/target/release`.
From there on, you can use the `zokrates` CLI.
Alternatively you can build the container yourself with the following commands:
### From source
You can build the container yourself from [source](https://github.com/JacobEberhardt/ZoKrates/) with the following commands:
```bash
git clone https://github.com/JacobEberhardt/ZoKrates
@ -20,11 +24,9 @@ docker run -ti zokrates /bin/bash
cd ZoKrates/target/release
```
Alternatively, you can build Cargo from [source](https://github.com/JacobEberhardt/ZoKrates/).
## Hello ZoKrates!
First, create the text-file `root.code` and implement your program. IN this example, we will prove knowledge of the square root of a number:
First, create the text-file `root.code` and implement your program. In this example, we will prove knowledge of the square root `a` of a number `b`:
```zokrates
def main(private field a, field b) -> (field):
@ -33,18 +35,22 @@ def main(private field a, field b) -> (field):
```
Some observations:
- The keyword `field` is the basic type we use, which is an element of a prime field.
- 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:
```bash
# compile
./zokrates compile -i root.code
# 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
```
The CLI commands are explained in more detail in this [section
](reference/cli.html) of the documentation.
The CLI commands are explained in more detail in the [CLI reference](reference/cli.html).

View file

@ -1,10 +0,0 @@
#ZoKrates Programming Concepts
## Variables
## Data Types
## Functions
## Control Flow

View file

@ -1,6 +1,6 @@
# ZoKrates Reference
The reference covers the details of various areas of Cargo.
The reference covers the details of various areas of ZoKrates.
- [ZoKrates Reference](index.md)
- [Grammar](grammar.md)

View file

@ -1,9 +1,9 @@
# Proving Knowledge of a Hash Pre-Image
# Tutorial: Proving knowledge of a hash preimage
Lets jump into ZoKrates by working through a hands-on project together! This chapter introduces you to the basic features of ZoKrates and how to use zkSNARKs in a real-world example.
Lets jump into ZoKrates by working through a hands-on project together!
Well implement a problem that's very typical in blockchain use-cases: proving the knowledge of a pre-image for a given hash digest.
In particular, we show how ZoKrates and the Ethereum blockchain can be used to allow a prover, lets call her Peggy, to demonstrate beyond any reasonable doubt to a verifier, lets call him Victor, that she knows a hash pre-image for a chosen digest by Victor, without revealing what the pre-image is.
Well 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, lets call her Peggy, to demonstrate beyond any reasonable doubt to a verifier, lets call him Victor, that she knows a hash preimage for a digest chosen by Victor, without revealing what the preimage is.
## Pre-requisites
@ -11,23 +11,25 @@ Make sure you have followed the instructions in the [Getting Started](gettingsta
## Computing a Hash using ZoKrates
We will start this tutorial by using ZoKrates to compute the hash-digest for an arbitrarily chosen pre-image, being the number `5` in this example.
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.code` with the following content:
```zokrates
import "LIBSNARK/sha256packed"
def main(private field a, private field b) -> (field):
c = sha256packed(a, b)
return c
def main(private field a, private field b, private field c, private field d) -> (field, field):
h0, h1 = sha256packed(a, b, c, d)
return h0, h1
```
Clearly, 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. The function takes 2 field elements as inputs. A `field` value, however, can only hold 254 bits due to the size of the underlying prime field used for elliptic-curve computation. As a consequence, the function unpacks each field element to its 254 bits and pads `00` on the left to obtain the required 256 bits. The two elements are then concatenated and a full SHA256 round on the 512 bits input is computed. Given that the resulting SHA256 hash-digest is 256 bit long the two most significant bits get removed and then the result is packed to a field element again. 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](https://blog.decentriq.ch/proving-hash-pre-image-zksnarks-zokrates) post.
The first line imports the `sha256packed` function from the ZoKrates standard library.
After this small detour let's go through the rest of the code:
The `main` function takes two private input arguments which are used to call the imported `sha256packed` function. In addition, we declare a field element `c` which is set to output of the hash function and gets returned from the program.
`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](https://blog.decentriq.ch/proving-hash-pre-image-zksnarks-zokrates) 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.
@ -43,92 +45,94 @@ As a next step we can create a witness file using the following command:
./zokrates compute-witness -a 0 5
```
Using the flag `-a` we can set the input arguments of the program. Recall that our goal is to compute the hash for the number `5`. Consequently we set `a` to `0` and `b` to `5`.
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 `witness` file for the return value:
Still here? Great! At this point, we can check the `witness` file for the return values:
```sh
grep '~out_0' witness
grep '~out' witness
```
which should lead to the following output:
```sh
~out_0 2841298070043759859224314537332116230625666178017083621071552164634727927312
~out_0 263561599766550617289250058199814760685
~out_1 65303172752238645975888084098459749904
```
Hence, we finally arrive at the following field value as the hash-digest for our selected pre-image :
`2841298070043759859224314537332116230625666178017083621071552164634727927312`
Hence, 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
At this point you might be wondering how all of this is useful. For now, we have seen that we can compute a hash using heavy finite field arithmetic on elliptic curves using ZoKrates.
For now, we have seen that we can compute a hash using ZoKrates.
Let's recall our goal: Peggy wants to proof that she knows a pre-image for a digest chosen by Victor, without revealing what the pre-image is. Without loss of generality, let's now assume that Victor choses the digest to be equivalent to our example above.
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 choses 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 digest 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.code`:
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.code`:
```zokrates
import "LIBSNARK/sha256packed"
def main(private field a, private field b) -> (field):
c = sha256packed(a, b)
c == 2841298070043759859224314537332116230625666178017083621071552164634727927312
def main(field a, field b, field c, field d) -> (field):
h0, h1 = sha256packed(a, b, c, d)
h0 == 263561599766550617289250058199814760685
h1 == 65303172752238645975888084098459749904
return 1
```
Not that we now compare the result of `sha256packed` with the hard-coded correct solution defined by Victor. Clearly, this program only returns true if all of the computed bits are equivalent.
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:
So, having defined the program, Victor is now ready to compile the code:
```sh
./zokrates compile -i hashexample.code
```
Based on that Victor can run the setup phase and export the Solidity verifier smart contract:
Based on that Victor can run the setup phase and export verifier smart contract as a Solidity file:
```sh
./zokrates setup
./zokrates export-verifier
```
`setup` will create a `verifiation.key` file and a `proving.key` file. Victor must make the `proving.key` publicly available to Alice.
`setup` creates a `verifiation.key` file and a `proving.key` file. Victor gives the proving key to Alice.
`export-verifier` creates a `verifier.sol` Solidity contract file that contains our verification key and a nifty function `verifyTx`. Victor deploys this smart contract to the Ethereum network.
`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.
Alice uses the `proving.key` to compute a witness to the problem:
Alice provides the correct pre-image as an argument to the program.
```sh
./zokrates compute-witness -a 0 5
./zokrates compute-witness -a 0 0 0 5
```
Note that Alice provides the correct pre-image as an argument to the program. However, these inputs are declared as private variables in the program and don't leak to Victor due to the zero knowledge aspect of the protocol.
Finally, Alice can run the command to construct the proof:
```sh
./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 eight variables that make up the zkSNARKs proof. The `verifyTx` function in the smart contract deployed by Victor accepts these eight values, along with an array of public inputs. The array of public inputs consists of:
* any parameters in the ZoKrates function, which do not contain the `private` keyword
* the return value(s) of the ZoKrates function
* 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 Alice has to define her public input array as follows: `[1]`
Victor is continuously monitoring the verification smart contract for the `Verified` event, which is emitted upon successful verification of a transaction. As soon as he observes the event triggered by a transaction from Alice's public address, he can be sure that Alice has a valid pre-image for the hash-digest he has put into the smart contract.
Alice can then submit her proof by calling `verifyTx`.
## Summary
Victor monitors the verification smart contract for the `Verified` event, which is emitted upon successful verification of a transaction. As soon as he observes the event triggered by a transaction from Alice's public address, he can be sure that Alice has a valid pre-image for the hash he set in the smart contract.
At this point, youve successfully ran you first zkSNARK on the Ethereum blockchain! Congratulations!
## Conclusion
This project was a hands-on way to introduce you to ZoKrates and the workflow to develop dApps using zkSNARKs.
At this point, youve successfully ran you first zkSNARK on the Ethereum blockchain. Congratulations!
Remember that in this example only two parties have been involved. This special case makes it easy to deal with zkSNARK's trust assumptions: only Vitor was interested in verifying the claim by Alice, hence he can trust his execution of the setup phase.
However, in more general use-cases there might be multiple parties interested in verifying the correctness of Alice's statement. For example, in the zero-knowledge based cryptocurrency Zcash every 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.
Currently, ZoKrates doesn't provide support for these types of setups.
>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 Alice, hence he can trust his execution of the setup phase.
>
>In general, multiple parties may be interested in verifying the correctness of Alice'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!