zkGeth Design

Changed History

Date	Memo	Editor
2023-09-27	update memory commitment methodology	@sungmingwu

Background

Apply ZK Proof on EVM execution correctness is the huge milestone for Ethereum. To prove EVM correctness, below categorize into 2 methods.

Method 1:

Write a separate zk circuit to model the EVM specs (yellow paper). Ideally, this make zk circuit agnostics to the implmenetation language, and so as client. However in reality, we usually stick to one execution client execution trace and convert to witness.

Method 1, to some sense, is what the PSE zkEVM currently adopt. This aggresive way somehow means write a new complex program to model EVM spec. Since program is write by human, audit effort is needed, and might not be easier to accomplish, since EVM state space is very complex, formal verification model is too complex and not achievable.
Besides, spec (EIPs) keep changing as new released

Method 2:

Here explore a different way to prove EVM execution, which is by proving Geth execution correctness instead. To achieve that, the goal is compiling Geth (golang) into a small and stable Risc-ISA, then intepreted by a Risc-VM.

An assumption: Geth in golang will be compiled to RiscEth in exactly the same functionality. No manual writing DSL.

The new Risc-based program will be called RiscEth.

Now the original problem reduce to another problem: prove the RiscEth program correctness. A Risc-VM will be implemented to execute the RiscEth, along with a zkSNARK to attest the correctness of RiscEth execution.

pic from https://medium.com/@sin7y/a-programmable-privacy-platform-for-ethereum-understanding-olas-design-principles-and-technical-8a47ff07e725 in paragraph zkDSL vs zkVM

Compare with zkDSL based circuit construction to attest EVM execution, which usually means need to write the constraints circuit in another DSL language, zkVM have its shiny pros, and of course come with few cons, which will be accounted for below.

Benefits

• Achieve all functionality in Geth naturally : EVM, precompile, MPT, … in one shot!
• stable and fix constraints due to stable and simpler ISA.
• Adapted to fast EVM envolution. New EIP will be automatically adapted by compiling new version of Geth.
• Control by zkTeam how to extending ISA, instead of passive extention from new EIPs merge. ISA will be pretty stable.
• Bound/Hook soundness closed with Geth implementation, less audit effort. Less under-constraints risk!
• No need for padding
• support dynamic feature, such as dynamic block, naturally like a charm

Of course come with few challenges

• since the arithmetical constraints now in more low level, one thing forsee is execution trace will be pretty long.

For long execution trace. usually it is bounded by the nth root of unity choice. However, after state-of-the-art computational unbounded folding scheme methodology is proposed, this problem can be addressed and solved maybe…ENTIRELY!! Detail will be giving below.

Rationale and Techstack

The monorepo is under https://github.com/hero78119/zkGeth

Detail design of VM will be in another docs

GETH

GETH will refer cannon, geth in MIPS project. Thanks to the modulo codebase, we can patching GETH MPT part. Instead of load from leveldb, we can replace it with hash pre-image Oracle and read from memory directly. A memory commitment will be provided, with few pre-defined memory address filling with opcodes/MPT root/pre state root/new block/mpt proof, mpt leaf etc information.

Special note for MPT path + leaf + rlp: Oracle will read those in global memory with a counter. This just need a very simple design on golang Oracle. Those global memory will be provided memory commitment in runtime, and memory commitment can be built from geth Geth execution trace.

ISA

we choose RiscV64

• support by go official compiler, by simply GOARCH=riscv64
• free software license.
• Well developed ISA with standard and whitepaper. Widely used for embedded system and micro-controller.

We choose to implement RiscV64 ISA by a unique microopcode SUBtract and branch if Less-than or EQual to zero, abbrev as SUBLEQ. It's turing complete OISC and has be study for years under the topic: One-Instruction-Set-Computer OISC.

The SUBLEQ instruction is a three-operand instruction, performing
a combined subtraction and branching operation

reg_a reg_b reg_c

• reg_b = reg_b - reg_a
• pc = pc + reg_c if reg_b <=0 else pc + 1

Such simple microopcode can implement any computation, and so as Risc ISA. This microopcode can also be used as building block for formal verification if ISA, and circuit. More detail will be below.

Formal Verification

all the opcode will be implemented in microopcode SUBLEQ following this project

