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/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 满足这个方程。