ZK13: Linear-Time Accumulation Schemes - William Wang

Transcript

[Music] Yeah, I guess just to introduce myself briefly, I'm a PhD student at NYU. Um, this work is with Benedict, my adviser, as well as uh Jacamal from EPFL. Great. Okay, so let's just get started. So let me just first start by motivating the problem we're trying to solve like with a toy example. So suppose I want to prove uh the correct execution for some program. I'm going to kind of abstractly model this as a CPU circuit where the

circuit step function is f and there's some initial state to the program which I'll call like state zero. And we can sort of model this execution of the program as just repeatedly applying the CPU circuit onto the state over and over again. So you know if I want to prove correctness kind of the natural approach would be to just use uh you know some proof system like a succinct argument for example. Uh but I want to argue that this is not ideal for a number of reasons. Okay so first it's not memory efficient. So typically when you look at these proof systems, proving will typically require kind of space proportional to the entire uh length of the program. Whereas when you actually

run the program, the only thing you need to do is keep track of the current state. Okay. And second, it's not incremental. So maybe your computation is evolving over time and you want to periodically generate proofs to certify the current state of the computation. And again, if you just use just some generic proof system, this would basically require you to reproof everything you've proved before every time you want to generate a proof, even though you haven't done much more uh steps of the computation.

Okay, so this task that we're trying to solve is known as incrementally verifiable computation. I'm sure a lot of us are already familiar with what this is, but I just want to kind of give a brief overview so that we can like get everyone in the room caught up. So, IVC is a proof system where you can run the prover on the current state of the computation and what the prover will do is well first it will kind of increment the state by applying the step function and then it's going to prove that this current state was done correctly. And the cool thing about IVC is that you can kind of do this. Oh, and I should say this is I call this the IVC proof. And the cool thing is you can kind of rerun this IVC prover to

increment the state one more time and have the IVC prover just update the IVC proof in order to obtain a new proof that certifies the new state of the computation. Okay. And you can do this an unbounded number of times. And at any point in time you can run the IBC verifier which just looks at the current state of the computation as well as the current proof to decide whether the full history of the computation was was valid. Okay. And the important efficiency feature here is that kind of the work of the prover and verifier at each step is independent of the the overall length of the IVC which is what gives us kind of the efficiency benefits that I talked about in the previous slide. Okay. So I should also mention

that there's this related primitive called proof carrying data. So if you think of IBC as kind of proving line computations, PCD is sort of analogously proving graph computations. But that's all I'll say on that. And both IVC and PCD have a tremendous number of applications um both for specific types of things that you want to prove like you know verifiable VMs, rollups, signature aggregation as well as just more um general proof systems that have a lot of desirable features like low memory usage or uh being paralyzable. Okay.

So I also want to talk about kind of the classical approach to constructing IVC which is using this technique known as recursive proof composition. So imagine you have some succinct argument uh I've labeled the prover and the verifier var. And what the IBC prover will do is well first it's going to increment the state of the computation and it's going to prove that it did this correctly using the succinct argument and not only that it's also going to prove that the previous proof was valid. Okay. And this is how kind of implicitly you are certifying the full history of the computation by sort of recursively proving that the previous proof was valid. Okay. And in

particular, I've kind of boxed in a dash line this uh this circuit. And essentially, this circuit is sort of encoding the statement, right? There exists some previous state with a valid proof which explains the new state of the computation. This is the sort of statement that the succinct argument is proving for. Okay. So now let's kind of turn to the the more modern approach of constructing IBC which is built on reductions. So you can think of reductions as a generalization of arguments. So it's a proof system where the prover wants to convince the verifier of some membership claim to a relation. Okay. So the prover receives the the instance and the witness. The

verifier receives the instance and the prover is going to send a proof to the verifier. Now after this the proven verifier going to output a new statement. So w prime a new witness and x prime a new instance. And the point is that the verifier has now sort of reduced the claim about membership in R into a new claim about membership in some relation RP prime. Right? So we haven't fully proved the statement, but we've kind of reduced the membership claim into a hopefully simpler membership claim that we can kind of further iterate on. So so completeness is a you know a property that we want from these reductions.

