Extra constraints and possible incompatibility issues in EthSnarks CircuitReader

[akosba]

Hi,

Thanks for your work on this tool.

In a recent issue reported in xjsnark, @sanchopansa mentioned that evaluating one of the xjsnark output circuits (which uses the same output format as jsnark) gave an error with the modified version of CircuitReader that EthSnarks has. The xjsnark circuits seemed to run normally with the original CircuitReader, so I tried to give a look, and thought to share some general findings and/or possible reasons for the issue. Feel free to correct me if I misinterpreted anything in the code, or let me know if any of the following was intentional for a reason.

Extra constraints: The original CircuitReader translates the input arithmetic circuit file in a way that matches the number of constraints reported by jsnark/xjsnark tools. However, the modified version used by EthSnarks seems to add many extra constraints that will lead to noticeable mismatches given the same input arithmetic files. This means that developers will not get the expected performance benefits of using tools like jsnark or xjsnark.
As an example, the sha256 circuit produced by jsnark results in about 26000 constraints, but using EthSnarks circuit reader with the jsnark circuit output will lead to about 37000 constraints. For other kinds of circuits, the amplification factor can be integer factors higher. (The simple circuit here will be translated to 7 constraints, instead of 2).
This can be verified by checking the QAP pre degree in the printed libsnark trace when running EthSnarks CircuitReader (the pinocchio executable) in test mode.

Not sure if there was a need to add those, but the extra constraints seem to appear in both addition and constant multiplication methods (handleAddition, handleMulConst and handleMulNegConst). Also, there is an additional binary check in the non-zero check. Checking that Y*Y = Y is not necessary, because the checks:
(X * M) = Y
X * (1 - Y) = 0
will guarantee that Y is either 0 or 1 as far as I can tell.
The pack operation as well can be represented with no constraints (but this change is not in the original circuit reader)

Possible incompatibility issues:

• The original circuit reader does not assume that inputs, nizkinputs or outputs will appear in a certain order, because jsnark/xjsnark can declare inputs/outputs at any arbitrary point. This is why there was some mapping logic in the original version. I was not able to verify that this takes place in the same way here. I also noticed that in EthSnarks CircuitReader the number of inputs to the protoboard was set as: this->pb.set_input_sizes(numInputs); while I think it should be numInputs + numOutputs. More details are in the second bullet here. This is also why both input and output variables were instantiated first here.

• In addNonzeroCheckConstraint, the output is assumed to be:
  auto& Y = varGet(outputs[0], FMT("zerop output", " (%zu)", outputs[0]));
  while I think it should be outputs[1] as in the original circuitreader (this selection of output wire was chosen in a compatible way with the Pinocchio compiler ). For example, this circuit produced directly by the Pinocchio compiler, uses the second zerop wire for the rest of the circuit. I was not also able to find where the value of M was set based on my quick look. In the original circuit reader, this was done in the mapValuesToProtoboard method.

[HarryR]

Hi,

I really appreciate the feedback, you have raised very insightful points.

• Ordering of inputs, nizkinputs and outputs: I had assumed they are ordered to avoid needing a mapping layer, with a general aim of being able to stream the constraints & witness while reading from input file.
• For addNonzeroCheckCostraint I will make more test cases to verify compatibility between Pinocchio, jsnark and xjsnark, using the correct output etc. The current tests are: https://github.com/HarryR/ethsnarks/tree/master/test/pinocchio

I was initially unsure about removing the binary check from the result of the zerop operation, but having checked again I agree, it's not possible for Y to be anything other than 0 or 1, so I can get rid of the redundant constraint.

I think it would be good for me to spend a week working on compatibility, test cases and verifying the constraints it emits are correct - I'm also looking at re-targeting the FairPlay SFDL compiler to output a compatible format.

[HarryR]

Another reason for the increase in the number of constraints is because of code I removed, but now I see the difference between the 7 constraints vs 2 constraints for examples.generators.SimpleCircuitGenerator. I removed the code needed to handle linear combination values, so while your one can truncate the expressions into a single constraint mine maps to at least 1 constraint per operation.