appliedzkp的zkevm（3）Word Encoding

1. 引言

在EVM中，每个word对应256个bit。在zkevm中，对word的encode方式有所不同：

• 为random linear combination of 8 bit words

这种编码方式有助于使用plookup来表达Arithmetic、Bitwise oprations和Comparators。而stack和memory不需要关注该编码方式，因为stack和memory仅需处理commitments值。

将256 bit 拆分为 8 bit chunks主要基于以下2方面考虑：

• 1）使用的BN254曲线。BN254曲线的最大值可以254 bit表示，所有的arithmetic都是对254 bit素数取模完成。
• 2）通过plookups来进行conditional checks和bitwise operations。 2 25 2^{25} 225行的size限制了需要work in smaller chunks of the word。在plookup中需要做多项式除法。Plonk prover使用FFT来高效实现多项式触发。BN254曲线支持的最大FFT size为 2 28 2^{28} 228。某些需要常量开销和自定义约束。因此，限制了多项式最大degree为 2 25 2^{25} 225。

2. Word编码举例（Endianness）

将256 bit word以little endian编码。 如对于256 bit的value 1：

word256 = 1

将word256变量切分为32个8 bit words表示：

word8s = [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]

3. Commitment

该256 bit表示为其8 bit words的random linear combination。 该commitment check应保证该32 chunks in 8 bit range。

4. Addition

验证a256 + b256 = c256。支持overflow来匹配EVM behavior。 如：

a8s    ff 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0
b8s     2 1 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0
carry     1 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 0
sum8s   1 2 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0 | 0 0 0 0 0 0 0 0

a8s    ff ff ff ff ff ff ff ff | ff ff ff ff ff ff ff ff | ff ff ff ff ff ff ff ff | ff ff ff ff ff ff ff ff
b8s     2  0  0  0  0  0  0  0 |  0  0  0  0  0  0  0  0 |  0  0  0  0  0  0  0  0 |  0  0  0  0  0  0  0  0
carry      1  1  1  1  1  1  1 |  1  1  1  1  1  1  1  1 |  1  1  1  1  1  1  1  1 |  1  1  1  1  1  1  1  1  1
sum8s   1  0  0  0  0  0  0  0 |  0  0  0  0  0  0  0  0 |  0  0  0  0  0  0  0  0 |  0  0  0  0  0  0  0  0

5. Comparator

会检查如下关系：

• a256 > b256
• a256 < b256
• a256 == b256

将8 bit chunks group为 16 bit chunks来优化该table。 该result会carry the conclusion of the comparision from the higher significant chunks all the way down。 如：

a       1 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 1 0 0 |
b       1 0 0 0 | 0 0 0 0 | 0 0 0 0 | 0 0 0 0 |
result  1 1 1 1 | 1 1 1 1 | 1 1 1 1 | 1 1 0 0 |

6. Comparator Take 4

# This value is determined by the curve we use
FIELD_SIZE = 2**254 # 为SCALAR_FIELD_SIZE

class SignTable:
    """
    x: 18 bits signed ( -(2**17 - 1) to 2**17 - 1)
    sign: 2 bits (0, -1, 1)
    (1 column and 2**18 - 1 rows)
    """
    def __init__(self):
        self.rows = []
        self.rows.append({"x": 0, "sign": 0})
        for x in range(1, 2**17):
            self.rows.append({"x": x, "sign": 1})
            self.rows.append({"x": -x + FIELD_SIZE, "sign": -1})
                
    def lookup(self, diff: int, sign: int) -> bool:
        """Returns True if the row exists in the table"""
        ...

def compare(
        a8s: Sequence[U8],
        b8s: Sequence[U8],
        result: Sequence[int],
    ) -> int:
    """
    returns -1 if a < b
             0 if a == b
             1 if a > b
    """
    assert len(a8s) == len(b8s) == 32
    assert len(result) == 16
    
    # Before we do any comparison, the previous result is "equal" 
    result = result[:] + [0]

    for i in reversed(range(0, 32, 2)):
        a16 = a8s[i] + 256 * a8s[i + 1]
        b16 = b8s[i] + 256 * b8s[i + 1]
    
        diff = (a16 - b16) % FIELD_SIZE
        previous, current = result[i//2+1], result[i//2]
        require(
            SignTable.lookup((diff + 2**16 * previous) % FIELD_SIZE, current)
        )

    return result[0]

previous会影响当前lookup结果。previous=0表示仅由diff决定result。 对于u256比较，需16次linear combination和16次lookup。 具体举例为：

参考资料

[1] https://hackmd.io/HfCsKWfWRT-B_k5j3LjIVw [2] https://hackmd.io/QUiYS3MnTu29s62yg9EtLQ [3] https://hackmd.io/6jzBI4nmRR-JvSG2TFHrDw [4] zkEVM-specs Word Encoding