ZoKraTez: How to play Zero Knowledge Proofs using ZoKrates and Tezos

NOTE: This works with ZoKrates 0.6.3. In a recent ZoKrates release 0.7.14, zokrates export-verifier fails for the combination of bls12-381 and g16. See Wokraround for new Zokrates for details.

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.

I cannot stop thinking of a fat pig when I hear "Socrates".

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.

Workaround for new ZoKrates

Recent release of ZoKrates, 0.7.14 cannot produce Solidity code when the code is compiled with -c bls12-381. You can use -c bn128 instead, which is supported for Ethereum:

$ zokrates compile -c bn128 -i root.zok
$ zokrates setup -s g16
$ zokrates export-verifier

It produces (somehow) the same verification code.

We still need to use -c bls12-381 for the points:

$ zokrates compile -c bls12_381 -i root.zok
$ zokrates setup -s g16
$ zokrates compute-witness -a 337 113569
$ zokrates generate-proof -s g16
$ zokrates verify
blockchain  tezos  scaml  zk