Recursive SNARKs: A Comprehensive Primer
Recently, there have been a number of exciting results concerning proof recursion. A sketch for Halo has suggested the possibility of proof recursion without a costly trusted setup, while Fractal has demonstrated the first instantiation of proof composition which is post-quantum secure. We’ll go into these results later after discussion what proof composition is, the technical challenges associated with achieving it, and how it ties into commonly used proof systems as Groth 16 and Bulletproofs.
There are a number of use cases for recursive composition. One of the most well-known at the moment is that of Coda, a fully-succinct blockchain protocol allowing clients to validate the entire chain by checking a small cryptographic proof in the tens of kilobytes. Recursive proofs have also been proposed for other blockchain scaling solutions, such as recursively proving validity of Bitcoin’s proof of work consensus algorithm, and on Celo using bounded recursion to efficiently verify aggregated signatures for mobile clients.
A use case outside of the blockchain space concerns proving legitimacy of photographs. You could, for example, prove that an original photograph was modified only with crop and rotation operations. Each update of the photo would require one additional layer of proof recursion, updating
This post has two intentions; to serve as an introduction to recursive proof composition and the technical challenges which arise in achieving it, and also as a crash-course in the computational model most commonly used for zero-knowledge proofs; that of arithmetic circuits. As we will see, the first goal cannot be realized without the second. The challenges involved in constructing recursive proofs involve many fundamental aspects of circuit construction encountered in practice, such as the connection between the choice of elliptic curve and arithmetic circuit used, in addition to the impact of the structure of a circuit’s input and the use of hash functions. While we will be giving a theoretical exposition, every piece of it will be relevant in practice for the engineering of general-purpose zero-knowledge proofs.
As such, this post is suitable for anyone who either has worked with ZKPs before and wants to know how recursive proofs work, or for anyone wanting to learn at an introductory level how arbitrary ZKPs are engineered in practice given an existing proof system.
Most of the discussion will be at a relatively high and intuitive level; it is assumed only that the reader has a basic familiarity with zero-knowledge proof systems, group theory, and computational complexity up to understanding the class of problems known as NP.
We also alternate between additive and multiplicative notation where each is most intuitive, sacrificing consistency for the sake of clear exposition. Multiplicative notation
We will begin with a brief review of proof systems and arithmetic circuits.
General-Purpose Proof Systems
A zero-knowledge proof system consists of a prover
NP is the class of “efficiently” verifiable problems, or of problems which can be verified in polynomial time. In other words,
We will again abuse terminology in this post by referring to
Given the symmetry of our two definitions of verifiers above, we might guess that proof systems are particularly useful for NP relations. This is in fact true, particularly since we can construct them for NP-complete problems. An NP-complete problem is one which is in NP and for which any NP problem can be reduced to it. In practice this means that is it efficiently verifiable and that we can both in theory and in software build a compiler which reduces any NP problem to it.
As a brief example, 3-colorability is NP-complete, and we can build zero-knowledge proof systems for it. In theory we could build a compiler such that for any program in our specified format expressing an NP relation, we can compile it down to an equivalent problem expressed in terms of 3-colorability. In practice this would be very inefficient.
We would like a more natural computational model for proof systems. We can think of modern computer architecture as being based on performing bit operations. This raises a question; what fundamental operations would we like our new model based on some NP-complete problem to use? Much of modern public-key cryptography including proof systems uses elliptic curve groups, or points
There is a crucial point to understand here. Suppose we have an elliptic curve
where also
Given that we want to express our inputs in the field
The NP-complete problem we want to target for our proof system is thus arithmetic circuit satisfiability. Intuitively we can think of this as an NP-relation
Earlier we mentioned compiling NP problems down to our single NP-complete problem so thart we can use a single proof system for any NP relation. But there is a very subtle point here which can be a bit confusing. Let
Bit Operations
We will continue by outlining a proof that arithmetic circuit satisfiability is NP-complete, and in doing so will uncover some practical considerations when constructing arithmetic circuits in practice; these will be particularly relevant later when discussing a technical difficulty involving hashing inside of a circuit in our recursive proofs construction.
Recall that to show a problem is NP-complete, we can simply reduce another NP-complete problem down to it. This implies we can reduce any problem in NP down to the one we are considering.
Boolean circuits, while less practical for general-purpose zero-knowledge proofs, are more widely studied in computational complexity theory than their arithmetic counterparts. They are like arithmetic circuits described above, except that each gate computes one of boolean operations AND, OR or NOT on its inputs (or some equivalent set of operations; using only NAND is equally expressive). In fact, the canonical example of an NP-complete problem, 3-SAT or satisfaction of boolean formulas with clauses of at most size 3, can easily be reduced to boolean circuit satisfiability. Simply make each variable an input to the circuit, and each operation in the formula a gate.
To reduce boolean circuit satisfiability to arithmetic circuit satisfiability is slightly harder but still fairly simple. Every boolean operation can be effectively simulated by field element operations. In particular, suppose we want to “unpack” a field element
in addition to checking that
This is assuming we do not care about the summation on the left being larger than the modulus, which we would in practice. This check would take just over another n constraints.
To simulate AND for two
Notice that we have performed here a sleight of hand. We have not explicitly constructed a circuit but rather a list of constraints which may be expressed in circuit form. In fact, many modern proof systems use directly so-called “R1CS” or Rank-1 Constraint Systems such as the one shown above, both in theory and in software compilers meant for users to encode NP relations. R1CS is another NP-complete problem similar in form to arithmetic circuit satisfiability as only operations over a fixed field are used. Systems such at Groth16 take the additional intermediate step of compiling the R1CS down to what is known as a Quadratic Arithmetic Program, or QAP, an NP-complete problem having to do with the satisfaction of certain kinds of polynomials. Still other systems such as the newer PLONK or Sonic eschew R1CS altogether in favor of using the satisfaction of other certain kinds of polynomials for their schemes. This justifies the use of arithmetic circuit satisfiability both here and in the literature as an abstraction that subsumes all constraint systems used in practice, as the simplest and most intuitive way of thinking about the computation of any NP problem using only field additions and multiplications.
We’ve effectively shown that arithmetic circuit satisfiability is NP-complete by reducing boolean circuit satisfiability down to it. But how well can we perform boolean operations inside arithmetic circuits in practice? Many useful algorithms operate on bit values. In the current most well-known and used proof systems such as Groth16 and Bulletproofs, addition gates are “free” while multiplication gates cost 1. In fact, the secret inputs to Bulletproofs
Throughout this post we will make use of SNARKs in which the prover’s memory and time complexity both increase linearly or worse with the cost or number of multiplication gates in our circuit. This can make very large circuits painful to work with.
The asymmetry above between field operations and bit operations means that while
Proof Recursion
Recall that in a general purpose proof system, a prover creates a proof
In the simplest case our recursive proofs will prove a relation
How could we do this? First we would build a circuit
In practice this raises several questions. What exactly does the input to our circuit look like? Does our choice of elliptic curve, and equivalently our choice of field the circuit is defined over, matter? How does the verifier encoded in our circuit know what NP-relation
A preprocessing SNARK
To determine what we will want our input
where each iteration of
A bit more precisely, we can say that we have a list of input tuples
What do the inputs to a PCD look like? We will allow our notation here to become slightly confused in order to agree with the literature, noting where our PCD notation is analogous to the notation used earlier in our discussion of proof systems.
After the proving and verification keys
The verifier
Above we have a diagram illustrating the PCD construction when generating proof
We are now able to give a preliminary answer to what our public input
There is one extension that can be made to the above PCD scheme. We have been discussing an inductive chain of proofs, and will continue to assume we are working in the case for most of the rest of this post. However, we can also extend
On top of this discussion we should be careful to emphasize that as far as we are concerned for proof recursion there is no additional “special” machinery specific to constructing PCDs; it is simply an abstraction used to define what it is to perform computations securely in a trustless and distributed manner. For our purposes here it is less an object in its own right and more of a rigorous outline of what we hope to achieve in practice through recursive proofs.
Cycles of Elliptic Curves
We will now discuss the most important practical constraint encountered when working to achieve proof composition; the choice of elliptic curve used to instantiate our system. The most efficient and useful SNARKs use pairings in their construction. To make use of them we will need to choose a pairing-friendly curve. This requirement significantly constrains our choices of elliptic curves. And in fact, we will need not one but two.
Recall that we want to choose an elliptic curve
The obvious solution is to choose some curve such that
There is, fortunately, a better option. The intuition is that we want to construct two circuits so that we can cycle back and forth between them, getting the verifier and circuit arithmetic to always be over the same field.
Suppose we have two elliptic curves
How can we use two circuits to acheive one layer of proof recursion? Suppose circuit
Because the proof
- If
, set , else - If
check that accepts - Check that
accepts
- Check that
accepts
Recall that we want to use two elliptic curves
The MNT Curve Cycles
We will first explain an important property for the security of pairing-friendly elliptic curves, that of a curve’s embedding degree. A pairing function
where
where
This might seem complicated, but in fact we obtain all distinct
The fundamental problem in elliptic curve cryptography is the discrete logarithm problem. Given
Using a curve with an efficient pairing function introduces a new potential security flaw. While we can use it to efficiently map curve points to
This means that we want both
This brings us to some unfortunate news; the only curve cycles found so far are instantiations of the so-called MNT curves. It can be shown that each MNT4 curve of embedding degree 4 has a corresponding MNT6 curve of degree 6. Worse, security reduces to the weaker curve, here MNT4. This means we need a relatively large base field to achieve acceptable levels of security, at nearly 800 bits.
This is not a hopeless situation; several techniques so far have been proposed to get around this limitation. In addition, it is still possible that a better cycle of curves can be found. However, several impossibility results have been found, suggesting that this will be difficult. We will close this section by listing some of them, to give a sense of what the current siutation is like.
- Any cycle of MNT curves must alternate between embedding degrees 4 and 6
- Cycles using curves of non-prime order do not exist
- Cycles using Barreto-Naehrig or Freeman curves, which are known to be of prime order, do not exist
In particular, it is at least possible that useful cycles will be possible for new constructions of prime-order curves, or that they can be constructed using a combination of MNT, BN, and Freeman curves in one cycle together.
Shortening the Message Length
There is a critical problem with the above circuit designs. An arithmetic circuit
Since our design has two verifier keys
We can then pass in
- Check that
- If
, set , else - If
check that accepts - Check that
accepts
- Check that
accepts
There is one more optimization we can perform to reduce the cost of hashing. We may want to do this because hashing has been known to be particularly expensive inside of arithmetic circuits. Because symmetric cryptography does not require exploiting algebraic structure to the degree that public key schemes do, crytographers have been free to develop cryptographic hashes using the most efficient operations possible on a typical modern computer architecture. This involves many bit operations. However, we established earlier that bit operations inside of an arithmetic circuit are very expensive.
Recently several algebraic hashes have been developed using field operations for use inside of arithmetic circuits. They use dramatically fewer constraints than conventional hashes as SHA256. However, they have yet to undergo sufficient cryptanalysis for us to be virtually guaranteed of their security. While very promising, we will not consider them in this post.
Shortening the Message Length: Redeux
Given that we want to reduce the size of hashing inside of the circuit, we must reduce the size of the verification key. As described above, we can do this by reducing the size of the public input
- Check that
- If
, set , else - If
check that accepts - Check that
accepts
- Check that
accepts
Extractor Size
There is one last theoretical issue to cover. Using a “proof of knowledge” suggests that the prover must know the witness in order to generate a proof which convinces the verifier. We can prove formally that this is the case, by demonstrating there exists some polynomial size extractor algorithm
How can we prove extractability for recursive proofs? Suppose we are dealing with the simple inductive case, where we have
Proving extractability of the
This is fine if we know in advance how many steps of recursion we will use. We know that even the
To keep the guarantee of soundness, we can bound in advance the number of steps of recursion we perform. Above we mentioned that our PCD scheme can also be modified to work for vectors of proof inputs. Instead of performing recursion in a linear inductive fashion, we can instead perform it on trees of proofs.
One option would be to construct a binary tree of proofs with a bounded depth
Another option is to simply ignore the issue, as so far this is only theoretical and no concrete attacks have been demonstrated. Intuitively it feels as though soundness of even unbounded recursion should reduce to soundness of the underlying proof system. Caveat emptor.
Recent Results and Future Work
Note that in developing a scheme for recursive composition we have devised a technique for producing a single proof for an NP relation in which the components of the relation are performed by circuits paramaterized by different cryptographic primitives, here elliptic curves. We might ask if this can be generalized, and the answer is yes.
One such generalization has triggered interest in generating a lollipop of curves. We have already observed that the MNT curves are inefficient, but so far are necessary for pairing-friendly recursive composition. We can partly solve this issue by introducing a third and more efficient “stick” curve connected to the two cycle curves. The majority of computation is done in the stick, with a proof fed into the main cycle curve along with the
We may not even be interested in recursive composition at all, but rather in composition of restricted depth. Instead of using a cycle of curves, here we want to create a chain of curves. In the case of a 2-chain, we want curves
Another possible technique would be to eliminate the use of elliptic curves altogether in the proof system used. This is the approach taken by Fractal, by developing and using a proof system which is instantiated only with a field
Finally, Halo is a recently developed proof system which aims to improve the efficiency of recursion by using elliptic curve cycles which do not leverage pairings, in a manner which also eliminates having a trusted setup by using a non-preprocessing proof system. This is similar to Bulletproofs, in that the lack of setup prevents us from creating a succinct cryptographic description of our circuit. We are rather guaranteed that the verifier will need to read in the entire circuit, with a linear verificaiton runtime of
Resources and Further Reading
Alessandro Chiesa’s original work on Proof Carrying Data is the basis for the above construction.
The bulk of theory for recursive composition of proofs can be found in Recursive Composition and Bootstrapping for SNARKs and Proof-Carrying Data by Nir Bitansky, Ran Canetti, Alessandro Chiesa, and Eran Tromer.
The first implementation of recursive proofs was achieved in Scalable Zero Knowledge via Cycles of Elliptic Curves by Eli Ben-Sasson, Alessandro Chiesa, Eran Tromer, and Madars Virza. The majority of the exposition in this post was adapted from this paper, which is well-worth reading for additional depth.
The impossibility results for cycles of elliptic curves were taken from On cycles of pairing-friendly elliptic curves by Alessandro Chiesa, Lynn Chua, and Matthew Weidner.
Thanks
I am at least mildly indebted to Alessandro Chiesa for discussions about proof system reductions, and Dev Ojha for help understanding Fractal. I am also grateful to Eli Ben-Sasson and Ariel Gabizon for clarifications regarding STARKs on twitter.
I would also like to thank Kobi Gurkan, Georgios Konstantopoulos, and Alan Flores-Lopez for comments and critical feedback.