Try   HackMD

Sin7Y Tech Review (31): Looking into Lookup Arguments

TL;DR

As mentioned in the previous article Hello, OlaVM!, OlaVM’s vision is to build a high-performance ZKVM, and this article will focus on one of the tools that make OlaVM high-performance, namely, Lookup Arguments. Lookup Arguments play an important role in reducing the size of the circuit, thereby improving Zero Knowledge efficiency, and it's widely used in the circuit design of ZKVMs. Throughout this article you'll learn more about the following:

  1. What role do Lookup Arguments play in ZKVM?
  2. Plookup protocol principles
  3. Lookup Argument protocol principle of Halo 2
  4. The connection between the two Lookup Argument algorithms

The roles of a ZKVM

The ZKVM utilizes Zero Knowledge to constrain all the execution processes of the VM, and the execution process of the VM can generally be divided into: instruction execution, memory access and built-in function execution. It is somewhat impractical to execute constraints on these operations in one trace. First of all, in a trace, a row represents an operation type, and one operation type corresponds to multiple constraints, and different constraints correspond to different numbers of columns, resulting in different widths. If one of the rows is too wide due to one constraint corresponding to too many columns, then the width of the entire trace is affected, becoming too large. Resource usage of this design is wasteful when the rows corresponding to the remaining constraints do not require so many columns. Then, if there are too many different operation types in a single trace, more selectors will be introduced, increasing not only the number of polynomials, but also the order of the constraint. Finally, due to the order limitation of the group, the number of rows of the trace itself cannot exceed the order of the group, so the number of trace rows occupied by a certain type of operation should be minimized.
So, for simplicity, we need to:

  1. Split different operation types into multiple sub-traces and prove them separately, with data consistency between the main trace and the sub-traces to be ensured by Lookup argument.
  2. For some ZK-unfriendly computations, we can reduce the size of the trace by Lookup Argument techniques, such as bitwise operations.
    Of course, there are other technical means to reduce the size of the trace, and that will be explained further down in this article.

Lookup between trace tables

All the execution processes of the VM will form a complete trace, called "the main trace". "Complete" refers to that it contains all the states of the VM execution, but not auxiliary states, such as some extended information that is convenient for ZK verification. As mentioned earlier, including this auxiliary information in the main trace will make the main trace complex and difficult to constrain. Therefore, for the convenience of constraints, some sub-traces are usually established, and then constrained for these sub-traces respectively, and the main traces are mainly used to execute the correct program constraints and Context constraints.

By creating different sub-traces, we divide the different operations performed by the VM and ensure that the data in the sub-trace is derived from the main trace by using Lookup Argument techniques. For the data validity proof in the sub-trace, you need to generate different traces according to a specific operation type, and then use the corresponding constraints to prove the validity of these traces. In particular, for zk-unfriendly operations such as Bitwise and rangecheck.

Lookup for ZK-unfriendly operations

As mentioned earlier, the proofs of each sub-trace are independent, so getting the smallest possible trace will improve the efficiency of prover. Taking Bitwise as an example, Bitwise operations include AND, XOR, and NOT. If you simply want to implement the constraints of Bitwise operations through circuits, you may need to split each OP into multiple binary limbs, and if these OPs are 32 bits wide, they will be split into 32 limbs. Then, you need to constrain that:

  1. Sumcheck: All bits combined together equals the original OP,
    a=2ilimb_ai
  2. Bitwise check per bit:
    limb_ailimb_bi=limb_ci

A total of 2+323=99 trace cells, and the number of constraints is 3 * sumcheck +33 bitwise=35.
If there are some truth tables at this time, for AND, XOR, and NOT calculations, you can define three tables, which contain data for bitwise calculations that refer to the op with a specified bit width, such as 8-bit. For 32-bit ops, you only need to split them into four 8-bit limbs, and then the bitwise relationship between these OP limbs does not need to be implemented with corresponding constraints, only needs to execute Lookup on the fixed table. At this time, a total of 3+4*3=15 trace cells are taken up with 3 constraints sumcheck and one Lookup argument (Batch Lookup is supported).

