axiom-eth

This crate is the main library for building ZK circuits that prove data about the Ethereum virtual machine (EVM).

Modules

Primitives

The rest of this crate makes heavy use of the following primitives:

• halo2-base Specifically the BaseCircuitBuilder and LookupAnyManager.
• rlc: In this crate we introduce a new custom gate, which is a vertical gate (1 advice column, 1 selector column) using 3 rotations. This is in PureRlcConfig. We extend BaseCircuitBuilder to support this gate in RlcCircuitBuilder. RlcCircuitBuilder is the core circuit builder that is used in the rest of this crate.
• keccak: The keccak hash plays a very special role in the EVM, so it is heavily used in chips in this crate. The keccak module contains an adapter KeccakChip that collects requests for keccak hashes of either fixed length or variable length byte arrays. It is very important to note that the KeccakChip does not explicitly constrain the computation of these keccak hashes. The hash digests are returned as unconstrained witnesses. The verification of these hashes depends on the concrete Circuit implementation that uses the KeccakChip. To that end, we now discuss the Circuit implementations in this crate.

Circuit implementations

This crate has three main Halo2 Circuit trait implementations:

• RlcKeccakCircuitImpl: this is the most direct circuit implementation. It creates a standalone circuit with a RlcCircuitBuilder managed sub-circuit as well as a vanilla zkEVM keccak sub-circuit. The keccak calls collected by KeccakChip are directly constrained against the output table from the zkEVM keccak sub-circuit. One creates such a circuit by implementing EthCircuitInstructions.
• EthCircuitImpl: this creates a circuit with a RlcCircuitBuilder managed sub-circuit. In addition, it loads a table of keccak hashes (and their inputs) as private witnesses and outputs a Poseidon hash of the table as a public output. The keccak calls collected by KeccakChip are dynamically looked up into the table of keccak hashes. One creates such a circuit by implementing EthCircuitInstructions. It is important to note that a proof generated by this circuit is not fully verified yet: the loaded keccak table must be verified by constraining the Poseidon hash of the table equals the public output of a KeccakComponentShardCircuit that actually proves the validity of the table. This must be done by an aggregation circuit.
• ComponentCircuitImpl: this is part of the Component Framework. See there for more details. Note that the implementation of EthCircuitImpl is really a specialized version of ComponentCircuitImpl since it uses the same PromiseLoader, PromiseCollector pattern.

Data structures

• rlp: this module defines RlpChip, which heavily uses RLCs to prove the correct encoding/decoding of RLP (Recursive Length Prefix) serialization.
• mpt: this module defines MPTChip, which uses rlp and keccak to prove inclusion and exclusion proofs of nodes in a Merkle Patricia Trie (MPT).

Ethereum execution layer (EL) chips

• block_header: proves the decomposition of an RLP encoded block header (as bytes) into block header fields. Also computes the block hash by keccak hashing the block header.
• storage: proves account proofs into the state trie and storage proofs into the storage trie.
• transaction: proves inclusion of an RLP encoded transaction into the transaction trie. Also provides function to extract a specific field from a transaction.
• receipt: proves inclusion of an RLP encoded receipt into the receipt trie. Also provides function to extract a specific field from a receipt.
• solidity: proves the raw storage slot corresponding to a sequence of Solidity mapping keys.

Circuit Builders

This is an abstract concept that we do not codify into a trait at the top level. This crate builds heavily upon halo2-base, and specifically the use of virtual region managers. Within this framework, circuits are written using circuit builders, which is some collection of virtual region managers. A circuit builder owns a collection of raw Halo2 columns and custom gates, but stores the logic of the circuit itself in some virtual state. The circuit builder may then do auto-configuration or optimizations based on this virtual state before assigning the raw columns and gate selectors into the raw Halo2 circuit.

Therefore for each phase of the Halo2 Challenge API, there are two steps to writing a circuit:

• Specifying the assignments to virtual regions within the circuit builder
• Assigning the raw columns and gate selectors into the raw Halo2 circuit

In this crate we make heavy use of Random Linear Combinations (RLCs), which require two phases: phase0 and phase1. Phase0 corresponds to the FirstPhase struct in raw Halo2, and phase1 corresponds to the SecondPhase struct. Because the correct calculations of the virtual assignments in phase1 require a challenge value, phase1 virtual assignments must be done after phase0 Concretely, this means that one cannot fully pre-populate all virtual regions of your circuit builder ahead of time. Instead, you must specify a function for the virtual assignments to be done once the challenge value is received.

The above motivates the definitions of the core traits in this module such as CoreBuilder and PromiseBuilder. These are traits that specify interfaces for variations of the functions:

• virtual_assign_phase0
• raw_synthesize_phase0
• virtual_assign_phase1
• raw_synthesize_phase1

These four functions are all called in sequence in the Circuit::synthesize trait implementation in raw Halo2, with the phase0 columns being commited to between raw_synthesize_phase0 and virtual_assign_phase1 so that the challenge values are availabe starting in virtual_assign_phase1. (The other technical distinction is that virtual_assign_* can be called outside of Circuit::synthesize without a Layouter, for any precomputation purposes.)

Most of the time, one circuit builder can be re-used for different circuit implementations: the raw_synthesize_* logic stays the same, and you only need to specify the virtual_assign_* instructions to quickly write new circuits.

Phase0 Payload

Results/data from phase0 also needs to be passed to phase1 to "continue the computation". Ideally one would use Rust closures to auto-infer these data to be passed between phases. However due to some compiler limitations / possible instability, we have opted to require all data that is passed from phase0 to phase1 to be explicitly declared in some kind of Payload struct. These should always be viewed as an explicit implementation of a closure.

Component Framework

See README.