Formal verification will be introduced follow this paper (best paper reward in #FDL2022)
Formal Verification of SUBLEQ Microcode implementing the RV32I ISA to assure microopcode procedure is implemented correctly.

IVC Risc-VM

So far, Nova IVC is one of the state-of-the-art fast IVC: prover no FFT/quotiant computation, and claimed to be smallest verifier circuit. For R1CS, the dominated just few vectors dot product (no sum) + multi-scalar multiplication. With Nova, we have strong condident to fold circuit into more granularity unit, and per opcode is nature choice.

Another killing feature of Nova folding is its unbounded computation, means there is no restriction on circuit hyper parameter setting, max length of execution trace from Nth root of unity, etc.

More detail on Nova refer to reading Towards a Nova-based ZK VM

To avoid build everything from scratch, there is a plan to fork an existing ZK Risc rust implmentation https://github.com/risc0/risc0 with below planned modification

• Support RiscV64 ISA, currently it's RiscV32. The change is easier, since major difference is memory/register width is on bit64.
• replace STARK proof with Nova-Based folding scheme + SNARK.
• implemented opcode circuit in bellmon follow Nova, with SUBLEQ microopcode as the unit. Implemented SUBLEQ
• Risc circuit implemented in zkVM toolings Powdr, and integrate SuperNova as proving backend.

Supernova follow up works has been shift to Lurk-labs Nova fork Arecibo.

The IVC will be fold per opcode based. It's follow SuperNova non-uniform IVC.

Conceptual diagram

Per folding step circuits F_op(pc) in R1CS involving

• opcode verkle proof circuit
• memory verkle proof/register verkle proof circuit
• opcode arithmetics (by SUBLEQ) buiding block circuit
• IVC verifier circuit

Here, SuperNova non-uniform-IVC is adapted to reduce the folding steps. Another possible way is flatten all ISA into SUBLEQ and just using uniform-ivc, however it will exponeitiate steps of folding. We still choose SuperNova as it preserve the space for exending instruction in the future.

Just keep in mind, we need a tool, i.e. formal verification, to verify the security/correctness of ISA, especially when we extended.

zkSNARK on RiscV Nova & Public Input handling

Follow Von_Neumann and RiscV, we will prepare program opcode/public inputs/register/memory into a rw (memory)commitment. For program opcode, memory commitment will be pre-process and populated during execution client release on CI. In the process of SNARK proof generation, prover/verifier need to merge pre-processed program commitment, initial register value, along with other public input related to eth block execution (storage root merkle proof..) into a single public input commitment. Commiment merge rely on the underlyine commitment scheme. We plan to adopt rw lookup tricks solution Lookup Argument in Nova tricks: permutation checking without re-ordering

Reference link

• Lookup Argument in Nova tricks: permutation checking without re-ordering
• [Proto-Danksharding](EIP-4844 https://eips.ethereum.org/EIPS/eip-4844)

VM Memory Layout

Key generation steps

Geth Oracle design

File Descriptor R/W

TBD

Step Circuit F_op(pc) Circuit Layout in R1CS

TBD

Challenges

Folding Steps

• One folding step including up to 2 register/memory to read and 1 register/memory to write. Implemented verkle tree based on R1CS need careful benchmark
• SuperNova one opcode need one R1CS instance, whereas in RiscV64 ~40 opcodes means there will be 40 running instances. With curve cycling, it might be double running instances. In curve cycling, it's #opcode + 1 running instance, where the 1 come from the opcode folding.

Opcode efficiency

• There will be longer opcode especially for bit-operation. However comparing with Verkle verification circuit it might be negligible.

Security

TBD

Benchmark

The most important for PoC is benchmark. Before benchmark, there might need 2 data

• avg instruction count / ethereum transaction
• avg numbers of SUBLEQ per opcode

Then we can estimate the time to prove one transaction by #avg execution trace/#folding per second. Same method can be applied on block.

POC Milestones

• (Ongoing) Lookup scheme in Nova R1CS
  • https://github.com/lurk-lab/arecibo/pull/48
  • https://github.com/powdr-labs/powdr/pull/453
• 30 June 2023: vm(emulator) + minigeth successfully run through a transaction.
• 27 June 2023: Pending for golang riscv memory alignment fix https://github.com/golang/go/issues/61018
• 25 June 2023: Completed minigeth oracle to read memory image in sequencial https://github.com/hero78119/minigeth/commit/68a8f370e4753e8f20ee12f7849a190f271732cc
• 25 June verified cannon oracles patch approach on helloword example.
• 6 June 2023: VM can successfully run golang helloworld. support RIV64 isr along with few linux syscalls patching + mmap to support golang runtime.
• 24 April 2023: Partially porting GETH in Risc execute on VM.
• 21 April 2023: integrate risc0 and use gnu tool objdump to inspect the elf binary file compiled from sha example vs go build, result looks promising
• 20 April 2023: inspect minigeth RiscV64 elf
• 19 April 2023: successuflly compile minigeth to RiscV64 via go compiler.

How about multi-client ?

Multi-client will be prompt to discussion, as in the future they might all need to interect with zkEVM.

See the Vitalik post Ethereum’s multi-client iteract with zkEVM

Below is a conceptual idea for Nova-baase RiscVM to support multi-client.