Basically, if the original statement were in the relation, then the new statement will also be in the relation. And analogously soundness says if this original instance was not in the language, then with high probability, the new thing will also not be in the language. Okay? And I just like have this notation. This LR just means the the set of instances which are in the relation. Cool. So now let's talk about accumulation schemes. So you can view an accumulation scheme as a specific kind of uh reduction where an accumulation scheme for some relation R is a reduction from this product relation R* RAR to RAR. So

RAR here is uh just some arbitrary relation that you can kind of freely define so long as your accumulation scheme satisfies this definition. Okay. So what do I mean by product relation? So basically now we want to test two membership claims. One membership claim for the relation R and another membership claim for the relation R star. Okay. And you can run this non-interactive reduction in order to have a new claim that some new statement is in RAR. Okay. So intuitively you can kind of think of what an accumulation scheme is doing is it allows you to kind of compress an unbounded number of membership claims in R into a single membership claim in RAR by kind of

iteratively applying this reduction over and over again. Okay. Uh oh. So I should say that I'm calling this an accumulation scheme. Like technically speaking, this is a split accumulation scheme, also known as a folding scheme. But in this talk, I'm just going to call it accumulation. Cool. And one more thing. So I've kind of defined a simple example of accumulation scheme where just where we're just compressing one membership claim of R and one membership claim of RAR. But in general, an accumulation scheme should be able to support, you know, an arbitrary number of R membership claims and an arbitrary number of RSAR membership claims. Uh, this is necessary for constructing proof carrying data. Okay, so now let's really quickly look at how to construct IVC from

accumulation. So I'm not going to go into the actual uh the actual construction because it's quite technical, but I just want to kind of highlight the the highle like what's actually going on. So you have an IBC prover inside of it, it's going to be running the accumulation prover and the accumulation prover is going to be proving some sort of statement about the step function f as well as the accumulation verifier. Namely like there exists some previous state with the accumulation verifier accepting such that uh this explains the new state of the computation. Okay, so I've kind of handwaved it quite a bit, but really the only reason why I care about this is just to uh sort of compare it against the succinct argument approach. So I'

I've displayed both of them here and as you can see they look quite similar. Uh this is also intentional. Um the only difference between these two sort of approaches is well the IVC for from succinct arguments we're running the argument prover and it's proving statements about the argument verifier. Whereas when you construct IVC from accumulation, you're running the accumulation prover which is proving statements about the accumulation verifier. And the important thing here is that kind of we can design accumulation schemes these reductions which are a lot more efficient than we can uh than corresponding arguments. So in particular we can try to construct accumulation provers which are a lot faster concretely than any known

argument prover and we can also construct accumulation schemes where the verifier is a lot smaller both in concrete and asmtoic terms than any known argument verifier. So these are the two reasons why kind of the modern approach to constructing IBC is via these accumulation or folding schemes. Cool. So let's get to our results. Um first I'm going to just define the sort of NP relation we care about which is uh I call it polinomial equation satisfiability. So basically you know you have some instance which is some field elements and some witness which is some other field elements and basically this is in the relation if the instance

and witness satisfies a bunch of polomial equalities. Okay, so I'm not claiming anything new here. Really the only point of talking about polomial equation satisfiability is that it sort of models a bunch of actual NP relations we care about like R1CS, uh, CCS or generalized R1Cs. All of these things can just be interpreted as polinomial equation satisfiability. Uh, I just want this definition here because it's a lot nicer to to abstractly think about, but there's nothing fancy going on in this slide. So just as an example, this is how you would model uh R1CS as a instance of polinomial equation satisfiability. Right? The M R1CS matrices if you're familiar with R1CS kind of implicitly define a bunch of these quadratic polomials which we can

um uh constrain. Okay. So let's get to warp. So warp is a hashbased accumulation scheme for this relation. And again when I say this relation I'm you know you can instantiate it with r1cs or ccs or whatever you you'd like um with some very nice properties. So first in terms of prover cost it's uh very efficient and in fact linear time. Um here I'm like this absolute value of this p hat is just the the amount of time it takes or the number of field operations it takes to actually uh evaluate the polomials themselves which qualifies as linear time.

