基本介紹
Memory Align SM包含兩部分： executor部分和內(nèi)部的Memory PIL 脸秽， 用來定義驗證規(guī)則。
Memory SM是對 32字節(jié)words 進行讀寫蝴乔，EVM 可以以字節(jié)層面偏移讀寫32字節(jié)的words, 分別如下表所示：
Memory Align SM 用來檢查 32字節(jié)尋址和字節(jié)尋址的正確關(guān)系记餐，主要需要檢查以下三種內(nèi)存操作：
-
MLOAD: 接收一個偏移量（offset）， 返回從偏移量開始的32個字節(jié)薇正； -
MSTORE: 接收一個偏移量剥扣，從偏移位置開始巩剖，保存32個字節(jié)； -
MSTORE8: 接收一個偏移量钠怯，從偏移位置開始保存一個字節(jié)。
一般而言曙聂，MLOAD 需要讀取兩個words中的字節(jié)晦炊，如下圖所示：
現(xiàn)在來介紹如何驗證一個讀操作。假設(shè)要驗證在地址0x22 執(zhí)行了一個MLOAD 操作宁脊，得到值: 断国。 此時，主狀態(tài)機將執(zhí)行以下一些操作：首先榆苞，查詢值
和
稳衬， 然后調(diào)用 Memory SM 驗證這些查詢。
首先需要根據(jù)地址 查詢內(nèi)存的位置坐漏， 若
是
MLOAD 的內(nèi)存的位置薄疚，則 在內(nèi)存的位置總是為：
，
在內(nèi)存的位置為：
赊琳。 本例中街夭，
， 因此
位置為
躏筏，
存在
.
然后需要抽取 offset, offset為是0到32之間的一個數(shù)板丽， 。 然后主狀態(tài)機利用
Plookup 趁尼， 根據(jù) 驗證Memory Align SM 讀取的值
val 是正確的埃碱。
對于 MSTORE，一般需要在兩個words中寫入字節(jié)酥泞。和 MLOAD 類似砚殿，用w0 和 w1 分別表示對于 m0 和 m1 進行寫操作之后的words。
例如婶博，若要寫入以下的值：
val=0xe201e6…662b
到地址 0x22處瓮具，即如下圖所示：
主狀態(tài)機需要執(zhí)行以下操作：
- 對于給定的地址
addr和offset，寫入值val凡人。 和之前類似名党，主狀態(tài)機負責讀取zkEVM 內(nèi)存中的 m0 和 m1，此時通過Plookup驗證讀取值的有效性挠轴，和MLOAD類似传睹。 - 主狀態(tài)機計算w0 和 w1 ， 為了驗證 w0 和 w1 的正確性岸晦，需要執(zhí)行
Plookup, 根據(jù)val, m_0, m_1, offset檢查 w0 和 w1 的正確性欧啤。
最后對于MSTOREE睛藻，類似地，但它只影響 m0邢隧， 并且只寫入一個字節(jié)店印，因此只考慮val 的最后一個字節(jié)， 對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 字節(jié)操作
編譯后對應(yīng)的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 的執(zhí)行過程為：
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。
主狀態(tài)機約束
通過Plookup, 限定主機狀態(tài)變量在MemAlign狀態(tài)機的約束纫谅。
/////////
// 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字節(jié)寫操作
MemAlign.wr8, // 是否為單字節(jié)寫操作
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
構(gòu)建的常量多項式為：
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組下一個兩字節(jié)
// 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
對于主狀態(tài)機生成的的Mem Align Action, 通過Mem Align executor 進行執(zhí)行炫贤，主要是對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
