# `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`](https://github.com/axiom-crypto/halo2-lib/tree/main/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`](./src/rlc/circuit/mod.rs). We extend `BaseCircuitBuilder` to support this gate in [`RlcCircuitBuilder`](./src/rlc/circuit/builder.rs).
  `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](./src/utils/README.md). 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](https://github.com/axiom-crypto/halo2-lib/pull/123). 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](./src/utils/component/circuit.rs) and [PromiseBuilder](./src/utils/component/circuit.rs).
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](./src/utils/README.md).