zkStudyClub - ProtoStar (Binyi Chen & Benedikt Bünz, Espresso Systems)

14 Jul 2023 · 1:08:01

Zero Knowledge's zkStudyClub features Espresso Systems researchers Benedikt Bunz and Binyi Chen presenting ProtoStar, an accumulation scheme for incrementally verifiable computation that avoids recursive SNARKs. They walk through a generic, efficient folding scheme applicable to a broad class of special-sound protocols, with a prover cost that scales logarithmically in the number of supported circuits.

Speakers

Topics

Transcript

Hello again everyone. Welcome back to another edition of ZK Study Club. This week we're excited to welcome back Ben Yi Chen and Benedict Boons to talk about their recent work ProtoStar on generic efficient IBC schemes. So with that Ben Yi, the floor is yours. Thank you. Thanks Alex and thanks for introduction and thanks to everyone for coming. I'm Ben Yi and today Benedict and I will present ProtoStar which is a new generic but also efficient incrementally verifiable computation scheme. Okay.

Um Wait. So why is it not Okay, it's working. Okay, so let's consider the following problem. Okay, imagine you have initial input V0 and you've done some computation and obtain some output VM. What the computation is somewhat somewhat like iterative computation but in each step you are running some step function given the previous output and some online witness which can be different for each step and finally get this output. So now how could you prove to someone else that an efficiently proving it to someone else that VM is actually the correct output rather than than some garbage values. So more precisely, how could you prove that there do exist some intermediate witness

such that each intermediate execution of step function was done correctly and the finally the output is VM. So the solution to this problem can be quite useful for example in blockchain world because this type of computation actually capture a lot of scenarios. For example, verifiable delay function. Here the step function is just a round function and the number of iterations basically the hardness parameter. And also like succinct blockchain like Mina, well you can understand this intermediate output VI as the ledger state and you can understand this online witness as some transactions coming in the block. And more importantly recently there's a really popular application ZK EVM which is basically proving the

correct execution of a block of EVM transactions. Well, here the step function is a little different, but not much. Basically, it's a a family of functions which consists of multiple opcodes, and at each step you can pick one of the opcode to execute. And given this is really useful and meaningful to study this problem. But interestingly, actually, this kind kind of problem has already been studied long, long time ago, even like around Bitcoin was invented back in 2008. Paul Valiant already introduced this great notion of IVC.

Well, in the scheme, the prover can iteratively generate some small proofs given the previous proof, which we call IVC proof. Here's the pi m here, pi m minus one here, and given this and given also the online witness, you should be able to generate the next IVC proof. And then finally, the verifier only needs to check this final output plus this really tiny IVC proof to ensure or to check that all the previous computation were done correctly. And we require that suppose this intermediate provers are all honest, and they have the right witness.

Intuitively, they should be able to generate correct proof that pass the verified check finally. And this is so-called completeness. And on the other hand, informally and intuitively, if the verifier has passed some past the proof for proof for check for some proof, like pi pi m here, it should be the case that all this possibly malicious prover are actually knowing some valid witness. And intuitively, this is what's so-called knowledge soundness. And more generally, it's not always we don't need to restrict to prove like this kind of chain of computation. We can be more general, like proving like tree of computation, or DAG of computation, or some more general like topology of computations. And this

is called uh proof carrying data or PCD. And but for simplicity in this talk we are focused on IVC, but we know that the techniques in this paper can also be generalized to work for PCD as well. Okay, so it is well known that actually the IVC scheme can be constructed from another really powerful primitive like SNARKs, which is a primitive like enable you to prove the correct execution of some gigantic circuit of computation using some really small proof which can be easily verified. So here the idea is basically a very simple which is like basically a recursive SNARK. With IVC prover will just generate a SNARK proof for the statements that last execution

of the step function was done correctly and the previous IVC proof was verified correctly by the SNARK verifier. So we have to embed the circuit inside this large circuit as well. And this is this is a really neat and simple idea. However, in practice it's not so performance because many because the in this circuit in this recursive circuit the SNARK verification part can be really expensive. It can be really takes a lot of constraint to capture the logic of a SNARK verifier. Moreover, because of the use of SNARK we have to use some like expensive pairing friendly cycles or trusted setup which is also undesirable.

Given this many researchers were exploring the way where there exists another way to construct SNARKs without using SNARKs. Can we do it more efficiently from some other bigger primitives? And one particular popular and promising direction is the so-called split accumulation scheme or folding scheme introduced by BCLMS 20 I've seen published in TCC 20 and also the Nova paper in 2021. And basically the idea is the following. So, given some NP relation, uh, the accumulation scheme or the folding scheme, uh, the the goal is to reduce the task of proving two NP instances into proving a single instance. How to

do that? The idea is that given two instance witness pair, we have some way to merge them together into a single one, so that we only need to check the folded one rather than the one that we had before. More specifically, we have these following algorithms in the scheme. Well, first we have accumulation prover algorithm, which would take sub two instance witness pair, like X1W1 and X2W2. And usually the instance part, the X1 uh, part are usually small, while the witness part can be possibly large. And then taking this as input, the accumulation prover can merge them together and the folded into another instance witness pair, which is XW.

Okay? And then there's another algorithm called accumulation verifier that will check that this uh, folded instance is done correctly, is computed correctly. Basically, it it will take some small input X1X2 and get some meta information from the prover and check that the output uh, folded instance was the correct one. Okay? And the final also I want to mention here is that one highlight here is the accumulation verifier is usually much cheaper than the SNARK verifier, and it can be can use much smaller a circuit to represent this accumulation verifier, which is the key that we can have a much more efficient IVC scheme.

