Polygon zkEVM Keccak 状态机

作者: 雪落无留痕 | 来源:发表于2023-09-13 00:07 被阅读0次

基本介绍

Sponge Construction

Sponge 构造是一个简单迭代的构造，用于构建函数：
$F: \mathbb{Z}^* \to \mathbb{Z}^l$
具有变长的输入，任意长度的输出。 $F$ 基于一个固定长度的置换：
$f: \mathbb{Z}^b \to \mathbb{Z}^b$
其中 $b$ 称为状态的宽度。状态分为两部分： $r$ (bitrate) 和 $c$ (capacity)。Sponge 构造分为三个阶段：

初始阶段：对输入字符串进行填充，使其为 $r$ 的整数倍，随后为会为 $r$ 的块。将 $b$ 位的状态初始化为0.
吸收阶段：输入的 $r$ 位块和状态的前 $r$ 位异或处理，然后应用函数 $f$ ，直到处理完所有的 $r$ 位的块。注意状态的后 $c$ 位从不从吸引任何输入。
压缩阶段：状态的 $r$ 位作为输出的块。输出块的个数由用户决定。

Sponge Function Construction

sponge 构造由三个参数确定：固定长度的置换函数 $f$ , 填充规则 $\textbf{pad}$ , 和 $r$ 。

zkEVM 相关的构造

zkEVM 使用两种hash 函数，主要原因是EVM存储使用 KECCAK-256 函数构造Merkle Tree. zkEVM的内部hash, 采用Poseidon 函数，用来减少证明者复杂度。

KECCAK-256

EVM 使用KECCAK-256 作为函数函数，采用KECCAK[512] sponge构造。对于KECCAK[c] sponge 构造，操作的状态为1600位， $r$ 的大小为： $1600-c$ 。对于KECCAK [512]， $r$ 为1088位， $c$ 为512位。KECCAK[c] 采用的置换为KECCAK-p[1600, 24]。填充规则为 $10*1$ 。若定义 $j = (-m-2)\ mod\ r$ ， $m$ 为输入消息的长度，则填充的消息为：
$P = 1 || 0^j || 1.$

$KECCAK[c](M,d)$ 用来对于输入的消息 $M$ ，输出长度为 $d$ 。

NIST SHA3主要在于填充规则不一样，即：
$\text{SHA3-256}(M) = \text{KECCAK}[512](M \mid\mid 01, 256).$

Keccak 算术化过程

Keccak-f 是SHA-3的伪随机置换，需要执行 $N$ (12~24) 次。

其中主要有两个常量： $r$ ，为 $5 \times 5$ 的数组，范围为 $[0, 63]$ ； $RC$ ，为 $N\times 64$ 数组，每个为64位的向量。

本文主要关注：在给定输入的情况下，如何利用一些低次的多项式，验证每轮的输出是正确的。

位运算算术化

首先分析下如何使用低次多项式计算位运算，先以下面的代数等式为例：
$x\ AND\ y = x\ \&\ y = xy \\ x\ XOR\ y = x \oplus\ y = x + y-2xy \\ NOT\ x = ~x = 1-x$
对于3列多项式 $x,y,z$ ，长度分别为 32，值为 0 或 1. 即对于 $0\leq i\leq 32,$ $z_i =x_i\oplus y_i$ ，其等价于32个简单的多项式条件：
$x_i + y_i-2x_iy_i-z_i=0$
为了测试这些多项式条件，证明者需要保存96个域元素，但可以优化，仅需要65个。可以将 $z_i$ 合并成一个 $u32$ :
$z = z_0+2z_1+\cdots+2^32z_{31}$
可以将32个多项式合并成一个条件，输入为2次的：
$z-\sum_{i=0}^{31}2^i(x_i+y_i-2x_iy_i)=0 \\$
另外，可以转换约束为：
$z_i=x_i\oplus y_i \Leftrightarrow y_i = x_i \oplus z_i \Leftrightarrow x_i = y_i \oplus z_i$
因此挑选任间一列，将其折叠成一个 $u32$ 值。

下面给出一些三元运算的多项式：
$xor3(x,y,z)=x\oplus y \oplus z = x + y + z -2 (xy +xz+yz)+ 4xyz \\ xorandn(x,y,z) = x\oplus ((-y)\ \&\ y)=x+z-yz-2xz+xyz$

大规模位运算算术化