Utilizing Lookup Arguments is a huge boost not only for proofs of bitwise operations, but also for rangecheck operations. For a 32-bit OP, you only need to split it into two 16-bit limbs. There are two good designs here. One is that it allows rangecheck to take up fewer trace cells, and the other is that our customized ADD-MUL constraint can be reused for rangecheck’s sum constraint. For different calculation types, being able to reuse the same constraint is of great help to the overall efficiency improvement. As shown in the figure above, the customized ASS-MUL gate can support the constraint reuse of five calculation types: ADD, MUL, ADD-MUL, EQ, and RANGECHECK.

Plookup Protocol

Introduction

Plookup is a protocol used to check that a polynomial

fF<n[x] of the order less than n, the value on the multiplicative group
H
of n order is contained in a d-dimensional table
Fd
. A typical scenario is to do a rangecheck in a zk-snark, verifying that the values of all polynomials over
H
are on [0, m].

Symbol Description

  • H={g,...,gn+1}
    is a multiplicative group of order n+1 on
    F
    , and for
    fF[x]
    , if
    fi=f(gi),i[n+1]
    , then
    fi
    can be expressed as
    f(gi)
    , where
    [n+1]
    represents
    {1,2,3...,n+1}
  • The vector
    fFn
    can also be expressed by the polynomial
    fF<n[X]
    , where
    f(gi)=fi
    .
  • Given two vectors
    fFn
    ,
    tFd
    ,
    ft
    represents
    {fi}i[n]{ti}i[d]
    .

Pretreatment

  1. Suppose
    d=n+1
    • If
      dn
      , repeat the last element
      nd+1
      times.
    • d
      is at most
      n+1
      , because the group has only
      n+1
      order.
  2. The polynomial
    tF<n+1[X]
    represents the value of the lookup
    • t
      is
      n+1
      sets of finite field elements,
      t.degree()<n+1
      .
  3. The input polynomial is represented by
    fF<n[X]
    .

Protocol Process

  1. $s \in F^{2n+1} represents the combined vector of

    (f,t), and then two polynomial
    h1h2
    on
    F<n+1[X]
    to represent
    s
    :
    h1(gi)=si,i[n+1]

    h2(gi)=sn+i,i[n+1]

    • There are
      2n+1
      elements in
      s
      .
      h1
      represents
      {s1,s2,...,sn+1}h2
      represents
      {sn+1,sn+2,....,s2n+1}
      which means:
      h1(gn+1)=h2(g)=sn+1
  2. P calculates
    h1h2
    and sends it to a trusted third party
    I

  3. V randomly selects random numbers
    βγF
    in two finite fields
    F
    , and sends them to
    P

  4. P uses
    βandγ
    to calculate a polynomial
    ZF<n+1[X]
    , defined as follows:

    • Z(g)=1
    • For :
      i[2,n]

      Z(gi)=(1+β)i1Πj<i(γ+fj)Π1j<i(γ(1+β)+tj+βtj+1)Π1j<i(γ(1+β)+sj+βsj+1)(γ(1+β)+sn+j+βsn+j+1)
    • Z(gn+1)=1
  5. P sends
    Z
    to
    I

  6. V checks the correctness of
    Z
    , for each
    xH
    :

    • L1(x)(Z(x)1)=0
    • (xgn+1)Z(x)(1+β)(γ+f(x))(γ(1+β)+t(x)+βt(gx))=(xgn+1)Z(gx)(γ(1+β)+h1(x)+βh1(gx))(γ(1+β)+h2(x)+βh2(gx))
    • Ln+1(x)(h1(x)h2(gx))=0
    • Ln+1(x)(Z(x)1)=0
  7. V outputs acc if all the equations in step 6 are satisfied.

Protocol Understanding

  1. Define two polynomials
    F
    and 
    G
    :
    F(β,γ)=(1+β)nΠi[n](γ+fi)Πi[d1](γ(1+β)+ti+βti+1)

    G(β,γ)=Πi[n+d1](γ(1+β)+si+βsi+1)

    where
    FGd=n+1
    ,if and only if:
    • ft
    • s
      is the ordering of
      (f,t)
      with respect to
      t

This transfers the proof

ft to the proof
FG
, which is to prove that
s
is a permutation of
(f,t)
.

Prove that

ab is the prerequisite for
FG
to be true:
F(β,γ)=(1+β)n+d1Πi[n](γ+fi)Πi[d1](γ+ti+βti+11+β)

G(β,γ)=(1+β)n+d1Πi[n+d1](γ+si+βsi+1)1+β

