Using Aurora/Ligero for Boolean Circuits

[DAHeath]

Hi!

We're interested in compiling a benchmark comparison between different ZK protocols. We'd like to include Aurora and Ligero in the comparison and were hoping we could use your library to do this.

Based on looking around the library a bit, there doesn't seem to be an obvious method for executing proof relations encoded as Boolean circuits. For example, we'd like to demonstrate that a prover knows the pre-image of an invocation of a call to SHA-256, where SHA-256 is encoded as a Boolean Circuit (e.g. http://stevengoldfeder.com/projects/circuits/sha2circuit.html).

(More precisely, the prover knows w such that H(w) = h where h is a publicly known value.)

Is there some way to achieve this with your library?

Any help would be appreciated!
David

[ValarDragon]

Aurora and Ligero both take as input Rank 1 constraint systems, which can be efficiently obtained arithmetic circuits with a fan-in of 2 for multiplication gates, and arbitrary fan-in for addition gates. They can't take in boolean circuits directly, the boolean circuit would have to be compiled into a Rank 1 Constraint system

For the particular problem of verifying a pre-image of SHA-256, there are rank 1 constraint systems already written for it, which could be used in libiop. It may be possible to include gadgets from GadgetLib into the libiop R1CS format, I'm not sure. (Gadgetlib sha256: https://github.com/scipr-lab/libsnark/blob/master/libsnark/gadgetlib1/gadgets/hashes/sha256/sha256_gadget.hpp)

If you just wanted a quick estimate, you could run instrument_aurora_snark with log_n = 15. SHA-256 takes ~27000 R1CS constraints, but Aurora requires the input matrices to have a power of two number of constraints, hence running it with 2^15 = 32k. The outputted prover time/verifier time/argument size of this should be very close to what you'd get for a single SHA256 invocation.

I haven't update the public repo in awhile (just haven't gotten around to it), but our internal repo has a 2x speed improvement over the current prover and verifier times of Aurora, at the same argument size. I'll try to update the public repo soon.

[DAHeath]

Thanks for the response!

Do you know of a tool that can convert general Boolean Circuits to rank 1 constraint systems? If not (or if it's a pain to run it), is there a method for computing the number of rank 1 constraints given a Boolean Circuit. My understanding is that it is essentially the number of Boolean gates times 3. Is this correct (I understand that in certain cases, this can be optimized, like in SHA-256).

Thanks again for your help!
David

[ValarDragon]

I don't know of any such tool. As a generic method, you can test that each variable of input to the circuit is boolean with 1 constraint per variable. You can handle an AND of n boolean variables with max(n - 1, 3)constraints. See https://github.com/daira/r1cs/blob/master/zkproofs.pdf for an explanation of that. I haven't worked out how many constraints n-ary OR is, I imagine its similar.

I imagine that there should be something better than direct application of the above for most large circuits though

[ValarDragon]

If you're still working on this, it turns out the method to make any of our SNARKs work for a boolean circuit is just an additional virtual oracle. You would use an additional virtual oracle that would assert that
fz(1 - fz) / Z_H = 0, which is equivalent to the assertion that "every variable in the assignment z is 1 or 0".

I am happy to give guidance on how to do this, if you're interested. It should be a fairly isolated change.