当运算只涉及很少输入的时候，相应的多项式比较简单。当对于 $n$ 元操作，需要使用一个 $n$ 次的多项式。

定理对于 $n$ 元布尔操作，可以表示成一个如下形式的 $n$ 次多项式：
$z=p(\bf{x}) = \sum_{i\in\{0,1\}^n}a_ix_1^{i_1}...x_n^{i_n}$
若是我们要求整个次数 $\leq3$ ，可以使用的最大的位运算次数也是3。但有时可以找到一个多项式 $P(z,\bf{x})=0$ , 当且仅当 $z=p(\bf{x})$ .

此时，将 $z=p(\bf{x})$ 作为计算多项式（computation polynomial）， $P(z, \bf{x})=0$ 为验证多项式（verification polynomial）。

对以下5个 $xor$ 的运算为例：
$z=x_1\oplus x_2 \oplus x_3 \oplus x_4 \oplus x_5$
任意的计算多项式的次数为5，但有一些方法能生成次数为3的验证多项式。

根据定义， $z$ 为 $x_1 + x_2+x_3+ x_4+x_5$ 的奇偶校验位，因此：

$x_1 + x_2 +x_3+x_4+x_5-z\in \{0,2,4\}$

因此当 $z$ 正确的时候，以下等式成立：
$(x_1+x_2+x_3+x_4+x_5-z)(x_1+x_2+x_3+x_4+x_5-z-2)(x_1+x_2+x_3+x_4+x_5-z-4)=0$

或者采用另外一种方法，对于：

$z=x_1\oplus x_2 \oplus x_3 \oplus x_4 \oplus x_5$

可以写成：
$z\oplus x_1 \oplus x_2= x_3 \oplus x_4 \oplus x_5$
当且仅当如下式子成立：
$xor3(x_1, x_2, z)-xor3(x_3,x_4,x_5)=0$
其中 $xor3$ 是一个3次多项式。

Keccak 验证

为了验证Keccak，需要保存2406个域元素，但这还可以优化。另外，有一些变量需要为 $u32$ . 为了区分这两种场景，使用 $A[x,y,z]$ 表示单独的位，其中 $0\leq z \leq 63$ ; $\bf{A}[x,y,j]$ 表示一个 $u32$ 的值，其中 $j\in \{0,1\}$ .

大小为： $5 \times 5 \times 2$ : $\bf{A}[x,y,j]$ 为 $u32$ 对；
大小为： $5 \times 64$ :

$C[x,z]=A[x,0,z]\oplus A[x,1,z]\oplus A[x,2,z] \oplus A[x,3,z] \oplus A[x,4,z]$

大小为： $5\times 5 \times 64$ :

$A'[x,y,z]=A[x,y,z]\oplus C[x-1,z]\oplus C[x+1,z-1]$

大小为： $5\times 64$ :

$C'[x,z]=C[x,z]\oplus C[x-1,z]\oplus C[x+1,z-1]$

大小为： $5\times 5 \times 2$ : $\bf A''[x,y,j]$ 定义为：

$A''[x,y,z]=B[x,y,z]\oplus((\thicksim B[x+1,y,z])\ \&\ B[x+2,y,z])$

其中 $B$ 为：
$B[x,y,z]=A'[3y+x,x,z-r[x,y]]$

大小为64：包含 $A''[0,0,z]$ 所的各个位；
大小为2： $\bf A'''[0,0,j]$ 的 $u32$ 对，定义如下：
$A'''[0,0,z]=A''[0,0,z]\oplus RC[k,z]$

下面将详细介绍需要验证的细节，主要分为两组：首先要验证 $A'$ 是由 $A$ 正确计算得到；然后验证 $A'', A'''$ 是由 $A'$ 正确计算得到。

$A'$ 计算的验证

由于 $A$ 存为 $u32$ 的值，可以它上面的计算多项式，所有的多项式需要是以下形式：
$A[x,y,z]=p(A',C, C')$
首先需要使用 $xor3$ 检查 $C$ 和 $C'$ 的关系，主要有以下多项式关系：
$xor3(C[x,z], C[x-1,z], C[x+1,z-1])=C'[x,z]$
然后，可以重写 $A'$ 的定义为：
$A[x,y,z]=A'[x,y,z]\oplus[x,z]\oplus C'[x,z]$
这些可以通过 $xor3$ 和 $u32$ 技术验证，即：
$\sum_{i=0}^{31}xor3(A'[x,y,i+32j], C[x,i+32j], C'[x,i+32j])=\bf{A}[x,y,j]$
可以利用下面的定理：