Okay, so after having this having this folded instance with spare, there will be another algorithm called decider that will check that this instance witness pair is inside the relation. Okay, so this is the accumulation scheme and similarly it it needs to satisfy the following requirements. First, that if the original instance X1X2 are satisfiable, it must be the case that folded instance is also satisfiable. On the other hand, if the accumulate uh the prover can generate some witness, some folding witness, uh that pass the final deciding check, it must be the case that he also know the corresponding witness for the original two instances that was folded before. And that's the intuition of

knowledge soundness. Okay, given this, it turns out to be quite easy uh to to generate to build an IVC scheme from accumulation scheme. The general idea, uh this is already explained in the previous paper, but uh the general idea is the following, that the idea is just to iteratively and continuously uh folding some running statements about uh about the folding uh stuff. For the folding statement, first is the last execution of the step function was done correctly. And second is that uh the output accumulator, uh in particular, output accumulator instance was folded correctly. So, after having this proof, it's okay for the IVC prover

to iteratively generate this accumulator from the from some non instances, for example, from some non proofs. And after and then we can So, we ensure that this instance was done correctly given this proof. And and we use this uh accumulation prover to generate the folded instance with pair. And after having that, we can ensure that as long as the final resulting accumulation accumulator is checked correctly by the decider, which will be run the verifier, all the previous computation was will be done correctly. And also, because we have this proof, which has been checked, the uh the accumulator is also the correct one that we needs to be checked.

So, that's the general idea. But, the highlight here is that in this scheme, the IVC prover only needs to generate some non-interactive proof, which might not be succinct for some small circuits because the accumulator verifier's circuit is much smaller than SNARK verifier's circuit. That's why in in the concrete sense, it's much more efficient. Okay, so there's one small caveat here is that we don't have any guarantee that this decider is really really succinct. Like we don't have like a guarantee that it's always constant complexity, and the complexity of you might be linear to the instance size.

But this is easy to resolve by adding another SNARK that delegates the computation of decider at the end. So finally, the IVC proof will only run this check this SNARK proof rather than running the decider himself. Okay, so that's It's just one one thing Penny yeah. Go ahead. It's you know, there's a it's constant in one one thing that is important is the decider will always be constant in the number of iterations. So in there's there's two things. There's the size of the function F, and then there's the number of iterations. So both the accumulator and the the entire bit accumulator, so the witness and the instance um are and the decider are constant in the size and the number

of steps, but uh some parts here, so especially the accumulator witness and the decider do not have to be constant in the function uh in the step function. Exactly. In in general, it is still satisfied the notion of IVC. IVC's notion only require that the verifier complexity is independent of the number of iterations, which here we still satisfy. But it's just uh in in practice, if the circuit is large, maybe the decider complexity can be relatively large compared to checking a SNARK proof.

Yeah. Okay great. So I I have a I have a question about the um how the concrete security depends on the number of iterations. Um and think that's maybe a complicated subject, so we should perhaps leave that to the end. Yeah, maybe we can discuss this in the end. I think this is a good question, but yeah, we can we can discuss it later after the this talk, I guess. Yeah, after this the presentation. Yeah, Bending, please help me to remember this this question. Yeah. Right. So, given this background, we we know that there's already there are already some very efficient construction of IVC, like Nova and also in PCL MS 20.

Basically, the accumulation profile complexity is only around like two or three group exponentiation. However, there's still a gap for supporting some advanced application like CK EVM. The main reason are two folds. The first is that the existing accumulation scheme usually only support R1CS constraint system, for example, Nova or PCL MS 20. And this R1CS is a type of constraint system that's a kind of really traditional and is kind of less expressive than some recent advanced gates like high degree gates or lookup gates. By expressive, what I mean is that basically, to represent the same type of functionality, for example, elliptic curve addition, you you might only need

like one or two constraints if you're using high degree gates, but you might need more if you're using R1CS. So, we are saying that high degree gate can be more expressive in terms of in terms of its representation power. And this is really useful also in in the in the EVM applications. And we also know that while while we have this finished this paper, we also know there's also some other really elegant follow up like Sangria and Origami that still support Plonk or lookup gates, but there's some caveat here. The main issue is that if when the degree of the gate increases, the folding complexity also grows by a factor of D, which is the degree of the gates. That means you can kind of cancel

out the advantage of using this expressive gate because amortized cost per gate can also increase, so you might not be you might better just use Nova in that case. So, this is not enough, I think. And this is one of the good feature with that are missing. And second one is that we do not have really efficient circuit branching support for most of the scheme except some recent work called Supernova. What does it mean? The mean Let me illustrate by example. Let's assume there's a like we want to simulate EVM execution and EVM has a hundreds of OP code, right? And in each step, what you want to do is just to pick one of them and execute.

But if you are using Nova, what you can do is only to embed all these OP code gadget inside a single recursive circuit and do some routing when when you do the proving. And the folding complexity like consequently be proportional to the sum of the size of these OP codes circuits, which is undesirable because there are hundreds of OP codes. So, what we want is to have another scheme where are the recursive circuit size is only proportional to the single OP code that has been being executed at runtime. That can save us a lot of proving cost because the circuits can be much smaller when the number of instruction is a lot.

So we we highlight that these two requirements are really essential and important for ZK-EVM applications because first ZK-EVM are heavily using this like recent advanced type of gates and second EVM do have a lot of instructions like hundreds of instructions in their instruction set. Beyond this, another different reason why we want to have a new paper here is because we see that many existing scheme of IVC do have really different flavors of description as well as the security proofs. It would be great if we can have a unified and the form framework for understanding all this IVC scheme and make the make the analysis and the developments much easier. So, that's another

motivation of ProtoStar. So, given this I want to highlight our contribution here is that first we have come up with a new general recipe for constructing IVC scheme and more precisely the folding scheme. Basically, given some empty relation R and given some special sound interact protocol for relation R, we can generically transform it into some folding scheme for this relation and it turns out to be actually quite efficient and Novalize just a one special case in this modular framework.

