|
|
TODO
|
|
TODO
|
|
|
|
|
|
|
|
排序：在当做电路的输入之前，需要将这个table排序。按元组排序：先按tag，再按callid, pointer hi, pointer, stamp的顺序排序。
|
|
|
|
|
|
|
|
|
|
|
|
验证排序的方式：将元组编码为16bit的limbs，假设有L个。（可以bit更大但是那样比较难做range proof）。上下两行的limbs作差，有L个diff。第一个非零的diff，index记为first_diff_limb。要求diff[first_diff_limb]==0即可。
|
|
|
|
|
|
|
|
|
|
|
|
具体做法：用binary表示first_diff_limb. 需要用log_2 L个变量。再定义变量limb_diff表示diff[first_diff_limb]。再定义inv表示前者的逆。
|
|
|
|
约束1：建立一个expr数组v，是diff的累计RLC：[diff[0], diff[0]+r diff[1], diff[0]+r diff[1]+r' diff[2]...]。约束first_diff_limb.equal(i) * v[i] == 0。即，前first_diff_limb是否都为0。注：equal是binary表示的一种工具。
|
|
|
|
注：也许可以把RLC改成^2
|
|
|
|
约束2：first_diff_limb.equal(i) * diff[i] - limb_diff。即，limb_diff值是否正确
|
|
|
|
约束3：limb_diff存在inv. 1-limb_diff * inv == 0。即它非零
|
|
|
|
约束4：limb_diff in range u16 |
|
|
|
\ No newline at end of file |
