zkStudyClub: Supernova (Srinath Setty - MS Research)

20 Apr 2023 · 1:07:25

Microsoft Research's Srinath Setty presents SuperNova, a recursive proof system for producing succinct zero-knowledge proofs of program execution on stateful machines like the EVM or RISC-V, on this zkStudyClub session. He explains how SuperNova builds on the Nova proving system and its folding schemes to support a rich instruction set without raising per-step proving costs, formalizing the approach as non-uniform incrementally verifiable computation.

Speakers

Topics

Transcript

Hello everyone and welcome back to this iteration of ZK study club. This time we're very excited to welcome Sreeram N. Reddy who's actually presented on here before, but he's presenting some new work which has generated a bit of buzz in the ZK industry around folding schemes specifically Nova and Supernova. And so really excited to have him here to present this work and apparently there's some even newer work on the same theme that we can look forward to here shortly, but with that Sreeram would you like to share a little bit about this work and what you're doing with Supernova and Nova?

Thanks. Thanks Alex. It's great to be back here. I'm super excited to talk about this work. It's called Nova Supernova. This is joint work with Abhiram Kothapalli from CMU and Yana Tiago who used to be at NYU and now she's at Google. So this talk is going to be about these two papers that are linked. One of them appeared at Crypto last year and another one was posted on ePrint a few months ago. So so let me start with this simple question. So what is Supernova? Supernova is a proof system. So there's a prover verifier. The prover sends a proof.

So what's different is it targets what we call semi-structured computations. So there is some computation that I'm going to get into more details on what this means, but there's some input. The circuit itself can be decomposed into multiple pieces and then finally a an output comes out. So it targets these kinds of computations. And this might look strange, but it this kind of pattern actually applies to many applications that I think people care about like proving EVM executions or CPU executions like risk five or web assembly other things that you might not think about like ZKML, ZK bridge, photo proof, or even PDF. All

of these fit into this pattern. I'll I'll talk about more later in the slide how it fits. But there are a lot of applications that can be made to work in this model. Another So, the two high-level takeaways that I want to highlight here about Supernova, which is that the Supernova prover, because it sort of targets this kind of computations, its prover is actually cheaper than using a general ZK-Snark prover to prove such computations. The other aspect is that the Supernova's prover's per-step cost is actually proportional to the size of the circuit that's actually executed executed the the instruction that's actually executed. Let's say your virtual machine

has like tens of instructions, and at each step it only executes one instruction, and the cost of the prover is actually proportional only to what's executed. It does not really depend on what else is supported. Like, for example, if your instruction set has add, mul, maybe Keccak, when an add is executed, it doesn't really pay for the cost of Keccak. We call this a la carte cost profile. I'll talk about this more later. Another aspect that I want to highlight in this slide is this Supernova is built on what is called a folding scheme. So, just to give an intuition on what a folding scheme is, suppose you have two circuits that sort of have the same structure, and they're

executed on different inputs. Now, this folding scheme is going to combine both of those. Like, instead of proving both circuit satisfiability instances, they're sort of combined into one folded instance, and this folding is going to be inexpensive. So, you can do this as many times as you want before you actually prove this folded instance. That's where all of these savings in the prover's cost is coming from. So, I'll talk more about all these different things throughout the talk. And and maybe I can just interrupt. I saw I you said you were okay with interrupting questions, so I'll be I'll provide the first interrupting question. Can you describe I mean maybe just for the context for both the audience but also

for the viewers of this you know when it gets recorded at this scheme like I think some folks may have heard of incrementally verifiable computation IBC. Like how would you do you think this is a a type of IBC or how do you compare this to IBC in general? Yes. as contextualizing. Yes. Yes, I'll talk more about this later, but in a nutshell this folding scheme will be a key ingredient to construct IBC. So we'll we'll talk more about this in a very few slides. Okay, great. I'll let you get to it.

So so the rest of the talk is sort of organized around these two questions. Like whenever the topic of Nova or Supernova comes up, one of the question that people ask is like where is Supernova situated relative to other proof systems? And of course how the Supernova itself works. So first I'm going to answer this. I'm going to spend a few minutes to answer the first question. So to answer the first question I sort of created a framework that depicts all of the works that have appeared in the literature going all the way back to the first succinct argument that was implemented called Pepper.

So I've sort of organized this as an evolution of practical succinct arguments and I've organized this in three stages. And in each of the stages I've depicted works in chronological order like top to top to bottom. And in each of these categories I'm going to highlight one major development that sort of led to the works that are depicted at the bottom of the slide. So in the first category which are all based on linear PCPs and what's now called linear only encodings. Earlier works like Pepper and Ginger sort of required the prover to spend quadratic time in the worst case. So, this changed with the introduction of QAPs, which provided a QAP-based linear

PCP where the prover can be quasi-linear and so which is almost linear time. Similarly, in the second category, all of the earlier works sort of required the verifier to be non-succinct in the worst case because the verifier had to read the description of the circuit itself. Uh so, this changed with the introduction of this technique called computational commitments, which is also sometimes called holography, where uh the verifier only needs a succinct encoding of the circuit itself uh to uh verify. So, this is how uh succinct verification can be achieved in all of these works depicted below.

Similarly, in the third category, all of the earlier works sort of to build a recursive SNARK, they uh started with a SNARK uh and then uh built a recursive SNARK out of it. Uh so, the later works sort of um uh sort of relaxed this requirement where instead of using a SNARK to recurse, you could uh use a uh a SNARK-less recursion or use a folding scheme to construct a recursive SNARK. Uh so, now that I have sort of highlighted one major development in each of these categories, I'm going to about how each of these categories uh evolved over the earlier categories.

So, in the first category, we got the shortest proofs like with uh construction like Groth16. Uh but, it also has a per-circuit trusted setup. Um so, the second category of works sort of got around this uh per-circuit trusted setup with uh so-called universal or even fully untrusted setup. It uh this setup just depends on the type of the polynomial commitment scheme used. And the second category of works can also support uh this notion of customizable circuits. So, it can be used to drive down the cost of a prover.

