ZK11: Insights into Practical Folding - Mara Mihali

Transcript

[Music] hi everyone um I'm Laura um and this is yet another talk about folding but today I'm going to try to talk about the more practical side of folding uh namely how we adapted Proto Galaxy to fit in our proving system and aex infrastructure so uh in astec we want privacy which basically means that proofs of user contracts need to be executed client side and should not disclose any information about the statement being

proven so should be zero knowledge and to achieve that um we represent client contracts as circuits um via our um DSL and our aim is to support large client s uh large client circuits something up to 2 to the and to make this even more complicated we want to generate this grps on commodity hardware and in the browser and also we want to give contracts the like functions of contracts the ability to call functions of other contract so something like a function f calling a function G calling a function H all belonging to different contracts so okay so how do we prove this these functions

will be represented in like separate circuits so we need to um prove the validity of this circuits individually and we also need to establish the correctness of the function callstack uh and the fact that like the previous like the recursive verifier of previous proofs return true and this is what we refer refer to as the konal circuit so we need to prove and verify all this stuff um and you might already have in mind because this is a talk about folding that we're going to this is like an example on IVC and okay how can we do this um we can take a naive approach and just do Brute Force recursion we take an IOP and a PCS we take an elliptic curve PCS

because we want fast verification on chain um and we prove each circuit and then we recursively verify it but the problem with this is that you end up with very large recursive verifiers due to the nonnative operations there um uh caused by the PCS you can go a step further and use cycles of Curves because we use b254 so that means we represent group operations from coming from the PCS uh on grumping natively you can go another step further and like do goblinz yeah we have great names um which kind of means delaying like every time you see a group operation you add it to a queue and you delay it uh until later and at the end when you finished

executing or your circuits you kind of you um send this queue to two VMS specialized in um executing scolar multiplications efficiently on grin um I hope people hear me but what if we don't have to do PCS all together and we can do folding um and this give us like a recursive folding verifier that only does logarithmic field work um and we still need to do some group operations but they are constant and we can still Goblin IE them and protal gives us the advantage that we have like no cost implications on the types of circuits being folded and we because clients can write any contract we need

to be able to fold any circuit okay so let's look at the drawing of this to make a bit of sense so this is a case where like we fold only two things at once um so we take function f and function G we fold it we get a nice purple accumulator Cube um then we run what we call the initial kernel circuit which uh basically gets the first folding proof recursive verifies and then some does some other logic then we fold this um then we fold another function H then we run a bigger kernel circuit uh which runs two recursive folding verifiers and some

other kernel logic and we also fold this into an accumulator um and all these circuits if they do group operations um we add those group operations to a que and that Q gets fed into like our two uh big VMS that will produce proofs by themselves as well so in the end we kind of have four proofs because we have to do like a decider proof to check that the last cube is actually like a valid accumulated instance so there we do a PCS IOP and we also need to like send the final folding proof to establish correctness okay so what do we prove with we prove with something called Ultra Goblin honk again great names um

which is blanish arithmetic so we have circuits with custom Gates we have a s Che IOP in the style of hyper plong and we have we use zeror as the multilinear polinomial commitment and these are Concepts that deserve like 25 minutes talks separately um and basically what we do in the proof system we map custom gaze to something we call relations and the wires in the com custom gates are represented as polinomial in these relations and relations are batched in an identity that needs to sum to zero for satisfiable circuits and this is proven bya Su Che okay let's talk about folding with Proto Galaxy first in abstract terms um

so in proto Galaxy we Define this concept of an instance which is a very overloaded term in this field I know and an instance is composed like of of some F and some omega uh where Fe is the commitment of Omega with some commitment function and Omega has some function f with which we can establish its satisfiability and the aim is to fold these instances into like a relaxed randomized version of it uh which we refer to as accumulators um where we relax the satisfiability statement by introducing a power vector and error error some like uh error some Resort and the general

techniques with which we do this is lran interpolation for folding and we also like because the power polinomial is structure we avoid the need to commit uh to Beta yes I explained the paper in the slide I'm sorry about this okay so let's um see what we're folding exactly because we want to like actually fold circuits belonging to that were previously in the proof system um um so this R becomes like something called an Ru where the commitment function is Zer morph and we turn the satisfiability function into what used to be proven by

uh Su uh which is an identity with like all the possible relations that we would encounter like whose gate like whose Gates we would encounter in circuits which are batched with powers of an alpha uh to make sure they're like satisfiable independently and basically the aim is for satisfiable circuit you would have this function evaluating to zero okay um so yeah instead of constructing proofs for this topple we fold them but now the question is okay we have a two Greek letters let's see what these are concretely um so we have the Prov perspective which is sort of so uh the color mapping is

red is information only available to the prover while green is information available to both prover and verifier and Omega contains public inputs contains like the polinomial that appear in the relations which are with have coefficients in like the scaler field and then it also includes some Fiat Shamir challenges and these are the challenges that we use for bding relations and also for constructing relations um and what do I mean by this so in some relations um we have some polinomial that are constructed at proving time and the grand product polinomial is something like an example of this and if we look at the numerator

