Polygon zkEVM Memory状态机

Posted 2022-09-09 mutourend

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 $\text{0xc417...81a7}$ 和 $\text{0x88d1...b723}$，相应的布局为：【每个word具有32字节，且以Big-Endian形式存储——即最高有效byte存储在更低的地址中】

$\mathbf{ADDRESS}$	$\mathbf{BYTE}$
$0$	$0xc4$
$1$	$0x17$
$⋮$	$⋮$
$30$	$0x81$
$31$	$0xa7$
$32$	$0x88$
$33$	$0xd1$
$⋮$	$⋮$
$62$	$0xb7$
$63$	$0x23$

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

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

• 1）MLOAD：按指定offset地址读取内存，返回32字节word。如上表中，MLOAD 1返回的为$\text{0x17...a788}$。

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

  $\mathbf{ADDRESS}$	$\mathbf{BYTE}$
  $0$	$0xc4$
  $1$	$\text{0x74}$
  $2$	$\text{0xf0}$
  $⋮$	$⋮$
  $31$	$\text{0xce}$
  $32$	$\text{0x92}$
  $33$	$0xd1$
  $⋮$	$⋮$
  $62$	$0xb7$
  $63$	$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状态机内的布局为：

$\text{ADDRESS}$	$\text{32-BYTE WORD}$
$0$	$0xc417...81a7$
$1$	$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字节）$\text{addr}$标记，指向32-byte word。word的值存储在内存中，以$\text{val}$标记，具体为8个4字节寄存器$\text{val[0..7]}$（256-bit）。

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

$\text{step}$	$\text{mOp}$	$\text{mWr}$	$\text{addr}$	$\text{val[7]}$	$\text{val[6]}$	$\dots$	$\text{val[0]}$
11	1	1	6	2121	3782	$\dots$	5432
31	1	1	4	3231	9326	$\dots$	8012
55	1	0	6	2121	3782	$\dots$	5432
63	1	1	6	4874	1725	$\dots$	2074
72	1	0	4	3231	9326	$\dots$	8012
89	1	1	2	9167	5291	$\dots$	6001

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

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

Memory状态机的trace必须检查：

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

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

$\text{step}$	$\text{addr}$	$\text{mOp}$	$\text{mWr}$	$\text{val[7]}$	$\text{val[6]}$	$\dots$	$\text{val[0]}$
89	2	1	1	9167	5291	$\dots$	6001
31	4	1	1	3231	9326	$\dots$	8012
72	4	1	0	3231	9326	$\dots$	8012
11	6	1	1	2121	3782	$\dots$	5432
55	6	1	0	2121	3782	$\dots$	5432
63	6	1	1	4674	1725	$\dots$	2074

Table 5: Corresponding Memory SM Execution Trace.

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

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

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

• 1）$\text{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）$\text{mOp}$和$\text{mWr}$仅能为0或1，且当且仅当$\text{mOp}$为1时，$\text{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，当${\text{mOp}}^{\prime }$和${\text{mWr}}^{\prime }$均为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
  以上是关于Polygon zkEVM Memory状态机的主要内容，如果未能解决你的问题，请参考以下文章
   
   Polygon zkEVM可验证计算简单状态机示例
   Polygon zkEVM Arithmetic状态机
   Polygon zkEVM Binary状态机
   Polygon zkEVM哈希状态机——Keccak-256和Poseidon
   Polygon zkEVM的pil-stark Fibonacci状态机代码解析
   Polygon zkEVM的pil-stark Fibonacci状态机初体验