zkStudyClub: Accumulation w/o Homomorphism (Wilson Nguyen - Stanford, William Wang - NYU)

10 May 2024 · 1:03:44

Stanford's Wilson Nguyen and NYU's William Wang present a new accumulation scheme for incrementally verifiable computation that avoids the homomorphic vector commitments prior constructions relied on. Speaking at zkStudyClub, they explain how spot-checking error-correcting encodings lets their scheme rely only on symmetric-key assumptions like Merkle trees, and how bounded-depth accumulation still supports proof-carrying data.

Speakers

Topics

Transcript

uh Hey everybody welcome back to another edition of ZK Study Club today we're very excited to uh be discussing a new paper um with some folks who presented here before uh Benedict Boones and prou Mishra have both presented on this uh you know on this channel before and and their grad students have recently also been or worked with them on on co-authoring this most recent work one of whom uh will Wang of NYU is going to be presenting here today so with that will um please take it away great yeah so thanks for having me um so today I want to talk about some recent work that we've been doing on accumulation or folding and yeah this is Joint with Benedict prou and

Wilson okay size motivation uh let's consider the task of proving a sequential computation okay so we have some initial State x0 and we want to apply like f like a function f a bunch of times to x0 and so one example of this is let's say you know repeatedly hashing um some data and so for example like a vdf you could construct a vdf just by you know do doing a bunch of hashing and maybe you want to prove that you did all of this work correctly okay and more generally we can also consider functions which receive like an additional non-deterministic input so for example example if you want

to proove a BM computation like in this case like f would represent the CPU circuit X would be the current state of the VM and W would be the current instruction and maybe you want to prove that you know X4 is the the result of a running four instructions on this VM from some default initial State x0 okay so formally this is the kind of statement that we want to prove okay and so if you want to have s proce kind of the natural approach would be to use a snark and you know this works but there are some drawbacks so the first is that uh it's not memory efficient and what I mean by

this is you know if you actually consider doing the computation itself you only have to ever keep track of your current state along with like the current input to the computation but when you're actually trying to prove this in a snark it might very well be the case that you need to remember or have all of the States along like all the intermediate values along this computation in your head and so you know if T is let's say a million you need like a million different states uh simultaneously in in your memory and you know ideally there'd be some way to exploit the structure of this computation so that you can also have memory efficient proving so another issue is that also you know for real world evolving

computations the prover often wants to kind of output a proof attesting to the current state of the computation and then later on maybe it wants to run some more steps and then publish a new proof for the new current state of the computation and if you're to kind of just use a snark in a blackbox fashion right you would have to redo the work of proving everything up to that point when kind of the only thing that you should be proving is the most recent step of your computation cool so one way to avoid these drawbacks is to use this technique called incrementally verifiable computation and the idea is as follows uh you have some initial State x0 and

some empty proof which is denoted bot and you have some proving algorithm which takes the the current state and outputs the next state and additionally we'll also output a proof attesting to this state's validity okay and the point is you can kind of do this repeatedly so given the next state and a proof for that State you can generate the the next state as well and approve for that as well and you can kind of do this repeatedly for an unbounded number of steps and at any point in the computation uh someone can verify the current state of the computation just by uh verifying the current proof okay so there are three Key Properties uh for IVC the first is

completeness which basically says that given a valid proof for current state the proving algorithm is always able to generate a new valid proof for the next state okay uh knowledge soundness basically states that given current proof for the current state um there's some way to kind of extract the full history uh of the computation uh such that like everything is consistent okay and the final key property of IVC is efficiency which basically says that the size of your proof as well as the pro and verifier run times should essentially be independent of T and this is kind of the key feature which eliminates the drawbacks uh that I described earlier

when it comes to using snarks directly okay so the state as of like the stateof the art there are kind of two main approaches to constructing IVC uh so the first is like a snark based IVC and in particular we'll focus on like a hash based proof systems um and so yeah so so one advance AG of this approach is that you use hash based cryptography and you know this is very useful for a number of reasons like Computing hashes is very fast on our computers um you kind of free choice over how to arithmetization um and it's also posibly postquantum

okay and probably the big downside of of using like these kinds of snark based ivcs is that you concretely you get a very high recursive overhead and we'll get to what recursive overhead means later but roughly you can think of uh think of it as kind of the amount of extra things that you need to prove besides the the IBC computation like f itself okay and so I have this figure is reported by fractal uh which is essentially recursive fry that says that the recursive overhead for their scheme is around a million Gates okay so the other big approach to doing IBC is from accumulation which is also called

folding and really the big Advantage is that it's incredibly simple so accumulation avoids a lot of this snark Machinery um in fact as we'll see it's like these proof systems are almost ridiculously simple essentially all the pro will need to do is make a single commitment to a witness and then maybe some like basic arithmetic on top of that okay accumulation schemes also have extremely low recursive overhead so I have this figure around like 10,000 gates from Nova which is a very widely used uh folding scheme okay and so the these are great um but kind of the big downside of accumulation is that all current accumulation schemes obviously with the

