ext_gadget.txt

This file provides some information on using ext_gadget() in
verifiable computations to inject arbitrary external constraint subsystems
that have can be compiled and verified outside of pepper.

You call ext_gadget like any other C function, but the compiler
treats it in a special way. When the prover is executing the
computation and solving the constraints, it will execute a
user-provided program as a child process. This program needs to respond to
three commands.

1. <exe> size: 	returns the number of intermediate variables the external subsystem 
				requires (used to allocate space in the pepper generated system)
2. <exe> constraints: returns the constraints as a list of the form:
					  [
						{indexA1: coeffA1, indexA2: coeffA2, ...}, 
						{indexB1: coeffB1, indexB2: coeffB2, ...}, 
						{indexC1: coeffC1, indexC2: coeffC2, ...}
					  ] 
3. <exe> witness [inputs]: Generate a fulfilling assignment for the constraints in the 
						   gadget and return it separated by a space (including inputs)

An example of ext_gadget in action can be found here:
    https://github.com/pepper-project/pequin/tree/master/pepper/apps/ext_gadget_example.c

The prototype for ext_gadget, were it actually a C function, would look
something like this:
    void ext_gadget(field_t *inputs, field_t *output, int gadget_number);
(where field_t represents a field element).

Some information about the arguments to ext_gadget:

  - inputs is an array of input variables provided to the gadget.

  - output is an array whose contents are set by the gadget when it
    computes the witness.

  - gadget_number tells the prover what executable to run. The number
    is appended to the string "gadget" (e.g., "gadget0"), and the prover
    will expect to find an executable of this name in the pepper/bin
    directory.

Each input value is provided as a large integer strings. 
Outputs from the program should be in a format that's
compatible with the libgmp function mpq_set_str().

We have an implementation of ext gadgets:
  https://github.com/pepper-project/pequin/tree/master/pepper/ext_gadget_bridge.cpp

To make the binary for the example bridge run `make gadget0` (or any other gadget_number you want to generate) from the pepper directory. This will create `bin/gadget0`.

If you want to see in more detail how the prover constructs the inputs
and interprets the outputs, here's the code in the prover that actually
handles ext_gadget calls:
    https://github.com/pepper-project/pepper/blob/master/compiler/frontend/src/SFE/Compiler/ExtGadgetStatement.java#L98-L112
	https://github.com/pepper-project/pepper/blob/master/compiler/backend/zcc_parser.py#L1674-L1712
	https://github.com/pepper-project/pepper/blob/master/pepper/libv/computation_p.cpp#L709