This is a continuation and clarification of my previous post which was a very rough description of a possible scheme of adding lookups (and any other challenge arguments) to Groth16.
It generated some traction and comments. Mainly I would like to thank Weikeng Chen who gave me some references on similar approaches (based on LegoSNARK), and confirmed that it should be possible to get rid of all interfacing between different argument systems (which loosely works similar to Pinoccio), instead using a singular Groth16-styled equation.
It seems that it is, indeed, possible. I describe the protocol here, and provide a sketch of proof.
This turned out to be quite long, tbh. Can be skipped, but it makes sense to look on zero-knowledgness / soundness proofs here to make sense of my arguments for the UltraGroth.
Here,
Individual constraints, thus, correspond to the rows of the matrix:
Some subset of indices of the witness, is also called "public inputs", and will be exposed by the proof, and all others are private.
Now, we map the set of constraints to some set
Then, the R1CS problem can be reformulated as finding such witness vector
where
Now, lets recall how this problem is turned into a zk-proof.
We have the following toxic waste elements:
for
for
for
[…]
The Groth16 prover (given the solution to R1CS in the polynomial form described above) creates two random blinding scalars
and
And the verifier does the following check:
Let's see why this works:
First, unwind this check to see that it passes. I will calculate LHS and RHS (and abuse notation a bit to calculate by omitting casting it to multiplication group
LHS:
RHS:
Now, small modification of LHS makes clear that all terms with
LHS:
The rest is direct inspection.
Now, let's recall why this is perfectly zero-knowledge, and why this is computationally sound in algebraic group model.
Zero-knowledge: it is clear that
Note: even a stronger fascinating property, re-randomizability, holds. It means that having a correct proof triple (A, B, C) one can construct a new proof (A', B', C') uniformly randomly distributed in the space of all proofs, without knowing the original witness. This property will, sadly, be broken in my extended UltraGroth protocol.
Soundness in AGM: I won't go into details of AGM, but this has the following intuition: imagine that
and
And let's assume they succeed, i.e. the expressions satisfy
First, let's notice that
Ocurrence of
Now, let's see that in
Let us also notice that occurence of
Therefore, we are in a situation where
WLOG, lets modify
In this form, appeareance of any nonzero
The terms with
Hence,
Wlog, assume that there is no linear dependencies between nonzero
Assume also wlog that in such form no linear combination of
Now, we want to show that after such transformations
Similarly, all terms with
Assume, that our R1CS circuit is endowed with the additional structure. I.e., private section of the set of indices
Let's define the space
We define
Strategy of
We will call a full witness the set of such strategies, for each round, which, while being used successively, succeed with overwhelming probability for random challenges.
Definition: Algebraic witness is a solution of R1CS over the field of rational functions on the space of challenges
Algebraic witness trivially implies the aforementioned strategy.
It is useful to think about algebraic witnessess, but likely not so useful to work with them in practice - computations in the field of rational functions are not that friendly. I believe the mentioned above general definition in terms of strategies is a more adequate abstractions; i.e. in practice the witness to the circuit will be a bunch of functions executing some computations on the already computed part of the witness vector.
Now, we will emulate the challenge responses of the verifier, using Fiat-Shamir heuristic. Let's construct the following toxic waste:
and obtain the following reference string:
all as before, with
Now, for each round but the last, lets assume that the prover also exposes some point
Verifier, then, sends the set of challenge inputs
!! Note: it is important that we can not just put challenge to be the hash of j and C^(k), without running the risk of prover retroactively rewinding previous rounds without changing C^(k), which might be possible in some cases.
After we have run such process non-interactively, we have obtained the full witness vector
Honest prover, then, picks two more random values
for k < d as before
Then, the following equation (*) holds:
Full verification algorithm checks this equation, correctness of public input and correctness of challenges.
It is, in fact, a direct inspection. Only thing that sufficiently differs from normal Groth16 is the blinding factors. Let's see how it works: the factor
I claim that the honest verifier produces an uniformly random proof. Reason for this is the fact that
I feel a bit shaky here. Anyways, let's proceed and work in AGM + ROM for the hash. Then, we first prove the following lemma:
Lemma: Any solution to equation (*) is a valid solution to R1CS, and
The fact that solution to this equation in AGM leads to R1CS can be done with the following trick. Solution in AGM is solution in terms of some polynomials (i.e. treating toxic waste as variables). Let's substitute in this solution
It is also easy to see that
Therefore, interactive protocol of communication with verifier (which we emulate by Fiat-Shamir) can be represented as follows: prover is providing some sequence of commitments to parts of the witness, and then generates a valid zk-proof with witness it had committed to.
I am not sure if I messed up here somewhere, requires proofread / review.