exception of you know this work and some concurrent work like lotf uh work with group based cryptography Okay and like group operations are relatively slow uh and they also restrict your how you arithmetization your computation and in particular you're forced to use like these large Prime Fields um and there's really no flexibility there as a result your arithmetic is somewhat expensive okay and finally it's also not postquantum so kind of the big overarching research question that we tackle in this paper is like can we get the best of both worlds and in particular can we build accumulation using hash based techniques and the point is we want to

get uh the benefits from accumulation like simple construction low recursive overhead as well as the benefits from hash based uh crypto so like very good performance and kind of a free choice over arithmetization okay and obviously postquantum security as well cool so before we actually get into the our I guess our work I do want to give some background on accumulation schemes just because I imagine some of you and the audience might not be as familiar with it um so so kind of the the goal of an accumulation scheme is to verify a sequence of proofs right we have proofs Pi 1 through Pi n and we want to check

all of them and of course you can always just individually verify each proof but the hope is that somehow you can batch the verification together such that you do less work okay and so the key idea for accumulation is that somehow maybe we can fold these proofs into a run running accumulator okay and only check the final accumulator at the end so in this example here I have like um kind of I have a starting default accumulator denoted bot and a proof pi1 okay and this folding is going to be implemented by an accumulation prover denoted p uh which takes these two things in and outputs a new accumulator

act one okay and you can kind of repeat this process over and over again you can run the accumulation prover on act one and another proof Pi 2 to produce a new accumulator act two okay so you do this for all of the proofs and then finally at the end you run this decider algorithm denoted d uh to validate the accumulator okay and if the decider accepts like ideally this should guarantee that the entire sequence of proofs is valid um and this is not this is not quite true you do need to also verify that each folding step done by the prer was uh was correct okay and this is done by this accumulation verifier denoted V uh and just to emphasize this accumulation

verifier is not testing the validity of a proof or an accumulator it's only testing uh that the folding was done correctly and the idea is that maybe checking validity is expensive but checking the folding itself can be quite cheap and so if kind of the cost of checking End foldings plus the cost of a final validation is cheaper than the cost of just verifying in each proof individually then the accumulation scheme gives you savings cool so there key uh there are three Key properties of an accumulation scheme the first is completeness so given any valid accumulator and a valid proof Pi uh the accumulation Prov will always be able to Output a new

accumulator uh which is both valid and the folding is also correct okay and soundness roughly says uh if you have accumulator in a proof which correctly fold into a new accumulator that is valid then you know that the old accumulator and the proof are both valid as well okay and you can kind of repeat this process recursively so if the decider accepted act two in this diagram and you know that the verification the folding was done correctly then you know that act one was a valid accumulator and that Pi 2 is valid and then you apply the same argument again to act one if Act One correctly folded Pi 1 then you know that Pi 1 is also valid and so by this argument you can kind of recursively

show that every single proof was um was valid okay and the final key property of an accumulation scheme is efficiency which basically says the size of the accumulator is independent of the number of things that you're accumulating and also the accumulation verifier V should be very cheap and in particular sublinear so this sublinear requirement will turn out to be crucial for constructing IVC from accumulation [Music] schemes uh finally note that you know in these accumulation schemes the proofs and accumulators do not actually have to be succinct right so they don't have to be snark proofs they can just be normal narc proofs let's say and in this case

like the verifier will only access a small part of the proof and accumulator in order to um make its decision and this is very important because the fact that we don't need snarks is why accumulation can be so simple right these proofs and accumulators will actually be extremely easy to generate in large part because they their size is linear in the size of the statement cool so how do we actually construct IBC from a cumulation so before we talk about that I do want to go over uh constructing IVC from snarks uh which is a very can I ask a quick question yeah yeah go ahead um can you go back to the end of the slide of the pr

slide yeah um so am I right in understanding that uh the proof might be like the complexity of the proof might be not succinct but because it depends on a small part of the data that's how you manage the sizes of the verifications yeah exactly is that kind of what you're saying yeah okay all right thanks cool yeah and so this is known as um split accumulation I I didn't really go into detail here but um if you're interested like bs21 is the paper that introduced this

idea Okay cool so snark based IVC um so let's consider a snark with aov p and verifier V okay um and we're we're going to look at how to actually construct the IBC prover so first of of course it's going to evaluate the IC function f on the the current state to produce the next state okay and it's going to prove that it computed this step correctly uh just with the snark Prov okay and so the dotted line here just represents the circuit that the snark prover is proving okay and in addition to that it also will prove that the old proof

outputed outputed by the previous step of the IVC computation was indeed valid okay and by this logic you can kind of like chain these proofs together such that you know the final your final proof is implicitly verifying all of the previous proofs cool and so just to reiterate you know the circuit that you're proving not only consists of f but also the snark verifier V represented as a circuit and we say that this uh this additional circuitry uh is the recursive overhead so for snark based IVC the recursive overhead would just be the snark verifier itself cool so this is the construction

of snark based IVC so accumulation based IVC is a little bit more complicated uh we start off with uh a narc PV uh just to reiterate this this doesn't have to be succinct okay we do the same thing as before uh you compute one step of the function and you prove that this step was computed correctly and in addition you're going to fold in the the previous steps proof an accumulator into a new accumulator uh a i+1 okay and finally you also need to prove that you did the the folding correct and so uh for accumulation based IVC uh the circuit that you're proving consists of