of it um it's constructed with some challenges that are generated at Pro time at proving time and these challenges also need to be folded uh so that the uh the final accumulator the one that the decider decides has all the information needed to like run the Su IOP so basically like this stle is everything that we need to generate to like be able to run some check and then zero morph and like in the same way um Omega uh fee should be everything the verifier needs to verify approve so we have the public input we have the commitments to the polinomial and again we have the Fatam

challenges okay so how do we represent these polinomial because we use the S based IOP um we represent the polinomial are some evaluations over the Boolean hyper Cube and for a circuit of size n the Boolean hyper Cube will have logarithmic size and we call this representation where all the polinomial are like in evaluation form we call this the execution trace and we Define a row in the execution Trace by fi of Omega um having some value and if we reduce our big relation to like just standard PL having just the arithmetic and permutation relation at the ice index we expect to see like the evaluations of

the polinomial in for example the arithmetic relation at uh point I and these should sum to zero assuming we have an arithmetic gate that satisfiable row I okay so now let's talk about uh the major Proto Galaxy component so we have two big components in proto Galaxy uh that we found interesting to implement and I'm going to go through each of them and talk about the implementation challenges okay first we have if you've opened Proto Galaxy you've seen a polinomial called f we've given names to it because we like names um so basically we're at some iteration of folding and

we have an accumulator and we want to fold some more instances how do we like bind the prover to these specific instances and usually the answer is like we generate some challenges and what happens is basically like we perturbed the power Vector um of the accumulator using the new Fiat air challenges um in such a way that we obtain a univariate that has quite a nice form it looks like it has length n but in fact like it's a univariate of like logaritmic size so it's nice to operate on and the prover and the verifier can compute this the evaluation of this um um polinomial and because of the way the

power power polinomial is structured we can compute uh this polinomial in logarithmic time so there are quirks to it um in our big relation we have something called Global linear relations so we have relations where we want to check do that the sum of the polinomial included in that relation over the entire execution Trace is zero and the log derivative look up is an example of that but the problem is that this power polom the reason why it's here is to ensure that the relation holds at each uh Row in the execution Trace

separately um so what we can do about it is tweak the polinomial in such a way that we accumulate the linearly like the glob linearly dependent relations separately and add them to the constant term to not increase the length of it um and we can do that because like uh pow has a nice structure of being uh one at anything and this holds because you know we are batching this two values together with like a uh challenge with a batching challenge Alpha okay uh so now how do we ensure that like what this round of in would produce a new

accumulator um and that the instances that we've been folding are also valid um we do like what we basically do we do a unitization um of these instances so let's try to enroll a bit of the combiner I could talk 20 minut 25 minutes about how we enroll the combiner but we're going to be a bit quick um so let's look at like a circuit of size two um where we fold only one one instance um these are the two values of the execution Trace if we enroll it in the arithmetic and the St arithmetic and the permutation relation we're going to basically see that like we're like we're

producing relation univariates um rather than like values of relations and these univariates their coefficients will depend on like the values in the execution trace on the instances being folded and you're going to have to believe me that like if we evaluate this polinomial the term that helps us at the challenge um that gives us the error sum of the new accumulator uh given that the new accumulator was produced by lrange interpolation with the same challenge so the problem is that uh with custom Gates you have high degree relations which means that we're producing like univariates of quite High degree and you might so for like a

relation of uh degree D you're going to need d+1 evaluations and in the combiner you're going to get need like approximately hold on a second about uh with that fact you're going to need like a kd+ one uh number of evaluations because the because of the L Ranch bases uh but in proto Galaxy like each instance at each row gives you like one value of pols so how do we get additional evaluations ideally efficiently and the answer is bicentric evaluations which like given any evaluations of a polinomial you're able to get to compute more in O and Time by changing the representation based on

lrange basis um and you need to store uh N squared pre-computed uh pre-computed data but the fun thing about like all these relations Is that their degree and the number of instances we fold are no one at compile times so we can do all this precomputation at compile time okay so we need to send in this stage we need to send some communication that's like dependent of the degree of the combiner um and they are field elements and they're going to impact the communication cost and verifier work and we're going to see that the degree of the combin is some big D multiplied by k

um and D is like sort of the maximum degree of the combined Rel um so if we look at like the numerator that we've seen before uh you think that this is going to have a degree equal to three but then like when we fold it especially because we have to fold um the challenges as well you get to something that's a degree six so it's very important to like design your relations to be like as uh saving as possible and like try to not work work with um powers of challenges in this instance and another like scenario where like powers of challenges like are really bad for you

is remember how you were saying that like we're batching uh the full relation using powers of challenges um when we're combining uh this uh big identity we're basically going to use lrange interpolation for the for this scalers as well and you're going to be in a situation where because you are raising to the power of 20 you're going to have like an degree increase of 20 in the combiner um and this was non obvious it was we have this funny thing where like if our our univariant length is determined and at compile time and you can basically not compile if like you

