---
tags: zkevm-circuits
---
# zkevm-circuits doc/spec draft
code: https://github.com/scroll-tech/zkevm-circuits.git `develop` branch
This draft may serve as a preliminary version of a part of future documentation/spec.
Notice that the document is <i>not final</i> and may change due to potential errors in my understanding of the codebase or due to frequent changes of the codebase itself.
Corrections, suggestions and comments are very welcome at any time.
## super_circuit
### Purpose
The Super Circuit is a circuit that contains all the circuits of the zkEVM in order to achieve two things:
- Check the correct integration between circuits via the shared lookup tables, to verify that the table layouts match.
- Allow having a single circuit setup for which a proof can be generated that would be verified under a single aggregation circuit for the first milestone.
### Architecture and Layout
```markmap
# super_circuit
## lookup tables
- tx_table
- rw_table
- mpt_table
- poseidon_table
- bytecode_table
- block_table
- q_copy_table
- copy_table
- exp_table
- rlp_table
- keccak_table
## sub circuits
- evm_circuit
- state_circuit
- tx_circuit
- pi_circuit
- bytecode_circuit
- copy_circuit
- exp_circuit
- keccak_circuit
- rlp_circuit
- mpt_circuit
## challenges
- after FirstPhase: evm_words, keccak inputs
- after SecondPhase: lookup_inputs
```
Each sub-circuit, such as evm_circuit, state-circuit, ... etc. are implemented as a `SubCircuit` of the super_circuit, that performs the verification of a specific part of the full Ethereum block verification.
In super_circuit, we configure each table and each sub-circuit as listed above. When synthesizing the circuit, we load each lookup table using its `load` method and we synthesize each sub-circuit using its `synthesize_sub` method (inherited from `SubCircuit` trait). New sub-circuits are build from Ethereum block witnesses using `new_from_block` method (inherited from `SubCircuit` trait). We use `Challenge` API to provide random numbers needed (see the section on `Challenge` API).
### `Challenge` API
We use the the newly added feature of `Challenge` API from Halo2. It produces random challenges according to the transcript at different stages of the proof generation through Fiat-Shamir procedure. Currently it is associated with three phases of the proof generation: `FirstPhase`, `SecondPhase` and `ThirdPhase`. The randomness is generated after the `FirstPhase` and the `SecondPhase`. This ensures, for example, soundness of nested use of RLC in EVM circuit. In our zkevm-circuits, we enable these challenges as defined in `util::Challenges`
```markmap
# Challenges
## after FirstPhase
- used for RLC evm_words and keccak inputs
## after SecondPhase
- used for RLC lookup_inputs
```
## evm_circuit
### Architecture
Our zkSNARK-proof system for the correctness of EVM execution trace is based on decomposing the latter into <i>execution steps</i> and enforcing constraints for each step/step state transition. We characterize each execution by its `StepState` consisting of the following components:
```markmap
# StepState
## execution_state
- InternalState
- BeginTx
- EndTx
- EndBlock
- OpcodeSuccessfulStates
- STOP
- ADD_SUB
- ...
- ErrorCases
- ErrorInvalidOpcode
- ErrorStack
- ...
## step_context
- rw_counter
- call_id
- is_root
- is_create
- code_hash
- program_counter
- stack_pointer
- gas_left
- memory_word_size
- reversible_write_counter
- log_id
```
An API layer `constraint_builder` is developed to build constraint expressions for each execution step/step state transition, including custom gates and plookups:
```markmap
## ConstraintBuilder
### add_constraint
- require_equal
- require_zero
- require_in_set
- ...
### add_lookup
- range_lookup
- opcode_lookup
- bytecode_lookup
- tx_context_lookup
- rw_lookup
- ...
### split_expression (used to split high degree expression to deg 2)
### store_expression (store those splitted expressions)
### build
- constraints
- curr step constraints
- first step constraints
- last step constraints
- not last step constraints
- stored expressions
- curr step height
```
At each execution step, we use `constraint_builder` to configure constraints for this step/step state transition, and we use a method `assign_exec_step` to fill in witness values into constraints. These are implemented for each `ExecutionGadget` that correspond to an opcode (methods `configure` and `assign_exec_step` for each `ExecutionGadget`). In our case, we often combine several opcodes into one `ExecutionGadget`.
The backend proof system is based on Halo2, so all constraints are implemented as Halo2 custom gates and plookups. We use `CellManager` to configure geometric layout of Halo2 cells that settle our constraints within an execution step. So indeed we have the following architecture:
```mermaid
stateDiagram
Step --> StepState
Step --> CellManager
ConstraintBuilder --> CellManager
CellManager --> Halo2
StepState --> ExecutionState
StepState --> step_context
ExecutionState --> ConstraintBuilder
step_context --> ConstraintBuilder
```
### Execution Layout
At each step, we enable 3 selector columns
- `q_usable`, if this step is a step that is actually used in execution;
- `q_step_first`, if this step is the first execution step;
- `q_step_last`, if this step is the last execution step.
Then we enable an advice column
- `q_step`, the dynamic selector for the start of this execution step since the witnesses of each execution step may occupy variable height in the circuit layout.
A few extra columns are enabled for various purposes, including
- `constants`, a fixed column, to hold constant values used for copy constraints
- `num_rows_until_next_step`, an advice column, count the number of rows until next step
- `num_rows_inv`, an advice column, for constrain that enforce `q_step` := `num_rows_until_next_step == 0`
In alignment with `Challenge` API, we classify all above columns as in phase 1 columns, so the expressions stored in them are classified into `Celltype:StoragePhase1`.
After that, a rectangular region of advice columns are arranged for the execution step specific constraints that corresponds to an `ExecutionGadget`. The width of this region is set to be a constant `STEP_WIDTH`=140. The step height is not fixed, so it is dynamic. This part is handled by `CellManager`.
For each step, `CellManager` allocates an area of advice columns with given height and number of advice columns as width. The allocation process is in alignment with `Challenge` API. So within the area of advice column allocated, `CellManager` marks the first batch of columns ( `N_PHASE_3_COLUMNS`=10) as phase 3 columns to constrain gate cells (`CellType::StoragePhase3`), then followed by lookup columns (`CellType::Lookup`, `LOOKUP_CONFIG`=8 Fixed, 4 Tx, 8 Rw, 4 Bytecode, 1 Block, 24 Byte, 1 Copy, 1 Keccak, 1 Exp so in total 52 columns, use phase 3 random challenge), then followed by phase 2 columns (`N_PHASE_2_COLUMNS`=10) to constrain gate cells (`CellType::StoragePhase2`), then followed by columns for copy constraints (`CellType::StoragePermutation`, 2 columns), and finally followed by phase 1 columns (all rest columns with in `STEP_WIDTH`) to constrain gate cells (`CellType::StoragePhase1`).
When inserting a new cell into a region that is restricted to a specific column type, say `CellType::Lookup` cells that are for one particular Lookup Table, `CellManager` always add it to the column with the shortest current height of inserted cells (columns that do not have inserted cells have height 0). If there are multiple cells to be inserted, we just iterate the above behavior. So this induces a "row by row" queries of cells, see figure below
When different column cell types occupy different height, it results the figure below:
Summarizing, the overall circuit layout for one particular step looks like
An example of the evm-circuit fills in the following witnesses (TODO, fill in more details in the part handled by `CellManager`):
|`q_usable`|`q_step_first`|`q_step_last`|`q_step`|`constants`|`num_rows_until_next_step`|`num_rows_inv`|Gadget Specific Witnesses (128 columns maximum)|
|-|-|-|-|-|-|-|-|
|1|1|0|1|...|5|1/5|...|
|1|1|0|0|...|4|1/4|...|
|1|1|0|0|...|3|1/3|...|
|1|1|0|0|...|2|1/2|...|
|1|1|0|0|...|1|1|...|
|1|1|0|0|...|0|$\infty$|...|
|1|0|0|1|...|6|1/6|...|
|1|0|0|0|...|5|1/5|...|
|1|0|0|0|...|4|1/4|...|
|1|0|0|0|...|3|1/3|...|
|1|0|0|0|...|2|1/2|...|
|1|0|0|0|...|1|1|...|
|1|0|0|0|...|0|$\infty$|...|...|...|...|...|...|...|...|...|
|1|0|1|1|...|3|1/3|...|
|1|0|1|0|...|2|1/2|...|
|1|0|1|0|...|1|1|...|
|1|0|1|0|...|0|$\infty$|...|
|0|0|0|0|padding|padding|padding|padding|
The constraints for opcode specific `ExecutionGadget` are classified according to the selectors corresponding to `q_step`, `q_step_first`, `q_step_last` and `not_q_step_last`. These constraints are built in `ConstraintBuilder::build`, in which each gadget's specific constraints are multiplied by the selector for this particular execution state.
### Lookup Tables
#### Logistics
During the proof of an execution step, we sometimes use plookup type arguments to verify the correctness of the evm behavior generated at execution. The rationale is that if we can find a recorded item in a lookup table that is equal to the current evm behavior for which we want to constrain, we assert the latter's correctness.
For example, when stack push/pops a stack element, we lookup the rw_table for the correct stack read/write behavior. Another example is the bytecode table that we can lookup to verify the correctness of bytecode stored in the contract.
We use `Lookup::input_exprs` method to extract input expressions from evm execution trace that we want to do lookup, and we use `LookupTable::table_exprs` method to extract table expressions from a recorded lookup table. The plookup argument aims at proving the former expression lies in the latter ones. This is done by first RLC both sides of expressions using the same randomness at challenge phase 2 (`lookup_powers_of_randomness` obtained from `Challenges::lookup_input_powers_of_randomness`) and then plookup the RLC expression (see discussion below on how we config lookups inside circuit).
In a lookup table, each column correspond to one lookup expression. For the evm circuit, there are internal and external lookup tables. We summarize them as follows:
- evm_circuit internal lookup tables
|Lookup Table|Columns|
|-|-|
|Fixed|tag, value1, value2, value3|
|Byte|value|
- evm_circuit external lookup tables
|Lookup Table|Columns|
|-|-|
|TxTable|tx_id, tag, index, value|
|RwTable|is_counter, is_write, tag, id, address, field_tag, storage_key, value, value_prev, aux1, aux2|
|BytecodeTable|code_hash, tag, index, is_code, value|
|BlockTable|tag, index, value|
|CopyTable|is_first, src_id, src_tag, dst_id, dst_tag, src_addr, src_addr_end, dst_addr, length, rlc_acc, rw_counter, rw_inc|
|KeccakTable|is_enabled (=1), input_rlc, input_len, output_rlc|
|ExpTable|is_step (=1), identifier, is_last, base_limbs[0], base_limbs[1], base_limbs[2], base_limbs[3], exp_lo_hi[0], exp_lo_hi[1], exponentiation_lo_hi[0], exponentiation_lo_hi[1]|
#### How lookups are configured in evm_circuit layout
The `add_lookup` method in `ConstraintBuilder` uses RLC to combine execution induced input expressions into an RLC expression and store it inside `CellType::Lookup` region handled by `CellManager`. Notice that this may be a result of expression splitting first, and only the first term in the splitted expression (the RLC term) will be stored in `CellType::Lookup`, and the rest are put into `CellType::StoragePhase3`. (<i>Remark</i>: The logic here is a little bit intrigue. Actually, `split_expression` throws `expr` into a celltype according to `CellType::storage_for_expr(&expr)` which is determined by `Celltype::expr_phase`. For an advice column, this `expr_phase` is then determined by the phase of Advice column. When we query advice columns in `execution`, we assign phase via `meta.advice_column_in`, so all lookups are assigned to be in phase 3 columns, thus their splitted expressions are in phase 3 storage cells).
At execution level, same RLCs (with `lookup_powers_of_randomness`) are done for the recorded table expressions, and `config_lookup` configures the lookup between the input expression RLCs and the table RLCs.
#### Are the numbers of lookup columns in the evm_circuit layout optimal?
In the evm_circuit, `CellManager` labels lookup columns in the circuit layout based on `LOOKUP_CONFIG`, which says, for example, we have 24 byte lookup columns etc. However since all these lookup columns are storing RLC values of actual witnesses that should correspond to a lookup table row (due to `add_lookup` method in `ConstraintBuilder`), the number of lookup columns in `LOOKUP_CONFIG` theoretically can be arbitrary. Say even if we had only 1 column for each table it is still working, but just it will make step height maybe too high so that prover has too much cost. So we can see that the number of `Celltype::Lookup` columns for each lookup table can leverage between prover&verifier costs. The numbers that we currently use (8 Fixed, 4 Tx, 8 Rw, 4 Bytecode, 1 Block, 24 Byte, 1 Copy, 1 Keccak, 1 Exp so in total 52 columns) may not be optimial and are subject to future tuning.
#### Nested use of RLCs and security concerns that are resolved by `Challenge` API
Nested use of RLCs happen very often in our constraint system when dealing with plookup type arguments. For example, `CallOpGadget` (in `callop.rs`) computes `callee_code_hash` by applying RLC to the byte array in little endian of `CodeHash`, using `evm_word_powers_of_randomness`. At the execution level, this RLCed `called_code_hash` enters as one of rw table witnesses together with `call_id` and `CallContextFieldTag::CodeHash`. When doing lookup to the rw table, these witnesses are to be RLCed again using `lookup_power_of_randomness`. So this induces a nested use of RLCs in the constraint system.
There used to be security concerns regarding this nested use of RLCs (see [EVM-summary-and-proposal] by Aurel). This is because the RLC function is a product of inputs with powers of a challenge, and when nested, the terms multiply and overlap with others, merging inputs additively, which is unsafe. Mathematically, when we multiply two random variables, we cannot guarentee the product is still random unless we are sure of independency of the two random variables. For example, if $X$ is uniformly distributed in $[1,2]$, then $\dfrac{1}{X}$ is also random but $X\cdot \dfrac{1}{X}=1$ is not random any more.
With the newly added `Challenge` API that produces different levels of randomness, this issue should be resolved, because we are using different levels of randomness at different levels of RLCs: when RLC `evm_words` we use `evm_word_powers_of_randomness` (challenge phase 1) and at lookup we use `lookup_powers_of_randomness` (challenge phase 2). These randomnesses are guarenteed to be not fully dependent on each other due to mechanism of Fiat-Shamir procedure.
[EVM-summary-and-proposal]: https://miro.com/app/board/uXjVPLsk0oU
### General Constraints (TODO)
explain general step-transition constraints
### Opcode Specific Constraints (TODO)
will be based on expanding [ConstraintAnalysisOpcodesGadgetsChips], analysis for each opcode, ensure their constraints are sound
[ConstraintAnalysisOpcodesGadgetsChips]: https://www.overleaf.com/read/gjnxcvsdrrjd
## state_circuit
### Purpose
State circuit aims to prove the correctness of evm's each read-write record at execution. In evm_circuit, all read-write records are listed in rw_table as witnesses. Each row of rw_table, i.e. `RwRow` has the following table columns:
```markmap
# RwRow
- rw_counter
- is_write
- tag
- id
- address
- field_tag
- storage_key
- value
- value_prev
- aux1
- aux2
```
For different types of evm read-write records, the above RwRow items may carry different types of information. We list them as follows
|evm read-write type|rw_counter (usize)|is_write (bool)|tag (RwTableTag)|id (usize)|address (Address, 20bytes)|field_tag (u64)|storage_key (word)|value (field element)|value_prev|aux1|aux2|
|-|-|-|-|-|-|-|-|-|-|-|-|
|Start|rw_counter|false|RwTableTag::Start|None|None|None|None|0|None|0|None|
|TxAccessListAccount|rw_counter|is_write|RwTableTag::TxAccessListAccount|tx_id|account_address|None|None|is_warm|is_warm_prev|0|None|
|TxAccessListAccountStorage|rw_counter|is_write|RwTableTag::TxAccessListAccountStorage|tx_id|account_address|None|RLC storage_key in le bytes|is_warm|is_warm_prev|0|None|
|TxRefund|rw_counter|is_write|RwTableTag::TxRefund|tx_id|None|None|None|value|value_prev|0|None|
|Account|rw_counter|is_write|RwTableTag::Account|None|account_address|AccountFieldTag::{Nonce, Balance, CodeHash, NonExisting}|None|value or RLC value's le bytes if AccountFieldTag == {CodeHash, Balance}|value_prev or RLC value_prev's le bytes if AccountFieldTag == {CodeHash, Balance}|0|None|
|AccountStorage|rw_counter|is_write|RwTableTag::AccountStorage|tx_id|account_address|None|RLC storage_key in le bytes|RLC value's le bytes|RLC value_prev's le bytes|only used for AccountStorage::tx_id which moved to key1, but actually the current code assigns 0 (check??)|RLC committed_value's le bytes|
|AccountDestructed|rw_counter|is_write|RwTableTag::AccountDestructed|None|account_address|None|None|is_destructed|is_destructed_prev|0|None|
|CallContext|rw_counter|is_write|RwTableTag::CallContext|call_id|None|CallContextFieldTag::{RwCounterEndOfReversion, CallerID, TxID, Depth, CallerAddress, CalleeAddress, CallDataOffset, CallDataLength, ReturnDataOffset, ReturnDataLength, Value, IsSuccess, IsPersistent, IsStatic, LastCalleeID, LastCalleeReturnDataOffset, LastCalleeReturnDataLength, IsRoot, IsCreate, CodeHash, ProgramCounter, StackPointer, GasLeft, MemorySize, ReversibleWriteCounter}|None|value or RLC value's le bytes if CallContextFieldTag == {CodeHash, Value}|None|0|None|
|Stack|rw_counter|is_write|RwTableTag::Stack|call_id|stack_pointer to big endian bytes last 20 bytes as address|None|None|RLC value's le bytes|None|0|None|
|Memory|rw_counter|is_write|RwTableTag::Memory|call_id|memory_address|None|None|byte|None|0|None|
|TxLog|rw_counter|is_write|RwTableTag::TxLog|tx_id|(index, field_tag, log_id) built into tx_log address|TxLogFieldTag::{Address, Topic, Data}, it is None in actual table and field tag info enters address|None|value or RLC value's le byte if TxLogFieldTag == {Topic}|None|0|None|
|TxReceipt|rw_counter|is_write|RwTableTag::TxReceipt|tx_id|None|TxReceiptFieldTag::{PostStateOrStatus, LogLength, CumulativeGasUsed}|None|value|None|0|None|
In state_circuit, we ensure that the following types of constraints are satisfied (for details, see the section on state circuit constraints):
- general constraints: for example, some of the items such as is_write shall be boolean, first access reads do not change value, etc..
- the correctness of each of the above form of read-write records as `RwRow` - the rows of the rw table are in lexicographic order, i.e. ordered by (tag, id, address, field_tag, storage_key, rw_counter) (`LexicographicOrderingConfig`)
- id, address and rw_counter come from the correct multiple-precision-integer (`MpiChip`)
- storage_key comes from correct RLC (`RlcChip`)
### Architecture
state_circuit is configured by first set up the following `Queries` of Halo2 columns
```markmap
# Queries
## selector
## rw_table: RwRableQueries
- rw_counter
- prev_rw_counter
- is_write
- tag
- id
- prev_id
- address
- prev_address
- field_tag
- storage_key
- value
- value_prev
## mpt_update_table: MptUpdateTableQueries
- address
- storage_key
- proof_type
- new_root
- old_root
- new_value
- old_value
## lexicographic_ordering_selector
## rw_counter: MpiQueries
## tag_bits
## id: MpiQueries
## is_tag_and_id_unchanged
## address: MpiQueries
## storage_key: RlcQueries
## value_prev_col
## initial_value
## initial_value_prev
## is_non_exist
## mpt_proof_type
## lookups
## power_of_randomness
## first_different_limb
## not_first_access
## last_access
## state_root
## state_root_prev
```
state_circuit uses `constraint_builder` to establish constraint expressions on these queries. `constraint_builder` builds constraints for each type of `RwRow` as well as some general constraints, so the architecture looks as follows
```markmap
# constraint_builder
## general constraints
- build_general_constraints
## constraints for each type of `RwRow`
### Start
- build_start_constraints
### TxAccessListAccount
- build_tx_access_list_account_constraints
### TxAccessListAccountStorage
- build_tx_access_list_account_storage_constraints
### TxRefund
- build_tx_refund_constraints
### Account
- build_account_constraints
### AccountStorage
- build_account_storage_constraints
### AccountDestructed
- build_account_destructed_constraints
### CallContext
- build_call_context_constraints
### Stack
- build_stack_constraints
### Memory
- build_memory_constraints
### TxLog
- build_tx_log_constraints
### TxReceipt
- build_tx_receipt_constraints (currently not implemented)
## establish constraint exprs
- require_zero
- require_equal
- require_boolean
- require_in_set
- add_lookup
```
Besides the above constraints, some of the queries are sent to specific chips for further verification, including
```markmap
# Chips in state_circuit
## lexicographic_ordering
### to ensure the rows of the rw table are in lexicographic order
- tag
- id
- address
- field_tag
- storage_key
- rw_counter
## random linear combination
(to ensure RLC correctness)
- storage_key
## multiple_precision_integer
- rw_counter
- address
- id
## lookups (for range checks u8, u10, u16 and call_context_field_tag)
- memory value is a byte
- stack address fits into 10 bits
- field_tag in CallContextFieldTag range check
```
Also, a few common math gadgets are used to constraint queries, including
- `BinaryNumberChip`
- tag
- `BatchedIsZeroChip`
- is_non_exist
The witnesses of state_circuit are taken from `block.rw.table_assignments()` as well as `block.mpt_state` (to determine whether there is any mpt updates). Given the rw rows and the mpt updates, `StateCircuitConfig::assign_with_region` assigns the witnesses to Halo2 region for constraint proof.
### Constraints (TODO)
Analyze general constraints used in `constraint_builder` and specific constraints in chips used for state_circuit, including `lexicographic_order`, `lookups`, `multiple_precision_integer`, `random_linear_combination`
#### general constraints:
- is_write is boolean
- check if first access
- ...
#### constraints for each type of `RwRow`
- Start constraints
- rw_counter increases correctly
- ...
- tx access list constraints
- state root remains unchanged
- ...
- tx access list account storage constraints
- state root remains unchanged
- ...
- tx refund constraints
- account constraints
- account storage constraints
- storage root is updated appropriately (`MptTable`)
- ...
- account destructed constraints
- call context constraints
- stack constraints
- memory constraints
- memory address fits into two limbs
- memory value is a byte
- ...
- tx log constraints
- tx receipt constraints
#### constraints in `lexicographic_order`
#### constraints in `multiple_precision_integer`
#### constraints in `random_linear_combination`
#### constraints in `lookups`
## bytecode_circuit
### Purpose
evm_circuit needs to lookup at the bytecode table that stores the correct bytecode information. This ensures that the bytes stored in the contract are the same as the bytes loaded in the table. The bytecode table has the following column structure:
|codehash|tag (u64)|index|is_code|value|
|-|-|-|-|-|
|RLC hash's le bytes using evm_word randomness|BytecodeFieldTag::Length|0|0|len of bytes|
|RLC hash's le bytes using evm_word randomness|BytecodeFieldTag::Byte|idx|is_code|byte|
|0|BytecodeFieldTag::Padding|0|1(check??)|0|
The bytecode circuit aims at constraining the correctness of the bytecode table. This includes:
- constrain the code size
- constrain the code hash
- ensure PUSH behavior: `is_code = push_data_left == 0` and lookup `push_table` for PUSH1-PUSH32
- correct propagation of each row within one bytecode
- type checks, such as boolean
- start, end and padding constraints
### Architecture
Raw `bytes` with the Keccak codehash of it `code_hash=keccak(&bytes[...])` are feed into `unroll_with_codehash` that runs over all the bytes and unroll them into `UnrolledBytecode{bytes, rows}`, which fits the bytecode table layout. This means each row contains `(code_hash, tag, index, is_code, value)`. (The only difference is that here `code_hash` is not RLCed yet.) Notice that only `PUSHx` will be followed by non-instruction bytes, so `is_code=push_rindex==0`, i.e. `unroll_with_codehash` computes `push_rindex` that decays from push size to zero and when it is zero it means the byte is an instruction code. With `UnrolledBytecode`, we contrain its rows via `BytecodeCircuit`, so the structure looks like
```mermaid
stateDiagram
bytes --> UnrolledBytecode
bytes --> code_hash
code_hash --> UnrolledBytecode
UnrolledBytecode --> BytecodeCircuit
BytecodeCircuit --> SubCircuit
```
The `BytecodeCircuit` is configured using the following columns, (internal and external) tables, as well as chips (which are just smaller-sized circuits):
```markmap
# BytecodeCircuitConfig
## selectors
### q_last
## fixed columns
### q_enable
### q_first
## advice columns
### push_rindex
### hash_input_rlc
### code_length
### byte_push_size
### is_final
### padding
### push_rindex_inv
### length_inv
## internal tables (within zkevm-circuits)
### bytecode_table
### push_table
- internally constructed via `load_aux_tables`
## external tables
### keccak table
## chips
### IsZero
- push_rindex_iszero
- length_iszero
```
Here we have
- `push_rindex` stands for the reverse byte index of push, i.e. it decays from push_size to 0 during each push operation
- `code_length` stands for the length of the current bytecode
- `push_rindex_inv`, `push_rindex_is_zero`, `length_inv`, `length_is_zero` are used to check is_zero for `push_rindex` or `code_length`
- `hash_input_rlc` is the RLC of the input bytes using keccak_input_randomness (a `SecondPhase` randomness, i.e. generated after `FirstPhase` of the proof, currently the same as evm_words randomness)
- `byte_push_size` is the push size of a push op
- `is_final` indicates the row with the last byte
- `padding` indicates whether this row is a padding row
`BytecodeCircuitConfig` uses `assign_internal` and `set_row` to assign `witness: &[UnrolledBytecode<F>]` into `BytecodeCircuit`. These witnesses are loaded from block bytecode data via `new_from_block_sized`.
### Constraints
- Type check:
- `is_final`, `padding` are boolean
- Correct `code_length`
- `code_length` is the bytecode_table length
- Constrain PUSH behavior:
- if current row is an opcode, then `push_rindex=byte_push_size`, otherwise it decays by $1$ from previous `push_rindex`
- lookup `push_table` to justify PUSHx behavior
- For any row that is not the first row nor the last byte row within one bytecode:
- `index` increase by $1$ except for the row with tag `length`, where index is $0$;
- `is_code=is_push_rindex_prev==0`
- `hash_input_rlc` is the RLC of bytes (input of keccak hash) using keccak_input_randomness
- `code_hash`, `code_length` and `padding` keep the same
- For the start row of a bytecode:
- if `length==0` then next row is padding, else next row is byte
- `value` is `code_length`
- For the last row
- `padding` is $1$ or last row is a last byte
- Constrain padding behavior:
- `padding` changes from $1$ to $0$ only once
and for the start of padding row:
- `padding` is $1$
- not the start of a new bytecode
- correct code_hash
- lookup Keccak table (Posidon hash table? in the codebase it is keccak)
## Keccak_circuit
See [KeccakDocumentation] for a documentation
Also see [KeccakCircuitLayout] for the current circuit layout for Keccak.
[KeccakDocumentation]: https://www.overleaf.com/read/qqhbxhmbkdkr
[KeccakCircuitLayout]: https://docs.google.com/spreadsheets/d/1Pe5kkcWsD6Go3oDTey3GT0vpscxpCxzj4DglzWXF5zc/edit?usp=sharing
## tx_circuit
### Purpose
tx_circuit provides constraints that validates the correctness of an ethereum transaction. According to this document of [ETHTransactions], a submitted (legacy) transaction got recorded by the ethereum network will include the following information:
- `raw`: RLP encoded form of the tx `RLP([nonce, gasPrice, gasLimit, to, value, data, v, r, s])`
- `nonce`: sequence number of tx
- `gasPrice`: tx gas price per gas unit
- `gasLimit`: the maximum amount of gas units that can be consumed by the tx
- `to`: callee address
- `value`: amount of eth value (U256) to be transferred by the tx
- `data`: CallData, this is used when tx creates a contract bytecode, in form of bytes and one row per byte
- `v`, `r`, `s`: signature of the tx sender, `v` (U64) is determined by ChainID, `(r,s)` (U256, U256) is the ECDSA signature
- `hash`: U256, Keccak-256 hash of the signed tx's data (TxHash in RLP table, it includes `Nonce`, `Gas`, `GasPrice`, `To`, `Value`, `CallData`, `v, r, s`)
[ETHTransactions]: https://ethereum.org/en/developers/docs/transactions/
Some metadata is also available for the tx circuit, which includes:
- CallerAddress: this is recovered from the tx and its signature using `ecrecover`
- IsCreate: bool, this is recovered by `rlp_tag==To` and `tag_length=1`
- CallDataLength: provided by the smart contract
- CallDataGasCost: U64
- TxSignHash: U256, Keccak-256 hash of tx's transaction data that needs to be signed (TxSign in RLP table, it includes `Nonce`, `Gas`, `GasPrice`, `To`, `Value`, `ChainID`, `CallData`)
The tx circuit aims at constraining the following aspects of tx
- lookup into tx_table to check correctness of accumulated `CallDataGasCost` on the last row of tx's call data bytes
- lookup into rlp_table to check
- tx's transaction data that needs to be signed (TxSign data, including `CallData`)
- TxHash data
- lookup into keccak_table to check
- TxHash data length and hash result
- TxSign data length and hash result
- correct behavior of tx id, cum_num_txs and call_data_length etc.
- tx_id increases in u16
- tx_id <= cum_num_txs
- lookup cum_num_txs in block table
- tx_id changes at the final `CallData` byte
- correct padding
- tx signature via ECDSA done correctly
- caller address recovered from ECDSA signature correctly
### Architecture
See this link for [tx_circuit-layout]
[tx_circuit-layout]: https://docs.google.com/spreadsheets/d/1CHKL7_7f954J29AoV67KTnjtFdXxtvvIWv3oaCW4YmU/edit?usp=sharing
q_enable|tx_id|tag|rlp_tag|value |is_calldata|is_create|is_final|call_data_length|call_data_gas_cost_acc|chain_id|is_tage_block_num|is_padding_tx|cum_num_txs|sv_address|LookupCondition::TxCallData|LookupCondition::Tag|LookupCondition::RLPCallData|LookupCondition::RLPSignTag|LookupCondition::RLPHashTag|LookupCondition::Keccak|
|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|
|1|1|Nonce|RlpTxTag::Nonce|txs[0].nonce|0||false|None|None|0|||||
|1|1|GasPrice|RlpTxTag::GasPrice|txs[0].gas_price|0||false|None|None|0|||||
|1|1|Gas|RlpTxTag::Gas|txs[0].gas|0||false|None|None|0|||||
|1|1|CallerAddress|RlpTxTag::Padding|txs[0].caller_address|0||false|None|None|0|||||
|1|1|CalleeAddress|RlpTxTag::To|txs[0].callee_address|0||false|None|None|0|||||
|1|1|IsCreate|RlpTxTag::Padding|txs[0].is_create|0||false|None|None|0|||||
|1|1|TxFieldTag::Value|RlpTxTag::Value|RLC of txs[0].value|0||false|None|None|0|||||
|1|1|CallDataLength|RlpTxTag::DataPrefix|txs[0].calldata.len()|0||false|None|None|0|||||
|1|1|CallDataGasCost|RlpTxTag::Padding|txs[0].call_data_gas_cost|0||false|None|None|0|||||
|1|1|SigV|RlpTxTag::SigV|txs[0].v|0||false|None|None|0|||||
|1|1|SigR|RlpTxTag::SigR|RLC of txs[0].r|0||false|None|None|0|||||
|1|1|SigS|RlpTxTag::SigS|RLC of txs[0].s|0||false|None|None|0|||||
|1|1|TxSignLength|RlpTxTag::RlpLength|rlp_unsigned_tx_be_bytes.len()|0||false|None|None|0|||||
|1|1|TxSignRLC|RlpTxTag::Rlp|RLC of rlp_unsigned_tx_be_bytes|0||false|None|None|0|||||
|1|1|TxSignHash|RlpTxTag::Padding|tx_sign_hash|0||false|None|None|0|||||
|1|1|TxHashLength|RlpTxTag::RlpLength|rlp_signed_tx_be_bytes.len()|0||false|None|None|0|||||
|1|1|TxHashRLC|RlpTxTag::Rlp|RLC of rlp_signed_tx_be_bytes|0||false|None|None|0|||||
|1|1|TxHash|RlpTxTag::Padding|RLC of tx.hash|0||false|None|None|0|||||
|1|1|BlockNumber|RlpTxTag::Padding|tx.block_number|0||false|None|None|0|||||
|...|...|...|...|...|...|...|...|...|...|...|...|...|...|...|
|1|1|CallData|RlpTxTag::Data|byte|1||0|5|16|0||false|||
|1|1|CallData|RlpTxTag::Data|byte|1||0|5|32|0||false|||
|1|1|CallData|RlpTxTag::Data|byte|1||0|5|48|0||false|||
|1|1|CallData|RlpTxTag::Data|byte|1||0|5|52|0||false|||
|1|1|CallData|RlpTxTag::Data|byte|1||1|5|68|0||false|||
|...|...|...|...|...|...|...|...|...|...|...|...|...|...|...|
|1|0|CallData|RlpTxTag::Data|...|...|...|...|...|...|...|...|...|...|...|
|...|...|...|...|...|...|...|...|...|...|...|...|...|...|...|
|1|0|CallData|RlpTxTag::Data|...|...|...|...|...|...|...|...|...|...|...|
|...|...|...|...|...|...|...|...|...|...|...|...|...|...|...|
|0|...|Null (padding)|...|...|...|...|...|...|...|...|...|...|...|...|
<i>Note</i>: For historical reasons tx_circuit's lookup arguments for the value column is actually replaced by the tx_table's value column. Thus PI circuit has to copy constraint on tx hashes, and can manually assign region_idx, row, column.
<i>Note</i>: `sv_address` column is the sign-verified caller address used for EIP2718 (?)
### Constraints
- lookup to tx_table for CallData (LookupCondition::TxCallData)
- When (1) tag is CallDataLength and (2) CallDataLength is not 0
- Lookup tx table to validate call_data_gas_cost_acc
- Lookup tx table to validate last call data byte in tx has index = call_data_length-1 when the call data length is larger than 0
- lookup to RLP table for CallData (LookupCondition::RlpCallData)
- When (1) tag is CallData and (2) CallData byte is not 0
- Lookup RLP table to validate tx calldata bytes for TxSign and TxHash
- lookup to RLP table for TxSign tag (LookupCondition::RlpSignTag)
- When tag (tx_tag) is one of the following: Nonce, GasPrice, Gas, CalleeAddress, Value, CallDataLength, TxSignLength, TxSignRLC
- Lookup RLP table to validate the value correspond to any of these tags with RlpDataType::TxSign
- lookup to RLP table for TxHash tag (LookupCondition::RlpHashTag)
- When tag (tx_tag) is one of the following: Nonce, GasPrice, Gas, CalleeAddress, Value, CallDataLength, SigV, SigR, SigS,TxHashLength, TxHashRLC
- Lookup RLP table to validate the value correspond to any of these tags with RlpDataType::TxHash
- lookup to Keccak table for TxSign and TxHash data length and hash result (LookupCondition::Keccak)
- When tag (tx_tag) is TxSignLength or TxHashLength
- Lookup Keccak table to validate the value correspond to TxSign or TxHash data input_rlc, input_length and output_rlc
- lookup to Block table for cum_num_txs
- When tx (tx_tag) is BlockNumber and the row is not padding row
- Lookup Block table to validate the cum_num_txs is for the current block_num
- constraints for tx_id
- tx_id <= cum_num_txs
- tx_id_next - tx_id in u16
- tx_id changes on the final call data byte
- constraints for padding tx
- when CallerAddress=0
- constraints for tx calldata bytes
- is_final is bool
- for any row that is not a final row (is_final = false)
- index::next == index::cur + 1
- tx_id::next == tx_id::cur
- calldata_length::cur == calldata_length::next
- calldata_gas_cost_acc::next == calldata_gas_cost::cur + gas_cost_next
- for the final row (is_final = true)
- calldata_length == index::cur + 1
- tx_id changes
- constraints for is_create
- is_create == 1 iff rlp_tag == To && tag_length == 1
- constraints for ECDSA signature and CallerAddress
- ECDSA signature verified by the sign_verify chip
- CallerAddress recovered from signed tx data using `ecrecover` for secp256k1 (`CallerAddress=keccak(recover_pk(v,r,s,msg_hash))[-20:]`)
<i>Note</i>: At the current time of writing this documentation the tx signagure v part related to ChainID constraints has not been added
<i>Note</i>: Currently only legacy tx supported. EIP2718 rejection not enabled.
### ECDSA sign_verify chip
According to the [EllipticCurveDigitalSignatureAlgorithm] (ECDSA), the signatures `(r,s)` are calculated via ECDSA from `msg_hash` and a `public_key`. In the case of an ethereum tx, the scheme looks as follows
`msg_hash=keccak(RLP(TxSign))`
`(r,s)=ecdsa(msg_hash, public_key)`
where `TxSign` is the tx data that needs to be signed (TxSign is in RLP table), and `RLP(TxSign)` is the RLP encoded bytes of the unsigned tx. The `public_key` can be recovered from `(v,r,s)` and `msg_hash` using `ecrecover`, which further determines the caller address (`caller_address=keccak(public_key)[-20:]`, because this is the way account address is created, which is derived from its public key. Notice that only EOA address can initiate a tx and contract address cannot, because contract address is not calculated from public key but from nonce and EOA address).
[EllipticCurveDigitalSignatureAlgorithm]: https://en.wikipedia.org/wiki/Elliptic_Curve_Digital_Signature_Algorithm
The sign_verify_chip verifies the correctness of the signature `(r,s)` computed from `msg_hash` and `public_key`. It can be viewed as an additional layer between the signature `(r,s)` and `(msg_hash, public_key)` besides `halo2_ecc` circuit.
Moreover, the sign_verify chip also helps to obtain the RLC of tx msg which is RLP(TxSign) and its keccak-256 hash, as well as the RLC of public_key and its keccak-256 hash. This is done by its `sign_data_decomposition` method. Thus the sign_vefify chip returns `AssignedSignVerify` containing
- address: this is given by `keccak(public_key)[-20:]`
- msg_len: length in bytes of `msg=RLP(TxSign)`
- msg_rlc: RLC using `keccak_input` randomness of msg in bytes
- msg_hash_rlc: RLC using `evm_words` randomness of `keccak(msg)` in bytes
- sig_is_valid: bool, whether signature is valid
This piece of `AssignedSignVerify` information will be sent to tx_circuit for further constraints such as checking the keccak hash is done correctly.
It also returns `[is_address_zero, pk_rlc, pk_hash_rlc]` for further Keccak lookups (check where?). <i>Note</i>: This piece of info is not sent to tx_circuit.
Within the sign_verify chip there are many places putting constraints using the halo2_ecc api, such as range checks. This is sometimes done inside the sign_data decomposition process.
## pi_circuit
### Purpose
`PublicData` contains the block header information (block contexts) as well as transactions information. It is structured as follows:
```markmap
# PublicData
## ChainID (Word)
## transactions
- Transaction
- block_number
- id
- hash
- nonce
- gas
- gas_price
- caller_address
- callee_address
- is_create
- value
- call_data
- call_data_length
- call_data_gas_cost
- chain_id
- rlp_unsigned
- rlp_signed
- v
- r
- s
- calls
- steps
- Transaction
- ...
## block_ctxs (BTreeMap)
- Block Context
- coinbase
- gas_limit
- number
- timestamp
- difficulty
- base_fee
- history_hashes
- chain_id
- eth_block
- Block Context
- ...
## prev_state_root (256bit hash)
## withdraw_trie_root (256bit hash)
```
The above `PublicData` is assigned to the pi_circuit byte-by-byte (see pi_circuit layout). The keccak hash result of the following `raw_public_input_bytes` data in sequential order is used to check the correctness of public input data
- previous state root
- current state root
- withdraw trie root (currently set as 0)
- block hash
- parent hash
- block number
- block timestamp
- block base_fee
- num_txs
- num_l1_msgs (currently set as 0)
- `tx_hash` padded by `dummy_tx_hash` (0..max_txs)
Each `tx_hash` is of the form `keccak(rlp(tx_sign))`. The `dummy_tx_hash` corresponds to tx private key = 1.
For chain_id, coinbase, difficulty, they are checked as constants indentities.
### Architechture
See this link for [pi_circuit_layout]
[pi_circuit_layout]: https://docs.google.com/spreadsheets/d/1-ZOqjF3lzCTqhcxP-yp8iMx4wcwOl_tJ6VnAAT0v7as/edit?usp=sharing
constant|rpi|rpi_field_bytes|rpi_field_bytes_acc|rpi_rlc_acc|rpi_length_acc|is_rpi_padding|real_rpi|pi|q_field_start|q_field_step|q_field_end|is_field_rlc|q_start|q_not_end|q_keccak|q_block_tag|cum_num_txs|
|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|
| | | | | | | | | | | | | | | | | | |
- `constant`: for chain_id, coinbase, difficulty in bytes.
- `rpi_field_bytes`: fills `PublicData` in a byte-by-byte manner. After all rpi data field are filled, this column is used to record keccak(rpi) hi/lo in bytes.
- `rpi`: the RLC (using evm_word randomness) or LC (using `BYTE_POW_BASE=256`) of the current section of public input data bytes.
- `rpi_field_bytes_acc`: accumulation of RLC/LC of `rpi_field_bytes`, final row in one rpi section becomes `rpi`
- `rpi_rlc_acc`: cumulative RLC of `rpi_field_bytes` regardless of rpi section using evm word randomness. After all rpi data bytes are finished, this column is then used to record keccak of raw_public_inputs data (`q_keccak=1`).
- `pi`: record keccak_hi and keccak_lo
### Constraints
- constraints for `rpi_bytes_acc`
- correct accumulation of rpi bytes in `rpi_bytes_acc`
- when `is_field_rlc==true`: `rpi_bytes_acc` accumulates `rpi_bytes` in RLC manner using evm word randomness
- when `is_field_rlc==false`: `rpi_bytes_acc` accumulates `rpi_bytes` in LC manner using coefficient `BYTE_POW_BASE=256`
- at row for field start `q_field_start==1`: `rpi_bytes_acc==rpi_bytes`
- at row for field end `q_field_end==1`: `rpi_bytes_acc==rpi`
- at row for intermediate field step `q_field_step==1`: `rpi` keeps the same
- constraints for `rpi_rlc_acc`
- correct accumulation of rpi bytes in `rpi_rlc_acc` when `q_not_end==1`
- When `is_rpi_padding` is false: `rpi_rlc_acc` accumulates `rpi_bytes` in an RLC manner using keccak randomness
- When `is_rpi_padding` is true: `rpi_rlc_acc` keeps the same
- correct incrementation of `rpi_length` when `q_not_end==1`: increase or remain the same base on `is_rpi_padding` false or true
- at the start row `q_start==1`: `rpi_rlc_acc` initialized from the initial `rpi_bytes`
- constraints for `real_rpi` when `q_not_end==1`
- `is_rpi_padding` is boolean
- when `is_rpi_padding==0`, then `real_rpi` equals `rpi`
- when `is_rpi_padding==0`, then `real_rpi` equals 0
- lookup to keccak table for `keccak(rpi)` when `q_keccak==1`
- lookup item `q_keccak * (1, rpi, rpi_length_acc, rpi_rlc_acc)` into keccak table for `(is_enabled, input_rlc, input_length, output_rlc)`
- constraints for `cum_num_txs`
- for the first row, `cum_num_txs` is 0
- increase `cum_num_txs` at the next row by `num_txs` in the block, which is fetched from block table
## copy_circuit
### Purpose
copy_circuit aims at constraining the read-write steps for copied bytes when executing such opcodes as CALLDATACOPY, CODECOPY and LOGs. An evm `CopyEvent` is defined as follows
- CopyEvent
- `src_addr` (u64): the start address at the source of the copy event
- `src_addr_end` (u64): the end address at the source of the copy event
- `src_type`: CopyDataType, including Padding (for copy circuit padding rows, <i>this is different from copy step padding rows</i>), Bytecode (as copy source), Memory (as copy source/destination), TxCallData (as copy source), TxLog (as copy destination), RlcAcc (RLC acccumulation of some rows in copy circuit, used for SHA3 op lookup verification)
- `src_id`: NumberOrHash, the relevant ID for source, usize number value or 256-bit hash value
- `dst_addr`: u64, the start address at the destination of the copy event
- `dst_type`: CopyDataType, the destination type
- `dst_id`: NumberOrHash, the relevant ID for destination
- `log_id`: `Option<u64>`, the log ID in case of the destination being TxLog
- `rw_counter_start`: RWCounter, rw counter at start of this copy event
- `bytes`: `Vec<(u8, bool)>`, the list of (bytes, is_code) copied during this copy event. Here `is_code = push_data_left == 0` is the same definition as in bytecode circuit
When a copy event happens, witnesses are filled into the `CopyTable` which consists of the following columns
- Copytable
|is_first|id|addr|src_addr_end|bytes_left|rlc_acc|rw_counter|rwc_inc_left|tag|
|-|-|-|-|-|-|-|-|-|
|the first read-write pair for a copy event|Call ID/Caller ID for CopyDataType::Memory|source/destination address for this copy step. Can be memory address, byte index in the bytecode, tx call data, and tx log data|end of the source buffer for the copy event. Any data read from an address greater than or equal to this value will be 0|number of bytes left to be copied|accumulator for RLC value, used for example for tag == CopyDataType::RlcAcc|rw_counter|reversed rw_counter|tag for Bytecode, Memory, TxCalldata, TxLog, RlcAcc or Padding|
||RLC encoding of bytecode hash for CopyDataType::Bytecode||||||||
||Transaction ID for CopyDataType::TxCalldata, CopyDataType::TxLog||||||||
The behavior of these witnesses will be constrained inside copy_circuit.
### Architecture
|q_step|is_last|value|is_code|is_pad|q_enable|copy_table columns (9 columns)|
|-|-|-|-|-|-|-|
|||value of this read-write copy or RlcAcc||this is 1 if the current row is padding <i>for the current copy event step</i>, i.e., when `src_addr >= src_addr_end`|||
In the above, the copy_table columns are columns taken directly from the copy_table (9 columns, including `is_first`, `id`, `addr`, `src_addr_end`, `bytes_left`, `rlc_acc`, `rw_counter`, `rwc_inc_left`, `tag`).
When a `CopyEvent` happens, witnesses are generated from it and assigned to both the `CopyTable` and the above circuit columns. Assignments of witnesses are in the form of read-write pairs, where each read-write pair occupies two rows, with the order of read row first and then followed by the write row.
The copy circuit is able to hold witnesses for may copy events, and each one might have its own padding rows (`is_pad==1`) when `src_addr >= src_addr_end`. At the end of all copy events, the copy circuit adds padding rows (`tag=CopyDataType::Padding`) until the number of rows is equal `max_copy_rows`. So in particular, for rows where `tag=CopyDataType::Padding` we assign `is_pad=0`.
<i>Note</i>: The column `q_step` is the same as `is_read==1-is_write` where `is_write` is in the rw table. A little bit redundency to create another term `q_step`.
### Constraints
- constraints for each copy_circuit row where `q_enable==1`
- `is_first`, `is_last` are boolean
- when `q_step==1`, `is_last==0`, and when `q_step==0`, `is_first==0`
- if not last two rows (`1-is_last (current row)-is_last (next row)==0`) and `tag!=CopyDataType::Padding`, then read-write pair in consecutive rows
- `id`, `tag`, `src_addr_end` remain the same between current row and current row + 2
- `addr` increase by 1 from the current row to current row + 2
- if not last row (`is_last==0`)
- `rw_counter` increase by 1 (`rwc_inc_left` decrease by 1) from current row to next row if `tag==CopyDataType::Memory` or `tag==CopyDataType::TxLog` and `is_pad==0` for the current row; otherwise they remain the same
- `rlc_acc` remains the same between current row and next row
- if last row (`is_last==1`)
- `rwc_inc_left` is 1 if `tag==CopyDataType::Memory` or `tag==CopyDataType::TxLog` and `is_pad==0` for the current row; otherwise it is 0
- when `tag` is `CopyDataType::RlcAcc`, then `value==rlc_acc`
- constraints for rows where `q_step==1` (which means current row is read and next row is write)
- if `is_last==1` for the next row, then for the current row `bytes_left==1`
- if `is_last==0` for the next row, and `tag!= CopyDataType::Padding` for the current row, then `bytes_left` descrese by 1 from current row to current row + 2 (which corresponds to `bytes_left_next`)
- if `tag!=CopyDataType::RlcAcc` for the next row, or if `is_first==1` for the current row, then current row `value` is the same as next row `value`
- if `is_pad==1` for the current row, then `value==0`
- `is_pad==1 - (src_addr < src_addr_end)` for the current row
- `is_pad==0` for the next row
- constraints for rows where `q_step==0`
- if `q_enable==1`, `is_last==1`, `is_pad==0` and `tag==CopyDataType::RlcAcc`, then `current_row_value * keccak_randomness + next_row_value==current+2_row_value`
- lookup into rw_table
- memory lookup: in case `q_enable==1` and `tag==CopyDataType::Memory` and `is_pad==0`, lookup into rw table for `(rw_counter, 1-q_step, RwTableTag::Memory, id, addr, 0, 0, value, 0, 0, 0)`
- tx_log lookup: in case `q_enable==1` and `tag==CopyDataType::TxLog`, lookup into rw table for `(rw_counter, 1-q_step, RwTableTag::TxLog, id, addr, 0, 0, value, 0, 0, 0)`
- lookup into bytecode_table
- in case `q_enable==1` and `tag==CopyDataType::Bytecode` and `is_pad==0`, lookup into rw table for `(id, BytecodeFieldTag::Byte, addr, is_code, value)`
- lookup into tx_table
- in case `q_enable==1` and `tag==CopyDataType::TxCalldata` and `is_pad==0`, lookup into rw table for `(id, TxContextFieldTag::CallData, addr, value)`
## bus-mapping
### Purpose
Bus mapping serves as an intermediate layer that turns geth instance data fetched by its RPC client into data that are needed for zkevm-circuits (such as witness data). In this way, zkevm-circuits can focus on building constraint system based on and only on those data provided by bus mapping.
### Design and Architecture
The smallest granuity for bus-mapping to collect circuit input data is at the level of eth transaction. It maps tx data into `Exec_Step` including begin_tx step, all intermediate execution steps and end_tx step. These exec steps are expressed via `operation` (such as stack, memory and storage operations) which is the best language that is understandable by the circuit. The mapping process is done via `gen_begin_tx_ops` (for begin_tx), `gen_associate_ops` (for intermediate exec steps) and `gen_end_tx_ops` (for end_tx). The high-level architecture looks as follows
```mermaid
stateDiagram
GethClient --> BuilderClient
chain_id --> BuilderClient
CircuitsParams --> BuilderClient
BuilderClient --> stateDB
BuilderClient --> codeDB
BuilderClient --> Block
BuilderClient --> BlockContext
stateDB --> circuit_input_builder
codeDB --> circuit_input_builder
Block --> circuit_input_builder
BlockContext --> circuit_input_builder
circuit_input_builder --> begin_tx_step
circuit_input_builder --> exec_steps
circuit_input_builder --> end_tx_step
begin_tx_step --> block.txs
exec_steps --> block.txs
end_tx_step --> block.txs
```
When Geth instance data is fetched in the form of `GethExecStep`, they will be transformed into the form of `CircuitInputStateRef` and fed into `circuit_input_builder` to be turned to `ExecStep` that is further provided to zkevm-circuits. `GethExecStep`, `CircuitInputStateRef` and `ExecStep` have the following structure
```markmap
# GethExecStep
- pc (ProgramCounter)
- op (OpcodeId)
- gas (Gas)
- gas_cost (GasCost)
- refund
- depth (u16)
- error
- stack
- memory
- storage
```
```markmap
# CircuitInputStateRef
## sdb (StateDB)
- state
- access_list_account
- access_list_account_storage
- dirty_storage
- destructed_account
- refund
## code_db (codeDB)
- HashMap(Hash, Vec(u8))
## block (Block)
- headers (u64 -> BlockHead as BTreeMap)
- BlockHead
- chain_id
- history_hashes
- coinbase
- gas_limit
- number
- timestamp
- difficulty
- base_fee
- eth_block (which is original block from geth)
- BlockHead
- ...
- prev_state_root
- withdraw_root
- prev_withdraw_root
- OperationContainer
- txs
- Transaction
- Transaction
- ...
- CopyEvents
- CopyEvent
- CopyEvent
- ...
- code (Hash -> Vec(u8) as HashMap)
- sha3_inputs
- BlockSteps
- end_block_not_last: ExecStep
- end_block_last: ExecStep
- exp_events
- ExpEvent
- ExpEvent
- ...
- CircuitsParameters
- chain_id
## block_ctx (BlockContext)
- rw_counter
- call_map: call_id -> (tx_index, call_index)
- cumulative_gas_used
## tx (Transaction)
- block_num
- nonce: u64
- hash: H256
- gas: u64
- gas_price: Word
- from: caller address
- to: callee address
- value: Word
- input: Vec of u8
- chain_id: u64
- signature: Signature
- l1_fee: Current values of L1 fee
- pub l1_fee_committed: Committed values of L1 fee
- calls: Calls made in the transaction
- steps: Vec of ExecStep
## tx_ctx (TransactionContext)
- l1_fee
- tx_id
- log_id
- is_last_tx
- calls
- CallContext
- CallContext
- ...
- call_is_success
- reversion_groups
- ReversionGroup
- ReversionGroup
- ...
```
```markmap
# ExecStep
- exec_state
- Opcode
- BeginTx
- EndTx
- EndBlock
- pc (ProgramCounter)
- stack_size
- memory_size
- gas_left
- gas_cost
- gas_refund
- call_index
- rwc (RWCounter)
- reversible_write_index
- reversible_write_counter_delta
- log_id
- bus_mapping_instance
- OperationRef
- Start
- Memory
- call_id
- address
- value
- Stack
- call_id
- address
- value
- Storage
- address
- key
- value
- value_prev
- tx_id
- committed_value
- TxAccessListAccount
- TxAccessListAccountStorage
- TxRefund
- Account
- CallContext
- TxReceipt
- TxLog
- OperationRef
- ...
- copy_rw_counter_delta
- error
```
### Example
As an example, assume an eth transaction results in a geth execution trace that contains the [SHA3 opcode](https://www.evm.codes/#20?fork=shanghai). Let us carefully analyze how bus mapping produces circuit witness data for the SHA3 opcode as a `GethExecStep`. This is done in the function `Sha3::gen_associated_ops`.
The function `gen_associated_ops` for SHA3 opcode takes two inputs:
(1) `state`, which is of type `&mut CircuitInputStateRef`;
(2) `geth_steps`, which is a slice of `GethExecStep` where first element is opcode input and second element is opcode output.
Inside `gen_associated_ops`, we fetch the `offset` and `size` from `geth_steps[0].stack` and give them to `state` by doing stack read of `offset` and `size`. In case `size>0`, we extend the `state`'s memory part by `offset+size` and read memory from `offset` to `offset+size` to get Keccak256 input. We then write the Keccak256 hash of its input back to `state`'s stack. Up to here, we are just doing an identical behavior as the original SHA3 opcode but we mirror map it onto the `CircuitInputStateRef` side which will finally be handled to circuit.
The additional information obtained by bus mapping is done here via parsing
(1) memory read operations, i.e. memory read from `offset` to `offset+size` in a byte-by-byte manner, and record rw counter accordingly;
(2) call_id;
(3) copy event, i.e., copy from memory to `RlcAcc` of the bytes in memory read. (<i>Note: This should be needed by copy circuit.</i>)
Finally, the returned `exec_step` by `gen_associate_ops` of SHA3 opcode is obtained along with `state` updates described above.
## aggregation circuit
### Purpose
The zkevm-supercircuit is able to provide SNARK proofs for all the transations within a <i>chunk</i> of L2 blocks (see [this comment](https://github.com/scroll-tech/zkevm-circuits/blob/94b76371dffba65ce1db7708cf7c30ac571f2687/bus-mapping/src/circuit_input_builder.rs#L165) for L2 block). We aggregate transaction data across many chunks into a <i>batch</i>. The aggregation circuit aims at proving at once the correctness of all transactions within a batch. This is done by "accumulating" SNARK proofs for different chunk data as well as "gluing" public inputs that are used in the SNARKs with public input aggregation scheme.
### Architecture
#### Chunk and Batch public input data structure
Chunk data that will be collected into `ChunkHash` has the following structure
```markmap
# chunk_pi_hash (256 bit hash)
## Keccak256
### ChunkHash
#### chain_id (u64, in be bytes)
#### prev_state_root (256-bit hash)
#### post_state_root (256-bit hash)
#### withdraw_root (256-bit hash)
#### data_hash (256-bit hash of chunk data)
```
The above-listed data fields will be concatenated in the shown order and mapped through Keccak256 into this chunk's public input hash `chunk_pi_hash`.
Batch data is a concatenation of a sequence of chunk data. Batch data that will be collected into `BatchHash` has the following structure
```markmap
# BatchHash
## chain_id (u64)
## chunks
### chunk_0
### chunk_1
### ...
### chunk_k-1
## data_hash (256 bit hash)
### keccak256
#### chunk_0.data_hash
#### chunk_1.data_hash
#### ...
#### chunk_k-1.data_hash
## public_input_hash (256 bit hash)
### keccak256
#### chain_id
#### chunk_0_prev_state_root
#### chunk_k-1_post_state_root
#### chunk_k-1_withdraw_root
#### data_hash (of the Batch)
```
#### SNARK data structure
When zkevm-superciruit does proof on a chunk data, a SNARK proof is produced that consists of 2 elliptic-curve group points (EC G1 points, since we use Halo2 as backend proving system), which are the left and right inputs to the pairing. Each EC G1 point is a pair of $\mathbb{F}_q$ (base field) elements $(x,y)$, so in total 4 $\mathbb{F}_q$ elements. We decompose each $\mathbb{F}_q$ points into $3$ limbs and encode each limb with an $\mathbb{F}_r$ (scalar field) element. So in total we use 12 $\mathbb{F}_r$ elements to encode one SNARK proof.
#### Compression Circuit
Proof compression circuit takes in a SNARK proof (12 field elements) as input, as well as the same public inputs from input SNARK proof. The output is an accumulated SNARK proof (presumably with a smaller proof size) via `KzgAs` accumulation scheme, as well as the same public inputs from input SNARK proof. The scheme looks as
`(old_accoumulator, public_inputs) -> (new_accumulator, same public_inputs)
`
Compression circuit is applied
(1) at chunk proof: twice to each chunk's SNARK proof with different configurations (1 wide and 1 thin). In the chunk case public_input is taken as chunk's public input, and it consists of 72 field elements.
(2) at batch proof: to the proof produced by aggregation circuit. In the batch case public_input is taken as batch's public input hash it consists of 32 field elements.
`KzgAs` is an accumulation scheme with a circuit to produce an accumulation proof. If there are $k$ proofs to be accumulated, roughly speaking, `KzgAs` produces EC points as
$\text{acc_ec_pt} = \text{ec_pt}_0 + \text{ec_pt}_1 * r + ... + \text{ec_pt}_k * r^{k-1} \ ,$
where $r$ is a challenge squeezed from the proof. This is applied to the EC points on both sides of the pairng. In the compression circuit, we only take $1$ proof to accumulate, while in the aggregation circuit we take multiple proofs to accumulate.
#### Aggregation Circuit
After 2-layers of proof compression, we obtain a family of $k$ SNARKs in a batch, each one with
(1) 12 field elements as accumulator;
(2) 72 field elements as chunk public input instances.
We use aggregation circuit to accumulate all above SNARK proofs into one snark proof with an aggregated `public_input_hash` for the batch. This consists of two steps
(1) accumulate the SNARK proofs. Each SNARK proof is given by 2 EC G1 points (left and right of pairing). This applies `KzgAs` to all $k$ SNARK proofs;
(2) accumulate the public inputs for each SNARK in the chunk. This applied public input aggregation scheme, where the final aggregated public input is given by `batch_public_input_hash=keccak256(chain_id||chunk_0_prev_state_root||chunk_k-1_post_state_root|| chunk_k-1_withdraw_root|| batch_data_hash)`. Since this ignores all intermediate chunk's prev and post state root, and the data hash is given by the hash of all chunk's data hash (`batch_data_hash := keccak(chunk_0.data_hash || ... || chunk_k-1.data_hash)`, we need to impose constraints to connect these public inputs. These connection type constraints can be found in the <b>Constraints-Constraints for public input aggregation</b> session.
#### Overall Workflow
### Constraints
#### Constraints for proof compression and SNARK aggregation
These constraints are outsourced to `KzgAs` etc.
#### Constraints for public input aggregation
- all hashes are computed correctly
- the relations between hash preimages and digests are satisfied
- `batch_data_hash` digest is reused for batch's aggregated `public_input_hash`
- batch's aggregated `public_input_hash` used same roots as `chunk_pi_hash`
- same `data_hash` is used to compute `batch_data_hash` and `chunk_pi_hash` for all chunks
- chunks are continuous: they are linked via the state roots
- all hashes uses a same chain_id
- the batch_pi_hash matches the circuit's public input (32 field elements) above
Sign in with Wallet
Connect another wallet