Polygon zkEVM storage状态机

2023-09-18 本文已影响0人雪落无留痕

Storage State Machine 介绍

存储状态机负责zkProver存储数据的所有操作。它从主状态机获收指令，也称为： $\textbf{Storage Actions}$ 。 Storage Actions是一些典型的数据库操作： Create, Read, Update, Delete (CRUD)。

存储状态机事实上是一个微处理器，分为固件和硬件两部分。

在固件部分设置逻辑规则，以JSON 格式存在 ROM 中。 zkASM 用来映射zkProver 主状态机中的指令到其它状态机中。在本例中，是映射到存储状态机的 Executor 中。主状态机中的指令（Storage Actions），由Storage SM Executor 根据逻辑规则执行。

硬件部分使用另外一种新的语言，称为PIL，专为zkProver 设计，因为几乎所有的状态机将计算表述为多项式。状态转移必须满足计算相关的多项式恒等关系。

存储状态机执行所有的Storage Actions, 生成承诺和常量多项式。

PIL 代码用来检查SM 相关的Actions 正确执行，因此将承诺和常量多项式作为输入。

为了实现零知识证明，所有的数据以Merkle Tree的形式存储，这意味着存储状态机需要向其它状态机发出请求，如Poseidon SM，来执行hashing 运算。

Storage SM 主要执行SMT （Sparse Merkle Trees）上的计算，包含： CREATE， READ, UPDATE, DELETE.

在Storage SM 中， keys和 values都是256 位。

状态机设计

zkProver 存储中数据以SMT (Sparse Merkle Tree) 的形式存放，同时结合Merkle Tree 和 Patricia tree.

Merkle Trees

Merle 树有 leaves, branches, root, 如下图所示：

有相同父节点的称为 siblings，例如 $B_{ab}$ 和 $B_{cd}$ 为 siblings。

使用Keys定位 Merkle 树叶子节点

key中的 0 代表左边，1代表右边，例如对于 $( K_{\mathbf{d}} , V_{\mathbf{d}})$ , 其中 $K_{\mathbf{d}} = 10010110$ ，定位 $V_{\mathbf{d}}$ 的过程如下：

首先读取 $K_{\mathbf{d}} = 10010110$ 的最低位，为0，因此从左边遍历树，到达 $B_{abcd}$ ；
然后依次读取倒数第2位，为1，因此从右边遍历，到达 $B_{cd}$ ;
再次读取倒数第3位，为1，因此从右边遍历，到达 $H(V_d)$ .

由于 $H(V_d)$ 为叶子节点，因此对于 $K_{\mathbf{d}}$ , $V_{\mathbf{d}}$ 的值即为 $H(V_d)$ 。

tree-address 用来表示 $V_x$ 在Merkle 树的位置，表示从根到达 $L_d$ 的key bits, 但是为相反的顺序，例如上述 $V_d$ 的tree-address 为 011。

基本概念

level 用来表示从根节点定位到叶子节点的边数，用 $lvl(\mathbf{L}_x)$ 表示，例如对于下面的示例：
$\begin{aligned} (\mathbf{K}_{\mathbf{a}} , V_{\mathbf{a}}),\ \ (\mathbf{K}_{\mathbf{b}} , V_{\mathbf{b}}),\ \ (\mathbf{K}_{\mathbf{c}} , V_{\mathbf{c}}),\ \ (\mathbf{K}_{\mathbf{c}}, V_{\mathbf{c}}),\\ (\mathbf{K}_{\mathbf{d}}, V_{\mathbf{d}}),\ \ (\mathbf{K}_{\mathbf{e}}, V_{\mathbf{e}}),\ \ (\mathbf{K}_{\mathbf{f}}, V_{\mathbf{f}})\ \ {\text{and}}\ \ (\mathbf{K}_{\mathbf{g}} , V_{\mathbf{g}}) \end{aligned}$
其中键值为：
$\begin{aligned} K_{\mathbf{a}} = 10101100, K_{\mathbf{b}} = 10010010, K_{\mathbf{c}} = 10001010, &K_{\mathbf{d}} = 11100110,\\ K_{\mathbf{e}} = 11110101, K_{\mathbf{f}} = 10001011, K_{\mathbf{g}} = 00011111. \end{aligned}$
叶子节点的层级分别为：

$\text{lvl}(\mathbf{L}*_{\mathbf{a}}) = 2$ , $\text{lvl}(\mathbf{L}_*{\mathbf{b}}) = 4$ , $\text{lvl}(\mathbf{L}*_{\mathbf{c}}) = 4$ , $\text{lvl}(\mathbf{L}_*{\mathbf{d}}) = 3$ ,

$\text{lvl}(\mathbf{L}*_{\mathbf{e}}) = 2$ , $\text{lvl}(\mathbf{L}_*{\mathbf{f}}) = 3$ and $\text{lvl}(\mathbf{L}_{\mathbf{g}}) = 3$

height of an SMT 定义为最大的level，也即key的长度。

The Remaining Key 叶子节点不仅存放值 $V_x$ ，还有未使用的从根节点定到叶子节点未使用的key-bits, 称为remaining key, 用 $RK_x$ 表示。

例如上图中7个叶子节点的remaing keys 分别为：

$\text{RK}*_{\mathbf{a}} = 110101$ , $\text{RK}_*{\mathbf{b}} = 1001$ , $\text{RK}*_{\mathbf{c}} = 0001$ , $\text{RK}_*{\mathbf{d}} = 00111$ , $\text{RK}*_{\mathbf{e}} = 101111$ , $\text{RK}_*{\mathbf{f}} = 10001$ and $\text{RK}_{\mathbf{g}} = 11000$

Fake-Leaf Attack

攻击者可能将中间节点伪装成叶子节叶，通过Merkle 验证。

为了解决这个问题，对叶子和中间计算的时候分别采用不同的hash函数，即 $H_{leaf}$ 和 $H_{noleaf}$ 。

Non-Binding key-value pairs

攻击可能根据现有的 $(K_d, V_d)$ ，生成新的 $(K_x, V_x)$ , 通过Merkle 验证。例如对于下图， $K_d = 11100110$ , 可以选择 $K_x = 10100110$ ，使 $(K_x, V_x)$ 通过Merkle 验证，虽然 $(K_x, V_x)$ 并不存在。

攻击成功的原因在于key-value没有绑定关系。为了解决这个问题，可以更改叶子节点的生成方式为：
$\begin{aligned} \mathbf{L_{x}} = \mathbf{H_{leaf}}(K_{\mathbf{x}} \| V_\mathbf{{x}} ) \end{aligned}$
或者
$HV_\mathbf{{x}} = H_{noleaf}(V_x)$

$\begin{aligned} \mathbf{L_{x}} = \mathbf{H_{leaf}}(RK_{\mathbf{x}} \| HV_\mathbf{{x}} ) \end{aligned}$

引入零知识证明

对于key-value 对 $(K_x, V_x)$ ，可以先计算 $V_x$ 的hash值，即：
$\begin{aligned} \text{Hashed Value} = \text{HV}_\mathbf{{x}} = \mathbf{H_{noleaf}}(V_\mathbf{{x}}) \end{aligned}$
然后构建叶子节点为：
$\begin{aligned} \mathbf{L_{x}} = \mathbf{H_{leaf}}( \text{RK}_\mathbf{x} \| \text{HV}_\mathbf{{x}}) \end{aligned}$
验证者只需要 $HV_x$ 验证Merkle 证明，从而隐藏实际 $V_x$ 的值。

READ Operation

证明者承诺 key-value 对 $(K_x, HV_x)$ ，其中 $HV_x$ 是 $V_x$ 的Hash值，然后声明叶子节点 $L_x$ 包含 $V_x$ 的值。

READ 操作主要验证叶子 $L_x$ 确实包含值 $V_x$ ，采用Merkle 证明实现。因此证明除了提供 $(K_x, HV_x)$ , 还需要root, $RK_x$ ，和所有必要的siblings。

UPDATE Operation

UPDATE 操作包含两步：

首先检查 $\mathbf{READ}$ 操作；
沿着路径重计算所有节点。

image.png

CREATE Operation

