美文网首页
Polygon zkEVM Memory Align 状态机

Polygon zkEVM Memory Align 状态机

作者: 雪落无留痕 | 来源:发表于2023-09-12 23:52 被阅读0次

基本介绍

Memory Align SM包含两部分: executor部分和内部的Memory PIL , 用来定义验证规则。

Memory SM是对 32字节words 进行读写,EVM 可以以字节层面偏移读写32字节的words, 分别如下表所示:

\mathbf{ADDRESS} \mathbf{BYTE}
\mathtt{0x00}\\ \mathtt{0x01}\\ \mathtt{0x02}\\ \mathtt{\ldots}\\ \mathtt{0x1e}\\ \mathtt{0x1f} \mathtt{0xc4}\\ \mathtt{0x17}\\ \mathtt{0x4f}\\ \mathtt{\ldots}\\ \mathtt{0x81}\\ \mathtt{0xa7}
\mathtt{0x20}\\ \mathtt{0x21}\\ \mathtt{0x22}\\ \mathtt{\ldots}\\ \mathtt{0x3e}\\ \mathtt{0x3f} \mathtt{0x88}\\ \mathtt{0xd1}\\ \mathtt{0x1f}\\ \mathtt{\ldots}\\ \mathtt{0xb7}\\ \mathtt{0x23}
\mathtt{0x40}\\ \mathtt{0x41}\\ \mathtt{0x42}\\ \mathtt{\ldots}\\ \mathtt{0x5e}\\ \mathtt{0x5f} \mathtt{0x6e}\\ \mathtt{0x21}\\ \mathtt{0xff}\\ \mathtt{\ldots}\\ \mathtt{0x54}\\ \mathtt{0xf9}
\mathbf{ADDRESS} \mathbf{32-BYTE~~WORD}
\mathtt{0x00} \mathtt{0xc4174f...81a7}
\mathtt{0x01} \mathtt{0x88d11f...b723}
\mathtt{0x02} \mathtt{0x6e21ff...54f9}

Memory Align SM 用来检查 32字节寻址和字节寻址的正确关系,主要需要检查以下三种内存操作:

  • MLOAD: 接收一个偏移量(offset), 返回从偏移量开始的32个字节;
  • MSTORE: 接收一个偏移量,从偏移位置开始,保存32个字节;
  • MSTORE8: 接收一个偏移量,从偏移位置开始保存一个字节。

一般而言,MLOAD 需要读取两个words中的字节,如下图所示:

现在来介绍如何验证一个读操作。假设要验证在地址0x22 执行了一个MLOAD 操作,得到值: \mathtt{0x1f\dotsb7236e21}。 此时,主状态机将执行以下一些操作:首先,查询值 m_0m_1 , 然后调用 Memory SM 验证这些查询。

首先需要根据地址 0x22 查询内存的位置, 若 aMLOAD 的内存的位置,则 m_0 在内存的位置总是为: \lfloor \frac{a}{32} \rfloorm_1 在内存的位置为: \lfloor \frac{a}{32} \rfloor + 1。 本例中, a = 0x22 = 34, 因此 m_0 位置为 \lfloor \frac{34}{32} \rfloor = 0x01m_1 存在\lfloor \frac{34}{32} \rfloor + 1 = 0x02.

然后需要抽取 offset, offset为是0到32之间的一个数,offset = a (mod\ 32) 。 然后主状态机利用Plookup , 根据m_0, m_1, offset 验证Memory Align SM 读取的值 val 是正确的。

对于 MSTORE,一般需要在两个words中写入字节。和 MLOAD 类似,用w0 和 w1 分别表示对于 m0 和 m1 进行写操作之后的words。

例如,若要写入以下的值:

val=0xe201e6…662b

到地址 0x22处,即如下图所示:

主状态机需要执行以下操作:

  • 对于给定的地址addroffset,写入值 val。 和之前类似,主状态机负责读取zkEVM 内存中的 m0 和 m1,此时通过Plookup验证读取值的有效性,和 MLOAD类似。
  • 主状态机计算w0 和 w1 , 为了验证 w0 和 w1 的正确性,需要执行 Plookup, 根据val, m_0, m_1, offset 检查 w0 和 w1 的正确性。

最后对于MSTOREE,类似地,但它只影响 m0, 并且只写入一个字节,因此只考虑val 的最后一个字节, 对m1,w1 不再进行约束。

