ZK11: Application of Graph Methods for Efficient Quotient Polynomial Computation in Halo2 - Karthik
19 Apr 2024 · 32:15
Karthik Inbasekar of Ingonyama presents research at ZK Summit 11 on applying graph methods to the quotient polynomial evaluation inside the Halo2 zero-knowledge proof system, a step that is often a compute and memory bottleneck for large circuits. He shows how partitioning the computation into weakly connected groups lets it run in parallel across multiple GPUs, demonstrated on Taiko's zkEVM super circuit to cut both latency and memory use.
Speakers
Topics
Transcript
[Music] thanks everyone for coming H and um so this talk is actually going to be somewhat complimentary to to sh H so in snar when you want to prove some argument uh you can actually compute a sound check or you compute a quotient polinomial using a quotient argument so and surprisingly we are also going to address uh in this talk some memory bottlenecks that appear in h to okay so uh I'm kasik I'm a researcher at ingonyama we work on Hardware acceleration and so that's why uh we are
focusing on memory bottlenecks and so on so this work is based on this uh uh this uh uh this paper uh which I uh wrote with Roman and Guy uh from inyama and you can download this paper from this uh link uh let me begin by uh uh just giving outline so I'm going to start with a quick introduction to Halo 2 how many of you here are familiar with Halo 2 okay great so I uh and I'm just going to then make it sort of brief and uh mostly try to address it from the point of view of uh uh how the computational uh uh data dependencies appear in Halo 2 and then uh we have uh two solutions uh
which are based on graph ideas which you can use used to identify structures for computation uh basically for computing the quo polinomial and these are connected components and the community detection and then we're going to apply these ideas to some uh ZK evm circuits uh because these memory bottlenecks are usually a problem only when the circuits are really huge for example there are like many many columns in your Halo 2 Trace table like 600 700 and of that order and for smaller C cutes this is not going to be so relevant uh you will have to think of other ideas like hardcoding the computation yourself in unus things like cash escaping okay and
uh so let me uh go ahead um so we're going to start with the Halo 2 Halo 2 is a zkp system that uses a blanish arithmetization uh which uh means uh we have the circuit data which is encoded in a trace table so in Halo to the public data which is the data about the circuits the constraints are encoded in the instance fixed and selector columns and the and the private data which is generated by the approver uh for circuit satisfiability is encoded in that viice columns and uh the idea is that circuit constraints are converted to polinomial identities and then you prove them using the quotient argument uh so basically
you can have a uh circuit constraints like where each row represents a gate and the wiring is relationship between different uh pixels in the trace table and uh you also have lookups and all of these can be expressed in terms of some uh constraints and we convert them to polinomial identities and uh before we do any computation of the quotient uh we going to have to first commit to the witness basically comeing to the trace table and commitment basically uses uh multiscalar mul M lication elliptic curve field arithmetic and all of this and the reason I want to mention uh this here is that this is a universal primitive it doesn't really depend on
the circuit and most of these algorithms have been killed to death now so we don't really think it's a much of a like a problem so in general these are very good GPU problems you can fit it in the GPU do a lot of parallel compute and you can get pretty good results even with just simple knif drop in replacement of the commitments so by the way this logo is for the icle GPU Library which was developed by inama uh it's open source so feel free to try it out yourself or reach out to us if you want something so basically the MS based MSM based compute Primitives are highly power lightable uh but on the other hand uh the uh quo polinomial uh is a sort of a varied
quantity it depends on which circuit you are using it could be compute bound and memory bound depending on which kind of of circuit how you are optimizing how you are calculating the uh circuits and so on and so forth the main bottleneck there is uh number thetic transforms and it uses mostly scalar field arithmetic and the big problem is that this is uh not Universal so and as a hardware company we want to look at things which are Universal so you can build effective Solutions and the goal here is to see if there are ways we can come up with uh to somehow use the structure which is built in blanish arithmetization but somehow find a way without breaking the
definition but sort of work with it work around it somehow and break this data flow dependency so how this data flow dependency appears in in in Halo to is in plonc you have this columns and Trays which have three different constraints gate permutations and lookups so these constraints are mathematically independent but highly data flow dependent meaning the same data is copied to evaluate different types of constraints so the issue is of course the columns that you saw in the trace table have to be extended several times to several degrees for each of these constraints and the columns may be repeating across the constraints and you have to decide oh should I recompute should I store and it's not something
that you can do very easily okay so uh it's hard to make Universal uh agnostic optimizations for constraint evaluation and roughly the equation polinomial for very large circuits like ZK avms and popular ZK ml models is the 30 to 40% and most of the time it's memory bottleneck as in like we have to read from host to device which we try to avoid as much as possible because this even if your computer is really really fast host to device data transfer basically kills the performance entirely so we want to avoid this and uh the question of when where and how to extend is the key to minimize the number and size of the fer transforms and uh so just uh I'm going to do a very quick uh
run through of how do you evaluate a constraint so let's take a sample polinomial here so here you have a polinomial I not put the A1 of X each of it a function of some X it's a polinomial and it's like a degree uh three uh the highest variables uh which have A1 F3 A3 and uh let's represent them in terms of this uh blobs which are columns and we're going to use a degree cluster method where you're going to basically divide the expression in terms of the degree of the terms that appear so you have degree one terms you have degree two terms and you have degree three terms right so the idea is that like what if you try to do the
evaluation in the following stupid way which is that like you try to take oh I will do degree one degree two and degree three in some way what's the big Advantage here the thing is that like you can do coet entities you never have to do large entities you can do small entities of several coets and each coet can be done independently so all of these red blobs here are independent fixed size entities which you can run in parallel and this is good for GPU right but now you see that between one cluster and another cluster there are like overlapping columns and then you have this question should I copy or should I recompute so the blue blob here represents the one which are copied and here in this particular diagram you see that like you have some kind of dependency across different clusters and
you can't can't essentially compute them independently if you don't want the copy right if you don't want to copy you either recompute or you wait for the cluster to finish then you copy and then you go on so this is called cluster interdependency and this kind of makes it very difficult to paralyze so this is like a toy version of the problem that you actually face in evaluating the quotient polinomial you have to constantly make these decisions and it's not very easy to do it anyway in the end whatever way you do evaluate you'll have to extend the polinomial to the maximum degree so that you can compute the final result okay so the question is how to parallelize so the idea is that a relationship between columns and constraint is like a graph relation
between nodes and edges right and Halo to already uses some symbolic representation of constraints in abstract syntax tree so for a simple multiplication gate like this you have some uh as which tells you how the relationship between the prer computer data which is LHS rhs and out is actually uh following some sequence uh you can actually lift it out directly from the dev uh part and Halo to uh our idea is not to actually use the as graph but it was more like we inspired uh by this idea we want to extend this idea to use partition methods which are available in graph Theory and to see
which circuit is paralyzable which circuit is not paralyzable and questions like that so the criteria that we used this connected components it's something extensively used in data science and machine learning uh and uh it'sa you know we thought that okay well let's try it out and see what happens and the other idea is to find communities which are weekly connected groups and the idea is to see if we can use this uh these techniques to find paraly ability criteria so it's more like a exploratory Observatory idea and uh never use these kind of tricks at the level of constraints because if you try to take the constraints and do these kind of tricks then you will introduce
bugs because each time you break a constraint or slice a constraint you have to put some kind of a uh condition for separ separating the constraint so most of the talk is that we're going to sort of apply these ideas after the Prov is committed to the data so we have the relationship between columns and constraints which we know from the as but we use it at the quotient polinomial evaluation level and then at the polinomial level you can do whatever you want you can separate add do everything because the pro already sort of uh sorry about that Pro already committed to the witness data okay so let's start with the connected components so what are connected components in a graph so let's
represent a graph as a tuple we have a vertex and an edge and this is for example a simple graph so you have a bunch of vertices and some edges and this is a multigraph when there are Loops between the same uh uh in this talk and also in general in this exploration multigraphs are a bit complicated to deal with so what we will do is always collapse a multigraph to a simple graph is that whenever there are Loops we'll collapse all the edges to a single edge and uh what is a connected component it's sort of intuitive here so if you take the simple graph here it's basically disjoint pieces in a graph so so it a a a connected component is a connected subgraph which is part of a
very large graph so you have an imagination in your imagination you have a very large graph and you're looking for small connected components which which are disjoined from other okay so these are connected components and uh but in order to build a graph uh in you need some kind of a huris stic you have to Define some rules and these rules are not something Universal you can come up with some huris stic which works and other huris stic which will not work and we want to go through this uh uh because what I'm going to say is not going to work and that will give you an idea of what you should do in order to make it work so uh theistic is the following so we're going to Define all the columns in the trace table as vertices and then
we're going to Define primary monomials which are just functions of these vertices basically simple if you have a column which is a b and c and you want to comp an expression ABC for example that would be an example of a primary monomial and then you can also have secondary monomials which are functions of the primary monomials as well as the columns so you can keep on going in a sequential way and build a lot of such sets and subsets and so on but for this talk this this is sufficient and uh then whenever there is a connection between uh different sets you add you add a sort of an edge between these uh two things and you you can easily do it do it using some standard algorithm like BFS and it
it's very easy to build this uh uh connected components in general so let's see an example of the connected components and go to the same uh bad example that we saw before so let's represent the columns uh the primary monomials so the primary monomials are just simple functions of the columns there and then you have the secondary monomials which are functions of primary monomials and the columns so what this shows is that like in this simple example it basically breaks off into two connected components and as you can see uh there is one element in the first connector components and eight elements in the second connector component and the highest degree of the second connector
component is four because in entity we always extend to powers of two so even though you have only three polinomial here so it's degree 3 and I just make a degree for and so what's the main idea here so for each element inside a connected component only do ntity to the maximum degree of the connected component so it of course pres presumes that there are many disjoint connector components otherwise this is not very useful and you will see what happens I'll give you a result of what happens when we applied it to some transaction circuit in the next slide and what is important for me is if there are disjoint connected component then you can do parallel compute this is what I'm looking for can I get disjoint connector components is it even possible okay so
let's look at this example that we saw before and basically you see that this copy structure that you sometimes find by manually trying to do things will just pop out right if you just apply connector components okay you know which uh part you have a problem with which part you may need to rewrite the circuit reate the constraint whatever you want so you can use this as an analytic tool to see okay you know what should I optimize my circuit differently in order to get my desired result okay so basically it identifies independently computable connected uh Expressions this is my main uh interest here uh as I said before uh several disjoint connected sets enhances paraly ability so we applied it to this uh transaction
circuit in PC and we find that there are two bunches of a connected components but if you apply it to some big circuit like ZK evm you see this everything becomes one big family here right so it's not very good for uh uh that se said this idea as a problem and what's the problem is that when you have permutations and lookups High circuit interconnectivity this kind of increases the data flow dependency and things that you need to copy and of course this is kind of obvious we are building big circuits right we going to have this problem so maybe we are just looking at it a little bit wrong maybe we shouldn't look for completely disconnected pieces maybe we should look for weekly connected pieces right and that's the whole idea of community detection and this idea is well known it's been there
for a long time uh people have been studying it in network Theory and so on and so for for and um so let's define what a community is thing is there is no good definition it's just sort of very humanistic so in a thing that works for me is that like you have a a bunch of a graph which is split into K groups and in each group The in group edges are very dense basically strongly connected components and the Intergroup edges are sparse so the edges that go between one connector component to the other are few right so this is what we looking for and this is my definition of a a community so basically Community is a bunch of weekly connected groups and each group
is a strongly connected component so these are all strongly connected but these and these are weakly connected okay again uh you can find this uh this is an NP hard problem don't try to do something you're not guaranteed to get anything so there are many heuristic Solutions you have modularity of partition you have Edge betweenness a ganum algorithm and you have Max flow in Cut which is one of the more stronger algorithms so in this talk I'm going to only focus on edge between us and G human because it's very physically intuitive but you can use any method it doesn't really matter so choose your favorite Community detection method and you might get something good out of it so this ganum algorithm is found in this physics paper
I was a former physicist so I I had to put this here this has about 177,000 citations only 2,000 citation lower than the famous uh ads CFT paper in string theory if there are any string theorist in the audience so uh so basically in giran you compute something called The Edge between the centrality so the edges that connect communities have high betweenness and what's the meaning of this betweenness is uh given an edge and you're going to compute the number of shortest paths in a graph that include this particular Edge and then you're going to count the number of shortest path between the same pairs of edges and then you're going to
sum over all possible edges okay let's look at a simple example here is a very symmetric graph so you can pick any pair of edges and ask how many of these paths actually pass to the edge CD right so this graph the denominator function is always one because if you take any pair of edges there is just exactly one shortest path but if you ask what's the shortest path between any pair of edges that will always contain this Edge then the answer is given here okay it's sort of intuitive if you start from BFS and start evaluating the shortest paths you will see that like uh this is sort of symmetric about this point and so this path uh this every path that has to pass
through will essentially have to pass through this so the idea of community detection is that a high traffic edges if you peel them off in a graph then you get community stru okay so this is our idea basically like you just know that this exists it's been applied always in network Theory we'll just use it to make polinomial evaluation easier right so uh recursive application you can do this but it'll uh sort of only split a graph into a subgraph and subgraph into subgraphs and the end result is like a tree right so this was written in it was surprisingly I didn't find it in Rust so Roman wrote a code which is is available uh in ped
graph Library so you can use this if you want to play around with it and um so we have to build the graph so we have to Define some htic and this time I had a problem like uh I didn't want to complicate matters too much because uh it's very htic and it runs for a long time uh so I defined it for only columns so this time the relationship graph is built simply between columns no sub Expressions no monomials no nothing so and then we're going to just see which edges are connecting which columns so we'll make an edge with the following criteria and this is very heuristic there is no Universal criteria here and my heris is that I'm going to put an edge between two vertices if they belong
to the same custom gate the same permutation set or the same lookup argument okay it's a very simple FIS stic and you can easily build the theory behind it and um the idea is that you apply the Gan human algorithm and it will CL cluster all the columns in the trace table in terms of different connected components so each of this is just a bunch of vertices okay so this is what the Gan algorithm does and then it will create this high traffic edges which basically connect across different col different columns okay so that's the result of the Gan algorithm and uh basically it contains subset of columns and the idea is to minimize the number
of high traffic edges okay the idea is to somehow minimize the number of high traffic edges so that different uh uh connected components that are appearing the Gan algorithm have fewer edges that are overlapping across them so uh of course we want to do a sort of simple split not to do many many many uh connector components so we use some kind of greedy algorithm and the idea was that like to take a large circuit and to split it into two approximately memory-wise even parts so that we can have them almost to be of the similar size imagine you have a GPU of 20 GB memory and you want to use a smaller GPU which is only 10 GB memory and you can use two of them because they are cheaper
whatever so you can try to split it in some way right that was the kind of uh intuition so I Define a good two-way split is if the largest community in the giran Newman algorithm is like 50 to 60% of the toal circuit size so this is what we do we use the gritty method of merging the smaller communities and uh we assign the columns to different objects which we call bins so we take the largest community and put it to bin one and then we merge the other smaller communities and whenever there is an overlap between the two like if you see there's an edge that connects from bin one to bin two I'm going to take the column from the largest bin and put it in the smaller bin okay so this is a price that I'm paying for this separation so that's why we want to have
minimal number of copied columns so that the overhead is sort of low and uh this is this is the optimization criteria so for separability you pay a price you you recompute some entities that's basically the whole idea and how do you evaluate this in practice because it's all nice in theory right right but H PO Code is a mess so we sort of had to come up with some uh uh way to assign which column belonged to which bin and you can do it using a simple Boolean Vector say that in bin one you have this look up this permutation this uh custom gate computation and in bin 2 you can have the same thing but also you they can appear in different terms of
the H poly right in quent polinomial you can have a custom gate part of it comes from bin one and part of it comes from bin two you can have things like that so the main idea is to somehow uh use this to wrap it inside the quotient polinomial evaluation code and what you see is that like you can put a simple for Loop that runs over the different bins so this means you can actually evaluate the each part of the quotient polinomial separately as two completely independent Expressions ideally you would want to do it at the circuit level but this very very complicated and it introduces bugs so in quo polinomial at least it's clean in terms of theory very dirty in terms of engineering okay so this is the problem the main problem is
that every constraint is linearly independent so there are powers of Y and part of it will uh sorry what happened part of it is evaluated in one bin and part of it is evaluated in another bin and both of them has the same power of Y so if a given constraint part A is coming from one and Part B is coming from another you will have to use the same powers that make the linear Independence on both and you have to keep track of it using some indexing so the whole thing is an indexing nightmare uh Theory wise it's very simple but engineering wise it took several several hours weeks even months to get the correctness right so bottom line is this uh so G gives you uh takes the grath and split it into bin one bin two and some
edges to copy so the effect is you take the trace you split it into two parts and you pay a price by copying uh some of the columns across okay yeah so essentially the quotient polinomial in bin one and Bin two can be run independently in parallel and the goal is somehow to keep these copied columns small so you can pay a small price for paralyze ability and I'll show you in an example where it actually is beneficial so essentially we can solve memory bottlenecks by splitting the trace and the tradeoff space as I said is to recompute small number of entities and if you can uh afford it it's it's a good tradeoff okay so let's apply it to uh some zkm circuits we first applied it to
Tao zkm because it's a sort of a medium sized in terms of zkm uh standards so you have uh given Manu partition on this and we got two connected components so you can see one of them has about 300 columns and another has about 250 columns and with an overlap of about 23 so we try to you can represent the graph in terms of some uh uh so the blobs that you see the black ones are actually the actual columns and there are many many edges and as you can see intuitively from the graph you have some kind of rough partition that you can create and the largest community is like 50% of the total Community size which is good and uh so we sort of ran this in CPU there's no
GPU implementation of this yet it's a proof of concept uh so what you see at the base level you have a a total instance size of 20 GB and in splitting it into two you roughly split it in 10 GB each okay and so it's also a memory bottleneck and in addition you see that the latency of the full run time is reduced to the latency of the largest community okay this for me is actually good because then you the other the combination is not so much of a problem because you essentially do field additions in the last part of merging the quotient polinomial so that's okay so that's not so much of a problem so the difficult part was reproducing that
the results produce the KN quotient polinomial entirely so it's an engineering optimization without doing any cryptographic change but the idea of separability we essentially took from uh uh the graph theories ideas and applied it to this so now let's apply to another zkm circuit and see if we can reproduce it all over the place and then we find that it's problematic so we applied it to scroll ZM and we find that the split is like 68% of the total circuit size so there was no efficient way to partition this so the largest community is about 658 columns and if you try to recursively apply this uh gan human it takes the 658 columns and split it into
564 and 94 and increases the number of edges you want to copy so the more you apply and more you partition the more price you pay for copying and recomputing which we don't want to do so I so I decided okay so the whole thing is about finding the largest community if you find a larg community which is like 50 to 60% you're good and if not maybe you want to rewrite your circuit or do some other optimization and so on and so forth and um the main reason for this is again you have about 190 Columns of permutation which participate in a permutation settings scroll and this is from an old data so things keep changing in this and by the time we finish getting correctness for the h poly
nightmare a circuit might have changed a little bit so there may be some changes but to just give you a comparison in Tao there are about 15 permutation columns and this is 190 so that's what actually causes this whole thing to become connected but but you can try different graph heuristic methods maybe Define your own heuristic explore a little bit experiment with Max flow Min cut and different algorithm and you might get slightly different results okay um but I think the general idea of giran is pretty to understand the intuitive structure of circuit you know what for example by plotting it in this form I can even tell you what part of a circuit is for example you see this triangle here uh that's the P circuit and these
snowflake thingies here they are from transaction circuit and somehow there is some kind of topology there and it's it's visible inside the graphs just know need to know how to represent it or how to visualize it and you you have some way of understanding circuits in a different dimensions I think it's pretty cool H so I think that's it I'm going to summarize uh so we applied graph methods and we tried to use connected components and the main takeaway from connected components is uh you only need to compute fora transforms uh which is of the largest degree in the CC set if you get many disjoint CC set you can paralyze but it rarely happens in ZK circuits so I think the more practical direction is to do community detection
and uh we applied Gan human uh you can apply any algorithm that you like but you should try different uh methods and there may be some trade-offs and essentially if you definition of circuit as large permutations you will have less paralyze ability uh but maybe there are ways around this so we try to apply to zkm circuits like Tao and scroll and we find that for Tao at least we have a pretty good split and uh we can solve memory bottlenecks so that's it thank you I'm going to leave you with this uh discussion slide if you have any questions uh feel free to quick
question uh yeah hi thanks for the talk it's very good um so this seems most immediately useful as a way to figure out how to parallelize VMS that were not necessarily written with paralyzation in mind yeah that being said do you have you thought about like now that we know how to do this kind of thing how would you design a VM custom made to like really lean into this technique yeah yeah actually it's a great question actually that's the direction that we are sort of trying to think uh if we can do stuff and I started by trying to apply to witness generation uh but it's very very hard usually everything becomes one big graph of connector components and uh uh I don't know if there is a way to do it
but VMS and I'm like looking at risk zero for example they have announced in their performance uh that they have found ways to chunk uh parts of the code uh and witness generation for these parts is itself is parallel in Gnar for example they find in Gnar plon they find actually like streams which are like like it's like the uh the compiler fires and finds that okay these constraints can be evaluated these constraints can be evaluated and it does in in parallel if it if it is possible but uh it's not like in the main code it's just a sort of a but in general yeah this is the direction that I think we need to do some research and the idea was to see if you could combine with tushar's
streaming algorithm somehow if you could identify chunks in circuit and prove these chunks and then somehow try to combine them in in a nice way uh but yeah yeah this is uh the direction that I would like to take it in uh in general yeah cool thank you let's thank speaker [Applause]