PSE zkEVM 规范

Super Circuit

zkEVM 由很多电路组成，每个负责验证 EVM 的某一方面，然后通过Super Circuit 将这些子电路组合起来，主要由以下circuits 和 tables 组成。

注： 还有其它一些子电路，例如 ECDSA电路，opcode 相关的电路，并没有在图上展示。

Bytecode 证明

bytecode 证明保证EVM中的字节码是可访问的，通过每个字节在字节码中的位置访问，还需要区分节码中的字节是否不是opcode 或者 PUSH 指令的数据。

Circuit 布局

tag 行用区分当前行和下一行不同的约束条件，主要有两个值：Header 和 Byte。 tag==Header 行之后会有一系列 tag==Byte 行。

列	描述
q_first	首行是1， 其它是0
q_last	最后一行是1， 其它是0
hash	字节码的keccak hash.
index	字节在字节码中的位置
value	对于Byte, 值为字节码的值，对于Header 值为长度
is_code	对于字节码值为1， 对于PUSH数据为0
push_data_left	PUSH 指令的数据部分剩作的部分
value_rlc	累加器，用于计算当前所有字节的RLC
length	字节码的长度
push_data_size	push指令数据的长度
push_table.byte	Push表的字节值
push_table.push_size	Push表的push指令数据长度

当所有的字节码添加之后， 剩余的行通过tag == Header && length == 0 && value == 0 && hash == EMPTY_HASH.

Push 表

Push表用于查找一个push指令数据长度，用于检测哪些字节是opcode, 哪些不是。

Byte	push的字节个数
[0, OpcodeId::PUSH1]	0
[OpcodeId::PUSH1, OpcodeId::PUSH32, ]	[1..32]
[OpcodeId::PUSH32, 256 ]	0

Witness 约束

电路的约束主要基于当前(cur)行和下一行(nex).

cur.q_first == 1 || cur.q_last == 1

若cur.q_first 或 cur.q_last 为1，则 cur.tag == Header.

约束条件主要基于cur.tag 或 next.tag：

若cur.tag==Header ，则在字节的起始位置，约束为：

assert cur.index == 0
assert cur.value == cur.length

若 cur.tag == Byte ，则处理字节码，约束为：

assert push_data_size_table_lookup(cur.value, cur.push_data_size)
assert cur.is_code == (cur.push_data_left == 0)

若cur.tag == Header and next.tag == Header, 则表示从一个空的字节码转移到另一个空的字节码：

assert cur.length == 0
assert cur.hash == EMPTY_HASH

若cur.tag == Header and next.tag == Byte:

则表示从头开始处理非空的字节码：

assert next.length == cur.length
assert next.index == 0
assert next.is_code == 1
assert next.hash == cur.hash
assert next.value_rlc == next.value

若cur.tag == Byte and next.tag == Byte， 则表示在处理中间的字节：

assert next.length == cur.length
assert next.index == cur.index  + 1
assert next.hash == cur.hash
assert next.value_rlc == cur.value_rlc * randomness + next.value
if cur.is_code:
    assert next.value_rlc == cur.value_rlc * randomness + next.value
else:
    assert next.push_data_left == cur.push_data_left - 1

其中index 是递增的，value_rlc 是累加值。

若cur.tag == Bytecode and next.tag == Header， 表示在处理字节码最后一个字节：

assert cur.index + 1 == cur.length
assert keccak256_table_lookup(cur.hash, cur.length, cur.value_rlc)

主要保证bytecode 长度和value_rlc值的准确性。

对于q_last == 1， 表示最后一行，约束条件为：

assert cur.length ==0
assert cur.hash == EMPTY_HASH

copy 证明

Copy 表主要包含以下13列：

• q_step: 1 表示读操作，0 表示写操作；
• is_first: 表示一次复制事件的第一行；
• is_last: 表示一次复制事件的最后一行；
• ID: RLC 编码的的txID, callID, codeHash；
• Type: 用于表示数据源的类型： Memory, Bytecode, TxCalldata, TxLog, RlcAcc;
• Address: 用于表示源数据的地址，可能是memory 地址， bytecode中的字节索引，tx calldata, tx log data; 当数据类型为 TxLog时，地址是由： byte index, TxLogFieldTag.Data, LogId 组合而成；
• AddressEnd: 表示源数据的地址边界，地址大于AddressEnd 的数据为0； AddressEnd只对读操作有效；
• BytesLeft: 剩余需要复制的数据；
• Value: 复制数据值；
• RlcAcc: 累加器值的RLC 表示；
• Pad: 表示来源的数据是填充的，只能读有效；
• isCode: 用于表示读在的value 是可执行代码或PUSH*操作的数据，只对 Bytecode 有效；
• RwCounter: 表明当前行的RW counter, 用于查找rw_table，只对Memory 或 TxLog 有效；
• RwcIncreaseLeft: 表明在在一个copy事件中，RW couter将增加的个数。

