The ZK Chronicles: Proof Composition

Last time we met, we upgraded our ZK toolkit with the addition of lookup arguments. They give us the ability to express non-arithmetic constraints in a convenient way, which makes our arithmetizations all the more flexible.

But they can't cover everything, and there's one type of computation in particular that they don't really cater for. You might want to take a breather before reading this one. Ready?

What about a proof of a computation that verifies a proof?What about a proof of a computation that verifies a proof?

Wait, what?

We're straight up inceptioning these things, huh?

Yeah, I know it sounds crazy (and by any reasonable measure, it is), but there's good reason for us to dive into this realm of recursive proofs.

So here's the plan: let me first convince you that this sort of strategy is necessary and actually pretty useful, and then we'll see what we can do about it.

Hang tight. This is gonna be a crazy (fun) one!

Proof Limitations

Throughout the series, we've been thinking about proving systems in isolation. You take some computation, express it as constraints, and generate a (hopefully succinct) proof that everything checks out. And when it works, it's a really powerful idea, no doubt about it.

However, we've been quietly assuming something that might not always be the case: that the computation in question is small enough to fit in one proof.

By this, I don't mean that it's not mathematically feasible to craft a proof for a large computation. Rather, I'm referring to the case where the prover would take so long to generate the proof, that it's practically infeasible for them to do it.

So what happens when we stumble upon a large computation?

Think about a blockchain, for example. At its core, a blockchain is just a long sequence of state transitions: Alice sends Bob some tokens, Bob sends Charlie some tokens, and so on. If you wanted to generate a ZK proof that the entire chain is valid (every single transaction, tracing back to the genesis block), you'd be asking the prover to process, say, hundreds of millions of steps (if not more) in a single circuit.

Needless to say, that circuit would be ginormous, and the proof would take forever to generate, so much so that nobody in their right mind would ever try doing it. Thus, generating such a proof for the verification of the entire history of a blockchain is, at least for now, out of reach.

Of course, verifying block-to-block transitions makes much more sense from a practical standpoint. But you'd be assuming that the previous block is correct, which may or may not be a sensible thing to do, depending on the context.

Hint hint: perhaps it would be better to prove the correct execution of a block, and then somehow attach a proof that the previous block is correct!

Here's another scenario with much the same problem: you're designing a system where you have a thousand users, each generating their own proof of some private computation. The system acts as the verifier, and has to check the proofs generated by all users. Each verification might be fast, sure - but a thousand verifications still take a thousand times as long as a single one. If only we could somehow combine them...

Both examples point in the same direction: we need a way to handle computation that grows over time, or that exists in many parallel pieces, without paying a proportional price in verification cost.

And there's one idea that can solve both of these.

A Proof That Proves a Proof

Ponder this for a moment: just what is the verification step, if not a computation? You know, it takes a proof as input, does some arithmetic, and outputs "yes" or "no."

So then, if verification is nothing more than a computation... can we not prove that we ran it correctly?

Let that sink in for a moment.

What I'm saying is that if we could build a proof system expressive enough to verify another proof as part of its circuit, then we could chain proofs together. The prover kills two birds with a single stone: they prove the current execution step is valid, and that the previous proof was valid at the same time. And the genius of all this is that the verifier only needs to check the latest proof, because it implicitly certifies everything before it is correct!

This is called recursive proof composition. And even if we don't yet know how to do this, we can at least in theory create something truly amazing: computations that are incrementally verifiable. It was such an important development in the field, that it received its own name: Incrementally Verifiable Computation, or IVC.

Let's try to put this into slightly more formal terms. Suppose we have a computation split into $\ell$ steps, each applying some function $F$ to a state $z$:

$$z_1 = F(z_0), \quad z_2 = F(z_1), \quad \ldots, \quad z_{\ell} = F(z_{\ell-1})$$

Similar to the state transition function of STARKs!

IVC lets us produce a proof $\pi_i$ at each step such that:

• $\pi_i$ proves that $z_i = F(z_{i-1})$
• $\pi_i$ also proves that $\pi_{i-1}$ was valid

Therefore, anyone holding $\pi_{\ell}$ can verify the entire chain of $\ell$ steps, in the time it takes to verify a single proof. And the size of the proof stays constant, regardless of how many steps were chained.

The canonical real-world example of this is the Mina Protocol, with its Kimchi proof system. It's a blockchain where the entire history (every block, every transaction, etc.) is represented as a single recursive SNARK. The chain state is always a single proof, fixed at around 22 KB, no matter how old the chain gets. A new block is valid if and only if there's a valid proof certifying both the new transactions and the prior chain proof.

