Try   HackMD

Can Groth16 support lookups?

yes (sort of)

Huge thanks to Lúcás Meier @cronokirby for asking this question.


UPDATE: Weikeng Chen has suggested an even simpler version of this approach, which is relative to it in a similar way to how Pinoccio is related to Groth16.

This largely deprecates the "Pinoccio" approach. Brief explanation: instead of just separating private and public inputs as in normal Groth16, lets make a more refined separation of witness, by using few elements

γ1,...,γn, and the elements
Ci
belonging to a subset of a witness will be divided by
γi
. This will achieve the desired effect of witness commitment separation.


So, more precisely, the question asked was "can R1CS support lookups". There is, indeed, a very simple and natural extension of the R1CS language which can support lookups and all sorts of other interesting things.

Here, I will describe it, and suggest possible Groth16-style proof system for this language.

SR1CS

The instance of SR1CS (sequential rank 1 constraint system) is defined as follows:

It is a R1CS circuit, together with the splitting - the set of wires

S is split
S=S0S1...Sn
, and a special group of public inputs called "challenges" indexed from 1 to n, with the following properties:

  • The splitting is monotone: the output of the constraint lies in a subset with index
    of the argument indices.
  • The challenges of index i are assumed to live in
    Si
    .

Morally, it should be thought of as a sequential process: some constraint system is created, and then the verifier is asked for some challenges. In the next round, we add additional constraints (and additional wires), and maybe use challenges, and repeat the process.

I will not define witness here (because it encodes an interactive process), but knowledge of SR1CS means that we are able to respond to random challenges in this sequential process with overwhelming probability.

How to prove knowledge of SR1CS

There are, probably, few different ways of doing it (I could imagine staightforward one exposing KZG-commitment as public input IC, and then interfacing between them using this).

I will suggest a simple method based on KoE. I wonder if it can be improved.

UPD: yes, it can be improved, as suggested by Weikeng Chen.

Namely, lets assume that with each element

Ci (here, public inputs are also treated in the same way, I just don't write it down) of the standard Groth16 CRS, we are also given element
C~i=qjCi
, where
iSj
. Here,
q0,...,qn
are toxic waste.

Now, the following data is produced:

A,B,C,D0,...,Dn1,D~0,...,D~n // and
Dn
is calculated as
=C+ICD0...Dn
.

Here,

Di's are parts of our commitment to the witness
C+IC
corresponding to subsets
Si
, and
D~i
's are them multiplied by
qi
.

The following conditions need to be checked:

  1. Standard Groth16 equation.
  2. Pinoccio-style proofs of proportionality:
    Di,Qi=D~i,G
    , where
    Qi=[qi]2
    .
  3. Challenges are calculated as
    Hash(Di)

For example, normal lookup argument will then require 3 more group elements and 1 additional pairing check (because it only involves 1 challenge round).

Is it useful?

I am not sure, but I think yes.

The overhead of doing this is few more MSMs, but the crucial O(nlog(n)) part of producing the witness is completely unchanged.

I will try to compare R1CS to KZG-PlonK here.

  • Naive "narrow config" PlonK must be outperformed by SR1CS with this approach. Not only it is already outperformed without lookups, but in PlonK each lookup requires a column of full size. Here we will be completely unconstrained by this restriction.
  • Wide config likely loses by proof size, but might recover a bit because it is asymptotically better, requiring only smaller FFTs.
  • Custom gates are still a win for PlonK, but SR1CS might hold the ground because of the unlimited additions fan-in - in particular, wrongfield arithmetic must be advantageous.
  • It is possible that the access to challenges in R1CS unlocks more efficient lookup arguments that are the ones used in PlonK - though I'm not exactly sure.

It also potentially allows different kinds of useful arguments using challenges - Liam Eagan's MSM comes to mind.