the step function f as well as the accumulation verifier uh V okay uh and in order to like verify the the IVC computation what you would do is you would just verify the proof and you would also validate the accumulator um using the decider algorithm okay and so if you didn't completely follow the construction it's not a big deal uh kind of the key distinction between the approaches that I want to highlight is um well uh first of all the narc prover and accumulation Pro Pro will ideally be much faster than the snark Pro and hence an accumulation-based IBC prover should hopefully be hopefully be a lot faster

than the snark based IVC Pro and second our recursive overhead is slightly different so for snark based IVC the recursive overhead was the snark verifier but for accumulation based IVC it's actually the accumulation verifier and ideally we can make the accumulation verifier much smaller than the snark verifier and this is what allows us to kind of minimize the recursive overhead um of the computation and these two facts together are kind of what really makes accumulation based IBC so powerful cool so if accumulation explained we can finally talk about our contributions so first we show how to do accumulation from symmetric key Primitives and in

particular just hashing um and this is with the caveat that our accumulation scheme only supports floating a bounded number of times okay and this property is not captured by existing definitions it's a bit weaker and so because of this we also need to introduce a new definition uh which we call bounded depth accumulation which captures our construction so again bounded depth accumulation is weaker than normal accumulation but nonetheless we'll show that is actually still sufficient for constructing IVC and from a theoretical point of view the IVC that we attain has a lower ASM totic overhead compared compared to the prior state of the art so in particular um fractal which you can just think of as recursive fry as

this recursive overhead o of Lambda * log s n and we eliminate a factor of log n and replace it with this uh D um which you can think of as like a small constant okay and finally we also give some optimizations that we believe should significantly improve the concrete performance of our scheme and so I I'll I'll briefly mention the optimizations at the end of the talk as well all right so let's actually get into how to construct our accumulation scheme so our starting point will be an existing accumulation scheme this can be Nova protostar or kind of like anything else that's been proposed before but for the purposes of this talk let's like

stick with a concrete example uh which will be like a slight variant of Nova so we'll consider this a mented R1 CS relation uh where the instance is like some matrices ABCD and the witness is a vector Z and we'll say it's valid if az. bz is equal to cz. DZ where this dot is the hadamar product okay and of course in R1 CS there's also like a small portion of the of Z which should be part of the instance but for Simplicity let's just ignore this okay additionally we'll also make use of a Pon commitment which essentially just map a vector Z to um a group element in a cryptographically

hard group and kind of the the key feature of a pedison commitment which will use in accumulation is that it's homomorphic namely for any two vectors right the commitment to their sum is equal to the sum of their commitments okay so let's talk about kind of what proofs we're actually going to accumulate and what you'll see is this is kind of like the like a ridiculously simple proof it's probably like the dumbest thing you can imagine so what the pro is going to do is okay it's going to commit to the witness value Z to get a commitment z bar okay and it's just going to send Z and z bar over to the verifier and and the verifier is going to literally just compute the augmented R1 CS relation it's just going to check

it itself and it's also going to check that the commitment is indeed opens to the to the that Vector um and so the Commit This like this whole commitment see this commitment thing might seem a bit Superfluous but uh it will turn out to actually be useful for accumulation but this is just like the core narc that we're going to be who proofs that we're going to accumulate okay so in order to accumulate we also need to define the accumulator so first recall that like the proof consists of a vector as well as its commitment you know such that uh it satisfies the r1c relation okay and then and an

accumulator will look quite similar it will consist of a vector W and it's commitment W bar plus a new Vector e which will referred to as the error uh and its commitment ebar such that um aw. BW minus cw. DW is equal to e rather than zero okay and remember our goal is to somehow fold a proof and an accumulator into a new accumulator cool so what does this accumulation protocol look like so at the start the pro and verifier both have the accumulator AC can and the proof Pi okay and kind of the natural thing to do to produce a new accumulator is to

you know take a random linear combination so the new the new accumulators W will just be like a random linear combination of um the old w and z okay and if you try to compute what like the corresponding error term is um you don't actually have to like look at this equality the point is that it's actually just the new error term will be equal to the old error plus Alpha times a bunch of cross terms which will call T and so the prover will just like first compute t uh as well as commitment and send it to the verifier the verifier response with the the random challenge okay and the prover will now compute WP Prime and E Prime as well as their commitments and this constitutes the new

accumulator act Prime okay the prover will send this back and the verifier will check that um kind of the prover computed the new accumulator correctly and it does so by checking the linear relation um and one key detail is that like it's only going to check this linear relation over the commitments but since the commitment scheme is binding this somehow enforces that the linear relation holds over the underlying committed vectors okay and in this way you get like a verifier that only touches the commitments and hence is uh sublinear cool and so just for completeness I'll also describe the deci the deci just checks the equality for

the new accumulator and it'll check that the commitments indeed open up to the desired vectors cool so I've described this as a kind of an interactive protocol but you can always make this non- interactive by applying fat Shamir and in this case like T Bar and Alpha would constitute the accumulation proof all right and so if you didn't follow this entire construction uh that's also not a big deal because for the rest of the talk we're really only going to be focusing on a small part and namely it's like this this pink box okay and the reason is because this pink box is the only place where we actually need to take advantage of the