Truly fascinating stuff.

In short, IVC is a type of argument system, similar to what we already saw in inner product arguments and lookup arguments. Where those proved a single, static claim about some private data, IVC proves something about incremental computations. And since the prover accumulates evidence across all steps into one certificate rather than proving each step in isolation, this kind of construction is also called an accumulation scheme.

Mixing and Matching

Before we start looking into how this composition works, I want us to pause on an important detail.

When we say a proof verifies another proof, it's easy to imagine that we're talking about the same proving system all the way down, so for example, a Groth16 proof verifying a Groth16 proof. But nothing actually forces that!

In most cases, we'll have two different systems. One will produce the proof we want to verify, which we'll call the inner system $\mathcal{I}$, and the other wraps around it (to prove the validity of $\mathcal{I}$'s proof), so we'll call it the outer system $\mathcal{O}$.

When we carefully choose these two systems, composition becomes a way to get the best of both worlds.

Here's an example. Suppose our inner system $\mathcal{I}$ is a STARK. STARKs are wonderful for many reasons: they are transparent (no trusted setup), fast to prove, and more. But you know what's their main shortcoming? Their proofs are quite chunky, often ranging in the tens or hundreds of kilobytes.

Which is not ideal in some situations. For instance, if you have to post that proof on a blockchain, where every byte costs you, then this could become a big pain point!

So what do we do? We just wrap it! All we have to do is choose an outer system $\mathcal{O}$ that produces succinct (tiny) proofs, like say Groth16, and have $\mathcal{O}$ prove the statement "I verified this STARK proof, and it checks out".

That's it! The verifier never sees the bulky STARK, and they only ever have to check the lean little SNARK on the outside. We get the STARK's fast, transparent proving on the inside, and the SNARK's lightweight proof on the outside. And for these reasons, this pattern is very common in production systems today.

And succinctness isn't the only thing we can buy with this strategy. Suppose instead our inner system is efficient but not zero-knowledge. We can then pick an outer system that is zero-knowledge, and have it prove "the inner proof is valid" without revealing the inner proof itself. The privacy gets added by the outer wrapper, even though the inner system never had it in the first place!

So the general rule is that each layer can contribute a different property, be it succinctness, transparency, zero knowledge, or anything else - and composition lets us stack the ones we want.

Problems in Paradise

That's the promise, at least. I think we can all agree that the idea itself is worth pursuing.

I suspect you're already wondering though: how do we even begin to build such a thing? Building a circuit that verifies a SNARK sounds... complicated, at the very least.

And you'd be right to wonder. You see, there's a fundamental tension lurking quietly in the shadows here that complicates things quite a bit. It's not immediately clear what the problem is though, so in order to address it, let's try to see what we'd need systematically, and then the problem will reveal itself quite clearly.

First, let's briefly recall how SNARKs work at a high level. When we produce a proof, what we're doing is taking a set of constraints that define the problem, and encoding those as polynomials for which some very specific identities should hold. As we already know, these polynomials are defined over some finite field. Let's denote that field $\mathbb{F}_p$.

Then, in order to work with these polynomials, we usually commit to them, and in some cases (but not all) these commitments live on a different domain, which is that of elliptic curve points. And I don't think I mentioned this back in our passage through groups, but elliptic curves are also defined over another field, usually called its base field. We shall denote it by $\mathbb{F}_q$.

In other words, every point in an elliptic curve group is a pair $(x, y)$ that satisfies the affine equation $E$, but also where $x$ and $y$ live in $\mathbb{F}_q$. In fact, the curve itself is sometimes written as $E(\mathbb{F}_q)$ to make this explicit.

Also, note that $\mathbb{F}_p$ contains the field elements we use for scalar multiplications of group elements (i.e. $g^k$, where $k \in \mathbb{F}_p$). This is why it's often called the curve's scalar field.

If you're curious about the naming and some more context, I recommend you check my Elliptic Curves In-Depth series, and in particular, this article.

The problem, my dear reader, is that $\mathbb{F}_p$ and $\mathbb{F}_q$ are usually not the same field.

That's gonna give us quite the headache here.

You see, if we imagine we want to verify a proof (say, a PLONK proof) inside a circuit, then we need to perform a bunch of elliptic curve operations - you know, point additions, scalar multiplications, and pairing checks. Those operations are natively expressed in $\mathbb{F}_q$, which is the finite field where point coordinates live.

But to create a proof about the verification, we might want to build a circuit, and encode it as polynomial identities. And therein lies the problem: even if we build gates to perform the elliptic curve operations, those gates must live in $\mathbb{F}_p$!

Because of this, we're forced to represent elliptic curve operations sub-optimally, using a similar trick to the one we used for range proofs last time.

We need to decompose each foreign field element into limbs, and manually implement the arithmetic. Which might sound complicated, but it's exactly what happens when you try to represent integer operations on a CPU that only understands binary, which is in itself a finite field!

This decomposition is actually pretty costly, introducing roughly ten to twenty times more constraints than native operations.

So yeah, verifying a SNARK inside a circuit adds quite a lot of overhead. Or, well... a pretty brutal amount, really.

Something had to be done about it.

Completing the Cycle

Okay, but what options do we have?

Well, the easiest solution would of course be to try and match $\mathbb{F}_p$ and $\mathbb{F}_q$. If we could use the same field for both the elliptic curve's base field and the scalar field, then everything would work like clockwork, and we'd be done. The problem with this, however, is that for any given elliptic curve, $\mathbb{F}_p$ and $\mathbb{F}_q$ are always close in size, but never equal. And not by accident: making them equal would compromise the security assumptions the curve is built on. Therefore, we can't just pick a curve where they match, because the math won't allow it.

So what's the next best thing we could do? Well, if validations require computations in $\mathbb{F}_q$... then why don't we simply build those circuits on $\mathbb{F}_q$?

What I mean is the following: suppose we have an initial proof where the original circuit is in $\mathbb{F}_p$. Its verification would require operations in $\mathbb{F}_q$, so what we could do is build a circuit over $\mathbb{F}_q$, and have that be the scalar field of yet another curve, whose base field is yet another $\mathbb{F}_r$!

This way, there's no mismatch at all!

Yet, one little problem remains: we'd need a new curve for each chained verification, and you know, secure elliptic curves are not that abundant.

And that's the final piece of the puzzle: what if we could find only two curves so that their base field and scalar field are interchanged? That is, two curves $E_1$ and $E_2$ such that:

• The scalar field of $E_1$ equals the base field of $E_2$
• The scalar field of $E_2$ equals the base field of $E_1$

A little cycle of elliptic curves of sorts!

That's very promising, because in that case, we could alternate between them! Each curve's verification operations are native arithmetic for the other, so there's no need for decomposition (which was where most of the overhead was sitting), and we can stack as many recursive proofs as we want!

Then again, finding such curves is no small feat. They are rare, and finding secure pairs of them took considerable effort. But people managed to find such instances, with the most famous example of this construction being the Pasta curves, designed by the Zcash team for exactly this purpose.

With these cycles of curves, recursive proofs became not just theoretically possible, but genuinely practical. For the first time, we could actually build a system that verifies itself, one curve at a time, flipping back and forth indefinitely.

And this idea was in fact first practically realized in the Halo protocol, and later Halo2.

Everything is bliss, we're happy, until... we realize there's yet another problem with this approach.

The Cost of Self-Reference

Even if we find a valid cycle of curves, there's a clear elephant in the room we need to address: encoding the verifier inside a circuit still carries overhead. Essentially, every time we want to encode a verification step, we have to pay the full cost of said verification, which translates to an explosion in the size of our circuits, and therefore, in the number of constraints.

This extra cost adds up as we add more and more recursive steps, and it does so pretty fast. If the verification circuit has, say, $V$ gates, and you're chaining $n$ steps, then the prover time is roughly proportional to $n \cdot V$. That's linear in $n$. And if we've learned anything about linear scaling... it's that we'd like to avoid it.

At least this is still better than the naive approach of not using recursion at all! But it's still not great...

Ideally, we'd want to find a way to embed verification so that the incremental cost of each step is small, no matter how many steps came before. So as always, we wonder: can we do better?

You bet we can. However, we'll need a different approach to get there, courtesy of an old acquaintance we've made along the way.

It's time for a second round of folding!

Folding, Revisited

If you recall from back when we worked through Inner Product Arguments, the whole gist of the matter was to methodically reduce a statement about a vector, to a statement about another vector which was half the size.

We called that folding at the time. The point was that we could apply folding over and over, eventually getting to a condition that's trivial to check. All we needed was a verifier challenge on each step, which we used to build a random linear combination, and each step only cost a constant amount of work.

Interesting, right? And you know what? It gets even better when I ask you this: what if we could do something similar not only with vectors, but with entire proofs?

Oh yeah! Folding is a much more flexible idea than what we made it look like a few articles back. The essence really lies in the idea of taking random linear combinations. So the question is:

Could we combine two proofs into a single one?Could we combine two proofs into a single one?

Would be nice, huh?

It's not like there's a magic recipe though, and it took some time before the first methods that exploited this idea materialized into existence.

So let's try to build one such method! How about we apply it to, say, R1CS instances?

A Practical Example

A few articles back, we saw what an R1CS constraint looked like:

$$(\mathcal{A} \cdot \mathbf{w}) \circ (\mathcal{B} \cdot \mathbf{w}) = \mathcal{C} \cdot \mathbf{w}$$

where $\mathbf{w}$ is the witness vector, $\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}$ are public matrices, and $\circ$ is element-wise multiplication. Any satisfying witness $\mathbf{w}$ (or circuit evaluation) should satisfy this equation as well.

