zk-Ed25519: Underlying Mathematics

Ed25519 has emerged as the signature scheme of choice in the blockchain ecosystems such as Cosmos, NEAR, Solana, and others. Verifying blockchain consensus requires verifying a large number of Ed25519 signatures (validators’ signatures). Hence, there is a need for succinct verification of a batch of Ed25519 signatures.

As such, we have developed a library that enables creating a zk-snark proof of a batch of Ed25519 signatures. The code can be found here. Our circuits are built using Circom and we use Rapidsnark for proof generation.

Let's dive into how it works.

To implement the Ed25519 signature verification in a zk-circuits, we do the following 3 steps —

1. Define the finite field used by Ed25519 inside the SNARK finite field
2. Defining basic operations such as addition, multiplication, and modulo for the Ed25519 finite field inside the zk-circuit
3. Defining the twisted Edwards curve inside the SNARK finite field

1. Defining Ed25519 Finite Field Inside SNARK Finite Field

The Problem Statement

Verification of SNARKs can be particularly expensive in on-chain execution environments. For cheaper and efficient verification, Ethereum includes precompiles introduced in EIP 196 and EIP 197, which support curve operations and optimal ate pairing check for the elliptic curve alt_bn128. This means we should also use the alt_bn128 curve for generating our proofs if we want efficient proof verification on-chain.

The alt_bn128 curve is defined under a finite field modulo the prime p = 21888242871839275222246405745257275088548364400416034343698204186575808495617. (henceforth referred to as prime128). This means that operations inside a zk-circuit using this curve can only support numbers up to prime128.

Similarly, the generation and verification of Ed25519 signatures are operations on the twisted Edwards curve which is defined in a finite field under the prime p = 2²⁵⁵— 19 (hence referred to as prime 25519). Note that prime25519 > prime128.

Now, in order to generate SNARK proofs of Ed25519 signatures that can be verified cheaply on Ethereum, we need to perform Ed25519 curve operations inside the alt_bn128 finite field.

To achieve this, since prime25519 > prime128, we essentially need to represent a larger finite field inside a smaller one. This means we can not use the native/decimal representations for Ed25519 field elements since the numbers will overflow. Hence, we must define our field elements in an alternative number system.

We tried two different approaches—

Approach 1: Binary (Base 2) representation

The easiest approach is to represent all numbers in binary format, with each signal (field element) in Circom representing each bit. Since the only enumerable value for each signal/variable is 0 | 1, implementing addition, subtraction (using 2's complement), and multiplication is fairly straightforward. Any well-known algorithms can be used to do the same. However, using a binary representation is not efficient because we end up using only a fraction of the information each signal can capture, requiring a much larger number of signals to define the same computation. This, in turn, leads to a infeasibly large number of constraints.

Approach 2: Using a larger base

We can represent numbers in the same manner as a lot of BigInteger libraries do, by fitting smaller chunks inside the largest possible native element and using an array of such chunks to form larger numbers. We can fit at max d = largest_possible_field_element - 1 in a single signal. Instead of base 2 (binary), we can let each signal represent a "digit" up to this number d. In other words, a number system with base d+1. Now the information captured by each signal can be maximized, reducing the required computation for basic arithmetic operations compared to a binary representation.

The base we used in our implementation is 2⁸⁵, which is much smaller than the maximum base that we can use. There’s a specific reason for this, related to our implementation of the modulus operation. This is discussed in later sections.

2. Finite Field with Base 2⁸⁵

Now that we can represent the elements from the Ed25519 finite field inside the alt_bn128 finite field, let us see how we can perform operations on these numbers. Given that we are not using the native/decimal representations for field elements, we cannot used the native + and *operations provided by the CPU. We must define our own custom functions for operators such as addition, multiplication and modulus.

Addition and Multiplication

Find the implementation of base 2⁸⁵ adder here and base 2⁸⁵ Multiplier here. The multiplication algorithm is basically standard long multiplication, where the carry is handled in the end.

Modulus under prime25519

We must perform the modulo operation in such a way that long division is avoided since it would be too expensive inside a zk-circuit. The algorithm we have used is as follows —

Let the prime p for the curve to be defined as p = 2²⁵⁵ - 19. Given input x, we need to calculate x % p

We define c = 2^255 and,
r = x % c(Note that r < 2²⁵⁵. Also r is simply the least significant 255 bits of x )
q = x // c(q is simply x sans the least significant 255 bits of x )

Note that 255 = 85*3 . This is the reason we have selected 2⁸⁵ as the base. Calculating r (and by extension q) becomes very efficient since we can simply take the first 3 elements of the array representing x to calculate r. Long division is not needed.

Hence we derive equation (1)

x = q*c + r
x = q*(p+19) + r   -- (1)

Simplifying (1) and taking modulus p on both sides

x % p = 19*q % p + r % p

Now, calculate r % p as:

if (r>=p): r % p = r - p
if (r<p): r % p = r

However, there is no way to define conditional logic inside a circuit. Instead, we use a multiplexer which serves the same purpose when one out of multiple values needs to be selected. In this particular case, we provide both r and r-p as the input signals to the multiplexer, and assign the selector to be 0 | 1 based on whether r - p underflowed or not.

We can apply this algorithm recursively to calculate 19q % p. Recursion also means that x can be of arbitrary size.

Now that we have the basic operators in place for the Ed25519 finite field, we can use these as building blocks to define the twisted Edwards curve inside our zk-circuit.

3. Defining the Twisted Edwards Curve in the alt_bn128 Finite Field

We need to take two things into account —

1. All the curve operations for Ed25519 must be implemented from scratch using our custom operators defined in the previous section.
2. We must represent all the Ed25519 operations as polynomials so that they can be represented in the R1CS constraint model.

Let's start with point addition. Re-arranging the point addition equation for the twisted Edwards curve such that only + and * are used, we get:-

If three points (x1, y1), (x2, y2) and (x3,y3) satisfy these two polynomials, we can say that the third point is the sum of the first two points.

Please note that for the + and * operations in the equations above, we will use the custom adder, and multiplier (and modulo) defined in the previous section.

In our Circom implementation, rather than using cartesian coordinates, we use the radix format as defined in the reference implementation (given here). This changes the polynomials a bit, but the core logic is the same. Please see the code here.

Scalar multiplication on the curve is essentially repeated point addition, hence it was easily implemented using the above circuit. Finally, we needed a Circom implementation for SHA512. We were able to modify the existing SHA256 implementation from the Circom library to achieve this.

Using the above as building blocks, we achieved a working implementation for Ed25519 signature verification, with the following performance parameters —

All metrics were measured on a 16-core 3.0GHz, 32G RAM machine (AWS c5a.4xlarge instance).

Next Steps

Since the largest power of tau ceremony available is 256 mn constraints, we can fit a max of 99 signatures in a single SNARK. However, validator sets could contain 1000’s if not 100s of 1000s of validators, and hence there is a need to scale this.

We are currently working on STARK based implementations and exploring the use of recursive proofs to achieve logarithmic scaling of proof generation time. We are also working with hardware acceleration companies for reduce proof generation time.