testudo/src/r1csproof.rs
src/r1csproof.rsRaw
1#![allow(clippy::too_many_arguments)]
2use crate::constraints::{VerifierCircuit, VerifierConfig};
3use crate::group::{Fq, Fr};
4use crate::math::Math;
5use crate::parameters::poseidon_params;
6use crate::poseidon_transcript::{AppendToPoseidon, PoseidonTranscript};
7use crate::sumcheck::SumcheckInstanceProof;
8use ark_bls12_377::Bls12_377 as I;
9use ark_bw6_761::BW6_761 as P;
10use ark_poly::MultilinearExtension;
11use ark_poly_commit::multilinear_pc::data_structures::{Commitment, Proof};
12use ark_poly_commit::multilinear_pc::MultilinearPC;
13
14use super::commitments::MultiCommitGens;
15use super::dense_mlpoly::{DensePolynomial, EqPolynomial, PolyCommitmentGens};
16use super::errors::ProofVerifyError;
17
18use super::r1csinstance::R1CSInstance;
19
20use super::scalar::Scalar;
21use super::sparse_mlpoly::{SparsePolyEntry, SparsePolynomial};
22use super::timer::Timer;
23use ark_crypto_primitives::{CircuitSpecificSetupSNARK, SNARK};
24
25use ark_groth16::Groth16;
26use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystem};
27use ark_serialize::*;
28use ark_std::{One, Zero};
29
30use std::time::Instant;
31
32#[derive(CanonicalSerialize, CanonicalDeserialize, Debug)]
33pub struct R1CSProof {
34 // The PST commitment to the multilinear extension of the witness.
35 comm: Commitment<I>,
36 sc_proof_phase1: SumcheckInstanceProof,
37 claims_phase2: (Scalar, Scalar, Scalar, Scalar),
38 sc_proof_phase2: SumcheckInstanceProof,
39 eval_vars_at_ry: Scalar,
40 proof_eval_vars_at_ry: Proof<I>,
41 rx: Vec<Scalar>,
42 ry: Vec<Scalar>,
43 // The transcript state after the satisfiability proof was computed.
44 pub transcript_sat_state: Scalar,
45}
46#[derive(Clone)]
47pub struct R1CSSumcheckGens {
48 gens_1: MultiCommitGens,
49 gens_3: MultiCommitGens,
50 gens_4: MultiCommitGens,
51}
52
53// TODO: fix passing gens_1_ref
54impl R1CSSumcheckGens {
55 pub fn new(label: &'static [u8], gens_1_ref: &MultiCommitGens) -> Self {
56 let gens_1 = gens_1_ref.clone();
57 let gens_3 = MultiCommitGens::new(3, label);
58 let gens_4 = MultiCommitGens::new(4, label);
59
60 R1CSSumcheckGens {
61 gens_1,
62 gens_3,
63 gens_4,
64 }
65 }
66}
67
68#[derive(Clone)]
69pub struct R1CSGens {
70 gens_sc: R1CSSumcheckGens,
71 gens_pc: PolyCommitmentGens,
72}
73
74impl R1CSGens {
75 pub fn new(label: &'static [u8], _num_cons: usize, num_vars: usize) -> Self {
76 let num_poly_vars = num_vars.log_2();
77 let gens_pc = PolyCommitmentGens::new(num_poly_vars, label);
78 let gens_sc = R1CSSumcheckGens::new(label, &gens_pc.gens.gens_1);
79 R1CSGens { gens_sc, gens_pc }
80 }
81}
82
83impl R1CSProof {
84 fn prove_phase_one(
85 num_rounds: usize,
86 evals_tau: &mut DensePolynomial,
87 evals_Az: &mut DensePolynomial,
88 evals_Bz: &mut DensePolynomial,
89 evals_Cz: &mut DensePolynomial,
90 transcript: &mut PoseidonTranscript,
91 ) -> (SumcheckInstanceProof, Vec<Scalar>, Vec<Scalar>) {
92 let comb_func = |poly_tau_comp: &Scalar,
93 poly_A_comp: &Scalar,
94 poly_B_comp: &Scalar,
95 poly_C_comp: &Scalar|
96 -> Scalar {
97 (*poly_tau_comp) * ((*poly_A_comp) * poly_B_comp - poly_C_comp)
98 };
99
100 let (sc_proof_phase_one, r, claims) = SumcheckInstanceProof::prove_cubic_with_additive_term(
101 &Scalar::zero(), // claim is zero
102 num_rounds,
103 evals_tau,
104 evals_Az,
105 evals_Bz,
106 evals_Cz,
107 comb_func,
108 transcript,
109 );
110
111 (sc_proof_phase_one, r, claims)
112 }
113
114 fn prove_phase_two(
115 num_rounds: usize,
116 claim: &Scalar,
117 evals_z: &mut DensePolynomial,
118 evals_ABC: &mut DensePolynomial,
119 transcript: &mut PoseidonTranscript,
120 ) -> (SumcheckInstanceProof, Vec<Scalar>, Vec<Scalar>) {
121 let comb_func =
122 |poly_A_comp: &Scalar, poly_B_comp: &Scalar| -> Scalar { (*poly_A_comp) * poly_B_comp };
123 let (sc_proof_phase_two, r, claims) = SumcheckInstanceProof::prove_quad(
124 claim, num_rounds, evals_z, evals_ABC, comb_func, transcript,
125 );
126
127 (sc_proof_phase_two, r, claims)
128 }
129
130 fn protocol_name() -> &'static [u8] {
131 b"R1CS proof"
132 }
133
134 pub fn prove(
135 inst: &R1CSInstance,
136 vars: Vec<Scalar>,
137 input: &[Scalar],
138 gens: &R1CSGens,
139 transcript: &mut PoseidonTranscript,
140 ) -> (R1CSProof, Vec<Scalar>, Vec<Scalar>) {
141 let timer_prove = Timer::new("R1CSProof::prove");
142 // we currently require the number of |inputs| + 1 to be at most number of vars
143 assert!(input.len() < vars.len());
144
145 // create the multilinear witness polynomial from the satisfying assiment
146 let poly_vars = DensePolynomial::new(vars.clone());
147
148 let timer_commit = Timer::new("polycommit");
149 // commitment to the satisfying witness polynomial
150 let comm = MultilinearPC::<I>::commit(&gens.gens_pc.ck, &poly_vars);
151 comm.append_to_poseidon(transcript);
152 timer_commit.stop();
153
154 let c = transcript.challenge_scalar();
155 transcript.new_from_state(&c);
156
157 transcript.append_scalar_vector(input);
158
159 let timer_sc_proof_phase1 = Timer::new("prove_sc_phase_one");
160
161 // append input to variables to create a single vector z
162 let z = {
163 let num_inputs = input.len();
164 let num_vars = vars.len();
165 let mut z = vars;
166 z.extend(&vec![Scalar::one()]); // add constant term in z
167 z.extend(input);
168 z.extend(&vec![Scalar::zero(); num_vars - num_inputs - 1]); // we will pad with zeros
169 z
170 };
171
172 // derive the verifier's challenge tau
173 let (num_rounds_x, num_rounds_y) = (inst.get_num_cons().log_2(), z.len().log_2());
174 let tau = transcript.challenge_vector(num_rounds_x);
175 // compute the initial evaluation table for R(\tau, x)
176 let mut poly_tau = DensePolynomial::new(EqPolynomial::new(tau).evals());
177 let (mut poly_Az, mut poly_Bz, mut poly_Cz) =
178 inst.multiply_vec(inst.get_num_cons(), z.len(), &z);
179
180 let (sc_proof_phase1, rx, _claims_phase1) = R1CSProof::prove_phase_one(
181 num_rounds_x,
182 &mut poly_tau,
183 &mut poly_Az,
184 &mut poly_Bz,
185 &mut poly_Cz,
186 transcript,
187 );
188 assert_eq!(poly_tau.len(), 1);
189 assert_eq!(poly_Az.len(), 1);
190 assert_eq!(poly_Bz.len(), 1);
191 assert_eq!(poly_Cz.len(), 1);
192 timer_sc_proof_phase1.stop();
193
194 let (tau_claim, Az_claim, Bz_claim, Cz_claim) =
195 (&poly_tau[0], &poly_Az[0], &poly_Bz[0], &poly_Cz[0]);
196 let prod_Az_Bz_claims = (*Az_claim) * Bz_claim;
197
198 // prove the final step of sum-check #1
199 let taus_bound_rx = tau_claim;
200 let _claim_post_phase1 = ((*Az_claim) * Bz_claim - Cz_claim) * taus_bound_rx;
201
202 let timer_sc_proof_phase2 = Timer::new("prove_sc_phase_two");
203 // combine the three claims into a single claim
204 let r_A = transcript.challenge_scalar();
205 let r_B = transcript.challenge_scalar();
206 let r_C = transcript.challenge_scalar();
207 let claim_phase2 = r_A * Az_claim + r_B * Bz_claim + r_C * Cz_claim;
208
209 let evals_ABC = {
210 // compute the initial evaluation table for R(\tau, x)
211 let evals_rx = EqPolynomial::new(rx.clone()).evals();
212 let (evals_A, evals_B, evals_C) =
213 inst.compute_eval_table_sparse(inst.get_num_cons(), z.len(), &evals_rx);
214
215 assert_eq!(evals_A.len(), evals_B.len());
216 assert_eq!(evals_A.len(), evals_C.len());
217 (0..evals_A.len())
218 .map(|i| r_A * evals_A[i] + r_B * evals_B[i] + r_C * evals_C[i])
219 .collect::<Vec<Scalar>>()
220 };
221
222 // another instance of the sum-check protocol
223 let (sc_proof_phase2, ry, _claims_phase2) = R1CSProof::prove_phase_two(
224 num_rounds_y,
225 &claim_phase2,
226 &mut DensePolynomial::new(z),
227 &mut DensePolynomial::new(evals_ABC),
228 transcript,
229 );
230 timer_sc_proof_phase2.stop();
231
232 // TODO: modify the polynomial evaluation in Spartan to be consistent
233 // with the evaluation in ark-poly-commit so that reversing is not needed
234 // anymore
235 let timmer_opening = Timer::new("polyopening");
236 let mut dummy = ry[1..].to_vec().clone();
237 dummy.reverse();
238 let proof_eval_vars_at_ry = MultilinearPC::<I>::open(&gens.gens_pc.ck, &poly_vars, &dummy);
239 println!(
240 "proof size (no of quotients): {:?}",
241 proof_eval_vars_at_ry.proofs.len()
242 );
243 timmer_opening.stop();
244
245 let timer_polyeval = Timer::new("polyeval");
246 let eval_vars_at_ry = poly_vars.evaluate(&ry[1..]);
247 timer_polyeval.stop();
248
249 timer_prove.stop();
250
251 let c = transcript.challenge_scalar();
252
253 (
254 R1CSProof {
255 comm,
256 sc_proof_phase1,
257 claims_phase2: (*Az_claim, *Bz_claim, *Cz_claim, prod_Az_Bz_claims),
258 sc_proof_phase2,
259 eval_vars_at_ry,
260 proof_eval_vars_at_ry,
261 rx: rx.clone(),
262 ry: ry.clone(),
263 transcript_sat_state: c,
264 },
265 rx,
266 ry,
267 )
268 }
269
270 pub fn verify_groth16(
271 &self,
272 num_vars: usize,
273 num_cons: usize,
274 input: &[Scalar],
275 evals: &(Scalar, Scalar, Scalar),
276 transcript: &mut PoseidonTranscript,
277 gens: &R1CSGens,
278 ) -> Result<(u128, u128, u128), ProofVerifyError> {
279 self.comm.append_to_poseidon(transcript);
280
281 let c = transcript.challenge_scalar();
282
283 let mut input_as_sparse_poly_entries = vec![SparsePolyEntry::new(0, Scalar::one())];
284 //remaining inputs
285 input_as_sparse_poly_entries.extend(
286 (0..input.len())
287 .map(|i| SparsePolyEntry::new(i + 1, input[i]))
288 .collect::<Vec<SparsePolyEntry>>(),
289 );
290
291 let n = num_vars;
292 let input_as_sparse_poly =
293 SparsePolynomial::new(n.log_2() as usize, input_as_sparse_poly_entries);
294
295 let config = VerifierConfig {
296 num_vars,
297 num_cons,
298 input: input.to_vec(),
299 evals: *evals,
300 params: poseidon_params(),
301 prev_challenge: c,
302 claims_phase2: self.claims_phase2,
303 polys_sc1: self.sc_proof_phase1.polys.clone(),
304 polys_sc2: self.sc_proof_phase2.polys.clone(),
305 eval_vars_at_ry: self.eval_vars_at_ry,
306 input_as_sparse_poly,
307 // rx: self.rx.clone(),
308 ry: self.ry.clone(),
309 transcript_sat_state: self.transcript_sat_state,
310 };
311
312 let mut rng = ark_std::test_rng();
313
314 let prove_inner = Timer::new("proveinnercircuit");
315 let start = Instant::now();
316 let circuit = VerifierCircuit::new(&config, &mut rng).unwrap();
317 let dp1 = start.elapsed().as_millis();
318 prove_inner.stop();
319
320 let start = Instant::now();
321 let (pk, vk) = Groth16::<P>::setup(circuit.clone(), &mut rng).unwrap();
322 let ds = start.elapsed().as_millis();
323
324 let prove_outer = Timer::new("proveoutercircuit");
325 let start = Instant::now();
326 let proof = Groth16::<P>::prove(&pk, circuit, &mut rng).unwrap();
327 let dp2 = start.elapsed().as_millis();
328 prove_outer.stop();
329
330 let start = Instant::now();
331 let is_verified = Groth16::<P>::verify(&vk, &[], &proof).unwrap();
332 assert!(is_verified);
333
334 let timer_verification = Timer::new("commitverification");
335 let mut dummy = self.ry[1..].to_vec();
336 // TODO: ensure ark-poly-commit and Spartan produce consistent results
337 // when evaluating a polynomial at a given point so this reverse is not
338 // needed.
339 dummy.reverse();
340
341 // Verifies the proof of opening against the result of evaluating the
342 // witness polynomial at point ry.
343 let res = MultilinearPC::<I>::check(
344 &gens.gens_pc.vk,
345 &self.comm,
346 &dummy,
347 self.eval_vars_at_ry,
348 &self.proof_eval_vars_at_ry,
349 );
350
351 timer_verification.stop();
352 assert!(res == true);
353 let dv = start.elapsed().as_millis();
354
355 Ok((ds, dp1 + dp2, dv))
356 }
357
358 // Helper function to find the number of constraint in the circuit which
359 // requires executing it.
360 pub fn circuit_size(
361 &self,
362 num_vars: usize,
363 num_cons: usize,
364 input: &[Scalar],
365 evals: &(Scalar, Scalar, Scalar),
366 transcript: &mut PoseidonTranscript,
367 _gens: &R1CSGens,
368 ) -> Result<usize, ProofVerifyError> {
369 self.comm.append_to_poseidon(transcript);
370
371 let c = transcript.challenge_scalar();
372
373 let mut input_as_sparse_poly_entries = vec![SparsePolyEntry::new(0, Scalar::one())];
374 //remaining inputs
375 input_as_sparse_poly_entries.extend(
376 (0..input.len())
377 .map(|i| SparsePolyEntry::new(i + 1, input[i]))
378 .collect::<Vec<SparsePolyEntry>>(),
379 );
380
381 let n = num_vars;
382 let input_as_sparse_poly =
383 SparsePolynomial::new(n.log_2() as usize, input_as_sparse_poly_entries);
384
385 let config = VerifierConfig {
386 num_vars,
387 num_cons,
388 input: input.to_vec(),
389 evals: *evals,
390 params: poseidon_params(),
391 prev_challenge: c,
392 claims_phase2: self.claims_phase2,
393 polys_sc1: self.sc_proof_phase1.polys.clone(),
394 polys_sc2: self.sc_proof_phase2.polys.clone(),
395 eval_vars_at_ry: self.eval_vars_at_ry,
396 input_as_sparse_poly,
397 // rx: self.rx.clone(),
398 ry: self.ry.clone(),
399 transcript_sat_state: self.transcript_sat_state,
400 };
401
402 let mut rng = ark_std::test_rng();
403 let circuit = VerifierCircuit::new(&config, &mut rng).unwrap();
404
405 let nc_inner = verify_constraints_inner(circuit.clone(), &num_cons);
406
407 let nc_outer = verify_constraints_outer(circuit, &num_cons);
408 Ok(nc_inner + nc_outer)
409 }
410}
411
412fn verify_constraints_outer(circuit: VerifierCircuit, _num_cons: &usize) -> usize {
413 let cs = ConstraintSystem::<Fq>::new_ref();
414 circuit.generate_constraints(cs.clone()).unwrap();
415 assert!(cs.is_satisfied().unwrap());
416 cs.num_constraints()
417}
418
419fn verify_constraints_inner(circuit: VerifierCircuit, _num_cons: &usize) -> usize {
420 let cs = ConstraintSystem::<Fr>::new_ref();
421 circuit
422 .inner_circuit
423 .generate_constraints(cs.clone())
424 .unwrap();
425 assert!(cs.is_satisfied().unwrap());
426 cs.num_constraints()
427}
428
429#[cfg(test)]
430mod tests {
431 use crate::parameters::poseidon_params;
432
433 use super::*;
434
435 use ark_std::UniformRand;
436
437 fn produce_tiny_r1cs() -> (R1CSInstance, Vec<Scalar>, Vec<Scalar>) {
438 // three constraints over five variables Z1, Z2, Z3, Z4, and Z5
439 // rounded to the nearest power of two
440 let num_cons = 128;
441 let num_vars = 256;
442 let num_inputs = 2;
443
444 // encode the above constraints into three matrices
445 let mut A: Vec<(usize, usize, Scalar)> = Vec::new();
446 let mut B: Vec<(usize, usize, Scalar)> = Vec::new();
447 let mut C: Vec<(usize, usize, Scalar)> = Vec::new();
448
449 let one = Scalar::one();
450 // constraint 0 entries
451 // (Z1 + Z2) * I0 - Z3 = 0;
452 A.push((0, 0, one));
453 A.push((0, 1, one));
454 B.push((0, num_vars + 1, one));
455 C.push((0, 2, one));
456
457 // constraint 1 entries
458 // (Z1 + I1) * (Z3) - Z4 = 0
459 A.push((1, 0, one));
460 A.push((1, num_vars + 2, one));
461 B.push((1, 2, one));
462 C.push((1, 3, one));
463 // constraint 3 entries
464 // Z5 * 1 - 0 = 0
465 A.push((2, 4, one));
466 B.push((2, num_vars, one));
467
468 let inst = R1CSInstance::new(num_cons, num_vars, num_inputs, &A, &B, &C);
469
470 // compute a satisfying assignment
471 let mut rng = ark_std::rand::thread_rng();
472 let i0 = Scalar::rand(&mut rng);
473 let i1 = Scalar::rand(&mut rng);
474 let z1 = Scalar::rand(&mut rng);
475 let z2 = Scalar::rand(&mut rng);
476 let z3 = (z1 + z2) * i0; // constraint 1: (Z1 + Z2) * I0 - Z3 = 0;
477 let z4 = (z1 + i1) * z3; // constraint 2: (Z1 + I1) * (Z3) - Z4 = 0
478 let z5 = Scalar::zero(); //constraint 3
479
480 let mut vars = vec![Scalar::zero(); num_vars];
481 vars[0] = z1;
482 vars[1] = z2;
483 vars[2] = z3;
484 vars[3] = z4;
485 vars[4] = z5;
486
487 let mut input = vec![Scalar::zero(); num_inputs];
488 input[0] = i0;
489 input[1] = i1;
490
491 (inst, vars, input)
492 }
493
494 #[test]
495 fn test_tiny_r1cs() {
496 let (inst, vars, input) = tests::produce_tiny_r1cs();
497 let is_sat = inst.is_sat(&vars, &input);
498 assert!(is_sat);
499 }
500
501 #[test]
502 fn test_synthetic_r1cs() {
503 let (inst, vars, input) = R1CSInstance::produce_synthetic_r1cs(1024, 1024, 10);
504 let is_sat = inst.is_sat(&vars, &input);
505 assert!(is_sat);
506 }
507
508 #[test]
509 pub fn check_r1cs_proof() {
510 let num_vars = 1024;
511 let num_cons = num_vars;
512 let num_inputs = 10;
513 let (inst, vars, input) =
514 R1CSInstance::produce_synthetic_r1cs(num_cons, num_vars, num_inputs);
515
516 let gens = R1CSGens::new(b"test-m", num_cons, num_vars);
517
518 let params = poseidon_params();
519 // let mut random_tape = RandomTape::new(b"proof");
520
521 let mut prover_transcript = PoseidonTranscript::new(¶ms);
522 let (proof, rx, ry) = R1CSProof::prove(&inst, vars, &input, &gens, &mut prover_transcript);
523
524 let inst_evals = inst.evaluate(&rx, &ry);
525
526 let mut verifier_transcript = PoseidonTranscript::new(¶ms);
527
528 // if you want to check the test fails
529 // input[0] = Scalar::zero();
530
531 assert!(proof
532 .verify_groth16(
533 inst.get_num_vars(),
534 inst.get_num_cons(),
535 &input,
536 &inst_evals,
537 &mut verifier_transcript,
538 &gens,
539 )
540 .is_ok());
541 }
542}