Lasso
Last updated
Last updated
by Srinath Setty, Justin Thaler and Riad Wahby
This paper introduces , which is a lookup argument that allows an untrusted prover to commit to a vector and prove that all entries of reside in some predetermined table .
's performance characteristics unlock the so-called "".
A key difference of from other lookup arguments is that, if the table is structured(as we will explain later), then no party needs to commit to , enabling the use of enormous tables (e.g. of size or larger). Most common use cases of lookup argument, such as range checks, bitwise operations or big-number arithmetic, obtains huge benefits in cost from this characteristic of .
Imagine that a prover wishes to establish that at no point in a program's execution did any integer ever exceed .
A naive approach to accomplish this inside a circuit-SAT instance is to have the circuit take 128 field elements as its advice inputs, which constitute the binary representation of . The circuit checks that all 128 advice elements are in and they indeed equal to the binary representation of , i.e., . A single overflow check turns into at least 129 constraints and additional 128 field elements in witness.
Lookup tables offer a better approach. The verifier initializes a lookup table containing all integers between and . Then the overflow check above amounts to simply confirming that is in the table. Of course a table of size is way too large to be represented, even for the prover. This paper is devoted to describe the techniques to enable such a table lookup without requiring the table to ever be explicitly materialized by either of them. Indeed, the table in this example is highly structured in a way that it can be optimized using the techniques we will introduce.
's starting point is , which is an optimal polynomial commitment scheme for sparse multilinear polynomials from Spartan. Just as Spartan, can be instantiated with any multilinear PCS. Particularly for SNARKs that have the prover commit to the witness using a multilinear PCS, can be applied seamlessly to provide a lookup argument in either R1CS or Plonkish circuit satisfiability.
is a RISC-V-powered zkVM which achieved substantial improvements in front-end design by exploiting . replaces the instruction execution part of a zkVM circuit with by letting it look up into a gigantic evaluation table rather than evaluating it in a circuit. For each of the primitive RISC-V instructions, the resulting evaluation table has the structure that we require to apply for a significant reduce in the cost. Thaler states that and together essentially achieve a vision outlined by Barry WhiteHat called the - seeking to transform arbitrary computer program into circuits that only perform lookups.
The fact that the MLE of a function is unique offers the following method to represent any multilinear polynomial, which is briefer than its point-value representation or coefficient representation.
Proving the matrix-vector multiplication above is equivalent to confirming that
Equation (1):
Above equation can be simplified to:
Equation (2):
to the following checks:
Offline memory checking is a protocol between an untrusted memory and a trusted checker, which is the prover and the verifier in our protocol's context, respectively.
I skip the proof of the claim, but the example below demonstrates how the first direction of the claim holds. Three memory slots with addresses 1, 2 and 3 are initialized with values 100, 101 and 102. Three read operations at address 2, 2 and 3.
(1, 100, 0)
(1, 100, 0)
(1, 100, 0)
(1, 100, 0)
(1, 100, 0)
(2, 101, 0)
(2, 101, 0)
(2, 101, 0) (2, 101, 1)
(2, 101, 0) (2, 101, 1)
(2, 101, 0) (2, 101, 1) (2, 101, 2)
(2, 101, 0) (2, 101, 1)
(2, 101, 0) (2, 101, 1) (2, 101, 2)
(2, 101, 2)
(3, 102, 0)
(3, 102, 0)
(3, 102, 0)
(3, 102, 0)
(3, 102, 0) (3, 102, 1)
(3, 102, 1)
Specializing for Lasso
00
0
2
1
01
1
3
1
10
2
0
1
11
3
0
1
Generalizing the struct of lookup tables
Going back, we rewrite the Equation (2) as below:
Now the prover should prove that
Final PIOP is described below.
As they already explained in previous presentations, I skip the parts for Multilinear extensions, SNARKs, Polynomial commitment scheme, Polynomial IOP and the .
-sparse refers to multilinear polynomials in variables such that for at most values of . In other words, has at most non-zero coefficients in its multilinear Lagrange polynomial basis. If , only a tiny fraction of the possible coefficients are non-zero. If , we refer to such as a dense polynomial.
A multilinear polynomial can be represented uniquely by the list of tuples such that for all if and only if .
Here, is the canonical injection from to and is the inverse mapping. You can think of them as transformations between a field element and its binary representation.
We refer to as the dense representation of a sparse polynomial .
A multilinear polynomial in variables is a sparse multilinear polynomial if is sub-linear in . Otherwise, it is a dense multilinear polynomial.
For a lookup argument from to , it suffices for a prover to show that it knows a sparse matrix such that (1) for each row of , only one cell has a value of 1 and the rest are zeroes and that (2) .
Below demonstrates a simple example of demonstrating that is a valid lookup into the table . You can see that is indeed sparse.
for an randomly sampled by the verifier.
To run a sumcheck protocol on this equation to prove it, the verifier should be able to evaluate at some random succintly, i.e. with a cost independent of , regarding that the size of lookup table might be very large. Clearly, we cannot achieve this by committing to and using normal PCS.
is a sparse matrix where only elements out of are non-zero. Hence, the above is efficiently provable by having the prover commit to the sparse polynomial using , which is a generalization of for , and instead of commiting to the enormous , sending only its succint description assuming that it is structured in a way we define. Once we have such a commitment scheme, we instantly obtain the desired lookup argument.
, as explained above, is a polynomial commitment scheme for sparse polynomials. Let be a ()-variate multilinear polynomial with sparsity . The prover commits to a unique dense representation of the sparse polynomial , which is the list that specifies only the multilinear Lagrange bases with non-zero coefficients. When the verifier requests an evaluation , the prover returns the claimed evaluation along with the evaluation proof.
Let be such that without loss of generality. There is a simple algorithm that takes as input the dense representation of and outputs in time.
Decompose the variables of into blocks, each of size , writing . Then any ()-variate Lagrange basis polynomial evaluated at can be expressed as a product of smaller Lagrange basis polynomials. With cost of pre-computing a write-once memory, each basis polynomial can be calculated by memory look-ups and extra field operations.
Let , and .
Let for . Otherwise, for . Subscript 1, 2, and 3 each denotes the 2-bits length partition of the 6-bits binary string. is equal to .
Observe that the evaluation of on some can be decomposed in this way:
The memory is composed of subtables and where each is a table of size populated by the values from to . Each subtable can be computed by the prover in , leading to a total computation cost of .
Notice that this is cheaper with a factor of than a naive approach, whose cost is since there are Lagrange basis polynomials with variables.
The efficiency of the algorithm above comes from the fact that is sparse. is merely a SNARK as an argument that the prover correctly ran this algorithm on the committed description of . For simplicity, in the demonstrations below, we talk about the special case where and then expand it for a general result.
Let be a -sparse ()-variate multilinear polynomial, as we fixed the value of to be 2. For now, you can think of as an matrix with only nonzero elements.
When its dense representation is given, one can express its evaluation as below, by decomposing the ()-variate Lagrange basis polynomial into two ()-variate Lagrange basis polynomial.
Let's introduce three ()-variable multilinear polynomials , and , which extend the dense representation of . That is, iterates the m nonzero elements in in some canonical order, and for each , there exist some such that , and .
maps to each value of the nonzero elements and and maps to a corresponding location of it in (or, equivalently, to the index of each two subtables in Algorithm 1).
Let and each of which are ()-variate. We define a PIOP for proving the evaluation of at . We assume that is committed to beforehand.
: and as oracles.
: run the sumcheck reduction to reduce this statement
and .
where the claimed values are provided by and is randomly sampled by at the end of the sumcheck protocol.
: check if the three equalities above hold with an oracle query to each of the polynomials.
A key part of achieving a sound argument with the PIOP above is to enable the verifier to check that the committed and are built correctly, i.e.
.
Checking the above is equivalent to checking if an untrusted prover ran Algorithm 1 above (which is the case where and the two subtables correspond to and ), i.e., that the prover initialized the memory with correct values and the subsequent memory read operations occurred in a correct manner. We introduce offline memory checking, which is a protocol that reduces such memory consistency argument to a multiset equality check.
The checker maintains two local state sets : and . is initially empty. For -sized memory, is initialized as following : for all , the tuple is included. Here, the first element is the index, second one is the value and the third one is the accessed count of each memory slot.
For each read operation at address , suppose that the untrusted memory responds with a value-count pair . Then the checker updates its local state as follows:
store at address in the untrusted memory, and
.
If for every read operation, the untrusted memory returns the tuple last written to that location, then there exists a set with cardinality consisting of tuples of the form for all such that , where is simply the current memory view. Conversely, if the untrusted memory ever returns a value for a memory read which does not equal the value initially written to cell , then there does not exist any set such that .
You can see that there exist an such that , and the is equal to the final memory view.
Now we define the counter polynomials. Given the size memory and a list of addresses involved in read operations, one can compute two vectors and where stores the 'correct' count that would have been returned for -th read operation and stores the 'correct' final count stored at memory location after the read operations. Computing these requires operations over .
Let , , and . We refer to these polynomials as counter polynomials.
Regarding a ()-variate multilinear polynomial, suppose that () is committed in advance, and
are the polynomials sent by the prover at the beginning of the evaluation proof. Notice that the verifier can manually compute and .
If is correctly computed, i.e. ,
then the following holds : , where
and
The high-level conclusion of the memory checking above is that when is the polynomial that is produced by an untrusted memory, the checker (verifier) initializes the memory with which are the expected 'correct' values, and then by checking if the memory lookups are correctly done for each of the , the verifier is convinced that the provided is correct. The same logic is applied for .
In reality, the verifier doesn't perform the check above manually. Instead, to check that , two parties run a grand product argument, which is a multiset equality check that is performed via a GKR protocol whose circuit is simply a binary tree of multiplication gates. Since running a GKR protocol is reduced to a single evaluation of the input vector on a random value sampled by the verifier, and the verifier virtually has an oracle access to all of the required polynomials assuming they are committed by the prover (or is able to evaluate by himself), the memory check above can be done efficiently with a few evaluation proofs. For a more detailed explanation on the grand product argument, refer to of the paper.
We will generalize the above protocol, , so that it supports an arbitrary value for rather than a fixed value of 2, which implies that the gigantic lookup table can be decomposed into even smaller subtables of size .
Subsequently we will specialize for with some cost optimization exploiting the properties of lookup arguments. Eventually, we will further generalize by relaxing the conditions that make a table 'structured' for to be applied. With these modifications altogether, we introduce , as a sparse polynomial commitment scheme for and its final PIOP.
Supporting variables, rather than .
can be interpreted as the number of the subtables which are the result of decomposition of the original table of size . We can simply factor into a product of terms, instead of two terms, each of which are a -variate multilinear Lagrange basis polynomial. Hence, from this point, we use the notation of for , for representing the injection from a boolean hypercube to an index in each subtable, instead of and .
As we saw in Equation (1), the sparse matrix that we want to commit to can only have value 1 as its non-zero element. It means that the polynomial is also fixed to 1 and the commitment to it is unnecessary. We can save one polynomial to commit to with this per each lookup argument.
Furthermore, if we let and sample from and from (this means that each and represents the row index and column index of matrix ), since each row has exactly one non-zero element, is simply . can be evaluated by verifier on its own, thus there is no need for committing to it or proving its well-formness.
is a 4 x 4 matrix with sparsity of 4. Let be a two bits binary string for indexing 4 nonzero elements, i.e. . The table below is the description of mapping and . It is obvious that the mapping is simply an iteration from 0 to 3, which is virtually equal to . This is because there are exactly one nonzero element per each row. Therefore, it is unnecessary to commit to the polynomial , as well as . Check the table below.
We redefine the term 'structured' to be more comprehensive and well-defined for the properties that the lookup tables may have. If (1) a lookup table can be expressed as a tensor product of smaller tables (i.e. decomposible), and (2) for each subtable its multilinear extension polynomial can be evaluated quickly (i.e. MLE-structured), we regard such table as structured and Lasso can be applied.
Suppose that there is an integer and tables of size along with an -variate multilinear polynomial such that the following holds.
It means that each element of can be briefly expressed by each corresponding element in .
A table for a range check in the first example () can be easily expressed in the way above with and , for instance.
If and only if , the equation above holds, with a soundness error . In , after committing to (by committing to ) and , the verifier sends random sampled to see if above holds.
Let denote the unique nonzero column in row of . We can rewrite the LHS as following:
And with the decomposibility of ,
for some , above is equal to , using the sum-check protocol and
are built with correct lookups into the subtables , using the offline memory checking.
Assuming that the verifier can evaluates the MLE of each subtables quickly, both parties can participate in the protocol only with the short descriptions about the subtables, without ever fully materializing the entire lookup table throughout the protocol.
has committed to multilinear polynomials , each over variables.
: 2 different ()-variate multilinear polynomials , ,..., and different ()-variate multilinear polynomials , ..., .
// is purported to specify the values of each of the reads into .
// and are the "counter polynomials" for each memory slot of the subtables after the computation.
and apply the sumcheck protocol to the polynomial which reduces the check of the sum of on the boolean hypercube to : for .
: check if the above equalities hold with one oracle query to each .
// Up to this point, the correctness of is are not guaranteed yet. and runs the offline memory checking to check that equals for all .
: .
// In practice, instances of the sumcheck protocol below can be reduced to a single run of a sumcheck applied to random linear combinations of the polynomials.
: For , run a GKR-based grand products protocol to reduce the check to the following checks:
: check the equalities above with an oracle query to each of , , and .
Input : A polynomial commitment to the multilinear polynomials , and a description of a structured table of size .
sends a -commitment to the multilinear extension of a matrix . This consists of different ()-variate multilinear polynomials .
picks a random and sends to . makes one evaluation query to to learn .
and apply , allowing to prove that .
It's worth of noting that while at first glance it seems like increasing incurs an increase in the commitment size and verification cost in a factor linear to , since most of the PCS have efficient batching properties for evaluation proofs, the factor can be omitted (i.e. the prover and verifier costs for verifying polynomial evaluations do not grow with ).
The prover can compute its message for the sumcheck protocol with field operations where and is the number of monomials in . For many tables of practical interest, and factor can be eliminated (where has a 1 or 2 total degree, which is also the case of the range check example above), which gives total cost.
For the offline memory checking argument, the costs for the prover is similar to : field operations plus committing to a low-order number of field elements.
The verifier performs field operations. The costs of the memory checking argument, which can be batched, are identical to .
Written by