This is an old version of this page. You can view the most recent version or browse the history.

5 state

回顾介绍中的内容，zkEVM 的核心是通过零知识证明技术来验证以太坊虚拟机（EVM）执行的智能合约程序的正确性。zkEVM 通过各种子电路（如 Core、State、Bytecode、Copy 等）分解和管理复杂的证明过程，每个子电路负责处理特定的逻辑部分。State 子电路专门处理虚拟机中各类状态的读写操作。

布局

StateCircuitConfig 结构体

StateCircuitConfig 定义了 State 子电路所需的配置，它包括多个列和选择器，用于管理和验证状态操作。以下是 StateCircuitConfig 的详细介绍：

pub struct StateCircuitConfig<F> {
    q_enable: Selector,
    tag: BinaryNumberConfig<Tag, LOG_NUM_STATE_TAG>,
    stamp: Column<Advice>,
    value_hi: Column<Advice>,
    value_lo: Column<Advice>,
    call_id_contract_addr: Column<Advice>,
    pointer_hi: Column<Advice>,
    pointer_lo: Column<Advice>,
    is_write: Column<Advice>,
    _marker: PhantomData<F>,
}

q_enable: 一个选择器，用于启用相关的约束。

tag: 一个二进制数配置，用于表示状态操作的类型，如堆栈（stack）、内存（memory）、存储（storage）、调用上下文（call context）、调用数据（call data）或返回数据（return data）。它通过 BinaryNumberConfig 实现，可以根据值启用特定的约束。

stamp: 每个状态操作的唯一标识，按顺序递增。

value_hi 和 value_lo: 代表状态值的高位和低位，用于存储 256 位数据。

call_id_contract_addr: 用于存储调用 ID 或合约地址。

pointer_hi 和 pointer_lo: 用于存储指针的高位和低位，指针可以是存储键、调用上下文标签、堆栈指针、内存地址或数据索引。

is_write: 表示操作是写操作还是读操作的二进制值。

_marker: 一个 PhantomData 类型，用于在编译时检查泛型类型 F。

Tag 枚举

Tag 枚举定义了不同的状态类型，每种类型对应不同的状态操作：

pub enum Tag {
    Memory,
    Stack,
    Storage,
    CallContext,
    CallData,
    ReturnData,
    EndPadding,
}

Memory: 内存操作。

Stack: 堆栈操作。

Storage: 存储操作。

CallContext: 调用上下文操作。

CallData: 调用数据操作。

ReturnData: 返回数据操作。

EndPadding: 用于填充的末尾数据。

其中，tag我们没有简单的使用一个advice列，而是用了一个电路小工具名叫“BinaryNumberConfig/BinaryNumberChip”。它既可以表示一个tag，也可以当做动态选择器，用于启用约束。例如，我们想tag的值为stack(1)时启动约束1，为memory(0)时启动约束2。那么，示例代码如下

let condition_1 = tag.value_equals(1);
let condition_2 = tag.value_equals(0);
vec![condition_1 * constraint_1, condition_2 * constraint_2]

关于BinaryNumberChip，详见here。

CallContextTag 枚举

CallContextTag 枚举定义了调用上下文中的不同标签：

pub enum CallContextTag {
    ParentCallId,
    ParentCodeContractAddr,
    ParentProgramCounter,
    ParentStackPointer,
    StorageContractAddr,
    SenderAddr,
    Value,
    CallDataSize,
    ReturnDataSize,
    ReturnDataCallId,
}

这些标签用于表示调用上下文中的不同字段，如父调用 ID、父代码合约地址、父程序计数器、父堆栈指针、存储合约地址、发送者地址、调用数据大小、返回数据大小和返回数据调用 ID。

列的含义

Tag不同，含义不同，如下。

