... | ... | @@ -35,7 +35,7 @@ pub struct CoreCircuitConfig<F: Field, const NUM_STATE_HI_COL: usize, const NUM_ |
|
|
- opcode:当前程序计数器指向的指令
|
|
|
- cnt:为了在执行一步占用多行的情况下设计的,在执行状态这一章会详细讲解。
|
|
|
|
|
|
在EVM执行轨迹的电路设计中,每一行代表程序的一个执行步骤,程序状态变量(如pc)在每一行都有相应的变化,并且这些变化需要通过逻辑门约束来确保其符合预期的行为。具体例子中,如果pc在当前行增加2,那么在witness表中pc列的下一行的值也要增加2,并且电路中需要一个约束来确保pc的增量为2。
|
|
|
在EVM执行轨迹的电路设计中,程序状态变量(如pc)随着执行步骤会有相应的变化,并且这些变化需要通过逻辑门约束来确保其符合预期的行为。例如,如果pc在当前行增加2,那么在witness表中pc列的下一行的值也要增加2,并且电路中需要一个约束来确保pc的增量为2。
|
|
|
|
|
|
## 2 多功能列 Versatile columns
|
|
|
为了减少列的使用,缩减电路规模,我们设计了多功能的列。在不同的执行状态、不同的指令下,这些列起到不同的作用。除了上述单功能的列以外,其他我们需要的状态、变量等等,都使用多功能的列,可以达到重复利用列的效果。
|
... | ... | @@ -58,7 +58,7 @@ pub struct CoreCircuitConfig<F: Field, const NUM_STATE_HI_COL: usize, const NUM_ |
|
|
|
|
|
### 3.1 概念
|
|
|
|
|
|
执行状态是core子电路中每一步骤的种类,用以区分不同步骤的不同操作。EVM中的步骤的种类是指令(或opcode),而电路中的步骤的种类是执行状态。指令与执行状态*基本*成一一对应关系。有些相似指令,可以用同一种执行状态概括这些指令的操作。有些指令操作过于复杂,需要用连续的多个执行步骤进行处理。执行步骤的设计理念是使得代码尽量简单。
|
|
|
执行状态是core子电路中每一步骤的种类,用以区分不同步骤的不同操作。EVM中的步骤的种类是指令(或opcode),而电路中的步骤的种类是执行状态。指令与执行状态*基本*成一一对应关系。有些相似指令,可以用同一种执行状态概括这些指令的操作。有些指令操作过于复杂,需要用连续的多个执行步骤进行处理。执行步骤的设计理念是使得代码尽量简单。一个执行状态会使用连续多行的列。
|
|
|
|
|
|
在代码里,使用enum来标识执行状态。执行状态的种类分为以下几种:
|
|
|
#### 3.1.1 指令可对应的状态
|
... | ... | @@ -200,7 +200,7 @@ pub(crate) struct Auxiliary { |
|
|
|
|
|
### 3.3 用于state的查找表格子
|
|
|
|
|
|
在cnt=1行,32个格子用于state的查找表,每个查找表用8个连续的格子,所以总共可以有4个查找表。不到4个,格子填充默认值0。
|
|
|
在cnt=1行,32个格子用于state的查找表,每个查找表用8个连续的格子。
|
|
|
|
|
|
一个查找表操作在代码里用enum表示,state是enum其中一个。成员即是8个格子,代码里用Expression结构。
|
|
|
```rust
|
... | ... | @@ -233,20 +233,24 @@ pub enum LookupEntry<F> { |
|
|
```
|
|
|
要在代码里创建这种查找表操作,我们要用`meta.query_xx`将8列变为8个表达式Experssion,然后再创建这种enum。需要注意的是,代码的Rotation我们要用prev,即-1,因为我们设计的参照行是cnt=0行,cnt=1行是其上一行。
|
|
|
|
|
|
### 3.4 其他用途的格子
|
|
|
|
|
|
在cnt=1,2,3...等行中,多功能列的格子会有不同用途,根据执行状态的设计而定。
|
|
|
|
|
|
## 4 约束和分配数值
|
|
|
|
|
|
### 4.1 执行工具 Execution Gadget
|
|
|
|
|
|
`ExecutionGadget` 是一个定义在 Rust 中的 trait,用于配置和生成执行状态的约束和证据。这个 trait 包含以下关键部分:
|
|
|
`ExecutionGadget` 是一个定义在 Rust 中的 trait,用于配置和生成执行状态的证据和约束。这个 trait 包含以下关键部分:
|
|
|
|
|
|
- **NUM_STATE_HI_COL+NUM_STATE_LO_COL**: 动态选择器所需的列数。
|
|
|
- **NUM_STATE_HI_COL, NUM_STATE_LO_COL**: 动态选择器所需的列数。
|
|
|
- **name()**: 返回执行工具的名称。
|
|
|
- **execution_state()**: 返回执行状态。
|
|
|
- **num_row()**: 返回该执行状态在核心电路中使用的行数。
|
|
|
- **unusable_rows()**: 返回在实际证据之前和之后不能使用的行数,这决定了选择器不能启用的行数。
|
|
|
- **get_constraints()**: 类似configure函数,返回值是表达式的向量,用于创建门约束。
|
|
|
- **get_lookups()**: 返回用于查找表约束的 LookupEntry 向量。不过只负责查找表的部分。
|
|
|
- **gen_witness()**: 生成此执行状态的核心子电路的具体数值,并生成其他子电路需要的行。`Trace` 表示执行轨迹,`CurrentState` 表示当前的 EVM 状态。
|
|
|
- **get_lookups()**: 返回用于查找表约束的 LookupEntry 向量。用于创建查找表约束。
|
|
|
- **gen_witness(trace, current_state)**: 生成此执行状态的核心子电路证据的具体数值,并生成其他子电路需要的行。`trace` 表示执行轨迹,`current_state` 表示当前的 EVM 状态。
|
|
|
|
|
|
```rust
|
|
|
/// Execution Gadget for the configure and witness generation of an execution state
|
... | ... | @@ -312,6 +316,7 @@ pub(crate) trait ExecutionGadget< |
|
|
/// | 0 | DYNA_SELECTOR | AUX |
|
|
|
/// +---+-------+-------+-------+----------+
|
|
|
```
|
|
|
|
|
|
## 5 执行状态的转换流程
|
|
|
|
|
|
![image.png](../image/state_transform.png)
|
... | ... | |