Now suppose you have two satisfying witnesses, $\mathbf{w}_1$ and $\mathbf{w}_2$. Could we somehow combine both checks into a single one?

Well, we can take a hint from our folding adventures back in Bulletproofs, and use a random linear combination of both witnesses:

$$\mathbf{w}' = \mathbf{w}_1 + r \cdot \mathbf{w}_2$$

I'll take a wild guess, and say that you're probably wondering if that makes any sense at all. Let's find out! If we substitute that combination in the left-hand side of the constraint:

$$(\mathcal{A} \cdot \mathbf{w}') \circ (\mathcal{B} \cdot \mathbf{w}') = (\mathcal{A}\mathbf{w}_1 + r \cdot \mathcal{A}\mathbf{w}_2) \circ (\mathcal{B}\mathbf{w}_1 + r \cdot \mathcal{B}\mathbf{w}_2)$$

Expanding this product, you get:

$$= (\mathcal{A} \cdot \mathbf{w}_1)(\mathcal{B} \cdot \mathbf{w}_1) + r \cdot \underbrace{\left[(\mathcal{A} \cdot \mathbf{w}_1)(\mathcal{B} \cdot \mathbf{w}_2) + (\mathcal{A}\mathbf{w}_2)(\mathcal{B} \cdot \mathbf{w}_1)\right]}_{\text{cross term } T} + r^2 \cdot (\mathcal{A} \cdot \mathbf{w}_2)(\mathcal{B} \cdot \mathbf{w}_2)$$

