ZK Whiteboard Sessions – Module Fifteen: Inner Product Argument in Halo 2 with Ying Tong
15 Nov 2022 · 59:08
Cryptographer Ying Tong, a contributor to the Ethereum Foundation, Electric Coin Company, and 0xPARC, walks host Brendan Farmer through the inner product argument at the heart of Halo 2 in this ZK Whiteboard Sessions module. They cover the Halo 2 polynomial commitment scheme, atomic and split accumulation, and how these zero-knowledge proof techniques are used in Zcash.
Speakers
Topics
Transcript
foreign [Music] welcome to another episode of the ZK whiteboard series presented by ZK hack I'm Brendan I work on ZK stuff at polygon and I'm really excited to be joined by Ying Tong who is a very talented cryptographer and engineer who currently works at the electric Coin Company she also collaborates with the ef-0x park and is involved in a lot of cool things uh in the zika crypto ecosystem so welcome thanks Brandon um hi everyone so today we're going to
talk about Halo 2. which is a proof system that allows for recursive composition without a trusted setup so the first thing we're going to do is a high level overview of Halo 2 and then we'll zoom in on sort of the back end part of it which is the inner product argument and the accumulation scheme so Halo 2 starts out at the front end with what is called arithmetization and this is the process of taking a bunch of values and constraints on these values and and coding them as low degree polynomials so for Halo 2 we've chosen
the Planck arithmetization and this is a highly expressive and flexible way to express things like custom constraints equality constraints and even lookup arguments so um Planck gives us our circuit in the form of low degree polynomials and this is then input into what we call the multi-point opening argument so the multi-point opening argument um involves committing to these polynomials
evaluating them at all the required points and then constructing a polynomial that checks the consistency between the commitments and the evaluations so it is the polynomial produced by the multi-point opening argument that we then input into the inner product argument so the inner product argument is a polynomial commitment scheme and it's a particularly good one for the purpose of building an accumulation scheme and the reason is because um the inner product argument has a
succinct accumulation verifier and we'll see what this means later on but you can think of it as a verifier that has both a succinct part and an expensive linear time part so in the context of recursion we perform the succinct check at every recursive step and we delay the linear time expensive check um so that it's amortized across a batch of recursive proofs and then yeah so basically what I just described was
um an accumulation scheme um right now we're using or what's called an atomic accumulation scheme um yeah so we're gonna focus on number three and four um because I think plonk has been covered very well in another session already yeah yeah so we've looked at Park um oh that that sounds good so so the if we think about like what Halo 2 is we start with uh our program or the thing that we want us to prove um arithmetize it uh commit to it or arithmetize it uh perform an IOP that depends on like the
opening of some limited set of polynomials prove that those no meals can be opened and are sort of being evaluated correctly and then when we want to do recursion we have this really cool um approach that uh yeah the the sort of like uh I I think we'll obviously get into this later but it was like it's really like groundbreaking step forward for workers approves yes definitely so the inner product argument is a polynomial commitment scheme and um we should first start with looking at its API so what what it takes in is um commitment
to a polynomial so purportedly C is a commitment to some degree and polynomial p and then it also takes in some challenge point at which this commitment is opened and lastly it takes in v which is the value that we're claiming the commitment opens to at X so we're claiming that p x equals V and we're also claiming that um
C is the commitment to an in Halo 2 we use the Pederson commitment so we're claiming that um C is the result of an inner product between the coefficients of P and the some fixed bases G which are part of the public parameters so so you give me a group element and you say I claim that this is the commitment to this particular polynomial and I say okay prove it I'm going to give you some random X and you're and it should like if it is in fact the
spinomial or if it Bears this relation to these other polynomials it should evaluate to G or to start to V and and so the iPad just allows us to prove it exactly so and in particular the proof of the IPA is succinct um in in the sense that it's logarithmic in the size of the polynomial we're coming into so to give you a preview um the proof consists of a vector of group elements l a vector of group elements are and each of these are length K where k equals log n and it further consists of a group
element um g0 as well as a field element P0 and uh we'll we'll learn more about we'll learn more about how this proof was produced as we go through the rounds of the inner product argument so yeah I think we're ready to get into the inner product argument um the inner product argument um is trying to convince us of these two statements um and we can rewrite them um we can rewrite them slightly so uh we we've written c as an inner
product of the coefficients of p with our fake spaces G and similarly we can write p as an inner product between the polynomial p uh oh sorry this this should have been V over here whoops um the polynomial p and some polynomial B and B here is simply um the powers of our challenge point x so yeah you can see that uh the inner product of the coefficients of p with B
is the same as just evaluating um p and X right you guys recall with the inner product we multiply like sort of a element or entry-wise or element-wise yes exactly a DOT product yeah okay so these are the two statements of Interest the two inner products of interest um and we can sort of combine these two expressions into a single one let's call it CK so remind reminder K is log n and we're going to proceed the inner product argument in K rounds um and the first in the case round we
start at the kth round with c k equals C plus v u um yeah so now we start let's start with our polynomial P which has n terms um and I'm going to index it k we're in the kth room here all right and then I'm also going to put here the polynomial B which is just um the powers
of x b k and we also actually have GK which is the vector of our fixed bases um but I don't have space for it here and furthermore um it behaves very similarly to B they're both like publicly known and we're going to treat them very similarly so in the kth round so our strategy for each round is to gradually try and shrink the size of the polynomials until um at the zeroth round we're left with um constant polynomials so single terms yeah
so I'm sneakily just re-indexing zero indexing things um so how we're going to do this is through the use of a challenge um so at Round K minus 1 we're going to derive a challenge UK minus 1. and we can derive this from um the commitment C yeah and so the purpose of UK minus 1 is to separate the high and low halves of our original polynomials so what I mean by this
is that I'm gonna cut P into P low and P High and then I'm gonna put a factor of u k minus one here and then u k minus one inverse here so we so we have these coefficients that uh we have sort of an order of like the degree of the monomial that they multiply and so we take the top half and put it here and then the bottom half and put it there yes okay yeah so what we're gonna do is we're simply going to add
them up it's a linear combination of the low and high hops so we're gonna in fact define p for our next round of the IPA PK minus two um and PK minus 2 is just going to be the sum of these two degree n over 2 polynomials yeah so P2 equals UK minus 1 p k low plus UK minus 1 inverse PK hi and so so crucially there are only uh because we're like folding them together
uh they're half the number of terms exactly yeah yeah um and similarly we're gonna shrink b um but over here we're gonna flip uh our use we're gonna flip the power of the challenge that we're using so we'll we'll put UK minus one inverse here for below and then UK minus one without the inverse for B High and then again this gives us b k minus two for for the next round of the IPA
um just just a sum of these two halves separated by um the challenge UK minus one so B hi okay and G is going to be the exactly the same as B so g k minus two uh except um the elements of G are group elements so we have to write them these are scalar multiplications G
low so we're using the brackets to denote let's go and multiplication yes additive notation yeah um and then you can fill us in um now um so if if you see here we started at Round Round K minus one with the CK minus 1 equals c plus bu right AKA it equals um p K minus one g k minus one let's see plus
um he and B K minus 1. so just using Gates exactly yeah we initialized um the K minus one in the in the Cs to the input vectors um so that was the the C that we started with in round K minus one now in in round K minus 2 we can Define CK minus 2 in a similar way but using these new um sort of folded vectors right so
this will now be p k minus 2. which has only n over two terms now yeah so we're having the degree in every round yes exactly um and then Plus a corresponding um p and B in a product K minus 2. so another interesting thing to note is actually and I'm just gonna assert this now
and we can we can show that later CK minus 2 can be also written as CK minus 1 Plus um some terms with um the factor UK minus 2. times some group element plus some terms with the factor UK minus two inverse squared plus another group element so do you want to write that up yes I do
want to write that out um yeah let's let's write that out yeah uh erase everything okay yeah because I I thought it was cool how you did it in the first one yeah so um just to remind ourselves um the inner product arguments opening proof consists of these terms and we're gonna see um how we got them so we were saying just now that
um CK minus two can be written as the inner product between PK minus two and JK minus two sorry uh no I think that's right yeah I think this no it wouldn't it be minus one yeah I think this is minus one yeah and then JK minus one plus
um um in a product so this scalar shirt is the result of an inner product between PK minus one and B K minus 1. actually no no it's K minus 2 I think so uh well no but but aren't you aren't you then going in and then substituting uh this for uh yeah sorry so it's K minus two and then you do Kmart
okay this this indexing got confusing because um yeah we we zero indexed everything yeah yeah but so sort of the punch line of this is that um I claim that after we expand all this out um we'll get CK minus one and CK minus 2 in the following form so it'll be c k minus 1 Plus some term with the factor u k minus two
squared um multiplied by some group element l k minus 2. Plus a term with the factor u k minus 2 inverse squared multiplied by some group element l k minus 2. yeah so and the point here is that these two terms are what's interesting and what we have to retain um from the K minus first round so we need to retain
LK minus I'm actually really confused about the um indices let's see uh I I think that that's right given now because we're on the next round uh so this should be LK minus one here uh no because we're on the aren't we on the K minus two uh [Music] right it's it's fun though okay it's off by one indices but maybe possibly yeah the the spirit of it is that um at each of these K rounds um we're collecting two group elements
that l k and RK and these have to go into a proof and that's how in our proof we get um a vector of k l elements and a vector of KR elements yeah can we see how yes yes to see how we get from here to here all we have to do is expand so if you recall uh what what PK minus 2 is really it's just Peak a minus 1 low multiplied by some a factor u k minus 1.
Plus oh minus 2. okay minus two and that's super confused by some Challenge and then the high half of it is multiplied by the inverse um of that challenge so when when I say PK minus 2 I mean the folded version of p k minus 1 and it's folded using this using different powers of this challenge right and then similarly for G
um except if you recall um we flip the powers of the challenges so this is UK minus two plus you can minus 2 inverse G High GK minus 1 High I think we want to flip through these right that which is oh yeah flipped slipped yeah so the powers of the challenges are flipped from um those used to compress the P vector yes and then since B is a very we use it in
a very similar way it would be tedious to write it out and you can it's an exercise for the viewer yeah um but if we try to multiply these terms let's see so we'll we'll notice um that some terms cancel out so this term has a UK minus two this term has a UK minus two inverse and so that's going to cancel out and give us just P low dot product gilo right whereas there's some terms um with the same factor the same power
of UK so these two terms multiplied together it would give us something with um something with a vector um UK minus 2 inverse squared yeah so are we sure it would be P High and G low which is a cross term yeah yeah jilo yeah and similarly um let's see these two terms are both UK minus two without the inverse so if I multiplied those together I would
get something with a factor of u k minus 2 squared um P low and G High which is again a cross term so I'm pretty sure I left out some uh just the remaining uh oh yeah so this one you can see that um for those terms whose challenges canceled out we're left with basically pilo gilo plus b high jihai is the same as saying PNG yeah yeah right and I think if we did PB in this way as well
we would get we would get back pbu so in other words we get back PG Plus pbu which is CK minus one yep and then we're just left with those terms with actually some Factor um of the challenge in front um in other words our cross terms yeah yeah so so the the L and the r are just like the cross terms from that round that are kind of like these leftover things we have to account for exactly yeah so you can see that at each round um we're really just accumulating cross terms and challenges yeah
so that was our first sort of round of compression um and if we keep going we'll start around K minus 2 with a vector that's already like n over two with n over two terms right and then we'll Fold It Again and that will give us two more cross terms there that we're accumulating and so on until at the zeroth round um we are left with um constant polynomials meaning we're left with just a single term and by which I mean P0
is a single field element G zero is a single group element and b0 is a single field element right and if we write up c0 again um c0 is um c0 can be expressed using like the basically the terms we have left at the end of round zero so it can be expressed as p 0 g 0.
Plus P zero b0 um scalar multiplied U right but as we saw just now it can also be expressed as um C1 plus um U I don't know what the index is here squared um l zero one okay forgive the indexing um plus u zero inverse squared um are zero yeah yeah right and then if we take
if we keep going actually we take C1 we can express it as a C2 plus something like that like plus the cross terms from round one and if we keep on going we'll end up with something like c0 equals c k minus one plus the sum of all the cross terms from all K rounds um with their challenges so u i squared l i Plus u i inverse squared r i and these lies and our eyes are precisely what we've been collecting and
putting in the proofs here I like all right now so the verifier at the end of K rounds and looking at the proof the verifier has access to all the allies and all the RIS um so the verifier is trying to check the equivalence between this expression of c0 and this um yeah so so we've shown that uh yeah these two things are equal and this equality will only hold if in fact the prover has been honest yes exactly um yeah yeah evaluated not every step okay so exactly and so and so the verifier
has this so using allies in our eyes the verifier can derive the round challenges the uis [Music] um now the verifier has CK minus one because this was the original C that we started with this was the C that purportedly committed to the polynomial that we input into this IPA now the verifier also has P0 plus we put it in the proof um the verifier also has g0
and the verifier does not have b0 something something to note about g0 and b0 um basically these are the results of folding the G and B vectors over K rounds and the G and B vectors to begin with were publicly known already so um what the verifier has to do what's left for the verifier to do is firstly compute b0 and the verifier is completely capable of doing that because
um again B is just the powers of X and this was known to everybody and secondly the verifier needs to check that g0 had been correctly constructed given the starting G vector and given what the verifier knows about the round challenges so so check g0 and yeah this is what's left for the verifier to do so remember we said that the IPA has a succinct check and an expensive check so this number one is a succinct check the
verifier can compute b0 and log n time and whereas number two here that's the linear time check um this is a multi-scaler multiplication involving n terms and this check is the one that we're trying to delay at every step of the recursive verifier and amortize across the budget proofs so we'll go we'll go now into how the verifier does these two steps so if you recall we the verifier had to compute b0 where B is just the powers of x
and the verifier had to check that g zero was correctly constructed so now it turns out that basically all the extra information encoded in b0 and g0 um all that information is basically the challenges the round challenges because that's what's been used to produce b0 and g0 given the starting B and G vectors so we can in fact rewrite b0 as an inner product between some Vector s and the starting B vector
um and similarly we can do this for G 0. [Music] now an S here um the terms of s is a length n vector whose terms are made up of the round challenges arrangement of binary counting order so what this means is s is made up of s is made up of n terms so and each term is some product of the round challenges
you okay my name um and how we're going to construct each term is that so for the First Column we're going to alternate this power um of the challenge at every row and so this and this binary counting order is intuitive because um because of the way we folded things in half at each round um and for a more rigorous and for a proof of this you should see the Halo paper yeah but for now um
how we construct s's so we alternate the power for u0 at every row for you one at every two rows and for you to um every four rows and so on and for UK minus one every K minus two rows and in this way we construct um the vector s that encodes um the round challenges and also retains the structure um the structure of the folding that happened at each round so I claim that the inner product of S and B can be computed in logarithmic time
and um I'm not gonna prove it here but just to sketch it out um the inner product of S and B that's the same thing as saying um evaluating s at X right because yeah because these are both field elements and yeah exactly yes so yeah so it turns out that um yeah we can write we we can do this computation in login time yeah and you can see the Halo paper to see
how we do that um however um this inner product which is between a field it's it's a bunch of it's a multi-scaler multiplication here this there's no shortcut around it and expensive it's expensive in fact it's n operations because this is n terms n terms so this is the linear time check that we're going to delay at each recursive step so I think with this in mind if you took away nothing else from the inner product argument just
remember that it has a succinct check and an expensive check and this is enough for us to go on to the accumulation scheme yeah the the I think the explanation of the IPA is really cool like we just I I think yeah what I would take away is just uh the mechanism by which we like reduce something into like a log logarithmic number of terms because obviously for the prover they're just handing me all the coefficients to the polynomial yes that doesn't really help us if we want to sync proofs exactly so yeah our proof you know is only log n number of terms um yeah whereas for the Patterson commitment for example
um you you're to fully evaluate the proof you need um just the coefficients um of the polynomial yeah so the atomic accumulation scheme here uh we're instantiating it over the inner product argument as the predicate um and sort of the structure yeah the diagrams are going to get a lot prettier now um the structure of this is basically let's start with um sort of the classical recursion right for for for classical recursion um
by which I mean full recursion you have some application f um such that f x zero equals X1 right and then you have you bundle it together with some recursive verifier V and you call you call these two circuits together they're recursive circuit so the recursive circuit the requires a verifier additionally takes in some proof um that proves the previous instance of itself and
um this whole recursive circuit in turn outputs the next proof um for the next instance so you will notice that um to fully include a recursive verifier in the recursive circuit you need the verifier of your proof to be sublinear because if if let's say your verifier were linear the next verifier would be the size of this circuit right and then you know you just get blow up so we don't want that
um at all also just for like practical like proving times we would love to have a succinct yes exactly so no the IPA verifier is not sublinear so if you recalls those three terms yeah there's like a what is it there was like this SB which is is sublinear and then there is this SG which is definitely linear right so we can't just do this with the IPA verifier um
instead um we're just we're gonna call this the accumulation verifier and in the accumulation verifier we are only going to do the sub synced checks um right and what about the linear check that's what we are accumulating so that's what we are constantly delaying at each step um to the next instance so we the accumulation verifier has to in addition take in some accumulator from the previous instance and output um the updated accumulator
um for the next instant yeah so I think what we should do now is go into exactly how we update the accumulator yeah so if you notice here um what the accumulation verifier is doing is taking two instances and combining them into one so what I mean by this so um so Pi zero and the previous accumulate later x0 are things that have the same shape they're both instances [Music]
um so I'll call I'll call them cute eyes so we're Q zero is pi zero and q1 is X zero so an instance has the following shape it's basically an IPA proof shape so it has some commitment some challenge point and some evaluation and then it has the IPA proof that we saw just now so
let's see else ours G zero P0 yeah so both both of these instances have this shape right so now um what the accumulation verifier is going to do is see first of all okay this is the pack verifier
so first of all it's going to do the succinct chat um on each of these instances so for I in zero one sex sync check on qi foreign I definitely need to refer to my notes here because this is this gets mind-boggling um and then secondly um so now that it's done the succinct checks it's now concerned with
accumulating these two instances into one new instance yeah and how it's gonna do that is a random linear combination so we we assemble some Randomness Alpha um that's using uh let's see yeah we samples them Randomness Alpha let's not fear Shamir this random um so using this Alpha we can now accumulate our two instances into one new instance um so what we're going to do is we're gonna Define
a c so we're going to basically make an inner product argument for for that this s polynomial that we're not checking yeah so we'll Define this C as a linear combination of the G's that we didn't check so G zero zero plus Alpha G one zero here right and then um this is a commitment
um two the polynomial s which is our challenges yeah because if you're if you recall um G 0 is the inner product of S and G in other words it is a commitment a Patterson commitment to us right so c c here is a commitment to um S 0 plus alpha s one sure right um
so it's this is what we mean when we say like we're accumulating all of the challenges from uh like yeah like we're accumulating these two instances into a new instance yeah so um and then so we're basically instantiating an inner product argument for this new instance yeah so we sample some X yeah let me subscript all these as well so we sample some X some random X at which to evaluate this new s
and then we Define okay I'm gonna put stars on um all the terms that go into our new accumulator and our new accumulator let me just write out what it should look like it should look like C star X star V Star and it should also have an IPA proof l r G zero star um
P0 star yeah very cool so V Star is just um s star s evaluated at X star so we have that and then the prover the accumulation verifier now has C Star Extra and V Star and proceeds to run an IPA for sea star extern V Star um at the end of which
um it gets this new IPA proof for an IPS for C Star based r X star and output this thing yeah so you see that we put in two instances and accumulated them into one new one okay yeah and can we we can also generalize that for more instances like like right now we sort of have this uh like chain
of recursive proofs right we can imagine that if we wanted to batch a lot of proofs we could take um like multiple instances and just have a longer linear combination yes absolutely yes cool tall in this way we keep delaying having to do this on this length and MSM but eventually we have to do it um and when we do it that's called the accumulation decider that's doing it so let's imagine we've had like a long chain of accumulation verifiers and now we are finally ready to do that expensive check
so what this is going to look like is the accumulator here uh let's see let's see this is so we've chained together a bunch of IVC provers and oh IVC here stands for incrementally verifiable computation it's what you said basically this linear shape that just doesn't deal with like n inputs but rather just change them one after the other and the end of this chain um we have the IBC verifier that actually tells us whether or not this whole chain has been valid yeah so now
in the IVC verified accumulator is given to um the ACT this cider and what the ACT decider does is checks this yeah so so finally checks yes exactly but but like the the nice not the preemptive but but the the nice thing is that we can do this check outside the circuit right right yeah yeah we can do that and so it's like even though it's linear time not only have we amortized the cost over all of the proofs that we've recursed over but we get to it's linear time like on the
CPU which is right right yes exactly um and then we also need to deal with the these uh the last new instance and the last sort of output from our application circuit and so this would be input to the full snart verifier which will also do all checks like even the expensive ones yeah cool yeah so that's how we get Atomic accumulation from the inner product argument cool so Atomic accumulation is when we
consider this whole accumulator as a single thing whereas more recently there has been a scheme called split accumulation that actually allows us to um only make a short part of the accumulator public so we can call this accumulator.x which is public and then have a longer part of the accumulator that's private so if we do split accumulation for the inner product argument um so now we're forgetting the IPA for now
um the witness would be um literally the polynomial that uh is committed to by C right and then sort of [Music] um at each step of in Split accumulation at each step of the accumulation verifier um we are verifying that um basically we're accumulating two polynomials um that evaluate to the correct values at the correct challenges but we are not
verifying that these set of polynomials committed to um by the seeds see eyes because again that verification is a Patterson commitment is an um Owen is an uh MSM with n terms so this final verification is delayed to the decider once again but I think the point of split accumulation is that basically you no longer need a succinct argument so the inner products argument was succinct um it was log n and therefore we could
input the whole argument into the accumulation verifier whereas if you had a super long argument like this that's like n terms plus a few um then like you know um all is not lost and you can split up your accumulator and still be able to um have a succinct split accumulation verifier yeah yeah because so so even though the proof is linear the incremental verifier is still succinct so you don't have this problem with uh like the proof circuit complexity blowing up right and um
so we don't have to do like when we just uh give the verifier this polynomial we don't it's it's cheaper from the the prover time perspective because we don't have to do like the folding and the the IPA reduction we just have that we we just have this um uh like Peterson commitment to the polynomial which we would have to do in both cases in both the IPA case so it's strictly better from the approval times yes yes um I think where it's worse is that the argument says at the end is larger yeah but there are also ways around that well we we can just do the IPA at the end
right exactly yes yeah cool cool um well great uh this has been really really interesting um how do you want to talk a little bit about how this is used in Z cash or yeah so right now um Halo the Halo 2 proof system has been deployed in Z cash without recursion so it entered the IPA and we're doing the full verifier every time for every proof um now when we have recursion implemented um what we're gonna do is compose proofs so in zcash
um every uh sort of action which which means every group of spends and outputs uh produces a proof of the validity of that action um and in within a transaction and within a block there are multiple actions so um we can aggregate um multiple proofs um multiple action proofs such that we have we end up with only one proof per block and this reduces zcash's chain State because we don't have to keep so many proofs on Jane um
oh we can so that's batching action proofs within a blogger we can also batch block proofs such that the whole chain history can be verified with just one single proof and that's what Mina is already doing yeah very cool well thank you so much for for joining and this has been really interesting yeah thank you for having [Music]