CREATE 操作添加新的叶子 $L_{new}$ , 插入到Merkle 树中，键值对为： $( \mathbf{{K_{new}}} , \mathbf{V_{\mathbf{new}}} )$ 。

当从root 定位的时候， $\mathbf{K_{new}}$ 可能是空节点，或者是已经存在的节点，分别如下图所示：

DELETE/REMOVE Operation

DELETE 操作删除叶子节点，主要有两种场景：

DELETE 操作等价于UPDATE操作，将非空的节点变成空节点， SMT 拓扑节点不变；
DELETE 操作作为CREATE操作的反向过程，删除一些扩展节点，会改变SMT 拓扑结构。

zkProver Storage Parameters

在 Storage SM 中，key和value 皆为256位。

Keys 由四个64位的域元素组成 $\text{Key}_{\mathbf{0123}} = \big( \text{Key}_{\mathbf{0}} , \text{Key}_{\mathbf{1}} , \text{Key}_{\mathbf{2}} , \text{Key}_{\mathbf{3}} \big)$ ，其中 $Key_i \in \mathbb{F}_p$ ， $p = 2^{64}-2^{32} +1$

虽然Hash 值是256位，由4个域元素组成，但是256位承诺的值写作8个32位的分块，即 $\text{V}_{\mathbf{01..7}} = \big( \text{V}_{\mathbf{0}} , \text{V}_{\mathbf{1}} , \text{V}_{\mathbf{2}} , \dots , \text{V}_{\mathbf{7}} \big)$ 。

Constructing Navigation Paths

对于 $\text{Key}_{\mathbf{0123}} = \big( \text{Key}_{\mathbf{0}} , \text{Key}_{\mathbf{1}} , \text{Key}_{\mathbf{2}} , \text{Key}_{\mathbf{3}} \big) \in \mathbb{F}_{p}^4$ , 对于每个 $Key_i$ ，
$\begin{aligned} \text{Key}_{\mathbf{0}} = k_{\mathbf{0,63}\ } k_{\mathbf{0,62}\ } \dots k_{\mathbf{0,2}\ } k_{\mathbf{0,1}\ } k_{\mathbf{0,0} },\ \ \text{Key}_{\mathbf{1}} = k_{\mathbf{1,63}\ } k_{\mathbf{1,62}\ } \dots k_{\mathbf{1,2}\ } k_{\mathbf{1,1}\ } k_{\mathbf{1,0} }, \\\text{Key}_{\mathbf{2}} = k_{\mathbf{2,63}\ } k_{\mathbf{2,62}\ } \dots k_{\mathbf{2,2}\ } k_{\mathbf{2,1}\ } k_{\mathbf{2,0} },\ \ \text{Key}_{\mathbf{3}} = k_{\mathbf{3,63}\ } k_{\mathbf{3,62}\ } \dots k_{\mathbf{3,2}\ } k_{\mathbf{3,1}\ } k_{\mathbf{3,0} }, \end{aligned}$
其中 MSB 位为 $k_{i,63}$ , LSB 位为 $k_{i,0}$ , 其中 $i\in \{0,1,2,3\}$

构建的key 值为：
$\begin{aligned} k_{\mathbf{0,0}\ } k_{\mathbf{1,0}\ } k_{\mathbf{2,0}\ } k_{\mathbf{3,0}\ } k_{\mathbf{0,1}\ } k_{\mathbf{1,1}\ } k_{\mathbf{2,1}\ } k_{\mathbf{3,1}\ } k_{\mathbf{0,2}\ } k_{\mathbf{1,2}\ } k_{\mathbf{2,2}\ } k_{\mathbf{3,2}\ }\\ \dots k_{\mathbf{0,62}\ } k_{\mathbf{1,62}\ } k_{\mathbf{2,62}\ } k_{\mathbf{3,62}\ } k_{\mathbf{0,63}\ } k_{\mathbf{1,63}\ } k_{\mathbf{2,63}\ } k_{\mathbf{3,63} }. \end{aligned}$

反过来，也可以根据 Path-Bits 重构 Key。

POSEIDON Hash

POSEIDON SM 执行Main SM 和 Storage SM 的指令，即计算这两个SM消息的Hash值，并检查其正确性。

zkProver 使用goldiocks POSEIDON ，定义的域为 $p = 2^{64} - 2^{32} + 1$ .

POSEIDON SM 有12个内部的状态，即： in0, in1,... , in7, hashType, cap1, cap2, cap3 进行置换运算 $\text{POSEIDON}^{\pi}$ .

$\text{POSEIDON}^{\pi}$ 运行30轮，分3次，总共90轮。输出4个hash 值，即： hash0, hash1, hash2, hash3

对于zkProver storage, 有两个 $\text{POSEIDON}$ ， $\text{HASH0}$ 用来创建分支节点， $\text{HASH1}$ 用来创建叶子节点，主要有参数hashType 决定。

Storage State Machine Design

Storage SM 主要由3部分组成：Storage Assembly code, Storage Executor code，和 Storage PIL 代码。

Storage Assembly

Storage Assembly code 主要将主状态机的CRUD 指令映射到 secondary Storage Assembly codes，总共有8个。

Storage Actions	File Names	Code Names	Action Selectors In Primary zkASM Code
READ	Get	Get	isGet()
UPDATE	Set_Update	SU	isSetUpdate()
CREATE new value at a found leaf	Set_InsertFound	SIF	isSetInsertFound()
CREATE new value at a zero node	Set_InsertNotFound	SINF	isSetInsertNotFound()
DELETE last non-zero node	Set_DeleteLast	SDL	isSetDeleteLast()
DELETE leaf with non-zero sibling	Set_DeleteFound	SDF	isSetDeleteFound()
DELETE leaf with zero sibling	Set_DeleteNotFound	SDNF	isSetDeleteNotFound()
SET a zero node to zero	Set_ZeroToZero	SZTZ	isSetZeroToZero()

get -> get the value

              - update -> update existing value
              - insertFound -> insert with found key; found a leaf node with a common set of key bits
              - insertNotFound -> insert with no found key, at a zero node
              - deleteFound -> delete with found key
              - deleteNotFound -> delete with no found key
              - deleteLast -> delete the last node, so root becomes 0
              - zeroToZero -> value was zero and remains zero

Storage Executor

Storage Executor 主要根据 Assembly 代码逻辑规则，执行SMT Actions。

Storage PIL

Storage SM中计算都需要是可验证的，PIL来用定义这些多项式需要满足的约束，如下表所示：

Selectors	Setters	Instructions
selFree[i]	setHashLeft[i]	iHash
selSiblingValueHash[i]	setHashRight[i]	iHashType
selOldRoot[i]	setOldRoot[i]	iLatchSet
selNewRoot[i]	setNewRoot[i]	iLatchGet
selValueLow[i]	setValueLow[i]	iClimbRkey
selValueHigh[i]	setValueHigh[i]	iClimbSiblingRkey
selRkeyBit[i]	setSiblingValueLow[i]	iClimbSiblngRkeyN
selSiblingRkey[i]	setSiblingValueHigh[i]	iRotateLevel
selRkey[i]	setRkey[i]	iJmpz
	setSiblingRkey[i]	iConst0
	setRkeyBit[i]	iConst1
	setLevel[i]	iConst2
		iConst3
		iAddress

MemDB

MemDB 主要用于保存SMT 中的key-value 值（生产环境下采用Postgre数据库）。

MemDB 构造函数如下：

   /**
     * Constructor Memory Db
     * @param {Field} F - Field element
     * @param {Object} db - Database to load  // key-value 数据库
     */
    constructor(F, db) {
        if (db) {
            this.db = db;
        } else {
            this.db = {};
        }
        this.F = F;
    }

MemDB相关的接口为：

//  设置SMT 树的节点值，其中 `key` 为 长度为4 的数组，数组每个元素为64位。`value` 为 64位元素值的数组。
     /**
     * Set merkle-tree node
     * @param {Array[Field]} key - key in Field representation
     * @param {Array[Field]} value - child array
     */
    async setSmtNode(key, value) {
       ...
    }
       

