[Bug] The implementation of `/` operator

[whbjzzwjxq]

In Circom language, / is defined as Multiplication by the inverse modulo p.

Circom version

circom compiler 2.1.0

Bug Description

Giving a test circuit:

pragma circom 2.0.0;

template Test() {
    signal input in1;
    signal input in2;
    signal output out;
    out <-- in1 / in2;
    log("Out: ");
    log(out);
    out * in2 === in1;
}

component main = Test();

If I provide {"in1": "0", "in2": "0"}, according to the definition of inverse modulo, the witness generator should throw out undefined-behavior, however, the witness generator outputs Out: 0.

Root cause

Run

circom ./test.circom --r1cs --c --sym --O0

This line out <-- in1 / in2; is translated to

Fr_div(&expaux[0],&signalValues[mySignalStart + 1],&signalValues[mySignalStart + 2]); // line circom 7

The definitions of Fr_div in fr.cpp:

void Fr_inv(PFrElement r, PFrElement a) {
    mpz_t ma;
    mpz_t mr;
    mpz_init(ma);
    mpz_init(mr);

    Fr_toMpz(ma, a);
    mpz_invert(mr, ma, q);
    Fr_fromMpz(r, mr);
    mpz_clear(ma);
    mpz_clear(mr);
}

void Fr_div(PFrElement r, PFrElement a, PFrElement b) {
    FrElement tmp;
    Fr_inv(&tmp, b);
    Fr_mul(r, a, &tmp);
}

According to the documentation of mpz_invert: https://machinecognitis.github.io/Math.Gmp.Native/html/e3072efb-05a9-947c-5532-6d806c157e4a.htm

If the inverse exists, the return value is non-zero. If an inverse doesn’t exist the return value is zero.
In that case, 0 has no inverse, so the return value is zero. However, the cpp code Circom translates doesn't handle this corner case.

Suggest Fix

Add a runtime error to handle this case.