Note: An update on Dark Forest v0.4 is coming soon.

In this post, we’ll cover one of the zkSNARKs used in Dark Forest in more detail. This is a follow-up to the first post in our ZKPs for Engineers sequence - if you haven’t read the introductory post, we’d recommend that you check it out!

Dark Forest is secured by two zero-knowledge circuits: init and move (see here for an old verion). Players generate a ZKP from the init circuit when they join the game, and a ZKP from the move circuit whenever they make a move. We’ve written all of our circuits in iden3’s Circom SNARK language; for a more in-depth look at the language, we highly recommend checking out the circom and snarkjs repositories and tutorials. We’ll be walking through a simplified version of our init circuit in this article.

The MiMC Hash Function

As we’ve mentioned before, all player location information is kept private. This means that the coordinates of all of your planets are never uploaded to the blockchain, where all data is publicly accessible. Instead, only the hashes of the coordinates of your planets are uploaded to the Dark Forest core contract. We call the hash of any coordinate pair the ID of the location. For example, the ID of the location \((25, 16)\) is \(10416772522344246412829212518211502356912209709429179585505073494732305933882\).

When you initialize at a new home planet, and whenever you conquer a new planet, you send the ID of the location of interest up to the blockchain. Without zkSNARKs, there’s an obvious attack vector - a malicious player could simply upload random bytestrings up to the blockchain, destroying the integrity of the game. Therefore, we require that all players always submit ZK Proofs along with location IDs that they interact with, to ensure that they really are performing operations on valid game locations.

The core of all Dark Forest zkSNARKs is therefore a SNARK for our chosen location ID hash function, the MiMC hash. MiMC is a hash function in a family of “SNARK-friendly” hashes–hash functions which are easy to generate ZKPs for.

What makes a function SNARK-friendly? Previously, we discussed how any function that gets fed into a SNARK needs to get broken down at some level into a series of prime field multiplication and addition operations. While this is theoretically possible for almost all functions, some functions are less costly to break down than others. For example, functions which require lots of bit operations are actually among the most expensive to represent in terms of field multiplications and additions. So SNARK-friendly functions are functions which as much as possible stick to native field arithmetic.

The MiMC hash function is a very simple function constructed with the above in mind. It involves a sequence of 220 repeated multiplications and additions: enough so that it’s extremely costly to try to reverse-engineer the pre-image of the hash, but few enough so that its still practical to compute with the modern SNARK tools we currently have available. Despite its simplicity, it still takes nearly a minute for us to actually generate the MiMC SNARK on a modern Macbook Pro!

The init Circuit

On initialization, players can choose any valid home planet to start the game on. Players pick some location \((x, y)\), compute the hash \(h\) of the location, and send the hash to the blockchain along with a ZKP that they computed the hash from a valid location.

A valid location is any coordinate pair \((x, y)\) that is no greater than \(r\) units away from the origin, where \(r\) is the current world radius (players can’t initialize arbitrarily far out). So our SNARK needs to prove 2 things:

Here’s the Circom circuit that makes this all happen.

include "./mimcsponge.circom"
include "./comparators.circom"

template Main() {
    signal private input x;
    signal private input y;
    signal input r;

    signal output h;

    /* check x^2 + y^2 < r^2 */
    component comp = LessThan(64);
    signal xSq;
    signal ySq;
    signal rSq;
    xSq <== x * x;
    ySq <== y * y;
    rSq <== r * r;
    comp.in[0] <== xSq + ySq
    comp.in[1] <== rSq
    comp.out === 1;

    /* check MiMCSponge(x,y) = pub */
    component mimc = MiMCSponge(2, 220, 1);

    mimc.ins[0] <== x;
    mimc.ins[1] <== y;
    mimc.k <== 0;

    h <== mimc.outs[0];
}

We’ll walk through all of the major components of this circuit below.

Imports

Circom allows you to write and import reusable SNARK circuit components. At the top of our circom file, we import ./mimcsponge.circom and ./comparators.circom, two circuits from circomlib, a library of useful utility circuits written by iden3 and volunteers.

Once we’ve imported ./mimcsponge.circom, we gain access to the MiMCSponge component. This is a reusable circuit component which can be “plugged in” to larger circuits, such as our init circuit. Similarly, comparators.circom gives us access to the LessThan component, which allows us to determine which of two values we are comparing is larger.

Public and Private Signals

In the beginning of our circuit, we declare four signals, which you can think of as variables. Two of these are private: x and y. The other two, r and h, are public. Note that we provide only x, y, and r; circom will compute h and generate the appropriate constraints.