//  获取 SMT 树的节点值，其中 `key` 为 长度为4 的数组，数组每个元素为64位。返回值为 64位元素值的数组。
   /**
     * Get merkle-tree node value
     * @param {Array[Field]} key - key in Array Field representation
     * @returns {Array[Fields] | null} Node childs if found, otherwise return null
     */
    async getSmtNode(key) {
      ...
    }
 
      
   // 设置key(256位)的值   
    /**
     * Set value
     * @param {String | Scalar} key - key in scalar or hex representation
     * @param {Any} value - value to insert into the DB (JSON valid format)
     */
    async setValue(key, value) {
        const keyS = Scalar.e(key).toString(16).padStart(64, '0');
        this.db[keyS] = JSON.stringify(value);
    }

    
    // 获取key（256位）的值  
      /**
     * Get value
     * @param {String | Scalar} key - key in scalar or hex representation
     * @returns {Any} - value retirved from database
     */
    async getValue(key) {
        const keyS = Scalar.e(key).toString(16).padStart(64, '0');

        if (typeof this.db[keyS] === 'undefined') {
            return null;
        }

        return JSON.parse(this.db[keyS]);
    }
      
    
    //key 为4个64位域元素的数组， value 为byte 数组   
    /**
     * Set program node
     * @param {Array[Field]} key - key in Field representation
     * @param {Array[byte]} value - child array
     */
    async setProgram(key, value) {
       ...  
    }  
      
   // key 为4个64位域元素的数组， 返回值为byte 数组   
    /**
     * Get program value
     * @param {Array[Field]} key - key in Array Field representation
     * @returns {Array[Byte] | null} Node childs if found, otherwise return null
     */
    async getProgram(key) {
       ... 
    }

SMT

SMT (sparse merkle tree)的构造函数如下：

   /**
     * Constructor Sparse-merkle-tree
     * @param {Object} db - Database to use  // 数据库-mebdb
     * @param {Object} hash - hash function // hash函数-poseidon
     * @param {Field} F - Field element  // 有限域-Goldilocks 
     */
    constructor(db, hash, F) {
        this.db = db;
        this.hash = hash;
        this.F = F;
        this.empty = [F.zero, F.zero, F.zero, F.zero];
    }

SMT 主要有set 和get 两个函数：

    /**
     * Insert node into the merkle-tree
     * @param {Array[Field]} oldRoot - previous root
     * @param {Array[Field]} key - path merkle-tree to insert the value
     * @param {Scalar} value - value to insert
     * @returns {Object} Information about the tree insertion
     *      {Array[Field]} oldRoot: previous root,
     *      {Array[Field]} newRoot: new root
     *      {Array[Field]} key modified,
     *      {Array[Array[Field]]} siblings: array of siblings,   
            // SMT 路径,以叶子节点向上直接根节点的所有中间节点 
     *      {Array[Field]} insKey: inserted key,   // 为found key和 value值， 否则undefined.
     *      {Scalar} insValue: insefted value,
     *      {Bool} isOld0: is new insert or delete,  // 若found， 则为false, 否则为true
     *      {Scalar} oldValue: old leaf value,
     *      {Scalar} newValue: new leaf value,
     *      {String} mode: action performed by the insertion,
             // mode模式有： update, insertFound, insertNotFound, deleteFound,       
             //  deleteNotFound, deleteLast, zeroToZero
             
     *      {Number} proofHashCounter: counter of hashs must be done to proof this operation
     */
    async set(oldRoot, key, value) {
        ...
    }

对于空树，SMT Root为： [0, 0, 0, 0]

若插入一个节点：（key, value）

hashVaule = hash(value, [0,0,0,0])
hashLeaf = hash(key, hashValue, [1,0,0,0])

则SMT 根节点为： hashLeaf;

若挺入两个节点：(key_0, value_0), (key_1, value)，分别表示第一层的左右两个叶子节点：

hashVaule_0 = hash(value_0, [0,0,0,0])
hashLeaf_0 = hash(key_0_R, hashValue, [1,0,0,0])   // R 表示Remaing key

hashVaule_1 = hash(value_1, [0,0,0,0])
hashLeaf_1 = hash(key_1_R, hashValue, [1,0,0,0])   // R 表示Remaing key

root  = hash(hashLeaf_0,  hashLeaf_1, [0,0,0,0])

得到的根节点即为 root。

get 函数有的接口如下：

   /**
    * Get value merkle-tree
    * @param {Array[Field]} root - merkle-tree root
    * @param {Array[Field]} key - path to retoreve the value
    * @returns {Object} Information about the value to retrieve
    *      {Array[Field]} root: merkle-tree root,
    *      {Array[Field]} key: key to look for,
    *      {Scalar} value: value retrieved,
    *      {Array[Array[Field]]} siblings: array of siblings,  // MPT 树的Path
    *      {Bool} isOld0: is new insert or delete,
    *      {Array[Field]} insKey: key found,
    *      {Scalar} insValue: value found,
    *      {Number} proofHashCounter: counter of hashs must be done to proof this operation
    */
   async get(root, key) {
    ... 
   }

若能找到对应key 的值，则返回value, 否则 value 为0；

insKey 和 insValue 表示，在未查到目前key 情况下，能查找到的key 和 value, 此时 isOld0 值为false.

      if (typeof (foundKey) !== 'undefined') {
            if (nodeIsEq(key, foundKey, F)) {
                value = foundVal;
            } else {
                insKey = foundKey;
                insValue = foundVal;
                isOld0 = false;
            }
        }

常量多项式构建

module.exports.buildConstants = async function (pols) {
    const poseidon = await buildPoseidon();
    const fr = poseidon.F;

    // Init rom from file
    const rawdata = fs.readFileSync("testvectors/storage_sm_rom.json");
    const j = JSON.parse(rawdata);
    rom = new StorageRom;
    rom.load(j);

    const polSize = pols.rLine.length;

    for (let i=0; i<polSize; i++) {
        // TODO: REVIEW Jordi
        const romLine = i % rom.line.length;
        const l = rom.line[romLine];

        pols.rHash[i] = l.iHash ? BigInt(l.iHash) : 0n;
        pols.rHashType[i] = l.iHashType ? BigInt(l.iHashType) : 0n;
        pols.rLatchGet[i] = l.iLatchGet ? BigInt(l.iLatchGet) : 0n;
        pols.rLatchSet[i] = l.iLatchSet ? BigInt(l.iLatchSet) : 0n;
        pols.rClimbRkey[i] = l.iClimbRkey ? BigInt(l.iClimbRkey) : 0n;
        pols.rClimbSiblingRkey[i] = l.iClimbSiblingRkey ? BigInt(l.iClimbSiblingRkey) : 0n;
        pols.rClimbSiblingRkeyN[i] = l.iClimbSiblingRkeyN ? BigInt(l.iClimbSiblingRkeyN) : 0n;
        pols.rRotateLevel[i] = l.iRotateLevel ? BigInt(l.iRotateLevel) : 0n;
        pols.rJmpz[i] = l.iJmpz ? BigInt(l.iJmpz) : 0n;
        pols.rJmp[i] = l.iJmp ? BigInt(l.iJmp) : 0n;
        let consFea4;
        if (l.CONST) {
            consFea4 = scalar2fea4(fr,BigInt(l.CONST));
        } else {
            consFea4 = [fr.zero, fr.zero, fr.zero, fr.zero];
        }
        pols.rConst0[i] = consFea4[0];
        pols.rConst1[i] = consFea4[1];
        pols.rConst2[i] = consFea4[2];
        pols.rConst3[i] = consFea4[3];

        pols.rAddress[i] = l.address ? BigInt(l.address) : 0n;
        pols.rLine[i] = BigInt(romLine);

        pols.rInFree[i] = l.inFREE ? BigInt(l.inFREE) : 0n;
        pols.rInNewRoot[i] = l.inNEW_ROOT ? BigInt(l.inNEW_ROOT):0n;
        pols.rInOldRoot[i] = l.inOLD_ROOT ? BigInt(l.inOLD_ROOT):0n;
        pols.rInRkey[i] = l.inRKEY ? BigInt(l.inRKEY):0n;
        pols.rInRkeyBit[i] = l.inRKEY_BIT ? BigInt(l.inRKEY_BIT):0n;
        pols.rInSiblingRkey[i] = l.inSIBLING_RKEY ? BigInt(l.inSIBLING_RKEY):0n;
        pols.rInSiblingValueHash[i] = l.inSIBLING_VALUE_HASH ? BigInt(l.inSIBLING_VALUE_HASH):0n;

        pols.rSetHashLeft[i] = l.setHASH_LEFT ? BigInt(l.setHASH_LEFT):0n;
        pols.rSetHashRight[i] = l.setHASH_RIGHT ? BigInt(l.setHASH_RIGHT):0n;
        pols.rSetLevel[i] = l.setLEVEL ? BigInt(l.setLEVEL):0n;
        pols.rSetNewRoot[i] = l.setNEW_ROOT ? BigInt(l.setNEW_ROOT):0n;
        pols.rSetOldRoot[i] = l.setOLD_ROOT ? BigInt(l.setOLD_ROOT):0n;
        pols.rSetRkey[i] = l.setRKEY ? BigInt(l.setRKEY):0n;
        pols.rSetRkeyBit[i] = l.setRKEY_BIT ? BigInt(l.setRKEY_BIT):0n;
        pols.rSetSiblingRkey[i] = l.setSIBLING_RKEY ? BigInt(l.setSIBLING_RKEY):0n;
        pols.rSetSiblingValueHash[i] = l.setSIBLING_VALUE_HASH ? BigInt(l.setSIBLING_VALUE_HASH):0n;
        pols.rSetValueHigh[i] = l.setVALUE_HIGH ? BigInt(l.setVALUE_HIGH):0n;
        pols.rSetValueLow[i] = l.setVALUE_LOW ? BigInt(l.setVALUE_LOW):0n;
    }
}

