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 in Ouroboros is a random number between 0 and 1 (which one provably has generated fairly) such that is less than some threshold depending on . Concretely, that threshold is where 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 . It's not at all clear how we can compute a fractional number raised to a fractional power!
The technique will go as follows:
- We'll use Taylor series to approximately reduce the problem to doing arithmetic with real numbers.
- We'll approximate the arithmetic of real numbers using the arithmetic of rational numbers.
- We'll then approximate the arithmetic of rational numbers using integer arithmetic.
- Finally, we'll simulate integer arithmetic using finite field arithmetic.
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
by taking the first terms. The Taylor polynomials nearly compute , 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 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 , we compute where is plus some small error , we have so the result is close to (since is small).
Similarly for multiplication we have . If are small enough compared to and , then will be small as well, and so will be close to .
What this means is that instead of computing the Taylor polynomial
using real numbers like (which is irrational), we can approximate each coefficient 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, has 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.
Here, addition can be simulated using integers as follows. A rational number is represented as the pair . Say . 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.
- We approximated our exponential by arithmetic over the reals using Taylor polynomials.
- We approximated real arithmetic by rational arithmetic using continuity.
- 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 . 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 , then we can safely compute , 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.
Let's survey the net result of all this approximation: We have a very efficient way of approximately computing an exponential function on fractional inputs inside of a SNARK, in such a way that we can have concrete bounds on the error of the approximation. Pretty cool! This enables us to use a threshold function for Ouroboros that guarantees a constant density of blocks regardless of the distribution of stake.