A Snarky Exponential Function

In Coda, we use the proof-of-stake protocol Ouroboros for consensus. Naturally since this is Coda, that means we have to check proofs-of-stake inside a SNARK.

Fig. 2: The minimum dominating set of a graph

A proof-of-stake for a person with some amount of stake $a$ in Ouroboros is a random number $s$ between 0 and 1 (which one provably has generated fairly) such that $s$ is less than some threshold depending on $a$. Concretely, that threshold is 1−(1/2)aT1 – (1/2)^{\frac{a}{T}}1−(1/2)Ta where $T$ is the total amount of stake in the system.

It’s important to use a threshold of this form because it means that the density of blocks over time does not depend on the distribution of stake.

If you know anything about SNARKs, you know that inside of a SNARK all we can do is arithmetic (that is, addition and multiplication) in a finite field FpF_pFp. It’s not at all clear how we can compute a fractional number raised to a fractional power!

We’ll go through a very cool technique for computing such a thing. All the code for doing what we’ll talk about is implemented using snarky and can be found here.

The technique will go as follows:

1. We’ll use Taylor series to approximately reduce the problem to doing arithmetic with real numbers.
2. We’ll approximate the arithmetic of real numbers using the arithmetic of rational numbers.
3. We’ll then approximate the arithmetic of rational numbers using integer arithmetic.
4. Finally, we’ll simulate integer arithmetic using finite field arithmetic.

Taylor Series

First we need a way to reduce the problem of computing an exponentiation to multiplications and additions in a finite field. As a first step, calculus lets us reduce exponentiation to multiplication and addition over the real numbers (a field, but not a finite one) using a Taylor series.

Specifically, we know that

We can truncate this Taylor series to get polynomials TnT_nTn

by taking the first $n$ terms. The Taylor polynomials nearly compute 1−(1/2)x1 – (1/2)^x1−(1/2)x, but with some error that gets smaller as you take more and more terms. You can see this in the image of the actual function (in blue) along with the first few Taylor polynomials (in black).

It turns out there’s a handy formula which lets us figure out how many terms we need to take to make sure we get the first $k$ bits of the output correct, so we can just use that and truncate at the appropriate point for the amount of precision that we want.

From Reals to Rationals

Multiplication and addition are continuous, which means if you change the inputs by only a little bit, the outputs change by only a little bit.

Explicitly, if instead of computing x1+x2x_1 + x_2x1+x2, we compute a1+a2a_1 + a_2a1+a2 where aia_iai is xix_ixi plus some small error eie_iei, we have a1+a2=(x1+e1)+(x2+e2)=(x1+x2)+(e1+e2)a_1 + a_2 = (x_1 + e_1) + (x_2 + e_2) = (x_1 + x_2) + (e_1 + e_2)a1+a2=(x1+e1)+(x2+e2)=(x1+x2)+(e1+e2) so the result is close to x1+x2x_1 + x_2x1+x2 (since e1+e2e_1 + e_2e1+e2 is small).

Similarly for multiplication we have $a1a2=(x1+e1)(x2+e2)=x1x2+e1x1+e2x2+e1e2$. If $e1,e2$ are small enough compared to x1x_1x1 and x2x_2x2, then $e1x1+e2x2+e1e2$ will be small as well, and so $a1a2$ will be close to $x1x2$.

What this means is that instead of computing the Taylor polynomial

using real numbers like $\log (2)$ (which is irrational), we can approximate each coefficient log⁡(2)k/k!\log(2)^k / k!log(2)k/k! with a nearby rational number and compute using those instead! By continuity, we’re guaranteed that the result will be close to the actual value (and we can quantify exactly how close if we want to).

From Rationals to Integers

There are a few ways to approximate rational arithmetic using integer arithmetic, some of which are more efficient than others.

The first is to use arbitrary rational numbers and simulate rational arithmetic exactly. We know that

so if we represent rationals using pairs of integers, we can simulate rational arithmetic perfectly. However, there is a bit of an issue with this approach, which is that the integers involved get really huge really quickly when you add numbers together. For example, $1/2+1/3+\cdots +1/n$ has $n!$ as its denominator, which is a large number.

That’s a problem for us inside the SNARK, because we’re working with a finite field and want to make sure there is no overflow.

A better approach is to use rational numbers whose denominator is a power of two. These numbers are called dyadic rationals and are basically the same thing as floating point numbers.

Here, addition can be simulated using integers as follows. A rational number a2k\frac{a}{2^k}2ka is represented as the pair $(a,k)$. Say $k\le m$. For addition, we have

so the denominator of a sum is the max of the denominators of the inputs. That means that the denominators don’t get huge when you add a bunch of numbers (they will stay as big as the largest input to the sum).

Moreover, any rational number can be approximated by a number of this form (it’s just the binary expansion of that number).

From Integers to a Finite Field

To recap, we’ve done the following.

1. We approximated our exponential 1−(1/2)x1 – (1/2)^x1−(1/2)x by arithmetic over the reals using Taylor polynomials.
2. We approximated real arithmetic by rational arithmetic using continuity.
3. We approximated rational arithmetic by the arithmetic of dyadic-rationals/floats, again using continuity. Moreover, we saw that floating point arithmetic can easily be simulated exactly using integer arithmetic.

Now our final step is to simulate integer arithmetic using the arithmetic of our prime order field Fp\mathbb{F}_pFp. But this step is actually the easiest! As long as we are careful about numbers not overflowing, it’s the same thing. That is, if we know ahead of time that $a+b<p$, then we can safely compute $a+b\mathrm{m}\mathrm{o}\mathrm{d}p$, knowing that the result will be the same as over the integers. The same is true for multiplication. So as long as we don’t do too many multiplications, the integers representing the dyadic rationals we’re computing with won’t get too big, and so we will be okay. And if we don’t take too many terms of the Taylor series, this will be the case.

Conclusion