CDAP Development Update #1

Date: 1 July 2021
Author: Ying Tong (yingtong@z.cash)

Background

I'm contributing to zkEVM, a project led by the EF's Applied ZKP group. The aim of this project is to verify a valid Ethereum state transition inside a SNARK circuit. This extends the functionality of zkRollups beyond simple transfers, to support Ethereum transactions.

WIP spec: https://hackmd.io/Hy_nqH4yTOmjjS9nbOArgw
WIP state proof spec: https://hackmd.io/Nwd0e5AgTVSBWRQlp-Ving
WIP circuits: https://github.com/appliedzkp/zkevm-circuits

We are writing our circuits using the UltraPLONK arithmetisation as implemented in halo2: https://zcash.github.io/halo2/concepts/arithmetization.html

Progress

1. High-level design

Note: Many parts of the proposed design are still in flux, but the high-level architecture is stable. I document here my high-level understanding.

The validity proof is actually composed of two proofs: the "state proof" and the "EVM proof". These proofs share the same public input: a commitment to the "bus mapping", i.e. the witnessed operations involved in the state transition.

A global_counter is initialised for each proof. This counts the number of operations (read / write / push / pop) performed in the circuit.

a) State proof

The state proof checks that the message calls perform legal reads and writes on memory, storage, and the stack. This includes checking that:

all opcodes used are legal;
all addresses accessed are legal;
a READ does not alter the value accessed;

To check whether a value is legal, we pre-load lookup tables of allowed values, and constrain witnessed values to be a subset of these tables.

Operations in the state proof are ordered first by the address they access, and then by global_counter.

b) EVM proof

The EVM proof checks that the witnessed values correspond to valid operations. This includes checking:

the business logic of message calls. For example, for a message call involving the opcode ADD, the EVM proof checks that the value of the witnessed sum is consistent with the values of the witnessed summand.
the program_counter, which is the byte offset in a smart contract's bytecode, is updated from one operation to another in an expected way. For example, a PUSHX should increase the program_counter by ++ (1 + X); a JUMP should set the program_counter to the location of the jump.

Operations in the EVM proof are ordered by global_counter.

2. (PoC) State proof memory subcircuit

This is a partial implementation of the memory subcircuit in the state proof:
https://github.com/appliedzkp/zkevm-circuits/blob/main/src/state_circuit/memory.rs

3. Possibilities for inter-operability

The zkEVM circuit is designed with zkRollups in mind; separately, I'm interested in how it can be used for interoperability. For example, two EVM-compatible chains could each verify transactions on the other, without having to re-execute the transactions. This would mean that any contract on Chain A could directly use the outcome of a transaction on Chain B.