Polygon zkEVM Memory状态机

1. 引言

前序博客有：

Polygon zkEVM Arithmetic状态机
Polygon zkEVM中的常量多项式
Polygon zkEVM Binary状态机

Memory状态机为Polygon zkEVM的六个二级状态机之一，该状态机内包含：

executor part：sm_mem.js：负责生成execution trace，为常量多项式和隐私多项式赋值。
验证规则集PIL：mem.pil：定义了约束系统，检查that memory reads and writes aligned to 32-byte words are correct。

以太坊虚拟机的memory为可变读写内存，用于存储执行智能合约交易函数中的临时数据。在交易执行过程中，内存中的数据是存续的，但是内存中的数据无法跨交易存续。以太坊虚拟机内的memory为一组256-bit（32字节）words，可通过addresses以byte level访问，即内存中的每个字节具有不同的地址。

memory具有32-bit地址，初始状态为内存中的所有位置均为0 byte set。

假设内存中有2个word 0xc417...81a7 \texttt{0xc417...81a7} 0xc417...81a7 和 0x88d1...b723 \texttt{0x88d1...b723} 0x88d1...b723，相应的布局为：【每个word具有32字节，且以Big-Endian形式存储——即最高有效byte存储在更低的地址中】

A D D R E S S \mathbf{ADDRESS} ADDRESS B Y T E \mathbf{BYTE} BYTE 0 \mathtt{0} 0 0 x c 4 \mathtt{0xc4} 0xc4 1 \mathtt{1} 1 0 x 17 \mathtt{0x17} 0x17 ⋮ \mathtt{\vdots} ⋮ ⋮ \mathtt{\vdots} ⋮ 30 \mathtt{30} 30 0 x 81 \mathtt{0x81} 0x81 31 \mathtt{31} 31 0 x a 7 \mathtt{0xa7} 0xa7 32 \mathtt{32} 32 0 x 88 \mathtt{0x88} 0x88 33 \mathtt{33} 33 0 x d 1 \mathtt{0xd1} 0xd1 ⋮ \mathtt{\vdots} ⋮ ⋮ \mathtt{\vdots} ⋮ 62 \mathtt{62} 62 0 x b 7 \mathtt{0xb7} 0xb7 63 \mathtt{63} 63 0 x 23 \mathtt{0x23} 0x23

Table 1: Layout in memory of 0xc417...81a7 and 0x88d1...b723.

EVM提供了3个opcode来与内存交互：

1）MLOAD：按指定offset地址读取内存，返回32字节word。如上表中，MLOAD 1返回的为 0x17...a788 \texttt{0x17...a788} 0x17...a788。
2）MSTORE：按指定offset地址存储32byte。如上表中，MSTORE 1 0x74f0...ce92$,，会修改内存中的数据为：【若offset不是32（0x20）的倍数，则返回的结果会跨不同的word。】

A D D R E S S \mathbf{ADDRESS} ADDRESS B Y T E \mathbf{BYTE} BYTE 0 \mathtt{0} 0 0 x c 4 \mathtt{0xc4} 0xc4 1 \mathtt{1} 1 0x74 \mathtt{\textbf{0x74}} 0x74 2 \mathtt{2} 2 0xf0 \mathtt{\textbf{0xf0}} 0xf0 ⋮ \mathtt{\vdots} ⋮ ⋮ \mathtt{\vdots} ⋮ 31 \mathtt{31} 31 0xce \mathtt{\textbf{0xce}} 0xce 32 \mathtt{32} 32 0x92 \mathtt{\textbf{0x92}} 0x92 33 \mathtt{33} 33 0 x d 1 \mathtt{0xd1} 0xd1 ⋮ \mathtt{\vdots} ⋮ ⋮ \mathtt{\vdots} ⋮ 62 \mathtt{62} 62 0 x b 7 \mathtt{0xb7} 0xb7 63 \mathtt{63} 63 0 x 23 \mathtt{0x23} 0x23
Table 2: Layout in memory after the introduction of 0x74f0...ce92.
3）MSTOREE：将某byte数据存入指定offset地址。【注意，MSTOREE为按单个byte写入。】

2. Memory状态机布局

Memory状态机负责证明execution trace中的内存操作。如上所述，通过使用地址来实现EVM中的byte级别的读写操作。但是，若进行逐字节证明，将消耗状态机trace内大量的值，因此，在Polygon zkEVM的Memory状态机中，是按word（32字节）进行操作的。

如，在Memory状态机内的布局为：

ADDRESS \textbf{ADDRESS} ADDRESS 32-BYTE WORD \textbf{32-BYTE WORD} 32-BYTE WORD 0 \mathtt{0} 0 0 x c 417...81 a 7 \mathtt{0xc417...81a7} 0xc417...81a7 1 \mathtt{1} 1 0 x 88 d 1... b 723 \mathtt{0x88d1...b723} 0x88d1...b723

Table 3: Layout in the memory state machine.

Polygon zkEVM的Memory状态机通过访问32字节word来进行读写。但是，由于实际EVM也支持a byte级别的读写，因此，需要检查byte access和32-byte access之间的关系，为此，需要引入名为Memory Align的状态机。

