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 ark_bls12_377::Fr as Scalar;
 12use ark_ff::{BigInteger, PrimeField};
 13use ark_std::{One, UniformRand, Zero};
 14<<<<<<< HEAD
 15use libspartan::{InputsAssignment, Instance, SNARKGens, VarsAssignment, SNARK};
 16=======
 17use libspartan::{
 18  parameters::poseidon_params,
 19  poseidon_transcript::{self, PoseidonTranscript},
 20  InputsAssignment, Instance, SNARKGens, VarsAssignment, SNARK,
 21};
 22>>>>>>> implement alternative transcript with poseidon backend
 23use merlin::Transcript;
 24
 25#[allow(non_snake_case)]
 26fn produce_r1cs() -> (
 27  usize,
 28  usize,
 29  usize,
 30  usize,
 31  Instance,
 32  VarsAssignment,
 33  InputsAssignment,
 34) {
 35  // parameters of the R1CS instance
 36  let num_cons = 4;
 37  let num_vars = 4;
 38  let num_inputs = 1;
 39  let num_non_zero_entries = 8;
 40
 41  // We will encode the above constraints into three matrices, where
 42  // the coefficients in the matrix are in the little-endian byte order
 43  let mut A: Vec<(usize, usize, Vec<u8>)> = Vec::new();
 44  let mut B: Vec<(usize, usize, Vec<u8>)> = Vec::new();
 45  let mut C: Vec<(usize, usize, Vec<u8>)> = Vec::new();
 46
 47  let one = Scalar::one().into_repr().to_bytes_le();
 48
 49  // R1CS is a set of three sparse matrices A B C, where is a row for every
 50  // constraint and a column for every entry in z = (vars, 1, inputs)
 51  // An R1CS instance is satisfiable iff:
 52  // Az \circ Bz = Cz, where z = (vars, 1, inputs)
 53
 54  // constraint 0 entries in (A,B,C)
 55  // constraint 0 is Z0 * Z0 - Z1 = 0.
 56  A.push((0, 0, one.clone()));
 57  B.push((0, 0, one.clone()));
 58  C.push((0, 1, one.clone()));
 59
 60  // constraint 1 entries in (A,B,C)
 61  // constraint 1 is Z1 * Z0 - Z2 = 0.
 62  A.push((1, 1, one.clone()));
 63  B.push((1, 0, one.clone()));
 64  C.push((1, 2, one.clone()));
 65
 66  // constraint 2 entries in (A,B,C)
 67  // constraint 2 is (Z2 + Z0) * 1 - Z3 = 0.
 68  A.push((2, 2, one.clone()));
 69  A.push((2, 0, one.clone()));
 70  B.push((2, num_vars, one.clone()));
 71  C.push((2, 3, one.clone()));
 72
 73  // constraint 3 entries in (A,B,C)
 74  // constraint 3 is (Z3 + 5) * 1 - I0 = 0.
 75  A.push((3, 3, one.clone()));
 76  A.push((3, num_vars, Scalar::from(5u32).into_repr().to_bytes_le()));
 77  B.push((3, num_vars, one.clone()));
 78  C.push((3, num_vars + 1, one.clone()));
 79
 80  let inst = Instance::new(num_cons, num_vars, num_inputs, &A, &B, &C).unwrap();
 81
 82  // compute a satisfying assignment
 83  let mut rng = ark_std::rand::thread_rng();
 84  let z0 = Scalar::rand(&mut rng);
 85  let z1 = z0 * z0; // constraint 0
 86  let z2 = z1 * z0; // constraint 1
 87  let z3 = z2 + z0; // constraint 2
 88  let i0 = z3 + Scalar::from(5u32); // constraint 3
 89
 90  // create a VarsAssignment
 91  let mut vars = vec![Scalar::zero().into_repr().to_bytes_le(); num_vars];
 92  vars[0] = z0.into_repr().to_bytes_le();
 93  vars[1] = z1.into_repr().to_bytes_le();
 94  vars[2] = z2.into_repr().to_bytes_le();
 95  vars[3] = z3.into_repr().to_bytes_le();
 96  let assignment_vars = VarsAssignment::new(&vars).unwrap();
 97
 98  // create an InputsAssignment
 99  let mut inputs = vec![Scalar::zero().into_repr().to_bytes_le(); num_inputs];
100  inputs[0] = i0.into_repr().to_bytes_le();
101  let assignment_inputs = InputsAssignment::new(&inputs).unwrap();
102
103  // check if the instance we created is satisfiable
104  let res = inst.is_sat(&assignment_vars, &assignment_inputs);
105  assert!(res.unwrap(), "should be satisfied");
106
107  (
108    num_cons,
109    num_vars,
110    num_inputs,
111    num_non_zero_entries,
112    inst,
113    assignment_vars,
114    assignment_inputs,
115  )
116}
117
118fn main() {
119  // produce an R1CS instance
120  let (
121    num_cons,
122    num_vars,
123    num_inputs,
124    num_non_zero_entries,
125    inst,
126    assignment_vars,
127    assignment_inputs,
128  ) = produce_r1cs();
129
130  let params = poseidon_params();
131
132  // produce public parameters
133  let gens = SNARKGens::new(num_cons, num_vars, num_inputs, num_non_zero_entries);
134
135  // create a commitment to the R1CS instance
136  let (comm, decomm) = SNARK::encode(&inst, &gens);
137
138  // produce a proof of satisfiability
139  let mut prover_transcript = PoseidonTranscript::new(&params);
140  let proof = SNARK::prove(
141    &inst,
142    &comm,
143    &decomm,
144    assignment_vars,
145    &assignment_inputs,
146    &gens,
147    &mut prover_transcript,
148  );
149
150  // verify the proof of satisfiability
151  let mut verifier_transcript = PoseidonTranscript::new(&params);
152  assert!(proof
153    .verify(&comm, &assignment_inputs, &mut verifier_transcript, &gens)
154    .is_ok());
155  println!("proof verification successful!");
156}