Step-by-step information to use Zokrates with Tezos.

Tezos has upgraded its protocol to 008 Edo. It supports BLS12-381 elliptic curve which permits zero knowledge proofs in Tezos. Cool! However, there are not much examples of them today. How can we play with ZK? Unfortunately, Edo does not tell us much since it only implements types and opcodes to verify BLS12-381 pairings. Building these pairs and how to convert your idea of ZK to Tezos code are off chain, therefore they are not in the code of Tezos node.

The sole example I found is `groth16.tz`

which is a verifier of knowledge of the square root of a natural number. It says:

The verifying key, proof, and inputs are generated from ZoKrates, modified to use BLS12-381.

Playing few hours with ZoKrates, a zero knowledge proof tool kit, I manged to find how to use it for Tezos. So this article:

- The latest ZoKrates can produce verification circuit and proofs using BLS12-381 out of the box.
- We can use ZoKrates to generate the data and code for ZK in Tezos. Small conversions are still required, though. I will show you how to do it in this article.

Disclaimer: I am a dummy of ZK. I hope I can learn some of it through playing in Tezos.

## Configuration

ZoKrates must be used with the following curve and proving scheme for Tezos:

- BLS12-381
- Since Tezos provides BLS12-381 elliptic curve operators for ZK proofs, ZoKrates must be used with it, instead of its default curve BN128.
- G16
- G16 proving scheme must be chosen for BLS12-381.

Specifying BLS12-381 and G16 at each step of ZoKrates, you can get required information to build ZK proof circuits and proofs.

## Step by step example

We follow the `root.zok`

example and make a Tezos smart contract to verify the knowledge of the square root of the given number. `groth16.tz`

is actually the same contract. Therefore here we are going to reproduce it.

### Installation of ZoKrates

I used the one-line installation script available at https://zokrates.github.io/gettingstarted.html .

### Write `root.zok`

“I know the square root `a`

of `b`

”:

```
def main(private field a, field b) -> bool:
return a * a == b
```

Quite straightforward except it is in Pythonish DSL which I am not very familiar with :-)

### Compilation

```
zokrates compile -c bls12_381 -i root.zok
```

Do not forget to add `-c bls12_381`

option!

### Perform the setup phase

```
zokrates setup -s g16
```

This produce `verification.key`

### Export the verifier code in Solidity

```
zokrates export-verifier -s g16
```

This generates `verfier.sol`

, a Solidity code.

Do **not** put `-c bls12_381`

option here. Since Ethereum does not support BLS12_381 yet, ZoKrates rejects the export with the option. The code without the option is not correct for BLS12-381 but we can still get the algorithm to verify proofs.

### Compute witness

“I know sqrt(113569) is 337”:

```
zokrates compute-witness -a 337 113569
```

This produces a file `witness`

.

### Generate a proof of computation

```
zokrates generate-proof -s g16
```

It converts the witness to a proof `proof.json`

.

### Verify the proof with ZoKrates

You can check the proof verification by:

```
zokrates verify -s g16 -c bls12_381
```

### Porting to Tezos

We need the following files:

`verification.key`

and`verification.sol`

to build a smart contract to verify proofs`proof.json`

to build a proof

Since the encoding of G1,G2, and Fr values in Tezos are different from one of ZoKrates, we need some work here.

#### G1 and G2 points

G1 and G2 points in `verification.key`

and `proof.json`

are pairs of x and y coordinates. For example, a G1 point looks like:

```
[
"0x09323a4fd658ab2e113dd6a2b79a8afb68ee2172a19da27c6d5fd2b165fbc5c6cb22a3e109095105917775ba152c3b96",
"0x138b65ff88e08a00e7cbe3180a132b5248d2593ace21babd1c063ddf0634d637c087b786b8cfce5d7bb6d30f1147cdeb"
]
```

Michelson (Tezos’s smart contract VM) uses a natural number instead of the coordinates. Conversions are available in `bls12-381`

OCaml library:

`Bls12_381.G1.Uncompressed.of_z_opt`

for G1 points`Bls12_381.G2.Uncompressed.of_z_opt`

for G2 points

For now this requires a small OCaml programming.

#### Fr values

Fr points in Michelson are in little endian.

A Fr value in ZoKrates such as

```
0x000000000000000000000000000000000000000000000000000000000001bba1
```

which is 113569, must be converted to

```
a1bb010000000000000000000000000000000000000000000000000000000000
```

in Michelson. Yes, you have to reverse the bytes. Again, we can do this conversion with `bls12-381`

:

