HackMD - Collaborative Markdown Knowledge Base

Porting ethereum execution-clients implementation onto Risc-zkVMs with bounded soundness -------------- ### Movivation - a crazy project https://github.com/ethereum-optimism/cannon run compiled geth on MIPS emulated by EVM, its derived from optimistic rollup design. - Ethereum's multi-client iteract with zkEVM https://vitalik.eth.limo/general/2023/03/31/zkmulticlient.html ### Background As known, there are many types of zkVMs each targetting differrent goals. There are being categoried into type 1 - 4, quantitized by their deviation regarding to EVM specifications. There are few challenges in current PSE type-1 zkEVM implementations - **Few thousands of constraints** to assure arithmetics computation/state transition correctness. One of the reason is also because aggresively modeling each op code (instruction) as basically building block. As design of EVM op code is CISC style to support high code density and functionality richness, therefore to constraints those it's pretty high effort. - **High audit cost**. zkEVM need to accommodate every new iterations of EVM execution client new release accordingly. - **Non-settle opcode set** although EVM is turing complete, new EIP proposals keep emerging and new opcode will forsee to be add in the future. Everytime new opcode added there comes the effort of zkEVM. ### Soundness > TODO to literally explain why modeling arithmetics in small granularity can improve soundness ### Prelimenary Thoughts Instead of using DSL (such as Halo2) to build a new circuit to constrain the execution traces, which potiential exposing more risk of witness manipulation and lead to potiential soundness problem, how about we `hook` the soundness to the existing execution client implementation? > explain what is `Hook` In more detail: porting existing ethereum client via (zk-)llvm FE to IR, then to asm, then finally executed on RISC-zkVMs. The great benefit is zkEVM team will work on a RISC-zkVM, which number of constraints is bounded by a fixed size since the RISC-VM ISA didn’t change for the new EIP proposal adapted and merge. It's especially useful, since EVM still envolve rapidly. Any new ethereum client just release on github ci and once compile pass, the codehash will be push to block chain/consensus. Then we can design zkSNARK with public input + codehash to prove the execution correctness on the new RISC-VMs. With that, the audit effort for zkEVM after every new releases will also be elimiated - [Cannon: geth on MIPS](https://github.com/ethereum-optimism/cannon) - [How will Ethereum's multi-client philosophy interact with ZK-EVMs?](https://vitalik.ca/general/2023/03/31/zkmulticlient.html) ### Risc-VMs choice One thing can forsee is execution trace will be large since the circuit is expressed by a RISC ISA. However, there are not that hard after come across few inspiring posts - Towards a Nova-based ZK VM https://zkresear.ch/t/towards-a-nova-based-zk-vm/105 unbounded computation execution. - Extreme case: one-instruction set computer (OISC) https://en.wikipedia.org/wiki/One-instruction_set_computer which only 1 single instruction and able to achieve turing complete. It’s good for Nova which is uniform-IVC. ### Task breakdowns - [ ] Nova-benchmark improvement: compare Kzg/IPA accumulation schema with Nova folding schema. - [ ] Compile geth to LLVM-IR by gollvm. Setup Docker 20.04 for gollvm environment - Q1 how golang gc handling? terminate gc in IR level? - Q2 how to handle bit operation efficiently? - [ ] Compile LLVM-IR to RiscV program. - [ ] Implement Risk0 in CIRCOM, where the instruction is built from microopcode SUBLEQ. Constraints based on SUBLEQ as building block - [ ] Compile CIRCOM and import to Nova - [ ] Integrate Verkle tree lookup for register to handle memory constraint - [ ] Handle opcode constraint by Verkle tree - [ ] Introduce Formal Verification - [ ] Nova: import circom implementation + witness generation to follow https://github.com/privacy-scaling-explorations/Nova. ### VM Memory Replace memory lookup with Verkle tree and implemented pairing in R1CS. - memory using Verkle tree https://hackmd.io/vF1jobzsRoubyUASqQG0Zw Efficient pairing in R1CS - Pairings in Rank-1 Constraint Systems https://eprint.iacr.org/2022/1162.pdf Maybe memory/register and even opcode can be used in Verkle way. ### Formal Verification on Risc-V. [Formal Verification of SUBLEQ Microcode implementing the RV32I ISA](https://drive.google.com/file/d/1q9IJILMLIWW4Qq7yXyalnJZfxJMWoD_u/view?usp=sharing) best paper reward in #FDL2022, provide a good starting point to verify IR -> Risc-zkVM ISA correctness via formal verification. It use one instruction to realized the procedure. - here is ISA repo https://github.com/ics-jku/goldcrest-vp - and verification https://github.com/ics-jku/goldcrest-microcode-verification ### LLVM related target golang first - BE: risc-v is supported in llvm backend https://llvm.org/docs/GettingStarted.html#local-llvm-configuration - FE https://go.googlesource.com/gollvm/ > example build on [CI](https://github.com/advancedwebdeveloper/gollvm_build_process/pull/37/files) based on my test, still have version mismatch problem so I test few version to make it works #### gollvm cross compile setting - cmake setting for gollvm cross compile risc https://groups.google.com/g/golang-codereviews/search?q=gollvm%3A%20Add%20support%20for%20crosscompiling #### currently adapted solution Go compiler support compile go program into RiscV64, which even make thing more efficient. From go 1.18 -> go 1.19, it's from stack back to register base, see [this](https://danielmangum.com/posts/risc-v-bytes-go-1-19-register-calling/) ### Mess reference https://github.com/MarcoCrepaldi-iit/mOISC-dRISC C to LLVM IR to OISC (one instruction set computer) ### Possible Vision https://app.diagrams.net/#G1SXP8cfrjHtThwMDGEx_yStSi60OqMHMg ![zkEVM](https://i.imgur.com/lc6NUUZ.png)