Polynomial is not Divisible

[MarkCampbell90]

Hello,
I compiled following circom program using circom v2.1.9 and the flags --O0, --r1cs, --sym, --wasm, --c, --json

pragma circom 2.1.9;

template main_template() {

    signal input a;
    signal input b;
    signal input c;
    signal input d;

    signal output out;

    // var e = 1;   // <------ OK
    var e = 0;      // <------- ERROR
    var f = 1;

    signal tmp0;
    tmp0 <-- (a / b);

    signal tmp1;
    tmp1 <-- (c / d);

    // out <== (tmp0 * tmp1 * e + tmp0 * f);    // <----- OK
    out <== tmp0 * ( tmp1 * e + f);      // <----- ERROR
}

component main = main_template();

But when I try to generate and verify a proof using the generate witness generation and snarkjs with PLONK or FFLONK as proof system I get following error:

[ERROR] snarkJS: Error: Polynomial is not divisible
    at Polynomial.divZh (/usr/local/lib/node_modules/snarkjs/build/cli.cjs:7694:27)
    at computeT (/usr/local/lib/node_modules/snarkjs/build/cli.cjs:8734:23)
    at async round3 (/usr/local/lib/node_modules/snarkjs/build/cli.cjs:8568:9)
    at async plonk16Prove (/usr/local/lib/node_modules/snarkjs/build/cli.cjs:8243:5)
    at async Object.plonkProve [as action] (/usr/local/lib/node_modules/snarkjs/build/cli.cjs:13586:36)
    at async clProcessor (/usr/local/lib/node_modules/snarkjs/build/cli.cjs:481:27)

While playing around with it, I found out that the error disappears when:

• using the --O1 or --O2 flag,
• changing the RHS to (tmp0 * tmp1 * e + tmp0 * f),
• changing the value of e to a non zero value.

The inputs seem not to affect the behavior as I can change them freely without affecting the error.
The inputs I used are:

{
    "a" : 4,
    "b" : 6,
    "c" : 8,
    "d" : 9
}

I found this behavior very strange, especially how the error is not triggered by applying any of the listed changes.
Is this something on the circom or the snarkjs side ?

[miguelis]

I am taking a look to this. Can you tell me exactly which steps do I need to make to get the error.

[MarkCampbell90]

Sure!

I copied the above code snipped into circuit.circom and the input into input.json.
Furthermore, I use a pre-computed ptau file from snarkjs (powersOfTau28_hez_final_11.ptau).

Now, following steps should reproduce the above error:

> circom --O0 --r1cs --wasm

> node circuit_js/generate_witness.js circuit_js/circuit.wasm input.json circuit.wtns

> snarkjs plonk setup circuit.r1cs powersOfTau28_hez_final_11.ptau circuit.zkey

> snarkjs plonk prove circuit.zkey circuit.wtns circuit.proof.json circuit.public.json

The error can also be reproduced using flonk instead of plonk or the cpp generation instead of wasm.
I hope this helps @miguelis :)

[Arvolear]

Hey, @MarkCampbell90, the error you are facing is due to the fact that the circuit has 0 constraints. When e == 0, the circom compiler optimizes the circuit by eliminating unused multiplications by zero. As a result, the expression tmp0 * (tmp1 * e + f) becomes non-quadratic, not generating a constraint.

[MarkCampbell90]

Hey @Arvolear,
Thank you for looking into this!

If it is an optimization problem why does it only occur with O0 but not with O1 and O2?
Additionally, the first expression (tmp0 * tmp1 * e + tmp0 * f) which does not lead to an error seems also easy to optimize compared to the failing tmp0 * ( tmp1 * e + f).

I find it weird that the optimizer has an effect on whether the proof generation fails or succeeds. Shouldn't a proper witness always pass the proof generation with snarkjs?
Is this the expected behavior?

[MarkCampbell90]

Also, the bug seems to occur even with quadratic constraints present.
The following code:

pragma circom 2.1.9;

template main_template() {

    signal input a;
    signal input b;
    signal input c;
    signal input d;

    signal output out;

    var e = 0;
    var f = 1;

    signal tmp0;
    tmp0 <-- (a / b);
    a === tmp0 * b;

    signal tmp1;
    tmp1 <-- (c / d);
    c === tmp1 * d;

    out <== tmp0 * ( tmp1 * e + f);
}

component main = main_template();

compiles with non-linear constraints: 3 and still produces the mentioned error.

[MarkCampbell90]

Here a minimal example:

pragma circom 2.1.9;

template main_template() {
    signal input a;
    signal input b;
    signal input c;

    signal output out;

    signal d;
    d <== a * b + c;

    out <== d * ( d * 0 + 1 );
}

component main = main_template();

[Arvolear]

I've managed to reduce the example to the following:

pragma circom 2.1.9;

template main_template() {
    signal input a;
    signal input b;

    signal output out;

    out <== a * (b * 0 + 1);
}

component main = main_template();

The thing is when the compiler is called without any optimization flags or either --O1 or --O2, it takes the branch of "simplification" and removes out <== a * (b * 0 + 1) as this expression doesn't produce a constraint. However, with --O0 flag, the circuit is taken as is, without any optimization whatsoever. In the latter case, it seems like plonk zkey generator doesn't like this "half constraint expression" and fails to calculate the required polynomial... Though it is strange that this circuit works with groth16.

[MarkCampbell90]

This expression might not, but the d <== a * b + c; expression in my example is a quadratic constraint.
All the operands are unknown signals at compile time so the optimizer should not touch them right?
As far as I understood circom, this expression results in a quadratic-constraint inside of the compiled constraint system so the set of quadratic-constraint should not be empty, or is this assumption wrong?
So the expression out <== d * ( d * 0 + 1 ); should not matter since we already have a quadratic-constraint present.
Also when I run my example with the semantic equivalent statement out <== d; instead of out <== d * ( d * 0 + 1 ); the prover works fine. 🤔
It seems that something weird is happening with the expression d * ( d * 0 + 1 ) ...

[MarkCampbell90]

I think I understand now better what you meant with your explanation.
Replacing <== with <-- removes the error so the problem is actually the constraint generated by the out assignment and nothing else.

I played around with some equivalent expressions (see below), but the error still makes no sense to me.

out <== a;               // OK
out <== a * 1;           // OK
out <== a * (1 + 0);     // OK
out <== a * (1 + 0 * 1); // OK
out <== a * (1 + 0 * b); // ERROR
out <== a + a * (0 * b); // OK
out <== a + (0 * b);     // OK

// if b = 1
out <== a * (b + 0 * b); // OK

Are there any news on why this occurs just for this specific expression and why it does not happen for groth16 ?

[Arvolear]

Thanks for bringing this up. I am in the middle of plonk keys generation research, trying to figure this out. However, please don't expect anything certain on that matter soon. This does seem like a bug, yet for now I haven't been able to identify the error.

p.s.

I am not a core circom dev, so tackling this is quite a challenge 😁