zkEVM Word encoding 资料

[yz89]

PSE 的 zkEVM 电路中使用BN254曲线，而BN254曲线所能表示的最大数字是254位，即所有算术运算都是对254位素数取模完成的。所以一个 EVM word(256 bit) 无法assign 到 halo2 一个 cell 中，也无法直接做 range check，需要做 decompose 处理。

以下是 PSE zkEVM 的 word encoding 设计及 scroll 团队的代码实现。

docs:
zkevm-specs，
PSE zkvmbook

code：
https://github.com/scroll-tech/zkevm-circuits/blob/b3db7f095b/gadgets/src/evm_word.rs

[yz89]

关于 zkevm 中 ADD_SUB 计算的约束

由于BN254限制，无法直接计算2个word 加法。PSE zkEVM 在约束加法操作时，将一个 word 拆分成2个128bit 的值，然后结合 carry 部分分别约束。

code：
https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/main/zkevm-circuits/src/evm_circuit/util/math_gadget/add_words.rs#L51

---

关于约束，以下是一个 u16 以大端序表示的简单的例子。

ADD_SUB Constrain:

sum(addends_lo) == sum_lo + carry_lo ⋅ 2^128
sum(addends_hi) + carry_lo == sum_hi + carry_hi ⋅ 2^128

Example 1:

a16 0x00 | 0xff // 255
b16 0x01 | 0x02 // 258
carry 0x00 | 0x01
c16 0x02 | 0x01

lo:
0x00ff + 0x0002 = 0x0001 + 0x01 << 8
0x0101 = 0x0101

hi:
0x00 + 0x01 + 0x01 = 0x02 + 0x00 << 8
0x02 = 0x02

---

Example 2:

a16 0xff | 0xff
b16 0x01 | 0x02
carry 0x01 | 0x01
sum 0x01 | 0x01 (0x010101)

lo:
0xff + 0x02 = 0x01 + 0x01 << 8
0x0101 = 0x0101

hi:
0xff + 0x01 + 0x01 = 0x01 + 0x01 << 8
0x0101 = 0x0101