microsoft / Spartan

Spartan: High-speed zkSNARKs without trusted setup
MIT License
672 stars 112 forks source link

panics when testing assignment that doesn't meet constraints #44

Closed ikhaliq15 closed 2 years ago

ikhaliq15 commented 2 years ago

I am playing around with the provided examples/cubic.rs example. I changed it so that we print "success" if verification passes and "failed" if verification does not pass. However, when I test an example of a witness that does not satisfy the constraints, the program panics while trying to verify, rather than printing "failed". Is this expected? And is there a way for me to have proof.verify() return a ProofVerifyError when the verification does not pass rather than panicking?

Here is the code I was testing:

use curve25519_dalek::scalar::Scalar;
use libspartan::{InputsAssignment, Instance, SNARKGens, VarsAssignment, SNARK};
use merlin::Transcript;
use rand::rngs::OsRng;

#[allow(non_snake_case)]
fn produce_r1cs() -> (
    usize,
    usize,
    usize,
    usize,
    Instance,
    VarsAssignment,
    InputsAssignment,
) {
    // parameters of the R1CS instance
    let num_cons = 4;
    let num_vars = 4;
    let num_inputs = 1;
    let num_non_zero_entries = 8;

    // We will encode the above constraints into three matrices, where
    // the coefficients in the matrix are in the little-endian byte order
    let mut A: Vec<(usize, usize, [u8; 32])> = Vec::new();
    let mut B: Vec<(usize, usize, [u8; 32])> = Vec::new();
    let mut C: Vec<(usize, usize, [u8; 32])> = Vec::new();

    let one = Scalar::one().to_bytes();

    // R1CS is a set of three sparse matrices A B C, where is a row for every
    // constraint and a column for every entry in z = (vars, 1, inputs)
    // An R1CS instance is satisfiable iff:
    // Az \circ Bz = Cz, where z = (vars, 1, inputs)

    // constraint 0 entries in (A,B,C)
    // constraint 0 is Z0 * Z0 - Z1 = 0.
    A.push((0, 0, one));
    B.push((0, 0, one));
    C.push((0, 1, one));

    // constraint 1 entries in (A,B,C)
    // constraint 1 is Z1 * Z0 - Z2 = 0.
    A.push((1, 1, one));
    B.push((1, 0, one));
    C.push((1, 2, one));

    // constraint 2 entries in (A,B,C)
    // constraint 2 is (Z2 + Z0) * 1 - Z3 = 0.
    A.push((2, 2, one));
    A.push((2, 0, one));
    B.push((2, num_vars, one));
    C.push((2, 3, one));

    // constraint 3 entries in (A,B,C)
    // constraint 3 is (Z3 + 5) * 1 - I0 = 0.
    A.push((3, 3, one));
    A.push((3, num_vars, Scalar::from(5u32).to_bytes()));
    B.push((3, num_vars, one));
    C.push((3, num_vars + 1, one));

    let inst = Instance::new(num_cons, num_vars, num_inputs, &A, &B, &C).unwrap();

    // this is an assignment that does not satisfy the constraints
    let mut csprng: OsRng = OsRng;
    let z0 = Scalar::zero();
    let z1 = z0; // constraint 0
    let z2 = z0; // constraint 1
    let z3 = z0; // constraint 2
    let i0 = z0; // constraint 3

    // create a VarsAssignment
    let mut vars = vec![Scalar::zero().to_bytes(); num_vars];
    vars[0] = z0.to_bytes();
    vars[1] = z1.to_bytes();
    vars[2] = z2.to_bytes();
    vars[3] = z3.to_bytes();
    let assignment_vars = VarsAssignment::new(&vars).unwrap();

    // create an InputsAssignment
    let mut inputs = vec![Scalar::zero().to_bytes(); num_inputs];
    inputs[0] = i0.to_bytes();
    let assignment_inputs = InputsAssignment::new(&inputs).unwrap();

    (
        num_cons,
        num_vars,
        num_inputs,
        num_non_zero_entries,
        inst,
        assignment_vars,
        assignment_inputs,
    )
}

fn main() {
    // produce an R1CS instance
    let (
        num_cons,
        num_vars,
        num_inputs,
        num_non_zero_entries,
        inst,
        assignment_vars,
        assignment_inputs,
    ) = produce_r1cs();

    // produce public parameters
    let gens = SNARKGens::new(num_cons, num_vars, num_inputs, num_non_zero_entries);

    // create a commitment to the R1CS instance
    let (comm, decomm) = SNARK::encode(&inst, &gens);

    // produce a proof of satisfiability
    let mut prover_transcript = Transcript::new(b"snark_example");
    let proof = SNARK::prove(
        &inst,
        &decomm,
        assignment_vars,
        &assignment_inputs,
        &gens,
        &mut prover_transcript,
    );

    // verify the proof of satisfiability
    let mut verifier_transcript = Transcript::new(b"snark_example");
    if proof
        .verify(&comm, &assignment_inputs, &mut verifier_transcript, &gens)
        .is_ok() {
        println!("proof verification successful!");
    } else {
        println!("proof verification failed!");
    }
}

Error:

thread 'main' panicked at 'assertion failed: self.proof_eq_sc_phase1.verify(&gens.gens_sc.gens_1, transcript,\n        &expected_claim_post_phase1, &comm_claim_post_phase1).is_ok()',