circom-prover: Bad bls12-381 proofs

[DragonDev1906]

Problem

I've come across a circuit that works with BN254 but fails with BLS12-381. This issue might be in the Arkworks code, but I don't know that for sure (my own code was based on the circom-prover implementation), so I'm reporting this here.

Implementation	bn254b	Bls12-381
snarkjs	valid	valid
circom-prover	valid	invalid

I'd have tried with the other ProverLib, but it only supports bn254. Most changes to the circuit result in verification returning Ok(true), so this does not seem to be an issue with my setup or the trusted setup files.

This is not a purely theoretical example, I've found this issue while using Multiplexer from circomlib.

I was able to verify proofs generated with snarkjs (on a larger circuit) using circom-prover, so this issue likely lies in zkey parsing, with how Arkworks is used/called or is an issue within Arkworks.

Details

Minimal circuit:

pragma circom 2.2.3;

template Demo {
    signal input in;
    signal output out;

    signal x <-- 1;
    out <== in * x;
}
component main = Demo();

Rust code:

fn main() {
    let zkey_path = "zkey/mux.zkey";
    let input_json = r#"{"in":["42"]}"#;

    let mut proof = circom_prover::CircomProver::prove(
        circom_prover::prover::ProofLib::Arkworks,
        circom_prover::witness::WitnessFn::RustWitness(|_| {
            // Hard coding witness for simplicity of setup/compilation.
            vec![
                1.into(),  // Constant (first signal is always 1)
                42.into(), // main.out
                42.into(), // main.in
                1.into(),  // main.x
            ]
        }),
        input_json.to_owned(),
        zkey_path.to_owned(),
    )
    .unwrap();

    let valid = circom_prover::CircomProver::verify(
        circom_prover::prover::ProofLib::Arkworks,
        proof,
        zkey_path.to_owned(),
    )
    .unwrap();

    assert!(valid);
}

input4.json
mux.r1cs.txt
mux.sym.txt
mux.vkey.json
mux.zkey.txt

Acceptance criteria

Proof verification should work for the circuit with both curves (as it does with snarkjs).

[vivianjeng]

I found that there are some problems with QAP computation
here is the fix
https://github.com/zkmopro/mopro/pull/698/changes
and here is the script for building the circuits, zkey
https://github.com/zkmopro/mopro/blob/2d986e8f1e950482cf31c7db9870663673fac102/circom/scripts/build_circuits.sh

try to use the circom-prover with

circom-prover = { git = "https://github.com/zkmopro/mopro", branch = "bls-script"}

[DragonDev1906]

This change worked for the simple/minified circuit I posted above, but the Multiplexer use below still fails on bls12381 while working on bn254. Same behavior: No errors but verify returns Ok(false). I did check with snarkjs that the witness is the same for both curves.

pragma circom 2.2.3;

include "circomlib/circuits/multiplexer.circom";

template Demo {
    signal input in;
    signal output out;

    component dotCheck = Multiplexer(1,2);
    dotCheck.inp[0][0] <== 0;
    dotCheck.inp[1][0] <== in;
    dotCheck.sel <== 1;
    dotCheck.out[0] ==> out;
}
component main = Demo();

fn main() {
    let zkey_path = "zkey/mux.zkey";
    let input_json = r#"{"in":["42"]}"#;

    let mut proof = circom_prover::CircomProver::prove(
        circom_prover::prover::ProofLib::Arkworks,
        circom_prover::witness::WitnessFn::RustWitness(|_| {
            // Hard coding witness for simplicity of setup/compilation.
            vec![
                1.into(),  // Constant (first signal is always 1)
                42.into(), // main.out
                42.into(), // main.in
                // 1.into(),  // main.x
                0.into(),
                1.into(),
                0.into(),
                42.into(),
            ]
        }),
        input_json.to_owned(),
        zkey_path.to_owned(),
    )
    .unwrap();

    let valid = circom_prover::CircomProver::verify(
        circom_prover::prover::ProofLib::Arkworks,
        proof,
        zkey_path.to_owned(),
    )
    .unwrap();

    assert!(valid);
}

Commands to test it works in snarkjs:

