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