fact that the commitment scheme is homomorphic right so recall like the accumulation verifier needs to check that the linear relation holds over the underlying committed vectors and so when it has a homomorphic commitment it can just check it literally by Computing over the commitments okay um but the fact that we have these homomorphic commitments is kind of why we need to rely on group based cryptography and you know these are kind of the the things that we want to get rid of and so for our first attempt actually so so this is what the accumulations looks like for like this modified Nova and for our first attempt okay um let's just get rid of the peton

commitments and we're just going to replace them with Merkel tree commitments okay so so all I've done here is i' I've just changed every place where I use a Pon commitment to Merkel tree and now the commitments will just be the roots of the Merkel tree okay and because of this we can't actually do the the homomorphic eval evaluations anymore over the commitment and so well completeness is the same as before like if an honest PR just does everything according to the protocol then everything is accepted but for soundness we we really need to test this linear relation right because it might be like might very well be the case that um the a malicious prover commits to a w Prime which is totally unrelated to the

original w and z vectors right you really do need to check that W Prime is equal to W plus Alpha Z in order for for soundness to hold okay so let's focus on specifically uh just checking this uh linear relation okay so as before so we have like um three commitments uh and we want to check that the underlying committed vectors uh satisfy this linear relation namely like the first one is equal to the second one plus Alpha time the third one okay and because we can't really do anything with the commitments itself uh we actually need to um do a bit more work so one idea is okay let's just sample a bunch of random

locations on this Vector okay I've just randomly chosen a bunch of indices and call this set Q it's a query set okay and the verifier will send this to the approver and the prover will respond with the the claimed values at these locations across all of the all of the vectors um along with like opening proofs so for merel tree this would just be like a Merle path up to the root of the tree okay and the verifier will check that indeed like these opening proofs are valid and finally it will kind of like check this linear relation element wise so for each index I that we've queried it'll check that the I element of w Prime is equal

to the I element of W plus uh Alpha time I element of Z and the hope is somehow by like since we are randomly sampling the location like intuitively that means that most of the locations should be consistent otherwise you know we would have just randomly stumbled upon one of the inconsistencies okay so formally we can just consider like suppose like a Delta fraction of the locations across these vectors are inconsistent with each other then if you make t queries then um they will all like pass with proba like one minus Delta to T so basically each of the queries needs to avoid like in order for the like a malicious Prov to exist

to succeed each of the queries would need to not hit the inconsistent locations okay and if this is like some inequality but like if you set T to be equal to the security parameter divided by Delta then you can show that this probability is negligible okay and in particular if you only if you want to guarantee that a constant at most a constant fraction of locations are inconsistent then T will be like o of Lambda and you're happy because your accumulation verifier is only sampling very few points so there's a problem though which is like how do you detect a single inconsistency so you can imagine like maybe there exists some invalid proof

which only differs from a valid proof at a single location and from the verifier point of view the only way they can distinguish these two cases if is if uh it actually queries this location where they're inconsistent but if only like one out of n of the locations are inconsistent then you effectively would need to carry every single location in the in the vectors in order to check this and that kind of defeats the purpose of accumulation right we want the accumulation verifier to be extremely small and therefore it only should only be able to query a small number of locations and so it seems like we're stuck right because we don't want to make too many queries but if we don't make enough queries then the prover can

always sneak in a few inconsistencies that could like totally ruin the proof okay so to get around this we're going to introduce a new tool we're going to use airor correcting codes um and just in case anyone is unfamiliar with them I'll just like give a brief overview of what air correcting codes are sorry will can you go back I actually had a quick question on the last slide so I guess like the problem you highlighted actually is worse based on the number of rounds right so like if you're doing this round by round like the more rounds you have the potentially more the more yeah yeah yeah dangerous this problem is is that the way to think of it yeah so so for the purposes of like this current example like it's already totally broken with one round but but

you're right like round by round um kind of you would be able to inject even more inconsistencies into the proof yeah you're totally right and this is this fact will actually become relevant for our final construction um but yeah I'll I'll get to that in a sec as well thank you cool okay okay so error correcting codes um so an error correcting code is just like simply it's just a mapping from n element vectors which we call messages to L element vectors which we call code words and generally the code words will be much longer than the messages okay and the key property of a code that we want to make use of is the distance and the distance of a code just

refers to kind of the minimum uh Hamming distance between any two code words where Hamming distance just refers to the number of ENT where like two vectors are not equal okay um and error correcting codes should also support uh efficient decoding namely given a noisy code word can you recover the original message so let's say we have like a message and we encode it in the code to produce a code word and I'm going to corrupt some of the locations in this code word uh so here I've just corrupted at two locations and I've just replaced um replaced the entries with like some arbitrary field element is there a way to go from this noisy code word back to the original message that we started out

with and an error correcting code is useful if you can do this uh in particular for like a large number of Errors so we say that the unique decoding radius is equal to the kind of maximum number of Errors allowed cool and finally we'll also be interested in linear codes so linear codes are essentially just linear maps and so you can just imagine C being implemented by some sort of Matrix Vector multiplication okay and so many many examples of air crating codes are already linear so this is not really a big requirement and we'll be interested in linear codes with large distance like a large constant fraction distance uh and

