Polygon zkEVM Memory状态机

Posted mutourend

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了Polygon zkEVM Memory状态机相关的知识,希望对你有一定的参考价值。

1. 引言

前序博客有:

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

A D D R E S S \\mathbfADDRESS ADDRESS B Y T E \\mathbfBYTE BYTE
0 \\mathtt0 0 0 x c 4 \\mathtt0xc4 0xc4
1 \\mathtt1 1 0 x 17 \\mathtt0x17 0x17
⋮ \\mathtt\\vdots ⋮ \\mathtt\\vdots
30 \\mathtt30 30 0 x 81 \\mathtt0x81 0x81
31 \\mathtt31 31 0 x a 7 \\mathtt0xa7 0xa7
32 \\mathtt32 32 0 x 88 \\mathtt0x88 0x88
33 \\mathtt33 33 0 x d 1 \\mathtt0xd1 0xd1
⋮ \\mathtt\\vdots ⋮ \\mathtt\\vdots
62 \\mathtt62 62 0 x b 7 \\mathtt0xb7 0xb7
63 \\mathtt63 63 0 x 23 \\mathtt0x23 0x23
Table 1: Layout in memory of 0xc417...81a7 and 0x88d1...b723.

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

  • 1)MLOAD:按指定offset地址读取内存,返回32字节word。如上表中,MLOAD 1返回的为 0x17...a788 \\texttt0x17...a788 0x17...a788

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

    A D D R E S S \\mathbfADDRESS ADDRESS B Y T E \\mathbfBYTE BYTE
    0 \\mathtt0 0 0 x c 4 \\mathtt0xc4 0xc4
    1 \\mathtt1 1 0x74 \\mathtt\\textbf0x74 0x74
    2 \\mathtt2 2 0xf0 \\mathtt\\textbf0xf0 0xf0
    ⋮ \\mathtt\\vdots ⋮ \\mathtt\\vdots
    31 \\mathtt31 31 0xce \\mathtt\\textbf0xce 0xce
    32 \\mathtt32 32 0x92 \\mathtt\\textbf0x92 0x92
    33 \\mathtt33 33 0 x d 1 \\mathtt0xd1 0xd1
    ⋮ \\mathtt\\vdots ⋮ \\mathtt\\vdots
    62 \\mathtt62 62 0 x b 7 \\mathtt0xb7 0xb7
    63 \\mathtt63 63 0 x 23 \\mathtt0x23 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 \\textbfADDRESS ADDRESS 32-BYTE   WORD \\textbf32-BYTE WORD 32-BYTE WORD
0 \\mathtt0 0 0 x c 417...81 a 7 \\mathtt0xc417...81a7 0xc417...81a7
1 \\mathtt1 1 0 x 88 d 1... b 723 \\mathtt0x88d1...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 \\textttaddr addr标记,指向32-byte word。word的值存储在内存中,以 val \\textttval val标记,具体为8个4字节寄存器 val[0..7] \\textttval[0..7] val[0..7](256-bit)。

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

step \\textttstep step mOp \\textttmOp mOp mWr \\textttmWr mWr addr \\textttaddr addr val[7] \\textttval[7] val[7] val[6] \\textttval[6] val[6] … \\dots val[0] \\textttval[0] val[0]
1111621213782 … \\dots 5432
3111432319326 … \\dots 8012
5510621213782 … \\dots 5432
6311648741725 … \\dots 2074
7210432319326 … \\dots 8012
8911291675291 … \\dots 6001
Table 4: Memory Operations and an Execution Trace of the Main SM.

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

Memory状态机的trace必须检查:

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

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

step \\textttstep step addr \\textttaddr addr mOp \\textttmOp mOp mWr \\textttmWr mWr val[7] \\textttval[7] val[7] val[6] \\textttval[6] val[6] … \\dots val[0] \\textttval[0] val[0]
8921191675291 … \\dots 6001
3141132319326 … \\dots 8012
7241032319326 … \\dots 8012
1161121213782 … \\dots 5432
5561021213782 … \\dots 5432
6361146741725 … \\dots 2074
Table 5: Corresponding Memory SM Execution Trace.

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

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

Memory状态机内的约束有:【Memory状态机的execution trace必须对所有内存操作进行排序:首先按 addr \\textttaddr addr升序排序,然后按 step \\textttstep step升序排序。】

  • 1) lastAccess \\textttlastAccess 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 \\textttmOp mOp mWr \\textttmWr mWr仅能为0或1,且当且仅当 mOp \\textttmOp mOp为1时, mWr \\textttmWr 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 ′ \\textttmOp' mOp mWr ′ \\textttmWr' 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

    以上是关于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状态机初体验