And the other nice feature is the verifier cost. And so I should highlight that this sort of u number of random oracle queries that this verifier makes is essentially optimal for a hashbased accumulation scheme. Um and smaller than any known argument verifier. Okay. So we prove security in the pure random oracle model. There's no other cryptography you need. And in practice, this random oracle can be instantiated with a cryptographic hash function. Um, moreover, we're kind of totally agnostic to uh the field of choice. So, you can pick whatever field you want as long as it's sufficiently large, then we can get some uh a secure accumulation scheme. And in fact, actually, we can

use any field we want like a small field uh just by using field extensions, but I won't talk about this here. Cool. So, I have a very fancy table uh showing a lot of different succinct arguments and accumulation schemes. Um so the succinct arguments uh I've also only focused on the hashbased ones with a linear time prover. So I don't want to go through every row but basically my my point is that if you are interested in constructing IVC then it is reasonable to compare uh succinct arguments to accumulation schemes in terms of one the runtime of the prover and two the the size of the verifier. And so for for succinct arguments with a hashbased uh

that are hashbased and with a linear time prover um the verifier makes a larger amount of ver random oracle queries than all of these sorts of accumulation schemes uh warp being one of them. And if now we restrict to accumulation schemes um warp makes fewer uh random oracle queries than um well both arc in terms of concrete terms and as well as fax which is this uh concurrent work um also in terms of concrete terms. So here K is kind of this small constant which is uh from the fact that a lot of these succinct arguments as well as facts uh need to be instantiated with this object

called a multilinear IOP and K is just like some constant associated with uh this MLOP but I don't want to get into that uh my point here is just that um kind of warp kind of represents the the state-of-the-art both in terms of the prover time where linear time like this succinct arguments as well as the the verifier our size. Okay, so how do we actually get this done? Well, our main contribution is this new interactive oracle reduction of proximity. So I'm calling this an IUR and I'll define it shortly. And using sort of this existing method for compilation, we can first transform an IUR into an accumulation scheme. And the efficiencies of these two things are

closely related. And then we can kind of convert an accumulation scheme into uh proof carrying data uh using again known approaches. Uh and the the really important thing about our IU is that it's instantiable with any linear code over any field and in particular you know if you use a linear time encodable code then like what it spits out is a linear time prover. Okay. So as a bonus, we also get this this property called straight line extraction for any linear code. And uh I'll also get into what straight line extraction is. But uh prior to this work sort of if you wanted to use a linear time encodable code in order to have a

linear time snark then you were not able to get straight line extraction which is highly desirable. Um and in this work we actually show how to do it for any linear code and in particular linear time encodable codes. uh and I think this technique should also apply to linear time succinct arguments but again I'll talk about this at the end uh we also have this new technique for out of domain sampling for any linear code whereas previously this was only uh used in the context of read solment codes okay cool so let's talk about uh how the accumulation scheme actually works so first I want to just define what I mean by like these sorts of hashbased

reductions or IUS. Uh first I want to define this object called an interactive reduction. This is kind of just the same as uh the reduction that I defined before but now I'm making it explicitly clear that uh you can allow the proven verifier to interact with each other. So they can exchange messages back and forth and then decide on what the new statement is. Okay. Next we're going to kind of relax this further into an interactive oracle reduction. So in an IUR now the prover can send really long messages which the verifier can just query at individual points without reading in the entire message. Okay. Um and the point here is that by using this oracle model we can enable succinct

verification because the verifier does not have to read anything in. Okay. And then we have the non-interactive hashbased reduction that I described earlier. And there actually is sort of this standard compilation procedure for converting an interactive oracle reduction into a non-interactive hashbased reduction uh essentially by using Merkel trees as well as well as fetchir. So this is an adaptation of the BCS transform if any of you are familiar with that to the reduction setting. Okay. But for the rest of this talk I'm going to focus specifically on this interactive Oracle reduction object because kind of um this compilation part is fairly standard. I don't want to have to worry about that and instead we're just going to look at this sort of

abstract object of an IR. Okay. So what is an interactive oracle reduction? Well, now I'm going to consider these uh turnary relations where the instance is split into X and Y and the idea is basically the verifier will have oracle access to the to Y. Um so it can query it again at individual points and again the prover and verifier can you know exchange messages. The verifier can query both the provers's messages as well as the the instance oracle y and at the end it can output some new instance x prime y prime uh where y prime is selected from any of the oracles that