for example like a read Solomon code uh will satisfy this property like just essentially optimally um yeah and so so when I talk about codes you can kind of just imagine a read Solomon code that Maps a message like of a length n to a code word of length 2 N let's say cool so again this was our first attempt at doing like hash based accumulation where we just replace the the pon commitments with Merkle Tre commitments and as weall like this didn't work so what we'll do instead is instead of committing to the vectors directly we're going to encode to like we're

going to commit to encodings of vectors okay so I've highlighted them in blue but just everywhere where we like committed to just like a normal Vector before we'll we'll first compute the code word for that vector and then we'll do the meril Tre commitment over the code word okay and everything else is the same as before okay and now to kind of handle this uh linearity check that's like crossed out in red right now we're going to engage in in the spot check protocol I described earlier so first the verifier is just going to sample a bunch of random locations okay the appr will respond with openings and the verifier will just check the opening proofs and also check

that the linear relation holds element wise over all of the locations that it queried okay and so completeness actually um follows from the fact that the code is linear like namely we're testing the linear relation over the code words that are being committed to but actually like if if the original vectors were um satisfied the linear relation then so must the code words cuz see it's linear it will just distribute over the addition and scalar multiplication so we're good with uh completeness and soundness uh kind of crucially relies on the fact that we can um do this spot check uh and not have the proof or cheat somehow and so I'll

give kind of like a very brief and formal soundness analysis but it should hopefully just convey the intuition for for why this works so let's say you have like three committed vectors and you want to test the linear relation between them and we'll just call the underlying vectors A B and C and it's important to note that kind of a b and c do not have to be code words right for an honest prover they will always commit to code words but you could imagine a malicious prover that you know just commits arbitrarily to whatever Vector it wants and so really these are just vectors now the decider guarantees that the the final code word a like the random linear combination is actually a code word so we do know that a is a code word and the

verifier guarantees by the spot check um assuming that you set the parameters correctly that the hemming distance between a and the the purported linear combination B plus Alpha C is at most Delta far from each other where Delta is like some constant fraction like let's say 1/4 and and this immediately implies of course that the since a is a code word that this purported linear combination is also Delta close to the code okay and kind of intuitively since Alpha is just a randomly chosen field element you want to say that well if B plus Alpha C is Delta close then like with high probability then B and C must also be Delta close to C because

otherwise if if one of them were far away then if you just took a random linear combination presumably the result would also be far away from the code and you can like formally prove this using the so-called proximity gaps for code uh there are a ton of them out there um but like for example for Rolan codes we have a lot of very useful proximity gaps um and so if we just take this at face value B and C are Delta close to C then we can actually conclude that the decodings of a and the decodings of B and the decoding of C satisfy the linear relation that we want okay um and the point is like if a is a perfect code where B and C are only slightly

noisy if they obey the linear relation over the vectors then once you decode them it should also just obey the linear relation over the decodings and I mean in our paper we give like a a better proof using like a more um precise proximity Gap statement but just as like a simple example for like confirming this intuition you can imagine if you encode both sides if you encode the left hand side you just get back a which is a code word and if you encode the right hand side you get like a code word which is um like two Delta away from B plus Alpha C like bi triangle inequality and so you know and since you know that A and B plus Alpha C are also Delta close again by a triangle inequality You can conclude that like

the right hand side encoded and the left hand side encoded are three Delta close to each other and if like assuming that three Delta is less than the distance of the code this must this imp that you know these two code words are actually just equal and hence the decodings are equal okay but yeah this is just an intuition and the key thing I want to focus is focus on is you know by doing this error correction we are able to recover the homomorphism check over the decodings right like decode a is equal to decode B plus Alpha time decode C this is like the key um fact that we want to use in order to like show that the accumulation scheme is sound but

there is one issue which is namely that even though a is a code word our guarantee is not that being here code words it's they're only Delta close to the code right so they're slightly noisy and in general you can imagine that like um you know for the first for the first step of accumulation if you have a valid code word then what you guarantee for the previous step of accumulation is something that's slightly noisier and it turns out you can like run the same analysis again on the step before that but then your only guarantee is that like um those code words were two Delta close and so on and so forth like three Delta for Delta and in general like if you want to accumulate K steps then kind of the oldest proof or

oldest accumulator uh will be noisy like with like K Delta noise and as soon as this like noise exceeds like uh the unique decoding radius of the code it's kind of meaningless because you can't make any Claim about the underlying coding satisfying the linear relation and so kind of just to like wrap it up in order to support D accumulations first of all you mean you're going to set your spot check parameter Delta to be some constant such that D * Delta is less than the unique decoding radius okay and the point is like this this accumulation scheme would therefore be able to support D steps I do want to note that this also like uh corresponds to like a real world attack like if you set your parameters

such that your accumulation scheme only supports let's say 20 steps of accumulation and you try to do actually 21 steps it turns out there's actually like a malicious prover that can break your scheme and like fold in an invalid uh proof and roughly speaking the way they would do it as Alex mentioned before is they would just try to inject to the inconsistencies just a couple a couple locations per per accumulation step but the point is like after like 21 accumulation steps then kind of the entire code word has been or the ire Vector has been Rewritten to be like some unrelated valid code word cool and so this notion of accumulation where you can only support a bounded number of steps is not again it's not