Main executor

对于zkASM 指令:

 $               :MEM_ALIGN_WR,MLOAD(bytesToStore)  //Mem Align write 操作

 $ => A          :MEM_ALIGN_RD      //Memory Align read 操作

 B               :MEM_ALIGN_WR8 ; only use LSB of B, rest of bytes could be non zero. // Mem Align read 字节操作


编译后对应的json 为:

  {
   "freeInTag": {
    "op": ""
   },
   "inFREE": "1",
   "memAlign": 1,
   "memAlignWR": 1,
   "memAlignWR8": 0,
   "offset": 84,
   "mOp": 1,
   "mWR": 0,
   "line": 188,
   "offsetLabel": "bytesToStore",
   "useCTX": 0,
   "fileName": "utils.zkasm",
   "lineStr": "    $               :MEM_ALIGN_WR,MLOAD(bytesToStore)"
  },
  
  {
   "freeInTag": {
    "op": ""
   },
   "inFREE": "1",
   "setA": 1,
   "memAlign": 1,
   "memAlignWR": 0,
   "memAlignWR8": 0,
   "line": 250,
   "fileName": "utils.zkasm",
   "lineStr": "    $ => A          :MEM_ALIGN_RD"
  },
  
  
  {
   "inB": "1",
   "memAlign": 1,
   "memAlignWR": 0,
   "memAlignWR8": 1,
   "line": 1056,
   "fileName": "opcodes.zkasm",
   "lineStr": "    B               :MEM_ALIGN_WR8 ; only use LSB of B, rest of bytes could be non zero"
  }

在Main executor 的执行过程为:

        if (l.memAlign == 1) {
            const m0 = fea2scalar(Fr, ctx.A);
            const v = fea2scalar(Fr, [op0, op1, op2, op3, op4, op5, op6, op7]); 
            const P2_256 = 2n ** 256n;
            const MASK_256 = P2_256 - 1n;
            const offset = fea2scalar(Fr, ctx.C);

            if (offset < 0 || offset >= 32) {
                throw new Error(`MemAlign out of range (${offset}): ${ctx.ln} at ${ctx.fileName}:${ctx.line}`);
            }

            if (l.memAlignWR && !l.memAlignWR8) {   // 判断为memAlignWR 操作
                const m1 = fea2scalar(Fr, ctx.B);
                const w0 = fea2scalar(Fr, ctx.D);
                const w1 = fea2scalar(Fr, ctx.E);
                const _W0 = Scalar.bor(Scalar.band(m0, P2_256 - (2n ** (256n - (8n * offset)))), Scalar.shr(v, 8n * offset));
                const _W1 = Scalar.bor(Scalar.band(m1, MASK_256 >> (offset * 8n)),
                    Scalar.band(Scalar.shl(v, (256n - (offset * 8n))), MASK_256));
                if (!Scalar.eq(w0, _W0) || !Scalar.eq(w1, _W1)) {
                    throw new Error(`MemAlign w0,w1 invalid (0x${w0.toString(16)},0x${w1.toString(16)}) vs (0x${_W0.toString(16)},0x${_W1.toString(16)})` +
                        `[m0:${m0.toString(16)}, m1:${m1.toString(16)}, v:${v.toString(16)}, offset:${offset}]: ${ctx.ln} at ${ctx.fileName}:${ctx.line}`);
                }
                pols.memAlign[i] = 1n;
                pols.memAlignWR[i] = 1n;
                pols.memAlignWR8[i] = 0n;
                required.MemAlign.push({ m0: m0, m1: m1, v: v, w0: w0, w1: w1, offset: offset, wr256: 1n, wr8: 0n });     // 添加MemAlign action
            }
            else if (!l.memAlignWR && l.memAlignWR8) { // 判断为memAlignWR8 操作
                const w0 = fea2scalar(Fr, ctx.D);
                const _W0 = Scalar.bor(Scalar.band(m0, Scalar.shr(byteMaskOn256, 8n * offset)), Scalar.shl(Scalar.band(v, 0xFF), 8n * (31n - offset)));
                if (!Scalar.eq(w0, _W0)) {
                    throw new Error(`MemAlign w0 invalid (0x${w0.toString(16)}) vs (0x${_W0.toString(16)})` +
                        `[m0:${m0.toString(16)}, v:${v.toString(16)}, offset:${offset}]: ${ctx.ln} at ${ctx.fileName}:${ctx.line}`);
                }
                pols.memAlign[i] = 1n;
                pols.memAlignWR[i] = 0n;
                pols.memAlignWR8[i] = 1n;
                required.MemAlign.push({ m0: m0, m1: 0n, v: v, w0: w0, w1: 0n, offset: offset, wr256: 0n, wr8: 1n });  // 添加Mem Align Action
            } else if (!l.memAlignWR && !l.memAlignWR8) { //判断为Mem Align Read 操作
                const m1 = fea2scalar(Fr, ctx.B);
                const leftV = Scalar.band(Scalar.shl(m0, offset * 8n), MASK_256);
                const rightV = Scalar.band(Scalar.shr(m1, 256n - (offset * 8n)), MASK_256 >> (256n - (offset * 8n)));
                const _V = Scalar.bor(leftV, rightV);
                if (!Scalar.eq(v, _V)) {
                    throw new Error(`MemAlign v invalid ${v.toString(16)} vs ${_V.toString(16)}:` +
                        `[m0:${m0.toString(16)}, m1:${m1.toString(16)}, offset:${offset}]: ${ctx.ln} at ${ctx.fileName}:${ctx.line}`);
                }
                pols.memAlign[i] = 1n;
                pols.memAlignWR[i] = 0n;
                pols.memAlignWR8[i] = 0n;
                required.MemAlign.push({ m0: m0, m1: m1, v: v, w0: Fr.zero, w1: Fr.zero, offset: offset, wr256: 0n, wr8: 0n });   // 添加Mem Align Action
            } else {
                throw new Error(`Invalid memAlign operation (wr: ${l.memAlignWR}, wr8: ${l.memAlignWR8}): ${ctx.ln} at ${ctx.fileName}:${ctx.line}`);
            }
        } else {
            pols.memAlign[i] = 0n;
            pols.memAlignWR[i] = 0n;
            pols.memAlignWR8[i] = 0n;
        }

