Adding support to call into external libsnark gadgets

[fleupold]

This pull request will allow people to call into external gadgets (e.g. libsnark's sha256_two_to_one_hash_gadget) by providing an executable that can respond to three commands

1. gadgetN size: returns the number of intermediate variables the gadget requires
2. gadgetN constraints a|b|c: returns the constraints for the a|b|c matrix in the form row column value
3. gadgetN witness [inputs]: given the inputs, generate a fulfilling assignment for the constraints in the gadget and return it as a list of values.

This will allow you to use highly optimized gadget for expensive operations (e.g. hashing) while still using the convenience pepper offers for iterations, conditionals and other high level processing code. An example .c file using the ext_gadget call can be seen here: https://pastebin.com/kMExVe3L

The pull request will contain out of three steps:

1. Add support for an ext_gadget function call in the frontend (similar to exo_compute)
2. In the backend, when reading the ext_gadget command insert the external R1CS into the R1CS we are currently building.
3. In the prover, when trying to process the ext_gadget command call into the gadget to get the witness instead of letting the prover run

I am planning to break this PR up into multiple commits to make it easier to review. Please feel free to comment with suggestions already now.
I'm more than happy to redesign or iterate on the approach if you think there is a better one.

[fleupold]

Added documentation and an example. Also made sure that the exo_compute example is still running and we can run the same gadget in a loop.

[fleupold]

I'm not sure here, if I have to use different intermediate variable names if a gadget is compiled multiple times per program (e.g. in a loop).

I ran an example where I do ten sha256 hashes and both proof as well as verification were successful.

However, it looks like it is reusing the intermediate variables from the first gadget, and thus I'm not sure if the computation is safe against tampering.

bin/ext_gadget_example.params looks like this:

  273057 //num_constraints
  512 //num_inputs
  257 //num_outputs
  27352 //num_vars

If we used separate variables for each gadget, we should end up with ~10x num_vars.

[maxhowald]

You definitely don't want to "re-use" the intermediate variables if you're doing multiple iterations of a sub-computation. There's no way for a variable in an arithmetic circuit to have multiple values at different points in the same computation, in the way that a piece of memory can change value in an ordinary computation.

So I think you do need to add something to the lines you mentioned in order to give each variable a unique name across every "instance" of the same gadget.

Can you post the code you used for running the gadget in a loop, though?

I tried duplicating the ext_gadget line a few times so the example computation looks like this:

#include <stdint.h>
 #define INPUT_SIZE 512
#define OUTPUT_SIZE 256
 struct In { uint32_t preimage[INPUT_SIZE]; };
 struct Out { uint32_t value[OUTPUT_SIZE]; };
 struct Hash { 
    uint32_t values[OUTPUT_SIZE];
};
 void compute(struct In *input, struct Out *output){
    struct Hash hash[1];
    ext_gadget(input->preimage,hash,0);
    ext_gadget(input->preimage,hash,0);
    ext_gadget(input->preimage,hash,0);
    ext_gadget(input->preimage,hash,0);
    ext_gadget(input->preimage,hash,0);

    int i;
    for (i = 0; i < OUTPUT_SIZE; i++) {
        output->value[i] = hash->values[i];
    }
}

I see the same thing you mentioned: increasing number of constraints, but same number of variables. But in this case, it seems like only the final call to ext_gadget should have any effect on the outputs. Rather than adding extra variables, perhaps the extra constraints should be optimized away as dead code...

A more interesting test case might be taking the output of the first gadget and using it as the input for the next round, but I couldn't make the types quite work out for this.

Relatedly, how did you generate the inputs for your example computation? When I use the default input generation function (in input_generation/ext_gadget_example_v_inp_gen.h) I get an assertion failure when trying to run the prover.

Specifically:

pepper_prover_ext_gadget_example: libv/computation_p.cpp:723: void ComputationProver::compute_ext_gadget(FILE*): Assertion `strcmp(value, outTokIt->c_str()) == 0' failed.

Adding some debugging, it looks like value is set to 1804289383 (which is the first line of prover_verifier_shared/gadget.input), and outTokIt->c_str() is set to 1.

[maxhowald]

If I change the input generation function from:

mpq_set_ui(input_q[i], rand(), 1);

to
mpq_set_ui(input_q[i], rand() % 2, 1);

Things work. I think this makes sense, since the input and output of the SHA-256 function should be 512 and 256 bits. Since you're not using any of Pepper's bitwise operations in your example, I don't think it actually matters one way or the other, but for other examples it might not be too efficient to put each bit into a separate 32 bit integer...

[fleupold]

Thanks for elaborating on the intermediate variable issue. I will add unique identifiers to make sure we don't "reuse" variables. My example involved setting a different value in the out->values array in each iteration, so that the computation could not have been optimised away.

Relatedly, how did you generate the inputs for your example computation?

I never used the input_generation, I just handcrafted a gadget.inputs file and used that one.

As for using separate elements for each bit vs packing them into one value, I believe the approach highly depends on the gadget you'd like to use. We could pack the 512 input bits into 3 field elements for sha256. The standard libsnark gadget expects 512 separate bits and also outputs 256 separate bits. I didn't want to change the gadget much, which is why I chose to leave it separate in this example.