zkSummit: Overview of recursive SNARKs - Michael Straka (cLabs)

Transcript

Hi, Michael Straka. I do applied cryptography with C labs working on Celo and put together a small video giving a basic overview and introduction to recursive proof composition. Including their applications, how can we use and also the basics of how it's constructed. So, hope it's useful.

Let's get started. So, in this talk we're going to be covering recursive proof composition. In particular, I'm going to talk about some applications, why you might want to use them and also how they're constructed. So, there's a lot to cover, so we'll just dive right in. First of all, let's recall what a proof is in a proof system or argument system. Which is where soundness is come only holds versus computationally bounded adversaries. You have a prover and a verifier. Prover takes in some public input X which the verifier has also

and also a private input or witness W which the verifier does not have and if it's a zero knowledge proof will not will not learn. There's also going to be some extractor algorithm which if a malicious prover convinces the verifier can extract W. So, we know that the prover knows W. Prover is going to send a proof pi to the verifier attesting that XW here is a satisfying input to some arithmetic circuit C such that XW are part of some NP relation R.

The basics I'm assuming most of you know that already, so we can just skip ahead to the more interesting stuff. So, the main abstraction that recursive proofs use is known as proof carrying data created by Alessandro Chiesa in his PhD thesis appropriately titled proof carrying data. And the basic idea is that you're doing some distributed computation.

At each node in this computation you're going to have some data say Z2 and a proof string say pi 2. And this proof pi 2 is going to attest to the fact that Z2 was created according to some function specified by a compliance predicate big pi. And this big pi is going to take in Z2 the claimed output some local data Z local I which was specific to this node, so no one else necessarily

sees it or needs to see it. And also a vector of input data. Here just Z1. So, one application that you could imagine doing with this is uh say Bitcoin. At each node you're just past say Z1 that would be the previous data in the blockchain and Z2 would be a new block and you're just verifying that proof of work holds.

Or you could imagine there's a paper called photo proof that constructs a system using this abstraction where at each step you just verify that uh you get a photo that is either a crop or a rotation of a previous photo. Right, so you're just enforcing that there's some invariant that holds at each step. And uh basically the reason why you can do this is uh so in a normal snark you have some extractor algorithm that extracts the prover's input assuming the prover can convince the verifier. So, if you have a

malicious prover that convinces your verifier you'll always be able to extract a valid witness from that prover. And here what we can basically do is encode the previous proof say pi 1 as a witness to a snark and then that will allow us to uh given pi 2 and Z2 extract pi 1 in addition to Z1.

Sorry, we won't extract Z1. We'll just get Z1 as input. Right? So, given Z1, Z2 and pi 2 we can extract pi 1. So, we can extract a valid proof that Z1 is compliant and then we can go backwards in the graph right and all the way to extracting pi 0. So, in some sense what we can do is just extract the entire graph of computation given just uh so the the output node. So, in order to do this we can simply compose proofs recursively. So, what

what exactly do I mean when I say that? Well, really just means you have some proof say prover sends this verifier pi 0 a proof attesting that X0 and W0 are valid and then this verifier sends another prover should be the same algorithm. We'll see later on how they can these two can both be the same, but it's basically because we can just encode in our arithmetic circuit some bit flag that differentiates between the base case here and the sort of more general case that handles recursive proofs.

And basically the uh this prover here at the bottom it's going to take in as part of its witness the previous proof like we were just saying and it's going to use this to produce another proof pi 1 which will attest to both the uh validity of W1 prime here which can be valid in the same way that W0 was here. Uh it's you think of it as being approved by the same subcircuit in our arithmetic circuit and then also pi 0 which is going to be uh just going to be checked with the

snark verification algorithm inside of an arithmetic circuit itself. So, pi 1 here attests also to the validity of pi 0. And then we can just uh given the correct construction we can sort of compose these indefinitely. There's actually a technicality that prevents abstraction or extraction for unbounded recursion, but uh we'll gloss over that for now. Uh so if we take go back to uh the PCDs and how one instance of that would look it's basically

the prover is going to take in some local data some input the previous input uh some say proving key specific to the prover and some verifier key. The verifier takes in some verification key and then Z here is going to be the claimed output that both the prover and verifier need access to. And the prover is going to send the a new proof generated at the nth step.