Main_executor的执行

SLOAD

SLOAD 主要作用于A,B,C 寄存器中。

对于Main_executor对SMT 读的操作，以下所zkasm 代码为例：

;; Assert local exit root
        ; Read 'localExitRoot' variable from GLOBAL_EXIT_ROOT_MANAGER_L2 and check
        ; it is equal to the 'newLocalExitRoot' input
        %ADDRESS_GLOBAL_EXIT_ROOT_MANAGER_L2  => A
        %SMT_KEY_SC_STORAGE => B
        %LOCAL_EXIT_ROOT_STORAGE_POS => C
        $ => A                                          :SLOAD

编译得到的json 为：

  {
   "CONSTL": "995052982721906769083524541345745747257928364082",
   "setA": 1,
   "line": 147,
   "fileName": "main.zkasm",
   "lineStr": "        %ADDRESS_GLOBAL_EXIT_ROOT_MANAGER_L2  => A"
  },
  {
   "CONST": "3",
   "setB": 1,
   "line": 148,
   "fileName": "main.zkasm",
   "lineStr": "        %SMT_KEY_SC_STORAGE => B"
  },
  {
   "CONST": "1",
   "setC": 1,
   "line": 149,
   "fileName": "main.zkasm",
   "lineStr": "        %LOCAL_EXIT_ROOT_STORAGE_POS => C"
  },
  {
   "freeInTag": {
    "op": ""
   },
   "inFREE": "1",
   "setA": 1,
   "sRD": 1,
   "line": 150,
   "fileName": "main.zkasm",
   "lineStr": "        $ => A                                          :SLOAD"
  }

SLOAD 的执行过程如下，先计算key, 然后再smt 中获取对应的value, 最后将storage action 保存。

        if (l.sRD) {
            pols.sRD[i] = 1n;

            const Kin0 = [ // 表示在合约中的存储位置
                ctx.C[0],
                ctx.C[1],
                ctx.C[2],
                ctx.C[3],
                ctx.C[4],
                ctx.C[5],
                ctx.C[6],
                ctx.C[7],
            ];

            const Kin1 = [  // 表示合约地址+SC storage
                ctx.A[0],
                ctx.A[1],
                ctx.A[2],
                ctx.A[3],
                ctx.A[4],
                ctx.A[5],
                ctx.B[0],
                ctx.B[1]
            ];

            const keyI = poseidon(Kin0);
            const key = poseidon(Kin1, keyI); // 生成SMT中的key 

            const res = await smt.get(sr8to4(ctx.Fr, ctx.SR), key);
            incCounter = res.proofHashCounter + 2;

            required.Storage.push({    
                bIsSet: false,
                getResult: {
                    root: [...res.root],
                    key: [...res.key],
                    siblings: [...res.siblings],
                    insKey: res.insKey ? [...res.insKey] : new Array(4).fill(Scalar.zero),
                    insValue: res.insValue,
                    isOld0: res.isOld0,
                    value: res.value
                }});

            if (!Scalar.eq(res.value,fea2scalar(Fr,[op0, op1, op2, op3, op4, op5, op6, op7]))) {
                throw new Error(`Storage read does not match: ${ctx.ln}`);
            }

            for (let k=0; k<4; k++) {
                pols.sKeyI[k][i] =  keyI[k];
                pols.sKey[k][i] = key[k];
            }

        } else {
            pols.sRD[i] = 0n;
        }

SSTORE

SSTORE 主要作用于A, B, C 寄存器中，例如以下所zkASM 片段：

;;;;;;;;;;;;;;;;;;
;; C - Verify and increase nonce
;;;;;;;;;;;;;;;;;;

        $ => A, E                       :MLOAD(txSrcOriginAddr) ; Address of the origin to A and E
        %SMT_KEY_NONCE => B
        0 => C
        $ => A                          :SLOAD
        $ => B                          :MLOAD(txNonce)
        $ => C                          :EQ
        C - 1                           :JMPN(invalidIntrinsicTx) ; Compare nonce state tree with nonce transaction
        B                               :ASSERT ; sanity check
        A + 1 => D
        E => A
        %SMT_KEY_NONCE => B
        0 => C
        $ => SR                         :SSTORE ; Store the nonce plus one

SSTORE 的执行过程如下，先根据寄存器A, B, C计算key, 然后再设置smt 中对应的value (D寄存器), 最后将storage action 保存。

        if (l.sWR) {
            pols.sWR[i] = 1n;

            if ((!ctx.lastSWrite)||(ctx.lastSWrite.step != step)) {
                ctx.lastSWrite = {};

                const Kin0 = [
                    ctx.C[0],
                    ctx.C[1],
                    ctx.C[2],
                    ctx.C[3],
                    ctx.C[4],
                    ctx.C[5],
                    ctx.C[6],
                    ctx.C[7],
                ];

                const Kin1 = [
                    ctx.A[0],
                    ctx.A[1],
                    ctx.A[2],
                    ctx.A[3],
                    ctx.A[4],
                    ctx.A[5],
                    ctx.B[0],
                    ctx.B[1]
                ];

                ctx.lastSWrite.keyI = poseidon(Kin0);
                ctx.lastSWrite.key = poseidon(Kin1, ctx.lastSWrite.keyI);

                // commented since readings are also done directly in the smt
                // ctx.lastSWrite.keyS = Fr.toString(ctx.lastSWrite.key, 16).padStart(64, "0");
                // if (typeof ctx.sto[ctx.lastSWrite.keyS ] === "undefined" ) throw new Error(`Storage not initialized: ${ctx.ln}`);

                const res = await smt.set(sr8to4(ctx.Fr, ctx.SR), ctx.lastSWrite.key, fea2scalar(Fr, ctx.D));
                incCounter = res.proofHashCounter + 2;

                ctx.lastSWrite.res = res;
                ctx.lastSWrite.newRoot = res.newRoot;
                ctx.lastSWrite.step = step;
            }

            required.Storage.push({
                bIsSet: true,
                setResult: {
                    oldRoot: [...ctx.lastSWrite.res.oldRoot],
                    newRoot: [...ctx.lastSWrite.res.newRoot],
                    key: [...ctx.lastSWrite.res.key],
                    siblings: [...ctx.lastSWrite.res.siblings],
                    insKey: ctx.lastSWrite.res.insKey ? [...ctx.lastSWrite.res.insKey] : new Array(4).fill(Scalar.zero),
                    insValue: ctx.lastSWrite.res.insValue,
                    isOld0: ctx.lastSWrite.res.isOld0,
                    oldValue: ctx.lastSWrite.res.oldValue,
                    newValue: ctx.lastSWrite.res.newValue,
                    mode: ctx.lastSWrite.res.mode
                }});

            if (!nodeIsEq(ctx.lastSWrite.newRoot, sr8to4(ctx.Fr, [op0, op1, op2, op3, op4, op5, op6, op7 ]), ctx.Fr)) {
                throw new Error(`Storage write does not match: ${ctx.ln}`);
            }

            // commented since readings are also done directly in the smt
            // ctx.sto[ ctx.lastSWrite.keyS ] = fea2scalar(Fr, ctx.D).toString(16).padStart(64, "0");
            for (let k=0; k<4; k++) {
                pols.sKeyI[k][i] =  ctx.lastSWrite.keyI[k];
                pols.sKey[k][i] = ctx.lastSWrite.key[k];
            }
        } else {
            pols.sWR[i] = 0n;
        }

