Advancing Towards ZK Fraud Proof - zkGo: Compiling L2 Geth into ZK-Compatible Wasm

Transcript

[Music] e

e e of the example like etherum and current

plan is to use in the data availability Technologies so that each node does not need to download all the data but rather than just have the pieces of data and then be able to sample the data the rest of data in the network to know that oh data is guaranteed to be uh download by everybody in the network so that's basically the target of Da and also there requires some like a requirement in terms of CPU for example it requires uh some decent core number of cores of CPU with uh some memory and also storage uh for example a fresh etherum no Nows require about 1 taby of the storage and sometimes grows grows

higher because uh it has to have some intermediate stage during the execution um so to solve the CPU requirements and also the storage um the basic idea here is to using some uh proving mechanism for example eum proposal uh is for status uh n client um so that we can quickly verify the execution because here we just need to validate so we can quickly verify this execution of this this results uh using noow performance CPU or the CPU can be smart contract on top etherum that is for ler 2 and very small amount of the

storage just maintain some key minimum data um using the constraint uh resource constraint environment uh which definitely can be um our notes like cell in our cell phone or in our like eyewatch or the lay blockchain and that is the Smart contract so in the EV ZK EV category it sometimes is called type zero evm why it's called type zero because it's super General and which means that we are able to use in any language of code to write all this uh uh like just like a normal execution client but then we can proofy re introducing for example new circuits

um in maybe different from uh ZK setup like plish so what is ZK um mm is generally uh uh we try to solve the problem this all satisfaction a satisfactory problem that given a program and the instruction set architecture examp it can be Ms it can be War it can it can be xx6 we want to verify that given the input output of this uh um of this watch machine and its execution result is uh is correct and so in order to verify this we first need to choose a Isa um so

there are couple of Isa that we can choose for example Warson RIS 5 Ms those are open source which means that we can use them freely and definitely there are also x86 which proprietary and arm and we have a compiler which basically is able to compile any High Lev languages to this lowlevel um lowlevel instructions so on the right hand side is uh Assembly Language called web web ass web Assembly Language you know in terms ofb W format um tells what is a very simple instructions to add two variables so here we choose to using the Warson languages to to prove a long

execution of the the waron uh that so that we can compile any high level language code in wson and prove execution is execution is correct uh why we want to using uh wson because wson is becoming most popular uh language in the internet uh for example almost all the computer with a browser supports execution of Wason and so that like we also have a bunch of the tools that support execute the wson uh like like languages or compilation and um so next question is which language we would like to choose

to program the bit uh the blockchain and and then we would like to translate to a a warom language that can prove as ZK and here we Ed the Goan why because goine is perhaps one of the I would say easy to learn language we pretty uh a capability to scale so on the right hand side is one of my favorite graph which shows how many years so 6 months two 1 years 2 years 3 years 5 years and then on the on the Y AIS is the percentage of the programmer can believe he's mastering these languages so for go it just take about a couple months or one

year so that there are every developer is quite confident that they they can understand how it works can safely write a code and there are a couple of other language I think there one is c c languages the their the curve can even even goes down because when I use C language to write some code I feel oh there are so many new features that realize that oh I have to learn more and learn more and then I realize oh actually there's a lot of things I need to understand and so it's because it's so complicated and I also have copy collection all these features that can also simplify the burden of Developers and in the uh e World um go go L is also widely to develop a client uh for

example both famous like consensus client and execution client the go go implementation are the most popular ones for examp go ethereum at the time of writing after about a couple months ago yeah it's more than 80% of the adoption right now is a little bit decreased and also prison is also in goem um and also if we check the historical of the execution layer or cons layer development you can found there's a kind of meth effect that once the client has been adopted for more then it will be more people to to maintain it to fix it and then it become more stable and then more people will

come come further to use it and and and this goes to this circle then it will become more and more people using one specif specific type of client and this is happening and that's why even like ether is encouraging for client diversity but still a lot of people uh including myself uh using go as my U St curse so now with this all this environment setups we would like to narrow down what we like to achieve so the first of all we have the we want to uh compile the lay to execution layer that is return in go sometimes we call ler to gas or op gas and then compare it

into the Wason and then we have a wassom verifier approver that can prove that this long execution of this of wsom code is correctly um so that we are able to useing very constraint environment including uh for example L one smart contract or or or even like iatch to verify that the execution is correct and this is one of the I think the candidate for the future ethereum and game and this is a really good study point but when we dive into the details to implement all this they found there's a lot of challenges first of all even though wasm is widely adopted in like

