|
|
|
# State
|
|
|
|
|
|
回顾介绍中的内容,zkEVM 的核心是通过零知识证明技术来验证以太坊虚拟机(EVM)执行的智能合约程序的正确性。zkEVM 通过各种子电路(如 Core、State、Bytecode、Copy 等)分解和管理复杂的证明过程,每个子电路负责处理特定的逻辑部分。State 子电路专门处理虚拟机中各类状态的读写操作。
|
|
回顾介绍中的内容,zkEVM 的核心是通过零知识证明技术来验证以太坊虚拟机(EVM)执行的智能合约程序的正确性。zkEVM 通过各种子电路(如 Core、State、Bytecode、Copy 等)分解和管理复杂的证明过程,每个子电路负责处理特定的逻辑部分。State 子电路专门处理虚拟机中各类状态的读写操作。
|
|
|
|
|
|
# 布局
|
|
|
|
|
|
|
|
### StateCircuitConfig 结构体
|
|
## StateCircuitConfig 结构体
|
|
|
|
|
|
StateCircuitConfig 定义了 State 子电路所需的配置,它包括多个列和选择器,用于管理和验证状态操作。以下是 StateCircuitConfig 的详细介绍:
|
|
StateCircuitConfig 定义了 State 子电路所需的配置,它包括多个列和选择器,用于管理和验证状态操作。以下是 StateCircuitConfig 的详细介绍:
|
|
```rust
|
|
```rust
|
... | @@ -35,7 +36,7 @@ pub struct StateCircuitConfig<F> { |
... | @@ -35,7 +36,7 @@ pub struct StateCircuitConfig<F> { |
|
|
|
|
|
**_marker**: 一个 PhantomData 类型,用于在编译时检查泛型类型 F。
|
|
**_marker**: 一个 PhantomData 类型,用于在编译时检查泛型类型 F。
|
|
|
|
|
|
### Tag 枚举
|
|
## Tag 枚举
|
|
|
|
|
|
Tag 枚举定义了不同的状态类型,每种类型对应不同的状态操作:
|
|
Tag 枚举定义了不同的状态类型,每种类型对应不同的状态操作:
|
|
|
|
|
... | @@ -95,7 +96,7 @@ pub enum CallContextTag { |
... | @@ -95,7 +96,7 @@ pub enum CallContextTag { |
|
```
|
|
```
|
|
这些标签用于表示调用上下文中的不同字段,如父调用 ID、父代码合约地址、父程序计数器、父堆栈指针、存储合约地址、发送者地址、调用数据大小、返回数据大小和返回数据调用 ID。
|
|
这些标签用于表示调用上下文中的不同字段,如父调用 ID、父代码合约地址、父程序计数器、父堆栈指针、存储合约地址、发送者地址、调用数据大小、返回数据大小和返回数据调用 ID。
|
|
|
|
|
|
# 列的含义
|
|
## 列的含义
|
|
|
|
|
|
Tag不同,含义不同,如下。
|
|
Tag不同,含义不同,如下。
|
|
|
|
|
... | @@ -135,14 +136,14 @@ Tag不同,含义不同,如下。 |
... | @@ -135,14 +136,14 @@ Tag不同,含义不同,如下。 |
|
- value_lo: byte数值
|
|
- value_lo: byte数值
|
|
- stamp, is_write: 望文生义即可
|
|
- stamp, is_write: 望文生义即可
|
|
|
|
|
|
# 约束
|
|
## 约束
|
|
|
|
|
|
为了保证读写一致性,我们需要对状态进行排序,排序规则如下:先按 `tag`,再按 `call_id`,`pointer_hi`,`pointer_lo`,`stamp` 排序。具体实现参考 scroll 的电路,我们使用以下方法:
|
|
为了保证读写一致性,我们需要对状态进行排序,排序规则如下:先按 `tag`,再按 `call_id`,`pointer_hi`,`pointer_lo`,`stamp` 排序。具体实现参考 scroll 的电路,我们使用以下方法:
|
|
|
|
|
|
1. 将 `tag`,`call_id`,`pointer_hi`,`pointer_lo`,`stamp` 元组编码为 16-bit 的 limbs。
|
|
1. 将 `tag`,`call_id`,`pointer_hi`,`pointer_lo`,`stamp` 元组编码为 16-bit 的 limbs。
|
|
2. 上下两行的 limbs 作差,第一个非零的 diff 的 index 记为 `first_diff_limb`,要求 `diff[first_diff_limb]` 是 16-bit 数。
|
|
2. 上下两行的 limbs 作差,第一个非零的 diff 的 index 记为 `first_diff_limb`,要求 `diff[first_diff_limb]` 是 16-bit 数。
|
|
|
|
|
|
## 具体约束方式
|
|
### 具体约束方式
|
|
|
|
|
|
- 用 `BinaryNumberChip` 表示变量 `first_diff_limb`,需要用 `log_2(L)` 个变量。
|
|
- 用 `BinaryNumberChip` 表示变量 `first_diff_limb`,需要用 `log_2(L)` 个变量。
|
|
|
|
|
... | @@ -160,7 +161,7 @@ Tag不同,含义不同,如下。 |
... | @@ -160,7 +161,7 @@ Tag不同,含义不同,如下。 |
|
|
|
|
|
> RLC: zkevm-circuits/zkevm-circuits/src/state_circuit/random_linear_combination.rs
|
|
> RLC: zkevm-circuits/zkevm-circuits/src/state_circuit/random_linear_combination.rs
|
|
|
|
|
|
## 不同Tag对应的约束
|
|
### 不同Tag对应的约束
|
|
定义变量`first_access`表示这个pointer的地方是否是第一次访问。其构造详情稍后详细描述。对于不是`first_access`的行,意味着上一行和这一行是同一个地方,我们排序又是按照`stamp`排的。因此,如果这一行是读(is_write=0),那么value必然等于上一行的`value`。
|
|
定义变量`first_access`表示这个pointer的地方是否是第一次访问。其构造详情稍后详细描述。对于不是`first_access`的行,意味着上一行和这一行是同一个地方,我们排序又是按照`stamp`排的。因此,如果这一行是读(is_write=0),那么value必然等于上一行的`value`。
|
|
|
|
|
|
**对不同tag,约束不同:**
|
|
**对不同tag,约束不同:**
|
... | @@ -201,10 +202,9 @@ Tag不同,含义不同,如下。 |
... | @@ -201,10 +202,9 @@ Tag不同,含义不同,如下。 |
|
|
|
|
|
`first_access`的表示可以用上述的`first_diff_limb`来判断。因为整个表格已经排好序了,如果`first_diff_limb`处于t`ag, callid`,`pointer hi`, `pointer lo`中,意味着要么这一行和上一行的tag不同,要么`callid`不同,要么`pointer`不同。也意味着是首次访问。反之,非首次访问。
|
|
`first_access`的表示可以用上述的`first_diff_limb`来判断。因为整个表格已经排好序了,如果`first_diff_limb`处于t`ag, callid`,`pointer hi`, `pointer lo`中,意味着要么这一行和上一行的tag不同,要么`callid`不同,要么`pointer`不同。也意味着是首次访问。反之,非首次访问。
|
|
|
|
|
|
### 约束 `is_write`
|
|
**约束 `is_write`**
|
|
|
|
|
|
- `is_write * (is_write - 1) = 0`
|
|
- `is_write * (is_write - 1) = 0`
|
|
|
|
|
|
这个约束表示 `is_write` 必须是 0 或 1,因为只有 0 和 1 满足这个方程。
|
|
这个约束表示 `is_write` 必须是 0 或 1,因为只有 0 和 1 满足这个方程。
|
|
|
|
|
|
### |
|
|
|
\ No newline at end of file |
|
|