the prover. Okay. Other than that this is sort of a standard reduction. So for completeness if the original statement was in the relation then the new statement will be in the relation and for soundness essentially um if the old statement is far from the relation then with high probability the new statement will be far from the relation and here by far I just mean in terms of uh having distance of y to the to the the language of the relation which I've like denoted here.

Okay, cool. So, let's get to warp. In a nutshell, warp is sort of an IU for this constrained code uh constrained code accumulation. So, what is a constrained code? Well, first of all, take any linear code you'd like and also we're just going to consider any lowderee algebraic constraint FE. So you can think of f as sort of maybe like a lowderee polomial um which is allowed to be in many variables and we're going to define a constrain code to be a subset of the code uh which sat the subset of code words which satisfy your your algebraic constraint which I've denoted cy.

Now in a constrained code accumulation scheme what we want to do is we want to have like two we have two membership claims for uh these constraint codes and then via the prover and verifier reduce it into a new statement about uh a single constraint code. So in particular uh the prover and verifier will again exchange messages. The verifier can make some queries and then it's going to output a new constraint fee and the new membership claim is that f is in uh in this new constraint code. Okay. And my I argue that sort of this object is all we need to construct an accumulation scheme and we're actually just going to focus on this specific task of constraint code

accumulation. So really let me highlight like we can use any code we want. So whereas you know protocols like fry stir and were um as well as a previous accumulation scheme of mine called arc need to use read solomon codes and like crucially the protocol depends on properties of read solomman codes. We can literally like we're agnostic to the code. Um and additionally we can use any lowderee algebraic constraint that we'd like. So for a lot of IOPS like fry and stir they do not support constraints and protocols like were only support a very limited uh class of constraints for us as long as fee is low degree in some sense we can support it and in particular uh fee will

essentially kind of encode this fact that um f1 and f2 actually are just valid valid witnesses for the original relation you want to care about. Okay, so let's get into the protocol overview. Um, I like to view this protocol as being split into two phases. So, first there's this batching phase where the proven verifier uh exchange the messages to reduce two membership claims about constraint codes into a single membership claim about some random combination of the vectors. So, I'm kind of batching the claims together.

And then in the switching phase again the proven and verifier are going to exchange some messages in order to reduce um in order to reduce this membership claim about a random combination of vectors into a membership claim about a single vector that the prover. Okay. So let me highlight two uh efficiency features which are extremely relevant for um concrete concrete numbers. So first the the prover actually in this protocol literally only sends one oracle whereas in a lot of these distinct arguments as well as other accumulation schemes you're going to need to send multiple oracles throughout the protocol and this translates into multiple Merkel commitments that you have to do and multiple openings that you have to make.

Um and also the verifier will only make uh like a security parameter number of queries to the to the oracles in this construction which again I argue if you want to um have negligible soundness is essentially optimal. Okay. Okay. So let's like focus in on these two phases of the protocol. The first is the batching phase. So here what's really going on is it's a standard folding reduction. So if you're already familiar with folding schemes like Nova or Protostar, really this is all that's going on. Uh we're running a very lightweight sum check protocol to um kind of interpolate these two constraints into a new single new constraint um which we now uh want to claim that the random combination of

vectors is a member of. And here the soundness also relies on the so-called proximity gap for the code C. So proximity gap is this special property that I don't want to talk too much about but it is known for any linear code and this is sort of like the the secret sauce that allows us to um to to do the reduction and here the key idea is to use this this new um definition which is mutual correlated agreement in order to do these sort of folding reductions over over oracles. So mutual correlated agreement is this relatively new notion um of proximity gap which kind of allows us to uh to do these things simultaneously and this was I think first pioneered in base fold and

also used in were okay second in the switching phase um the idea here is that while the prover is going to send some new oracle and refresh the the proximity claim so that now you don't actually have to um uh refresh this proximity claim so that now we're only talking about the new oracle f and here kind of what the verifier needs to do is it needs to check consistency between the original random combination defined over the two vectors as well as just the new vector okay and what it do is it's just going to sample these two points from the original vectors and then it's going to output some new constraint which is an augmented version of the old constraint