Copy 表是个虚拟表，lookup表的条目并不是表的一行，也不得每一行对应着一个查找表条目。每个copy 事件的前两行构造一个查找表条目：(is_first, ID, Type, ID[1], Type[1], Address, AddressEnd, Address[1], BytesLeft, RlcAcc, RwCounter, RwcIncrease), 其中 is_first 为1， Column[1] 对应着下一行。

Exp 证明

Exeponention 的实现算法为：

Function exp_by_squaring(x, n)
    if n = 0  then return  1;
    if n = 1  then return  x;
    if n is odd:
    return x * exp_by_squaring(x, n - 1)
    if n is even:
    return (exp_by_squaring(x, n / 2))^2

例如对于3 ^ 13 == 1594323 (mod 2^256) , 可以分解为以下的步骤：

3      * 3   = 9
9      * 3   = 27
27     * 27  = 729
729    * 729 = 531441
531441 * 3   = 1594323

Exponentiation 表由11列组成，即：

• is_step: 用于表示是否为exponentiation表的起始位置；
• identifier: exponentiation trace 的识别符；
• is_last: 用于表示exponentiation 的最后一行；
• base_limb[i]: exponentiation trace 表的赋值；
• exponent_lo_hi[i]: 两个128位的整数 exponent;
• exponentiation_lo_hi: 两个128位的 exponentation 操作；

对于 3 ^ 13 == 1594323 (mod 2^256)， exponentiation 表赋值为：

is_step	identifier	is_last	base_limb0	base_limb1	base_limb2	base_limb3	exponent_lo	exponent_hi	exponentiation_lo	exponentiation_hi
1	$rwc	0	3	0	0	0	13	0	1594323	0
1	$rwc	0	3	0	0	0	12	0	531441	0
1	$rwc	0	3	0	0	0	6	0	729	0
1	$rwc	0	3	0	0	0	3	0	27	0
1	$rwc	1	3	0	0	0	2	0	9	0

交易 证明

对于每个交易：(nonce, gas_price, gas, to, value, data, sig_v, sig_r, sig_s), 主要验证以下的条件：

1. txSignData: bytes = rlp([nonce, gas_price, gas, to, value, data, chain_id, 0, 0])
2. txSignHash: word = keccak(txSignData)
3. sig_parity: {0, 1} = sig_v - 35 - chain_id / 2
4. ecdsa_recover(txSignHash, sig_parity, sig_r, sig_s) = pubKey or equivalently verify(txSignHash, sig_r, sig_s, pubKey) = true
5. fromAddress = keccak(pubKey)[-20:]

交易表主要有以下的列：

• Nonce
• Gas
• GasPrice
• GasTipCap
• GasFeeCap
• CallerAddress
• CalleeAddress
• IsCreate
• Value
• CallDataLength
• TxSignHash

对于交易验证过程如下所示：

opcode

01ADD_03SUB

对于从栈上取出a 和 b，计算：

对于ADD 操作码，计算 c = ( a + b) % 2**256, 将c 压到栈上；

对于SUB 操作码，计算c = (a - b)% 2**256, 将c 压到栈上；

ADDGadget 对于输入的参数：a:[u8;32], x:[u8;32], y:[u8;32], is_sub，计算：

总是计算y= (a + x) % 2**256:

• 若为ADD, 栈为： [a,x, ....] 和 [y,...]；
• 若为SUB， 栈为[a,y,...] 和 [y,....]

约束条件

1. opcodeId 检查

   对于ADD, opId === OpcodeId(0x01) ；

   对于SUB， opId === OpcodeId(0x03);

2. 状态转移

   • gc + 3
   • Stack_pointer +1
   • pc + 1
   • gas + 3

3. Lookups: 3 个 busmapping lookups

   • a 在栈顶；
   • b 在栈的第二个位置；
   • c 为 栈计算的结果。

02MUL_04DIV_06MOD

取出栈上两个EVM words a 和 b， 将c 推到栈上， c 的计算方式为：

• 对于MUL， 计算 c = (a * b) % 2^256;
• 对于DIV， 计算 c = a // b, 其中 b != 0;
• 对于 MOD， 计算 c = a mod b, 其中 b != 0;

约束条件

1. OpcodeId 检查

   • 对于MUL，opId === OpcodeId (0x02)；
   • 对于DIV, opId === OpcodeId (0x04);
   • 对于MOD, opId === OpcodeId (0x06).

2. 状态转移

3. Lookups: 3 个 busmapping lookups

参考

https://privacy-scaling-explorations.github.io/zkevm-docs/

https://github.com/privacy-scaling-explorations/zkevm-specs