Since both $\mathbf{w}_1$ and $\mathbf{w}_2$ originally satisfy R1CS, we can substitute like this:

$$(\mathcal{A} \cdot \mathbf{w}') \circ (\mathcal{B} \cdot \mathbf{w}') = \mathcal{C} \cdot \mathbf{w}_1 + r \cdot T + r^2 \cdot \mathcal{C} \cdot \mathbf{w}_2$$

A little extra manipulation (using the fact that $\mathcal{C} \cdot \mathbf{w}' = \mathcal{C} \cdot \mathbf{w}_1 + r \cdot \mathcal{C} \cdot \mathbf{w}_2$) gets us to a pretty nice form for the above equality (feel free to check the numbers!):

$$(\mathcal{A} \cdot \mathbf{w}') \circ (\mathcal{B} \cdot \mathbf{w}') {-} (\mathcal{C} \cdot \mathbf{w}') = r \cdot T + r(r-1) \cdot \mathcal{C} \cdot \mathbf{w}_2$$

So, we get to something very similar to the R1CS constraint for the combined vector $\mathbf{w}'$, only that... we now have a couple extra terms!

One is purely a set of cross-terms, while the other appears because of the quadratic nature of R1CS.

This is pretty much the same phenomenon we saw with inner product folding: we get to a new instance of the same problem, only that we have to deal with a couple new terms. The only remaining question is how the heck do we do that!

One option is to go the Nova way, which proposes a very clean solution: we work with an extended form of R1CS, that admits an error term from the get-go. So instead of requiring the original equality to hold, we use a relaxed version of the constraint:

$$(\mathcal{A} \cdot \mathbf{w}) \circ (B \cdot \mathbf{w}) = u \cdot \mathcal{C} \cdot \mathbf{w} + E$$

Where $E$ is an error vector, and $u$ is just a scalar.

For a valid witness of the original R1CS system, we have $u = 1$, and $E$ is a vector of zeros, which we can denote $E = 0^n$.

Sure, this is not really the original type of constraint, but it's a constraint system nonetheless - a different one, of course. And notice, if we allow ourselves the luxury of working with this relaxation, then we can take two valid instances of this new problem, with witnesses $(\mathbf{w}_1, u_1, E_1)$ and $(\mathbf{w}_2, u_2, E_2)$, and combine them using some challenge $r$, which gives us:

$$\mathbf{w}' = \mathbf{w}_1 + r \cdot \mathbf{w}_2, \quad u' = u_1 + r \cdot u_2, \quad E' = E_1 + r \cdot T + r^2 \cdot E_2$$

If you do the substitutions carefully now, everything will work out to be:

$$(\mathcal{A} \cdot \mathbf{w}') \circ (B \cdot \mathbf{w}') = u' \cdot \mathcal{C} \cdot \mathbf{w}' + E'$$

Which is a valid relaxed R1CS instance! There's no need to do anything too fancy about the cross terms, since they are already part of the problem!

A small but important note here: the prover commits to the cross term $T$ before seeing the challenge $r$, so they can't choose $T$ after the fact to make the fold work out. This is important to preserve soundness!

And boom! Just like that, we've now folded two (relaxed) R1CS instances into a new one! All that would remain is to prove the relation holds, a single time.

Plus, there's no need to limit ourselves to folding only two instances together. Why stop there? What if we could fold many of these?

Folding All the Way

Getting from two folded instances to many is, as you may already be imagining, quite simple: we just fold one step at a time!

Concretely, Nova represents $F$ as a fixed circuit, since the same matrices $\mathcal{A}$, $\mathcal{B}$, and $\mathcal{C}$ are used at every step. What changes is the witness: each execution of $F$ produces a fresh assignment $\mathbf{w}_i$ to the circuit's wires.

The process goes like this:

• Start with a trivial accumulator: a relaxed R1CS instance with $u = 1$ and $E = \mathbf{0}$.
• Evaluate the circuit for step 1. This produces a fresh standard R1CS instance with witness $\mathbf{w}_1$.
• Treating the fresh instance as a relaxed R1CS instance, fold it into the accumulator, producing a new relaxed R1CS instance.
• Rinse and repeat for all $\ell$ steps.

At the end, you hold a single relaxed R1CS instance (the accumulator) encoding a compressed claim about all $\ell$ executions, and just run one SNARK to prove its validity!

A couple of things worth flagging here. First, the fold is purely algebraic: the instances being combined don't need to share inputs or outputs. Folding doesn't "chain" circuit evaluations - it combines their evidence. The state threading $z_i = F(z_{i-1})$ is enforced inside each circuit evaluation, and the accumulator just carries the running proof that all those evaluations were valid.

Second, only the public part of the wires is ever revealed - as you may remember from our pass through Groth16. The private wire assignments stay hidden behind commitments throughout the entire process.

And with that, we've managed to compress all those R1CS evaluations! How cool is that?

Summary

So there you have it! With $\ell$ folds plus one SNARK proof at the end, we get an incremental cost that's constant per step: each new fold costs roughly the same as running $F$ once, no matter how deep the chain goes!

There are some interesting generalizations of this that cover other arithmetizations, and even allow us to fold different constraint systems together: HyperNova does it by generalizing different arithmetizations into a single unifying framework called a Customizable Constraint System (CCS).

Which is definitely a compelling vision for proof composition: a modular ecosystem of constraint systems that can be combined via folding.

Also worth mentioning, under the hood, CCS instances are folded by recasting their constraints as multilinear extensions, and using sum-check to reduce the folding check to a single evaluation. Bet you weren't expecting that one!

So, yeah... quite the journey, huh? Remember, everything started with us tinkering with the idea of recursive proofs, which got us into a whole mess of cyclic curves, field mismatches, and increasing verification costs.

And while there may be some ways to try and circumvent those costs, changing our plan entirely had a bigger payoff: by folding and accumulating, we could defer all validation to a single step.

With this, we've accumulated (heh) quite a big repertoire. Arbitrary computations, expressive arithmetizations, incremental verification - it really seems like we can do it all!

Plus, and I know we talked about this many moons back, we know any NP statement can be cast into another equivalent NP statement, so we can choose the proving system that better suits our needs!

So naturally, we might wonder: don't we have all the ingredients we need to prove the correct execution of just about any program? You know, not just circuits, but actual code running on an actual (virtual) machine. That would be pretty cool, wouldn't it?

That's exactly the next milestone we'll be exploring in our journey: zkVMs! And let me assure you: it's gonna be an amazing crowning jewel that will put all our accumulated knowledge to the test.

See you there!