| ... | @@ -23,7 +23,34 @@ pub struct StateCircuitConfig<F> { | 
... | @@ -23,7 +23,34 @@ pub struct StateCircuitConfig<F> { | 
| 
 | 
    is_write: Column<Advice>,
 | 
 | 
    is_write: Column<Advice>,
 | 
| 
 | 
    _marker: PhantomData<F>,
 | 
 | 
    _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。那么,示例代码如下
 | 
 | 
其中,tag我们没有简单的使用一个advice列,而是用了一个电路小工具名叫“BinaryNumberConfig/BinaryNumberChip”。它既可以表示一个tag,也可以当做动态选择器,用于启用约束。例如,我们想tag的值为stack(1)时启动约束1,为memory(0)时启动约束2。那么,示例代码如下
 | 
| 
 | 
```rust
 | 
 | 
```rust
 | 
| 
 | 
let condition_1 = tag.value_equals(1);
 | 
 | 
let condition_1 = tag.value_equals(1);
 | 
| ... | @@ -32,6 +59,44 @@ vec![condition_1 * constraint_1, condition_2 * constraint_2] | 
... | @@ -32,6 +59,44 @@ vec![condition_1 * constraint_1, condition_2 * constraint_2] | 
| 
 | 
```
 | 
 | 
```
 | 
| 
 | 
关于BinaryNumberChip,详见[here](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
 | 
 | 
关于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
 | 
 | 
 | 
 | 
- 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的顺序排序。
 | 
 | 
为了保证读写一致性,我们需要排序,按照如下顺序排序的:先按tag,再按callid, pointer hi, pointer lo, stamp的顺序排序。
 | 
| ... | @@ -46,9 +111,9 @@ vec![condition_1 * constraint_1, condition_2 * constraint_2] | 
... | @@ -46,9 +111,9 @@ vec![condition_1 * constraint_1, condition_2 * constraint_2] | 
| 
 | 
- 用BinaryNumberChip表示变量first_diff_limb。需要用log_2(L)个变量。
 | 
 | 
- 用BinaryNumberChip表示变量first_diff_limb。需要用log_2(L)个变量。
 | 
| 
 | 
- 再定义变量limb_diff表示diff[first_diff_limb]。
 | 
 | 
- 再定义变量limb_diff表示diff[first_diff_limb]。
 | 
| 
 | 
- 再定义inv表示前者的逆。				
 | 
 | 
- 再定义inv表示前者的逆。				
 | 
| 
 | 
- 约束1:建立一个expr数组v,是diff的累计RLC:[0, diff[0], diff[0]+r diff[1], diff[0]+r diff[1]+r' diff[2]...]。约束first_diff_limb.value_equals(i) * v[i] == 0。即,前first_diff_limb是否都为0。注:value_equals(x)方法是BinaryNumberChip中用来判断值是否等于x的,若等于输出1,否则输出0。				
 | 
 | 
- 约束1:建立一个expr数组v,是diff的累计RLC:[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				
 | 
 | 
注:也许可以把RLC改成^2。		
 | 
| 
 | 
- 约束2:first_diff_limb.value_equals(i) * diff[i] - limb_diff。即,limb_diff值是否按照定义等于diff[first_diff_limb]。				
 | 
 | 
- 约束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。即它非零。
 | 
 | 
- 约束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。
 | 
 | 
- 约束4:limb_diff in range u16,即[0,2^16-1]。因为两个limb如果都属于u16,大的limb(下一行的)减小的limb(上一行的)的diff必然也是u16。反之,小的limb减大的limb的diff必然不是u16。
 | 
| 
 | 
 | 
 | 
 | 
| ... | @@ -80,4 +145,6 @@ vec![condition_1 * constraint_1, condition_2 * constraint_2] | 
... | @@ -80,4 +145,6 @@ vec![condition_1 * constraint_1, condition_2 * constraint_2] | 
| 
 | 
  - pointer_hi=0
 | 
 | 
  - pointer_hi=0
 | 
| 
 | 
  - value_hi=0
 | 
 | 
  - value_hi=0
 | 
| 
 | 
 | 
 | 
 | 
| 
 | 
first_access的表示可以用上述的first_diff_limb来判断。因为整个表格已经排好序了,如果first_diff_limb处于tag, callid, pointer hi, pointer lo中,意味着要么这一行和上一行的tag不同,要么callid不同,要么pointer不同。也意味着是首次访问。反之,非首次访问。 | 
 | 
first_access的表示可以用上述的first_diff_limb来判断。因为整个表格已经排好序了,如果first_diff_limb处于tag, callid, pointer hi, pointer lo中,意味着要么这一行和上一行的tag不同,要么callid不同,要么pointer不同。也意味着是首次访问。反之,非首次访问。
 | 
 | 
\ No newline at end of file | 
 | 
 | 
 | 
 | 
 | 
还有一个约束,is_write必须是0或1。 | 
 | 
 | 
 | 
\ No newline at end of file |