So, in the third category, what what it provides is it provides the fastest prover for certain kinds of computations, like incremental circuits. I'll talk more about this later. And the other advantage of this third category of succinct arguments is the prover is much more easy to parallelize. And it also gets all of the benefits of the second group. For example, it can have universal setup or untrusted setup, or it can also use customizable circuits.

So, one thing I'll note here is that some of the works that are depicted, they have not appeared in public, but they are in the process. Like, for example, this work called SuperSpartan and SuperNova, they are going to be on ePrint very soon. They are already in the ePrint queue. The other work that is depicted here called a HyperNova, which will be on ePrint soon. I'll talk more about what this work provides. Are there any questions so far? Uh no, I just a comment though. I think this is a great slide. This is a wonderful summary of kind of the work so far in this area. So, thank you for just putting this together.

Yeah, amazing slide. Thank you. All right. So, now let's get into the second question, which is how does SuperNova actually work? So, one one-sentence summary of SuperNova is it's sort of taking Nova and then generalizing it to semi-structured computations or semi-structured circuits. So, I'm going to first So, to explain how SuperNova works, I'm going to sort of go in stages where I'll start with Nova and then eventually generalize it to SuperNova. Uh so, at a very high level, our goal in both Nova and SuperNova is to sort of construct fast ZK-SNARKs for structured

computations. Suppose we have a computation where we can decompose this into multiple steps. So there is a circuit C and it takes some non-deterministic input at each step like I've depicted this with W's and then it the circuit also takes some input. It produces an output which is fed into the next step of the competition so and so on and you keep repeating this competition to get the final output Zn. So this actually as I mentioned earlier this pattern applies and shows up in many practical scenarios. For example in the case of a VDF C would be one or more invocations of some delay function something like

MinRoot that takes non-trivial sequential time to compute. So in the case of a ZKVM the C would be a step of a VM for example EVM or WASM or LLVM or even a CPU like RISC-V. And in the case of the ZK bridge C could validate its state according to some rules of the blockchain. And in case of what's called ZKML C can apply a layer of the model. And in case of photo proof C can apply a particular transformation to the photo for example blurring or resizing.

And in the case of a public key directory like the one that WhatsApp announced recently C could check if the directory the public key directory maintained by the service is up and only in each epoch. That the directory service publishes its state. So there are a couple of things I'll mention which is in the later part I'll generalize this to semi-structured competition where in each step we're not only applying one circuit we can apply one of the possible circuits from a predefined list. And I'm going to depict this competition in a sequential manner but the proof generation does not have to be sequential. In particular, the prover could execute the sequentially first and

then produce the proof in parallel, for example, by using binary tree structure. Now, but for the rest of this talk, I'm going to just ignore all this the the the binary tree optimization and just focus on the sequential proving. So, one naive approach to prove this kind of structured computation, we just unroll this computation, construct a giant circuit that invokes all of the circuits with all the non-deterministic inputs, and it produces one output.

And then we could take that circuit, apply a ZK-SNARK, any ZK-SNARK, uh pick the fastest and prove with it. Uh one downside, obviously, is the prover would have to get memory that's proportional to the number of times the circuit was invoked. Uh it's, in general, harder to parallelize and distribute monolithic ZK-SNARKs. Uh the verified time might also depend on n, depending on the construction. And it obviously does not provide a faster prover than a general ZK-SNARK, because we are applying a ZK-SNARK to the circuit, and it's not leveraging the structure that's present within this unrolled circuit.

Uh so, in 2008, there was an approach provided called incrementally verifiable computation. So, this comes back to the question that Alex was asking earlier, where instead of actually proving this computation in one shot, we are going to do this in multiple steps. And in each step, we're not going to prove just the invocation of C, but we're going to prove an invocation of an augmented circuit. So, in particular, there is a circuit C, and we're going to put a verifier inside the circuit. And at each step, the prover Yeah, I don't quite follow, so I was a So then Sorry Justin, were you

you aiming for a question? You want me to repeat anything? No, I'm so sorry about this. Please ignore what I said. I'm I will mute myself. All right, cool. No worries. I can tell you're asking a question now. Welcome though. Yeah, go ahead, keep rolling for now. All right. So, so at each step the verifier would take a proof that was produced from the prior step and it would verify this proof. And then it would pass and it applies an execution of C and then pass an output to the next step. Uh, and in 2019, so so obviously like maybe before I say this 2019 work, obviously the one downside of this approach is like it encode the SNARK verifier in entirety inside the circuit which can have

overheads. Also in 2019, this work called Halo provided an improved approach where you don't need to encode the full SNARK verifier. In particular, you can defer certain expensive steps in the SNARK verification by using this notion of accumulation where in addition to this proof, there is this accumulator that I've depicted here with UIs, U0, U1 and so on. So each step takes not only the proof from the prior step, but it also takes this accumulator. And this V prime, what it's going to do is it verifies part of the proof and then it updates the accumulator. And in the end,

we get a proof and this accumulator and then eventual verifier has to verify both of those. And this actually led to major developments like for example, we could now use SNARKs without trusted setup. Previously, we had to rely on SNARKs with trusted setup because of those were the ones which had a succinct verifier. Now this approach allows us to use a SNARK without trusted setup that might not have even have a succinct verifier. Daira, SNARKs is correct to jump in here a question. So, this was I think this was pop- I mean, I know you you mentioned some of the earlier work, but I think it was popularized Is it correct to say this was popularized by Halo? Like this concept of like the the Halo um IBC system where you're recursively

proving a single statement. Go ahead, Daira. I think you wanted to say something. It was invented by by us uh for the original version of Halo. Yes. Cool. I think the B actually, I guess this is maybe an important point to to point out is the B is Bow, right? Daira, I believe these are all These are Bows. Uh yeah. Um Sean Bow, uh me, and Jack Grigg for the original paper. Yes. Yeah. Cool. Well, uh so awesome. It's great to have you here, so uh and contribute to the discussion. But yeah, I just wanted to clarify that for for some folks in the audience just who maybe are unfamiliar with the acronyms, but would maybe know these schemes as they are often referred to in industry. So, it's not really a question. I just wanted to highlight that for uh folks in the audience. Sorry