And second, we also construct some really efficient special sound protocols, which I will I'll talk about later. Some special sound protocol for some really expressive relations like high degree gates, lookup relation, non-uniform circuit selection and also CCS, which is recent advancement on the constraint system, which is generalization of R1CS to higher degree gates. And the result and by combining these two parts, the first part is general recipe, the second part is the special sound protocol, we obtain a new IVC scheme called ProtoStar and the highlight here is that dominant cost of IVC proving is only a one MSM of size of the witness and the also

a a knock proof for the recursive circuit that's dominated by three group of exponentiations. In particular, there's no dependence in terms of number group exponentiations, there's no dependence on the gate degree as well as the lookup table size. Also, we know that there's a concurrent work HyperNova, which is also really an elegant work and they also achieve some similar results. And the difference here is that we think that our support to lookup seems to be much more cheaper. almost for us like our support lookup is almost for free while their support lookup can can add a lot of overhead.

And second, in this recursive circuit, we know that the number of hash hash operation and a non-native field operation inside circuit is also significantly smaller in our case. And moreover, because our support lookup, the circuit for non-native field operation can be even even smaller, so gives even more advantage out of that. So we think that for some application like a CKEVM, it can be favorable Protostar can be can be a favorable choice. Okay, so that's the contribution and now let me go to the the detail part and let me explain how the general recipe works for building a folding scheme.

Okay, so recall that our main goal here is that given multiple instance with a spares, we want to fold them into single one, right? And we follow the framework as as below. Basically, we have three steps. First, for some MP relation R, we first have some multi-round special sound protocol for it, which turns out to be usually pretty easy and we'll later later. And after having this interactive special sound protocol, we can use some really standard trick to transform into non-interactive arguments knowledge.

And after that, we can we propose to have a generic and efficient transform to construct a folding scheme for the very for a set of verifiable check in this non-interactive proofs. And this is basically a generalization of Nova. Okay, so but at this point, still is is still not good enough because the as as the degree of the gate increases, still the number of group operations is still proportional to the degree of the gates. So that's another key here is that we add one more step at the beginning.

Well, given some interact protocol for this relation R, we add one more rounds and then transform it into another interactive special sound protocol, but with a much more compressed verified check. So, the the least set of verified check is much simpler and and has much lower like mostly has not a a lot of a lot of a lot of high degree guess. And after that, we use the same transformation as we did before. And it turns out the resulting scheme becomes much more efficient in terms of number of operations.

In particular, the number of group operations now is independent of the degree of the verified check. So, that's the general framework and let me go into more details later. So, for now, any any quick questions? Okay. So, before coming to the detail of construction, let me quickly recap what a special sound protocol is since I already mentioned it for multiple times. So, in treat free, what special sound protocol means is this following. So, given some relation R, suppose you have some interact protocol for the for proving this relation R, and we say this protocol is case special sound if it if given K different accepting transcript, we would be able to extract some witness

for this relation. Then we say it's case special sound. For example, let's take this really naive example where there's no public input, but the goal of prover is just to prove to the verifier that he knows some really long vectors ABC that satisfies some Hadamard product relations. And there's a really naive special sound protocol for it. Basically, the prover just send the the entire witness ABC to the verifier, and the verifier just check all the equation need to be checked in order to to ensure that it's inside a Hadamard product relations.

And this is still a special sound protocol. And first, it's obviously one special sound because every accepting transcript is basically just a accepting all that witness inside a relation. And we know there are three important parameters we care about in a interact protocol. The first is R, which is the number of runs that prover will send messages. So here you see this non-interactive basically just on only one move, so R equals 1. And the second there is a parameter called D, which is the maximal degree of the set of equations checked by the verifier. And third is another parameter L, which is the number of checks done by the verifier. So so more specifically in this example, the verifier will conduct

N different equation checks. Each of them is just a multiplication, right? So because multiplication is degree 2, that means D here equals 2 and L here equals N because we check N different equations here. And to to expressing some language of a SNARK circuit, but this is basically the number of constraints in a circuit and this is basically the gate of the degree of the gate. Okay, so that is it. That's special sound protocol and before coming to the next step, I want to highlight one one more thing here is that usually it's much much easier to design a special sound protocol for some relation. And the main reason I think here is that we don't have any requirements on the complexity of this

communication as well as the complexity of this the verifier checks. So basically prover can send a lot of things. Can send a really gigantic possibly large witness together to to the verifier and the verifier can do a lot of checks to check these things inside a relation and still is a valid special sound protocol. So that this makes our analysis and design much easier to think in thinking in the special sound protocol case. Okay, so now suppose we have this interact protocol, which is special sound. We can use really some really tricks to transform it into a non-interactive argument for knowledge using commit and open and Fiat Shamir.

So, basically finally what you get is is a knock transcript. It consists of two parts. The first part is the short commitment to the messages that's being sent initially in this original protocol. And the second part is the big openings of these commitments, which is basically the messages sent by the prover in the initial protocol. And also you need to come up with some random challenges using Fiat Shamir. And it is it was proved by some previous work that as long as their original protocol is special sound, the resulting knock knock protocol also have knowledge soundness. So, basically now we we have obtained obtained some knock proof for the same relation R,

but also have knowledge soundness. And our goal is reduced to fold these knock proofs. Okay? And uh for now uh let's see we have already have this knock proof for this relation. For simplicity, let me just uh assume the public input is empty, but when the public is not empty, we just put it inside the instance part of this proof. So, now in this knock proof, we have two parts. The first part is what we called uh proof instance, which consists of short commitments to the messages and the challenges uh and possibly public input, which we are ignoring for simplicity. And second part is the this long proof for messages.

