Ethsnarks / ethsnarks-il

Intermediate Language for zkSNARK circuits
GNU Lesser General Public License v3.0
7 stars 3 forks source link

Extra constraints and possible incompatibility issues in EthSnarks CircuitReader #3

Open akosba opened 5 years ago

akosba commented 5 years ago

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 YY = 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:

HarryR commented 5 years ago

Hi,

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

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 commented 5 years ago

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.