captured by uh the definition that I described earlier so it does need a new definition and we give this in the paper uh we call it bounded depth accumulation and informally it basically says okay so this is the original accumulation scheme definition so if an accum if an old accumulator correctly folds into a new accumulator and this new accumulator is valid then you know that the old accumulator is valid and what we're going to say is something slightly weaker if the old accumulator folds into a new accumulator and the new accumulator is valid then the old accumulator is still valid but it's like slightly noisy and formally we say it's just accepted by a weaker decider like a less stringent decider which we denote D1 and we can do this just in general

for like some DK uh if like if things correctly fold into uh something accepted by DK then the only guarantee that you can make for the the old accumulator is that uh it was accepted by even weaker decided DK plus one and you say that okay well this this uh implication only holds while K is less than D and so this is kind of like the flavor of definition that we give for bounded depth accumulation cool okay so for the rest of this for the rest of this talk I want to focus on I guess how to build IVC from uh bounded depth accumulation so this diagram here is just what like a IBC from normal

accumulation would look like and for us kind of everything Remains the Same syntactically like you can just plug in our accumulation scheme into this construction but the key issue is that if you have bounded depth accumulation then your resulting IBC scheme is also bounded length in the sense that you're only able to prove a bounded number of steps so if you set your parameters so that your accumulation scheme only supports 20 steps of accumulation then your IVC only supports 20 steps of computation okay and this is like quite useless right because in practice you know we want maybe we want our IVC to do like a million steps of computation and it would be kind of unrealistic to set our parameters such that you know your accumulation supports a million steps and again if you exceed this length

bound it corresponds to a practical attack the one I described before so the key problem that we still have to address is how do we construct like a useful IVC scheme which supports like a like a lot of steps from Bound in depth accumulation and the way we do this is actually largely taken from prior work um and so they get they talk about this within the context of like a theor like theoretical consideration but for us it actually turns out to be useful for actually practically constructing IC and so idea is as follows um so for normal IBC you can imagine like a proof like you have a bunch of provs and they're kind of aggregating

proof in a line right and so if you have t t steps of the computation you need to aggregate like T times and so the idea is quite simple we're just going to do like a quotequote tree based IVC approach where we um instead of aggregating a on a along a line uh we're just going to aggregate along a tree okay and this the depth of this tree is going to be log T and the point is you know if you um only do log T aggregations well like you know let's say you set the depth to you set your depth to be 128 then you can support like two to the 128 um you know steps of your computation which is like more than

enough and the point is you only need to do uh 128 accumulation steps because you only ever aggregate proofs like log T times um this does require generalizing our accumulation scheme to kind of accumulate multiple accumulators and multiple proofs at once but um this can be done and we show in the paper um and this technique also just generalizes to higher arities so in this picture I've depicted kind of a binary tree but you can imagine a tree where every node has like three children or five children or in general just m children and if you have RDM and depth D then this means that you can prove m to the D steps okay so I've called this tree

based IBC but if you actually look at the literature it's there's like a more general form of IVC called proof carrying data PCD uh which kind of is this concept that I'm describing here um yeah but I I mean I'll just stick to like kind of a high level overview of what's going on and so the again the key point is that the depth is small and therefore uh we can instantiate our bounded depth accumulation with that depth while also being able to like uh prove a bunch of steps okay so I also want to talk about like how you might actually practically construct this IVC scheme uh and the issue is that like our accumulation scheme uh the cost grows

with the depth D and so ideally we probably want D in practice to be quite small like let's say two or three and so if we actually wanted to implement an IBC scheme uh the way that we envision doing this would be to essentially use our tree IBC with our bonded depth accumulation scheme for like a decent number of steps and then run a kind of a snark prover on top so this prover this snark based IVC on top so this prover is just going to prove that well this tree IVC was correct and then we're going to generate a new tree and then we're going to have this Prov recursively prove that you know the old proof is correct and this new tree is valid okay and we kind of continue this process and in this in this sense we we we again get

IVC uh we do rely on snarks but the point is that the snark prover will only run once every m to the D steps so realistically like let's say we set m equal 16 and the depth of our accumulation scheme to be three then this means that our snark Pro only needs to be run every like 16 cubed or like 4,000 steps and hence like you know the amortized cost is actually you know quite low so this is this kind of construction is what uh we imagine um our accumulation scheme slotting into and sorry well just so I make sure I'm following the the choice of aity right has to be less than the D not d as in depth but like the um you know your in

terms of your decider like the threshold of weakness right right so your aity has to be greater than that or I'm sorry less than the at point at which the individual scheme breaks no so theity actually we kind of just have free choice over aity so you can just use actually any like polinomial sized aity um and everything works out I mean this is kind of what why um I guess bounded de accumulation is still useful yeah gotcha so go back I motiv motivation right question can you go back a few slides sorry I'm just trying to think if you're following this could keep going back uh one more Yeah so basically I guess what I'm asking is the aity

