1//! Demonstrates how to produces a proof for canonical cubic equation: `x^3 + x + 5 = y`.
  2//! The example is described in detail [here].
  3//!
  4//! The R1CS for this problem consists of the following 4 constraints:
  5//! `Z0 * Z0 - Z1 = 0`
  6//! `Z1 * Z0 - Z2 = 0`
  7//! `(Z2 + Z0) * 1 - Z3 = 0`
  8//! `(Z3 + 5) * 1 - I0 = 0`
  9//!
 10//! [here]: https://medium.com/@VitalikButerin/quadratic-arithmetic-programs-from-zero-to-hero-f6d558cea649
 11use curve25519_dalek::scalar::Scalar;
 12use libspartan::{InputsAssignment, Instance, SNARKGens, VarsAssignment, SNARK};
 13use merlin::Transcript;
 14use rand::rngs::OsRng;
 15
 16#[allow(non_snake_case)]
 17fn produce_r1cs() -> (
 18  usize,
 19  usize,
 20  usize,
 21  usize,
 22  Instance,
 23  VarsAssignment,
 24  InputsAssignment,
 25) {
 26  // parameters of the R1CS instance
 27  let num_cons = 4;
 28  let num_vars = 4;
 29  let num_inputs = 1;
 30  let num_non_zero_entries = 8;
 31
 32  // We will encode the above constraints into three matrices, where
 33  // the coefficients in the matrix are in the little-endian byte order
 34  let mut A: Vec<(usize, usize, [u8; 32])> = Vec::new();
 35  let mut B: Vec<(usize, usize, [u8; 32])> = Vec::new();
 36  let mut C: Vec<(usize, usize, [u8; 32])> = Vec::new();
 37
 38  let one = Scalar::one().to_bytes();
 39
 40  // R1CS is a set of three sparse matrices A B C, where is a row for every
 41  // constraint and a column for every entry in z = (vars, 1, inputs)
 42  // An R1CS instance is satisfiable iff:
 43  // Az \circ Bz = Cz, where z = (vars, 1, inputs)
 44
 45  // constraint 0 entries in (A,B,C)
 46  // constraint 0 is Z0 * Z0 - Z1 = 0.
 47  A.push((0, 0, one));
 48  B.push((0, 0, one));
 49  C.push((0, 1, one));
 50
 51  // constraint 1 entries in (A,B,C)
 52  // constraint 1 is Z1 * Z0 - Z2 = 0.
 53  A.push((1, 1, one));
 54  B.push((1, 0, one));
 55  C.push((1, 2, one));
 56
 57  // constraint 2 entries in (A,B,C)
 58  // constraint 2 is (Z2 + Z0) * 1 - Z3 = 0.
 59  A.push((2, 2, one));
 60  A.push((2, 0, one));
 61  B.push((2, num_vars, one));
 62  C.push((2, 3, one));
 63
 64  // constraint 3 entries in (A,B,C)
 65  // constraint 3 is (Z3 + 5) * 1 - I0 = 0.
 66  A.push((3, 3, one));
 67  A.push((3, num_vars, Scalar::from(5u32).to_bytes()));
 68  B.push((3, num_vars, one));
 69  C.push((3, num_vars + 1, one));
 70
 71  let inst = Instance::new(num_cons, num_vars, num_inputs, &A, &B, &C).unwrap();
 72
 73  // compute a satisfying assignment
 74  let mut csprng: OsRng = OsRng;
 75  let z0 = Scalar::random(&mut csprng);
 76  let z1 = z0 * z0; // constraint 0
 77  let z2 = z1 * z0; // constraint 1
 78  let z3 = z2 + z0; // constraint 2
 79  let i0 = z3 + Scalar::from(5u32); // constraint 3
 80
 81  // create a VarsAssignment
 82  let mut vars = vec![Scalar::zero().to_bytes(); num_vars];
 83  vars[0] = z0.to_bytes();
 84  vars[1] = z1.to_bytes();
 85  vars[2] = z2.to_bytes();
 86  vars[3] = z3.to_bytes();
 87  let assignment_vars = VarsAssignment::new(&vars).unwrap();
 88
 89  // create an InputsAssignment
 90  let mut inputs = vec![Scalar::zero().to_bytes(); num_inputs];
 91  inputs[0] = i0.to_bytes();
 92  let assignment_inputs = InputsAssignment::new(&inputs).unwrap();
 93
 94  // check if the instance we created is satisfiable
 95  let res = inst.is_sat(&assignment_vars, &assignment_inputs);
 96  assert!(res.unwrap(), "should be satisfied");
 97
 98  (
 99    num_cons,
100    num_vars,
101    num_inputs,
102    num_non_zero_entries,
103    inst,
104    assignment_vars,
105    assignment_inputs,
106  )
107}
108
109fn main() {
110  // produce an R1CS instance
111  let (
112    num_cons,
113    num_vars,
114    num_inputs,
115    num_non_zero_entries,
116    inst,
117    assignment_vars,
118    assignment_inputs,
119  ) = produce_r1cs();
120
121  // produce public parameters
122  let gens = SNARKGens::new(num_cons, num_vars, num_inputs, num_non_zero_entries);
123
124  // create a commitment to the R1CS instance
125  let (comm, decomm) = SNARK::encode(&inst, &gens);
126
127  // produce a proof of satisfiability
128  let mut prover_transcript = Transcript::new(b"snark_example");
129  let proof = SNARK::prove(
130    &inst,
131    &decomm,
132    assignment_vars,
133    &assignment_inputs,
134    &gens,
135    &mut prover_transcript,
136  );
137
138  // verify the proof of satisfiability
139  let mut verifier_transcript = Transcript::new(b"snark_example");
140  assert!(proof
141    .verify(&comm, &assignment_inputs, &mut verifier_transcript, &gens)
142    .is_ok());
143  println!("proof verification successful!");
144}