| ... | ... | @@ -183,8 +183,16 @@ CONCAT_RLC = R^5 RLC[0] + R^4 RLC[1] + R^3 RLC[2] + R^2 RLC[3] + R^1 RLC[4] + RL |
|
|
|
|
|
|
|
解决方法：上述的value都是在U128范围内的，因此，原来table的一个数值可以变为16个u8数值。那么原来table的一列就要新建一列，原来的一列中的一行的value，在新列中要占用16行。
|
|
|
|
|
|
|
|
再新建一列ring_16，以15,14...1,0这样循环。在ring_16==0时，对新列中16行和原来列的1行的value进行约束，证明16个u8拼成了一个value。
|
|
|
|
~~再新建一列ring_16，以15,14...1,0这样循环。在ring_16==0时，对新列中16行和原来列的1行的value进行约束，证明16个u8拼成了一个value。~~
|
|
|
|
|
|
|
|
这样，原来table的两行之间，要插入15行的填充行，填充行没有任何意义。lookup也要加上ring_16，且lookup时ring_16=0。
|
|
|
|
当Tag 不是Nil时，不是TxCalldata，不是TxLogData时，我们要约束Rotation 0到-15的行，约束1：他们的Tag要是Nil（除了当前行）。约束2：16行的16个u8拼成了一个value。
|
|
|
|
|
|
|
|
我们原来table有6列，因此需要进行6次这样的操作。 |
|
|
\ No newline at end of file |
|
|
|
这样，原来table的两行之间，要插入15行的填充行（tag为Nil），填充行在value的地方没有任何意义，只在u8的地方有意义。~~lookup也要加上ring_16，且lookup时ring_16=0。~~
|
|
|
|
|
|
|
|
当Tag是 TxCalldata 或 TxLogData 时，因为每一行之间有大量重复数据，例如Tag、block_tx_idx、value_3都是相同的，因此仅对于第一行（idx==0），进行类似约束：约束Rotation 0到-15的行，约束1：他们的Tag要是Nil（除了当前行）。约束2：16行的16个u8拼成了一个value。
|
|
|
|
|
|
|
|
对于第二行及以后（idx!=0），仅对于Rotation 0的行约束，约束byte（本来就是u8）等于相应的u8那列的值。同时还要约束tag等于tag_prev，idx=idx_prev+1等等。
|
|
|
|
|
|
|
|
这样，原来table的idx==0的行上边，要插入15行的填充行（tag为Nil）。idx!=0的行上边，不需要插入。
|
|
|
|
|
|
|
|
我们原来table有6列，因此对于每列，都要进行这样的约束。 |
|
|
\ No newline at end of file |
