Polygon zkEVM Memory Align状态机

Posted 2022-09-09 mutourend

1. 引言

前序博客有：

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

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

• executor part：sm_mem_align.js：负责生成execution trace，为常量多项式和隐私多项式赋值。
• 验证规则集PIL：mem_align.pil：定义了约束系统。

Polygon zkEVM Memory状态机通过使用a 32-byte word access来检查内存读写，而EVM支持对单个byte级别的offset进行读写。

如下图，分别表示了相同内容在 byte级别 和 32-byte级别的内存布局：

Table 7: Sample memory layouts for byte and 32-byte access.

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

$$\begin{array}{cc}\text{ADDRESS}& \text{32-BYTE WORD}\\ 0& 0xc417...81a7\\ 1& 0x88d1...b723\end{array}$$

32-byte与byte级别布局之间的关系称为“memory alignment”，而Memory Align状态机负责检查二者之间关系的正确性。

EVM支持3种内存操作：

• 1）MLOAD：按指定offset地址读取内存，返回内存中自该offset开始的32字节word。【注意，MLOAD可读取2个不同words的bytes。】【对应zkasm中的MEM_ALIGN_WR】
• 2）MSTORE：按指定offset地址存储32byte。【对应zkasm中的MEM_ALIGN_RD】
• 3）MSTOREE：将某单个byte数据存入指定offset地址。【注意，MSTOREE为按单个byte写入。】【对应zkasm中的MEM_ALIGN_WR8】

EVM是按byte级别操作的，仍以上表为例，对应2个word：
$${\mathtt{m}}_0=0x88d11f\cdots b723,{\mathtt{m}}_1=0x6e21ff\cdots 54f9.$$
当MLOAD 0x22时，返回的结果为：
$$\mathtt{val}=0x1f\cdots b7236e21.$$
跨越了2个word，将该读操作的结果标记为：${\mathtt{m}}_0\mid {\mathtt{m}}_1$：

验证MLOAD 0x22返回的结果$0x1f\cdots 7236e21$是否正确的流程为：

• 1）Main状态机需查询获得${\mathtt{m}}_0$ 和 ${\mathtt{m}}_1$值；
• 2）Main状态机需调用Memory状态机来验证所查询的结果有效；
• 3）Main状态机可很容易extract the memory positions to query from the address 0x22。事实上，若$a$为MLOAD操作的内存位置，则${\mathtt{m}}_0$总是存储在内存位置$\lfloor \frac{a}{32}\rfloor$ 且 ${\mathtt{m}}_1$ 存储在内存位置$\lfloor \frac{a}{32}\rfloor +1$。本例中 $a=0x22=34$，从而 ${\mathtt{m}}_0$ 存储在位置$\lfloor \frac{32}{34}\rfloor =0x01$ 且 ${\mathtt{m}}_1$ 存储在位置 $\lfloor \frac{32}{34}\rfloor +1=0x02$。
• 4）应从正确的offset提取，offset应为0-31的index，表示从${\mathtt{m}}_0$的读取$\mathtt{val}$的偏移位置。如本例中，offset为2（即offset为 $a\mathrm{mod}32$）。可借助Plookup来验证已知${\mathtt{m}}_0,{\mathtt{m}}_1$和$\mathtt{offset}$，所读取的$\mathtt{val}$值是正确的。

同理，对于$\mathtt{MSTORE}$为write bytes in two words。假设${\mathtt{w}}_0,{\mathtt{w}}_1$为${\mathtt{m}}_0,{\mathtt{m}}_1$进行$\mathtt{MSTORE}$操作之后的值。
如MSTORE 0x22 0xe201e6...662b，想要向基于单个字节布局的以太坊内存中的0x22地址写入：
$$\mathtt{val}=0xe201e6\dots 662b$$
写入成功之后，相应的${\mathtt{w}}_0,{\mathtt{w}}_1$值为：
$${\mathtt{w}}_0=0x88d1e201e6\dots ,{\mathtt{w}}_1=0x662b\mathtt{ff}\dots 54f9$$

已知：

• 1）an address $\mathtt{addr}$
• 2）an offset value $\mathtt{offset}$
• 3）待写入的值 $\mathtt{val}$

Main状态机的操作与上面MLOAD类似，只是改为需要检查${\mathtt{w}}_0,{\mathtt{w}}_1$确实是根据已知的$\mathtt{val},{\mathtt{m}}_0,{\mathtt{m}}_1$

Polygon zkEVM测试集——创建合约交易

Polygon zkEVM交易解析

Polygon zkEVM Prover

Polygon zkEVM网络节点

Polygon zkEVM节点代码解析

Polygon zkEVM——Hermez 2.0简介