The produced r1cs constraints are not correct and do not represent the actual circuit

[mhgharieb]

Encoding a simple multiplexer:

$$f(s) = \begin{cases} 1 & if ~~ s = 0\ a & if ~~ s = 1\end{cases} $$

can be represented as the following circom code:

pragma circom 2.0.0;
template test(){
    signal input a;
    signal input s;
    signal output out;

    (s) * (s - 1) === 0; //check that s is binary
    out <== 1 + s * (a - 1);

}

component main {public [a, s]} = test();

After compiling it using the following command

circom --wasm --sym --r1cs  test.circom

I received the output:

template instances: 1
non-linear constraints: 2
linear constraints: 0
public inputs: 2
public outputs: 1
private inputs: 0
private outputs: 0
wires: 4
labels: 4
Written successfully: ./test.r1cs
Written successfully: ./test.sym
Written successfully: ./test_js/test.wasm
Everything went okay, circom safe

To show the constraints, I used the command snarkjs

snarkjs r1cs print test.r1cs test.sym

and the output was:

[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616 +main.s ] * [ main.s ] - [  ] = 0
[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.a ] * [ main.s ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0

Since the used prime $p = 21888242871839275222246405745257275088548364400416034343698204186575808495617$, so $21888242871839275222246405745257275088548364400416034343698204186575808495616 \equiv -1 \mod p$

and the constraints will be

[ -1 +main.s ] * [ main.s ] - [  ] = 0 
[ -1main.a ] * [ main.s ] - [ -1main.out ] = 0 

which equivalent to

$$ (s -1) \times s = 0$$

$$ a \times s - out = 0$$

The first constraint is correct and the second one is not correct.

[victorcrrd]

If you try the command circom --wasm --sym --r1cs --json test.circom, circom will also generate a file test_constraints.json that contains all the constraints. I got the same result as you using snarkjs, but checking the constraints generated by circom I get the correct ones, so I guess it might be a bug in the snarkjs code that prints the constraints. Moreover, I can guess where the bug is. If I compile the following circom code (note that the only change with your previous code is that in the second constraint, the -1 is changed with a 1)

pragma circom 2.0.0;
template test(){
    signal input a;
    signal input s;
    signal output out;

    (s) * (s - 1) === 0; //check that s is binary
    out <== 1 + s * (a + 1);

}

component main {public [a, s]} = test();

with circom --wasm --sym --r1cs test.circom and then run snarkjs r1cs print test.r1cs test.sym I get the following output:

[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616 +main.s ] * [ main.s ] - [  ] = 0
[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616 +21888242871839275222246405745257275088548364400416034343698204186575808495616main.a ] * [ main.s ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0

Note that the -1 that didn't appear before is now showing up. So I guess it has to do with the way the value 1 is printed (maybe to simplify and not show an irrelevant factor of 1).

Something similar happens if you change the second constraint in your circom code to out <== 1 + s * (a - 2);.

I guess you should create a new issue in the snarkjs repo.

[mhgharieb]

@victorcrrd thank you for the clarification.