so the new constraint basically says well not only does this vector satisfy the old constraint but also it uh at this entry it is equal to this value. Okay. Okay. We can repeat this just a lambda security parameter a number of times in order to amplify soundness. And the important thing here is that sort of these new constraints that we're adding on to the adding on to the protocol need to be batch friendly. Right? In in the future steps of our accumulation scheme, we're going to need to compress these over and over again. And the key idea here is that we want to kind of arithmetize this this constraint essentially by using this uh multilinear extension of the vector um where we can now think about uh evaluation claims at

specific points as actually evaluation claims of the multilinear polinomial on some point in the boolean hyper cube but uh yeah that's just a highle idea of our approach. Cool. So let's talk about some additional extra stuff. So first of all as I mentioned before we we have this new sort of out of domain sampling technique that works for any linear code. So previously out of domain sampling was uh first defined as this sort of abstract tool for improving the concrete efficiency of these accumulation schemes and and succinct arguments. Uh and it was only really defined and used for read Solomon codes.

Um and this sort of outofdmain sample this instantiation of the of the technique is not actually batch friendly. it's not good for accumulation and it doesn't really support linear time proving. So we've actually defined this new um method for out of domain sampling. Uh it looks a bit complicated but really the the thing I want to highlight is that it's extremely batch friendly. If you you can kind of interpret this uh out of domain constraint as another multi-linear evaluation of the of the polomial um of the extension of the code word and this lets us accumulate these sort of proximity claims over and over again.

Okay. Finally I want to talk about uh straight line extraction. So traditionally both in succinct arguments and accumulation schemes uh if you want to get knowledge soundness you have two different approaches. One uh if your code supports efficient error correction then often times you can get a straight line extractor. So this is the case for fry stir and were um but if you don't use a a code that has an efficient error corrector then you really need to rei rely on these sort of rewinding techniques and so this applies to all known practical linear time succinct arguments like breakdown blaze and basefold uh and this is really not ideal because one these rewinding extractors don't

actually run in strict polinomial time you don't really get nice things like UC security with um uh in general like rewinding is lame. We just want to do straight line extraction. Uh and our contribution here is that we can actually show how to obtain straight line extraction for any linear code. And our technique crucially relies on two objects. First is eraser correction which is a sort of different from error correction but it's a property that any linear code provably has. And second we also rely on mutual correlated agreement which is this uh new uh new notion that I described earlier. Okay. Our definition also or our extraction technique also relies relies on some new definition of round by round knowledge soundness which I think uh will be

interesting to people working on succinct arguments and in general I think again these strategies can be used to show that protocols like breakdown blaze and base fault are all straight line extractable um and so I think in the future kind of we'll never have to worry about rewinding extraction for for hashbased both sin arguments and accumulation schemes Cool. So just to summarize uh warp is a hashbased accumulation scheme with uh nice properties like linear time prover the smallest known verifier. The key object that we build here uh is this IR for constrained codes. And we also give some new tools for working with arbitrary linear codes like straight line extraction and out of domain sampling which I think will be uh of independent interest for uh linear time

pre. Cool. And yeah this is on errint. Thanks. Okay. Um, we're a little bit over, but maybe one quick question if there is any since we started a bit late. Is there any question? Yep. Um, can you speak at all about kind of like the concrete prover complexity? Um, I guess you did know, you know, obviously like that it runs linearly. Um, do you have any idea like what the constants are?

Um okay. Yeah. So I think maybe the most important thing is just how many u Merkel commitments it's doing. I think this in general will dominate the the performance of the protocol. Um so for us at every IVC step the prover is going to do two Merkel commitments. One Merkel commitment to an encoding of the the witness for that step of the IBC and a second Merkel commitment to uh the combination or like the the new the new accumulator. like once you combine the previous accumulator and this encoded witness. So if you think about other hashbased accumulation schemes or let's first talk about hashbased succinct arguments uh for hashbased succinct arguments the prover will actually need

to do quite a few more uh merkel commitments in general I want to say like at least three plus the number the oracles that you have to send in your in your proximity test like fry or stir so that's quite a bit as well um for other accumulation schemes like arc it's like uh the progressive 3 um So very roughly I think maybe like uh 2/3 impro 33% reduction compared to arc which was like our previous hashbased accumulation scheme and then uh a bit more compared to succinct a succinct argument approach but okay uh we're working on implementation or hopefully

soon um so I can probably give better numbers then no no I mean I I want to do that as well. All right, we will have to move on. Thank you very much, William.