```
let `Hex h =
Hex.of_bytes
@@ Fr.to_bytes
@@ Fr.of_z
@@ Z.of_string "0x000000000000000000000000000000000000000000000000000000000001bba1"
```

### Verification code

If you observe `verifier.sol`

, you can find the code to verify proofs at the end of the file:

```
...
// Compute the linear combination vk_x
Pairing.G1Point memory vk_x = Pairing.G1Point(0, 0);
for (uint i = 0; i < input.length; i++) {
require(input[i] < snark_scalar_field);
vk_x = Pairing.addition(vk_x, Pairing.scalar_mul(vk.gamma_abc[i + 1], input[i]));
}
vk_x = Pairing.addition(vk_x, vk.gamma_abc[0]);
if(!Pairing.pairingProd4(
proof.a, proof.b,
Pairing.negate(vk_x), vk.gamma,
Pairing.negate(proof.c), vk.delta,
Pairing.negate(vk.alpha), vk.beta)) return 1;
...
```

All you need is to port this code to Tezos:

```
(* Compute vk_x as
(vk_gamma_b * input_x) + (vk_gamma_c * input_y) + vk_gamma_a
*)
let open BLS12_381.G1 in
let vk_x =
vk_gamma_b * input_x
+ vk_gamma_c * input_y
+ vk_gamma_a
in
let list =
[ (proof_a, proof_b);
(~- vk_x, vk_gamma);
(~- proof_c, vk_delta);
(~- vk_a, vk_b) ]
in
assert (BLS12_381.pairing_check list)
```

Sorry it is not Michelson. This is SCaml, my experimental Michelson backend of OCaml language. Its dev branch supports BLS12-381 related types and functions. I hope it is easier to read than the equivalent Michelson VM code for most people. Of course you can write the same program using your preferred high level languages which compile to Michelson. It should not be difficult if they support the BLS12-381 constants and functions.

Michelson code should look just like `groth16.tz`

, however, the parameters I got from ZoKrates are different from this Michelson code. I have no idea why they are different.

### Final code in SCaml

Adding the definitions of G1,G2 parameters converted from `verification.key`

, we have the verifier code for Tezos. G1, G2, and Fr encodings in Tezos are written as `G1Bytes "0x..."`

, `G2Bytes "0x..."`

, `FrBytes "0x..."`

respectively:

```
open SCaml
let [@entry] main
( ( ( input_x : bls12_381_fr),
( input_y : bls12_381_fr) ),
( ( proof_a : bls12_381_g1 ),
( proof_b : bls12_381_g2 ),
( proof_c : bls12_381_g1 ) ) )
()
=
let vk_a = G1Bytes "0x169d7633e3da4d413bf1918c412fc54c548ddf641a423f47b61ca883c0ba1b85f5ee13dd63d7c1661cc4fe2ca38f00e1065dbcfb2123f8258ae2b3cf92035485f621e55d433b1f251ad37c02ae2b3ec6a1658ae23bbc77649878ec0871a6d8f1" in
let vk_b = G2Bytes "0x16c58ffdfec9c8b7a4d3826e32a40f99e97bd237067971e474438078e8bca6ccbbee0870bef905972fe879030273dd671116f52efd0f128a0bd6be9042bec761332408e765609caae2b6f7805ab3287143a9bafeb94a7cdd6635fd1ee293c2cf037bef7f92e32e639cd632611077b121db404705da6a507b9b8d8adc08a38eba27b2d31b7b22e95a96e22e26660162d30dd3791f5adb64150c2e7082f23a214b7ef5aa97fd903e648637deb13c156061788756f74b75545c3453e10822012e6a" in
let vk_gamma = G2Bytes "0x00e3114ca5fa1c0af741154f059c94a4d2647481ba6071b97317587a937e21f048e5f85191ba2fbd0f3929121485f4e21889d7bcf405c1932c7cc66ea8d353b34844769b50da863b3f0f11079371d2e6b7c10031e270761f136e2f4e52f162241182c943f4672b1293f79699f6747d874e805f57e8211aae940d3e31693619054e2be22cb99b177cfc092db80c1f789616872517c4811f11bba424dc64fdb3e6f27455e736d369d04de53a3e51eb36d4be6686a07f8be5352c138aceea7c6357" in
let vk_delta = G2Bytes "0x1394d62459f5e72373706504085111cae6afb88121e8f5707a9ff82daf97d300b9a20fc52a6ac7149dac1626d1e4d0ae095f3f088b18f2ab4e44df666560e101f4c83da739ce074527deb3fde2fcb25e2a19fe2a0f7c4f546ca7f904575875b916ec4958b2b639d08f0c1bbd4af8e9e9289280e84b7308d790da4707ceefe61c78b661fbd76f8be9bd365ddd9a5f0b250d108a1585684a6ccbc94bdcb37c133579866e5dabb75c77178927d38f59a687015995d7c6d7fb536ee9f76f7e8081b2" in
let vk_gamma_a = G1Bytes "0x07f1710668da99b2b45e6392d5cd89db7a1d34eff180ead6c886d51bca063f8111a179640d5d2dfc209e0a92783fea070b5a9436d5c1be84f88a4127c9a02d307c5858df52ce76ae0b6fbb5c0d855438419e06a1c37f633b306e9da44eaf345e" in
let vk_gamma_b = G1Bytes "0x18c1bf32977afa48e224b2209e9df000ea072af1cf06efc9e83cf9b156ff577e154da015b077626e2bab7a8300a087ea18dbc6bb77f98da0fc7e492c0624fd30b513ef5cfb54f2ed052216485052ba8a117f83a63e925b735fb6fe7c4c88e364" in
let vk_gamma_c = G1Bytes "0x102bae3361383e2cef7d4aed348743201f6fd5fd25f4400d0888451a5556cd980f311510e6457e36fe8f3309472695390cf8968b8d779e53c04632588e402ae5884cc49ee3988159ede6a292fb3b9cd1071eec4bf3fffe51b7325184cadeab1d" in
(* Compute vk_x as
(vk_gamma_b * input_x) + (vk_gamma_c * input_y) + vk_gamma_a
*)
let open BLS12_381.G1 in
let vk_x =
(*
Pairing.G1Point memory vk_x = Pairing.G1Point(0, 0);
for (uint i = 0; i < input.length; i++) {
require(input[i] < snark_scalar_field);
vk_x = Pairing.addition(vk_x, Pairing.scalar_mul(vk.gamma_abc[i + 1], input[i]));
}
vk_x = Pairing.addition(vk_x, vk.gamma_abc[0]);
*)
vk_gamma_b * input_x + vk_gamma_c * input_y + vk_gamma_a
in
let list =
(*
if(!Pairing.pairingProd4(
proof.a, proof.b,
Pairing.negate(vk_x), vk.gamma,
Pairing.negate(proof.c), vk.delta,
Pairing.negate(vk.alpha), vk.beta)) return 1;
*)
[ (proof_a, proof_b);
(~- vk_x, vk_gamma);
(~- proof_c, vk_delta);
(~- vk_a, vk_b) ]
in
assert (BLS12_381.pairing_check list);
[], ()
```

SCaml repo has the same example with the following sample input to prove the knowledge of the sqrt of 113569:

```
((FrBytes "0xa1bb010000000000000000000000000000000000000000000000000000000000",
FrBytes "0x0100000000000000000000000000000000000000000000000000000000000000"),
(G1Bytes "0x0be7a1f93063b64f1c4fe808f270fd6c8308308ece32e008210f74eb86528763134fc88a712c5451fe8ceef98284206f1940743c0c34528170e0f5c1c65cd6d60a0ea8697d95ebd8dc0a878e9443bc32f3388c47f596cfc6574b2c3a4c362b1b",
G2Bytes "0x0308a50cce70539b2770a3aa721134800236f8f7b26d76dccf8c367f29b6f5c423555b1b98441a7e795d696e6d23e4c20cca39682acbf7fa4ec06de7c8cf0054bdd7905ac84d4828152f8aa041162d97c6437f414577b5cdd2c11fbfc4aa098909c9678e63994ce7846898f592c1f51c8f164e5f1f299050dc0f6e656692f1e3d10e63ce24ab46045e4c9b7727d12df20e6bbc8cf1f6a0516cd52c322a336a28de8b86a1d15ed3c8d727245991b145d2cb3ac69043a8619832319e533c49455a",
G1Bytes "0x09323a4fd658ab2e113dd6a2b79a8afb68ee2172a19da27c6d5fd2b165fbc5c6cb22a3e109095105917775ba152c3b96138b65ff88e08a00e7cbe3180a132b5248d2593ace21babd1c063ddf0634d637c087b786b8cfce5d7bb6d30f1147cdeb"))
```

## Better syntax for G1, G2, and Fr

G1, G2, Fr conversions from ZoKrates to Tezos are tedious. SCaml supports better scripting:

`G1Point (x,y)`

and`G2Point ((x1,x2), (y1,y2))`

which can take the point coordinates of G1 and G2 of ZoKrates.`Fr z`

which can take the same Fr values of ZoKrates. No reversal of bytes required.

You can see uses of these constructors here.

## Conclusion

This article demonstrates how to use ZoKrates to generate the necessary information for ZKP for Tezos. ZoKrates is not designed for Tezos therefore we need some data conversion. But it is not difficult.

I believe Tezos ZK gurus will provide a nicer Tezos native ZK framework in near future. Until then, ZoKrates gives us a small ZK playground for Tezos.