... | @@ -113,12 +113,14 @@ Tag不同,含义不同,如下。 |
... | @@ -113,12 +113,14 @@ Tag不同,含义不同,如下。 |
|
- 用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]...]。约束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。
|
|
- 约束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。
|
|
注:也许可以把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得到的。
|
|
- 约束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。
|
|
|
|
|
|
|
|
> RLC: zkevm-circuits/zkevm-circuits/src/state_circuit/random_linear_combination.rs
|
|
|
|
|
|
## 不同Tag对应的约束
|
|
## 不同Tag对应的约束
|
|
还有其他约束。
|
|
还有其他约束。
|
|
|
|
|
... | | ... | |