**Lemma ** 假设：
$A[x,y,z]=A'[x,y,z]\oplus C[x,z]\oplus C'[x,z]$
则下面的陈述是等价的：

$C[x,z]=\oplus_{i=0}^4 A[x,i,z]$
$C'[x,z]=\oplus_{i=0}^4A'[x,i,z]$

因此可以通过验证 $C'$ 去验证 $C$ ，因此，定义：
$D[x,z]=(\sum_{i=0}^4A'[x,i,z])-C'[x,z]$
然后验证：
$D[x,z] (D[x,z]-2)(D[x,z]-4)=0$
由于 $D$ 是线性的，所以上式的次数为3.

验证 $A''$ 和 $A'''$ 的计算

对于：
$B[x,y,z]=A'[3y+x,x,z-r[x,y]]$
是 $A'$ 的一个旋转，因此可以直接验证 $A''$ ，使用 $xorandn$ 和 $u32$ 的技巧，得到：
$\sum_{0}^{31}2^ixorandn(B[x,y,i+32j], B[x+1,y,i+32j], B[x+2,y, i+32j])=\bf A''[x,y,j]$
然后需要检查 $A''[0,0,z]$ 匹配 $\bf A''[0,0,j]$ ，对应如下的条件：
$\sum_{i=0}^{31}2^iA_{0,0}''[i+32j]=\bf A''[0,0,j]$
最后，为了验证 $A'''[0,0]$ ，使用简单的2次多项式描述 $xor$ ，可以得到：
$\sum_{i=0}^{31}2^ixor(A''_{0,0}[i+32j], RC[k,i+32j])=\bf A'''[0,0,j]$
即完成了整个验证过程。

Main_executor

以下面的zkASM代码片段为例，其主要计算keccak256(numBatch-1,0)，如下所示：

;; Set batch hash
        0 => HASHPOS ; A new hash with position 0 is started
        $ => E                              :MLOAD(lastHashKIdUsed)
        E+1 => E                            :MSTORE(lastHashKIdUsed)

        $ => A                              :MLOAD(numBatch)
        A - 1                               :HASHK(E)
        %STATE_ROOT_STORAGE_POS             :HASHK(E) ; Storage position of the batch hash
        HASHPOS                             :HASHKLEN(E)
        %MAX_CNT_KECCAK_F - CNT_KECCAK_F - %MIN_CNT_KECCAK_BATCH - 2:JMPN(outOfCounters)
        $ => C                              :HASHKDIGEST(E)

其编译后对应的json为：

{
   "CONST": "0",
   "setHASHPOS": 1,
   "line": 44,
   "fileName": "main.zkasm",
   "lineStr": "        0 => HASHPOS ; A new hash with position 0 is started"
  },
  {
   "freeInTag": {
    "op": ""
   },
   "inFREE": "1",
   "setE": 1,
   "offset": 15,
   "mOp": 1,
   "mWR": 0,
   "line": 45,
   "offsetLabel": "lastHashKIdUsed",
   "useCTX": 0,
   "fileName": "main.zkasm",
   "lineStr": "        $ => E                              :MLOAD(lastHashKIdUsed)"
  },
  {
   "inE": "1",
   "CONST": "1",
   "setE": 1,
   "offset": 15,
   "mOp": 1,
   "mWR": 1,
   "line": 46,
   "offsetLabel": "lastHashKIdUsed",
   "useCTX": 0,
   "fileName": "main.zkasm",
   "lineStr": "        E+1 => E                            :MSTORE(lastHashKIdUsed)"
  },
  {
   "freeInTag": {
    "op": ""
   },
   "inFREE": "1",
   "setA": 1,
   "offset": 7,
   "mOp": 1,
   "mWR": 0,
   "line": 48,
   "offsetLabel": "numBatch",
   "useCTX": 0,
   "fileName": "main.zkasm",
   "lineStr": "        $ => A                              :MLOAD(numBatch)"
  },
  {
   "inA": "1",
   "CONST": "-1",
   "ind": 1,          // 根据E 寄存器计算地址偏移位置
   "indRR": 0,
   "offset": 0,
   "hashK": 1,
   "line": 49,
   "fileName": "main.zkasm",
   "lineStr": "        A - 1                               :HASHK(E)"
  },
  {
   "CONST": "0",
   "ind": 1,
   "indRR": 0,
   "offset": 0,
   "hashK": 1,
   "line": 50,
   "fileName": "main.zkasm",
   "lineStr": "        %STATE_ROOT_STORAGE_POS             :HASHK(E) ; Storage position of the batch hash"
  },
  {
   "inHASHPOS": "1",
   "ind": 1,
   "indRR": 0,
   "offset": 0,
   "hashKLen": 1,
   "line": 51,
   "fileName": "main.zkasm",
   "lineStr": "        HASHPOS                             :HASHKLEN(E)"
  },
  {
   "CONST": "464",
   "inCntKeccakF": "-1",
   "JMPC": 0,
   "JMPN": 1,
   "offset": 1858,
   "line": 52,
   "offsetLabel": "outOfCounters",
   "fileName": "main.zkasm",
   "lineStr": "        %MAX_CNT_KECCAK_F - CNT_KECCAK_F - %MIN_CNT_KECCAK_BATCH - 2:JMPN(outOfCounters)"
  },
  {
   "freeInTag": {
    "op": ""
   },
   "inFREE": "1",
   "setC": 1,
   "ind": 1,
   "indRR": 0,
   "offset": 0,
   "hashKDigest": 1,
   "line": 53,
   "fileName": "main.zkasm",
   "lineStr": "        $ => C                              :HASHKDIGEST(E)"
  }

上述主要涉及hashK, hashKlen, hashKDigest 三个过程：

hashK

        if (l.hashK) {
            if (typeof ctx.hashK[addr] === "undefined") ctx.hashK[addr] = { data: [], reads: {} };
            pols.hashK[i] = 1n;
            const size = fe2n(Fr, ctx.D[0], ctx);
            const pos = fe2n(Fr, ctx.HASHPOS, ctx);
            if ((size < 0) || (size > 32)) throw new Error(`Invalid size for hashK: ${ctx.ln} at ${ctx.fileName}:${ctx.line}`);
            const a = fea2scalar(Fr, [op0, op1, op2, op3, op4, op5, op6, op7]);
            const maskByte = Scalar.e("0xFF");
            for (let k = 0; k < size; k++) {
                const bm = Scalar.toNumber(Scalar.band(Scalar.shr(a, (size - k - 1) * 8), maskByte));
                const bh = ctx.hashK[addr].data[pos + k];
                if (typeof bh === "undefined") {
                    ctx.hashK[addr].data[pos + k] = bm;
                } else if (bm != bh) {
                    throw new Error(`HashK do not match ${addr}:${pos + k} is ${bm} and should be ${bh}: ${ctx.ln} at ${ctx.fileName}:${ctx.line}`)
                }
            }

            const paddingA = Scalar.shr(a, size * 8);
            if (!Scalar.isZero(paddingA)) {
                throw new Error(`Incoherent size (${size}) and data (0x${a.toString(16)}) padding (0x${paddingA.toString(16)}) for hashK (w=${step}): ${ctx.ln} at ${ctx.fileName}:${ctx.line}`);
            }

            if ((typeof ctx.hashK[addr].reads[pos] !== "undefined") &&
                (ctx.hashK[addr].reads[pos] != size)) {
                throw new Error(`HashK diferent read sizes in the same position ${addr}:${pos}`)
            }
            ctx.hashK[addr].reads[pos] = size;
            incHashPos = size;
        } else {
            pols.hashK[i] = 0n;
        }

其主要将keccak hash的每个输入保存在data 字节数组中：

 ctx.hashK[addr].data[pos + k] = bm;

将每个输入的长度保存在reads中：

 ctx.hashK[addr].reads[pos] = size;

hashKLen

        if (l.hashKLen) {
            pols.hashKLen[i] = 1n;
            const lm = fe2n(Fr, op0, ctx);
            // If it's undefined compute hash 0f 0 bytes
            if (typeof ctx.hashK[addr] === "undefined") {
                // len must be 0
                if (lm != 0) throw new Error(`HashK length does not match ${addr}  is ${lm} and should be ${0}`);
                ctx.hashK[addr] = { data: [], reads: {} };
                ctx.hashK[addr].digest = ethers.utils.keccak256("0x");
            }
            const lh = ctx.hashK[addr].data.length;
            if (lm != lh) throw new Error(`HashK length does not match ${addr}  is ${lm} and should be ${lh}`);
            if (typeof ctx.hashK[addr].digest === "undefined") {
                ctx.hashK[addr].digest = ethers.utils.keccak256(ethers.utils.hexlify(ctx.hashK[addr].data));
            }
        } else {
            pols.hashKLen[i] = 0n;
        }

hashKLen 实现Keccak256对 ctx.hashK[addr].data 的hash计算，保存在ctx.hashK[addr].digest 当中。

hashKDigest

      if (l.hashKDigest) {
            pols.hashKDigest[i] = 1n;
            const dg = fea2scalar(Fr, [op0, op1, op2, op3, op4, op5, op6, op7]);
            if (typeof ctx.hashK[addr].digest === "undefined") {
                throw new Error(`Cannnot load keccak from DB`);
            }
            if (!Scalar.eq(Scalar.e(dg), Scalar.e(ctx.hashK[addr].digest))) {
                throw new Error(`Digest doesn't match`);
            }
            incCounter = Math.ceil((ctx.hashK[addr].data.length + 1) / 136)
        } else {
            pols.hashKDigest[i] = 0n;
        }

hashKDigest 主要是获取得到的最终的Hash值。

PaddingKK Action

根据需要计算的Keccak hash的个数，生成PaddingKK Action.

    for (let i=0; i<ctx.hashK.length; i++) {
        const h = {
            data: ctx.hashK[i].data,  //为 hash输入字节数组
            reads: []       // hash输入的每个元素的字节个数
        }
        let p= 0;
        while (p<ctx.hashK[i].data.length) {
            if (ctx.hashK[i].reads[p]) {
                h.reads.push(ctx.hashK[i].reads[p]);
                p += ctx.hashK[i].reads[p];
            } else {
                h.reads.push(1);
                p += 1;
            }
        }
        if (p!= ctx.hashK[i].data.length) {
            throw new Error(`Reading hashK out of limits: ${step}`);
        }
        required.PaddingKK.push(h);
    }

主状态机约束

/////////
// HASHK Plookpups
/////////
    hashK {
        addr,   // 表示HashK的编号，
        HASHPOS,    // 表示起始位置
        D0,         // 表示size [0,32]
        op0, op1, op2, op3,   // 表示此次Hash的输入
        op4, op5, op6, op7
    } in
    PaddingKK.crLatch * PaddingKK.crValid {
        PaddingKK.addr,
        PaddingKK.len - PaddingKK.rem - PaddingKK.crLen + 1,
        PaddingKK.crLen,
        PaddingKK.crV0C, PaddingKK.crV1C, PaddingKK.crV2C, PaddingKK.crV3C,
        PaddingKK.crV4C, PaddingKK.crV5C, PaddingKK.crV6C, PaddingKK.crV7C
    };

    hashKLen {
        addr,  // hashK 的编号
        op0     // Hash输入数据字节个数
    } in
    PaddingKK.lastHashLatch {
        PaddingKK.addr,
        PaddingKK.len
    };

    hashKDigest {
        addr,               //hash编号
        op0, op1, op2, op3, // 得到的Hash值 
        op4, op5, op6, op7,
        incCounter        // 增加的Keccak_F的轮数
    } in
    PaddingKK.lastHashLatch {
        PaddingKK.addr,
        PaddingKK.hash0, PaddingKK.hash1, PaddingKK.hash2, PaddingKK.hash3,
        PaddingKK.hash4, PaddingKK.hash5, PaddingKK.hash6, PaddingKK.hash7,
        PaddingKK.incCounter
    };

    cntKeccakF' = cntKeccakF*(1-Global.L1) + incCounter*hashKDigest;

PaddingKK

constants

const BYTESPERBLOCK = 136;   // 每次KeccakF输入的字节数 r
const BlockSize = 158418;

module.exports.buildConstants = async function (pols) {
    const poseidon = await buildPoseidon();
    const F = poseidon.F;      // 多项式定义然Goldilocs 域上

    const N = pols.lastBlock.length;       // 总行数

    const nBlocks = 9*Math.floor((N-1)/BlockSize);  //  

    let p =0;

    pols.k_crF = [];
    for (let i=0; i<8; i++) {
        pols.k_crF[i] = pols[`k_crF${i}`];
    }

    for (let i=0; i<nBlocks; i++) {
        const bytesBlock = 136;
        for (let j=0; j<bytesBlock; j++) {
            pols.lastBlock[p] = (j == bytesBlock-1) ? 1n : 0n;
            pols.lastBlockLatch[p] = (j == bytesBlock-1) ? 1n : 0n;
            pols.crValid[p] = F.one;
            pols.r8Id[p] = F.e(p);
            pols.sOutId[p] =  (j == bytesBlock-1) ? F.e(i) : F.zero;
            pols.forceLastHash[p] = ((j == bytesBlock-1)&&(i==nBlocks-1)) ? F.one : F.zero;
            pols.r8valid[p] = F.one;
            p += 1;
        }
    }

    for (let i=p; i<N; i++) {
        pols.crValid[i] = F.zero;
        pols.r8Id[i] = F.zero;    // Must repeat the first byte
        pols.lastBlock[i] = i<N-1 ? F.zero : F.one;
        pols.lastBlockLatch[i] = F.zero;
        pols.sOutId[i] =  F.zero;
        pols.forceLastHash[i] = i==N-1 ? F.one : F.zero;
        pols.r8valid[i] = F.zero;
    }

    for (let i=0; i<32; i++) {
        pols.k_crOffset[i] = BigInt(i);
        const acci = Math.floor(i / 4);
        const sh = BigInt((i % 4)*8);
        for (let k=0; k<8; k++) {
            pols.k_crF[k][i] = (k == acci) ? BigInt(1n << sh) : 0n;
        }
    }

    for (let i=32; i<N; i++) {
        pols.k_crOffset[i] = pols.k_crOffset[0];
        for (let k=0; k<8; k++) {
            pols.k_crF[k][i] =  pols.k_crF[k][0]
        }
    }

}

Executor

首先对数据进行填充处理，先计算原始数据的keccak256 hash值，然后保存在input 的hash 字段中。

然后再进行填充，填充为了BYTESPERBLOCK (136) 的整数倍.

function prepareInput(input) {
    function hexToBytes(hex) {
        for (var bytes = [], c = 0; c < hex.length; c += 2)
            bytes.push(parseInt(hex.substr(c, 2), 16));
        return bytes;
    }

    for (let i=0; i<input.length; i++) {
        if (typeof input[i].data === "string") {
            input[i].dataBytes = hexToBytes(input[i].data);
        } else if (Array.isArray(input[i].data) ) {
            input[i].dataBytes = input[i].data.slice();
        }

        input[i].hash = ethers.utils.keccak256(input[i].dataBytes);

        input[i].realLen = BigInt(input[i].dataBytes.length);

        input[i].dataBytes.push(0x1);


        while (input[i].dataBytes.length % BYTESPERBLOCK) input[i].dataBytes.push(0);

        input[i].dataBytes[ input[i].dataBytes.length - 1] |= 0x80;
    }
}

当一个BYTESPERBLOCK 处理完的时候，会生成paddingKKBIT action, connected 用于表示是否后前面的action 相连。

if (j % BYTESPERBLOCK == (BYTESPERBLOCK -1) ) {
                required.paddingKKBit.push({
                    r: input[i].dataBytes.slice(j - BYTESPERBLOCK +1, j+1),
                    connected: (j<BYTESPERBLOCK) ? false : true
                });

                if (j == input[i].dataBytes.length - 1) {  // 最终处理的hash值

                    [
                        pols.hash0[p],
                        pols.hash1[p],
                        pols.hash2[p],
                        pols.hash3[p],
                        pols.hash4[p],
                        pols.hash5[p],
                        pols.hash6[p],
                        pols.hash7[p]
                    ] =  scalar2fea(F, Scalar.e(input[i].hash));

                    for (k=1; k<input[i].dataBytes.length; k++) {
                        pols.hash0[p-k] = pols.hash0[p];
                        pols.hash1[p-k] = pols.hash1[p];
                        pols.hash2[p-k] = pols.hash2[p];
                        pols.hash3[p-k] = pols.hash3[p];
                        pols.hash4[p-k] = pols.hash4[p];
                        pols.hash5[p-k] = pols.hash5[p];
                        pols.hash6[p-k] = pols.hash6[p];
                        pols.hash7[p-k] = pols.hash7[p];
                    }
                }

            }

Padding_kk 约束

通过lookup, 限定Padding_kk 在 PaddingKKBit 的约束为：

    lastHashLatch {
        hash0,
        hash1,
        hash2,
        hash3,
        hash4,
        hash5,
        hash6,
        hash7,
        sOutId
     } in {
        PaddingKKBit.sOut0,
        PaddingKKBit.sOut1,
        PaddingKKBit.sOut2,
        PaddingKKBit.sOut3,
        PaddingKKBit.sOut4,
        PaddingKKBit.sOut5,
        PaddingKKBit.sOut6,
        PaddingKKBit.sOut7,
        PaddingKKBit.sOutId
     };

上述是一整个Keccak256 Hash结果的限制。

Padding_kkbit

对于输入的Padding_kkbit action, 在Padding_kkbit executor 中执行时会生成Nine2One action, 代表一次KeccakF运算，如下所示：

        curState = keccakF(stateWithR);
        required.Nine2One.push([stateWithR, curState]);

其中stateWithR 和 curState 的结构为：

            stateWithR = [
                [[0,0],[0,0],[0,0],[0,0],[0,0]],
                [[0,0],[0,0],[0,0],[0,0],[0,0]],
                [[0,0],[0,0],[0,0],[0,0],[0,0]],
                [[0,0],[0,0],[0,0],[0,0],[0,0]],
                [[0,0],[0,0],[0,0],[0,0],[0,0]]
            ];

代表着 5 * 5 * 64 = 1600 位的输入和输出。

`Padding_kkbit` 约束

    /*
    connected, sOutBit, rBit   => sInBit
    0 0 0     0
    0 0 1     1
    0 1 0     0
    0 1 1     1
    1 0 0     0
    1 0 1     1
    1 1 0     1
    1 1 1     0
    */

    pol aux_sInBit = (sOutBit - 2*sOutBit*rBit);
    pol sInBit = connected * aux_sInBit + rBit;

    pol constant ConnSOutBit, ConnSInBit, ConnNine2OneBit;

    {sOutBit, sInBit, Nine2One.bit} connect {ConnSOutBit, ConnSInBit, ConnNine2OneBit}

Nine2one

对于输入的Nine2one Action, 生成KeccakF Action, 将每9个合并为一个，如下所示：

    for (let i=0; i<nSlots9; i++) {
        const keccakFSlot = [];
        for (j=0; j<1600; j++) {
            for (k=0; k<9; k++) {     // 每9个合并为一个
                pols.bit[p] = getBit(i*9+k, false, j);
                pols.field9[p] = accField9;
                accField9 = k==0 ? pols.bit[p] :
                    accField9 +  (pols.bit[p] << (7n * BigInt(k)));
                p += 1;
            }
            keccakFSlot.push(accField9);    // 每个keccakFSlot 包含1600个 域元素，每个域元素由9个bit 合并而成
        }
        for (j=0; j<1600; j++) {
            for (k=0; k<9; k++) {
                pols.bit[p] = getBit(i*9+k, true, j);
                pols.field9[p] = accField9;
                accField9 = k==0 ? pols.bit[p] :
                    accField9 +  (pols.bit[p] << (7n * BigInt(k)));
                p += 1;
            }
        }

        pols.bit[p] = 0n;
        pols.field9[p] = accField9;
        accField9 = 0n;
        p += 1;

        for (j=3200*9+1; j<SlotSize; j++) {
            pols.bit[p] = 0n;
            pols.field9[p] = 0n;
            p += 1;
        }

        required.KeccakF.push(keccakFSlot); // 添加到KeccakF action 中。
    }

Nine2one 约束

Nine2one 对应的PIL 约束为：

include "keccakf.pil";

namespace Nine2One(%N);
    pol constant Field9latch;  // 0,0,0,0,0,0,0,0,0,1,0,0,0
    pol constant Factor;  // 1, 1<<7, 1<<21, .....

    pol commit bit;
    pol commit field9;

    field9' = (1-Field9latch)*field9 + bit*Factor;
    bit *(1-bit) = 0;

    Field9latch*(field9 - KeccakF.a) = 0;   // 约束field9 和 KeccakF中的a相等

KeccakF

KeccakF executor 执行时会生成NormGate9 action，包含两种类型：XORN 和 ANDP，分别如下所示：

            const mask = 0b000000100000010000001000000100000010000001000000100000010000001n;
            if (l.op === "xor") {
                pols.c[r] = pols.a[r] + pols.b[r];
            } else if (l.op === "xorn") {
                pols.c[r] = (pols.a[r] & mask) ^ (pols.b[r] &  mask);
                required.NormGate9.push(["XORN", pols.a[r], pols.b[r]]);
            } else if (l.op === "andp") {
                pols.c[r] = ((pols.a[r]  &  mask) ^ mask) & (pols.b[r]  &  mask);
                required.NormGate9.push(["ANDP", pols.a[r], pols.b[r]]);
            }

KeccakF 约束

namespace KeccakF(%N);

    pol constant ConnA, ConnB, ConnC, NormalizedGate, GateType;
    pol commit a,b,c;

    {a, b, c} connect {ConnA, ConnB, ConnC};

    (1-NormalizedGate)*(a+b-c) = 0;

    NormalizedGate { GateType, a, b, c } in NormGate9.Latch { NormGate9.gateType, NormGate9.latch_a, NormGate9.latch_b, NormGate9.latch_c } ;

    Global.L1 * a = 0;
    Global.L1 * (72624976668147841-b) = 0;

Norm_gate9

            if (input[i][0] == "XORN") {
                pols.gateType[p] = 0n;
                pols.freeCNorm[p] = pols.freeANorm[p] ^ pols.freeBNorm[p];
            } else if (input[i][0] == "ANDP") {
                pols.gateType[p] = 1n;
                pols.freeCNorm[p] = (pols.freeANorm[p] ^ 0b000000100000010000001n) & pols.freeBNorm[p];
            } else {
                assert(false, "Invalid door " + input[i][0])
            }

norm_gate9 约束

namespace NormGate9(%N);

    pol constant Value3, Value3Norm;   // Normalization table
    pol constant Gate9Type, Gate9A, Gate9B, Gate9C; // AndN table
    pol constant Latch;   // 0,0,0,1,0,0,1,0,0,1,....
    pol constant Factor;  // 1, 1<<21, 1<<42, 1, 1<<21, 1<<42, ..... 1 << 42, 0, 0

    pol commit freeA, freeB;
    pol commit gateType;     // 0=XOR, 1=ANDN

    (gateType' - gateType)*(1 - Latch) = 0;

    pol commit freeANorm, freeBNorm, freeCNorm;

    { freeA , freeANorm } in { Value3, Value3Norm };
    { freeB , freeBNorm } in { Value3, Value3Norm };
    { gateType, freeANorm, freeBNorm, freeCNorm } in { Gate9Type, Gate9A, Gate9B, Gate9C}; // 内部查找表约束
    pol commit a, b, c;

    pol latch_a = a + Factor*freeA;
    pol latch_b = b + Factor*freeB;
    pol latch_c = c + Factor*freeCNorm;

    a' = latch_a * (1-Latch);
    b' = latch_b * (1-Latch);
    c' = latch_c * (1-Latch);

由此完成整个Keccak 状态机的约束。

参考

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

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

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

https://github.com/0xPolygonHermez/zkevm-storage-rom

https://blog.polygon.technology/zk-white-paper-efficient-zk-proofs-for-keccak/

Polygon zkEVM Keccak 状态机

基本介绍

zkEVM 相关的构造

Keccak 算术化过程

位运算算术化

大规模位运算算术化

Keccak 验证

$A'$ 计算的验证

验证 $A''$ 和 $A'''$ 的计算

Main_executor

hashK

hashKLen

hashKDigest

PaddingKK Action

主状态机约束

PaddingKK

constants

Executor

Padding_kk 约束

Padding_kkbit

`Padding_kkbit` 约束

Nine2one

Nine2one 约束

KeccakF

KeccakF 约束

Norm_gate9

norm_gate9 约束

参考

相关文章

网友评论

延伸阅读

深度阅读

栏目导航

热点阅读

Polygon zkEVM Keccak 状态机

基本介绍

zkEVM 相关的构造

Keccak 算术化过程

位运算算术化

大规模位运算算术化

Keccak 验证

计算的验证

验证 和 的计算

Main_executor

hashK

hashKLen

hashKDigest

PaddingKK Action

主状态机约束

PaddingKK

constants

Executor

Padding_kk 约束

Padding_kkbit

Padding_kkbit 约束

Nine2one

Nine2one 约束

KeccakF

KeccakF 约束

Norm_gate9

norm_gate9 约束

参考

相关文章

网友评论

延伸阅读

深度阅读

栏目导航

热点阅读

$A'$ 计算的验证

验证 $A''$ 和 $A'''$ 的计算

`Padding_kkbit` 约束