And this knock proof is valid if and only if a set of L equations are checked correctly. So, if and only if this L equations are evaluated to zero. And here the each equation out of this L equation in FD, we for simplicity we assume is homogeneous. It means that every term of this uh algebra formula exactly have degree D in its input. For example, X1 * x2 + x1 ^ 2 is is homogeneous cuz every term is degree 2. While x1 + x1 ^ 2 is not because x1 has degree 1 while x1 ^ 2 has degree 2.

But for simplicity, let's assume that every term are are the same. But it's actually without loss of generality because suppose we have some other more general formula, okay, which is inhomogeneous, we can just add a slack variable here, u, as a input, and we can pad every terms to exactly degree d by multiplying the power of u. And here in this instance, we just set u to be 1, right? So, it's it's without loss of generality and for simplicity, let's always consider this case. So, now our goal is to fold this Nark proof and and build accumulator out of it. And the accumulator exactly have really similar form, which also have these commitments and challenges and prove a massive

fields. The only difference here is that we add one more error vector commitments inside this accumulator instance, which is some short commitment to some long vector error vectors. And also the set of checks by the accumulator is changed a little bit. Well, in each equation, instead of requiring it to be exactly evaluating to zero, it's okay to be evaluating some other non-zero values as long as this L final L values are exactly consistent with the commitments inside this accumulator instance. And this is some trick very similar to I think similar to Nova and also BCIMS 20. Okay, so now our goal is to

is to fold this Nark proof onto this accumulator one by one okay? So, that's our goal and we call it the main goal here is to want to have a new accumulator instance such that if the new one is satisfiable, then all these checks all these previous checks for a previous accumulator check and this Nark proof will also be correct. So, how do you do that? Um a general idea is that we see that this this structure the two structure are really similar. They all have the same formula FD here. And what we can do, we can interpolate them using polynomial.

Okay? So, let's consider the following polynomial where we replace every message by the by some linear polynomial that is interpolating both the messages from the accumulator as well as from the knot. So, for example, we use X * M + M' to place M' and M. And similarly, use X * R + R' to replace those challenges. Why we care about this polynomial? The idea here is that because this FD is homogeneous, it has a really good feature and the property because basically, if you see the constant coefficient of this set of polynomials, they exactly matches the left-hand side of the accumulator's check. And if you see the degree D coefficients of the of this

polynomial, they exactly matches the left-hand side of this knot verify. And let me illustrate by one very simple example. Let's say there's only one equation being checked where L is one, so there's only one polynomial to be considered. And the degree equals two and this formula is just R1 squared. And then we rewrite this in this polynomial representation, replace everything with linear polynomial, and expand it. Well, now we do replace R1 to be this and do the square again, and we expand it, and we see some magic happens. It's exactly the constant term exactly accumulator's check, and the degree two term exactly

knot verify check. So, this is one simple example, but believe me it holds more generally. And given this feature, given this property, it gives us a a good way to to check that the previous two checks are done correctly. Basically, this is equivalent to check that this polynomial has the following form. First, the constant coefficient exactly is some vector being committed in in e here, and degree d coefficient is exactly zero. Right? So, we only to prove that. And how to do that?

The idea is the following. So, we we represent this polynomial in this form, its coefficient form, and the prover only needs to commit this polynomial and show that exactly this right-hand side polynomial has this form. So, the idea is the following. The prover will just send this intermediate cross error terms, which will bind this polynomial, and sometimes because e j can be long because of there are l number of equation being checked. So, we need some padding and commitment to make it short. And after that, we can reduce this polynomial check to to some random evaluation check, where the verifier will just sample some random challenges.

And now, this kind of check can be reduced to this this check, where the x is replaced by this random values alpha. And you see that this is exactly a new type of accumulator check. The only difference is that the message becomes the linear combination using alpha, and error terms also become some linear combination of the original cross error terms and error vector commitments. And so, that gives us a really natural way to do folding, which also also similar in Nova, is that we just do the random linear combination, for instance, and error commitments. And the prover will additionally fold this witness as well.

Okay. So, for now, I'm kind of little bit cheating because I'm always arguing the soundness, but actually what we need is something called noise soundness. So, we should be able to extract the original witness for these two checks, right? But actually, the idea is quite similar. So, proved by previous work, it's sufficient to only consider the special sounders and we can prove that this protocol satisfies D plus one special sounders. Basically, given D plus one different transcript with different challenges, then we can like first we can pick two accepting transcript and extract out like solving some equation equations and extract out M and M prime here.

And the second step is to prove that those M and M prime and R and R prime are the correct witness. And that is also simple because this FD is a degree D polynomial and this polynomial check are matching for D plus one points. That also means that these two polynomial are exactly are exactly identical by some fundamental algebraic theorem. And that means the extracting M and M prime exactly matches this these equations because the constant coefficients matches and the degree D coefficient also matches. So that proves that the extract witness is is a valid witness. So that's the intuition but I refer to paper for more detailed and

more formal proof. Okay, at this point is is still not very good enough, right? Because when you can see when D is good in D is large, the number of group operations by prover is actually around D times L because you have to commit to D minus one cross error terms here, each of which is length L. Similarly, the verifier needs to combine the error commitments and that accounts for D group operations, which is really expensive if D is large. So we need to figure out a way to make this much more efficient.

Any questions so far? Okay so let's see how we can optimize this scheme. You see the I the reason that we need this DL group operation is exactly because we need to do some Pedersen and commitments make to make it short, right? Well, each a vector is of length L and L is usually really large because the number of constraints is really really large for circuits. But let's suppose we have some special sound protocol in which there's only one check.

Okay? In that ideal case, we we don't need to use this pattern and commitment, right? Because the vector itself is already short. We just uh we can just uh send them in the clear without using any group operations. So, this gives some idea. The idea is just to given some any general special sound protocol, can we transform it into another protocol that's proving the same relation but they only use a single check, basically L equals 1. If that's the case, when we do the folding step, we can be much more efficient. So, that's the general idea and the solution to it is also pretty simple. So, suppose we have two gates, two equations, we can introduce one random variable and do the linear combination of it.