Stack
- call_id_contract_addr: call_id
- pointer_hi: None
- pointer_lo: 栈上的位置，从1开始增加
- stamp, value_hi, value_lo, is_write: 望文生义即可
Memory
- call_id_contract_addr: call_id
- pointer_hi: None
- value_hi: None
- pointer_lo: 内存的位置
- value_lo: byte数值
- stamp, is_write: 望文生义即可
Storage
- call_id_contract_addr: contract_addr
- pointer_hi, lo: 组合起来是一个256-bit的key
- value_hi, lo: 组合起来是一个256-bit的value
- stamp, is_write: 望文生义即可
CallContext
- pointer_lo: 用于CallContextTag
- pointer_hi: None
- value_hi, value_lo: 望文生义即可，value_hi在有些情况下可能是0
- stamp, is_write: 望文生义即可
- 普通CallContextTag，除ReturnDataCallId
  - call_id_contract_addr: 当前call_id
- CallContextTag是ReturnDataCallId时
  - call_id_contract_addr: None
  - 采用None的原因是：ReturnDataCallId可以看做是一个全局变量，不论处于那个Call下，它都记录着最后一次Return的Id。
CallData, ReturnData
- call_id_contract_addr: call_id
- pointer_hi: None
- value_hi: None
- pointer_lo: offset，或者理解为index
- value_lo: byte数值
- stamp, is_write: 望文生义即可

约束

为了保证读写一致性，我们需要对状态进行排序，排序规则如下：先按 tag，再按 call_id，pointer_hi，pointer_lo，stamp 排序。具体实现参考 scroll 的电路，我们使用以下方法：

将 tag，call_id，pointer_hi，pointer_lo，stamp 元组编码为 16-bit 的 limbs。
上下两行的 limbs 作差，第一个非零的 diff 的 index 记为 first_diff_limb，要求 diff[first_diff_limb] 是 16-bit 数。

具体约束方式

用 BinaryNumberChip 表示变量 first_diff_limb，需要用 log_2(L) 个变量。
定义变量 limb_diff 表示 diff[first_diff_limb]。
定义 inv 表示前者的逆。
约束1：建立一个 expr 数组 v，是 diff 的累计 RLC（随机线性组合）。约束 sum {first_diff_limb.value_equals(i) * v[i]} == 0，即前 first_diff_limb 是否都为 0。
约束2：sum {first_diff_limb.value_equals(i) * diff[i]} - limb_diff，即 limb_diff 值是否等于 diff[first_diff_limb]。
约束3：limb_diff 存在 inv，即 1 - limb_diff * inv == 0。
约束4：limb_diff 在范围 u16 内，即 [0, 2^16-1]。

RLC: zkevm-circuits/zkevm-circuits/src/state_circuit/random_linear_combination.rs

不同Tag对应的约束

定义变量first_access表示这个pointer的地方是否是第一次访问。其构造详情稍后详细描述。对于不是first_access的行，意味着上一行和这一行是同一个地方，我们排序又是按照stamp排的。因此，如果这一行是读（is_write=0），那么value必然等于上一行的value。

对不同tag，约束不同：

Memory:

如果 first_access 且 is_write == 0，则 value = 0。
pointer_hi = 0。
value_hi = 0。
0 <= value_lo < 256。

Stack:

如果 first_access，则 is_write = 1，即首次访问一个栈位置，必须是写。
pointer_hi = 0。
1 <= pointer_lo <= 1024。

Storage:

如果 first_access 且 is_write == 0，则 value 需要满足 MPT（默克尔前缀树）。

CallContext:

如果 first_access，则 is_write = 1，即首次访问，必须是写。
pointer_hi = 0。

CallData:

如果 first_access 且 is_write == 0，则 value = 0。
pointer_hi = 0。
value_hi = 0。

ReturnData:

如果 first_access，则 value = 0，即首次访问 return_data，value 必须是 0。
pointer_hi = 0。
value_hi = 0。

first_access的表示可以用上述的first_diff_limb来判断。因为整个表格已经排好序了，如果first_diff_limb处于tag, callid,pointer hi, pointer lo中，意味着要么这一行和上一行的tag不同，要么callid不同，要么pointer不同。也意味着是首次访问。反之，非首次访问。

约束 `is_write`

is_write * (is_write - 1) = 0

这个约束表示 is_write 必须是 0 或 1，因为只有 0 和 1 满足这个方程。