3. Memory状态机Execution Trace设计

sm_mem.js：负责生成execution trace，为常量多项式和隐私多项式赋值。

内存中的地址，以32-bit （4字节） addr \texttt{addr} addr标记，指向32-byte word。word的值存储在内存中，以 val \texttt{val} val标记，具体为8个4字节寄存器 val[0..7] \texttt{val[0..7]} val[0..7]（256-bit）。

以下为Main状态机execution trace中包含的内存操作：

step \texttt{step} step mOp \texttt{mOp} mOp mWr \texttt{mWr} mWr addr \texttt{addr} addr val[7] \texttt{val[7]} val[7] val[6] \texttt{val[6]} val[6] … \dots … val[0] \texttt{val[0]} val[0]1111621213782 … \dots …54323111432319326 … \dots …80125510621213782 … \dots …54326311648741725 … \dots …20747210432319326 … \dots …80128911291675291 … \dots …6001

Table 4: Memory Operations and an Execution Trace of the Main SM.

上例中， step \texttt{step} step为Main状态机中的execution step number，仅显示了执行内存操作的step，通过 mOp \texttt{mOp} mOp selector来标记是否为内存操作，通过 mWr \texttt{mWr} mWr来标记是内存读操作还是内存写操作。【注意，对特定内存地址通常是先有写操作，后续的读操作才有意义。即意味着若先有读操作，相应地址值应为初始化0值。】

Memory状态机的trace必须检查：

1）在相应step写入了正确的值；
2）在相应step读取了正确的值。

为了完成以上检查，Memory状态机的execution trace必须对所有内存操作进行排序：首先按 addr \texttt{addr} addr升序排列，然后按 step \texttt{step} step升序排列，具体如下表所示：

step \texttt{step} step addr \texttt{addr} addr mOp \texttt{mOp} mOp mWr \texttt{mWr} mWr val[7] \texttt{val[7]} val[7] val[6] \texttt{val[6]} val[6] … \dots … val[0] \texttt{val[0]} val[0]8921191675291 … \dots …60013141132319326 … \dots …80127241032319326 … \dots …80121161121213782 … \dots …54325561021213782 … \dots …54326361146741725 … \dots …2074

Table 5: Corresponding Memory SM Execution Trace.

最后，为了证明Memory状态机内的execution trace 与 Main状态机的读写顺序是一致的（写入操作存入指定的值；读取操作不更改值），需额外加入一些辅助列（多项式）。为此，Polygon zkEVM Memory状态机中额外加入了3列：

1） INCS \texttt{INCS} INCS：用于提供列中值的顺序。
2） lastAccess \texttt{lastAccess} lastAccess：用于启用地址更改，表示trace中当前地址的所有内存操作已完成。
3） ISNOTLAST \texttt{ISNOTLAST} ISNOTLAST：用于标记检查通过，没有任何内存访问操作了。

4. Memory状态机中的约束系统

mem.pil中多项式有：

	pol constant INCS; // 1......N
    pol constant ISNOTLAST; // 1, 1, 1, .........1, 1, 0

    pol commit addr;
    pol commit step;
    pol commit mOp, mWr;
    pol commit val[8];
    pol commit lastAccess; // 1 if its the last access of a given address

其中：

1） INCS \texttt{INCS} INCS常量多项式：赋值为 ( 1 , 2 , 3 , ⋯ , N − 1 , N ) (1,2,3,\cdots, N-1,N) (1,2,3,⋯,N−1,N)，表示 computational trace中的行号，用于做range check，以证明the incremental order of other columns。
2） ISNOTLAST \texttt{ISNOTLAST} ISNOTLAST常量多项式：最后一个值为0，其它所有值均为1。
3） step \texttt{step} step隐私多项式：表示在Main状态机中该内存操作所发生的位置。
4） mOp \texttt{mOp} mOp隐私多项式：为selector，用于标记是否执行了内存操作。
5） mWr \texttt{mWr} mWr隐私多项式：为selector，1表示内存写操作，0表示内存读操作。
6） addr \texttt{addr} addr隐私多项式：为4字节（32-bit）整数，表示32-byte word地址。
7） lastAccess \texttt{lastAccess} lastAccess隐私多项式：为selector，用于表示某特定地址是否已到达最后的内存访问操作。【// The list is sorted by [addr, step]】
8） val[0..7] \texttt{val[0..7]} val[0..7]共8个隐私多项式：该系列中包含了8个4字节整数，用于表示某特定地址的256-bit值。

Memory状态机内的约束有：【Memory状态机的execution trace必须对所有内存操作进行排序：首先按 addr \texttt{addr} addr升序排序，然后按 step \texttt{step} step升序排序。】

