Thanks CC for review and feedback
Intro
For years the central component of ZKPs was A* B + D == C. This check was applied repeatedly to build our full circuits. Any computation can be represented in this way. This representation is called R1CS.
It turns out R1CS is prohibitively expensive for certain tasks. This led to increased use of lookup arguments. Currently we use lookups and a variant of R1CS called polynomial constraints to build our circuits.
A lot of things are blocked if we want to build them using only r1cs. So the general flow is that some clever people get together and find efficient ways to arithmetise circuits. They create hand tuned circuits that include both polynomial constraints and lookup arguments. This is circuit specific and is not very scalable.
Polynomial constraints
Polynomial constraints are complicated. The circuit implementer makes many of these polynomial equations. The whole circuit is defined as a system of polynomial equations.
A solution to this system of equations makes a valid proof. It’s hard to reason about the results of systems of equations.
Formal verification tools cannot , at the moment, solve polynomial equations in a prime field.
Lookup arguments
Lookup arguments are set membership checks. They were first used to do efficient big integer arithmetic. Now used for that but also as control flow for VMs and to do operations that are not snark friendly. They are not more efficient for all operations. The cost per lookup introduces some prover cost. We currently try and use lookup arguments rarely because they are expensive in the prover
Why lookup arguments are good
Language
Currently snark friendly languages are very difficult for new programmers to learn. They use prime fields and polynomial constraints which are not a paradigm they are used to. A language that only uses lookup arguments could be much simpler. Current languages are good at doing computation that is specific to snarks but doing traditional computation is much more expensive. A lookup only language would be better on both counts.
Security review
Auditors are not used to finding solutions to a series of polynomial equations. Lookup arguments are much simpler to reason about.
Example:
Take a circuit is an AND of two input variables, the output is the result.
Lookup approach
out = get x,y from AND table
return(out)
The above lookup approach is much simpler than the polynomial approach shown next.
polynomial approach
(x)(x-1) = 0
y(y-1) = 0
x*y = out
return(out)
It is likely going to be much simpler to find bugs in lookup only circuits.
Formal verification
Formal verification tools need to solve the series of polynomial equations. Tools that solve these systems do not work well over prime fields. This leads to a lot of extra work being required to make a solver that works over a field. Using only lookup arguments would allow us to use already existing tools. It would also open up other methods for us to explore. Lookup arguments limit the set of valid variables at any point in the circuit. So we go from the set of possible variables being 2^{254} to being 2 or 2^{16}. This could even allow us to do things like state space enumeration to confirm our circuit is correct.
Information theory comparison
In order to effectively describe our program as a circuit we need to make a circuit that maps an input to the correct output. We can look at circuits as information encoded per second of prover time. This seems like a good way to compare the different ways we have of implementing circuits.
Polynomial constraints have limited degree. This is because the degree affects the prover time. The degree limits the information you can encode with them. You can make a polynomial that is degree 5 that can map 5 input values to 5 output values. You can’t include more values in the polynomial unless you increase the degree. In many cases this is fine because we use the structure of the polynomial constraint to do calculations. So multiplication is defined by a polynomial operation A * B == C but XOR is not and needs to be encoded as keys to values.
Lookup arguments can contain much more information. We have previously been limited in table size of 2^{28} elements. But recent work makes the limit of circuit size the maximum trusted setup you can feasibly complete. This limit on the table\_size. Baloo: Nearly Optimal Lookup Arguments. A single polynomial constraint can contain ~ 5 *2^{254} bits of information. Lookup arguments can contain 2^{254} * table\_size bits of information.
Polynomial constraints are very useful where you use the structure of the polynomial constraint. But as tables of bigger size become feasible this advantage will disappear.
Conclusions
If we can efficiently define circuits using lookup arguments only it will lead to simpler tooling and circuits.
Lookup arguments will become more efficient than polynomial constraints for almost everything with time.
We should start building the tooling for a lookup centric zkps
Future work
-
Compare efficiency of circuits right now.
-
Example lookup only language
-
Do a comparison of relative efficiency of various lookup arguments. Try and estimate the pace of improvements
-
Find examples where lookup arguments are better and worse than polynomial constraints
- Find the worst case examples for both
- Benchmark many circuits using: lookup arguments, lookup + polynomial constraints and compare them for efficiency