And it's easy to check if the final resulting gate is satisfiable, then the satisfiability of original Y is also the satisfiable. And now we successfully merge these two gates into a single uh gate. Okay? And more generally, given L different equation, we can uh interpolate all these L equations into a single equation using the power of beta uh power of beta. And this gives some idea of doing transformation. Okay? So, more precisely, given a uh some initial protocol, which is special sound, what we do is that a verifier will sample a random challenge and like merge all the checks we had before into a single check, which is the basically the randomly combination of

the all the checks. Okay? But this this special sound protocol is not good enough yet because the gate degree or the check the degree of the check becomes much higher because in some in one term we need to multiply by beta to the L, so the becomes D plus L, and L is large. So, still we have a really bad scheme as expensive. But, this issue is actually not not very difficult to solve. The idea is just to see and understand this power of beta as a single value as a single difference message, rather than a power of beta.

So, what we do is the following. So, after example this beta, the prover will compute the power of beta himself and send the last message as this power of beta. Okay? And and then the new check becomes the following. So, instead of writing this as beta to the J, we only to write as a BJ, which is the one of the message being sent by prover. And now the degree is only D plus one. Okay? So, this kind of solve the issue of high degree the degree blow up. However, they also introduce some two another two other issues. The further first issue is that the prover needs to send more messages. Basically, it needs to additionally send L messages. That means later it has to commit to to this L

terms, which can be expensive. And the second issue is that the verifier also need to check that these messages are done correctly, which will I'll talk about later. So, let's focus on the first issue here, where the prover is more expensive. And the solution to that is actually pretty easy. Well, instead of representing a power of beta using a single variable, we can represent it as a product of two variables. Or even more generally, you can represent a product of three, two, or even K variables, right? And that means instead of sending all these power of beta power of beta, the prover only needs to send this. The only needs to send square root of L number of message BI and BI prime, where BI prime is the beta to the I times square root of L. And still you

can have this check, which is only degree D plus two. And more generally, if you using K different product, you have you have like less message to be sent, but higher degree. But usually we find a sweet spot to using using two because initially already prover already needs to put some efforts. So using two already decrease from L to square root L. So usually it should be should be sufficient. Okay, so this solves the first issue while the prover's complexity doesn't increase much. And the second issue is the following. So recall again that initially what we have is we have L different degree D case, right? And using this trick we transform

into a single degree D case. However, we also introduce additionally square root L degree two checks here, which seems doesn't solve the problem. But the But the key observation here is that the additional check are low degree. So what we can do is that we separate the checks into two parts. The first part is a single degree D checks, which we are using D minus one cross error terms. However, these D minus one error terms are are really short, so we can just using field operations rather than passing commitment. And second part is this part, and we do need to add one more cross error vector commitments to commit these square root L terms. However, because it's low degree, we only to add

one more separate commitment for that instead of D of them. So that solves the issue, and then finally what we get is still like the the verifier only to perform R plus two group exponentiations. And plus two here is coming from two parts. The first part is the extra message being sent by the prover, and the other one is the extra separate commitments for these square root L checks. And we also note that a good racing here is that when we later support lookup, it really doesn't add any overhead because we have a special sound protocol for lookup that only involves degree two checks. We can batch all those checks inside this invest accumulated checks and we don't need to introduce any extra commitments out of

it. So that's also one reason that we can have really good support for lookup. Okay, so in summary, the general recipe works as follows. Given some empty complete relation, suppose we have some interactive protocol for special sound protocol for this, we first transform into some another special sound protocol that has compressed the verifiable check and use some standard trick to make it a non-interactive arguments of knowledge and finally we use this generic way to make folding scheme for this not verifier and then we use some previous works idea the IVC compiler to construct an IVC scheme. In particular, if you want to have more efficient construction, you can use the recently like proposed work by Ben and Wilson

that has using cycle curves to to build IVC, which is also some idea that has been described in our paper. Okay, so basically now we have reduced the problem of constructing IVC for some expressive relation into the problem of building some special sound protocol for some expressive constraint system, right? And it turns out to be actually pretty easy. In particular, we have obtained some only one move special sound protocols for a lot of building block relations like permutation relation, high degree case relation, non-uniform circuit selection and the CCS, which is the some recent advancement on constraint system.

And the main and this scheme is really almost trivial. It's very similar to the naive example I mentioned before. The idea is just let the prover send the entire witness and the verifier will just check the set of algebraic equations that represent this relation. And the main reason that we can do this is because all these building block relations, they can be represented as a set of algebraic equations over the initial witness. Okay? So this makes the design of very very easy. And this is also justify the claim I had before that building multi-round special sound protocol for many interesting relation can be actually pretty easy. And there's one like subtle exception here, which is a

lookup relation because we don't have a really straightforward way to represent this lookup relation as a set of algebraic equation only over the over the lookup values. But it turns out we can still have a really simple and efficient special sound protocol for it. And here the interaction will help. Okay, so let's let me quickly recap what lookup is. So lookup relation is saying that given some uh online lookup value, which consists of L values, we want to prove that they are they exist they belongs to some preprocessed table of elements T, which consists of T elements, where T can be really large depending on the table size. And like proof by this this paper by Haböck

in 2022 called log derivatives from for for lookup, which is also really elegant paper and recommend everyone to read this. It shows that this lookup relation holds true if and only if this fractional identity holds true. More precisely, if only there exist some multiplicity MI such that this two sum of fractional identity holds true, where the first one is 1 over X plus WI and the the terms in the second sum is MI over X plus TI. So intuitively what MI means here is that it is the number of appearance of this elements TI inside this lookup set, right? So basically if if that's the case, you can generate

