Formal model for circuit randomization

[hdevalence]

Our implementation of the R1CS system differs from the one described in the paper.

We extended the system to allow randomized constraints, obtained as Fiat-Shamir challenges bound to the entire previous proof transcript data. This makes the system more powerful: for example, we can do a proof-of-shuffle asymptotically faster (O(n)) than described in the paper (O(n log n)).

Our initial iteration of this idea had the limitation that the randomness could only be bound to the values of the externally committed wires (the individual V commitments), but for Cloak we needed to be able to bind the randomness to the values of internal wires (committed to by the a_L, a_R, a_O vector commitments).

To solve this problem, @oleganza came up with a two-phase construction where the vector commitments are "split" and randomized, e.g. a_L = a_L' + e*a_L'', where a_L' is a vector with nonzero "phase 1" entries, a_L'' is a vector with nonzero "phase 2" entries, and e is a FS challenge. (More details on the construction are available in our internal documentation).

Before we can release this API, we need to a) formalize the model for these randomized constraint systems and b) have a security proof in that model.

We described this problem to @bbuenz last fall and at the Stanford Blockchain Conference in January. As of ZCon1 I think he said that he had suggested the problem to an MSc student but I don't remember the details. I think this work would be done best in the open; this GH issue is a good place to keep track of it, because it blocks release of the R1CS API.

[Pratyush]

The vRAM (Section III-D) and "Linear-Size Constant-Query IOPs for Delegating Computation" (should be online soon) papers formalize this sort of "interactive constraint generation"; maybe looking there can help?

[hdevalence]

Thanks for the reference!

[arthurgreef]

Hi - can you recommend another rust library for R1CS ZK proofs that we can use until yoloproofs is stable? Just thought I'd ask the experts. Thanks.

[oleganza]

Hi - can you recommend another rust library for R1CS ZK proofs that we can use until yoloproofs is stable? Just thought I'd ask the experts. Thanks.

I'm not aware of any ZKP library that can be considered stable. Very few ZKPs are widely deployed (what comes to mind is Zcash, Monero and Liquid), and those are also a moving target.

What does "stable" mean for you? To me, apart from the need for the formal proof as stated above, there's also a concern about API stability. On that, we have two data points: (1) the novel two-phase construction is entirely optional and even the proof size is smaller by 96 bytes if you don't use it; (2) we didn't break the API in over a year. So if your concern is some gigantic refactoring required in the future, that is as likely as having v1.0 today and deciding to make a much better v2.0 tomorrow. But for the hypothetical "v1.0" to be reasonably supported anyway, it needs to be actually used in deployed systems. Currently, we'd like to collect some feedback from people building on top of R1CS API (I myself is doing so with ZkVM) that may influence tweaks to the API, such as recent #313.

[arthurgreef]

Thanks. I think stable to me meant no security vulnerabilities. I'm not concerned about API changes. I'll start using the library right now if there is no concern about the proof. Thanks a ton.

[oleganza]

I'll start using the library right now if there is no concern about the proof.

Well, you only live once ;-)

[hdevalence]

My understanding is that there's not likely to be any problem with the construction, it's just that formalizing and proving correctness is a bunch of work, and nobody has done it yet. It should probably be done before someone deploys the proof system, but maybe someone who's hoping to make use of the deployment could put resources towards proving correctness....

[oleganza]

I've looked at plookup paper (commentary) recently and it seems like it needs more than two phases than our API currently provides.

TL;DR of plookup

1. make a map of valid inputs->outputs for a given bitwise function.
2. compress each line via a challenge-based polynomial into a single scalar (that includes input and output bits) => {t_i}
3. do the same for the actual wires at hand => {f_i}
4. commit to a sorted list of the wires concatenated with lookup table {t} => {s_i} = sort(f || t).
5. perform permutation check (aka "grand product check", aka shuffle gadget): Prod[(x-a_i)] == Prod[x-b_i] with these two vectors:

{a} = {s_i + β*s_(i+1)} // randomized difference between neighbours
{b} = (1+β)*f || {t_i + β*t_(i+1)}

where β is an extra random challenge.

This yields 2(|f| + |t|) multipliers, while one-by-one membership check would take |f|*|t| multipliers

The idea behind concatenation is that you'll have each value from lookup table found at least once. So if your program used it K times, it'll be found K+1 times.

And the randomized "difference" would mean that for K times there's a match, you'd find it in (1+β)*f subvector, and for K+1st match it'd be at "transition" from one value to a different one, and would match with {t_i + β*t_(i+1)} subvector

Why more phases?

1. In phase 1: commit to individual wires
2. In phase 2: sample a challenge to tuple-compress groups of wires into scalars for lookup and commit these values along with a sorted vector of them (sorted vector contains values computed with challenges).
3. In phase 3: sample another pair of random challenges to perform final product check with "randomized difference vectors" (one challenge for randomized difference, another - for sampling polynomials for the shuffle gadget).