|
|
|
# 布局
|
|
|
|
state子电路基础的设计包含如下几列。注意，和LookupEntry的State基本一致。
|
|
|
|
```rust
|
|
|
|
pub struct StateCircuitConfig<F> {
|
|
|
|
q_enable: Selector,
|
|
|
|
/// Type of value, one of stack, memory, storage, call context, call data or return data
|
|
|
|
/// A `BinaryNumberConfig` can return the indicator by method `value_equals`
|
|
|
|
tag: BinaryNumberConfig<Tag, LOG_NUM_STATE_TAG>,
|
|
|
|
/// Stamp that increments for each state operation, unique for each row
|
|
|
|
stamp: Column<Advice>,
|
|
|
|
/// High 128-bit value of the row
|
|
|
|
value_hi: Column<Advice>,
|
|
|
|
/// Low 128-bit value of the row
|
|
|
|
value_lo: Column<Advice>,
|
|
|
|
/// Call id (other types) or contract address (storage type only)
|
|
|
|
call_id_contract_addr: Column<Advice>,
|
|
|
|
/// High 128-bit of the key (storage type only)
|
|
|
|
pointer_hi: Column<Advice>,
|
|
|
|
/// Low 128-bit of the key (storage type only) or call context tag
|
|
|
|
/// Or stack pointer or memory address or data index (call data and return data)
|
|
|
|
pointer_lo: Column<Advice>,
|
|
|
|
/// Whether it is write or read, binary value
|
|
|
|
is_write: Column<Advice>,
|
|
|
|
_marker: PhantomData<F>,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum Tag {
|
|
|
|
// in case for padding zeros, we make default = memory. memory read of unused pointer is 0.
|
|
|
|
#[default]
|
|
|
|
Memory,
|
|
|
|
Stack,
|
|
|
|
Storage,
|
|
|
|
CallContext,
|
|
|
|
CallData,
|
|
|
|
ReturnData,
|
|
|
|
EndPadding,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum CallContextTag {
|
|
|
|
#[default]
|
|
|
|
ParentCallId,
|
|
|
|
ParentCodeContractAddr,
|
|
|
|
ParentProgramCounter,
|
|
|
|
ParentStackPointer,
|
|
|
|
StorageContractAddr,
|
|
|
|
SenderAddr,
|
|
|
|
Value,
|
|
|
|
CallDataSize,
|
|
|
|
ReturnDataSize,
|
|
|
|
ReturnDataCallId,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
其中，tag我们没有简单的使用一个advice列，而是用了一个电路小工具名叫“BinaryNumberConfig/BinaryNumberChip”。它既可以表示一个tag，也可以当做动态选择器，用于启用约束。例如，我们想tag的值为stack(1)时启动约束1，为memory(0)时启动约束2。那么，示例代码如下
|
|
|
|
```rust
|
|
|
|
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](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
|
|
|
|
|
|
|
|
## 列的含义
|
|
|
|
|
|
|
|
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，再按callid, pointer hi, pointer lo, stamp的顺序排序。
|
|
|
|
|
|
|
|
在开发的代码中，例如Rust语言，排序十分简单。难的是在电路中增加约束保证整个Witness的行是符合排序规则的。参考scroll的电路，我们使用如下方法。
|
|
|
|
|
|
|
|
## 约束排序的方式
|
|
|
|
|
|
|
|
将tag, callid, pointer hi, pointer lo, stamp元组编码为16-bit的limbs，假设有L个limbs。（可以bit更大但是那样比较难做range proof）。上下两行的limbs作差，有L个diff。第一个非零的diff，index记为first_diff_limb。要求diff[first_diff_limb]也是16-bit数即可。因为如果排序的顺序反了，则diff[first_diff_limb]是小数减大数，在有限域上得到一个非常大的结果（2^255左右），必然不属于16-bit的数。
|
|
|
|
|
|
|
|
具体做法：
|
|
|
|
- 用BinaryNumberChip表示变量first_diff_limb。需要用log_2(L)个变量。
|
|
|
|
- 再定义变量limb_diff表示diff[first_diff_limb]。
|
|
|
|
- 再定义inv表示前者的逆。
|
|
|
|
- 约束1：建立一个expr数组v，是diff的累计RLC(random linear combination)：[0, diff[0], diff[0]+r diff[1], diff[0]+r diff[1]+r' diff[2]...]。约束sum \{first_diff_limb.value_equals(i) * v[i]\} == 0。即，前first_diff_limb是否都为0。sum是通过for循环取i=0..L得到的。注：value_equals(x)方法是BinaryNumberChip中用来判断值是否等于x的，若等于输出1，否则输出0。
|
|
|
|
注：也许可以把RLC改成^2。
|
|
|
|
- 约束2：sum \{first_diff_limb.value_equals(i) * diff[i]\} - limb_diff。即，limb_diff值是否按照定义等于diff[first_diff_limb]。sum是通过for循环取i=0..L得到的。
|
|
|
|
- 约束3：limb_diff存在inv。 1-limb_diff * inv == 0。即它非零。
|
|
|
|
- 约束4：limb_diff in range u16，即[0,2^16-1]。因为两个limb如果都属于u16，大的limb（下一行的）减小的limb（上一行的）的diff必然也是u16。反之，小的limb减大的limb的diff必然不是u16。
|
|
|
|
|
|
|
|
> RLC: zkevm-circuits/zkevm-circuits/src/state_circuit/random_linear_combination.rs
|
|
|
|
|
|
|
|
## 不同Tag对应的约束
|
|
|
|
还有其他约束。
|
|
|
|
|
|
|
|
首先，我们还需要一个变量叫`first_access`表示这个pointer的地方是否是第一次访问。其构造详情稍后详细描述。
|
|
|
|
|
|
|
|
对不同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。目前还没有涉及，详见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，则is_write=1. 即首次访问，必须是写。
|
|
|
|
- pointer_hi=0
|
|
|
|
- value_hi=0
|
|
|
|
|
|
|
|
first_access的表示可以用上述的first_diff_limb来判断。因为整个表格已经排好序了，如果first_diff_limb处于tag, callid, pointer hi, pointer lo中，意味着要么这一行和上一行的tag不同，要么callid不同，要么pointer不同。也意味着是首次访问。反之，非首次访问。
|
|
|
|
|
|
|
|
# 布局
|
|
|
|
state子电路基础的设计包含如下几列。注意，和LookupEntry的State基本一致。
|
|
|
|
```rust
|
|
|
|
pub struct StateCircuitConfig<F> {
|
|
|
|
q_enable: Selector,
|
|
|
|
/// Type of value, one of stack, memory, storage, call context, call data or return data
|
|
|
|
/// A `BinaryNumberConfig` can return the indicator by method `value_equals`
|
|
|
|
tag: BinaryNumberConfig<Tag, LOG_NUM_STATE_TAG>,
|
|
|
|
/// Stamp that increments for each state operation, unique for each row
|
|
|
|
stamp: Column<Advice>,
|
|
|
|
/// High 128-bit value of the row
|
|
|
|
value_hi: Column<Advice>,
|
|
|
|
/// Low 128-bit value of the row
|
|
|
|
value_lo: Column<Advice>,
|
|
|
|
/// Call id (other types) or contract address (storage type only)
|
|
|
|
call_id_contract_addr: Column<Advice>,
|
|
|
|
/// High 128-bit of the key (storage type only)
|
|
|
|
pointer_hi: Column<Advice>,
|
|
|
|
/// Low 128-bit of the key (storage type only) or call context tag
|
|
|
|
/// Or stack pointer or memory address or data index (call data and return data)
|
|
|
|
pointer_lo: Column<Advice>,
|
|
|
|
/// Whether it is write or read, binary value
|
|
|
|
is_write: Column<Advice>,
|
|
|
|
_marker: PhantomData<F>,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum Tag {
|
|
|
|
// in case for padding zeros, we make default = memory. memory read of unused pointer is 0.
|
|
|
|
#[default]
|
|
|
|
Memory,
|
|
|
|
Stack,
|
|
|
|
Storage,
|
|
|
|
CallContext,
|
|
|
|
CallData,
|
|
|
|
ReturnData,
|
|
|
|
EndPadding,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum CallContextTag {
|
|
|
|
#[default]
|
|
|
|
ParentCallId,
|
|
|
|
ParentCodeContractAddr,
|
|
|
|
ParentProgramCounter,
|
|
|
|
ParentStackPointer,
|
|
|
|
StorageContractAddr,
|
|
|
|
SenderAddr,
|
|
|
|
Value,
|
|
|
|
CallDataSize,
|
|
|
|
ReturnDataSize,
|
|
|
|
ReturnDataCallId,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
其中，tag我们没有简单的使用一个advice列，而是用了一个电路小工具名叫“BinaryNumberConfig/BinaryNumberChip”。它既可以表示一个tag，也可以当做动态选择器，用于启用约束。例如，我们想tag的值为stack(1)时启动约束1，为memory(0)时启动约束2。那么，示例代码如下
|
|
|
|
```rust
|
|
|
|
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](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
|
|
|
|
|
|
|
|
## 列的含义
|
|
|
|
|
|
|
|
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，再按callid, pointer hi, pointer lo, stamp的顺序排序。
|
|
|
|
|
|
|
|
在开发的代码中，例如Rust语言，排序十分简单。难的是在电路中增加约束保证整个Witness的行是符合排序规则的。参考scroll的电路，我们使用如下方法。
|
|
|
|
|
|
|
|
## 约束排序的方式
|
|
|
|
|
|
|
|
将tag, callid, pointer hi, pointer lo, stamp元组编码为16-bit的limbs，假设有L个limbs。（可以bit更大但是那样比较难做range proof）。上下两行的limbs作差，有L个diff。第一个非零的diff，index记为first_diff_limb。要求diff[first_diff_limb]也是16-bit数即可。因为如果排序的顺序反了，则diff[first_diff_limb]是小数减大数，在有限域上得到一个非常大的结果（2^255左右），必然不属于16-bit的数。
|
|
|
|
|
|
|
|
具体做法：
|
|
|
|
- 用BinaryNumberChip表示变量first_diff_limb。需要用log_2(L)个变量。
|
|
|
|
- 再定义变量limb_diff表示diff[first_diff_limb]。
|
|
|
|
- 再定义inv表示前者的逆。
|
|
|
|
- 约束1：建立一个expr数组v，是diff的累计RLC(random linear combination)：[0, diff[0], diff[0]+r diff[1], diff[0]+r diff[1]+r' diff[2]...]。约束sum \{first_diff_limb.value_equals(i) * v[i]\} == 0。即，前first_diff_limb是否都为0。sum是通过for循环取i=0..L得到的。注：value_equals(x)方法是BinaryNumberChip中用来判断值是否等于x的，若等于输出1，否则输出0。
|
|
|
|
注：也许可以把RLC改成^2。
|
|
|
|
- 约束2：sum \{first_diff_limb.value_equals(i) * diff[i]\} - limb_diff。即，limb_diff值是否按照定义等于diff[first_diff_limb]。sum是通过for循环取i=0..L得到的。
|
|
|
|
- 约束3：limb_diff存在inv。 1-limb_diff * inv == 0。即它非零。
|
|
|
|
- 约束4：limb_diff in range u16，即[0,2^16-1]。因为两个limb如果都属于u16，大的limb（下一行的）减小的limb（上一行的）的diff必然也是u16。反之，小的limb减大的limb的diff必然不是u16。
|
|
|
|
|
|
|
|
> 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。目前还没有涉及，详见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，则is_write=1. 即首次访问，必须是写。
|
|
|
|
- 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必须是0或1。 |
|
|
\ No newline at end of file |