For any
j[d1]
,there is
i[n+d1]
that makes
(tj,tj+1)=(si,si+1)

For (n*i) subscripts that are not listed above, there are always
si=si+1
and 2 sets of
{si}and{fi}
are equal,so
γ+si+βsi+11+β=γ+si=γ+fi

the prerequisite is true. Please refer to the paper for proof of sufficient conditions.

  1. What is

    Z of
    P
    in the calculation

    • Defined
      Z(gi)
      when
      i[2,n1]
      :
      Z(gi+1)=Z(gi)×(1+β)(γ+fi)(γ(1+β)+ti+βti+1)(γ(1+β)+si+βsi+1)(γ(1+β)+sn+i+βsn+i+1)
    • When
      i=1
      ,
      Z(g)=1
      , and when
      i=2
      ,
      Z(g2)=(1+β)(γ+f1)(γ(1+β)+t1+βt2)(γ(1+β)+s1+βs2)(γ(1+β)+sn+1+βsn+2)

      So the relations
      Z(gi+1)andZ(gi)
      are satisfied for
      i[1,n1]
      .
      When
      i=n
      ,
      Z(gn)=(1+β)n1(γ+f1)..(γ+fn1)×(γ(1+β)+t1+t2)..(γ(1+β)+tn1+tn)(γ(1+β)+s1+βs2)..(γ(1+β)+sn1+βsn)×(γ(1+β)+sn+1+βsn+2)..(γ(1+β)+s2n1+βs2n)

      Z(gn+1)=Z(gn)×(1+β)(γ+fn)(γ(1+β)+tn+βtn+1)(γ(1+β)+sn+βsn+1)(γ(1+β)+s2n+βs2n+1)=FG=1

      So the relations between
      Z(gi+1)andZ(gi)
      are satisfied for
      i[1,n]
      .
  2. What

    V is verifying:

    • V
      checks a and d to verify that
      Z(g)=1
      and
      Z(gn+1)=1
    • V
      checks c to verify that
      h1(gn+1)=h2(g)
      .
    • V
      checks b to verify that
      Z(gi+1)=Z(gi)×(1+β)(γ+fi)(γ(1+β)+ti+βti+1)(γ(1+β)+si+βsi+1)(γ(1+β)+sn+i+βsn+i+1)

      is satisfied for
      i[1,n]
      .

Further clarification of

Z,
F
and
G

Fi=(1+β)(γ+fi)(γ(1+β)+ti+βti+1)

Gi=(γ(1+β)+si+βsi+1)(γ(1+β)+sn+i+βsn+i+1)

Prove:
Πi[1,n]FiGi=1
,let
Ui=FiGi
,that is to prove
Πi[1,n]Ui=U1U2...Un=1

let
Z(g)=1

Z(g2)=U1

Z(g3)=U1U2

Z(gn)=U1U2...Un1
Z(gn+1)=1

And there is
Z(gn+1)=Z(gn)×Un
,so
U1U2...Un=1

Halo2 Lookup Protocol

Introduction

The lookup protocol function of Halo2 is to, given two columns of data

A and
S
with a length of
2k
, proving that every cell in
A
is in
S
, and some cells in
S
can not be in
A
, and

  • S
    can be fixed or variable.
    • The case where
      S
      is variable is the inclusion of columns in trace, and the values are not fixed.
  • A
    and
    S
    can contain duplicate data, and if the size of
    A
    and
    S
    does not reach
    2k
    , they need to be completed to
    2k
    .
    • Fill
      A
      with some data from
      S
      .
    • Complete
      S
      with the last data.

Protocol Process

  1. Let

    H={1,w,w2,...,w2k1}

  2. P calculates the permutations
    A
    and
    S
    of
    A
    and
    S

    • A
      is an ordering of
      A
      that places the same values on adjacent cells and randomly ranks between different values
    • S
      is an ordering of
      S
      , where the first cell of the different values in
      A
      has to be the same as the value in the corresponding row in
      S
      , and the other rows are random
    • A
      and S'$ satisfy
      Ai=Si
      or
      Ai=Ai1
  3. P calculates the polynomial
    Z
    :

    • Z0=Z2k=1
    • Zi+1=Zi×(Ai+β)(Si+γ)(Ai+β)(Si+γ)i[0,2k)
  4. V verifies
    A
    and
    S
    , and for each
    x
    on
    H
    , it satisfies:

    • (A(X)S(X))(A(X)A(w1X))=0
    • L0(X)(A(X)S(X))=0
  5. V verifies
    Z
    , and for each
    x
    on
    H
    , it satisfies :

    • Z(wX)(A(X)+β)(S(X)+γ)Z(X)(A(X)+β)(S(X)+γ)=0
    • L0(X)(1Z(X))=0
  6. V outputs acc if both the equations in 4 and 5 are satisfied.