So, say we're doing it's kind of an an inductive case where we just take in one proof at a time and we generate so we take in proof pi I and just generate proof pi I plus 1. So, here proof P would just take in pi sort of n minus 1 and then generate pi n and send that to the verifier. So, how might we actually do instantiate recursion with an arithmetic circuit? Well, like I was saying what we could just do is uh have an arithmetic circuit part of which

would check some compliance predicate pi. So, that if we have a input a X is a public input and then some witness with part of which is previous proof W prime here would be checked by the compliance predicate. And then pi here would just be checked by CV, which is actually just a verification algorithm of the snark encoded in an arithmetic circuit.

Right, so we can actually decompose that pretty nicely, but there's a problem here and that is that we're going to have So we're going to want to instantiate a snark with an elliptic curve. Let's say it's E over F P. So this just means the elliptic curve E instantiated using the base field F P. So the finite field of order P that it has P elements. So this this is actually a problem because

if we look at the order, the size of the elliptic curve, this is going to have Q points. But uh for certain technical reasons, Q will not be equal to P. So this means that the our arithmetic circuit uh just like the gates So this is uh

it is just uh computes arithmetic addition or multiplication in F P. And this is going to be it using F Q arithmetic, uh what's known as the scalar field, which is the same order as the curve itself because if you do uh I apologize for using multiplicative notation. Uh So mhm You know, please don't lock me away, but uh if you do computations with the elliptic curve,

uh they're going to look something like this where you're actually doing uh sorry. You're actually doing computations in the exponent of the curve elements and this is going to be effectively in the field F Q. So but uh when we do elliptic curve operations itself, they're actually going to reduce down to computations in this base field of P. So uh you're basically going to be able to to be trying to do when you do the snark verification algorithm encoded in the circuit, you're going to try to do F P arithmetic in a circuit uh defined over the finite field F Q. And this is a problem because

it uh you're going to end up need to do a lot of modulus operations, which will reduce the kind of bits that uh you you bit bitwise operations are very expensive in arithmetic circuits, so this is going to be really expensive. The blow up is going to be logarithmic in the size of your base field, it's going to be really bad. So you don't want to do this. What you really want to do is uh you want to be able to define a cycle of elliptic curves.

Say E over F P and uh E 1 over F uh it's going to get confusing. E Q over F P and then E P over F uh F Q where uh say the order of this curve is P, the order of this curve is Q and they're the size of each each other's base fields. Right so why why do we want to do this? Well, we can actually compose these these two curves in in the following manner. So instead of having one arithmetic circuit, we can have two such that one circuit

uh on the left is going to do our compliance predicate as we were discussing earlier. Uh the other subcircuit will be the uh snark verification algorithm. Uh note we have V Q and V V R here, that's because uh we're basically going to to have two instantiations of the snark, one for each elliptic curve. All right, so that's uh you we're going to have one for per arithmetic circuit. Uh and then each circuit is So the circuit defined over F R is going to need to use

the the verifier for the elliptic curve of order Q because it's base field will be of order R. So it's actually you can do that base field arithmetic in C R. Right? So basically each circuit needs it the other snark's verification code embedded in it. Uh and then once you compute the sort of main proof here that verifies the compliance predicate or attests to the correct satisfaction of the compliance predicate, you send it to the next circuit, which is sort of a wrapper circuit. And then that one is simply going to verify that this proof is correct and then generate a new proof that it is.

And in this manner, you can sort of achieve a consistent you can ensure that the the proofs you generate are all verifiable by the same uh kind of snark algorithm. Uh right, you just kind of use this circuit to convert the arithmetic back to the the form that you want. Uh so if we look at how this the actual sort of implementation of this uh we could do in pseudocode. Uh and this actually isn't quite quite what you would want because you'd actually need to reduce the uh public input.

Right, the public input here would need to be smaller so that the verification key would uh would be small enough cuz the verification key is going to get bigger the larger the public input is because that's going to blow up the size of uh of the you know, the input that the verifier needs to take in. Uh so you can do that with a pretty simple hashing trick. I'm not going to go into it, but uh um it's something you need to take care of. Uh Basically in the concrete implementation uh it's just what I was discussing except you also need some like base field bit flag to ensure that you can deal with