this MI. If not, then the fractional this polynomial identity on the left-hand side won't be equal to the right-hand side. So basically this this one holds true. That's the that's the general intuition. And given this, we can come up with a special sound protocol. The idea is also quite quite similar to what we did before is that we replace X with some random values by verifier. So, the idea is the following. In the in the initial rounds, the prover will send this witness and the multiplicity, which will bind these two polynomial a fractional polynomial identity. And after that, we just need to check that this fraction identity evaluation are equal over some random value R. So, verifier will sample this

random challenge, and the prover will send will compute these fractional identity evaluations and send it back. And now, the verifier only needs to check that these two sum are equal, and also needs to check that these vector being sent by prover are computed correctly using some degree two checks. Okay? So, make sure the H and the G are are computed correctly. And we note here that there's one great feature of this special sound protocol is that even though the prover message can be quite long, like have length T, they are actually pretty sparse. Basically, the number of non-zero elements inside these messages can be less than can only be will only will be less than

L, which is significantly smaller than T. And that means when later when you want to commit to it, the committing complexity can be much smaller because we don't need to do anything for those entries that are zero. And this gives us some inspiration that maybe we can have a really efficient IVC for a novel IVC folding scheme for for this lookup relation. However, there's a one subtle challenge. The The reason is following. So, remember that in this folding scheme, this folding protocol, at the beginning of this folding protocol, the prover needs to send those intermediate cross error terms, right?

And the computation of this error terms actually depends not only on this online non-proof, but also on the accumulated the But the messages is actually not sparse because they basically are some randomly combination of a multiple uh multiple proven messages. So, that means the computation of the error terms can can amounts to OT number of field operation, which is no longer independent of T. However, uh we we note that actually what we need is just the commitment of this uh cross error terms.

And it turns out we can compute them from homomorphically given the accumulated message commitments and accumulator error vector commitments without bothering to recompute the all the vectors on the line. So, that's the general idea of uh saving this T OT operations and still have an a complexity that's independent of table size. Okay, so uh I want to note one more thing here is that this lookup protocol can be easily generalized to support vector lookups. Well, basically every element in this table is just a vector of elements rather than a single element. And this can be quite useful in application like uh 32-bit arithmetics.

Well, you just store all those input-output uh arithmetic pairs and you just do lookup in the circuit, which can be really useful and is heavily used in ZK-EVM. Okay, so after having this uh sub protocols for building block relations uh if you want to have some NP-complete relation for uh for some expressive constraint system, what we do is just composition, right? We just compo- compose all these sub protocol to obtain final sub uh protocol of which is special sound and is for this uh NP-complete relation. And this uh filled last piece of our story, and we now uh have two parts. First, we have a general recipe for building folding scheme given some special sound protocol. Second, we have really simple

special sound protocol for some really expressive relation. And by combining these two, we obtain Protostar, which is the new IVC scheme in which the uh recursive circuit is only dominated by three group exponentiations and in particular we can support really high degree gates, really large look up table and really a lot of OP codes being executed in some instruction set. I think that's basically it and thanks everyone for listening and now I'm happy to discuss more and answering questions. I saw there are there are some cash questions in the chat not.

Okay cool. I know that's a suggestion to the papers. Okay, okay, thank you. Okay, maybe we can discuss the first discuss the question uh on the the road, right? Then do you want to give a comment first? Uh yes, so um when you're computing the the concrete security so um the determines what promises you want to use, um do you need to take into account the um the maximum length of a IBC chain um in your application or um

so how does the concrete security depend on that? So um well the interesting thing is that the provable security is actually um uh basically says you can only do IBC for a constant number of steps. Um so even like constant in the security parameter um which and the reason for it is that you know the the every time I uh when I do the security proof, I call the extractor and then I call the extractor of a previous proof and these things sort of blow up uh multiplicatively. So um after T steps of of IBC recursion, my

extractor is actually size something like poly lambda to the T. Um and if that gets too large, if that gets larger than polynomial, then at least theoretically this becomes an issue because it's it's it's sort of meaningless to say, "Oh, you know, I I now have an extractor which can break some assumption, but if that extractor is exponential size, then it it sort of becomes a vacuous statement." This, however, is only a theoretical issue. Um, I think practically there really is not any um Let me Let me think.

But my my interest is in the any I don't see any practical implications if the size is large enough, usually concrete implementations involve multiple steps. Concrete implementations involve multiple steps. Okay. Yeah, here's my intuition that um let's say your proof system is such that you need to find a um um a a targeted hash um collision. Um, so you could build a table that um includes all of your possible targets over multiple steps.

Um and then it's not clear that you won't losing security if you have um more targets. Yeah, I mean, I think another way to look at it is if we at at multiple points, and and this is where the theoretical issues come in, at multiple points we transform interactive protocols to non-interactive protocols. And that's even that's that's absolutely necessary for getting something like IVC, otherwise the notion sort of becomes meaningless. But you could look at sort of the unrolled like underneath it are interactive protocol. And you could look at the sort of, you know, it would be like T times R round, you know, uh interactive protocol because the even

the accumulation scheme is derived from an interactive protocol and then applying it to the intermediate. Um, and I don't think we know for for for for these for special sound protocols in this there's only out to prove it for these special sound protocol. There's not really any any issue in in sequentially composing them. for two rounds. Yeah, and also I think I'm not saying anything wrong but yeah. I think the parameter like the not the R also the degree D also affect the the concrete security bonds. But I think for reasonable large number of R or D usually shouldn't be the be an issue in practice. But of course if you like D is

super high then we definitely will blow up. So so what what you said about unrolling the protocol that as as though it were one big interactive protocol to which you applied Fiat Shamir. It sounds as though you might be able to to prove something about that and it's probably a Yeah, but it's really not like the important thing is so so Yeah, you can maybe prove something. The problem is it's really like Like one thing that is important to understand is that that kind of these IVC constructions it's not the same we don't just apply Fiat Shamir once, right? It's not just like you have some big old interactive protocol you apply Fiat Shamir once.

