libsnark fails for circuits with checkNonZero depending on execution order

[rogermb]

Hi!

I recently ran into an issue when creating a circuit in which checkNonZero gets called on wires whose values themselves depend on the results of calls to checkNonZero. The jsnark circuit generation and evaulation work without any issues, but when libsnark gets called, it often fails with the error message The constraint system is not satisifed by the value assignment - Terminating.

The strange part is that whether libsnark fails or not seems to depend on the execution order / order of operations in circuit.arith. For instance, in the minimal(-ish) example I've included below, sumPrime.add(cPrime) works just fine while cPrime.add(sumPrime) causes the aforementioned error in libsnark. If I replace calls to checkNonZero with a gadget that simply ORs all bit wires together, I'm also unable to reproduce the libsnark exception.

I think the root cause of this issue is how NonZeroCheckBasicOp is implemented in CircuitReader.cpp. In addNonzeroCheckConstraint and mapValuesToProtoboard, there seems to be an assumption that when the non-checkNonZero circuit inputs are set, all inputs of checkNonZero are present and can be used to compute the value of an auxiliary wire, which ultimately doesn't hold if the inputs of checkNonZero themselves depend on the outputs of other calls to checkNonZero.

Given that NonZeroCheckBasicOp already has 2 output wires and the order of operations is correct inside jsnark, wouldn't it be possible to define the required auxiliary wire as a witness wire, assign its value in NonZeroCheckBasicOp.compute, and then just read in that value in libsnark? If you'd like, I could try to implement this in both jsnark and libsnark and create a pull request for both on your repos :smile:

Thank you very much for your work on this project!

Minimal example:

import circuit.eval.CircuitEvaluator;
import circuit.structure.CircuitGenerator;
import circuit.structure.Wire;

public class MinimalExample extends CircuitGenerator {

    public static void main(String[] args) {
        MinimalExample example = new MinimalExample();
        example.generateCircuit();
        example.evalCircuit();
        example.prepFiles();
        example.runLibsnark();
    }

    private Wire a, b, c;

    public MinimalExample() {
        super("MinimalExample");
    }

    @Override
    protected void buildCircuit() {
        a = createInputWire("a");
        b = createInputWire("b");
        c = createInputWire("c");

        Wire aPrime = a.checkNonZero("a nonzero"); // = 0
        Wire bPrime = b.checkNonZero("b nonzero"); // = 0
        Wire sumPlusOne = aPrime.add(bPrime, "sum").add(1, "sum + 1"); // = 1
        Wire sumPrime = sumPlusOne.sub(sumPlusOne.checkNonZero("sum nonzero")); // = 0
        Wire cPrime = c.checkNonZero("c nonzero"); // = 0

        // Works
        // Wire resultPlusOne = sumPrime.add(cPrime, "result").add(1, "result + 1"); // = 1

        // Doesn't work
        Wire resultPlusOne = cPrime.add(sumPrime, "result").add(1, "result + 1"); // = 1

        addOneAssertion(resultPlusOne, "result + 1 == 1");
    }

    @Override
    public void generateSampleInput(CircuitEvaluator evaluator) {
        evaluator.setWireValue(a, 0);
        evaluator.setWireValue(b, 0);
        evaluator.setWireValue(c, 0);
    }
}

Output:

Running Circuit Generator for < MinimalExample >
Circuit Generation Done for < MinimalExample >  
     Total Number of Constraints :  9
     Total Number of Wires : 19
Running Circuit Evaluator for < MinimalExample >
Circuit Evaluation Done for < MinimalExample >

-----------------------------------RUNNING LIBSNARK -----------------------------------------
Reset time counters for profiling
(enter) Parsing and Evaluating the circuit  [             ] (0.0000s x0.99 from start)
(leave) Parsing and Evaluating the circuit  [0.0001s x1.00] (0.0001s x1.00 from start)
Translating Constraints ... 
    Constraint translation done
Note: Protoboard Not Satisfied .. 
Assignment of values done .. 
Num constraints: 9
constraint 5 (no annotation) unsatisfied
<a,(1,x)> = 1
<b,(1,x)> = 0
<c,(1,x)> = 1
constraint was:
terms for a:
    1 * 0
    x_1 * 1
    where x_1 (no annotation) was assigned value 1
      i.e. negative of 21888242871839275222246405745257275088548364400416034343698204186575808495616
    x_6 * 1
    where x_6 (no annotation) was assigned value 0
      i.e. negative of 0
    x_9 * 1
    where x_9 (no annotation) was assigned value 0
      i.e. negative of 0
terms for b:
    1 * 0
    x_13 * 1
    where x_13 (no annotation) was assigned value 0
      i.e. negative of 0
terms for c:
    1 * 0
    x_12 * 1
    where x_12 (no annotation) was assigned value 1
      i.e. negative of 21888242871839275222246405745257275088548364400416034343698204186575808495616
The constraint system is  not satisifed by the value assignment - Terminating.

(edit:) The generated circuit file:

total 19
input 0          # The one-input wire.
const-mul-0 in 1 <0> out 1 <1>
input 2          # a
input 3          # b
input 4          # c
zerop in 1 <2> out 2 <5 6>      # a nonzero
zerop in 1 <3> out 2 <7 8>      # b nonzero
add in 2 <6 8> out 1 <9>        # sum
add in 2 <9 0> out 1 <10>       # sum + 1
zerop in 1 <10> out 2 <11 12>       # sum nonzero
const-mul-neg-1 in 1 <12> out 1 <13>
add in 2 <10 13> out 1 <14>
zerop in 1 <4> out 2 <15 16>        # c nonzero
add in 2 <16 14> out 1 <17>         # result
add in 2 <17 0> out 1 <18>      # result + 1
assert in 2 <18 0> out 1 <0>        # result + 1 == 1

[akosba]

Hi,

Thanks for catching this problem and for helping with the minimal examples!

I traced the problem and found that line 618 in CircuitReader.cpp needs to be zeroPwires.push_back(make_shared<LinearCombination>(*l));  instead of zeroPwires.push_back(l);. I will push the fix later with other unrelated changes after verifying that it works, but so far, the problem seems to be in this line only. The problem appears in the patterns that you described, and when it happens, it leads to an observable error.

By the way, you mentioned that the code you provided works if the other line that sets resultPlusOne is used. I checked both cases, and both did not work before the fix. In the first case, the error is as you reported. In the second case, there is another exception. Both problems are fixed by changing the line that I mentioned above, but I am curious about the different behavior in the second case. Please confirm if it works completely fine under the same input before applying the suggested fix above.

[rogermb]

Please confirm if it works completely fine under the same input before applying the suggested fix above.

I made the change to line 618 as you suggested, and everything works as it's supposed to now 🎉

I think I also found the reason why the first case (// Works) worked on my machine - I was actually using a fork of libsnark that seems to contain a workaround for the first bug; and I completely missed that commit when I created this issue 😅

Thank you so much for your help!