Skip to content

Commit

Permalink
Fix typos (scroll-tech#1052)
Browse files Browse the repository at this point in the history
* fix typos README.md

* fix minor typos Bytecode_Circuit.md

* fix typos EVM_Circuit.md

* fix typos Keccak_Circuit.md

* fix typos MPT_Circuit.md

* fix typos Modexp_Circuit.md

* fix typos Public_Input_Circuit.md

* fix typos Sig_Circuit.md

* fix typos State_Circuit.md

* fix typos Tx_Circuit.md
  • Loading branch information
nnsW3 authored Dec 11, 2023
1 parent fb271ea commit 6a70be0
Show file tree
Hide file tree
Showing 10 changed files with 83 additions and 83 deletions.
12 changes: 6 additions & 6 deletions aggregator/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -133,19 +133,19 @@ This is done via comparing the `data_rlc` of `chunk_{i-1}` and ` chunk_{i}`.

Our keccak table uses $2^{19}$ rows. Each keccak round takes `300` rows. When the number of round is less than $2^{19}/300$, the cell manager will fill in the rest of the rows with dummy hashes.

The only hash that uses dynamic number of rounds is the last hash.
The only hash that uses a dynamic number of rounds is the last hash.
Suppose we target for `MAX_AGG_SNARK = 10`. Then, the last hash function will take no more than `32 * 10 /136 = 3` rounds.

We also know in the circuit if a chunk is an empty one or not. This is given by a flag `is_padding`.

For the input of the final data hash
- we extract `32 * MAX_AGG_SNARK` number of cells (__static__ here) from the last hash. We then compute the RLC of those `32 * MAX_AGG_SNARK` when the corresponding `is_padding` is not set. We constrain this RLC matches the `data_rlc` from the keccak table.
- we extract `32 * MAX_AGG_SNARK` number of cells (__static__ here) from the last hash. We then compute the RLC of those `32 * MAX_AGG_SNARK` when the corresponding `is_padding` is not set. We constrain this RLC match the `data_rlc` from the keccak table.

For the output of the final data hash
- we extract all three hash digest cells from last 3 rounds. We then constraint that the actual data hash matches one of the three hash digest cells with proper flags defined as follows.
- if the num_of_valid_snarks <= 4, which only needs 1 keccak-f round. Therefore the batch's data hash (input, len, data_rlc, output_rlc) are in the first 300 keccak rows;
- else if the num_of_valid_snarks <= 8, which needs 2 keccak-f rounds. Therefore the batch's data hash (input, len, data_rlc, output_rlc) are in the 2nd 300 keccak rows;
- else the num_of_valid_snarks <= 12, which needs 3 keccak-f rounds. Therefore the batch's data hash (input, len, data_rlc, output_rlc) are in the 3rd 300 keccak rows;
- we extract all three hash digest cells from the last 3 rounds. We then constraint that the actual data hash matches one of the three hash digest cells with proper flags defined as follows.
- if the num_of_valid_snarks <= 4, which only needs 1 keccak-f round. Therefore the batch's data hash (input, len, data_rlc, output_rlc) is in the first 300 keccak rows;
- else if the num_of_valid_snarks <= 8, which needs 2 keccak-f rounds. Therefore the batch's data hash (input, len, data_rlc, output_rlc) is in the 2nd 300 keccak rows;
- else the num_of_valid_snarks <= 12, which needs 3 keccak-f rounds. Therefore the batch's data hash (input, len, data_rlc, output_rlc) is in the 3rd 300 keccak rows;

|#valid snarks | offset of data hash | flags|
|---| ---| ---|
Expand Down
2 changes: 1 addition & 1 deletion docs/Bytecode_Circuit.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ The bytecode circuit aims at constraining the correctness of the above bytecode

## Architecture and Design

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 architecture looks like
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 constrain its rows via `BytecodeCircuit`, so the architecture looks like

```mermaid
stateDiagram
Expand Down
16 changes: 8 additions & 8 deletions docs/EVM_Circuit.md
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ The backend proof system is based on Halo2, so all constraints are implemented a

#### CellTypes

`Challenge` API is a feature of Halo2 that can produce SNARK's random challenges based on different phases of the proof in the transcript. In alignment with the `Challenge` API, EVM Circuit classifies its cells based on different phases of the proof. This results in `CellType`, which currently contains `StoragePhase1`, `StoragePhase2`, `StoragePermutation` and `Lookup` for different types of lookup tables, etc. . A given column in EVM Circuit will consist of cells with the same `CellType`. Columns under a given `CellType` will be horizontally layouted in a consecutive way to occupy a region. Cells that are of the same `CellType` will be subject to the same random challenge produced by `Challenge` API when Random Linear Combination (RLC) is applied to them.
`Challenge` API is a feature of Halo2 that can produce SNARK's random challenges based on different phases of the proof in the transcript. In alignment with the `Challenge` API, EVM Circuit classifies its cells based on different phases of the proof. This results in `CellType`, which currently contains `StoragePhase1`, `StoragePhase2`, `StoragePermutation` and `Lookup` for different types of lookup tables, etc. . A given column in EVM Circuit will consist of cells with the same `CellType`. Columns under a given `CellType` will be horizontally layouted in a consecutive way to occupy a region. Cells that are of the same `CellType` will be subject to the same random challenge produced by `Challenge` API when a Random Linear Combination (RLC) is applied to them.

#### Behavior of CellManager within columns of the same CellType

Expand Down Expand Up @@ -153,12 +153,12 @@ Then we enable an advice column:
A few extra columns are enabled for various purposes, including:

- `constants`, a fixed column, 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_until_next_step`, an advice column, count the number of rows until the next step
- `num_rows_inv`, an advice column, for a constraint that enforces `q_step:= num_rows_until_next_step == 0`

In alignment with the `Challenge` API of Halo2, we classify all above columns as in phase 1 columns using Halo2's phase convention.
In alignment with the `Challenge` API of Halo2, we classify all the above columns as in phase 1 columns using Halo2's phase convention.

After that, a rectangular region of advice columns is 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`. The step height is not fixed, so it is dynamic. This part is handled by `CellManager`.
After that, a rectangular region of advice columns is arranged for the execution step specific constraints that correspond to an `ExecutionGadget`. The width of this region is set to be a constant `STEP_WIDTH`. 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 a given height and the number of advice columns as its width. The allocation process is in alignment with `Challenge` API. So within the area allocated to advice columns, `CellManager` marks columns in consecutive regions from left to right as

Expand Down Expand Up @@ -245,7 +245,7 @@ For the EVM Circuit, there are internal and external lookup tables. We summarize

#### Lookup into the table

We use `Lookup::input_exprs` method to extract input expressions from an 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 lookup argument aims at proving the former expression lies in the latter ones. This is done by first RLC (Random Linear Combine) both sides of expressions using the same random challenge and then lookup the RLC expression. Here each column of a lookup table corresponds to one lookup expression, and EVM Step's lookup input expressions must correspond to the table expressions. See the following illustration:
We use `Lookup::input_exprs` method to extract input expressions from an 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 lookup argument aims to prove that the former expression lies in the latter ones. This is done by first RLC (Random Linear Combine) on both sides of expressions using the same random challenge and then lookup the RLC expression. Here each column of a lookup table corresponds to one lookup expression, and EVM Step's lookup input expressions must correspond to the table expressions. See the following illustration:

![evm-circuit-lookup](https://hackmd.io/_uploads/rynmiTWF2.png)

Expand All @@ -255,7 +255,7 @@ At the execution level, the input expression RLCs enter EVM Circuit's lookup cel

At each step, `CellManager` allocates a region with columns consisting of `CellType::Lookup(table)` that are for various types of lookups. Cells in these columns are filled with the RLC result of input expressions induced by the execution trace. This is done by the `add_lookup` method in `ConstraintBuilder`.

The number of columns allocated for one type of lookup (corresponding lookup will be into a particular lookup table) follows the configuration setting in `LOOKUP_CONFIG`. These numbers are tunable in order to make the circuit more "compact", i.e., with less unused cells, so that performance can be improved.
The number of columns allocated for one type of lookup (the corresponding lookup will be into a particular lookup table) follows the configuration setting in `LOOKUP_CONFIG`. These numbers are tunable in order to make the circuit more "compact", i.e., with less unused cells, so that performance can be improved.

#### Challenge used for EVM Circuit's lookup cells

Expand All @@ -269,7 +269,7 @@ Due to page limit we only discuss some examples here.

#### `SameContextGadget`

This gadget is applied to every execution step in order to check the correct transition from current state to next state. The constraints include
This gadget is applied to every execution step in order to check the correct transition from the current state to the next state. The constraints include
- lookup to Bytecode Table and Fixed Table (with `tag=FixedTableTag::ResponsibleOpcode`) for the correctness of the current opcode;
- check remaining gas is sufficient;
- check correct step state transition, such as change of `rw_counter`, `program_counter`, `stack_pointer` etc.
Expand Down Expand Up @@ -354,7 +354,7 @@ Note that the data to be copied to memory that exceeds return data size ($||\mu_

For RETURNDATACOPY opcode, EVM Circuit does the following type of constraint checks together with witness assignments:

- Constraints for stack pop of `dest_offset`, `data_offset` and `size`. This means they are assigned from the step's rw data (via bus mapping) and then they are checked by doing RwTable lookups with `tag=RwTableTag::Stack`, as well as verifying correct stack pointer update;
- Constraints for stack pop of `dest_offset`, `data_offset` and `size`. This means they are assigned from the step's rw data (via bus mapping) and then they are checked by doing RwTable lookups with `tag=RwTableTag::Stack`, as well as verifying the correct stack pointer update;
- Constraints for call context related data including `last_callee_id`, `return_data_offset` (offset for $\mu_{o}$) and `return_data_size` ($\|\mu_o\|$). These are assigned and then checked by RwTable lookups with `tag=RwTableTag::CallContext`. Here return data means the output data from last call, from which we fetch data that is to be copied into memory;
- Constraints for ensuring no out-of-bound errors happen with `return_data_size`;
- Constraints for memory related behavior. This includes memory address and expansion via `dest_offset` and `size`, as well as gas cost for memory expansion;
Expand Down
Loading

0 comments on commit 6a70be0

Please sign in to comment.