The protocol only checks against the expanded relationship between

A and
S
. How is it guaranteed that the expansion is valid for
S
?

Suppose A = {1,2} and S = {3,4}, both of which do not satisfy the subset argument, are expanded to become A = {1,2,3,4} and S = {1,2,3,4}, which can be justified by the subset argument. It is unreasonable, but how can it be proved to pass?

Support ZK

  • Finally, add
    t
    rows of random numbers, and only use the first
    0u=2kt1
    rows to store the data
    • Put
      Z(x)
      in row
      u
  • Polynomials
    qblind
    set the last
    t
    row to 1 and the others to 0
  • Polynomials
    qlast
    set the row
    u
    to 1 and everything else to 0, which is the last row of data cell
  • Change the
    V
    validation to
    • (1(qlast(X)+qblind(X)))(Z(wX)(A(X)+β)(S(X)+γ)Z(X)(A(X)+β)(S(X)+γ))=0
    • (1(qlast(X)+qblind(X)))(A(X)S(X))(A(X)A(w1X))=0
      • Why add
        qlast(X)
        here? The row u stores
        Z(wx)
        and it does not need to participate in validation
    • L0(X)(1Z(X))=0
    • L0(X)(A(X)S(X))=0
    • qlast(X)(Z(X)2Z(X))=0
      • Z(wu)
        can be 1or 0, as there may be
        Ai+β=0
        or
        Si+γ=0

Extend - 1 : Vector Lookup

Suppose P has

ω polynomials
f1,...,fωF<n[X]
and a data table
t(Fω)d
of
d
rows and
ω
columns, and to prove that
j[n],(f1(gj),...,fω(gj))t
, you need to first convert and
{fi}i[ω]
to
{ti}i[ω]
the previous column of data.

  1. Calculate
    ω
    polynomials for the column
    ω
    of data in
    t
    , and the column
    i
    of polynomials
    tiF<d[X]ti(gj)=ti,j,j[d]
  2. V
    selects a random number
    α
    to send to
    P
  3. P
    recalculates the polynomial and data that require lookup
    • f:=Σiωαifi
    • t:=Σiωαiti
  4. P
    and
    A
    use
    f
    and
    t
    and for the previous lookup process

Extend - 2 : Multi-tables

Further, suppose

P has multiple data tables
t1,...,tl
, where
ti(Fω)d/l
for each
i[n]
we need to prove that
j=j(i)[l],(f1(gj),...,fω(gj))tj
. For example, prove that every row of data in the witness is in some data table. Like a vector lookup, you want to transfer this into a case with only one polynomial and one column of data.

  1. Form
    t1,...,tl
    tables into
    t(Fω+1)d
    , and add a column to each subtable
    • For each
      j[l]i[d/l]
      , there is a row of elements
      (j,(tj)i)
      in
      t
  2. Calculate the polynomial
    qF<n[X]
    ,
    q(gi)=j(i)
  3. Use Vector lookup to prove that
    (q(gi),f1(gi),...,fω(gi))ti[n]

Comparison between Plookup and Lookup

Both the Plookup protocol and Halo2’s Lookup protocol can prove that

ft, but the ideas behind the two protocols are different and their differences are as follows:

  • Plookup needs
    f
    and
    t
    to build a new sequence
    s
    , where both the elements in
    f
    and
    t
    appear at least once in
    s
    . It then proves
    st
    by comparing the non-zero distance sets of elements in
    s
    are equal, and finally
    fstft
    .
  • Halo2’s lookup proves
    ft
    directly, without the need to construct a new sequence, and is more concise than Plookup.
  • Both Plookup and Halo2 lookup require sorting and completing the set. Once completed, Plookup is
    |t|=|f|+1
    , and Halo2 Lookup is
    |t|=|f|=2k
    .