to uh Yeah, I I've also noted the name of the system um Cool. So, uh so this this made a lot of progress, but I think there are still some downsides or uh rather opportunities for improvement. Uh so, one downside for uh doing this type of construction is uh it sort of necessarily requires producing a SNARK for each invocation of the circuit. Uh so, we can't really hope for a faster prover uh than the SNARK prover that was used.

And the verifier circuit can still be substantially large, for example, like on the order of 2 to the 18 multiplication gates, uh which can have large recursion overheads for certain applications. So, what uh Nova provides is it provides a new approach to realizing IVC. So, it avoids SNARKs and even uh non-succinct arguments of knowledge. So, one way to summarize the key results of Nova is probably it shows that if you have what is called a non-interactive folding scheme, you get an IVC.

And we also show that there exists a public coin one-round folding scheme for all of NP. And because it's public coin, we can make it non-interactive in the random oracle model, and then heuristically instantiate this non-interactive version in the plain model. So, in the construction, what we achieve is the the prover cost is now substantially cheaper than with a general SNARK. For example, it only requires two MSMs of size proportional to the circuit instead of like 22 or so, and other FFTs in case of Plonk. And the proof size there's one downside to this construction, which is the proof sizes are linear in the size of the circuit.

I'll show you later how we can use a general ZK-SNARK to compress those proofs. And if this compression is done infrequently, the cost of the prover can be kept I guess minimal. So, so the building block that we're going to use is called a folding scheme. So, here is the high-level description, where suppose the prover and the verifier have some circuit C, and they have two claims that they want to check. For example, some witness W1 and some public IO X1.

And if the circuit is evaluated on these things, it's it's going to output one, so that's one claim. And there's a similar claim for the second witness W2 and X2. And our goal is to compress this into one claim about W and X. And I'm going to describe what this folding scheme at a high level is and what these requirements are. So, the prover takes this witness and public IO for both of the original instances as input and it's supposed to output this um new witness and new public IO. And the verifier only takes the instance, which is the two public IOs, and it's supposed to output X. And one thing I will just note here is like there are a lot of other inputs that the prover and the verifier are going to

take, things like public key, proving key, and the verification key. I've sort of simplified that uh for the sake of keeping it simple. Uh so, at a very high level, uh there are some requirements this folding scheme should satisfy. Uh suppose if the the original instances are satisfiable, we require that the output instance is also satisfiable. Uh knowledge soundness says that the the if if uh this output instance if the prover knows an output instance for uh this folded instance, then it must actually know uh the witnesses for the original instances.

Uh succinct means the verifier's work uh is cheaper than uh is concretely cheaper than uh the checking one instance. Like the the cost of participating in this should be cheaper than checking the instance itself. Uh finally, zero knowledge says uh the interaction does not reveal anything about the input instances and the output instance, anything beyond what uh the verifier already can see. So uh so before I actually describe Nova's folding scheme, I'll I'll note that if you had a ZK-SNARK, you could trivially build a folding scheme. So, here is how we can do it.

Uh so, the prover has two instances to prove. So, what it does is it proves one of them one of the instances uh by sending a proof. And then the verifier verifies that SNARK and then sets this folded instance to be the second instance. And then the prover sets the folded witness to the second witness. And you can show that uh it actually satisfies all of the properties that that I just said. Uh but uh our goal is to actually devise a folding scheme without using snarks or even non-succinct arguments of knowledge.

I can see that there's a question in the chat. Yeah, sorry about that. I I was I was trying to avoid continually interrupting you with questions, so I directed it at Dara, but I'll say it for everybody. I was just trying to clarify here for just to distinguish between different types of systems. Would it be fair to say that a ZK-snark folding scheme Is Halo an example of a ZK-snark folding scheme? Uh in that class. Uh yeah, so so retrospectively, yes.

Um at the time it wasn't um described exactly that way, but um I I guess the the terminology has changed a little bit uh and been generalized mainly by um uh BCMS 20. Uh so BCMS 20 was the um the the terminology of accumulation schemes, and then I can't remember which paper introduced folding schemes. Maybe you know Suranga? Oh, the Nova the Nova paper. Nova paper, okay. Cool. Yeah, and I I don't mean to muddy the waters, but I do think it's helpful sometimes there's like, you know, similar-sounding terms folding and accumulation. Sometimes it's worth pulling those apart for the audience and making sure we understand like where the differences are, where the similarities are to the extent they're distinguished.

So anyway, I um didn't mean to interrupt your flow, but thank you for clarifying, Dara and Suranga. Thanks. So So our goal is to construct this kind of folding scheme without uh using snarks or even a simpler version of snarks that may not be succinct uh called narks. Uh so I'm going to uh so so the way Nova constructs folding schemes is it starts with R1CS, which was uh implicit in the construction of GGPR13. So here the circuit description is provided by these uh three matrices Uh and the public input is X. A witness is satisfying if for Z, which is a concatenation of the

witness, public IO, and a constant one, this matrix relationship holds where AZ * BZ = CZ, where the circle is the Hadamard product, entry-wise product between vectors. Um so, one thing that I want to sort of uh say here before I sort of continue with R1CS, there is some folklore or opinion in the community which is this R1CS arises over. This may or may not be true, but the one thing I want to say is um uh even though I'm going to describe um uh Nova for R1CS, there are variants of Nova like Sangria, which sometimes is also called Plonk Nova. It shows how Nova can easily generalize to degree-2

Plonkish. So, there is this other work that's actually in sitting in the ePrint queue, where we introduce something we call customizable constraint system. One of the key aspects of the CCS is it simultaneously generalizes R1CS, Plonkish, and Air, and it does so without actually paying any overheads. Uh and another work that's upcoming is called HyperNova that generalizes Nova to CCS, and then it also can capture Plonkish.

