來源：CertiK中文社區

爲了深入理解形式化驗證技術是如何應用於zkVM（零知識虛擬機）之上的，本文將聚焦於單條指令的驗證。關於ZKP（零知識證明）先進形式化驗證的總體情況，請查閱我們同期發布的“零知識證明區塊鏈的先進形式化驗證”文章。

什么是ZK指令的驗證？

zkVM（零知識虛擬機）能夠創建簡短的證明對象，以作爲證據來證明特定程序可以在某些輸入上運行、並成功終止。在Web3.0領域，zkVM的應用使得吞吐量變高，這是因爲L1節點只需要驗證智能合約從輸入態到輸出態轉變過程的簡短證明，而實際的合約代碼執行則可以在鏈下完成。

zkVM證明器首先會運行程序以生成每一步的執行記錄，然後將執行記錄的數據轉換爲一組數字表格（該過程被稱爲“算術化”）。這些數之間必須滿足一組約束（即電路），其中包括了具體表單元格之間的聯系方程、固定的常數、表間的數據庫查找約束，以及每對相鄰表行間所需要滿足的多項式方程（亦即“門”）。鏈上驗證可以由此確認的確存在某張能滿足所有約束的表，同時又保證不會看到表中的具體數字。

每條VM指令的執行都面臨很多這樣的約束，這裏我們將VM指令的這組約束簡稱爲它的“ZK指令”。下面是用Rust語言編寫的一個zkWasm內存加載指令約束的示例。

ZK指令的形式化驗證是通過對這些代碼進行形式化推理來完成的，我們首先將其翻譯成形式化語言。

即便只有單個約束包含錯誤，攻擊者都因此而有可能提交惡意的ZK證明。惡意證明所對應的數據表格並不對應智能合約的合法運行。與以太坊等非ZK鏈不同，後者有許多節點運行不同的EVM（以太坊虛擬機）實現，從而不太可能在同時同地出現相同的錯誤，一個zkVM鏈則只有單一的VM實現。單就這個角度而言，ZK鏈比傳統的Web3.0系統更爲脆弱。

更糟糕的是，和非ZK鏈不一樣，由於zkVM交易的計算細節並沒有被提交並存儲在鏈上，在攻擊發生後，不僅是要發現攻擊的具體細節非常困難，甚至要識別攻擊本身也會變得極具挑战性。

zkVM系統需要極爲嚴格的檢視，不幸的是，zkVM電路的正確性很難保證。

ZK指令的驗證爲何很難？

VM（虛擬機）是Web3.0系統架構中最爲復雜的部分之一。智能合約的強大功能是支撐Web3.0能力的核心，其力量源自於底層的VM，它們既靈活又復雜：爲了完成通用計算和存儲任務，這些VM必須能夠支持衆多的指令和狀態。比如，EVM的geth實現需要超過7500行Go語言代碼。類似的，約束這些指令執行的ZK電路也同樣龐大而復雜。像在zkWasm項目中，ZK電路的實現需要超過6000行Rust代碼。

zkWasm 電路架構

與專爲特定應用（如私人支付）設計的ZK系統中使用的專用ZK電路相比，zkVM電路的規模要大得多：其約束規則的數量可能比前者多出一到兩個數量級，而其算術化表格則可能包括數百列、含有數以百萬計的數字單元格。

ZK指令的驗證意味着什么？

我們在這裏想要去驗證zkWasm中的XOR指令的正確性。從技術上講，zkWasm的執行表對應一個合法的Wasm VM執行序列。所以宏觀來看，我們想要驗證的是：每次執行這條指令總是會產生一個新的合法的zkVM狀態：表中的每一行都對應VM的一個合法狀態，而緊接着的一行則總是要通過執行相應的VM指令來生成。下圖爲XOR指令正確性的形式化定理。

這裏“state_rel i st”表明狀態“st”是步驟“i”中智能合約的合法zkVM狀態。 正如你可能猜測的那樣，要證明“state_rel (i+1) …”不是輕而易舉的。

如何驗證ZK指令？

盡管XOR指令的計算語義很簡單，就是計算兩個整數的按位異或（bitwise xor）並返回整數結果，但它所涉及的方面卻比較多：首先，它需要從棧內存中取出兩個整數，進行異或計算，然後將這個計算得出的新整數存回同一個棧。此外，該指令的執行步驟應融入於整個智能合約的執行流程中，並且其執行順序及時機必須正確。

因此，XOR指令的執行效果應該是從數據堆棧中彈出兩個數，壓入它們的XOR結果，同時增加程序計數器，以指向智能合約的下一條指令。

