You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Apr 18, 2025. It is now read-only.
This is done via comparing the `data_rlc` of `chunk_{i-1}` and ` chunk_{i}`.
122
-
7. the hash input length are correct
122
+
7. the hash input length is correct
123
123
- first MAX_AGG_SNARKS + 1 hashes all have 136 bytes input
124
124
- batch's data_hash length is 32 * number_of_valid_snarks
125
125
8. batch data hash is correct w.r.t. its RLCs
@@ -131,7 +131,7 @@ This is done via comparing the `data_rlc` of `chunk_{i-1}` and ` chunk_{i}`.
131
131

132
132
133
133
134
-
Our keccak table uses $2^{19}$ rows. Each keccak round takes `300` rows. When the number of round is is less than $2^{19}/300$, the cell manager will fill in the rest of the rows with dummy hashes.
134
+
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.
135
135
136
136
The only hash that uses dynamic number of rounds is the last hash.
137
137
Suppose we target for `MAX_AGG_SNARK = 10`. Then, the last hash function will take no more than `32 * 10 /136 = 3` rounds.
@@ -154,4 +154,4 @@ For the output of the final data hash
154
154
|9,10 | 64 | 0, 0, 1|
155
155
156
156
Additional checks for dummy chunk
157
-
- if `is_padding` for `i`-th chunk, we constrain `chunk[i]'s chunk_pi_hash_rlc_cells == chunk[i-1].chunk_pi_hash_rlc_cells`
157
+
- if `is_padding` for `i`-th chunk, we constrain `chunk[i]'s chunk_pi_hash_rlc_cells == chunk[i-1].chunk_pi_hash_rlc_cells`
Copy file name to clipboardExpand all lines: docs/Bytecode_Circuit.md
+2-2Lines changed: 2 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -15,7 +15,7 @@ The EVM Circuit needs to lookup to the bytecode table that stores the correct by
15
15
|RLC of hash's little-endian bytes using evm_word randomness|BytecodeFieldTag::Header|0|0|len of bytes|
16
16
|RLC of hash's little-endian bytes using evm_word randomness|BytecodeFieldTag::Byte|idx|true when the byte is not an argument to a PUSHx instruction|byte|
17
17
18
-
Here `Header` is used to seperate bytecodes.
18
+
Here `Header` is used to separate bytecodes.
19
19
20
20
## Purpose of the Bytecode Circuit
21
21
@@ -98,5 +98,5 @@ Here
98
98
- when `tag` is `byte`, then lookup to push_table for `(value, push_data_size)`
99
99
100
100
- correct propagation of each row within one bytecode
101
-
- when `tag` transits from `byte` to `byte`, then `length` and `hash` remain the same, `index`increse by 1, `value_rlc` accumulates, and for push data `push_data_left` decay by 1, for code `push_data_left` remains the same as `push_data_size`
101
+
- when `tag` transits from `byte` to `byte`, then `length` and `hash` remain the same, `index`increases by 1, `value_rlc` accumulates, and for push data `push_data_left` decay by 1, for code `push_data_left` remains the same as `push_data_size`
Copy file name to clipboardExpand all lines: docs/EVM_Circuit.md
+2-2Lines changed: 2 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -29,7 +29,7 @@ Analogously, in EVM Circuit, we build <i>execution steps</i> according to the st
29
29
30
30
## Architecture
31
31
32
-
We decompose the execution trace into execution steps and impose constraints for each step/step state transition. A `Step` contains two parts: `StepState` carries the execution step and its context information; and `CellManager` helps to fill the step's information as witnesses into the circuit's cells. An API layer `ConstraintBuilder` is built upon the backend proof system (Halo2) to impose constraints. The oveall architecture looks as follows:
32
+
We decompose the execution trace into execution steps and impose constraints for each step/step state transition. A `Step` contains two parts: `StepState` carries the execution step and its context information; and `CellManager` helps to fill the step's information as witnesses into the circuit's cells. An API layer `ConstraintBuilder` is built upon the backend proof system (Halo2) to impose constraints. The overall architecture looks as follows:
33
33
34
34
```mermaid
35
35
stateDiagram
@@ -362,4 +362,4 @@ For RETURNDATACOPY opcode, EVM Circuit does the following type of constraint che
362
362
-`SameContextGadget`
363
363
- opcodeID checks: opId $==$ OpcodeId(0x3e);
364
364
- state transition: rw_counter+, stack\_pointer+3, pc+1, gas -(op_cost+memory expansion cost), memory expand to next memory word size.
Copy file name to clipboardExpand all lines: docs/Keccak_Circuit.md
+3-3Lines changed: 3 additions & 3 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -65,7 +65,7 @@ Cyclic shift offset constants $r[x,y]$ are picked according to the following tab
65
65
| $y=4$ | 56 | 14 | 18 | 2 | 61 |
66
66
| $y=3$ | 21 | 8 | 41 | 45 | 15 |
67
67
68
-
Round constants $RC[k]$ are also given, in hexiadecimal notion it looks like:
68
+
Round constants $RC[k]$ are also given, in hexadecimal notion it looks like:
69
69
70
70
$$\begin{array}{ll}
71
71
RC[ 0] & \verb"0x0000000000000001"
@@ -226,7 +226,7 @@ The parts splitted from the word is then determined bit-by-bit from `target_size
226
226
-`uniform` is true, then the remaining `rot`-sized bits [63-`rot`+1,...,63] are divided by `part_size` plus a remainder, and first 64-`rot` bits are determined by a section compensating previous remainder, plus divide by `part_size`, and plus the remainder from `target_size` division;
227
227
-`uniform` is false, then the remaining `rot`-sized bits [63-`rot`+1,...,63] are divided by `part_size` plus remainder, and first 64-`rot` bits determined by `part_size` plus a remainder.
228
228
229
-
The way we do the above split when `uniform` is true enables an optimization shown below, where after rotation the front and tail remainders combined together becomes an inverval of length `part_size`:
229
+
The way we do the above split when `uniform` is true enables an optimization shown below, where after rotation the front and tail remainders combined together becomes an interval of length `part_size`:
@@ -350,7 +350,7 @@ $$os[i][j]=s[i][j]+bc[(i+4)\mod 5]+\text{rot}(bc[(i+1)\mod 5], 1) $$ and set it
350
350
351
351
#### Rationale
352
352
- <i>Soundness</i>: Use the symbols in the previous section on Keccak-f permutation function, it can be checked that $C[x]$ is the same as the parity of $A[x,0]+A[x,1]+...+A[x,4]$. So this is what $bc[i]$ checks at the `normalize_6` table lookup step.
353
-
In a same rationale, $os[i][j]$ after normalization stands for the parity of $A[x,y]\oplus D[x]$. This normalization is postponed to $\rho/\pi$-step using `normalize_4` table lookup.
353
+
In the same rationale, $os[i][j]$ after normalization stands for the parity of $A[x,y]\oplus D[x]$. This normalization is postponed to $\rho/\pi$-step using `normalize_4` table lookup.
354
354
- <i>Completeness</i>: Since $C[x]$ is the same as the parity of $A[x,0]+A[x,1]+...+A[x,4]$, any selection of witnesses that satisfy original $\theta$-step in the Section on Keccak-f permutation function will pass the constraints.
0 commit comments