Uh so, for the rest of this talk, I'm sort of going to live with R1CS and leave the generalization to these later works. Any questions? Uh nope. I think there's no questions, so we can keep rolling. This is great. Thank you, Srinath. Thank you. Uh so, so now let me try to motivate the exact scheme that Nova uses to fold R1CS instances. So, let's uh start with this R1CS instance where the prover has the two witnesses and the verifier has these ABC matrices that describe the circuit and and the also takes us input the public IO X1 and X2.

And suppose we uh just do a the usual trick that often shows up in uh succinct arguments, which is the verifier sends a challenge to the prover. And now we just take a random linear combination of things. For example, we take X1 uh and then add with r * X2. And we do the same with the W, W1 + r * W2. And we set this to be the folded instance and witness respectively. And then the prover just outputs the witness and the verifier just outputs this uh instance X.

Unfortunately, this does not quite work. Uh the reason is the uh uh as I'm going to show you now. So, even if we just um uh uh take the Z1 is r * Z2. Uh this let's take this right-hand side, which is CZ. Uh so, this expands to this um AZ1 * BZ1 + r * AZ2 * BZ2. And then we take the LHS and then we expand it out. Uh we get a bunch of cross terms and also a some coefficients like r squared, which don't show up on the LHS.

So, uh so, what this means is like uh even if the original instances were satisfying uh for almost all values of r, the LHS is not going to be equal to the RHS. So, it's uh uh so, it's not going to satisfy even completeness that we uh want from the folding scheme. So, the way we are going to fix this is uh we introduce a small variant of R1CS that we call relaxed R1CS. And there are two differences here. One is uh it multiplies the CZ with a coefficient that I have denoted here by U. And then it also has this an extra term called E that's added after CZ. And the the goal of this extra error term is to capture

all those cross terms that show up on the LHS. And the goal of this U is to capture this R squared term that showed up. It showed up on one side but it did not show up on the other side. So this the goal of U is to capture that R squared term. Hey, so can I ask you a question here? Um So in general if if you allow E to be arbitrary then this is always going to hold for some E, right? So um So E has to be constrained in some way.

I I guess you're going to cover that now. Yes. Yes. Yes. So it's Yes, it is true that uh for uh if you don't constrain E uh it always holds for any constraint system but in our actual construction uh we're going to constrain that uh the steps uh that are representing the computation will have E set to zero and U should be set to one. Uh but we'll I'll talk about this later. Okay. Yeah. Um So this relaxed R1CS one thing to note here is that it uh sort of generalizes R1CS by uh for example, you can take any R1CS, set U to one and then E to zero, you get a relaxed R1CS. And the other direction also holds but it's a little more

complicated. So you just have to combine this uh CZ with E and you can recover an R1CS out of it. Uh so uh so now we have this relaxed R1CS. So let's try to build a folding scheme for relaxed R1CS. Uh so um so as before the prover takes two witnesses. The now the verifier takes this error term as well as the scalar that I introduced. Uh now we uh have the prover sends this cross term uh that shows up uh along with the extra terms involving use.

Uh so, the prover sends this. Now, the verifier sends the challenge after receiving this message from the prover. Now, the uh the the verifier takes the weighted combination of use Xs and then it uses uh the cross term that was sent by the prover uh to compute this new error term E. Uh similarly, the prover would uh use the random challenge to fold the witness that was uh that it holds. Now, the verifier and the prover output um the folded witness and the folded instance.

Yeah. And this it's important that E and U are part of the public input um rather than the witness. Yeah. Yes. Yes. Yes. Uh for now, yes. That's one of the issues that I will fix now. Uh so, there are actually like as uh Daira pointed out, E is actually in the witness uh in the instance rather than in the witness. This is actually not so good. Uh actually, let me uh talk about that first. So, the the problem with that is like this E is as big as the constraint system. Like in particular, it's as big as the number of constraints.

Uh so, the verifier is not really successful because it's taking the weighted combination of this uh E vectors. Um so, there is another problem that shows up while writing uh writing a security proof, which is the verifier can't really enforce that the prover is folding its witnesses correctly. Uh it doesn't show it doesn't show up in completeness, but it shows up in the knowledge soundness proof uh Turns out we can address both of these problems simultaneously. Uh in particular, the solution is to uh use homomorphic commitments uh where uh the instance contains commitments to these error vectors and the witness vectors. And now, we take this error vector that was part of the instance, we put it inside the witness.

And I've depicted all these commitments with this overline characters. So the verifier now holds only homomorphic commitments to the error vectors and the witnesses. So now the the protocol proceeds as before except that instead of sending the vector T, it would send a commitment to T. And the verifier sends challenge as before and now the verifier instead of folding the vectors, it's going to fold the two commitments that it holds.

And it can do so because this commitment scheme we're going to assume it's going to provide this additive homomorphism or something like Pedersen commitment. And the prover is now in charge of folding both the W as well as using the cross term and the original error vectors. Now the prover outputs the new witnesses and the verifier outputs the new instance. Um And we can show that this satisfies both completeness as well as knowledge soundness. It's also succinct because the verifier's work is only folding these commitments.

All right. So now that we have this folding scheme, so we are going to use this to construct IBC. So the approach is actually very similar to how Halo works except we have this verifier instead of running a SNARK verifier, it's going to run the folding scheme's verifier. And instead of taking this accumulator, it's going to take an a running instance. So it's going to take this U0 which is a running instance. And at each step, so it's going to take another proof.

It's going to take a instance that represents the last step of the computation. So if you look at this input to the second step, so there is Z1 which is the output of the first step. And And is a little U1 which is an instance that represents the last step. And then there is the capital U one which is the running instance. And what each step outputs is an updated running instance. So it takes the incoming instance, folds it into the running instance, and outputs the updated instance. So the U here is different from the U before that was added for the the relaxed R1CS. Yeah, yeah, sorry. I think it's the old one. No problem. Yes. Only 26 passes. Yes.

