Polygon zkEVM storage狀態(tài)機

Storage State Machine 介紹

存儲狀態(tài)機負(fù)責(zé)zkProver存儲數(shù)據(jù)的所有操作隆圆。它從主狀態(tài)機獲收指令椎组，也稱為： $\textbf{Storage Actions}$ 严卖。 Storage Actions是一些典型的數(shù)據(jù)庫操作： Create, Read, Update, Delete (CRUD)使兔。

存儲狀態(tài)機事實上是一個微處理器默色，分為固件和硬件兩部分。

在固件部分設(shè)置邏輯規(guī)則壶笼，以JSON 格式存在 ROM 中。 zkASM 用來映射zkProver 主狀態(tài)機中的指令到其它狀態(tài)機中雁刷。在本例中覆劈，是映射到存儲狀態(tài)機的 Executor 中。主狀態(tài)機中的指令（Storage Actions），由Storage SM Executor 根據(jù)邏輯規(guī)則執(zhí)行责语。

硬件部分使用另外一種新的語言炮障，稱為PIL，專為zkProver 設(shè)計坤候，因為幾乎所有的狀態(tài)機將計算表述為多項式胁赢。狀態(tài)轉(zhuǎn)移必須滿足計算相關(guān)的多項式恒等關(guān)系。

存儲狀態(tài)機執(zhí)行所有的Storage Actions, 生成承諾和常量多項式白筹。

PIL 代碼用來檢查SM 相關(guān)的Actions 正確執(zhí)行智末，因此將承諾和常量多項式作為輸入。

為了實現(xiàn)零知識證明徒河，所有的數(shù)據(jù)以Merkle Tree的形式存儲系馆，這意味著存儲狀態(tài)機需要向其它狀態(tài)機發(fā)出請求，如Poseidon SM顽照，來執(zhí)行hashing 運算由蘑。

Storage SM 主要執(zhí)行SMT （Sparse Merkle Trees）上的計算，包含： CREATE代兵， READ, UPDATE, DELETE.

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

狀態(tài)機設(shè)計

zkProver 存儲中數(shù)據(jù)以SMT (Sparse Merkle Tree) 的形式存放植影，同時結(jié)合Merkle Tree 和 Patricia tree.

Merkle Trees

Merle 樹有 leaves, branches, root, 如下圖所示：

有相同父節(jié)點的稱為 siblings谓媒，例如 $B_{ab}$ 和 $B_{cd}$ 為 siblings。

使用Keys定位 Merkle 樹葉子節(jié)點

key中的 0 代表左邊何乎，1代表右邊句惯，例如對于 $( K_{\mathbfsmqrjgi} , V_{\mathbfbvw7hxb})$ , 其中 $K_{\mathbf6mcsfoe} = 10010110$ ，定位 $V_{\mathbfxte1zrv}$ 的過程如下：

首先讀取 $K_{\mathbfpvghndo} = 10010110$ 的最低位支救，為0抢野，因此從左邊遍歷樹，到達(dá) $B_{abcd}$ 各墨；
然后依次讀取倒數(shù)第2位指孤，為1，因此從右邊遍歷贬堵，到達(dá) $B_{cd}$ ;
再次讀取倒數(shù)第3位恃轩，為1，因此從右邊遍歷黎做，到達(dá) $H(V_d)$ .

由于 $H(V_d)$ 為葉子節(jié)點叉跛，因此對于 $K_{\mathbfksrhu7w}$ , $V_{\mathbf5kxi1cb}$ 的值即為 $H(V_d)$ 。

tree-address 用來表示 $V_x$ 在Merkle 樹的位置蒸殿，表示從根到達(dá) $L_d$ 的key bits, 但是為相反的順序筷厘，例如上述 $V_d$ 的tree-address 為 011鸣峭。

基本概念

level 用來表示從根節(jié)點定位到葉子節(jié)點的邊數(shù)，用 $lvl(\mathbf{L}_x)$ 表示酥艳，例如對于下面的示例：
$\begin{aligned} (\mathbf{K}_{\mathbf{a}} , V_{\mathbf{a}}),\ \ (\mathbf{K}_{\mathbf摊溶} , V_{\mathbf}),\ \ (\mathbf{K}_{\mathbf{c}} , V_{\mathbf{c}}),\ \ (\mathbf{K}_{\mathbf{c}}, V_{\mathbf{c}}),\\ (\mathbf{K}_{\mathbfkfx2po6}, V_{\mathbffdv0bpt}),\ \ (\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充石} = 10010010, K_{\mathbf{c}} = 10001010, &K_{\mathbfnjzkuvv} = 11100110,\\ K_{\mathbf{e}} = 11110101, K_{\mathbf{f}} = 10001011, K_{\mathbf{g}} = 00011111. \end{aligned}$
葉子節(jié)點的層級分別為：

