美文网首页
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