It's you apply Fiat Shamir of like the the the intermediate components like for example the accumulation scheme and the intermediate and then you implement within the circuit, right? You build a circuit for that Right. non-interactive protocol and you cannot build a circuit for an interactive protocol, right? Like so it it doesn't you know, like the the it just doesn't really like it doesn't really track. I'm just trying to give an intuition here, right? Like there's no really meaningful thing that you can do or prove security about. It's just I'm just trying to say that like yeah, the combination of uh like uh T-round or like uh composing

special sound protocols uh sequentially seems to be fine. And these things are derived from uh special sound protocol. But that's kind of all we That's only a heuristic region. Yeah. Yeah, it's very heuristic, yeah. By the way, not a heuristic at all. But what's better is Yeah, uh go ahead. Sorry. Oh, like one thing that you can do if you care about the heuristics. So, we um uh we like uh so I think when you mentioned this, so you we we've given like these accumulation schemes, they work for kind of uh you can build basically the IBC chain in in a line, but you could also build it in a tree um because we give basically a folding argument or

uh you know, you could also fold two accumulators together or uh stuff like that. And then instead of building a line, you build a tree, and then at least you get a like your depth is only logarithmic. And um uh in the length of the computation, and um then some of these issues uh become a little bit better. And another advantage of using a tree is that sometimes it also helps with parallelizations. Like if you want to compute all the leaves together, right?

You can compute all the leaves in parallel and do it layer by layer, and it can be even faster. Yeah. Okay. Thank you. Um yeah, there there was a thing that I um uh pointed out in a um I think a previous time when you did a a similar talk, which is the the um optimization where you use a um the square root of um uh the number of challenges. You know, can we go back to that?

Yeah, it's the it's this one, yeah. So, this square root could be um replaced with a case root and then the degree would become D plus K. D plus K, yes. But I think I agree I think I agree I think I agree with you that that the square root is likely to be um sufficient in practice because this um uh O of square root um uh thing that you have to send is probably um small enough that that's not the bottleneck.

Yeah, suppose you for example is important to understand uh it's like go ahead Yeah, suppose you for example even you have 2 to the 30 base, right? The the square root is just the 2 to the 15. It's already very very small and uh usually you also have for another work in the previous runs, right? So, it it shouldn't be an over like big overhead usually when you do square roots. Yeah, I mean I think you can say this actually pretty generally because the size of M, the witness, is going to be at least L and you need to at least commit to M.

Um so, the only cases so so you're already paying for the cost of committing to M. Um which if M is dense, then that's a cost of L. So, you know, like committing to something that is square root of L should not be an overhead. Of course, there could be extreme scenarios where M is incredibly sparse. Um so, if M has a lot of zeros, um maybe it has like only square root of like L entries, then you might want to go to cube root. Um but exactly as you pointed out, Daragh, uh this this only adds like one to the degree, so it's really really cheap uh to do that. Um but in

general square root of L uh square root should be fine. And the advantage here is that it's always a parameter, right? Depending on the different application, you can choose your parameter, which uh you you choose what's the optimized one, right? Yep. Um I have a question. Uh so I think in the paper that you referenced at the very end, which uh is linked here, uh describes a soundness vulnerability in the original Nova protocol. Um and I was just curious, you know, if you guys had comments on whether or not that vulnerability applied to other schemes

that were based on, you know, Nova-style IBC schemes, and and uh and how you address it in this particular construction. Yeah, so basically I think that paper uh Krammer is from a long time. I think that paper is mostly about um correcting some vulnerability in the IBC compiler, right? This shouldn't be an issue. Actually, there's no issue for folding parts. And basically, for example, in our paper, we are just mostly focusing on folding, and then given this folding, we just use any IBC compiler that actually works. For example, we just use the IBC compiler in Dan's paper. Then I don't think that that that part will be affected. In particular, the the folding part in Nova as well as the um ProtoStar paper will be affected at that point.

Yeah. Um yeah, um Sean Beaulieu and I looked at this for Halo, and we're we're pretty sure that we um we didn't make the same mistake. The um IBC is not fully implemented for for Halo 2, but um in any case, it's the the mistake seemed to us to be kind of specific to um the what they did in Nova and they they basically did more work than um, they needed to and included another element in the um, the proof that they didn't need to and um, if you're looking at it with an engineer's eye then you would say I I can optimize this out and you wouldn't make a mistake.

I see. So Yeah, I mean but I think it was in it was essentially like you could say this was a bug in the implementation um, not in even the Nova paper. But like uh, you know, I think the real issue is that um, both the Nova and BCLMS like you know, the the and and Halo and and all the maybe not not Halo but like the the the compiler which like when people actually implement this when you describe it you describe it over one curve because that's the easiest way to do it. When when people implement this they use cycles of curves. Right, they use two curves and I think that this was just under specified. Nobody had actually like

written up and thought about formally of like how to do this. And when it's under specified like people it's easy to make mistakes and I think that is exactly what happened here and and this sort of uh, and like we're totally at fault here like in ProtoStar we don't give a precise compiler but like yeah, I mean it I think it shows like the value of like someone really going and and writing up the the details and I I I agree. I sympathize with paper authors because um, this is actually really complicated and would double the length of the paper at least um, and I think maybe it it belongs um, the the form of a paper is probably not

the um, the right way to do this. Um, in Halo 2 we have additional documentation. We have a Halo 2 book. Um, that is is where things like this belong and can be is not subject to page constraints or um Yeah, I read about you know the specification can include lots of background information. A very I was going to say a very comprehensive Halo 2 book if my memory serves correctly. But no, in general it's great and I appreciate you all's comments on it because I think it is it is interesting the interplay between theory and practice, right? And obviously where I sit as the CEO of a layer one blockchain trying to implement cryptographic schemes and Protosh on the