$\text{lvl}(\mathbf{L}*_{\mathbf{a}}) = 2$ , $\text{lvl}(\mathbf{L}_*{\mathbf莫换}) = 4$ , $\text{lvl}(\mathbf{L}*_{\mathbf{c}}) = 4$ , $\text{lvl}(\mathbf{L}_*{\mathbffbfzo77}) = 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 葉子節(jié)點不僅存放值 $V_x$ 拉岁，還有未使用的從根節(jié)點定到葉子節(jié)點未使用的key-bits, 稱為remaining key, 用 $RK_x$ 表示。

例如上圖中7個葉子節(jié)點的remaing keys 分別為：

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

Fake-Leaf Attack

攻擊者可能將中間節(jié)點偽裝成葉子節(jié)葉膛薛，通過Merkle 驗證。

為了解決這個問題补鼻，對葉子和中間計算的時候分別采用不同的hash函數(shù)哄啄，即 $H_{leaf}$ 和 $H_{noleaf}$ 。

Non-Binding key-value pairs

攻擊可能根據(jù)現(xiàn)有的 $(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沒有綁定關(guān)系寇漫。為了解決這個問題刊殉，可以更改葉子節(jié)點的生成方式為：
$\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}$
然后構(gòu)建葉子節(jié)點為：
$\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值遍膜，然后聲明葉子節(jié)點 $L_x$ 包含 $V_x$ 的值。

READ 操作主要驗證葉子 $L_x$ 確實包含值 $V_x$ 瓤湘，采用Merkle 證明實現(xiàn)瓢颅。因此證明除了提供 $(K_x, HV_x)$ , 還需要root, $RK_x$ ，和所有必要的siblings弛说。

UPDATE Operation

UPDATE 操作包含兩步：

首先檢查 $\mathbf{READ}$ 操作挽懦；
沿著路徑重計算所有節(jié)點。

image.png

CREATE Operation

CREATE 操作添加新的葉子 $L_{new}$ , 插入到Merkle 樹中剃浇，鍵值對為： $( \mathbf{{K_{new}}} , \mathbf{V_{\mathbf{new}}} )$ 巾兆。

當(dāng)從root 定位的時候猎物， $\mathbf{K_{new}}$ 可能是空節(jié)點虎囚，或者是已經(jīng)存在的節(jié)點角塑，分別如下圖所示：

DELETE/REMOVE Operation

DELETE 操作刪除葉子節(jié)點，主要有兩種場景：

DELETE 操作等價于UPDATE操作淘讥，將非空的節(jié)點變成空節(jié)點圃伶， SMT 拓?fù)涔?jié)點不變；
DELETE 操作作為CREATE操作的反向過程蒲列，刪除一些擴展節(jié)點窒朋，會改變SMT 拓?fù)浣Y(jié)構(gòu)。

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\}$

構(gòu)建的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}$

反過來邢享，也可以根據(jù) Path-Bits 重構(gòu) Key鹏往。

POSEIDON Hash

POSEIDON SM 執(zhí)行Main SM 和 Storage SM 的指令，即計算這兩個SM消息的Hash值骇塘，并檢查其正確性伊履。

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

POSEIDON SM 有12個內(nèi)部的狀態(tài)款违，即： 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}$ 用來創(chuàng)建分支節(jié)點递惋， $\text{HASH1}$ 用來創(chuàng)建葉子節(jié)點柔滔，主要有參數(shù)hashType 決定。

Storage State Machine Design

Storage SM 主要由3部分組成：Storage Assembly code, Storage Executor code萍虽，和 Storage PIL 代碼睛廊。

Storage Assembly

Storage Assembly code 主要將主狀態(tài)機的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 主要根據(jù) Assembly 代碼邏輯規(guī)則超全，執(zhí)行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 值（生產(chǎn)環(huán)境下采用Postgre數(shù)據(jù)庫）蛾坯。

MemDB 構(gòu)造函數(shù)如下：

   /**
     * Constructor Memory Db
     * @param {Field} F - Field element
     * @param {Object} db - Database to load  // key-value 數(shù)據(jù)庫
     */
    constructor(F, db) {
        if (db) {
            this.db = db;
        } else {
            this.db = {};
        }
        this.F = F;
    }

MemDB相關(guān)的接口為：

//  設(shè)置SMT 樹的節(jié)點值，其中 `key` 為 長度為4 的數(shù)組疏遏，數(shù)組每個元素為64位脉课。`value` 為 64位元素值的數(shù)組。
     /**
     * Set merkle-tree node
     * @param {Array[Field]} key - key in Field representation
     * @param {Array[Field]} value - child array
     */
    async setSmtNode(key, value) {
       ...
    }
       