上述分别在memAlignWR, memAlignWR8, memAlignRD 情况下,生成Mem Align action。

主状态机约束

通过Plookup, 限定主机状态变量在MemAlign状态机的约束。

/////////
// MemAlign Plookpups
/////////

    memAlign {
        memAlignWR,
        memAlignWR8,
        A0, A1, A2, A3,
        A4, A5, A6, A7,
        (1 - memAlignWR8) * B0, (1 - memAlignWR8) * B1, (1 - memAlignWR8) * B2, (1 - memAlignWR8) * B3,
        (1 - memAlignWR8) * B4, (1 - memAlignWR8) * B5, (1 - memAlignWR8) * B6, (1 - memAlignWR8) * B7,
        op0, op1, op2, op3,
        op4, op5, op6, op7,
        C0,
        (memAlignWR + memAlignWR8) * D0, (memAlignWR + memAlignWR8)*D1, (memAlignWR + memAlignWR8)*D2, (memAlignWR + memAlignWR8)*D3,
        (memAlignWR + memAlignWR8) * D4, (memAlignWR + memAlignWR8)*D5, (memAlignWR + memAlignWR8)*D6, (memAlignWR + memAlignWR8)*D7,
        memAlignWR * E0, memAlignWR*E1, memAlignWR*E2, memAlignWR*E3,
        memAlignWR * E4, memAlignWR*E5, memAlignWR*E6, memAlignWR*E7
    } in
    MemAlign.RESET {
        MemAlign.wr256,    //是否为32字节写操作
        MemAlign.wr8,      // 是否为单字节写操作
        MemAlign.m0[0], MemAlign.m0[1], MemAlign.m0[2], MemAlign.m0[3],    // m0
        MemAlign.m0[4], MemAlign.m0[5], MemAlign.m0[6], MemAlign.m0[7],
        MemAlign.m1[0], MemAlign.m1[1], MemAlign.m1[2], MemAlign.m1[3],    // m1
        MemAlign.m1[4], MemAlign.m1[5], MemAlign.m1[6], MemAlign.m1[7],
        MemAlign.v[0], MemAlign.v[1], MemAlign.v[2], MemAlign.v[3],      // v
        MemAlign.v[4], MemAlign.v[5], MemAlign.v[6], MemAlign.v[7],
        MemAlign.offset,                                                  //偏移量    
        MemAlign.w0[0], MemAlign.w0[1], MemAlign.w0[2], MemAlign.w0[3],   //w0
        MemAlign.w0[4], MemAlign.w0[5], MemAlign.w0[6], MemAlign.w0[7],
        MemAlign.w1[0], MemAlign.w1[1], MemAlign.w1[2], MemAlign.w1[3],   // w1
        MemAlign.w1[4], MemAlign.w1[5], MemAlign.w1[6], MemAlign.w1[7]
    };

    cntMemAlign' = cntMemAlign*(1-Global.L1) + memAlign;