call. I think he's still on the call. You know, he can probably speak to this uh specifically, right? The engineering of the thing versus the theory of a thing and there's just a whole number another dimension of complexity that gets introduced, of course. It feels when you're writing a paper, the goal is to be general and to have it be applied in multiple contexts, but of course in any specific system, there's specific implementation so uh feels like a bit of an There's also There's also the fact that the the cycles of curves were not the focus of most of these papers. Um I mean that it was a focus of the the original Halo paper.

Um But yeah, but even that didn't um include many of the details needed. Which I guess we should maybe explicitly recognize I think being I think at least uh the beginning of many of these ideas around recursion and and you know, accumulation. So I think that that was a definite 100% yeah. important moment in the field so um Well, and the naming scheme, no? Like Yeah. Um but yeah, no, I think there's also opportunities I mean of course when things get implemented and bugs like this get found it it results in new opportunities for research. So I think it's a great I mean this is one of the great things about this group in particular is I think we have both um people who are practitioners as well as theorists, so

Uh last question for me. Um and and sorry to hog the mic here, but um can you guys speak a little bit about the um, the way you see this as being applied in practice, particularly uh, on with blockchain-based systems like the EVM. So, how how concretely do you view this um, paper as being applicable to, you know, uh, the EVM or or or maybe making the EVM the the ZK-EVMs more practical? Yeah, so I think it's a kind of like starting points, but it really I think it really helps and uh, for the ZK-EVM applications because as we can see in a lot of ZK-EVM applications, they are really heavily used uh, lookup gates for first because there are a lot of range checks and they are simulating

arithmetics over like 2 to 64 or 2 to uh, 32. Uh, and uh, that's the first thing and they are also heavily used high high degree gates. And also they do do have the problem that they need to like support multiple uh, opcodes in in in in uh, in par par in par in simultaneously, right? And I think this our scheme is really applicable to those uh, to those area and can make make the ZK-EVM application like much more efficient. And on the other hand, I think that's not the end of story because for example, I heard from the the engineer who implements ZK-EVM, they say one of the really bottleneck is that how to simulate memory for example, like

in particular in our scheme, we still don't have uh, a really really good uh, way to uh, simulating memory access beyond just committing this entire memory table inside witness because they are online. So, we cannot use the sparse trick for table a preprocessed table uh, elements in in this setting. So, it's still really uh, interesting open question if we can solve that part. If that part is solved, I think uh, like we can come to another stage like well, we have we have a even more efficient application and implementation for ZK-EVM. And uh, that's that's my understanding. Yeah. So, if I can pull out Go ahead.

Um so, my understanding is that the ZK EVM um uh this the one by the Ethereum Foundation um depends heavily on dynamic tables. Um so, the the um the derivative technique um does that support Uh dynamic table? support it, but it's not that efficient. Like, you can still move this online table as some commitments. But, you don't have don't have this trick of sparseness because we need to require that those to be preprocessed. But, uh this this trick is still useful for us uh simulating bit arithmetics, right?

Well, you still have uh some fixed table Yes. beforehand. That's can can be That's also another really heavy part. But, I agree for dynamic table, the complexity is uh is higher uh if the table size is really large. But, still we can support that. Basically, we can still just uh just instead of sending the W and M, we also send the online table in the first round. That's the only difference. But, that means basically, you you will have uh more more complexity for prover. Oh, I see. Yeah. If I could pull out uh maybe the last bit of what you said then you uh a minute ago, I guess it sounds like an interesting future direction of work here is is around memory constrained provers. Is that right? So,

like provers where there's a limit on memory and therefore I'm trying to figure out how to make it more efficient in that context. Is that right or or is that is that not what you said? Uh I think it's more of the memory within the circuit, right? Like, it's like the you want to prove like the ZK EVM actually has a memory, right? Like, the the virtual machine and trying to efficiently prove like that this memory like the memory access is reads and writes and that I'm correct in this. Simulation simulation of the memory. Yeah. More efficient representation or simulation of memory in circuit effectively is the direction.

I I I mean we we could move towards more functional um smart contract languages that that don't require simulating memory. And that they might also be easier to prove with contract secure. This is like the lower lower Yeah, this is their direction. Exactly. Yeah, the direction from uh uh I think originally started with protocols and and they're using, you know, like um I think that this was originally built with Nova.

Um and but you know, I think like everywhere where you use Nova, like using sort of Protostar now would probably give you an improvement and and like the main benefit is the lookups in the high-degree gates and like the the trade-off, especially for high-degree gates, is is is better than in any other scheme that we've seen before. Like in in Hyper Plonk it's already better than in Plonk. Um you can, you know, sort of you get better trade-offs, but but for um Protostar um you have really really like uh I mean this is, you know, like again, like theory and practice. We have to see this in practice, but I mean you could support degree like easily 100 and maybe even 1,000 gates um

and um hopefully those are useful, but um you know, that's that's I think the the the additional cost for for increasing the degree really does not seem that high. Um So On the that's interesting. On the simulating memory um thing is it's also worth noting that you can write in um a an imperative language and compile it to single sign um form and um what you end up with is not very different from a functional program.

Um cuz um there's a um parallel language um called Clean which essentially did that um uh and got faster than C on on a um large range of programs. Awesome. Um well, thank you all very much. This has been a great discussion. Maybe I'll open it up to the floor in case anyone else has any final questions. Um okay. Well, uh thank you Benny and Benedict very much for being here and for presenting this work. Uh it's really exciting and looking forward to seeing uh how things progress from here.

Thank you. Thank you, Alex. Thanks for inviting. Yeah, we are also really happy to be back here. Yep. Thank you. Very very enthusiastic about our approach to stuff. Thank you. Bye-bye. Awesome.