Uh so the verifier, as I said, it's the verifier in the non-interactive. So we obviously like we can't use the interactive folding scheme's verifier. So we have to make it non-interactive before we can recurse. So the V here is the verifier in the non-interactive folding scheme. And now because it's only doing this folding, we can have the lowest recursion overhead. For example, the verifier circuit size is only like 10,000 R1CS gates. Uh and this UI is a commitment to the witness of the previous step. Uh and this capital UI is a commitment to the running witness and the running error term.

Uh and the recursive proof turns out as a combination of these two things. So it's the the the last step's commitment along with the running commitment plus the corresponding witnesses. So that's the recursive proof which is linear in the size of the step. Uh so so the so there are two so there are two components. One is the last step's instance and then there's the running instance and witness. Uh obviously this is linear in size. So what Nova does is it folds two into one by just applying one more invocation of the folding scheme. So we get just get one instance and one witness.

But obviously this is going to give some reduction like a factor two, but the proof sizes are still linear in the size of the step. Uh so naively what we could do is we could use a journal which is not to prove the knowledge of the satisfying U and W. And this can be used to get additional succinctness and zero knowledge. But it can be expensive because it's this is zero noise now it's going to prove some statements about commitments which may or may not have native representations. So what Nova does is it's going to look at this proof and then what it does is it treats these commitments like to vectors as commitments to multilinear polynomials.

So once we do this treatment what we can do is you can use a snark based on multilinear polynomials. In particular Nova uses Spartan to prove that this R1CS relationship holds on those committed polynomials. And what this provides is the proof size goes from linear number of field elements to a logarithmic number of group elements. This is an exponential improvement in proof size. Of course one may use other proof systems like Plonk or Marlin as long as you can sort of treat these commitments to vectors as commitments to some polynomials and then you can use those proof system directly.

And in particular using these proof systems might reduce the proof sizes further like for example you might get a constant number of group elements but the prover time may be more than what we had in Nova. So uh just a minute quick question here is do we even need to go to sort of PIOP style model here because I mean for example would it not be possible to use like a modification of the bulletproofs um arithmetic circuit proof system directly in the sense that we really are just proving sort of matrix vector multiplications right and then a Hadamard product. Um Yeah yeah yeah yeah actually that's a good question. I think um uh for the case where we only have, for

example, there are no pairings uh and we just started using some cycles. Um I think you'll get um uh similar um asymptotics like the log proof size, linear verification time just by using Bulletproofs. Uh but there is uh other settings. I think this going through this polynomial IOP we still have some advantages. For example, let's say at least one of the curves has pairings like I think there are many constructions like for example, there are some constructions that are has created. There are also, I guess, BN254 Groth16. There are other constructions of these curve cycles where at least one of them has the uh pairing then Yeah, they're half pairing cycles. Yes. Yeah.

Yes. You can use that to get uh even better verification times. Uh Yeah. Yeah. Yeah. Yeah, I was talking about the sort of uh uh the no pairing pairing-free cycle uh setting. So, in that setting, I think you could get better performance than Spartan because anyway you're paying like a linear verification time, so you don't actually care about holography. So, you wouldn't need to do like the matrix um arithmetization step. Yeah. Yes. Yes. Yes. But I think keeping this polynomial IOP route sort of opens up to other commitment schemes. For example, I think um uh uh uh half pairing cycles. And even I think if you're okay with some non-native arithmetic, you could do something like Dory

uh and get log verification. Sure. Good question. Thanks. Uh so uh so now that I've talked about this uh how Nova works and how it compresses these proofs, uh now let's look at how to prove machine executions, things like EVM or RISC-V or CPUs or more like uh uh what what I call semi-structured computations. Uh, so one approach would be uh, we could take the C and we encode a step of the VM and uh, this uh, C should be able to execute any of the supported instructions.

Uh, for example, it can execute add, mul, or Keccak, load, store, ECD, EdDSA, like all the uh, opcodes that are supported by this machine. Uh, so one downside at this at this point is like the size of the circuit is at least proportional to the sum of the sizes of these individual instructions. Uh, for example, you might need a circuit for Keccak, you need a separate circuit for mul, and the C is going to be at least of that size. Uh, so as a result, the prover's cost, even if you use Nova, which has the lowest prover cost, it's going to be proportional to the uh, at least of the crypto operations at each step.

Uh, so what this does is it forces the circuit C to be as minimal as possible. Like we can't really go for a a uh, a widely used virtual machine like EVM. We have to design a small VM that's maybe minimal instructions. Uh, so it's not really a solution because if you want to execute a real-world program, you'll have to execute tons of iterations of this minimal C. Uh, so what uh, what we introduce in this in the work Supernova is that uh, we define something we call non-uniform IVC where we have a collection of uh functions non-deterministic functions, which we denote with C1 through CL, and think of them as circuits encoding uh, different

instructions. And we also have this special uh, function called phi, uh, which is going to help us pick one of the instructions to execute. So there's an initial input as before, Z0, and the goal is to prove that Zn is the output after applying these uh, uh, different circuits. Like at each step, we're going to use phi to uh pick the circuit we want to execute. For example, at step zero, we compute phi on W0Z0. We get an index. So, phi is mapping from these witnesses and inputs to some index uh between 1 and L. So, we're going to apply that circuit, get an output, feed it to the next step. So, at each step,

uh uh there is a selection of which circuit to execute. And uh also, this is the model Sorry, this is the the non-uniform IVC model. And uh uh we can think of Nova as providing this NIVC, but only for a single instruction. So, before I uh sort of talk about how Supernova works, I'm going to uh get deeper into how Nova applies to the single instruction model. Uh so, I I I in the in the previous slides, I mentioned there is an augmented circuit. There is some C concatenated with the verifier verifier circuit. So, I've sort of just elaborated what's going on inside that circuit.

