一文了解Lookup Arguments

Sin7Y ｜2022-12-19 17:30

本文將重點介紹使得OlaVM獲得高性能的工具之一，Lookup argument。

TL;DR

在上一篇文章Hello, OlaVM!中提到，OlaVM的願景是建立一個高性能的ZKVM，本文將重點介紹使得OlaVM獲得高性能的工具之一，Lookup argument。 Lookup argument對縮減電路規模，以提高ZK效率有很重要的作用，在ZKVM的電路設計中被廣泛應用，通過本篇文章你可以了解到：

1.Lookup argument在ZKVM中將發揮著怎樣的作用？

2.Plookup協議原理。

3.Halo2的Lookup argument協議原理。

4.兩個Lookup argument算法之間的聯繫。

The roles in ZKVM

所謂的ZKVM，其實就是用ZK約束VM所有的執行過程，VM的執行過程一般可以分為：指令執行，內存訪問，內置函數執行等。在一個trace裡執行對這些操作的約束看起來有點不切實際，首先，不同操作類型的約束對應不同的trace的寬度，如果其中一個約束對應的trace寬度特別大，就會造成其餘約束對應trace的浪費；然後，一個trace裡有太多不同的操作類型，就會引入更多的selector，不僅會增加多項式的個數，而且還會增加約束的階；最後，由於群的階限制，trace的行數不能超過這個群的階，因此，應該盡量減少某種類型的操作所佔用的trace行數。

因此，為了簡單，我們需要：

a.把不同的操作類型分成多個子trace，然後分別證明，主trace和子trace之間需要通過Lookup argument來保證數據的一致性。

b.對於一些ZK-unfriendly計算，我們可以通過Lookup argument技術來縮減trace的規模，比如位運算等。

當然，也有其他的一些技術手段來減少trace規模，我們將在後面的文章中給予說明。

Lookup between trace tables

VM所有的執行過程會組成一個完整的trace，稱為主trace，這裡的完整是包含VM執行的所有狀態，不會涉及到輔助狀態，比如，方便ZK驗證的一些擴展信息等；如前面所述，在主trace裡麵包含這種輔助信息，會使得主trace變得複雜，難於約束。因此，為了約束方便，通常會建立一些子trace，然後分別針對這些子trace進行約束，而主trace主要用來進行執行正確的程序約束和Context約束。

一文了解 Lookup Arguments

圖片1. Lookup between traces

通過建立不同的子trace，我們把VM執行的不同操作進行劃分，通過Lookup argument技術來保證了子trace的數據源於主trace。對於子trace裡的數據有效性證明，需要根據具體的操作類型，生成不同的trace，然後用對應的約束去證明trace的有效性；特別是對於bitwise，rangcheck等zk-unfriendly操作。

Lookup for ZK-unfriendly operations

如前面所述，每個子trace的證明是獨立的，所以獲得一個盡可能小的trace，會提高prover的效率。以bitwise為例，bitwise操作包含AND, XOR, NOT三種操作。如果想通過電路單純的實現對bitwise操作的約束，那需要做的可能是，把每個op拆成多個2進制的limbs，如果這些op是32bit位寬，那就會拆分成32個limbs。然後，你需要約束：

一文了解 Lookup Arguments

總共佔用3 + 32 * 3 = 99個trace cell，約束個數為3次sumcheck + 32次bitwise = 35個。

如果這個時候有一些真值表，對於AND, XOR, NOT計算，你可以定義三個表，這些表裡存的是指定位寬的op進行bitwise計算的數據，比如8bit。對於32bit的op，只需要把它們拆分成4個8bit的limbs，然後這些op的limbs之間的bitwise關係，也不用對應的約束去實現，只需要在fixed table裡進行Lookup即可，此時，總共佔用了3+ 4 * 3 = 15個trace cell，約束個數為3次sumcheck + 1 次Lookup argument（支持Batch Looup）。

一文了解 Lookup Arguments

圖2. Lookup in Arithmetic operations

Lookup argument不僅對bitwise操作的證明有極大的提升作用，對於rangeck操作同樣。對於32bit的op，只需要把他拆分成2個16bit的limbs即可；這裡有兩個很好的設計，一個是會使得rangecheck佔用更少的trace cells；另外一個是rangcheck的sum約束可以復用我們自定義的ADD-MUL約束。對於不同的計算類型，能夠復用同一個約束，對整體的效率提升具有很大的幫助，如上圖所示，對於自定義的ADD-MUL gate，它可以支持ADD,MUL,ADD-MUL,EQ ,RANGECHECK五種計算類型的約束復用。