|
# 总体布局
|
|
# 总体布局
|
|
本段介绍结构体`CoreCircuitConfig`的列及其含义。
|
|
本段介绍结构体`CoreCircuitConfig`的列及其含义。
|
|
## 单功能列 Single-purpose columns
|
|
## 1 单功能列 Single-purpose columns
|
|
下面是core子电路中最简单的部分,单功能的列:
|
|
下面是core子电路中最简单的部分,单功能的列:
|
|
```rust
|
|
```rust
|
|
/// transaction index, the index inside the block, repeated for rows in one execution state
|
|
pub struct CoreCircuitConfig<F: Field, const NUM_STATE_HI_COL: usize, const NUM_STATE_LO_COL: usize>
|
|
|
|
{
|
|
|
|
/// Transaction index, the index inside the block, repeated for rows in one transaction
|
|
pub tx_idx: Column<Advice>,
|
|
pub tx_idx: Column<Advice>,
|
|
/// call id, unique for each call, repeated for rows in one execution state
|
|
/// Call id, unique for each call, repeated for rows in one execution state
|
|
pub call_id: Column<Advice>,
|
|
pub call_id: Column<Advice>,
|
|
/// contract code address, repeated for rows in one execution state
|
|
/// Contract code address, repeated for rows in one execution state
|
|
pub code_addr: Column<Advice>,
|
|
pub code_addr: Column<Advice>,
|
|
/// program counter, repeated for rows in one execution state
|
|
/// Program counter, repeated for rows in one execution state
|
|
pub pc: Column<Advice>,
|
|
pub pc: Column<Advice>,
|
|
/// the opcode, repeated for rows in one execution state
|
|
/// The opcode, repeated for rows in one execution state
|
|
pub opcode: Column<Advice>,
|
|
pub opcode: Column<Advice>,
|
|
/// row counter, decremented for rows in one execution state
|
|
/// Row counter, decremented for rows in one execution state
|
|
pub cnt: Column<Advice>,
|
|
pub cnt: Column<Advice>,
|
|
|
|
...
|
|
|
|
}
|
|
```
|
|
```
|
|
|
|
|
|
- tx_idx指交易是区块的第几笔
|
|
- tx_idx: 表示交易是区块的第几笔
|
|
- call_id是我们在处理执行轨迹的时候,遇到新的call,就给其分配一个唯一的id。注意不是每次增加1的
|
|
- call_id:在处理执行轨迹的时候,遇到新的call,就给其分配一个唯一的id (不是每次增加1)
|
|
- code_addr是此时运行的合约代码的地址
|
|
- code_addr:当前运行的合约代码的地址
|
|
- pc是此时程序计数器的位置
|
|
- pc:当前程序计数器的位置
|
|
- opcode是此时程序计数器指向的指令
|
|
- opcode:当前程序计数器指向的指令
|
|
- 较为难理解的是列cnt,它是为了在执行一步占用多行的情况下设计的。在执行状态这一章会详细讲解。
|
|
- cnt:为了在执行一步占用多行的情况下设计的,在执行状态这一章会详细讲解。
|
|
|
|
|
|
core子电路中,行数的推进也意味着EVM程序执行轨迹的推进,如果某变化发生,那么下一行的这个列的值就会发生变化,也会有门约束约束这个变化。例如,下一步的pc要加2,那么witness的表中pc这列的值下一行就要加2,并且电路需要约束pc的差为2。
|
|
在EVM执行轨迹的电路设计中,每一行代表程序的一个执行步骤,程序状态变量(如pc)在每一行都有相应的变化,并且这些变化需要通过逻辑门约束来确保其符合预期的行为。具体例子中,如果pc在当前行增加2,那么在witness表中pc列的下一行的值也要增加2,并且电路中需要一个约束来确保pc的增量为2。
|
|
|
|
|
|
## 多功能列 Versatile columns
|
|
## 2 多功能列 Versatile columns
|
|
为了减少列的使用,缩减电路规模,我们设计了多功能的列。在不同的执行状态、不同的指令下,这些列起到不同的作用。除了上述单功能的列以外,其他我们需要的状态、变量等等,都使用多功能的列,可以达到重复利用列的效果。
|
|
为了减少列的使用,缩减电路规模,我们设计了多功能的列。在不同的执行状态、不同的指令下,这些列起到不同的作用。除了上述单功能的列以外,其他我们需要的状态、变量等等,都使用多功能的列,可以达到重复利用列的效果。
|
|
|
|
|
|
目前设计有32个多功能的列,代码里呈现为
|
|
目前设计有32个多功能的列,代码里定义如下:
|
|
```rust
|
|
```rust
|
|
/// versatile columns that serve multiple purposes
|
|
/// Number of versatile columns in core circuit
|
|
|
|
pub const NUM_VERS: usize = 32;
|
|
|
|
pub struct CoreCircuitConfig<F: Field, const NUM_STATE_HI_COL: usize, const NUM_STATE_LO_COL: usize>
|
|
|
|
{
|
|
|
|
...
|
|
|
|
/// Versatile columns that serve multiple purposes
|
|
pub vers: [Column<Advice>; NUM_VERS],
|
|
pub vers: [Column<Advice>; NUM_VERS],
|
|
|
|
...
|
|
|
|
}
|
|
```
|
|
```
|
|
其具体功能在执行状态一章会详细讲解。
|
|
其具体功能在执行状态一章会详细讲解。
|
|
|
|
|
|
## 执行状态 Execution State in Versatile
|
|
## 3 执行状态 Execution State in Versatile
|
|
|
|
|
|
### 概念
|
|
### 3.1 概念
|
|
|
|
|
|
执行状态是core子电路中每一步骤的种类,用以区分不同步骤的不同操作。EVM中的步骤的种类是指令(或opcode),而电路中的步骤的种类是执行状态。指令与执行状态*基本*成一一对应关系。有些相似指令,可以用同一种执行状态概括这些指令的操作。有些指令操作过于复杂,需要用连续的多个执行步骤进行处理。执行步骤的设计理念是使得代码尽量简单。
|
|
执行状态是core子电路中每一步骤的种类,用以区分不同步骤的不同操作。EVM中的步骤的种类是指令(或opcode),而电路中的步骤的种类是执行状态。指令与执行状态*基本*成一一对应关系。有些相似指令,可以用同一种执行状态概括这些指令的操作。有些指令操作过于复杂,需要用连续的多个执行步骤进行处理。执行步骤的设计理念是使得代码尽量简单。
|
|
|
|
|
|
在代码里,使用enum来标识执行状态。执行状态的种类分为以下几种:
|
|
在代码里,使用enum来标识执行状态。执行状态的种类分为以下几种:
|
|
#### 指令可对应的状态
|
|
#### 3.1.1 指令可对应的状态
|
|
这类状态目的就是处理EVM的指令的执行轨迹。包括但不限于:
|
|
这类状态目的就是处理EVM的指令的执行轨迹。包括但不限于:
|
|
```rust
|
|
```rust
|
|
pub enum ExecutionState {
|
|
pub enum ExecutionState {
|
... | @@ -65,7 +76,7 @@ pub enum ExecutionState { |
... | @@ -65,7 +76,7 @@ pub enum ExecutionState { |
|
```
|
|
```
|
|
我们可以注意到,这两个名称“DIV_MOD”,“AND_OR_XOR”由下划线分隔了,意味着他们可以处理多个功能、逻辑相近的指令(DIV和MOD,AND、OR和XOR)。以逻辑运算指令AND、OR和XOR为例,尽管它们运算不同,但是操作模式相似。因此为了减少重复代码,可以使用一个执行状态处理这三种指令。
|
|
我们可以注意到,这两个名称“DIV_MOD”,“AND_OR_XOR”由下划线分隔了,意味着他们可以处理多个功能、逻辑相近的指令(DIV和MOD,AND、OR和XOR)。以逻辑运算指令AND、OR和XOR为例,尽管它们运算不同,但是操作模式相似。因此为了减少重复代码,可以使用一个执行状态处理这三种指令。
|
|
|
|
|
|
#### zkEVM电路内部的状态
|
|
#### 3.1.2 zkEVM电路内部的状态
|
|
在zkEVM电路中为了处理一些非EVM指令的流程,需要使用一些内部状态。EVM中不存在此概念。包括但不限于:
|
|
在zkEVM电路中为了处理一些非EVM指令的流程,需要使用一些内部状态。EVM中不存在此概念。包括但不限于:
|
|
```rust
|
|
```rust
|
|
pub enum ExecutionState {
|
|
pub enum ExecutionState {
|
... | @@ -79,37 +90,75 @@ pub enum ExecutionState { |
... | @@ -79,37 +90,75 @@ pub enum ExecutionState { |
|
......
|
|
......
|
|
}
|
|
}
|
|
```
|
|
```
|
|
#### EVM错误状态
|
|
#### 3.1.3 EVM错误状态
|
|
对于EVM执行智能合约遇到错误的情况,例如out of gas,stack overflow等等,我们也需要处理。因此需要使用一些状态来表示遇到了EVM的错误。还未设计。
|
|
对于EVM执行智能合约遇到错误的情况,例如out of gas,stack overflow等等,也需要进一步处理。因此需要使用一些状态来表示遇到了EVM的错误。目前本项目更关注正确执行的情况,错误状态还未设计。
|
|
|
|
|
|
|
|
### 3.2 多行布局
|
|
|
|
|
|
### 多行布局
|
|
#### 3.2.1 介绍
|
|
|
|
|
|
一个执行状态,会使用连续的多行多功能列。例如,使用3行,即代码里变量`NUM_ROWS=3`,那么相当于使用了3*32=96个格子。
|
|
一个执行状态,会使用连续的多行多功能列。例如,使用3行,即代码里变量`NUM_ROWS=3`,那么相当于使用了3*32=96个格子。
|
|
|
|
|
|
> 这个例子里,不直接使用1行96列的原因是我们想要减少列的使用。
|
|
> 这个例子里,不直接使用1行96列的原因是我们想要减少列的使用。
|
|
|
|
|
|
对于一个执行状态的多行,我们对每个格子的使用方法做了统一设计,也设计了cnt列的使用方法。统一设计可以使得不同执行状态的开发变得相似,有利于减少重复代码。同时,还可以合并不同执行状态的约束(主要是查找表约束)。规定如下:
|
|
对于一个执行状态的多行,我们对每个格子的使用方法做了统一设计,也设计了cnt列的使用方法。统一设计可以使得不同执行状态的开发变得相似,有利于减少重复代码。同时,还可以合并不同执行状态的约束(主要是查找表约束)。
|
|
|
|
|
|
|
|
**关于行的规定:**
|
|
|
|
|
|
|
|
1. **行数确定**:每个执行状态的行数(代码里的变量`NUM_ROWS`)需要确定,且必须是大于0的整数。例如,`NUM_ROWS=3`表示使用3行。
|
|
|
|
2. **连续的行**:执行状态使用的是连续的`NUM_ROWS`行。在这些行中,cnt列的值从`NUM_ROWS-1`递减至0。cnt的值决定了每行的具体功能。
|
|
|
|
|
|
|
|
**关于cnt列的使用方法:**
|
|
|
|
|
|
|
|
根据cnt列的值,每行的使用方法有所不同:
|
|
|
|
|
|
|
|
1. **cnt=0的行**:
|
|
|
|
- **前半部分(16列)**:作为“动态选择器”,动态选择不同的操作或数据。
|
|
|
|
- **后半部分(16列)**:用于“辅助变量”,存储临时数据或中间结果。
|
|
|
|
2. **cnt=1的行**:
|
|
|
|
- **变量的使用**:用于操作数及其属性的变量。
|
|
|
|
- **查找表功能**:可以作为来源进行去向是state子电路的查找表。这行的数据可以用于在state子电路中进行查找和匹配。
|
|
|
|
3. **cnt=2及以上的行**:
|
|
|
|
- **查找表功能**:用于除state子电路以外的查找表。这些行的数据用于其他类型的查找和匹配。
|
|
|
|
|
|
|
|
#### 3.2.2 动态选择器 Dynamic Selector
|
|
|
|
|
|
|
|
在电路设计中,不同的执行状态需要不同的约束。例如:
|
|
|
|
|
|
- 针对一个执行状态,开发时要确定其使用的行数,即代码里变量`NUM_ROWS`,应为大于0的整数。
|
|
- **加法操作(ADD)**:约束为`a + b - c = 0`
|
|
- 执行状态使用的行是连续`NUM_ROWS`行,这些行里,cnt列的值从`NUM_ROWS-1`递减至0。下文用cnt=X表示cnt取值为X时的行
|
|
- **乘法操作(MUL)**:约束为`a * b - c = 0`
|
|
- cnt=0的行的使用方法是:32列的前半部分作为“动态选择器”,后半部分用于“辅助变量”。
|
|
|
|
- cnt=1的行的使用方法是,作为操作数及其属性的变量,同时起到可以作为来源进行去向是state子电路的查找表的作用。
|
|
|
|
- cnt=2及以上的行的使用方法是,作为除state以外的查找表的作用。暂未完成全部说明。
|
|
|
|
|
|
|
|
#### 动态选择器 Dynamic Selector
|
|
在ADD执行状态下,需要启用加法约束并禁用乘法约束;在MUL执行状态下,则相反。传统的静态选择器(selector列)无法动态改变约束,因此需要一种动态选择器来实现这一功能。可以使用halo2的selector来启用、禁用约束,但是这种selector列是静态的,固定的,不像advice列一样是可以作为变量改变,而不改变电路的。因此,我们需要发明一种“动态选择器”,可以通过改变advice列的值来启用、禁用约束。
|
|
|
|
|
|
电路的约束,包括门约束和查找表约束,需要在不同执行状态下开启。例如,都是3个操作数a b c的执行状态,加法ADD和乘法MUL的门约束,一个应是a+b-c=0,一个应是a\*b-c=0。那么在ADD执行状态下,我们启用“a+b-c=0”,禁用“a\*b-c=0”,MUL执行状态下相反。可以使用halo2的selector来启用、禁用约束,但是这种selector列是静态的,固定的,不像advice列一样是可以作为变量改变,而不改变电路的。因此,我们需要发明一种“动态选择器”,可以通过改变advice列的值来启用、禁用约束。
|
|
动态选择器是一种电路组件,通过若干个advice列(变量)作为输入,输出N个0或1的表达式,用于控制N种执行状态的约束。具体来说:
|
|
|
|
|
|
动态选择器在概念上,是有若干个变量(advice列的格子)作为输入,输出N个0、1表达式的电路的一种组成部分。N个输出是由若干输入进行某种运算得出的,可用于控制启用、禁用N种执行状态的约束。由此可见,N也是执行状态的数目。一种最简单的设计是输入使用的个数也是N个advice列,使用当前行(`Rotation::cur()`)取得N个变量,直接作为N个输出。我们采用了更复杂的方法,使得输入变量的数目减少为2sqrt(N)。具体方法不在这里赘述。
|
|
1. **输入**:若干个advice列的值。
|
|
|
|
2. **输出**:N个0或1的表达式,用于启用或禁用N种约束。
|
|
|
|
3. **执行状态数目(N)**:输出的个数也是执行状态的数目。
|
|
|
|
|
|
|
|
N个输出是由若干输入进行某种运算得出的,可用于控制启用、禁用N种执行状态的约束。由此可见,N也是执行状态的数目。一种最简单的设计是输入使用的个数也是N个advice列,使用当前行(`Rotation::cur()`)取得N个变量,直接作为N个输出。我们采用了更复杂的方法,使得输入变量的数目减少为2sqrt(N)。具体方法不在这里赘述。
|
|
|
|
|
|
在代码上,我们的动态选择器是如下的结构体:`DynamicSelectorConfig`和`DynamicSelectorChip`。这两个结构体区别很小,只是一种代码习惯。结构体的成员就包括2sqrt(N)个advice列。结构体最重要的方法是获取第`target`个输出的方法:
|
|
在代码上,我们的动态选择器是如下的结构体:`DynamicSelectorConfig`和`DynamicSelectorChip`。这两个结构体区别很小,只是一种代码习惯。结构体的成员就包括2sqrt(N)个advice列。结构体最重要的方法是获取第`target`个输出的方法:
|
|
```rust
|
|
```rust
|
|
|
|
impl<F: Field, const CNT: usize, const NUM_HIGH: usize, const NUM_LOW: usize>
|
|
|
|
DynamicSelectorConfig<F, CNT, NUM_HIGH, NUM_LOW>
|
|
|
|
{
|
|
|
|
...
|
|
|
|
/// Get the selector value of target
|
|
pub fn selector(
|
|
pub fn selector(
|
|
&self,
|
|
&self,
|
|
meta: &mut VirtualCells<F>,
|
|
meta: &mut VirtualCells<F>,
|
|
target: usize,
|
|
target: usize,
|
|
at: Rotation,
|
|
at: Rotation,
|
|
) -> Expression<F>
|
|
) -> Expression<F> {
|
|
|
|
assert!(target < NUM_LOW * NUM_HIGH);
|
|
|
|
let high = target / NUM_LOW;
|
|
|
|
let low = target % NUM_LOW;
|
|
|
|
let target_high = meta.query_advice(self.target_high[high], at);
|
|
|
|
let target_low = meta.query_advice(self.target_low[low], at);
|
|
|
|
target_high * target_low
|
|
|
|
}
|
|
|
|
}
|
|
```
|
|
```
|
|
在创建约束时,使用动态选择器作为启用、禁用的条件的示例如下,以ADD为例(示例代码,非开发代码):
|
|
在创建约束时,使用动态选择器作为启用、禁用的条件的示例如下,以ADD为例(示例代码,非开发代码):
|
|
```rust
|
|
```rust
|
... | @@ -120,7 +169,7 @@ return vec![condition*(a+b-c)] |
... | @@ -120,7 +169,7 @@ return vec![condition*(a+b-c)] |
|
```
|
|
```
|
|
如上所述,我们的动态选择器的设计使用的变量,是来自2sqrt(N)个advice列的同一行的变量,因此,这些格子的布局可以在一行内装下,即cnt=0的行。只需保证2sqrt(N) < 32 即可。
|
|
如上所述,我们的动态选择器的设计使用的变量,是来自2sqrt(N)个advice列的同一行的变量,因此,这些格子的布局可以在一行内装下,即cnt=0的行。只需保证2sqrt(N) < 32 即可。
|
|
|
|
|
|
#### 辅助变量
|
|
#### 3.2.3 辅助变量Auxiliary
|
|
辅助变量是一些表示当前EVM执行的进度或者状态的变量,我们使用cnt=0行里的一些特定位置的格子进行记录。例如,上文所述的动态选择器使用了32列中前20列,那么我们可以设计,辅助变量使用21至32列。辅助变量包括:
|
|
辅助变量是一些表示当前EVM执行的进度或者状态的变量,我们使用cnt=0行里的一些特定位置的格子进行记录。例如,上文所述的动态选择器使用了32列中前20列,那么我们可以设计,辅助变量使用21至32列。辅助变量包括:
|
|
```rust
|
|
```rust
|
|
pub(crate) struct Auxiliary {
|
|
pub(crate) struct Auxiliary {
|
... | @@ -144,9 +193,7 @@ pub(crate) struct Auxiliary { |
... | @@ -144,9 +193,7 @@ pub(crate) struct Auxiliary { |
|
|
|
|
|
每个执行状态会对于这些变量进行不同的变化,例如ADD会将state_stamp加3,stack_pointer减1。
|
|
每个执行状态会对于这些变量进行不同的变化,例如ADD会将state_stamp加3,stack_pointer减1。
|
|
|
|
|
|
> 注:Gas & Refund已有设计,没实现。等待从钉钉文档搬运过来。Memory chunk 和 readonly 暂无。
|
|
### 3.3 用于state的查找表格子
|
|
|
|
|
|
### 用于state的查找表格子
|
|
|
|
|
|
|
|
在cnt=1行,32个格子用于state的查找表,每个查找表用8个连续的格子,所以总共可以有4个查找表。不到4个,格子填充默认值0。
|
|
在cnt=1行,32个格子用于state的查找表,每个查找表用8个连续的格子,所以总共可以有4个查找表。不到4个,格子填充默认值0。
|
|
|
|
|
... | @@ -181,9 +228,20 @@ pub enum LookupEntry<F> { |
... | @@ -181,9 +228,20 @@ pub enum LookupEntry<F> { |
|
```
|
|
```
|
|
要在代码里创建这种查找表操作,我们要用`meta.query_xx`将8列变为8个表达式Experssion,然后再创建这种enum。需要注意的是,代码的Rotation我们要用prev,即-1,因为我们设计的参照行是cnt=0行,cnt=1行是其上一行。
|
|
要在代码里创建这种查找表操作,我们要用`meta.query_xx`将8列变为8个表达式Experssion,然后再创建这种enum。需要注意的是,代码的Rotation我们要用prev,即-1,因为我们设计的参照行是cnt=0行,cnt=1行是其上一行。
|
|
|
|
|
|
# 约束和分配数值
|
|
# 4 约束和分配数值
|
|
|
|
|
|
|
|
## 4.1 执行工具 Execution Gadget
|
|
|
|
|
|
## 落实到代码:执行工具 Execution Gadget
|
|
`ExecutionGadget` 是一个定义在 Rust 中的 trait,用于配置和生成执行状态的约束和证据。这个 trait 包含以下关键部分:
|
|
|
|
|
|
|
|
- **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 状态。
|
|
|
|
|
|
```rust
|
|
```rust
|
|
/// Execution Gadget for the configure and witness generation of an execution state
|
|
/// Execution Gadget for the configure and witness generation of an execution state
|
... | @@ -220,28 +278,19 @@ pub(crate) trait ExecutionGadget< |
... | @@ -220,28 +278,19 @@ pub(crate) trait ExecutionGadget< |
|
fn gen_witness(&self, trace: &Trace, current_state: &mut CurrentState) -> Witness;
|
|
fn gen_witness(&self, trace: &Trace, current_state: &mut CurrentState) -> Witness;
|
|
}
|
|
}
|
|
```
|
|
```
|
|
- NUM_STATE_HI_COL+NUM_STATE_LO_COL是动态选择器所需的列数
|
|
## 4.2 门约束
|
|
- get_constraints类似configure函数,返回值是表达式的向量,用于创建门约束
|
|
每个执行状态都有对应的执行工具(Gadget),其方法 `get_constraints` 返回需要创建的所有门约束,形式为表达式的向量。在核心子电路中,通过循环对每一个执行工具调用 `get_constraints` 并创建其返回的门约束。
|
|
- get_lookups类似configure函数不过只负责查找表的部分。为了代码整洁,我们自定义了LookupEntry
|
|
|
|
- gen_witness,生成此执行状态的core子电路的`NUM_ROWS`行的具体数值,为了方便其他子电路,也生成其他子电路需要的行。此方法的输入,Trace是这一步骤的执行轨迹,CurrentState是此时我们程序所需要的EVM的当前状态,目前包括pc, stack, memory等状态。
|
|
|
|
|
|
|
|
## 门约束
|
|
|
|
每个执行状态有对应的执行工具Gadget,其方法get_constraints返回所有需要创建的门约束,形式为表达式的向量。
|
|
|
|
|
|
|
|
在core子电路中,通过循环对每一个执行工具都调用get_constraints并创建其返回的门约束。
|
|
|
|
|
|
|
|
## 查找表约束
|
|
## 4.3 查找表约束
|
|
每个执行状态有对应的执行工具Gadget,其方法get_lookups返回所有需要创建的查找表约束,形式为LookupEntry的向量。
|
|
每个执行状态都有对应的执行工具(Gadget),其方法 `get_lookups` 返回需要创建的所有查找表约束,形式为 `LookupEntry` 的向量。在核心子电路中,通过循环对每一个执行工具调用 `get_lookups` 并将相同的 `LookupEntry` 合并,然后创建查找表约束,即 `meta.lookup_any(...)`。
|
|
|
|
|
|
在core子电路中,通过循环对每一个执行工具都调用get_lookups,并将相同的LookupEntry合并,然后创建查找表约束,即`meta.lookup_any(...)`。
|
|
## 4.4 排列约束
|
|
|
|
目前没有用到Permutation constraints排列约束。
|
|
|
|
|
|
## 排列约束
|
|
## 4.5 分配数值
|
|
目前没有用到Permutation constraints。
|
|
因为证据(Witness)的表格设计和子电路的列的设计基本对应,分配数值的代码被简化。只需将表格每一行的数值分配给子电路的相应列的相应行(offset)。Witness 的生成由每个执行工具的 `gen_witness` 方法负责。
|
|
|
|
|
|
## 分配数值
|
|
## 4.6 例子
|
|
因为证据Witness的表格设计和子电路的列的设计基本呈对应关系,分配数值的代码被大大简化。我们只需将表格每一行的数值分配给子电路的相应列的相应行(offset)即可。Witness生成则由每个执行工具的gen_witness方法负责,详见其代码。
|
|
|
|
|
|
|
|
## 例子
|
|
|
|
形象展示:
|
|
形象展示:
|
|
```rust
|
|
```rust
|
|
/// Add Execution State layout is as follows
|
|
/// Add Execution State layout is as follows
|
... | @@ -258,9 +307,9 @@ pub(crate) trait ExecutionGadget< |
... | @@ -258,9 +307,9 @@ pub(crate) trait ExecutionGadget< |
|
/// | 0 | DYNA_SELECTOR | AUX |
|
|
/// | 0 | DYNA_SELECTOR | AUX |
|
|
/// +---+-------+-------+-------+----------+
|
|
/// +---+-------+-------+-------+----------+
|
|
```
|
|
```
|
|
代码:https://git.code.tencent.com/chainmaker-zk/zkevm/blob/develop/zkevm-circuits/src/execution/add.rs
|
|
代码:https://git.code.tencent.com/chainmaker-zk/zkevm/blob/develop/zkevm-circuits/src/execution/addmod.rs
|
|
|
|
|
|
# 执行状态的转换流程
|
|
# 5 执行状态的转换流程
|
|
|
|
|
|
![image.png](/uploads/2/088B5A7969A744E7850B04351472A9F1/image.png)
|
|
![image.png](/uploads/2/088B5A7969A744E7850B04351472A9F1/image.png)
|
|
|
|
|
... | @@ -275,33 +324,35 @@ pub(crate) trait ExecutionGadget< |
... | @@ -275,33 +324,35 @@ pub(crate) trait ExecutionGadget< |
|
最里面一层是交易内的普通状态,转换过程和solidity的调用类似,遇到RETURN/REVERT、STOP 则进入END_CALL返回父函数;如果当前已经是最顶层的函数,那么就结束交易。(通过call_id是否等于0来判断当前是否结束交易)
|
|
最里面一层是交易内的普通状态,转换过程和solidity的调用类似,遇到RETURN/REVERT、STOP 则进入END_CALL返回父函数;如果当前已经是最顶层的函数,那么就结束交易。(通过call_id是否等于0来判断当前是否结束交易)
|
|
|
|
|
|
|
|
|
|
## 执行状态的转换约束
|
|
## 5.1 执行状态的转换约束
|
|
某些执行状态之前或之后,需要约束为某个特定的执行状态,比如 end\_block,需要约束之前执行状态是END\_TX或BEGIN\_BLOCK,约束之后执行状态是 BEGIN\_BLOCK 或END\_CHUNK。
|
|
某些执行状态之前或之后,需要约束为某个特定的执行状态,比如 end\_block,需要约束之前执行状态是END\_TX或BEGIN\_BLOCK,约束之后执行状态是 BEGIN\_BLOCK 或END\_CHUNK。
|
|
|
|
|
|
constraints.append(&mut config.get_exec_state_constraints(
|
|
```rust
|
|
meta,
|
|
constraints.append(&mut config.get_exec_state_constraints(
|
|
ExecStateTransition::new(
|
|
meta,
|
|
// 之前的执行状态约束,没有cond,表示两种执行状态都可以。
|
|
ExecStateTransition::new(
|
|
vec![ExecutionState::END_TX, ExecutionState::BEGIN_BLOCK],
|
|
// 之前的执行状态约束,没有cond,表示两种执行状态都可以。
|
|
// 当前 gadget 的 NUM_ROW
|
|
vec![ExecutionState::END_TX, ExecutionState::BEGIN_BLOCK],
|
|
NUM_ROW,
|
|
// 当前 gadget 的 NUM_ROW
|
|
// 之后的执行状态约束
|
|
NUM_ROW,
|
|
vec![
|
|
// 之后的执行状态约束
|
|
// 如果 next_is_begin_block == 1,下个执行状态是 BEGIN_BLOCK
|
|
vec![
|
|
(
|
|
// 如果 next_is_begin_block == 1,下个执行状态是 BEGIN_BLOCK
|
|
ExecutionState::BEGIN_BLOCK,
|
|
(
|
|
begin_block::NUM_ROW,
|
|
ExecutionState::BEGIN_BLOCK,
|
|
Some(next_is_begin_block), // 这里为了减少 degree
|
|
begin_block::NUM_ROW,
|
|
),
|
|
Some(next_is_begin_block), // 这里为了减少 degree
|
|
// 如果 next_is_end_chunk == 1,下个执行状态是 END_CHUNK
|
|
),
|
|
(
|
|
// 如果 next_is_end_chunk == 1,下个执行状态是 END_CHUNK
|
|
ExecutionState::END_CHUNK,
|
|
(
|
|
end_chunk::NUM_ROW,
|
|
ExecutionState::END_CHUNK,
|
|
Some(next_is_end_chunk), // 这里为了减少 degree
|
|
end_chunk::NUM_ROW,
|
|
),
|
|
Some(next_is_end_chunk), // 这里为了减少 degree
|
|
],
|
|
),
|
|
// 和 next_is_begin_block, next_is_end_chunk 作用一样
|
|
],
|
|
// vec 内不为0的,对应之后的执行状态
|
|
// 和 next_is_begin_block, next_is_end_chunk 作用一样
|
|
Some(vec![1.expr() - is_zero.expr(), is_zero.expr()]),
|
|
// vec 内不为0的,对应之后的执行状态
|
|
),
|
|
Some(vec![1.expr() - is_zero.expr(), is_zero.expr()]),
|
|
)); |
|
),
|
|
\ No newline at end of file |
|
));
|
|
|
|
``` |
|
|
|
\ No newline at end of file |