Tabby: Automated Programming of Efficient Zero-Knowledge Proof Circuits | Hongbo Wen - Nubit

[Music] the co-founder of new bit uh today I will present our research work on ZK proof optimization uh Tabby uh synthesis AED compiler for high performance z uh D knowledge proof circuits uh this way uh this work is honored to be supported by the new bits uh Luke from polychain and the University of California Santa Barbara uh the start point of this week is uh of of O of this work is the existing ZK compilation pipeline Is Not So Satisfied uh there are two kinds of uh de proof uh languages uh lower level ones such as Halo 2 and uh circum asking the developer to construct constraints by themselves the devel the developers could perform fine green uh optimizations as far as they know how to do so correctly thus the performance of circuits uh will be good uh another kind of uh D knowledge proof language uh focus on being user friendly for example uh Noah and and Leo users could only write the highlevel statement M ments and the compiler will generate the code automatically however the generated code is inefficient about 10 times slower than lowlevel uh circuit as observed [Music] and thus uh how about inheriting the user friendly L interface from the Noah and generating optimized code that's how Tabby born uh we want to be user friendly but uh generate the fine green optimized uh day Circuit by the tabas uh work pipeline what uh okay and let's see an example to observe uh what's happening during the compilation on the 11 hand side is the source code uh on the 11 hand side is the uh is an example of a circuit right in Noah it has a few uh it has a few parameters values sign and exponential the circuit is constraint old and even elements in a loop the Noah compiler uh generates standard gates to constrain those signals and the compiled Halo to uh circuit is right is right hand side the estimated time cost of proving on this uh of proving on this circuit is marked as let's say 18 unites time cost the generated table has three columns of signals but many elements are redundant essentially by the way uh we use a community based tool to generate hello to circuits uh from the nor source code then assume we have uh we have a z then assume we have a ZK expert to help out uh he will write two custom Gates uh one one to constrain the column C and uh corresponding to the symbol sign being uh assigned by negative sign in the source code want to constraint the column AB A and C corresponding to other constraints in the source code um the generated table is smaller than the one generated by the compiler and the time cost uh unit uh unit is 16 around five times faster the reason con uh the reason costum gates are better is that they are closer to the original computation and so being more efficient the root cause of the compiler cannot generate Gates closer to the uh original computation uh like uh like customized ones is that the compiler can cannot guarantee the semantic equivalence automatically thus if if Tabby could find custom Uh custom Gates automatically the size and time cost of the generated circuit could be compacted okay here is the overall comparison uh between the uh Tabby generated uh between the circuit generated by the Tabby and generated by the compiler so the compiler has the workflow from A to B to C and to D and the the the tabi or the DK uh expert uh has workflow from a to E and F and the generated table in F uh compared with the generated table in D is smaller is smaller and then here and then here is the workflow to find custom gauge uh by the Tabby so first we got the source code and then we decompose the source code to a trace program the trace program is the symbolic representation of the concrete Source Code by using the symbolic representation uh we have a smaller search space to search for the uh optimized code and and it is easier to form analysis on the trace program uh being uh being the symbolic representation after compile the source code into the trace program we analyze the trace program and find potential uh component planning in it uh in the motivation example we could uh have a two components corresponding to cost cor correspond corresponding to two custom Gates as a as two components after the analyze analyze of the components we could do the syn uh we synthes the the Tabby synthesizes the components and have the optimized code uh at the end of day uh as shown as shown in my slides uh the optimized code has two custom Gates and uh they are very similar to the uh custom uh to the customer Gates writen by the uh the expert okay so let's go that uh let's go step into the details so first uh we got the source code and in the source code we assume that or uh we we assume that or essentially it's it is the requirement from the current uh crypto Primitives is that the loop is banded taby uses uh s sa based uh flatten uh algorithm to uh to decompose the uh to decompose the to decompose the the loop uh into a few uh uh into a few groups so here we assume uh the N equals to three and then we got three groups in the trace program and uh in each Trace program we have four constraints those four constraints is flattened from the source code uh in the E branch and the sign uh sign assignment and uh for the if else uh statements uh we decompose uh two branches into two constraints and constraint back to the sign for example we got uh if sign is true and the L Branch so there are two constraints com uh there are two constraints uh corresponding to those uh the if and else and then we summarize uh we we we add back to uh we add back those two constraints to one constraint so finally is so finally this the X in this source code is represented by the X3 uh in the trace program uh now we got uh four constraints uh in each group and we got three groups because we have three Loops uh in the source code after we got this uh the trace program we are uh we are essentially doing the analysis to get the potential component in this uh uh in in in those constraints so there are tons of itial components partition uh partition plannings for example we could group one and four uh the the constraint named as one and four to one group and two and three for another group and we could we could also group The constraint one and three to one group and two and four to another so the search space of the potential components partition is extremely large and the key insight in Tabby that we do a read and write dependencies graph analysis by doing this analysis we have we could we we could have the uh we could have the re and right dependencies graph between those constraints now we could say that hey the constraint four will uh dominate the constraint one and two and the constraint one and two and three are constrained by itself by itself then uh however the composition possibility are still huge to be searched in that case the Tabby utilize the strongly connected components of the uh re and right dependency graph of the constraint the behind observation is that Tabby wants to split components as many as possible because the the problem side is smaller and uh it is easier to Ras about uh small sets of constraints compared to its a large set of constraints the only case that prevents the spilling is when two constraints depend on each other uh dep uh depend on each other because we cannot reasoning across components so in that case it's it's too hard to Ras about uh the the the relationship between the constraint one and three automatically so thus without deeper semantic analysis uh just based on the re uh just based on the lightweight read and right analysis uh uh strongly uh connected components is a good choice to do the uh to do the component partition so we got two components here uh one uh the constraints one two three is constructed in one component and the constraint four is Con uh is being uh uh is constructed to another component uh after the component identification taby Maps the component to concrete constraints for example uh in the component one we got uh three so so we have three groups in this uh in the trace program so the constraint four essentially rep uh essentially represents four three constraints in the uh in the concrete uh in the trace program so we have S one a constraint by uh one minus s z and we got sign two sign three and it's ass same for the next group uh we got one the constraints one two 3 and we map to the concrete uh concrete Trace program and let's use the uh complex components as the example taby essentially tries to generate the custom the custom Gates by enumerating uh all possible statements so given the trace program we are trying to find a constraint or uh summarized custom gates to represent to represent those uh those constraint in the uh in the trace program for example we could have a costume Gates as a i is constrained by a i plus a uh plus b i uh at one so here a BC essentially is a column of signals in the Halo 2 circuit and a represents the X B represents the values and C represents the signs and uh so there are there are the essentially there are lots of candidates to be searched to to to cut off the search space uh uh essentially Tabby utilize a semantic based analysis to avoid the the enumeration of uh in uh incorrect candidates and uh such as the candidates I list as the first candidates and it will scan through a few few uncertain uh candidates and we uh and Tabit utilize the uh smt server to to find uh to find a a custume Gates uh to find a a candidate that satisfies the same semantic behavior of the custom gates in the uh in the source code so we got let's say a few uncertain candidates and finally Tabby could find out hey the what the the the the uh the the custom Gates I listed in uh at uh at at the end of sequence essentially uh is the one uh is the custom gate who satisfies uh the source codes uh in the source Noah program and finally uh Tabby generates custom gates for each component identified in the step two and use our domain specific language to represent the optimized code um so here uh the right the left hand side is the trace program and the right hand side uh is the synthesized but and optimized code uh Wren in our DSL and this d uh this domain specific program will be compiled into the uh concrete Halo 2 circuit and compared uh comp uh compared compared with the uh the the custom Gates uh Wren by the ZK expert or the uh normal Gates standard Gates uh generated by the compiler um the the the custom Gates um uh have a more have a more have a closer semantic uh to the source uh to the source uh computation so we uh so the uh the hello to Circuit generated by taby essentially is very similar to uh the table right uh the the table which uh which is generated by the uh D experts uh code and uh here is the evaluation result for the uh for the Tabby tool so the point one is that the C so the proven time of the circuits generated by tabi compared with the circuits generated by the no compiler has let's say four or five times faster so the point one is uh so so the so the point one here that the quality of the generated custom gates are not mattered if taby could find custom Gates the proving will be speed uh speed up a lot because the the the um because the quality of the generated Uh custom Gates by taby is various between benchmarks uh the point two here that the optimization space of existing compilation pipeline is still large because the table size generated by Tabby compared to as the table size uh the table size generated by the no compiler is uh let's say 10 times uh smaller uh in the average and uh for the uh for the proof size uh the proof size generate uh the proof size generated by Noah and uh and the proof size generated by taby uh essentially are quite different um so the point three here that both the time cost and proof size can be optimized to enhance the E econ uh e economic efficiency of the DK proof uh system because the pro the proof must be submitted to let's say layer one or other uh gas fee count uh blockchains uh to do the ZK Pro uh verification and uh that's all for today and our conclusion that the taby efficiently brid Bridges the gap between programmability and efficiency in they knowledge proov circuit generation and welcome to follow us on the Twitter and scan the telegram to have the further contact to the newb team uh thanks for the listening