| ... | ... | @@ -113,12 +113,14 @@ Tag不同，含义不同，如下。 |
|
|
|
- 用BinaryNumberChip表示变量first_diff_limb。需要用log_2(L)个变量。
|
|
|
|
- 再定义变量limb_diff表示diff[first_diff_limb]。
|
|
|
|
- 再定义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。
|
|
|
|
- 约束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对应的约束
|
|
|
|
还有其他约束。
|
|
|
|
|
| ... | ... | |