for example for all the browsers it is more suitable to for an internet browser environment with very limited Ed interfaces to perform for example system course like Al for example create a a connection s raw socket to connect to the underlying resources or accessing the files and so here we list all the basically key challenges both in terms of the the browser environment that wasn't the compiled go ethereum in wasm that is uh basic looks like and so that we are not able to using the ZK environment which because ZK only have

two inputs private input public input done so we need to change this kind of like Hol environment that is the interaction between the morom code and the host this this this external environment so to make sure that we still able to execute the correspond layer to gas but with minimum changes of this code second is that there's a huge diverge models there versus Wason and also the the Wason model that as I mentioned in the ZK envirment that's public and private inputs there's also a couple of others for example floating Point instructions that is not able to support in most of the ZK VM setup and

lastly is some uh like imp detail implementation of goand that have really weird execu uh the exit semantics which is uh uh quite different with what we expect so for example uh here is a code that we compare the um the go the go ethereum the lay to go ethereum and then we here list all the uh apis that the warom code relies to you can imagine kind of assistant code so that they can execute the code correctly and all these apis for example have file descriptor refile descript write clock read and all

kind of things are essentially impossible to be supported in the ZK environment how we able to translate all those F into a ZK friendly interfaces with public input and private inputs this is something we have to address and so this is the basically the the target of Z goal first we do not want to reimplement the go compiler into go to the wasn't by ourselves so we made a deep modification of the go compiler and so that with some um some modification we want like to have it to be able to directly compile any go go

land into ZK friendly Warson so the ZK go is uh basically open source and we also work closely with our collaborators to make it happen and or one mean I would say a attractive feature of the ZK go is that it maintain support most of the go features for example garbage collection and go routine is also supported but written in the warom languages with this IO so that you just need about uh three dependency of their external host environment public input private input

and there whether there's something that's wrong then it will exit the execution of the of the warm BM in early and so besides like replacing all this we also uh have for example replace the unsupported instructions like forlo instructions call using a soft float that is using the integers to mimic the execution of the floating point so that we can trans slate single floating Point instructions to multiple um integer in integer operations and and yeah a couple of things so uh let me see uh yeah this for

floating Point um instructions and so yeah this is something I would like to show so for example suppose I would like to write a symbol co go go code to verify uh like a a calculation of Bach sequence so if I using the traditional go code I will first read the data from for example from the CLI and then do some calculation that is uh 1,000 and then finally I print the corresponding uh outputs in the in because in the ZK environment we only have public input and private input so that we will first read two public inputs from the from external so that we are able to R ify

what is the inputs that the user Supply during the verification do the calculation and lastly and then we verify that the corresponding calculation result equals the same as the another public input this is basically how the ZK verification does like basically I I provide three public inputs the first two variables and and the results and then the ZK verifier will tell me whether it is correct or not so it is solving this fashion problem and since we are a go compiler so this is the uh so for for using go you just go build the Fibonacci uh go go

go program and using ZK go then it has the same semantics to using it just say hey I want to build the the the go code but the output will be the Wason um so that it will be generate a Wason code that can be directly proved by the ZK Wason improver for example here we using definers CLI uh which provides uh kind of like uh some parameters both into especially in terms of public inputs for example the first two initial variable of the Fage sequence would be zero and one and also would like to verify that the ending result is some large number

after doing the Fibonacci sequence in uh in like a 1,000 calculation and then we can basically using disci we can prove this language and also create corresponding the verifier in solidity and then deploy this verifier and to make sure that the code is is correct so in this way we greatly saves the developer Especial developers that we like to use in CK to solve their calculations without writing any circuits just write go L go whatever you want it can be even complicated as go it there um so for example one application that we are going to solve

is to verify the offchain execution of the of lay to gas layer to uh execution layer um so that we are able to for example to to use it in a CK for proof tell that the layer to sequencer when it post some result I can instantly challenge that this something is wrong and so the previous design using the binary section which I actually explained yesterday that it takes about 73 interactions of onchain to in order to figure out which instructions is incorrect and also uh need to um take about 7 days to settle so using Z ZK now

we are able to program all this L to in gas compare it into what wasn't and prove it using single transaction and verify on chain if something is wrong so this basic idea of CK fra proof uh we are glad that we received a grant from opack to support us to do the research in this area together with r z and also 01 Labs which are talking for def firm Isa so risk Z is talking for risk 5 and O Labs is talking for MPS we are talking for uh Wason and so the general goal is that we are able to Red have much l shorter latency just proof time plus one time

