R1CS support for circuits

[cathieyun]

1. get r1cs → bp to work, using naive transformation https://github.com/dalek-cryptography/bulletproofs/pull/106 1.1 make sure r1cs → bp pads circuits if n is not 0 or a power of 2.
2. improve transformation to get rid of multiplications (simplify if only scalar mults)
3. improve r1cs → bp by bypassing matrices: https://github.com/dalek-cryptography/bulletproofs/pull/131

other tasks:

• benchmarking
• explore bellman <-> our r1cs
• convert bp to use ProverInput and VerifierInput
• move the arithmetic circuit code to a new file, so mod is more balanced

[cathieyun]

One thing we would like to do is to give the verifier the ability to check that the circuit is correctly formed. This is easy for circuits that don't incorporate challenges (e.g. simple multiplication or addition: can check that the circuit is correctly formed easily.) For circuits such as merge/split and shuffle circuits that incorporate challenges, this is not as straightforward because the verifier should be able to check that the challenges were generated honestly (as opposed to being chosen maliciously). How should we do this?

1. The prover generates the challenges by committing to the variables, and using ProofTranscript to generate a challenge variable. This way, the verifier can receive the commitments to the variables and also use ProofTranscript to generate a challenge variable, and check that the challenge variable is the same.
2. Have a generic API/struct for a circuit builder parameterized by T, where T is either a pair of a secret and its commitment (if you are the prover) or just the commitment (if you are the verifier). Then, both the prover and verifier could build up a circuit from scratch, given the information they have. They can both generate challenge values (same as explained in point 1), and then can use those challenge values to allocate_variable(T). Both the prover and verifier can create_circuit(), and should generate the same circuit if they have the same constraints and challenge variable.
3. Another solution?

I will start by implementing point 1. This is the most simple version, as it uses a provably-honestly-generated challenge value. The downside to this is that there isn't an elegant workflow for the verifier to check that the circuit is constructed honestly.

Re: discussion with @oleganza on PR #106

[hdevalence]

I think that this problem would go away if we finished the R1CS-to-proof work first; then the prover and verifier can use the transcript to construct a circuit with the challenge values already built in.

[cathieyun]

Thoughts on the R1CS representation: Currently, we have a ConstraintSystem represented by a list of triplets of LinearCombinations, where LC_a * LC_b = LC_c. This mirrors the bellman R1CS implementation closely.

However, this representation makes it difficult to create circuits that contain linear relations between several a_L, a_R, a_O variables. For instance, in a range proof circuit, a_L[0] appears in two LinearConstraints (one that checks whether or not it's a bit, and the other to check whether it is part of a valid representation of v). We wouldn't be able to express this in the current R1CS representation, without adding additional commitments.

So, there are two approaches - construct R1CS instances in the bellman-like way, and then have a process that prunes redundant commitments... or construct R1CS instances in a way that allows us to create LinearCombinations that contain multiple a_L, a_R, a_O variables. The latter seems a lot better. But then we have to have a way to determine the values of a_L, a_R, a_O from the R1CS instance, which is harder (or potentially impossible) to do if you define them this way.

I will take a shot at doing the latter. I don't have a good answer for how to determine the values of a_L, a_R, a_O yet, but will figure that out as I go.

[Pratyush]

One approach, that I outlined here is to introduce a new type of Variable that is an enum with LinearCombination and Var variants. So now a variable in your R1CS instance can be either an actual variable, or a linear combination of variables. The gist also contains an example of how to implement a FieldGadget having free addition using this technique.

[cathieyun]

I think we can close this issue now, since we have a constraint system proof in place!