Storage zkasm

对于Main_executor 生成的的storage action，交由storage zkasm ，执行其验证过程。

下面的代码首先判断storage action 执行的操作类型：

Run:

    ; Reset the registers to 0 before evaluate next input, if there aren't inputs, for the rest of the evaluations
    0 => HASH_LEFT, HASH_RIGHT, OLD_ROOT, NEW_ROOT, VALUE_LOW, VALUE_HIGH, SIBLING_VALUE_HASH, RKEY, SIBLING_RKEY, RKEY_BIT, LEVEL

    ${isGet()}              :JMPZ(Run_IsSetUpdate)
                            :JMP(Get)    // get 操作
Run_IsSetUpdate:
    ${isSetUpdate()}        :JMPZ(Run_IsSetInsertFound)
                            :JMP(Set_Update) // setUpdate 操作
Run_IsSetInsertFound:
    ${isSetInsertFound()}   :JMPZ(Run_IsSetInsertNotFound)
                            :JMP(Set_InsertFound) // setInsertFound 操作
Run_IsSetInsertNotFound:
    ${isSetInsertNotFound()}:JMPZ(Run_IsSetDeleteLast)
                            :JMP(Set_InsertNotFound)  //setInsertNotFound 操作
Run_IsSetDeleteLast:
    ${isSetDeleteLast()}    :JMPZ(Run_IsSetDeleteFound)
                            :JMP(Set_DeleteLast)    // setDeleteLast 操作
Run_IsSetDeleteFound:
    ${isSetDeleteFound()}   :JMPZ(Run_IsSetDeleteNotFound)
                            :JMP(Set_DeleteFound) // setDeleteFound 操作
Run_IsSetDeleteNotFound:
    ${isSetDeleteNotFound()}:JMPZ(Run_IsSetZeroToZero)
                            :JMP(Set_DeleteNotFound)  // setDeletNotFound 操作
Run_IsSetZeroToZero:
    ${isSetZeroToZero()}    :JMPZ(SetAllToZero)
                            :JMP(Set_ZeroToZero)  //setZeroToZero 操作

get 示例

从叶子节点一直向上计算，看新计算的root 是否和原始的一致。

    ; Root Node (same as before)                # end of tree
    ;  / \                                      |
    ;     Intermediate Node (same as before)    ^ climb tree
    ;      / \                                  |
    ;         Leaf Value Node (same as before)  * start here

首先判断value 是否为0，若不为0，则计算叶子节点的hash, 如下所示：

Get_ValueIsNotZero:

    ; Create the value hash and the leaf node hash, which will be the initial value of old root

    ; ValueHash = Hash0( VALUE_LOW, VALUE_HIGH )
    VALUE_LOW => HASH_LEFT
    VALUE_HIGH => HASH_RIGHT
    $ => HASH_RIGHT                 :HASH0

    ; OldRoot = LeafNodeHash = Hash1( Rkey, Hash( VALUE_LOW, VALUE_HIGH ) )
    RKEY => HASH_LEFT
    $ => OLD_ROOT                   :HASH1

                                    :JMP(Get_InitLevel)

然后从叶子点节一直向上，直接到根节点：