transaction and tells that hey there's something wrong on the op execution and for any general purpose like layer to gas and one feature I like most for the ZK FR proof is that it can be easily to upgrade to support new Ean eips for example 7702 because it compiles any for example layer one changes in new changes to the layer two and compile in the Warson and directly prove using Z VN Technologies so that the cost of supporting upgrade is almost

negligible versus in the traditional ZK VM like type one type two type three if you would like to support this new features in general they have to reimplement the circuits and Audits and all this highly complicated things uh and it's called ZK evm scary they're scared once there's upgrade introduce some for example new hash or new simple features they have to reimplement all these things in the circuits which is extremely difficult and very easy to produce new issues and takes time to verify and using ZK VN and fer approach we can instantly support all the new

upgrad just just copy the layer one code to let to gas recompile generate the corresponding the verifier upgrade done so and this will also help to contribute to the multi prooving system that we also participate with the risk zero and also the one labs and so we are able to uh compile the Layer Two um execution engine and that is op gas uh with some minimum modification of the go ethereum but uh gen generally some some basically some IO adaption and so now we are able to generate the whole wsom be able to

compile and then be able to prove it using the the whole ZK wassom uh setup um yeah and so we can do a lot of things because we can basically prove any arbitrary execution some one crazy idea is that we are able to prove a lot of offchain database like exampling all these things using uh ZK go without writing a specific circuit and and also we able to like do a lot of offchain calculation for example machine learning and then we can Us in the uh basically zk4 proof to prove that the offchain interference of machine learning is

running correctly and so we are also working with Hyper Oracle to help solve this uh problem and there are a lot of couple of interesting work to be done uh one thing is to accelerate this proving procedure because this require tens of billions instructions which is perhaps the largest proving system that we found in the world and so it require a lot of optimization like using paralyzation multiple like gpus so that they can run in parallel and so that they can save the CH and also be able to aggregate the proof proof of the proofs this is a b general idea so that we can um aggregate them and then using

a single proof to prove all these uh parallel uh proven results we are also working on customized host circuits uh especially for some instructions that commonly used in if they like PR PS ECC k uh we can use in customer circuit to support it so that we can reduce the uh the trace of the uh nity proof and also couple of new proving system like V mentioned there's a growing of the called smaller Fields like bons all these smaller fields and so how we are able to use utilize this smaller fields and to incorporate to proving the wasm co is a very like Frontier of this

direction that's uh all I have for this talk um so there's a lot of technical details I'm happy to answer more questions if you have thank [Applause] you any questions sure hello again um I wonder what like what how does this compare with the existing ckvm like uh starware for example or even I know this is notk evm so it doesn't necessarily run the etherum the evm protocol but it does in

any way uh I guess verify random or whatever programs so it kind of relates with risk zero in a way and also with Stark uh with starkware or CYO uh even though those are AR necessarily um compilable by via VIA high level languages but also like polygon M and all these uh kind of high level language compilers to uh to wasm what's the main difference or are are are just a competitor not not chaming just sometimes uh yeah there a great questions about the comparison with maybe other Solutions like stock Weare or for examp res I think I think I

should really put a table for the comparison because I I think I get too much much details today uh um so compared to stock Weare first they have their uh CK like a language is ISA um so that they are able to prove the language uh using their um car prover all this tools one major difference is that uh the for the Carol support of Carol is still uh the two set is still pretty in early stage I no there some idea that using Caro and write some a Lota code to Emil evm like Kaka is doing uh I think this is really interesting Direction um

but at the same time uh one thing is that they have to reimplement all those things in the Carol language but for us uh if people are familiar with ob stack so right now they Layer Two there or lay two gas is uh a minimum modification of go ethereum that is 1,000 lines of changes to many to support Bri between lay one and lay two the great benefit of this that we are easily to reuse existing mature Cod of gold ethereum that has been developed which I show why why it's been widely adopted because a lot of you see a lot of people are fixing it optimizing it so

yeah uh so we are we are able to uh reuse all these benefits compared to stock rare need to rewind this this stack in Carol and also make sure it is upgrade to the latest EV eips if there's some etherum upgrade almost every year and so for those things we do not need to worry about we just hey recompile merge the code recompile and then submit a new verifier on chain and done so this is I think the great benefits versus the uh stock rare approach cool yeah um I think I'm run time so happy to ask me a question um

I'll be here and yeah thanks for attending my talk [Applause]