Mem Align executor

Constants

构建的常量多项式为:

mapRange = (value, fromValue, mappings, elseValue = 0) =>
    (value >= fromValue && value <= (fromValue + mappings.length - 1)) ? mappings[value - fromValue] : elseValue;

const CONST_F = {
    // 0 (x256), 1 (x256), ..., 255 (x256), 0 (x256), ...
    BYTE2A: (i) => (i & 0xFFFF) >> 8,     // BYTE2A 和 BYTE2B组下一个两字节

    // 0, 1, 2, 3, ..., 254, 255, 0, 1, 2, ...
    BYTE2B: (i) => (i & 0xFF),

    // 0 (x3072), 1 (x3072), ..., 255 (x3072), 0 (x3072), ...
    BYTE_C3072: (i) => (i / 3072) | 0,

    //    0 - 1023  WR256 = 0 WR8 = 0
    // 1024 - 2047  WR256 = 1 WR8 = 0
    // 2048 - 3071  WR256 = 0 WR8 = 1
    WR256: (i) => ((i % 3072) >= 1024 && (i % 3072) < 2048) ? true : false,
    WR8: (i) => (i % 3072) >= 2048 ? true : false,

    // 0, 1, 2, ..., 30, 31, 0, 1, ...
    STEP: (i) => i % 32,

    // 1, 0 (x31), 1, 0 (x31), 1, ...
    RESET: (i) => (i % 32) == 0 ? true : false,

    // 0 (x32), 1 (x32), ...., 31 (x32), 0 (x32), ...
    OFFSET: (i) => (i >> 5) % 32,

    // For internal use
    V_BYTE: (i) => (31 + (CONST_F.OFFSET(i) + CONST_F.WR8(i)) - CONST_F.STEP(i)) % 32,

    SELM1: (i) => (CONST_F.WR8(i) ? (CONST_F.STEP(i) == CONST_F.OFFSET(i)) :
        (CONST_F.OFFSET(i) > CONST_F.STEP(i))) ? 1 : 0,

    FACTOR: (index, i) => mapRange(i % 32, 28 - 4 * index, [0x1000000, 0x10000, 0x100, 1], 0),
    FACTORV: (index, i) => (CONST_F.V_BYTE(i) >> 2) == index ? [1, 0x100, 0x10000, 0x1000000][CONST_F.V_BYTE(i) % 4] : 0,
}

module.exports.buildConstants = async function (pols) {
    const N = pols.STEP.length;
    Object.entries(CONST_F).forEach(([name, func]) => {
        if (typeof pols[name] === 'undefined') return;

        if (func.length == 1) {
            for (i = 0; i < N; ++i) pols[name][i] = BigInt(func(i));
        }
        else {
            const indexCount = name.startsWith('SEL') ? 2 : 8;
            for (let index = 0; index < indexCount; ++index) {
                for (i = 0; i < N; ++i) pols[name][index][i] = BigInt(func(index, i));
            }
        }
    });
}

executor