time circom circuits/mux.circom --r1cs --wasm --sym -o zkey -l circuits -p bls12381
snarkjs groth16 setup zkey/mux.r1cs ptau/bls12381_14.ptau zkey/mux.zkey
snarkjs zkey export verificationkey zkey/mux.zkey zkey/mux.vkey.json
snarkjs wtns calculate zkey/mux_js/mux.wasm input4.json witness_mux.wtns
snarkjs groth16 prove zkey/mux.zkey witness_mux.wtns proof_mux.json public_mux.json
snarkjs groth16 verify zkey/mux.vkey.json public_mux.json proof_mux.json

snarkjs wtns export json witness_mux.wtns witness_mux.json && cat witness_mux.json

[vivianjeng]

Hi @DragonDev1906 I tried another fix
https://github.com/zkmopro/mopro/pull/698/changes
still in the same branch (different commitment)

circom-prover = { git = "https://github.com/zkmopro/mopro", branch = "bls-script"}

please check if it works with your circuits

[DragonDev1906]

Similar to before: It works on the Multiplexer(1,2) circuit but not on my more complex one. I was hoping the minimized version would be more useful for debugging this. Anyways, here is the relevant section of the circuit that keeps failing validation as soon as it is included (for bls12-381):

    assert(in.dotSep < MAX_HEADER_SIZE);
    component dotCheck = Multiplexer(1,MAX_HEADER_SIZE);
    for (var i = 0; i < MAX_HEADER_SIZE; i++) {
        dotCheck.inp[i][0] <== in[i];
    }
    dotCheck.sel <== dotSep;

In case it helps: Here is a bit more context on where the signals actually come from, though proof verification fails if the BEBits2Array use is commented out and the input is used directly, so that's not the root cause.

template BEBits2Array(n, k) {
    // We could allow other sizes, but then it's not obvious what needs to be padded.
    assert(n%k == 0);

    signal input bits[n]; // binary
    signal output out[k];

    // Calculate the required size for Bits2Num (last one can be shorter).
    var size = (n+k-1)\k; // div_ceil

    // Create the components
    component b2n[k];
    for (var i = 0; i < k; i++) {
        b2n[i] = Bits2Num(size);
        for (var x = 0; x < size; x++) {
            b2n[i].in[size-1-x] <== bits[i*size+x];
        }
    }

    // Wire up the output
    for (var i = 0; i < k; i++) {
        out[i] <== b2n[i].out;
    }
}


template Example(payload_bytes) {
    signal input in[payload_bytes*8];
    signal input dotSep;
    var MAX_HEADER_SIZE = 256;

    signal payload_b[payload_bytes] <== BEBits2Array(payload_bytes*8, payload_bytes)(in);

    assert(in.dotSep < MAX_HEADER_SIZE);
    component dotCheck = Multiplexer(1,MAX_HEADER_SIZE);
    for (var i = 0; i < MAX_HEADER_SIZE; i++) {
        dotCheck.inp[i][0] <== payload_b[i];
    }
    dotCheck.sel <== dotSep;
}

component main = Example(1024);

In the full circuit the input signals are in a Bus, but that shouldn't matter from what I can tell.

---

Btw: Is it normal that loading the zkey takes significantly longer for BLS? This is with --release and with a small circuit (around 15k constraints, slightly larger circuit than what I posted above):

• BN: 0.032 seconds
• BLS: 6.047 seconds

While prover times are around 0.3 seconds for both (8 core CPU). I've seen zkey loading go over a minute for bls (though that was without --release). I don't know about very large circuits, but it seems to take longer than proving does (at least for this circuit size).

[DragonDev1906]

Any updates? The circuit below works with SIZE<=3, but for SIZE>=4 it fails on bls (but works on bn254).

pragma circom 2.2.3;

include "circomlib/circuits/multiplexer.circom";

template Example(payload_bytes) {
    signal input in[payload_bytes];
    var SIZE = 4;

    component dotCheck = Multiplexer(1,SIZE);
    for (var i = 0; i < SIZE; i++) {
        dotCheck.inp[i][0] <== in[i];
    }
    dotCheck.sel <== 1;
}

component main = Example(8);

Cargo.lock entry:

[[package]]
name = "circom-prover"
version = "0.1.4"
source = "git+https://github.com/zkmopro/mopro?branch=bls-script#31c3b168a7586f0857b1f733e2500375fc9204c0"