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