对于主状态机生成的的Mem Align Action, 通过Mem Align executor 进行执行,主要是对m0,m1, v, offset, wr8, wr256, w0, w1的处理:

    for (let i = 0; i < input.length; i++) {
        let m0v = BigInt(input[i]["m0"]);
        let m1v = BigInt(input[i]["m1"]);
        const _v = BigInt(input[i]["v"]);
        const offset = Number(input[i]["offset"]);
        const reverseOffset = 32 - offset;
        const wr8 = Number(input[i]["wr8"]);
        const wr256 = Number(input[i]["wr256"]);
        const polIndex = i * 32;
        let vv = _v;
        for (let j = 0; j < 32; ++j) {
            const _vByte = ((31 + (offset + wr8) - j) % 32);
            const _inM0 = getByte(m0v, 31 - j);
            const _inM1 = getByte(m1v, 31 - j);
            const _inV = getByte(vv, _vByte);
            const _selM1 = (wr8 ? (j == offset) : (offset > j)) ? 1 : 0;

            pols.wr8[polIndex + j + 1] = BigInt(wr8);
            pols.wr256[polIndex + j + 1] = BigInt(wr256);
            pols.offset[polIndex + j + 1] = BigInt(offset);
            pols.inM[0][polIndex + j] = BigInt(_inM0);
            pols.inM[1][polIndex + j] = BigInt(_inM1);
            pols.inV[polIndex + j] = BigInt(_inV);
            pols.selM1[polIndex + j] = BigInt(_selM1);
            pols.factorV[_vByte >> 2][polIndex + j] = BigInt(factors[(_vByte % 4)]);

            const mIndex = 7 - (j >> 2);

            const _inW0 = ((wr256 * (1 - _selM1)) || (wr8 * _selM1)) ? _inV : ((wr256 + wr8) * _inM0);
            const _inW1 = (wr256 * _selM1) ? _inV : ((wr256 + wr8) * _inM1);

            const factor = BigInt(factors[3 - (j % 4)]);

            pols.m0[mIndex][polIndex + 1 + j] = ((j === 0) ? 0n : pols.m0[mIndex][polIndex + j]) + BigInt(_inM0) * factor;
            pols.m1[mIndex][polIndex + 1 + j] = ((j === 0) ? 0n : pols.m1[mIndex][polIndex + j]) + BigInt(_inM1) * factor;

            pols.w0[mIndex][polIndex + 1 + j] = ((j === 0) ? 0n : pols.w0[mIndex][polIndex + j]) + BigInt(_inW0) * factor;
            pols.w1[mIndex][polIndex + 1 + j] = ((j === 0) ? 0n : pols.w1[mIndex][polIndex + j]) + BigInt(_inW1) * factor;
        }
        for (let j = 0; j < 32; ++j) {
            for (let index = 0; index < 8; ++index) {
                pols.v[index][polIndex + 1 + j] = ((j === 0) ? 0n : pols.v[index][polIndex + j]) + pols.inV[polIndex + j] * pols.factorV[index][polIndex + j];
            }
        }

        for (let index = 0; index < 8; ++index) {
            for (j = 32 - (index * 4); j < 32; ++j) {
                pols.m0[index][polIndex + j + 1] = pols.m0[index][polIndex + j];
                pols.m1[index][polIndex + j + 1] = pols.m1[index][polIndex + j];
                pols.w0[index][polIndex + j + 1] = pols.w0[index][polIndex + j];
                pols.w1[index][polIndex + j + 1] = pols.w1[index][polIndex + j];
            }
        }
    }

Mem Align PIL 约束