1） lastAccess \texttt{lastAccess} lastAccess的值仅能为0或1：
```
lastAccess * (lastAccess - 1) = 0;
```
2）最后一行除外，当last_access=0即对应同一addr时（有(1 - lastAccess) * (addr' - addr) = 0），step应是升序排列的，有step'-step in INCS；当last_access=1即表示下一行为不同addr时，addr应是升序排列的，有addr'-addr in INCS；且对于最后一行，last_access必须为1，具体表示为：
```
ISNOTLAST { lastAccess*(  addr' - addr - (step'-step) )  +   (step'-step) } in INCS;
(1 - lastAccess) * (addr' - addr) = 0;

// lastAccess has to be 1 in the last evaluation. This is necessary to
// validate [rdDifferent * (val[0]') = 0;] correctly (in a cyclic way)
(lastAccess - 1) * (1 - ISNOTLAST) = 0;
```
3） mOp \texttt{mOp} mOp和 mWr \texttt{mWr} mWr仅能为0或1，且当且仅当 mOp \texttt{mOp} mOp为1时， mWr \texttt{mWr} mWr才能为1：
```
mOp * (mOp -1) = 0;
mWr * (mWr -1) = 0;
// mWr could be 1 only if mOp is 1
(1 - mOp) * mWr = 0;
```
4）引入中间变量isWrite，当 mOp ′ \texttt{mOp}' mOp′和 mWr ′ \texttt{mWr}' mWr′均为1时，isWrite=1，表示（下一行为）内存写操作；否则，isWrite=0表示（下一行为）内存读操作。当（下一行为）读操作时，若lastAccess=1表示当前行为当前addr的最后一次内存访问，引入中间变量rdSame=(1-mOp' * mWr') * (1-lastAccess)表示（下一行）该地址的值将保持不变；引入中间变量rdDifferent=(1-mOp' * mWr') * lastAccess，表示将开启新的cycle，若（下一行）为针对新addr的第一个操作为读操作，即意味着新cycle该地址值初始化值应为0：【注意，对特定内存地址通常是先有写操作，后续的读操作才有意义。即意味着若先有读操作，相应地址值应为初始化0值。】
```
pol isWrite = mOp' * mWr';
pol rdSame = (1-isWrite) * (1-lastAccess);
pol rdDifferent = (1-isWrite) * lastAccess;

rdSame * (val[0]' - val[0])  =  0;
rdSame * (val[1]' - val[1])  =  0;
rdSame * (val[2]' - val[2])  =  0;
rdSame * (val[3]' - val[3])  =  0;
rdSame * (val[4]' - val[4])  =  0;
rdSame * (val[5]' - val[5])  =  0;
rdSame * (val[6]' - val[6])  =  0;
rdSame * (val[7]' - val[7])  =  0;

// The first evaluation is successfully validated when the evaluation cycle is restarted
rdDifferent * (val[0]')  =  0;
rdDifferent * (val[1]')  =  0;
rdDifferent * (val[2]')  =  0;
rdDifferent * (val[3]')  =  0;
rdDifferent * (val[4]')  =  0;
rdDifferent * (val[5]')  =  0;
rdDifferent * (val[6]')  =  0;
rdDifferent * (val[7]')  =  0;
```

以zkevm-proverjs/test/sm/sm_mem_test.js为例，相应的execution trace为：

Memory executor i=0 addr=10 step=1 mOp=1 mWr=1 val=0:0:0:0:0:0:0:70 lastAccess=0
Memory executor i=1 addr=10 step=2 mOp=1 mWr=0 val=0:0:0:0:0:0:0:70 lastAccess=0
Memory executor i=2 addr=10 step=3 mOp=1 mWr=1 val=0:0:0:0:0:0:0:80 lastAccess=0
Memory executor i=3 addr=10 step=10 mOp=1 mWr=0 val=0:0:0:0:0:0:0:80 lastAccess=0
Memory executor i=4 addr=10 step=12 mOp=1 mWr=0 val=0:0:0:0:0:0:0:80 lastAccess=1
Memory executor i=5 addr=40 step=4 mOp=1 mWr=1 val=0:0:0:0:0:0:0:1000 lastAccess=0
Memory executor i=6 addr=40 step=5 mOp=1 mWr=1 val=0:0:0:0:0:0:0:1001 lastAccess=0
Memory executor i=7 addr=40 step=8 mOp=1 mWr=0 val=0:0:0:0:0:0:0:1001 lastAccess=0
Memory executor i=8 addr=40 step=11 mOp=1 mWr=1 val=0:0:0:0:0:0:0:1002 lastAccess=0
Memory executor i=9 addr=40 step=18 mOp=1 mWr=1 val=0:0:0:0:0:0:0:1003 lastAccess=1

参考资料

[1] Memory State Machine

附录：Polygon Hermez 2.0 zkEVM系列博客

ZK-Rollups工作原理
Polygon zkEVM——Hermez 2.0简介
Polygon zkEVM网络节点
Polygon zkEVM 基本概念
Polygon zkEVM Prover
Polygon zkEVM工具——PIL和CIRCOM
Polygon zkEVM节点代码解析
Polygon zkEVM的pil-stark Fibonacci状态机初体验
Polygon zkEVM的pil-stark Fibonacci状态机代码解析
Polygon zkEVM PIL编译器——pilcom 代码解析
Polygon zkEVM Arithmetic状态机
Polygon zkEVM中的常量多项式
Polygon zkEVM Binary状态机

Polygon zkEVM Memory状态机

最近更新

热门博客

[ 申请 ]友情链接：