不難看出，這裏的正確性屬性定義總體上與我們在驗證傳統字節碼VM（比如以太坊L1節點中的EVM解釋器）的時候所面對的情況非常相似。它依賴於機器狀態（這裏指棧內存和執行流）的高級抽象定義，以及關於每條指令預期行爲的定義（這裏指算術邏輯）。

然而，如我們下面所將要看到的，由於ZKP和zkVM的特殊性，其正確性的驗證過程經常與常規VM的驗證很不一樣。光是驗證我們這裏的單條指令，就要依賴於zkWASM中很多表的正確性：其中有一張用於限制數值大小的範圍表，一張用於二進制位計算中間結果的位表（bit table），一張每行都存儲恆定大小的VM狀態的執行表（類似物理CPU中的寄存器和鎖存器中的數據），以及代表動態可變大小的VM狀態（內存、數據棧和調用棧）的內存表和跳轉表。

第一步：棧內存

與傳統VM類似，我們需要確保指令的兩個整數參數可以從堆棧中讀取，並且其異或結果值被正確地寫回堆棧。堆棧的形式化表述看起來也相當熟悉（還有全局內存和堆內存，但XOR指令不使用它們）。

zkVM使用一種復雜的方案來表示動態數據，這是因爲ZK證明器並不能原生支持像堆棧或數組這樣的數據結構。相反的，對於壓入堆棧的每個數值，內存表用單獨的一行來記錄，其中的某些列則用於指示該表項的生效時間。當然，這些表的數據可以被攻擊者所控制，因此還必須加以一些約束，以確保表項真實對應於合約執行中的實際壓棧指令。這是通過精心計算程序執行過程中的壓棧次數來實現的。驗證每一條指令時，我們需要確保這個計數始終正確。此外，我們還有一系列引理，將單條指令生成的約束與實現堆棧操作的表查找和時間範圍檢查相關聯。從最頂層看，內存操作的計數約束定義如下。

第二步：算術運算

與傳統VM類似，我們希望確保位異或的運算正確無誤。這看起來很容易，畢竟我們的物理計算機CPU都能夠一次性完成這個操作。

但對於zkVM來說，這實際上並不簡單。ZK證明器原生支持的唯二算術指令是加法和乘法。爲了進行二進制位運算，VM使用了一個相當復雜的方案，其中一張表存放固定的字節級運算結果，另一張表則充當“草稿本”，用以在多個表行上展示如何將64位數字分解爲8個字節，然後再重新組合出結果。

zkWasm位表規範的片段

在傳統的編程語言中非常簡單的異或運算，在這裏則需要很多引理來驗證這些輔助表的正確性。對於我們的指令，我們有：

第三步：執行流

與傳統VM類似，我們需要確保程序計數器的數值正確更新。對於像XOR這樣的順序指令，每次執行步驟後，程序計數器需要加一。

由於zkWasm被設計用來運行Wasm代碼，因此也要確保在整個執行過程中，Wasm內存的不變性質始終得到保持。

傳統的編程語言對布爾值、8位整數、64位整數等數據類型有原生支持，但在ZK電路中，變量始終是在大素數（≈ 2254）模下的整數範圍內變化。由於VM通常以64位數運行，電路开發者需要使用一套約束系統來確保它們具有正確的數值範圍，而形式化驗證工程師則需要在整個驗證過程中追蹤關於這些範圍的不變性質。對執行流和執行表的推理會涉及到所有的其他輔助表，因此我們需要檢查所有表數據的範圍是否正確。

類似於內存操作數量管理的情形，zkVM需要一組類似的引理來驗證控制流。具體而言，每個調用和返回指令都需要使用調用棧。調用棧使用與數據棧類似的表方案來實現。對於XOR指令，我們並不需要修改調用棧；但驗證整條指令時，仍然需要追蹤並驗證控制流操作計數是否正確。

驗證這條指令

讓我們將所有步驟整合起來，驗證zkWasm XOR指令的端到端正確性定理。以下驗證是在交互式證明環境中完成的，其中每一個形式化構造和邏輯推理步驟都經過了最嚴格的機器檢查。

如上所見，形式化驗證zkVM電路是可行的。但這是一項艱巨的任務，需要理解和追蹤很多復雜的不變性質。這反映了被驗證軟件本身的復雜性：驗證中所涉及的每一條引理都需要得到電路开發者的正確處理。鑑於其中的風險很高，讓它們由形式化驗證系統進行機器檢驗，而不是僅僅依靠小心謹慎的人工審查，是非常有價值的。