namespace MemAlign(%N);

    /*
    * OPERATIONS
    *
    *  (m0,m1,D) => v
    *  (m0,m1,D,v) => (w0, w1)
    *
    *  @m0 = addr   @m1 = addr + 32 (ethereum)
    *
    *  Ethereum => BigEndian
    *  m0[7],m0[6],...,m0[1],m0[0],m1[7],m1[6],...,m1[1],m1[0]
    *
    *  inM (8 bits, 32 steps)
    */

    // 32 bytes of M0, M1 ordered from HSB to LSB (32, 31, 30, ... == M[7].3, M[7].2, M[7].1, M[7].0, M[6].3, ..)
    pol commit inM[2];

    // 32 bytes of V
    pol commit inV;

    // write 32 bytes (256 bits)
    pol commit wr256;

    // write 1 byte (8 bits), its special case because need to ignore
    // the rest of bytes, only LSB of V was stored (on w0 with offset)
    pol commit wr8;

    pol commit m0[8];
    pol commit m1[8];
    pol commit w0[8];
    pol commit w1[8];
    pol commit v[8];

    // when m1 is "active", means aligned with inV
    // also when wr8 = 1, used to indicate when store the LSB
    pol commit selM1;

    // factors to build V[] in correct way, because order of V bytes
    // changes according the offset and wr8
    pol commit factorV[8];

    pol commit offset;

    // BYTE2A = 0 (x256), 1 (x256), 2 (x256), ..., 255 (x256)
    pol constant BYTE2A;

    // BYTE2B = 0, 1, 2, 4, **, 255, 0, 1, ..., 255
    pol constant BYTE2B;

    pol constant BYTE_C3072;

    // FACTOR was same for all combinations of offset, wr8, wr256 is a f(step)
    // FACTOR[7] = 2**24, 2**16, 2**8, 1, 0 (x60)
    // FACTOR[6] = 0, 0, 0, 0, 2**24, 2**16, 2**8, 1, 0 (x56)
    // FACTOR[5] = 0, 0, 0, 0, 0, 0, 0, 0, 2**24, 2**16, 2**8, 1, 0 (x52)
    // :
    // FACTOR[0] = 0 (x28), 2**24, 2**16, 2**8, 1, 0 (x32)
    pol constant FACTOR[8];

    // FACTOR change according the combinations of offset, wr8, wr256 and step.
    pol constant FACTORV[8];

    // STEP = 0,1,2,...,62,63,0,1,2,...
    pol constant STEP;

    // STEP
    //    0 - 1023  WR256 = 0 WR8 = 0
    // 1024 - 2047  WR256 = 1 WR8 = 0
    // 2048 - 3071  WR256 = 0 WR8 = 1
    pol constant WR256;
    pol constant WR8;

    // OFFSET = 0 (x64), 1 (x64), ... , 31 (x64), 32 (x64), 0 (x64), 1 (x64), ...
    pol constant OFFSET; // 0 - 31

    // RESET = 1, 0 (x63), 1, 0 (x63)
    pol constant RESET;

    pol constant SELM1;

    //              RangeCheck                  Latch   Clock
    // factorV      Plookup (FACTORV)           no      yes
    // wr256        Plookup (WR256)             yes     no
    // wr8          Plookup (WR8)               yes     no
    // offset       Plookup (OFFSET)            yes     no
    // inV          RangeCheck (BYTE_C3072)     no      yes
    // inM[0..1]    RangeCheck (BYTE2A,BYTE2B)  no      yes
    // m0[0..7]     Built                       no      yes
    // m1[0..7]     Built                       no      yes
    // w0[0..7]     Built                       no      yes
    // w1[0..7]     Built                       no      yes
    // v[0..7]      Built                       no      yes
    // selM1        Plookup (SELM1)             no      yes

    // Latchs
    (1 - RESET) * wr256' = (1 - RESET) * wr256;
    (1 - RESET) * offset' = (1 - RESET) * offset;
    (1 - RESET) * wr8' = (1 - RESET) * wr8;

    // RangeCheck
    {inM[1], inM[0]} in {BYTE2A, BYTE2B};  

    // Plookup
    {
        STEP, offset', wr256', wr8', selM1, inV,
        factorV[0], factorV[1], factorV[2], factorV[3], factorV[4], factorV[5], factorV[6], factorV[7]
    } in {
        STEP, OFFSET, WR256, WR8, SELM1, BYTE_C3072,
        FACTORV[0], FACTORV[1], FACTORV[2], FACTORV[3], FACTORV[4], FACTORV[5], FACTORV[6], FACTORV[7]
    };

    m0[0]' = (1-RESET) * m0[0] + FACTOR[0] * inM[0];
    m0[1]' = (1-RESET) * m0[1] + FACTOR[1] * inM[0];
    m0[2]' = (1-RESET) * m0[2] + FACTOR[2] * inM[0];
    m0[3]' = (1-RESET) * m0[3] + FACTOR[3] * inM[0];
    m0[4]' = (1-RESET) * m0[4] + FACTOR[4] * inM[0];
    m0[5]' = (1-RESET) * m0[5] + FACTOR[5] * inM[0];
    m0[6]' = (1-RESET) * m0[6] + FACTOR[6] * inM[0];
    m0[7]' = (1-RESET) * m0[7] + FACTOR[7] * inM[0];

    m1[0]' = (1-RESET) * m1[0] + FACTOR[0] * inM[1];
    m1[1]' = (1-RESET) * m1[1] + FACTOR[1] * inM[1];
    m1[2]' = (1-RESET) * m1[2] + FACTOR[2] * inM[1];
    m1[3]' = (1-RESET) * m1[3] + FACTOR[3] * inM[1];
    m1[4]' = (1-RESET) * m1[4] + FACTOR[4] * inM[1];
    m1[5]' = (1-RESET) * m1[5] + FACTOR[5] * inM[1];
    m1[6]' = (1-RESET) * m1[6] + FACTOR[6] * inM[1];
    m1[7]' = (1-RESET) * m1[7] + FACTOR[7] * inM[1];

    // selW0 contains data to be store in w0, must be 0 in "reading mode"
    // in "writting mode", in particular with wr8 only on byte must be
    // stored, for this reason use selM1 that was active only one clock (in wr8 mode)
    pol selW0 = (1 - selM1) * wr256' + selM1 * wr8';

    // selW1 contains data to be store in w1, must be 0 in "reading mode"
    pol selW1 = selM1 * wr256';

    // NOTE: when wr8 = 1 implies wr256 = 0, check in this situations where use selM1
    // to verify that non exists collateral effects
    //
    // pol selW0 = selM1 (because wr256 = 0 and wr8 = 1)
    //
    // selM1 used in pol _inM, but _inM is only used on dataV
    // pol dataV = (1 - wr256' - wr8') * _inM + (wr256' + wr8') * inV;
    // pol dataV = inV (because wr256 = 0 and wr8 = 1)
    //
    // CONCLUSION: it's safe reuse selM1 to indicate when store byte

    // data to "write" on w, if current byte must be override by V contains inV
    // if not contains inM "in reading mode" must be 0.
    pol dataW0 = (wr8' + wr256') * inM[0] + selW0 * (inV - inM[0]);
    pol dataW1 = (wr8' + wr256') * inM[1] + selW1 * (inV - inM[1]);

    w0[0]' = (1-RESET) * w0[0] + FACTOR[0] * dataW0;
    w0[1]' = (1-RESET) * w0[1] + FACTOR[1] * dataW0;
    w0[2]' = (1-RESET) * w0[2] + FACTOR[2] * dataW0;
    w0[3]' = (1-RESET) * w0[3] + FACTOR[3] * dataW0;
    w0[4]' = (1-RESET) * w0[4] + FACTOR[4] * dataW0;
    w0[5]' = (1-RESET) * w0[5] + FACTOR[5] * dataW0;
    w0[6]' = (1-RESET) * w0[6] + FACTOR[6] * dataW0;
    w0[7]' = (1-RESET) * w0[7] + FACTOR[7] * dataW0;

    w1[0]' = (1-RESET) * w1[0] + FACTOR[0] * dataW1;
    w1[1]' = (1-RESET) * w1[1] + FACTOR[1] * dataW1;
    w1[2]' = (1-RESET) * w1[2] + FACTOR[2] * dataW1;
    w1[3]' = (1-RESET) * w1[3] + FACTOR[3] * dataW1;
    w1[4]' = (1-RESET) * w1[4] + FACTOR[4] * dataW1;
    w1[5]' = (1-RESET) * w1[5] + FACTOR[5] * dataW1;
    w1[6]' = (1-RESET) * w1[6] + FACTOR[6] * dataW1;
    w1[7]' = (1-RESET) * w1[7] + FACTOR[7] * dataW1;

    // _inM contains "active" value of inM
    pol _inM = (1 - selM1) * inM[0] + selM1 * inM[1];

    // contains data to store in V, could be one of inM if was reading or inV if was writting
    pol dataV = (1 - wr256' - wr8') * _inM + (wr256' + wr8') * inV;

    // factorV = f(STEP, offset, wr8)
    v[0]' = (1-RESET) * v[0] + factorV[0] * dataV;
    v[1]' = (1-RESET) * v[1] + factorV[1] * dataV;
    v[2]' = (1-RESET) * v[2] + factorV[2] * dataV;
    v[3]' = (1-RESET) * v[3] + factorV[3] * dataV;
    v[4]' = (1-RESET) * v[4] + factorV[4] * dataV;
    v[5]' = (1-RESET) * v[5] + factorV[5] * dataV;
    v[6]' = (1-RESET) * v[6] + factorV[6] * dataV;
    v[7]' = (1-RESET) * v[7] + factorV[7] * dataV;

参考

https://github.com/0xPolygonHermez/zkevm-doc

https://github.com/0xPolygonHermez/zkevm-commonjs

https://github.com/0xPolygonHermez/zkevm-proverjs

相关文章

网友评论

      本文标题:Polygon zkEVM Memory Align 状态机

      本文链接:https://www.haomeiwen.com/subject/bvwuvdtx.html