So, it takes two things, the little UI, capital UI, and it feeds it into this non-interactive folding scheme's verifier, which outputs a new running instance, UI + 1. So, what this little UI is really a claim about the prior step, and this capital UI is a claim about all the prior steps. And then, this UI + 1 is a claim about all of the prior steps plus uh uh the little UI combined. Uh so, this is exactly what happens uh at a particular step in Nova, and we can think of this as NIVC uh applied to one single instruction.

There's only one C. So, now, what Supernova does, this might look a little complicated, so I'm going to walk through. Uh so, what Supernova does is it it does exactly what Nova did, except it's going to change the verifier circuit. So, in particular uh uh it instead of a single C, we're going to index that with some what we call program counter. And at each step, the C PCI + 1 is going to be different. It's going to be It's going to be picked from this phi. So, we have this some computation that's executed. Think of that as the computation associated with the instruction.

Then there's phi inside the circuit. And then there is, as before, uh this non-interactive folding scheme. Um So, what this non-interactive folding scheme does is it takes a collection of running instances. So, there are now more than one capital I's. It applies a multiplexer. So, it picks just one of them. It so happens to pick just the the PCI provided from the last step. So, it picks one of the running instances. It picks the claim from the previous step. And it folds it into that picked running instance. And then it updates only one of those running instances.

So, So, at this stage, the the instances have to be chosen in advance so that the set of possible um uh instructions in this case has to be chosen in advance cuz your your your claims is at the size of them is proportional to the um the number of instructions. Yeah, yeah, that's a good question. So, I think um in the simplest version, I think we can think of it as being chosen like for example, the instruction set is fixed. Uh we have a well-defined, I guess, maybe some canonical ordering of these running instances. And you're going to update it based on that.

Uh but in practice, what's going to happen is um So, we're not going to have the circuit read all of the running instances because that's going to be expensive. It's going to be like if you have 100 instructions, this now the circuit has to read 100 instances, but it's going to update only one of them. So, that's not very useful. So, what we are going to do is one of the optimizations that we describe in the paper is it's it's it's somewhat standard where instead of taking all the instances, we are going to put them in a a verifiable memory. Think of it as a Merkle tree, but there are other structures like multi-sets. Uh and at each step, we are going to read only one of them.

And then write back uh whatever was updated. So, in this model, it turns out you can sort of uh uh support uh uh I guess instructions that may not have been fixed. For example, you encounter a new instruction, you can put it in some new location in the Merkle tree, for example. Uh so, it it sort of follows you to uh add new instructions. Yeah, so so so all you need to do basically is have some rules for how the Merkle tree can be updated. Yeah. So, so that could support things like smart contracts um for instance, adding a new contract. Yes. Yes.

Yeah, so so this is exactly what I was going to say. We don't have to really read all the instances. We just read what's necessary and update it um uh by applying this folding scheme. Thank you. Thanks. Um so, before I sort of summarize this talk, I'll uh I'll just note that there is actually a way to build this kind of VMs without using recursive ZK-SNARK. In particular, one of the early works called BRAM, what it does is it takes a non-recursive ZK-SNARK. And in the case of a non-recursive ZK-SNARK, it turns out you can sort of trim these universal circuits. So, so you don't really have to execute all the instructions uh that the machine supports at each step. So, I I sort of depicted these

three columns where there's recursive ZK-SNARK like Nova, Halo 2, uh and you run with universal circuit. Then there's uh ZK-SNARKs with trim circuits. Uh and then there's Supernova. And I've sort of picked these four characteristics to compare these three categories of works. Uh, sorry, what what do you mean by a trimmed circuit here? Yeah, like for example, I think here, let's say we have some virtual machine that has some instructions. Turns out when you execute, it only invokes some of them.

Uh, and instead of using a universal circuit, uh, you can just sort of pick the circuit that was actually executed, and you can build a a circuit only of the executed instructions. Think of it as just a constant. And it it works if you're not using recursive SNARKs, anyway. Uh, so uh, so the recursive SNARKs with universal circuit obviously don't satisfy this cost profile, the al la carte cost profile, which means pay only for what you execute. Uh, whereas this ZK SNARK with trimmed circuits can satisfy that, because they only pay for what what's executed.

Supernova, turns out even though it's using a recursive ZK SNARK, sorry, I think uh, my animation is a little messed up. Let me go through this. Uh, so so Supernova, even though it's using a recursive SNARK, it can get this al la carte cost profile. Uh, and incremental proof generation, obviously the recursive SNARKs can provide it, a non-recursive SNARK does not. Zero knowledge, turns out it's a little tricky in this case of VRAM, because it reveals the number of instructions of each type that's executed, whereas with recursive SNARKs and also Supernova, it's easy to get zero knowledge.

Uh finally one maybe disadvantage of recursive ZK SNARKs is there is some recursion overhead. Uh, and there are also some primitives that may not be as efficient. For example, one prime example might be memory. For example, if you have to use memory, we have to either use a Merkle tree or a multi-set based hash function. Both of this results in like at least few hundred constraints per memory operation whereas in the non-recursive smart context you can use permutation networks or other fingerprinting approaches that has much lower cost to access memory.

But one thing that I'll just note here is that this sort of recursive overhead can be mitigated if each instruction is doing at least some work. One ballpark number that I'll throw here is a if each instruction is doing at least 10,000 gates of work then this recursion overhead I think is not an issue. Are there any So so in in the case of simulating memory um So so you can do cheap memory operations within one of these um instructions um but then

so suppose you have a fully random access memory and you you don't know what part of the memory um each instruction is accessing do you still have to pay the overhead of the um the Merkle tree uh operations between steps? Oh yeah, that's a good question. So what what we can do is um we can still get the ala carte cost. What I mean by this is let's say at a particular step I want to access memory. I could have an instruction that's doing this memory load uh and it's going to pay for that memory Merkle tree or multi-set based whatever memory that we use only for that memory access. Let's say the next step is not accessing memory. It's not going to pay for that cost. We can sort of