related to the the the depth bound but s like it's not yeah they're they're largely independent I mean there's the aity does contri contribute to soundness error just in like a very negligible sense but like the picture I've described here like it's independent of aity essentially because like you're taking a random linear combination of two things you know you might as well take a random linear combination of three or five things and kind of the guarantees that you have stay the same okay got it okay okay thank you the other way around the higher you make the aity the lower depth your tree will be right it's only the depth of the tree that matters for this attack go back to the

other oh okay so I was thinking this is theity but it's actually the depth okay yeah right yeah aity means how many like right like one note how many leaves or per uh how many children each notes has and it's basically instead of folding two things together we can fold M things together it makes the folding verification a little bit more expensive right the the folding verifier is linear and M but it it really helps uh like you could imagine M like 16 or something it really helps with uh lowering the depth of the tree got it helpful and uh Dara I think just commented uh hidera by the way it's uh yeah it's so pretty that the

theoretical consideration about accumulation depth turned out to be useful for practice answered my question um I don't know if I asked your implicit question but if I did that's the first time and probably the last time in history that I will have ever asked a DK question um by accident so it was it it was the whole um conversation that that answered the question but yeah it was how does the um the concrete um sort of um uh security theorem depend on the um depth the parameters of the tree cool yeah yeah so again just to note like this kind of tree based construction is like in the past it was largely theoretical but if you were to actually implement the scheme you would want it and so um I mean actually this

is relevant to optimizations basically uh there's kind of a lot of um ways that we can try to uh optimize the tree based IVC Construction in order to get like significant uh concrete improvements okay so I think we're running out of time so I'll just like briefly go over these optimizations oh yeah and we'll just just to flag so we have technically to the half hour I don't know if you can go beyond the hour but yeah we technically have 30 minutes left with the session if you can go we can continue so don't feel rushed if you don't have a okay I see um yeah so so recall that you know when we're doing

the spot checks we want to query you know each Vector at a bunch of locations but actually like these locations are all the same across the vectors right uh because we want to test the relation element wise and so one idea is like okay you know if I have three commitments and I'm doing three queries to each commitment then this requires like nine Miracle tree paths but maybe there's a way to do better than that and the idea is actually pretty simple if we can somehow prepare w and z in advance simultaneously then we can just like commit to both of them at once and just like make the leaves of the Merkel trees like a tuple of elements okay and the point is well you know if you want to quy at this location

we just need to open the path once and you you've recovered like both of the items and so in this way you can kind of reduce the number of Merkel tree openings that the accumulation verifies has to check okay yeah again so if you want to commit to M Vector simultaneously instead of having like a multiplicative um multiplic multiplicative growth and cost it's actually just additive okay uh so the second optimization is a little bit more involved so I just try to briefly explain the intuition but recall that we're trying to like construct this so-called IBC tree for the IBC step function f um and the idea is basically well the leaf

nodes of the IVC tree are going to actually prove F and the kind of the internal nodes of the IVC tree are just going to aggregate the proofs together and in this sense it somehow like wastes proof space because you're not actually proving anything about F in the internal nodes and kind of um since like your proving needs to be uniform it's just essentially like proving garbage uh for no reason and so the idea is okay let's actually just accumulate the proofs for f separately and we'll use our IBC tree not to verify F but to actually just verify the accumulation verifier okay like that's a very rough intuition but this is kind of the idea of like what we want to do and the point

is that um you can kind of get significant savings like um like a factor of M essentially because this technique eliminates the the wasted proving F cool and of course like you can just see the paper for the details um uh for all the optimizations as well yeah okay so just to conclude uh so I guess the main takeaways that I want to give are first like we construct bounded depth accumulation for NP using basically just hash based crypto and we do this at a high level by kind of emulating the homomorphism using um error correcting codes and spot checks um and from a theory point of

view we show that bounded depth accumulation suffices for constructing bounded depth PCD which is like this the the tree construction and this inter implies poly length IVC by some prior work okay and we we find like ASM totically our IVC scheme also has or our PCD PCD scheme has a smaller ASM totic recursive overhead compared to the state-ofthe-art in terms of hash based PCD cool and for practical constructions uh we give some optimizations and kind of it's an open problem like we're working on this right now just in terms of implementation and stuff like how to actually set the parameters such that um you know we get the best performance possible um but

we're pretty optimistic that um you know these techniques will translate to you know real efficiency gains for doing IVC and uh just when you say parameters you mean like this is like the aity and the depth yeah exactly like the aity the depth like at what point do you want to start um doing the snark proving on top yeah that sort of stuff cool uh yeah that's it thanks um and you can find the paper on ePrint uh this link uh okay awesome thank you very much uh will this is a great presentation um I guess we can open it up for questions

does anyone have questions for will um not so much of a question but but own observation um so the the so you're using merel trees in a context where um you can you have a um a bound on how many times um you can do something that reminded me of sphinx where your um which is the the postquantum um signature scheme that I was involved with um and there you you construct um the overall signature scheme uh in terms of few time signature schemes which are which are insecure if you have if you use them too many times so I need to to kind of check

um you may have already done all of the uh optimizations from that context but um yeah I mean I don't know I'm Noto familiar with SS I mean sounds intriguing um yeah I mean it's definitely the case that you know maybe there are more optimizations to do here um I don't yeah I I I wouldn't really yeah I I mean snx was basically um sort of uh designed by um throwing as many orthogonal optimizations together as possible um yeah uh any other questions for

