零知識證明的形式化驗證：內存證明方法

在對零知識證明系統進行形式化驗證時,內存子系統的處理是一個關鍵挑戰。與傳統虛擬機不同,zkVM使用執行表和輔助表來表示內存狀態,這需要特殊的驗證方法。

zkWasm的內存系統由執行表和內存表組成。執行表記錄了指令執行過程,而內存表則保存了所有內存訪問的歷史記錄。爲了簡化開發,zkWasm提供了抽象層,通過alloc_memory_table_lookup_write_cell和alloc_memory_table_lookup_read_cell兩個函數來操作內存。

在驗證過程中,我們將內存表視爲可變數據結構,通過memory_at函數構建地址數據映射。這樣可以證明alloc函數生成的約束等價於對映射進行的set和get操作,從而將指令驗證簡化爲類似非ZK解釋器的形式。

爲防止攻擊者操縱內存表,zkWasm採用了計數機制來追蹤有效條目數量。執行表和內存表分別維護計數器,通過約束確保兩者一致。這要求驗證時更加精確,需要證明每條指令對應正確數量的內存表條目。

驗證過程採用自頂向下的方式,包括三個步驟:

1. 預估指令應創建的條目數量
2. 證明表中條目數不多於預期
3. 通過歸納法證明cum_mops和instructions_mops在表中始終一致

這種詳細的驗證方法有助於發現潛在錯誤,如跳轉表計數機制中的一個關鍵問題。

爲實現模塊化驗證,我們將系統分爲三個獨立部分:指令電路驗證、執行表驗證和內存表實現。這種結構使多位工程師可以並行工作,提高驗證效率。

總的來說,zkVM驗證雖然在處理動態狀態時存在差異,但通過匹配實現中的抽象層,仍可以採用類似於傳統解釋器驗證的模塊化方法。這種方法最大限度地減少了差異帶來的影響,使得每條指令都能基於get-set接口進行獨立驗證。