dusk-network/plonk

Circuit verification doesn't fail when wires selectors are different than the ones in the circuit description

Closed this issue · 1 comments

Describe the bug
When we test a circuit, we first create a circuit description for both the prover and the verifier. This circuit description essentially is the compressed blueprint of the circuit and when we verify certain circuits, they should only pass when they have that same circuit description.

But what seems to happen in the implementation is that only the witness, public input values and the constants are crosschecked with the circuit description, but not the wire selector values.

To Reproduce

use dusk_plonk::prelude::*;
use rand::rngs::StdRng;
use rand::SeedableRng;

// Because we derive the default trait, the circuit description will have zeros for all the wire selectors,
// and the values of all witnesses don't matter
#[derive(Default)]
pub struct TestCircuit {
    q_l: BlsScalar,
    q_r: BlsScalar,
    a: BlsScalar,
    b: BlsScalar,
}

impl TestCircuit {
    pub fn new(q_l: BlsScalar, q_r: BlsScalar, a: BlsScalar, b: BlsScalar) -> Self {
        Self { q_l, q_r, a, b }
    }
}

impl Circuit for TestCircuit {
    fn circuit<C>(&self, composer: &mut C) -> Result<(), Error>
    where
        C: Composer,
    {
        let w_a = composer.append_witness(self.a);
        let w_b = composer.append_witness(self.b);

        let constraint = Constraint::new()
            .left(self.q_l)
            .right(self.q_r)
            .a(w_a)
            .b(w_b);

        composer.append_gate(constraint);

        Ok(())
    }
}

fn main() {
    // Compile common circuit descriptions for the prover and verifier using
    // the `default` circuit representation
    let label = b"append_gate_with_constant";
    let rng = &mut StdRng::seed_from_u64(0x1ab);
    let capacity = 1 << 4;
    let pp = PublicParameters::setup(capacity, rng)
        .expect("Creation of public parameter shouldn't fail");
    let (prover, _verifier) = Compiler::compile(&pp, label)
        .expect("It should be possible to create the prover and verifier circuit descriptions");

    // Test unsatisfied circuit, the following expression doesn't equal 0:
    // q_l·a + q_r·b != 0
    let msg = "Proof creation of unsatisfied circuit should fail";
    let q_l = BlsScalar::one();
    let q_r = BlsScalar::one();
    let a = BlsScalar::random(rng);
    let b = BlsScalar::random(rng);
    let circuit = TestCircuit::new(q_l, q_r, a, b);
    let result = prover.prove(rng, &circuit);
    match result {
        Ok(_) => panic!("{}", msg),
        _ => println!("Test fails as expected"),
    }
}

Expected behaviour
It shouldn't be possible to create a proof for a circuit that is different than the circuit used for the circuit description. (Just like it is not possible to create a proof for a circuit that differs from the circuit used for the circuit description only in the constants or only in the length of the public input vector).

Logs/Screenshot
N/A

Platform
N/A

Additional context
Discovered when adding tests for append_gate in #741

On further inspection, this behavior is, though highly confusing, actually correct.

We use the default trait to create the circuit descriptions for both the prover and the verifier. Continuing with the protocol, both the prover and the verifier only care about the witness and public input, if they match the circuit that was used for the circuit description, the proof will pass.

In the above example the #[derive(Default)] caused the selector polynomials zero in the circuit description. Hence any witness satisfies the circuit.

Even though it is correct behavior, it is still highly confusing as well and we should think about re-structuring the Circuit trait in a way that makes this use impossible.

The issue #715 already thinks along those lines but it needs more thinking still.