will yeah just a quick one so just to make sure understand so the recursive of red you would end up getting for the scheme is verifying a feral path which is proportional to the the the distance parameter that you set uh plus one F rage roughly plus a few like linear field operations correct yeah yeah yeah yeah exactly that would be the rep and the as you will be using for the Merkle trees I assume that to you would also need to use you try to use something like posidon to also further reduce the recursive cost of that I guess right yeah I mean it would definitely help right cuz yeah again like the accumulation verifier like the only thing that accumulation verifier actually needs to do is be represented

as a circuit so yeah it would be like using a circuit friendly hash function would um I think yeah give you a lot of savings okay it's actually an interesting case where where you might want to use um something like uh um what are they called the reinforc concrete ones like bricks and uh uh break brick and mortar or something there's like basally this family of has function which are both or like the now the newest families of has functions are both circuit friendly but they're also fast on CPUs right because the the most costly operation unlike in a group based SAR is now actually the hashing so you care both about the circuit friendliness

and about it being fast um but it seems like at least there proposals for hash functions that get you the best of both world hopefully they're also secure yeah there's a recent one that is um um using the the um Tower binary field um construction I I haven't checked how it compares to others um to complete on J's question like the requirements for function are to be Collision resistant I guess but I was curious to know whether if you change from sort of the linear uh folding to the sort of tree part if the

requirements for the ash function concretely change there are like other types of attacks that you can have because things are done in parallel rather than sequentially when you fold things together yeah um I don't think anything changes I guess all of these things are um like we prove our accumulation scheme in the random Oracle model so okay it's secure with random Oracle and then I mean presumably if you just use like if it's just Merkle trees and that's all you care about in terms of like your your guarantees then it should be fine once you instantiate it even if they're yeah but um yeah I mean I guess the way we prove it is we prove the accumulation scheme is sec in the random Oracle model then we apply fat Shamir to get an accumulation scheme in standard

model and then we do like a proof that like PCD and IBC bill that is secure so uh I don't know I I think it should be fine thank okay maybe if I have another question not sure M I still add something no it's all good thank you okay so have you given some thought on like instantiation with like different like uh maybe not F friendly Fields small fields and different codes like it seems to me that for the you only use Solon mostly for the uh the linearity property efficient quity and good distance

and then because you have a strong proximity Gap all so it looks to me like the construction could very easily be ported to smaller field different codes course then you don't have the strong proximity gaps but you can do other things so we do give like an alternative con okay so yeah I guess first of all for the accumulation construction I described here you you actually could just replace it with um I think like even arbitrary linear codes and there's like a good enough proximity Gap um for the general case when we're trying to fold like multiple accumulators in multip Pro multiple proofs at the same time the random challenges won't actually be uniformly distributed in that case you do care about like specific Pro proximity gaps for specific you know

correlations and there that's why we use read Solomon but in the paper we do give like an alternative construction that's slightly more expensive but again and that one actually just works over um for arbitrary linear codes because essentially it's just going to make uniformly random uh linear combinations yeah that's like six and you could also use tensor I guess and that also gives you a there are opportunity G for General codes in that sense for Tor challenges and you can probably use that yeah yeah I wonder if there like any like uh you know uh any like significant obstacle to getting like to a beus like accumulation scheme but it does not I

don't so I mean I think it's mainly just because uh you know we're not as familiar with it but I don't I don't think there's any sort of like fundamental obstacle to to getting that I mean this is kind of the nice thing about these accumulation schemes is they're so dead simple and all we do essentially is replace the homomorphism with this linearity check and as long as uh and yeah we show that uh so so the key technical tool there is this proximity Gap and we show this works for arbitrary linear or we we have a construction um where we can use a proximity Gap result um for arbitrary uh for arbitrary linear codes so we can

work with any arbitrary linear code linear time encodable ones like the breakdown code uh you know vus things over binary Fields probably um uh there really is no yeah no limits the there's a footnote in the paper saying um we only claim plausible postc security uh as we prove our construction the random arle model instead of the quantum random arle model um is that just we haven't proven this yet um um yeah I mean it's basically just um no it can be done I think it's actually pretty straightforward so there's some existing so you can

rephrase our accumulation scheme as kind of like this just general interactive Oracle proof that's round by round sound and there are these like there's this paper by uh km manahar and Spooner that kind of show how to just generically proof that these kinds of things are secure in the qyr and so I I think you would just be able to do that okay thanks cool uh darl you still have your hand up I'm assuming that answer your question I just didn't know my hand just make it

sure is that oh is that this paper that I'm putting in the chat or is that something else uh soorry what were the auth this again um um no that's that's probably a different paper um yeah referring to is K manoir sponer 2020 if I remember correctly yeah I forget the title but it's like yeah uh succinct arguments in the

quantum random Oracle model uh I just pasted in yeah thanks cool uh anyone else have any questions on this paper on this talk questions for will Benedict okay well thank you very much everyone for being here thank you will for presenting uh this is a really great talk uh thank you for coming on CK Study Club today yeah thanks for having me