the base case effectively cuz you're not going to need to activate a V Q here. Right? There's no previous proof to verify. Uh So that's actually how you would instantiate fully recursive snarks. Mhm, but there's some bad news. Mhm, let me find it. Okay, the bad news is here. So basically uh the the the current instantiation of cycles of elliptic curves we have are known as the MNT curves. Uh ironically, they're some of the first elliptic curves considered for you know, cryptographic applications and they're also the only ones we found to use a bull sort of pairing friendly cycles, a cycle where both curves are pairing friendly.

And if you're using in both circuits, you're using a pairing friendly snark, then you need both elliptic curves to be pairing friendly. Right that's that's just how it is. Uh but unfortunately, the embedding degrees for both of these curves are very low. Uh we'll get to why that's important in a second. Uh and you know, there's some other restrictions that don't look too good. You can read them here. I'm not I'm not going to go into them either. Uh These were also from a paper by uh Chiesa and some friends. So Mhm, it's not clear how likely it is that we'll find something else that's workable in the near future. Uh

so there are a few ways people have proposed getting around this, but basically the problem is that uh in a pairing algorithm, which is you know, in some sense the reason you would want to use it is because it gives you this nice structure in the form of bilinearity, which is shown here. Right? If you have E X to the A Y to the B, that's going to equal E X Y to the A times B. Uh so that's a very nice property to have that lets you design nice mhm argument systems. Uh But uh it's also it's not just a constructive technique, it can also be used to form attacks in the sense that most pairings are instantiated with two

mhm uh subgroups of the R torsion uh group of the elliptic curve. Uh if you don't know what that means, don't worry about it. It's you can just think of these two as subgroups of the elliptic curve for now. Uh but they map onto uh here a finite field for the multiplicative group of a finite field. All right, it's just the field restricted to multiplication operations and that's going to be of order uh right.

It is Q to the R or more more standard would be a Q to the K where K is your embedding degree and Q is the size of your base field. So, the higher your embed So, you can use this to translate the discrete logarithm in elliptic curves to the discrete logarithm in infinite fields. Uh so, the larger this this field is, the more security you're going to have in the finite field discrete log problem. Uh so, to get more security there, you either need a larger base field or a larger embedding degree. And since the embedding degrees here are so low, we need larger base fields. And that can make things quite inefficient in SNARK-land. Uh your prover is going to

get pretty slow uh at least relative to what it could be if you use the smaller base field. So, uh it's not a great situation. There are some ways of getting around this if you only need finite depth recursion, you can use what's called the Cox-Zuckerman method to uh generate uh sort of uh chains of elliptic curves so that you can't compose them back and forth indefinitely, but you can kind of compose one into the other and then stop. So, you do like depth two or depth three recursion and then stop there. Uh although the base field doubles in size roughly every time you do that, so it does get very slow if you keep doing it indefinitely,

but your first curve is going to be a lot faster. Uh we're So, um Yeah, there's another thing that's interesting is that if you uh if you look back at this diagram, you don't actually need to instantiate both circuits with the same argument system. So, one thing that's been proposed uh so, this specifically by a a GitHub post by some people at Zcash is you could use for the circuit on the left something like Groth16 or Marlin that uses R1CS.

And uh just sort of um you know, just a normal SNARK that uses a pairing-friendly curve. And then use on the circuit on the right, you could instantiate that with Halo. Or uh you know, in theory another non- just any argument system that doesn't require pairings. Uh but Halo seems like the best choice right now. Uh you know, the uh the thing that's not so great about Halo is that it's um it's not succinct. There's no like sort of preprocessing generator algorithm that can give you a succinct uh uh sort of helper data in the form of a proving key and verifying key. So, there

you know, the basic intuition is that it's going to need to read in the circuit itself. So, your asymptotics are going to be linear in the size of the circuit at least. Uh but you you can compose that with uh a SNARK to get uh something that in the end does provide some succinctness. Right? Because this proof here is going to be succinct. So, uh and the uh the base fields you get from these sort of half pairing-friendly cycles are going to be about half the size of MNT curves, so it's actually uh they're actually pretty usable. Uh As we're running out of time, uh I'm

going to wrap up here. Uh here these are the main papers that I sort of constructed this presentation from. They're also great resources if you want to learn more. Um We also have a uh you know, project that working on at C Labs that kind of touches on it's a sort of at least finite depth recursion. I think Kobe's already talked about that. Uh so, that's also something to look at if you're interested. Um of course, there are also some other great projects doing work with recursive SNARKs like Coda and Zcash. Uh And so, thanks for your time.