got the length wrong and I just saw an increase in like it got from like the combiner got from like two digits to three digits and it was because of dispatching so ideally you would have a snark friendly hush function so it's easy for you to generate more challenges and the cost is low for the recursive verifier um another thing is if like if we're thinking about how um Gates appear in the execution Trace if like two instances have the same gate at uh uh different uh in different regions of the execution Trace uh during the combining stage we're basically activating all

these Gates over the entire execution tra so like at each row in the execution tra we're going to pay the degree of the highest ration possible but we can do better than this because we can do sorted execution TRS um which means that we have in the execution Trace we have blocks in which um one specific gate is active so then like in the combined result we're going to like at certain like rows in the execution Trace you're going to just pay the degree of the your highest relation that is active the this is still like something that we're working on the only drawback of this is like you have to fix blocks where a specific gate can be

active Okay so now let's see some benchmarks well no actually we're going to talk a bit about this either and recursive folding verifier so the decider is actually pretty easy you just have to like do a sum check that's uh of like the relaxed identity and the PCS will just validate F the folding um Omega in fee and in the folding verifier well this is like the group operation that it does like the WT witness commitments and the verification key which is like the commitments to the Circuit description and these are not native but you can use goiz let's see some benchmark marks now um so this Benchmark was done on Sunday

on master um for folding only one instance at a time and we have circuit with 2 to the 17 constraint um that are filled like we're we're using all the two to the 17 constraints um and we can fold six circuits in about 23 seconds and also produce the proof of the decider and the two VMS and by folding six circuits like we're folding six client circuits and then all the cernal circuits that we need to fold on top of this and a quick look at like what takes time well folding takes about like 50% of the time and then we're working on optimizing the construction of the circuit and the rest is like sort of small contributions um one after the

other so this is going to be 10 rounds of folding because you're going to have six client circuits and then four Cal circuit Cel circuit um and like sort of the major functions like Standalone functions um that uh like take time as you can see it's the combiner and the commitment function um and the round univ like Computing like we're doing a su check in the decider um so the round univ is also taking quite a bit of time and this is also partially because we do some check ground univariates with high degree uh they are high degree because of the custom gate and if we look a bit at the Proto

Galaxy stage this is just like the time like the percentage is from solely like the Proto Galaxy time um combiner takes the majority of time like the most time the preparation round also takes quite a bit of time the preparation round is like basically you have a circuit and you have to convert it to like the instance to be fold it so you have to compute all the grand product polinomial and commit to the witnesses and generate all the challenges you would have used for the grand product polinomial because you need to fold all of those okay um and this is some ongoing work like we're working on figuring out if we can fold

for higher K and yeah we're integrating the trace work and at some point we are going to fold actual actual nor circuits but I'm going to leave some time for questions [Applause] thank you so much uh any questions then no over there mic is coming behind us that the alpha in the in the

batching that the alphas in the batching how how are are they computed their SPH and miror they compile time okay yeah yeah yeah you you know how many relations you have because that's defined by the the type of the circuits you're going to work with um and you generate all the all the alphas one per like relation uh right before folding and then you you're able to fold those and you gen need to generate like separately for each instance you are folding but we moved to posidon and that's we found um experimental that's quite cheap okay oh yeah we got two questions

right okay take the the closest one there uh thanks for the great talk you mentioned bicentric evaluation and that you had to pre-compute some things at compilation time mhm is that what you were calling later circuit uh constructing the circuit or is that also a different moment um so constructing the circuits is basically going from like wire vectors um to polinomial and we do some like work to ensure nothing is non like nothing is non zero it's basically like that like bicentric evaluation doesn't happen at um in circuit construction so neither does the

pre-computation of what you need for the barric so the precomputation for the bicentric is like partially um computed compile time and like partially we have to do it like when we extend like polinomial cool at run time thanks thank you niik we had another one at the back that about the benchmarks do you know the RAM usage the what the RAM usage um right uh so we it's all about like how many instances you're storing in memory at once um and we found that like with two in like one instance is like

roughly 800 megabytes was it something like that something around 800 megabytes more or less but we haven't um so ideally it would have like 1 to 1.5 Giga of usage uh but yeah that's like another path to optimize like one of the problems with like folding like higher case is that you'll have to store a lot of things in the memory like at once thank you we do have time for another question if someone has one right M was sort of a backup question because it was more relevant to one comment at the beginning so yeah aste cares about uh Pro so clients are

proving because of privacy are there you folks investigating other approaches to that so there are no client side proving example NPC just throw a witness in an NPC and people do something so on so forth that could be a possibly if like if it's efficient it's a matter of like uh non-disclosing any client related information outside so like if you would convert information into like a zero knowledge like some sort of zero knowledge representation it could be possible if it operate fast and like we we haven't thought through MPC cuz it's still a growing field I would say okay thanks