The smart contract will receive the public signals, r and h, along with our ZK Proof that they correspond to a valid private coordinate pair \((x, y)\). So if this zkSNARK works correctly, the contract will be able to verify the validity of our starting coordinates without having any idea about what they actually are.

Checking the World Radius

We first want to prove that the private coordinates we’re initializing at are “in bounds.” To do this, we need to add constraints enforcing that, for the provided \(x\) (secret), \(y\) (secret), and \(r\) (public), \(x^2 + y^2 <= r^2\).

Fortunately, this is relatively straightforward. We constrain an intermediate signal xSq to be the product of x with itself; we do the same for ySq and rSq. Then, we can use the LessThan component imported from ./comparators.circom to constrain the sum of xSq and ySq to be at most rSq. LessThan.out is 1 if the LessThan.in[0] < LessThan.in[1], and 0 otherwise. So if we set comp to be a LessThan component with inputs xSq + ySq and rSq, our world radius constraint is enforced with the constraint expression comp.out === 1.

One last thing to check is that negative numbers don’t mess up any of our computations or constraints. Indeed, squaring works exactly how we’d like it to in a prime field: \((p-3)^2\) and \(3^2\) are both congruent to \(9\), so our distance checks still work!

/* check x^2 + y^2 < r^2 */
component comp = LessThan(64);
signal xSq;
signal ySq;
signal rSq;
xSq <== x * x;
ySq <== y * y;
rSq <== r * r;
comp.in[0] <== xSq + ySq
comp.in[1] <== rSq
comp.out === 1;

Constraining the Hash

MiMC is a relatively complicated function to write inside of a SNARK; it’s certainly much harder than our bounds checking logic. Fortunately, an implementation already exists in circomlib. We use the double-arrow notation to both compute and constrain \(h\), the hash of our coordinate pair.

component mimc = MiMCSponge(2, 220, 1);

mimc.ins[0] <== x;
mimc.ins[1] <== y;
mimc.k <== 0;

h <== mimc.outs[0];

Bonus 1: Range Proofs

Edit: Daira Hopwood points out that there is a subtle bug here - LessThan itself does not check the bit length. We’ve fixed our circuits, but we’ll leave this up for anyone else who wants to dig in.

There’s one more thing we have to watch out for: overflow errors. If a malicious player submits a pair \((x, y)\) whose squares just barely overflow the SNARK prime \(p\), they might be able to initialize at some extremely far away location without the SNARK knowing any better. To prevent this, we need to add in range proofs, to check that the absolute values of x and y are at most some reasonable number (here we choose \(2^{32}\)). Range proof circuits are shown below.

include "comparators.circom"

template RangeProof(bits, max_abs_value) {
    signal input in; 

    component lowerBound = LessThan(bits);
    component upperBound = LessThan(bits);

    lowerBound.in[0] <== max_abs_value + in; 
    lowerBound.in[1] <== 0;
    lowerBound.out === 0

    upperBound.in[0] <== 2 * max_abs_value;
    upperBound.in[1] <== max_abs_value + in; 
    upperBound.out === 0
}

// input: n field elements, whose abs are claimed to be less than max_abs_value
// output: none
template MultiRangeProof(n, bits, max_abs_value) {
    signal input in[n];
    component rangeProofs[n];

    for (var i = 0; i < n; i++) {
        rangeProofs[i] = RangeProof(bits, max_abs_value);
        rangeProofs[i].in <== in[i];
    }
}

Bonus 2: Perlin Noise

A new feature in Dark Forest v0.4 is that certain regions of space are designated as safe NEBULAs, while other regions of space are designated as dangerous but more rewarding DEEP SPACE. In order to do this securely, we must be able to assign a “temperature” to any location in the universe, such that nearby locations will tend to have similar temperatures.

This problem is solved by a class of methods known as procedural generation. We use a simple procedural generation algorithm called Perlin Noise to assign temperature values to locations in the universe. The implementation of Perlin Noise inside of a zkSNARK is out of scope of this post, but we’ll note that it would be the job of these lines to plug the MultiScalePerlin component into the init circuit, generating a proof of universe temperature:

signal input p;

/* check perlin(x, y) = p */
component perlin = MultiScalePerlin(3);
perlin.p[0] <== x;
perlin.p[1] <== y;
p === perlin.out;

We’ll cover the tools used to build up the MultiScalePerlin circuit in future posts!

Conclusion

The same basic tools we use to construct our relatively simple init circuit are also used to build the move circuit, as well as a few more complex circuits we’ll be releasing in the next edition of Dark Forest. Be on the lookout for future articles about more advanced SNARK circuits!