zk Dev tooling | Soowon Jeong, PSE | ETHTaipei 2024

uh I'm Swan Jong from PSC team so and today's my talk is about ZK development tools so it is kind of introducing several Frameworks and just not going deeply for the technically so first I will introduce some tools for writing circuit with existing libraries like sarcom hello2 or zkm and next I will explain about circuit safety and tools for it with like uh formal methods and static analysis and lastly it is very rarely used techniques for the Frameworks but it is writing own modular system with acas or modular libraries so let's start with ZK circuit development so when people are starting to code their circuit then they would wonder that how to write a circuit U before they get that answer then they will get another question that is so what is circuit so I think the circuit is the procedure of computation theorically so it consists of gates which are addition or multiplication and it is also directed to cyclic graph so it gets input from outside and then it will calculate the output with topological order so it's ckp from circuit so so all zkps are from proving schemes and they will Define what to prove inside of the protocol so all proving schemes just have um kind of concering system inside of it so it is not the circuit what I mentioned before so it's kind of the relation of polinomial so in rncs it is a matrix multiplication so it's a series of polinomial and also in plish arithmetization it is also a series of pols so this gap between the theoretical circuit and the circuit development can confuse what is the ZK circuit development so we call it circuit but actually it consists of the relations of conditions and rules of allocating values to these conditions so it is why ZK dsls have two parts which are constraint generation and witness generation so you should be aware of this fact that circuit is not a program and but it is a set of constraints and rules of allocation to this relations so let's see with real work examples so circom is our most famous ZK DSL for now so it has constraint Genera ation with this three equal signs in the code and with this generation part is other parts except constraints so snar JS does with generation with this other with um other part of wasm or generating from this circom compiler so it's a very lowlevel framework so there is no overhead for making constraints so I I think it is hard to understand workflow at first because all parts are integrated to the same code but it is actually very different for the workflow and Halo 2 is very famous for used by CK evm and it is also very complicated so you can understand constraint as relations that is defined before values come inside and the conr generation part is up to the abstraction but you can think it is a configuration for some kind of relations of values and witness generation is for assigning values to the Circuit so it is also very low level and can be hard to understand because all Logics are hidden in the Ros code so there are many approaches to reduce this hardness of understanding for the circuit so the one of approaches is hello to wrong made by PSC team so it is a kind of abstraction layer for General use so it has three layers for this inside so main gate is the base layer for the library so it has all arithmetic operations pre predefined arithmetic operation inside so you can just bring it to your code and just integrate to your code base and ECC and nonnative arithmetic build arithmetic is built on that so it can be used to many cryptographic Primitives as well so you don't need to Define any gates with this hell to wrong library and there is very different approach for eliminating constraint generation and withness generation which is jkvm so gkbm is kind of making circuit but all things are predefined before your code so CK Pro CK BM proves the execution of BM so if you write a program then compiler will will generate the BM execution trace and then the pro proves the execution trace of BM so let's see how it reduces the constraint generation and withness generation so so circuits are predefined for each instructions of BM and your code will be one of instructions in the for the BM so for example like add instruction so if you write the addition in your code then it will compile to add instruction and also constraints are already defined in the VM so you don't need to write the constraint generation logic or witness generation logic in the for the CBM but however it is it can make an overhead for for sure because you know the like if you write assembly program then it is very optimized but if you write the c or Ross program that it will generate the like bunch of calls for the same logic so next we'll see tools for circuit safety so the circuit safety is very important for the zkp because it is utilized to uphold user privacy or like verifying computational Integrity so let's see let's review this epistemic gap of circuit development so you can see that theoretical circuit and circuit written in DSL are very different I mean for your information is really different but I mean yeah for abstraction so the theoretical circuit is a procedural comput ation by topological order but in the circuit written in DSL is kind of arithmetic relations between the values so this Gap can make vulnerabilities to your circuit and also the ZK circuit is very different from the program this orinary program is uh python for checking whether X is zero so it returns one if x is zero and else then returns y uh zero but in this gkp circuit is also beave same but you should make more constraint because why it's is not initialized so it can be any field element so you should make constraints for that so so there are several common vulnerabilities for GK circuit and you can check it in the this gab repository by Z Spark so in my opinion just I think under constraint circuit is most dangerous Spock for circuit so under con circuit circuit is the circuit that doesn't have all of the required constraints for the circuit so multiple output can satisfy the same constraint for the same input so last example this this is a decoder circuit that decodes input for to the output so if the W is the length for the decoding value and if the input is bigger than length then it it will fail and the success value will be zero so when you put two to W and want to input then you can get um out zero should be zero and out one should be one and success will should be one for a bid case but this invalid input just satisfies this circuit because this assignment is not constraint it's just assignment so it is not affect to the Circuit constraint so to prevent this error there are several tools for check this under constraint problem so there there is circumspect which is static static analyzer lter for circum which is made by Trail bits and this is a common line interface tools so it can get the warning from On Assignment or like un constraint and next tool name pus is made by bise and it checks the uniqueness property of the values so it uses static analysis and smt solber and it is announced with this paper and it will make counter example which I mentioned before just they have several out possible outputs for same input so it can be B for the circuit and next tool is named correct and this is for checking correctness of Halo to circuit and it is made by Quant stamp and as known as hello to analyzer so it is checking on us gate and on constraint cell and on used column with the hello to code so for most tools are for sarom or RCS but if you are so if you are new to ZK I recommend using comfor safety however many stating methods and formal methods are made so I really I think really we need need more safety tools for ZK circuit for Halo 2 or the plish arithmetization and so for now just ZK circuits need to get audited before the production and next if you really want to make an extremely optimized thing then you can design modular structure for your work before using this technique you should be aware that uh it is it can be very dangerous for your uh security because all modular structure is audited for each but it doesn't guarantee that the whole integrated structure is also safe and also it is it can be over engineering for your work and I think it is not for simple circuit but for complex protocol like IBC or recursive snar folding scheme ckvm so workflow is like this you should select cryptographic protocol to use and you should find out which requirements are in the protocol like which field or elliptic curves should be used or which arithmetization is used and if it is interactive protocol then you should use f transformation and after that you can build with existing libraries um that implements this kind of requirements so I recommend using Rost because many tools are written in Rost for this cryptographic Primitives yeah from finder field analytic curb I think many works are using artworks fin field implementation or ZK cryptos so if you choose using existing library for the proving schemes or other components then you can like align the same find field implementation with it so if you need use and also if you need use like search in LP curb then you should find the any kind of implementation for L curb um for example BN curb in hello2 curbs and for arithmetization if you choose RCS to use then you can use RCS binary format made by ID 3 uh which is formalization of RCs format and and then you can use also parser in Ros made by zerol Network and for plish you can use fronen for the Halo to which is made by zash and with the plish arithmetization you can use H implementation for for proving system using plish it is modular system so it's front end is Jes and also you can replace the polinomial commitment scheme in the this modulus structure so it is very easy to replace some components in the library so you can do Benchmark or if you implement something on the top of that then you can just replace and do testing it's very easy to use and and also for the interactive protocol then you should use FIA sham transformation for sure so uh recently nimu was made by artworks it is performing FIA sham transform for public coin protocol so you can make your own like public protocol for this protocol and you can make your own using well-known Hesh like MC or posidon and addition of that just you can make a ZK BM with this powder toolkit is helps build GK VMS and similar proof Frameworks so you can set any VM frend for this framework so you can put the risk five or any other dkbm that defined by yourselves and you can use backend C hello to or E star so it it will generate witness automatically yeah thank you for listening so now we have five M minutes Q&A time does anybody have questions okay and so When developing your own own protocol um can you combine the Plage repo with the like the artworks like tooling stuff yeah yeah yeah you can just um if you want to integrate something on the top of that just you can align some like encoding for like field element or something then you can use it with any things with the modular system uh so the API itself is compatible the the API itself is it is it compatible yeah I think it's compatible with the artworks or some something else okay is there any like um like toy example repo that I can reference on is there any repo that is based on this kind of design like for example you use like plish um and then it also combined with the artwork tooling ah yeah so so did you ask about some other implementation that uses plish no no no uh I I'm asking like if there any like uh example repository that use the similar techniques uh which is using uh H plish repo and then uh intergrate with artworks ah I cannot remember the exact name but yeah I we'll talk about later okay okay thank you okay do you have an example repository that takes your modular approach yeah it's uh H to lasso which is made by tun Kim so it uses the lasso for the look up argument system for the plish aration and yeah doing some the name again Halo to lasso it's a yeah it's a kind of like a for dep tool but yeah you can use it for um uh what's a mature open source ZK VM ZK what's the most material points for ZK VM in your uh for ZK VM uh I think like um dkbm the DK DSL using zkm is kind of Noir or alio or CYO is just using gkbm for in the inside of the design of GK DSL um does anybody has have more questions okay thank you so much SU