//  獲取 SMT 樹的節(jié)點值财异，其中 `key` 為 長度為4 的數(shù)組倘零，數(shù)組每個元素為64位。返回值為 64位元素值的數(shù)組戳寸。
   /**
     * 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) {
      ...
    }
 
      
   // 設(shè)置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位域元素的數(shù)組呈驶， value 為byte 數(shù)組   
    /**
     * Set program node
     * @param {Array[Field]} key - key in Field representation
     * @param {Array[byte]} value - child array
     */
    async setProgram(key, value) {
       ...  
    }  
      
   // key 為4個64位域元素的數(shù)組， 返回值為byte 數(shù)組   
    /**
     * 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)的構(gòu)造函數(shù)如下：

   /**
     * Constructor Sparse-merkle-tree
     * @param {Object} db - Database to use  // 數(shù)據(jù)庫-mebdb
     * @param {Object} hash - hash function // hash函數(shù)-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 兩個函數(shù)：

    /**
     * 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 路徑,以葉子節(jié)點向上直接根節(jié)點的所有中間節(jié)點 
     *      {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]

若插入一個節(jié)點：（key, value）

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

則SMT 根節(jié)點為： hashLeaf;

若挺入兩個節(jié)點：(key_0, value_0), (key_1, value)订晌，分別表示第一層的左右兩個葉子節(jié)點：

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])

得到的根節(jié)點即為 root虏辫。

get 函數(shù)有的接口如下：

   /**
    * 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) {
    ... 
   }

若能找到對應(yīng)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;
            }
        }

常量多項式構(gòu)建

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的執(zhí)行

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 的執(zhí)行過程如下，先計算key, 然后再smt 中獲取對應(yīng)的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 的執(zhí)行過程如下，先根據(jù)寄存器A, B, C計算key, 然后再設(shè)置smt 中對應(yīng)的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 ，執(zhí)行其驗證過程一疯。

下面的代碼首先判斷storage action 執(zhí)行的操作類型：

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 示例

從葉子節(jié)點一直向上計算撼玄，看新計算的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掌猛，則計算葉子節(jié)點的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)

然后從葉子點節(jié)一直向上，直接到根節(jié)點：

Get_ClimbTree:

    ; If we are at the top of the tree, then goto Get_Latch
    ${GetTopTree()}                 :JMPZ(Get_Latch) // 是否到達(dá)root 節(jié)點

    ; 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)

最后執(zhí)行眉睹，執(zhí)行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的執(zhí)行過程如下废膘，主要有三個驗證條件：

計算得到的root 和原始的root一致；
從Remaing key得到的key 和原始的key 一致慕蔚；
最后得到的level 狀態(tài)為 [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 示例

對于葉子節(jié)點的更新丐黄，驗證過程如下，分別根據(jù)舊的葉子節(jié)點值和新的葉子節(jié)點值坊萝，一直沿SMT 樹向上計算孵稽，得到的舊的根節(jié)點和新的根節(jié)點许起，和原始的舊的根節(jié)和新的根節(jié)點是否一致十偶。

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

首先分別計算舊葉子節(jié)和新的葉子節(jié)點值：

   ${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

然后從葉子節(jié)點一直往上計算，直到根節(jié)點：

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狀態(tài)為[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 過程類似，在此不再詳細(xì)介紹鹿寻。

    ; 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
    }

主狀態(tài)機約束

下面的代碼展示了對Main_executor 執(zhí)行結(jié)查的驗證約束條件：

/////////
// 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 計算的準(zhǔn)確性毡熏；

通過lookup, 實現(xiàn)主狀態(tài)機 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

?著作權(quán)歸作者所有,轉(zhuǎn)載或內(nèi)容合作請聯(lián)系作者

人面猴
序言：七十年代末财搁，一起剝皮案震驚了整個濱河市蘸炸，隨后出現(xiàn)的幾起案子，更是在濱河造成了極大的恐慌尖奔，老刑警劉巖搭儒，帶你破解...
沈念sama閱讀 222,183評論 6贊 516
死咒
序言：濱河連續(xù)發(fā)生了三起死亡事件，死亡現(xiàn)場離奇詭異提茁，居然都是意外死亡淹禾，警方通過查閱死者的電腦和手機，發(fā)現(xiàn)死者居然都...
沈念sama閱讀 94,850評論 3贊 399
救了他兩次的神仙讓他今天三更去死
文/潘曉璐我一進店門甘凭，熙熙樓的掌柜王于貴愁眉苦臉地迎上來稀拐，“玉大人，你說我怎么就攤上這事丹弱〉虑耍” “怎么了铲咨？”我有些...
開封第一講書人閱讀 168,766評論 0贊 361
道士緝兇錄：失蹤的賣姜人
文/不壞的土叔我叫張陵，是天一觀的道長蜓洪。經(jīng)常有香客問我纤勒，道長，這世上最難降的妖魔是什么隆檀？我笑而不...
開封第一講書人閱讀 59,854評論 1贊 299
?港島之戀（遺憾婚禮）
正文為了忘掉前任摇天，我火速辦了婚禮，結(jié)果婚禮上恐仑，老公的妹妹穿的比我還像新娘泉坐。我一直安慰自己，他們只是感情好裳仆，可當(dāng)我...
茶點故事閱讀 68,871評論 6贊 398
惡毒庶女頂嫁案：這布局不是一般人想出來的
文/花漫我一把揭開白布腕让。她就那樣靜靜地躺著，像睡著了一般歧斟。火紅的嫁衣襯著肌膚如雪纯丸。梳的紋絲不亂的頭發(fā)上，一...
開封第一講書人閱讀 52,457評論 1贊 311
城市分裂傳說
那天静袖，我揣著相機與錄音觉鼻，去河邊找鬼。笑死队橙，一個胖子當(dāng)著我的面吹牛坠陈，可吹牛的內(nèi)容都是我干的。我是一名探鬼主播喘帚，決...
沈念sama閱讀 40,999評論 3贊 422
雙鴛鴦連環(huán)套：你想象不到人心有多黑
文/蒼蘭香墨我猛地睜開眼畅姊，長吁一口氣：“原來是場噩夢啊……” “哼！你這毒婦竟也來了吹由？” 一聲冷哼從身側(cè)響起若未，我...
開封第一講書人閱讀 39,914評論 0贊 277
萬榮殺人案實錄
序言：老撾萬榮一對情侶失蹤，失蹤者是張志新（化名）和其女友劉穎倾鲫，沒想到半個月后粗合，有當(dāng)?shù)厝嗽跇淞掷锇l(fā)現(xiàn)了一具尸體，經(jīng)...
沈念sama閱讀 46,465評論 1贊 319
?護林員之死
正文獨居荒郊野嶺守林人離奇死亡乌昔，尸身上長有42處帶血的膿包…… 初始之章·張勛以下內(nèi)容為張勛視角年9月15日...
茶點故事閱讀 38,543評論 3贊 342
?白月光啟示錄
正文我和宋清朗相戀三年隙疚，在試婚紗的時候發(fā)現(xiàn)自己被綠了。大學(xué)時的朋友給我發(fā)了我未婚夫和他白月光在一起吃飯的照片磕道。...
茶點故事閱讀 40,675評論 1贊 353
活死人
序言：一個原本活蹦亂跳的男人離奇死亡供屉，死狀恐怖，靈堂內(nèi)的尸體忽然破棺而出，到底是詐尸還是另有隱情伶丐，我是刑警寧澤悼做，帶...
沈念sama閱讀 36,354評論 5贊 351
?日本核電站爆炸內(nèi)幕
正文年R本政府宣布，位于F島的核電站哗魂，受9級特大地震影響肛走，放射性物質(zhì)發(fā)生泄漏。R本人自食惡果不足惜录别，卻給世界環(huán)境...
茶點故事閱讀 42,029評論 3贊 335
男人毒藥：我在死后第九天來索命
文/蒙蒙一朽色、第九天我趴在偏房一處隱蔽的房頂上張望。院中可真熱鬧组题，春花似錦葫男、人聲如沸速和。這莊子的主人今日做“春日...
開封第一講書人閱讀 32,514評論 0贊 25
一樁弒父案，背后竟有這般陰謀
文/蒼蘭香墨我抬頭看了看天上的太陽。三九已至峻呕，卻和暖如春，著一層夾襖步出監(jiān)牢的瞬間趣效，已是汗流浹背瘦癌。一陣腳步聲響...
開封第一講書人閱讀 33,616評論 1贊 274
情欲美人皮
我被黑心中介騙來泰國打工，沒想到剛下飛機就差點兒被人妖公主榨干…… 1. 我叫王不留跷敬，地道東北人讯私。一個月前我還...
沈念sama閱讀 49,091評論 3贊 378
代替公主和親
正文我出身青樓，卻偏偏與公主長得像西傀，于是被迫代替她去往敵國和親斤寇。傳聞我的和親對象是個殘疾皇子，可洞房花燭夜當(dāng)晚...
茶點故事閱讀 45,685評論 2贊 360