Get_ClimbTree:

    ; If we are at the top of the tree, then goto Get_Latch
    ${GetTopTree()}                 :JMPZ(Get_Latch) // 是否到达root 节点

    ; If next key bit is zero, then the sibling hash must be at the right (sibling's key bit is 1)
    ${GetNextKeyBit()} => RKEY_BIT
    RKEY_BIT                        :JMPZ(Get_SiblingIsRight)

最后执行，执行Get 验证：

Get_Latch:

    ; At this point consistency is granted: OLD_ROOT, RKEY (complete key), VALUE_LOW, VALUE_HIGH, LEVEL
                                    :LATCH_GET

    ; Return to the main loop
                                    :JMP(Run)

在storage exector中，对于iLatchGet的执行过程如下，主要有三个验证条件：

计算得到的root 和原始的root一致；
从Remaing key得到的key 和原始的key 一致；
最后得到的level 状态为 [1,0,0,0].

        // Latch get: at this point consistency is granted: OLD_ROOT, RKEY (complete key), VALUE_LOW, VALUE_HIGH, LEVEL
        if (rom.line[l].iLatchGet)
        {
            // Check that the current action is an SMT get
            if (action[a].bIsSet)
            {
                console.error("Error: StorageExecutor() LATCH GET found action " + a + " bIsSet=true");
                process.exit(-1);
            }

            // Check that the calculated old root is the same as the provided action root
            let oldRoot = [pols.oldRoot0[i], pols.oldRoot1[i], pols.oldRoot2[i], pols.oldRoot3[i]];
            if ( !fea4IsEq(fr, oldRoot, action[a].getResult.root) )
            {
                console.error("Error: StorageExecutor() LATCH GET found action " + a + " pols.oldRoot=" + fea42String(fr,oldRoot) + " different from action.getResult.root=" + fea42String(fr,action[a].getResult.root));
                process.exit(-1);
            }

            // Check that the calculated complete key is the same as the provided action key
            if ( pols.rkey0[i] != action[a].getResult.key[0] ||
                    pols.rkey1[i] != action[a].getResult.key[1] ||
                    pols.rkey2[i] != action[a].getResult.key[2] ||
                    pols.rkey3[i] != action[a].getResult.key[3] )
            {
                console.error("Error: StorageExecutor() LATCH GET found action " + a + " pols.rkey!=action.getResult.key");
                process.exit(-1);
            }

            // Check that final level state is consistent
            if ( pols.level0[i] != fr.one ||
                    pols.level1[i] != fr.zero ||
                    pols.level2[i] != fr.zero ||
                    pols.level3[i] != fr.zero )
            {
                console.error("Error: StorageExecutor() LATCH GET found action " + a + " wrong level=" + pols.level3[i] + ":" + pols.level2[i] + ":" + pols.level1[i] + ":" + pols.level0[i]);
                process.exit(-1);
            }

            logger("StorageExecutor LATCH GET");

            // Increase action
            a++;

            // In case we run out of actions, report the empty list to consume the rest of evaluations
            if (a>=action.length)
            {
                actionListEmpty = true;
                logger("StorageExecutor LATCH GET detected the end of the action list a=" + a + " i=" + i);
            }
            // Initialize the context for the new action
            else
            {
                ctx.init(fr, action[a]);
            }

            pols.iLatchGet[i] = 1n;
        }

set update 示例

对于叶子节点的更新，验证过程如下，分别根据旧的叶子节点值和新的叶子节点值，一直沿SMT 树向上计算，得到的旧的根节点和新的根节点，和原始的旧的根节和新的根节点是否一致。

    ; Root Node              Root Node (modified)                   # end of tree
    ;  / \                    / \                                   |
    ;    Intermediate Node       Intermediate Node (modified)       ^ climb tree
    ;     /\                      / \                               |
    ;       Old Value Node  --->     New Value Node (modified)      * start here

首先分别计算旧叶子节和新的叶子节点值：

   ${GetRkey()} => RKEY

    ; OldValueHash = Hash0( OLD_VALUE_LOW, OLD_VALUE_HIGH )
    ${GetOldValueLow()} => HASH_LEFT
    ${GetOldValueHigh()} => HASH_RIGHT
    $ => HASH_RIGHT                 :HASH0

    ; OldRoot = LeafNodeHash = Hash1( Rkey, Hash( VALUE_LOW, VALUE_HIGH ) )
    RKEY => HASH_LEFT
    $ => OLD_ROOT                   :HASH1

    ; NewValueHash = Hash0( VALUE_LOW, VALUE_HIGH )
    ${GetValueLow()} => VALUE_LOW, HASH_LEFT
    ${GetValueHigh()} => VALUE_HIGH, HASH_RIGHT
    $ => HASH_RIGHT                 :HASH0

    ; NewRoot = LeafNodeHash = Hash1( Rkey, Hash( VALUE_LOW, VALUE_HIGH ) )
    RKEY => HASH_LEFT
    $ => NEW_ROOT                   :HASH1

然后从叶子节点一直往上计算，直到根节点：

SU_ClimbTree:

    ; If we are at the top of the tree, then goto Get_Latch
    ${GetTopTree()}                 :JMPZ(SU_Latch)

    ; If next key bit is zero, then the sibling hash must be at the right (sibling's key bit is 1)
    ${GetNextKeyBit()} => RKEY_BIT  :JMPZ(SU_SiblingIsRight)

最后验证Latch_SET 操作：

SU_Latch:

    ; At this point consistency is granted: OLD_ROOT, NEW_ROOT, RKEY (complete key), VALUE_LOW, VALUE_HIGH, LEVEL
                                    :LATCH_SET

    ; Return to the main loop
                                    :JMP(Run)

在storage executor中，主要的验证条件有：

检查计算得到的root和action 中原始的旧的根一致；
检查计算得到的新的root 和 action中原始的新的根一致；
检查从remaining key 得到的key 和action中原始的key 一致；
检查最的level状态为[1,0,0,0]。

 // Latch set: at this point consistency is granted: OLD_ROOT, NEW_ROOT, RKEY (complete key), VALUE_LOW, VALUE_HIGH, LEVEL
        if (rom.line[l].iLatchSet)
        {
            // Check that the current action is an SMT set
            if (!action[a].bIsSet)
            {
                console.error("Error: StorageExecutor() LATCH SET found action " + a + " bIsSet=false");
                process.exit(-1); //@exit(-1);;
            }

            // Check that the calculated old root is the same as the provided action root
            let oldRoot = [pols.oldRoot0[i], pols.oldRoot1[i], pols.oldRoot2[i], pols.oldRoot3[i]];
            if ( !fea4IsEq(fr, oldRoot, action[a].setResult.oldRoot) )
            {
                let newRoot = [pols.newRoot0[i], pols.newRoot1[i], pols.newRoot2[i], pols.newRoot3[i]];
                console.error("Error: StorageExecutor() LATCH SET found action " + a + " pols.oldRoot=" + fea42String(fr,oldRoot) + " different from action.setResult.oldRoot=" + fea42String(fr,action[a].setResult.oldRoot));
                console.error("Error: StorageExecutor() LATCH SET found action " + a + " pols.newRoot=" + fea42String(fr,newRoot) + " different from action.setResult.newRoot=" + fea42String(fr,action[a].setResult.newRoot));
                process.exit(-1); //@exit(-1);;
            }

            // Check that the calculated old root is the same as the provided action root
            let newRoot = [pols.newRoot0[i], pols.newRoot1[i], pols.newRoot2[i], pols.newRoot3[i]];
            if ( !fea4IsEq(fr, newRoot, action[a].setResult.newRoot) )
            {
                console.error("Error: StorageExecutor() LATCH SET found action " + a + " pols.newRoot=" + fea42String(fr,newRoot) + " different from action.setResult.newRoot=" + fea42String(fr,action[a].setResult.newRoot));
                process.exit(-1);
            }

            // Check that the calculated complete key is the same as the provided action key
            if ( pols.rkey0[i] != action[a].setResult.key[0] ||
                 pols.rkey1[i] != action[a].setResult.key[1] ||
                 pols.rkey2[i] != action[a].setResult.key[2] ||
                 pols.rkey3[i] != action[a].setResult.key[3] )
            {
                console.error("Error: StorageExecutor() LATCH SET found action " + a + " pols.rkey!=action.setResult.key");
                process.exit(-1);
            }

            // Check that final level state is consistent
            if ( pols.level0[i] != fr.one ||
                 pols.level1[i] != fr.zero ||
                 pols.level2[i] != fr.zero ||
                 pols.level3[i] != fr.zero )
            {
                console.error("Error: StorageExecutor() LATCH SET found action " + a + " wrong level=" + pols.level3[i] + ":" + pols.level2[i] + ":" + pols.level1[i] + ":" + pols.level0[i]);
                process.exit(-1);
            }

            logger("StorageExecutor LATCH SET");

            // Increase action
            a++;

            // In case we run out of actions, report the empty list to consume the rest of evaluations
            if (a>=action.length)
            {
                actionListEmpty = true;

                logger("StorageExecutor() LATCH SET detected the end of the action list a=" + a + " i=" + i);
            }
            // Initialize the context for the new action
            else
            {
                ctx.init(fr, action[a]);
            }

            pols.iLatchSet[i] = 1n;
        }

Delete 示例

Delet过程如set update 过程类似，在此不再详细介绍。

    ; Root Node                                     Root Node (modified)                   # end of tree
    ;  / \                                           / \                                   |
    ;    Intermediate Node                              Intermediate Node (modified)       ^ climb tree
    ;     / \                                            / \                               |
    ;        Sibling Node (common RKEY lower bits)  --->    Intermediate Node (new)        ^ end of branch
    ;                                                        / \                           |
    ;                                                           Intermediate Node (new)    ^ climb branch
    ;                                                            / \                       |
    ;                                           (new) Sibling Node  New Value Node (new)   * start here

Storage PIL 约束

Storage PIL 主要是约束oldRook, newRoot, value, rKey, level，incCounter 计算过程的正确性。

include "poseidong.pil";

namespace Storage(%N);

    pol commit free0, free1, free2, free3;

    // Registers
    pol commit hashLeft0, hashLeft1, hashLeft2, hashLeft3;
    pol commit hashRight0, hashRight1, hashRight2, hashRight3;
    pol commit oldRoot0, oldRoot1, oldRoot2, oldRoot3;
    pol commit newRoot0, newRoot1, newRoot2, newRoot3;
    pol commit valueLow0, valueLow1, valueLow2, valueLow3;
    pol commit valueHigh0, valueHigh1, valueHigh2, valueHigh3;
    pol commit siblingValueHash0, siblingValueHash1, siblingValueHash2, siblingValueHash3;
    pol commit rkey0, rkey1, rkey2, rkey3;
    pol commit siblingRkey0, siblingRkey1, siblingRkey2, siblingRkey3;
    pol commit rkeyBit;
    pol commit level0, level1, level2, level3;
    pol commit pc;

    pol commit inOldRoot;
    pol commit inNewRoot;
    pol commit inValueLow;
    pol commit inValueHigh;
    pol commit inSiblingValueHash;
    pol commit inRkey;
    pol commit inRkeyBit;
    pol commit inSiblingRkey;
    pol commit inFree;
    pol commit inRotlVh;

    pol commit setHashLeft;
    pol commit setHashRight;
    pol commit setOldRoot;
    pol commit setNewRoot;
    pol commit setValueLow;
    pol commit setValueHigh;
    pol commit setSiblingValueHash;
    pol commit setRkey;
    pol commit setSiblingRkey;
    pol commit setRkeyBit;
    pol commit setLevel;

    pol commit iHash;
    pol commit iHashType;
    pol commit iLatchSet;
    pol commit iLatchGet;
    pol commit iClimbRkey;
    pol commit iClimbSiblingRkey;
    pol commit iClimbSiblingRkeyN;
    pol commit iRotateLevel;
    pol commit iJmpz;
    pol commit iJmp;
    pol commit iConst0, iConst1, iConst2, iConst3;
    pol commit iAddress;

    pol commit incCounter;
    incCounter' = incCounter*(1 - iLatchSet - iLatchGet - Global.L1) + iHash;

    // We assume hash and latch never goes together
    // We assume first instruction is not a latch nor a hash.

    // Selectors

    pol op0 =
        inOldRoot*oldRoot0 +
        inNewRoot*newRoot0 +
        inValueLow*valueLow0 +
        inValueHigh*valueHigh0 +
        inSiblingValueHash*siblingValueHash0 +
        inSiblingRkey*siblingRkey0 +
        inRkey*rkey0 +
        inFree*free0 +
        inRkeyBit*rkeyBit +
        inRotlVh*valueHigh3 +
        iConst0;

    pol op1 =
        inOldRoot*oldRoot1 +
        inNewRoot*newRoot1 +
        inValueLow*valueLow1 +
        inValueHigh*valueHigh1 +
        inSiblingValueHash*siblingValueHash1 +
        inSiblingRkey*siblingRkey1 +
        inRkey*rkey1 +
        inFree*free1 +
        inRotlVh*valueHigh0 +
        iConst1;

    pol op2 =
        inOldRoot*oldRoot2 +
        inNewRoot*newRoot2 +
        inValueLow*valueLow2 +
        inValueHigh*valueHigh2 +
        inSiblingValueHash*siblingValueHash2 +
        inSiblingRkey*siblingRkey2 +
        inRkey*rkey2 +
        inFree*free2 +
        inRotlVh*valueHigh1 +
        iConst2;

    pol op3 =
        inOldRoot*oldRoot3 +
        inNewRoot*newRoot3 +
        inValueLow*valueLow3 +
        inValueHigh*valueHigh3 +
        inSiblingValueHash*siblingValueHash3 +
        inSiblingRkey*siblingRkey3 +
        inRkey*rkey3 +
        inFree*free3 +
        inRotlVh*valueHigh2 +
        iConst3;

    // Setters

    hashLeft0' = setHashLeft*(op0-hashLeft0) + hashLeft0;
    hashLeft1' = setHashLeft*(op1-hashLeft1) + hashLeft1;
    hashLeft2' = setHashLeft*(op2-hashLeft2) + hashLeft2;
    hashLeft3' = setHashLeft*(op3-hashLeft3) + hashLeft3;

    hashRight0' = setHashRight*(op0-hashRight0) + hashRight0;
    hashRight1' = setHashRight*(op1-hashRight1) + hashRight1;
    hashRight2' = setHashRight*(op2-hashRight2) + hashRight2;
    hashRight3' = setHashRight*(op3-hashRight3) + hashRight3;

    oldRoot0' = setOldRoot*(op0-oldRoot0) + oldRoot0;
    oldRoot1' = setOldRoot*(op1-oldRoot1) + oldRoot1;
    oldRoot2' = setOldRoot*(op2-oldRoot2) + oldRoot2;
    oldRoot3' = setOldRoot*(op3-oldRoot3) + oldRoot3;

    newRoot0' = setNewRoot*(op0-newRoot0) + newRoot0;
    newRoot1' = setNewRoot*(op1-newRoot1) + newRoot1;
    newRoot2' = setNewRoot*(op2-newRoot2) + newRoot2;
    newRoot3' = setNewRoot*(op3-newRoot3) + newRoot3;

    valueLow0' = setValueLow*(op0-valueLow0) + valueLow0;
    valueLow1' = setValueLow*(op1-valueLow1) + valueLow1;
    valueLow2' = setValueLow*(op2-valueLow2) + valueLow2;
    valueLow3' = setValueLow*(op3-valueLow3) + valueLow3;

    valueHigh0' = setValueHigh*(op0-valueHigh0) + valueHigh0;
    valueHigh1' = setValueHigh*(op1-valueHigh1) + valueHigh1;
    valueHigh2' = setValueHigh*(op2-valueHigh2) + valueHigh2;
    valueHigh3' = setValueHigh*(op3-valueHigh3) + valueHigh3;

    siblingValueHash0' = setSiblingValueHash*(op0-siblingValueHash0) + siblingValueHash0;
    siblingValueHash1' = setSiblingValueHash*(op1-siblingValueHash1) + siblingValueHash1;
    siblingValueHash2' = setSiblingValueHash*(op2-siblingValueHash2) + siblingValueHash2;
    siblingValueHash3' = setSiblingValueHash*(op3-siblingValueHash3) + siblingValueHash3;

    rkey0' = setRkey*(op0-rkey0) + iClimbRkey*(climbedKey0-rkey0) + rkey0;
    rkey1' = setRkey*(op1-rkey1) + iClimbRkey*(climbedKey1-rkey1) + rkey1;
    rkey2' = setRkey*(op2-rkey2) + iClimbRkey*(climbedKey2-rkey2) + rkey2;
    rkey3' = setRkey*(op3-rkey3) + iClimbRkey*(climbedKey3-rkey3) + rkey3;

    siblingRkey0' = setSiblingRkey*(op0-siblingRkey0) + iClimbSiblingRkey*(climbedSiblingKey0-siblingRkey0) + iClimbSiblingRkeyN*(climbedSiblingKeyN0-siblingRkey0) + siblingRkey0;
    siblingRkey1' = setSiblingRkey*(op1-siblingRkey1) + iClimbSiblingRkey*(climbedSiblingKey1-siblingRkey1) + iClimbSiblingRkeyN*(climbedSiblingKeyN1-siblingRkey1) + siblingRkey1;
    siblingRkey2' = setSiblingRkey*(op2-siblingRkey2) + iClimbSiblingRkey*(climbedSiblingKey2-siblingRkey2) + iClimbSiblingRkeyN*(climbedSiblingKeyN2-siblingRkey2) + siblingRkey2;
    siblingRkey3' = setSiblingRkey*(op3-siblingRkey3) + iClimbSiblingRkey*(climbedSiblingKey3-siblingRkey3) + iClimbSiblingRkeyN*(climbedSiblingKeyN3-siblingRkey3) + siblingRkey3;

    rkeyBit' = setRkeyBit*(op0-rkeyBit) + rkeyBit;

    level0' = setLevel*(op0-level0) + iRotateLevel*(rotatedLevel0-level0) + level0;
    level1' = setLevel*(op1-level1) + iRotateLevel*(rotatedLevel1-level1) + level1;
    level2' = setLevel*(op2-level2) + iRotateLevel*(rotatedLevel2-level2) + level2;
    level3' = setLevel*(op3-level3) + iRotateLevel*(rotatedLevel3-level3) + level3;

    // Instruction that guarantees that op = hash(hl, hr); the poseidon SM will do the work; the result will be feeded by free
    iHash {hashLeft0, hashLeft1, hashLeft2, hashLeft3, hashRight0, hashRight1, hashRight2, hashRight3, iHashType, 0, 0, 0, op0, op1, op2, op3} in
        PoseidonG.LATCH {
            PoseidonG.in0,
            PoseidonG.in1,
            PoseidonG.in2,
            PoseidonG.in3,
            PoseidonG.in4,
            PoseidonG.in5,
            PoseidonG.in6,
            PoseidonG.in7,
            PoseidonG.hashType,
            PoseidonG.cap1,
            PoseidonG.cap2,
            PoseidonG.cap3,
            PoseidonG.hash0,
            PoseidonG.hash1,
            PoseidonG.hash2,
            PoseidonG.hash3};

    pol climbedKey0 = (level0*(rkey0*2 + rkeyBit - rkey0) + rkey0);
    pol climbedKey1 = (level1*(rkey1*2 + rkeyBit - rkey1) + rkey1);
    pol climbedKey2 = (level2*(rkey2*2 + rkeyBit - rkey2) + rkey2);
    pol climbedKey3 = (level3*(rkey3*2 + rkeyBit - rkey3) + rkey3);

    pol climbedSiblingKeyN0 = (level0*(siblingRkey0*2 + (1-rkeyBit) - siblingRkey0) + siblingRkey0);
    pol climbedSiblingKeyN1 = (level1*(siblingRkey1*2 + (1-rkeyBit) - siblingRkey1) + siblingRkey1);
    pol climbedSiblingKeyN2 = (level2*(siblingRkey2*2 + (1-rkeyBit) - siblingRkey2) + siblingRkey2);
    pol climbedSiblingKeyN3 = (level3*(siblingRkey3*2 + (1-rkeyBit) - siblingRkey3) + siblingRkey3);

    pol climbedSiblingKey0 = (level0*(siblingRkey0*2 + rkeyBit - siblingRkey0) + siblingRkey0);
    pol climbedSiblingKey1 = (level1*(siblingRkey1*2 + rkeyBit - siblingRkey1) + siblingRkey1);
    pol climbedSiblingKey2 = (level2*(siblingRkey2*2 + rkeyBit - siblingRkey2) + siblingRkey2);
    pol climbedSiblingKey3 = (level3*(siblingRkey3*2 + rkeyBit - siblingRkey3) + siblingRkey3);


    pol rotatedLevel0 = iRotateLevel*(level1-level0) + level0;
    pol rotatedLevel1 = iRotateLevel*(level2-level1) + level1;
    pol rotatedLevel2 = iRotateLevel*(level3-level2) + level2;
    pol rotatedLevel3 = iRotateLevel*(level0-level3) + level3;

    pol commit op0inv;
    pol opIsZero = 1-op0*op0inv;
    opIsZero*op0 = 0;
    pol doJump = iJmp + iJmpz*opIsZero;
    pc' = doJump*(iAddress - pc - 1) + pc + 1;

    // Last pc' must return to be pc=0 in order to close the program loop
    // Once the work is done, the rest of instructions must be:
    // if op0 = $n-1 (last instruction of the program) then pc=0 (jump to the beginning of the program)

    pol constant rHash;
    pol constant rHashType;
    pol constant rLatchGet;
    pol constant rLatchSet;
    pol constant rClimbRkey;
    pol constant rClimbSiblingRkey;
    pol constant rClimbSiblingRkeyN;
    pol constant rRotateLevel;
    pol constant rJmpz;
    pol constant rJmp;
    pol constant rConst0;
    pol constant rConst1;
    pol constant rConst2;
    pol constant rConst3;
    pol constant rAddress;
    pol constant rLine; // 0, 1, 2, ...
    pol constant rInFree;
    pol constant rInNewRoot;
    pol constant rInOldRoot;
    pol constant rInRkey;
    pol constant rInRkeyBit;
    pol constant rInSiblingRkey;
    pol constant rInSiblingValueHash;
    pol constant rSetHashLeft;
    pol constant rSetHashRight;
    pol constant rSetLevel;
    pol constant rSetNewRoot;
    pol constant rSetOldRoot;
    pol constant rSetRkey;
    pol constant rSetRkeyBit;
    pol constant rSetSiblingRkey;
    pol constant rSetSiblingValueHash;
    pol constant rSetValueHigh;
    pol constant rSetValueLow;

    {
        iHash, iHashType, iLatchGet, iLatchSet, iClimbRkey, iClimbSiblingRkey, iClimbSiblingRkeyN,
        iRotateLevel, iJmpz, iJmp, iConst0, iConst1, iConst2, iConst3, iAddress, pc,
        inFree, inNewRoot, inOldRoot, inRkey, inRkeyBit, inSiblingRkey, inSiblingValueHash,
        setHashLeft, setHashRight, setLevel, setNewRoot, setOldRoot, setRkey,
        setRkeyBit, setSiblingRkey, setSiblingValueHash, setValueHigh, setValueLow
    }
    in
    {
        rHash, rHashType, rLatchGet, rLatchSet, rClimbRkey, rClimbSiblingRkey, rClimbSiblingRkeyN,
        rRotateLevel, rJmpz, rJmp, rConst0, rConst1, rConst2, rConst3, rAddress, rLine,
        rInFree, rInNewRoot, rInOldRoot, rInRkey, rInRkeyBit, rInSiblingRkey, rInSiblingValueHash,
        rSetHashLeft, rSetHashRight, rSetLevel, rSetNewRoot, rSetOldRoot, rSetRkey,
        rSetRkeyBit, rSetSiblingRkey, rSetSiblingValueHash, rSetValueHigh, rSetValueLow
    }

主状态机约束

下面的代码展示了对Main_executor 执行结查的验证约束条件：

/////////
// Storage Plookpups
/////////
     // sKeyI 约束
    (sRD + sWR) {
        C0, C1, C2, C3, C4, C5, C6, C7,
        0, 0, 0, 0,
        sKeyI[0], sKeyI[1], sKeyI[2], sKeyI[3]
    } in
    PoseidonG.LATCH {
        PoseidonG.in0,
        PoseidonG.in1,
        PoseidonG.in2,
        PoseidonG.in3,
        PoseidonG.in4,
        PoseidonG.in5,
        PoseidonG.in6,
        PoseidonG.in7,
        PoseidonG.hashType,
        PoseidonG.cap1,
        PoseidonG.cap2,
        PoseidonG.cap3,
        PoseidonG.hash0,
        PoseidonG.hash1,
        PoseidonG.hash2,
        PoseidonG.hash3
    };
    
    // sKey 约束
    sRD + sWR {
        A0, A1, A2, A3, A4, A5, B0, B1,
        sKeyI[0], sKeyI[1], sKeyI[2], sKeyI[3],
        sKey[0], sKey[1], sKey[2], sKey[3]
    } in
    PoseidonG.LATCH {
        PoseidonG.in0,
        PoseidonG.in1,
        PoseidonG.in2,
        PoseidonG.in3,
        PoseidonG.in4,
        PoseidonG.in5,
        PoseidonG.in6,
        PoseidonG.in7,
        PoseidonG.hashType,
        PoseidonG.cap1,
        PoseidonG.cap2,
        PoseidonG.cap3,
        PoseidonG.hash0,
        PoseidonG.hash1,
        PoseidonG.hash2,
        PoseidonG.hash3
    };

    // sRD 约束
    sRD {
        SR0 + 2**32*SR1, SR2 + 2**32*SR3, SR4 + 2**32*SR5, SR6 + 2**32*SR7,
        sKey[0], sKey[1], sKey[2], sKey[3],
        op0, op1, op2, op3,
        op4, op5, op6, op7,
        incCounter
    } in
    Storage.iLatchGet {
        Storage.oldRoot0, Storage.oldRoot1, Storage.oldRoot2, Storage.oldRoot3,
        Storage.rkey0, Storage.rkey1, Storage.rkey2, Storage.rkey3,
        Storage.valueLow0, Storage.valueLow1, Storage.valueLow2, Storage.valueLow3,
        Storage.valueHigh0, Storage.valueHigh1, Storage.valueHigh2, Storage.valueHigh3,
        Storage.incCounter + 2
    };

    // sWR 约束
    sWR {
        SR0 + 2**32*SR1, SR2 + 2**32*SR3, SR4 + 2**32*SR5, SR6 + 2**32*SR7,
        sKey[0], sKey[1], sKey[2], sKey[3],
        D0, D1, D2, D3,
        D4, D5, D6, D7,
        op0 + 2**32*op1, op2 + 2**32*op3, op4 + 2**32*op5, op6 + 2**32*op7,
        incCounter
    } in
    Storage.iLatchSet {
        Storage.oldRoot0, Storage.oldRoot1, Storage.oldRoot2, Storage.oldRoot3,
        Storage.rkey0, Storage.rkey1, Storage.rkey2, Storage.rkey3,
        Storage.valueLow0, Storage.valueLow1, Storage.valueLow2, Storage.valueLow3,
        Storage.valueHigh0, Storage.valueHigh1, Storage.valueHigh2, Storage.valueHigh3,
        Storage.newRoot0, Storage.newRoot1, Storage.newRoot2, Storage.newRoot3,
        Storage.incCounter + 2
    };

首先通过Poseidon lookup 保证sKeyI, sKey 计算的准确性；

通过lookup, 实现主状态机 SMT 中set 和 get 的验证，即：

对于get 运算，主要比较oldRoot, rKey, value, incCounter 的一致性；
对于set运算，主要比较oldRoot, newRoot, rKey, value, incCounter的一致性。

参考

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