From 7b102a241f9d2777bb14c8b140d795511ded60e1 Mon Sep 17 00:00:00 2001 From: Jakub Konka Date: Wed, 16 Sep 2020 18:41:13 +0200 Subject: [PATCH] Add example proving knowledge of cubic equation solution (#26) --- .github/workflows/rust.yml | 4 +- README.md | 2 + examples/cubic.rs | 144 +++++++++++++++++++++++++++++++++++++ 3 files changed, 149 insertions(+), 1 deletion(-) create mode 100644 examples/cubic.rs diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 56792f3..b217a21 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -14,8 +14,10 @@ jobs: steps: - uses: actions/checkout@v2 - name: Install - run: rustup default nightly + run: rustup default nightly-2020-09-15 - name: Build run: cargo build --verbose - name: Run tests run: cargo test --verbose + - name: Build examples + run: cargo build --examples --verbose diff --git a/README.md b/README.md index db5a26f..d3edaf5 100644 --- a/README.md +++ b/README.md @@ -248,6 +248,8 @@ Finally, we provide an example that specifies a custom R1CS instance instead of # } ``` +For more examples, see [`examples/`](examples) directory in this repo. + ## Building `libspartan` Install [`rustup`](https://rustup.rs/) diff --git a/examples/cubic.rs b/examples/cubic.rs new file mode 100644 index 0000000..91c68fc --- /dev/null +++ b/examples/cubic.rs @@ -0,0 +1,144 @@ +//! Demonstrates how to produces a proof for canonical cubic equation: `x^3 + x + 5 = y`. +//! The example is described in detail [here]. +//! +//! The R1CS for this problem consists of the following 4 constraints: +//! `Z0 * Z0 - Z1 = 0` +//! `Z1 * Z0 - Z2 = 0` +//! `(Z2 + Z0) * 1 - Z3 = 0` +//! `(Z3 + 5) * 1 - I0 = 0` +//! +//! [here]: https://medium.com/@VitalikButerin/quadratic-arithmetic-programs-from-zero-to-hero-f6d558cea649 +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(); + + // compute a satisfying assignment + let mut csprng: OsRng = OsRng; + let z0 = Scalar::random(&mut csprng); + let z1 = z0 * z0; // constraint 0 + let z2 = z1 * z0; // constraint 1 + let z3 = z2 + z0; // constraint 2 + let i0 = z3 + Scalar::from(5u32); // 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(); + + // check if the instance we created is satisfiable + let res = inst.is_sat(&assignment_vars, &assignment_inputs); + assert_eq!(res.unwrap(), true, "should be satisfied"); + + ( + 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"); + assert!(proof + .verify(&comm, &assignment_inputs, &mut verifier_transcript, &gens) + .is_ok()); + println!("proof verification successful!"); +}