move all of this work into a separate instruction that's executed only when needed. I I guess I guess another thing you can do is that you you can kind of have a cache memory that's used within each step and then only the the higher level cache that gets um uh updated between steps. Yeah, yeah. That's a good point. Um Srinath, um so in the separate memory instruction uh case this doesn't quite work if you have say like a one moment architecture, right?

Where you have to do a memory load to fetch the instruction you're actually executing at that time step. Right? Um if you have the sort of Harvard style architecture, then sort of you hard coded the program so you know exactly what instruction you're going to execute next but this is not quite the case for um one moment style architectures, right? Yeah, yeah, yeah. That that's a good point. Yes, yes. I think if you're going to anyway read uh an instruction from memory and that might be self-modifying, yes, yes. I think you do need to load at each step.

Uh I agree. D- D- Don't do that because you you won't be able to audit or um prove anything about that kind of program anyway. I mean even if you don't have self-modifying like uh Yeah. Yeah. Yeah. program section of memory is not uh catchable or whatever, right? There's uh read only. Even then you still have to read to read from memory, right? Yeah, yeah. I think I think the best might be for the read-only memory case, I think the best might be to use the multi-set hash function because uh anyway you're going to read all of the program at least uh at each step you just use this multi-set hash-based memory where I think you pay only like few hundred constraints. Yeah, I mean

maybe the program size is small enough that you can uh fit it like within these 10,000 gates cheaply. Yes, yes. Um al- also another question. So, I guess uh you can generalize this Supernova idea to work um with other recursive SNARK constructions too, right? Essentially like you have a hash of all of the verification keys that you would want to uh uh for for each instruction for example, right? And then you you pick out from your your Merkel tree which which VK you would like to verify at this time step and then um uh yeah, you verify proof with respect to that VK only, right? So it is um

they I guess you can describe it at a level of abstraction maybe above folding schemes. Yeah, yeah, actually that's a good point. I think yeah, you could sort of treat this recursive snark or even a snark itself as a black box and then all of this selection of instructions and what verification key is being used, folded, running instance, all these things are picked at a layer above. I think you're totally right. One I guess downside of doing that might be the concrete overhead because now you might be doing all this folding at the layer above as well as the layer below. By sort of doing both together, you get some concrete improvements maybe at least a

factor two. Yeah, good point. Conceptually it may be easier to think about them as two separate things. Mhm. All right. So so in summary, Supernova is a new proof system with a fast prover and it also provides small proofs. It provides this a la carte gas profile where you pay only for what's executed. It introduces new techniques such as folding schemes. It also leverages best-in-class techniques like the linear time subjects through Spartan.

Nova is fully implemented. It's available. It's being used by several projects. And Supernova offers a new substrate for building proof-based trustless services and it I think it has many advantages over the alternatives. Uh finally, there is some upcoming work, uh, that allows proving customizable constraint systems, uh, in the style of Nova. Uh, with that, uh, I will conclude and happy to take more questions. Uh, and it's an MIT license that implementation. Yes. It It uses, uh, Pasta curves, uh, uh, Okay.

I I didn't realize it was there in the Thanks. Um, awesome. I don't think your co-authors ended up joining, Sruthi, at least I did not see them. Um, so I guess we can skip introducing them, but obviously thank you for presenting and thank you to all three of you for this work. Uh, do we have any questions from the group? Feel free to chime in or just write in the chat and I'll read it. I am quite curious about this new, uh, constraint system which generalizes R1CS and and Plonkish. Is there a an easy way to describe that in in a small amount of time, I guess?

Yeah, so I think, uh, like for example, if you look at R1CS, it takes this AZ time Hadamard with BC equals CZ. Uh, so what this, uh, you can sort of think of it as, uh, hardcoded with three matrices ABC. Uh, and it's picking two of them in the Hadamard product and then one of them, uh, to be the linear term. So what the CCS does is it allows you to, uh, basically sort of specify how many matrices you have and how each of those matrices are picked in different terms.

So, uh, you immediately get R1CS as a special case because you just have three matrices, you pick them in the, uh, special order. Uh, and then the generalization to Plonkish is uh so Plonkish applies, say, multivariate polynomial for each row of the constraint. So you can emulate the same thing by picking these matrices in a certain way and also the uh the multi-sets that sort of describe which matrices are picked in each term.

So, you can think of um uh R1CS being a special degree two equation, whereas the CCS being a a multivariate polynomial constraint. Uh but we don't need to go into the level of polynomials. We can still work just like in R1CS uh where everything is described in terms of matrix operations and Hadamard products. Um uh turns out one of the uh outcomes of uh sort of defining it this way was if you had a a a SNARK for R1CS, for example, Marlin or Spartan that were designed for R1CS, they almost very easily generalize to handle CCS.

Uh and then uh by the extension, they can also handle Plonkish. Uh so, this uh sort of decoupling the the constraint system from the proof system itself sort of uh I think made it easier to show these techniques apply to different proof systems so very easily. Yeah, there's there's there's currently an effort to standardize um Plonkish as an arithmetization. Uh and I'm just thinking it might be um a good idea to make sure that we we have a mapping of that to um CCS as it can be said.

Um Yeah, it seems feasible. Yes. Yes, so in the paper that's currently sitting on the ePrint queue we have we have a definition of CCS and also reductions. Happy to hear comments from folks working in the space. Uh I think it's online soon. Yeah, that sounds cool. Is there a rough idea that sort of you generalize the Hadamard product to be like a multi-product instead of a, um, you know, ZA times ZB equals ZC? Yes, yes, exactly. So, we we, in addition to this, allowing any number of matrices, we also ask you to specify some multi-sets. These multi-sets are supposed to describe how different matrices are sort of,

combined with the Hadamard product. Mhm. Uh, and then, I think, uh, the the the SNARK design sort of comes out of the out of this definition very easily. It is You know, all of these SNARKs, you sort of prove this, uh, what is called the RO check, and it automatically generalizes to this more general form. Yeah, exactly. The linear check, as before. So, so, the So, this generalizes to I want CS. Um, it has the same properties as I want CS, where you can have, um, linear combinations that, um, sort of a a very cheap, um, even if it's a large number of terms. Yes, yes, exactly. I think, uh,

it, um, it it it it has the exact same, uh, cost model. I guess, all of the behavior as R1CS. At each step, you sort of multiplying not just the variables, you're multiplying these linear combinations. Uh, Yeah, but I think, uh, for Marlin and and Spartan, also, like, the linear combinations are not exactly free, in that you pay for like the density of the, constraint matrices, right? In the proving step. But, as if you look at Groth16 the proof, like, the prover operation, the cryptographic operations scale only with the number of constraints, right?

Yeah, yeah, actually, that's a good point. I think, uh, uh, in the polynomial IOP, I guess, in my picture, the slide that had the three categories, I think the first, comes out also the last category, can have costs that don't depend on the number of non-zero entries in these matrices. For the commitments, yeah. Yeah, like, even the uh, the recursive stuff, they can don't have to pay for the uh, the non-zero entries. For the the ones at the time of compression obviously you have to pay and in the second category the non-recursive non-zero to pay for this the universal ones. They pay for the non-zero entries, so Yeah. Yeah, I I mean even in Plonk in some sense you're actually paying for

that like addition gates are not free same way. Yeah. Yeah, we we found that in practice um the additions are not that much of a constraint because the the things that you could do using the um sort of endless free additions in R1CS um you can do with running some gates and um things like that but um that you you can kind of do them in parallel with other operations that you were doing anyway.

Um but yeah, if if if there's a model that um So there's even if you do have to pay for non zero entries in the matrix um which I I think you have to do in all universal Mhm. uh systems then the simplicity of R1CS as a as an arith- arithmetization so that the fact for example that you have completely independent constraints, you don't have the complexities of um layouts that you have in um uh Plonk with um custom gates then um and then combining that with the

the ability to have polynomial polynomials of higher degree and that that is quite attractive. Yeah. Yeah, I think one of one of the at least for one of the things we hope that the CCS is I think you can maybe mix Plonk-ish with R1CS because it's it's defined in a unified manner. I think it may allow such mixing when appropriate uh And Srinath, I think you mentioned that uh CCS also generalizes AIR. And I guess these are the three like main competing arithmetizations. Uh I want CCS, plank and AIR.

I guess my question is, is there some like commonly used arithmetization which CCS does not capture naturally? Yeah, that that's a good question. So, yeah, it's I don't know. I think um Yeah, so far Yeah, I guess um it seems like it can capture all these three, but it it's not clear I guess if there is something else that it does not capture. It it would capture in the sense it's general enough you can transform, but the question is is there overhead to doing it um uh So, for these three we showed there's no overhead really to uh do it.

For something else, I think you should always be able to transform except there may be overhead depending on how it's specified. I have a question about or Do you want to continue that line? Yeah, carry on. Okay, I have a question about how you see the Well, turn my camera on, I guess. Um how you see the horizon with respect to AIR stuff. I think for the most part systems that use AIR are also using FRI, but this folding approach depends on additive homomorphic encryption scheme or commitment scheme. You mentioned Pedersen commitments as an option, but I was curious what you see as sort of the

the horizon in systems that are using AIR FRI arguments and looking at folding. Is that something you've talked about much? Yeah, I think that's a that's a question, but I I don't have I don't have anything concrete to add except that um um I think uh in those schemes that don't rely on the selected curves, I guess you can gain from using the smaller fields uh and so on and so forth. I think that's how a lot of the schemes sort of get better provers performance there. Uh but obviously as you said there is no homomorphism to exploit two folding schemes there. So I yeah, I think I don't know what what might happen now.

Well well, we we haven't mentioned lattice space schemes. So um I think that you you could get um both uh homomorphic commitments and um uh post-quantum security potentially. Um Yes. Yeah, yeah, that's a good point. I think I think yeah, people have mentioned this lattice commitments but I think there hasn't been I guess uh a concrete proposal or at least I haven't seen a an implementation or something that shows it's possible.

So Yeah, you have to figure how to deal with the errors that arise from lattice space stuff and also I guess in some sense you need like a cycle of lattices, whatever that might mean. Um for this to actually work out. Um Yes. Yeah, although yeah, actually I don't know if the cycle is crucial because it might be able to do non-native stuff because if it's small enough it might not be expensive. Yeah, so yeah, if you if you can do lookups um uh and it if you have um sort of uh polynomial constraints of some sort of small degree greater than two, so say four or five, then you can definitely do

lookups. Um so if you can do that then the the non-native arithmetic isn't necessarily that expensive. Um it's it's still more expensive than cycles of curves. Yeah. Srinath, you mentioned that CCS generalizes uh Plonkish with with no overhead. What what is the definition of of overhead in that in that context? Yes. Yeah, it's a good question. So, I think um uh there are I guess two ways to look at it. One is um if you go take the constraint system, transform into CCS, like what's the size of the witness,

what's the size of the number of constraints that you have to use. And I think one way a one rough way to capture this might be what's the running time of the NP checker in the old representation and in this new representation. Turns out the witness size does not grow, the public IO size does not grow, the number of constraints does not grow. The NP checker time does not grow. That's how we said uh uh the the two does not have overheads, but I think there is one more layer. We could look at the snot for Plonkish and the snot for CCS after the transformation, and we see what's the prover time. I think we haven't really done the second one yet.

Uh but I think that might also be more useful in practice. Uh but we have done the first one where we look at the witness sizes and uh the NP checker time. NP checker is just looking at the witness and the constraint system and checking if it's satisfiable. Okay, that makes sense. Thank you. Final call for questions for Srinath.

Okay, great. I think we can end it here. Thank you everyone for attending and thank you very much Srinath for presenting today. This is uh really good and there's some really great slides in here, too. By the way, if you have these if you're willing to share these slides, we'd love to uh link them to the uh to the video link or in the video description we post the video if that's okay. Of course, I'm happy to send them. Thanks. Thank you so much for all the questions and inviting me here. All right. Thanks everyone very much. Thanks.