testudo/src/r1csproof.rs
src/r1csproof.rsRaw
1#![allow(clippy::too_many_arguments)]
2use super::commitments::{Commitments, MultiCommitGens};
3use super::dense_mlpoly::{
4 DensePolynomial, EqPolynomial, PolyCommitment, PolyCommitmentGens, PolyEvalProof,
5};
6use super::errors::ProofVerifyError;
7use super::group::{CompressedGroup, GroupElement, VartimeMultiscalarMul};
8use super::math::Math;
9use super::nizk::{EqualityProof, KnowledgeProof, ProductProof};
10use super::r1csinstance::R1CSInstance;
11use super::random::RandomTape;
12use super::scalar::Scalar;
13use super::sparse_mlpoly::{SparsePolyEntry, SparsePolynomial};
14use super::sumcheck::ZKSumcheckInstanceProof;
15use super::timer::Timer;
16use super::transcript::{AppendToTranscript, ProofTranscript};
17use core::iter;
18use merlin::Transcript;
19use serde::{Deserialize, Serialize};
20
21#[derive(Serialize, Deserialize, Debug)]
22pub struct R1CSProof {
23 comm_vars: PolyCommitment,
24 sc_proof_phase1: ZKSumcheckInstanceProof,
25 claims_phase2: (
26 CompressedGroup,
27 CompressedGroup,
28 CompressedGroup,
29 CompressedGroup,
30 ),
31 pok_claims_phase2: (KnowledgeProof, ProductProof),
32 proof_eq_sc_phase1: EqualityProof,
33 sc_proof_phase2: ZKSumcheckInstanceProof,
34 comm_vars_at_ry: CompressedGroup,
35 proof_eval_vars_at_ry: PolyEvalProof,
36 proof_eq_sc_phase2: EqualityProof,
37}
38
39pub struct R1CSSumcheckGens {
40 gens_1: MultiCommitGens,
41 gens_3: MultiCommitGens,
42 gens_4: MultiCommitGens,
43}
44
45// TODO: fix passing gens_1_ref
46impl R1CSSumcheckGens {
47 pub fn new(label: &'static [u8], gens_1_ref: &MultiCommitGens) -> Self {
48 let gens_1 = gens_1_ref.clone();
49 let gens_3 = MultiCommitGens::new(3, label);
50 let gens_4 = MultiCommitGens::new(4, label);
51
52 R1CSSumcheckGens {
53 gens_1,
54 gens_3,
55 gens_4,
56 }
57 }
58}
59
60pub struct R1CSGens {
61 gens_sc: R1CSSumcheckGens,
62 gens_pc: PolyCommitmentGens,
63}
64
65impl R1CSGens {
66 pub fn new(label: &'static [u8], _num_cons: usize, num_vars: usize) -> Self {
67 let num_poly_vars = num_vars.log2();
68 let gens_pc = PolyCommitmentGens::new(num_poly_vars, label);
69 let gens_sc = R1CSSumcheckGens::new(label, &gens_pc.gens.gens_1);
70 R1CSGens { gens_sc, gens_pc }
71 }
72}
73
74impl R1CSProof {
75 fn prove_phase_one(
76 num_rounds: usize,
77 evals_tau: &mut DensePolynomial,
78 evals_Az: &mut DensePolynomial,
79 evals_Bz: &mut DensePolynomial,
80 evals_Cz: &mut DensePolynomial,
81 gens: &R1CSSumcheckGens,
82 transcript: &mut Transcript,
83 random_tape: &mut RandomTape,
84 ) -> (ZKSumcheckInstanceProof, Vec<Scalar>, Vec<Scalar>, Scalar) {
85 let comb_func = |poly_A_comp: &Scalar,
86 poly_B_comp: &Scalar,
87 poly_C_comp: &Scalar,
88 poly_D_comp: &Scalar|
89 -> Scalar { poly_A_comp * (poly_B_comp * poly_C_comp - poly_D_comp) };
90
91 let (sc_proof_phase_one, r, claims, blind_claim_postsc) =
92 ZKSumcheckInstanceProof::prove_cubic_with_additive_term(
93 &Scalar::zero(), // claim is zero
94 &Scalar::zero(), // blind for claim is also zero
95 num_rounds,
96 evals_tau,
97 evals_Az,
98 evals_Bz,
99 evals_Cz,
100 comb_func,
101 &gens.gens_1,
102 &gens.gens_4,
103 transcript,
104 random_tape,
105 );
106
107 (sc_proof_phase_one, r, claims, blind_claim_postsc)
108 }
109
110 fn prove_phase_two(
111 num_rounds: usize,
112 claim: &Scalar,
113 blind_claim: &Scalar,
114 evals_z: &mut DensePolynomial,
115 evals_ABC: &mut DensePolynomial,
116 gens: &R1CSSumcheckGens,
117 transcript: &mut Transcript,
118 random_tape: &mut RandomTape,
119 ) -> (ZKSumcheckInstanceProof, Vec<Scalar>, Vec<Scalar>, Scalar) {
120 let comb_func =
121 |poly_A_comp: &Scalar, poly_B_comp: &Scalar| -> Scalar { poly_A_comp * poly_B_comp };
122 let (sc_proof_phase_two, r, claims, blind_claim_postsc) = ZKSumcheckInstanceProof::prove_quad(
123 claim,
124 blind_claim,
125 num_rounds,
126 evals_z,
127 evals_ABC,
128 comb_func,
129 &gens.gens_1,
130 &gens.gens_3,
131 transcript,
132 random_tape,
133 );
134
135 (sc_proof_phase_two, r, claims, blind_claim_postsc)
136 }
137
138 fn protocol_name() -> &'static [u8] {
139 b"R1CS proof"
140 }
141
142 pub fn prove(
143 inst: &R1CSInstance,
144 vars: Vec<Scalar>,
145 input: &[Scalar],
146 gens: &R1CSGens,
147 transcript: &mut Transcript,
148 random_tape: &mut RandomTape,
149 ) -> (R1CSProof, Vec<Scalar>, Vec<Scalar>) {
150 let timer_prove = Timer::new("R1CSProof::prove");
151 transcript.append_protocol_name(R1CSProof::protocol_name());
152
153 // we currently require the number of |inputs| + 1 to be at most number of vars
154 assert!(input.len() < vars.len());
155
156 let timer_commit = Timer::new("polycommit");
157 let (poly_vars, comm_vars, blinds_vars) = {
158 // create a multilinear polynomial using the supplied assignment for variables
159 let poly_vars = DensePolynomial::new(vars.clone());
160
161 // produce a commitment to the satisfying assignment
162 let (comm_vars, blinds_vars) = poly_vars.commit(&gens.gens_pc, Some(random_tape));
163
164 // add the commitment to the prover's transcript
165 comm_vars.append_to_transcript(b"poly_commitment", transcript);
166 (poly_vars, comm_vars, blinds_vars)
167 };
168 timer_commit.stop();
169
170 let timer_sc_proof_phase1 = Timer::new("prove_sc_phase_one");
171
172 // append input to variables to create a single vector z
173 let z = {
174 let num_inputs = input.len();
175 let num_vars = vars.len();
176 let mut z = vars;
177 z.extend(&vec![Scalar::one()]); // add constant term in z
178 z.extend(input);
179 z.extend(&vec![Scalar::zero(); num_vars - num_inputs - 1]); // we will pad with zeros
180 z
181 };
182
183 // derive the verifier's challenge tau
184 let (num_rounds_x, num_rounds_y) = (inst.get_num_cons().log2(), z.len().log2());
185 let tau = transcript.challenge_vector(b"challenge_tau", num_rounds_x);
186 // compute the initial evaluation table for R(\tau, x)
187 let mut poly_tau = DensePolynomial::new(EqPolynomial::new(tau).evals());
188 let (mut poly_Az, mut poly_Bz, mut poly_Cz) =
189 inst.multiply_vec(inst.get_num_cons(), z.len(), &z);
190
191 let (sc_proof_phase1, rx, _claims_phase1, blind_claim_postsc1) = R1CSProof::prove_phase_one(
192 num_rounds_x,
193 &mut poly_tau,
194 &mut poly_Az,
195 &mut poly_Bz,
196 &mut poly_Cz,
197 &gens.gens_sc,
198 transcript,
199 random_tape,
200 );
201 assert_eq!(poly_tau.len(), 1);
202 assert_eq!(poly_Az.len(), 1);
203 assert_eq!(poly_Bz.len(), 1);
204 assert_eq!(poly_Cz.len(), 1);
205 timer_sc_proof_phase1.stop();
206
207 let (tau_claim, Az_claim, Bz_claim, Cz_claim) =
208 (&poly_tau[0], &poly_Az[0], &poly_Bz[0], &poly_Cz[0]);
209 let (Az_blind, Bz_blind, Cz_blind, prod_Az_Bz_blind) = (
210 random_tape.random_scalar(b"Az_blind"),
211 random_tape.random_scalar(b"Bz_blind"),
212 random_tape.random_scalar(b"Cz_blind"),
213 random_tape.random_scalar(b"prod_Az_Bz_blind"),
214 );
215
216 let (pok_Cz_claim, comm_Cz_claim) = {
217 KnowledgeProof::prove(
218 &gens.gens_sc.gens_1,
219 transcript,
220 random_tape,
221 &Cz_claim,
222 &Cz_blind,
223 )
224 };
225
226 let (proof_prod, comm_Az_claim, comm_Bz_claim, comm_prod_Az_Bz_claims) = {
227 let prod = Az_claim * Bz_claim;
228 ProductProof::prove(
229 &gens.gens_sc.gens_1,
230 transcript,
231 random_tape,
232 &Az_claim,
233 &Az_blind,
234 &Bz_claim,
235 &Bz_blind,
236 &prod,
237 &prod_Az_Bz_blind,
238 )
239 };
240
241 comm_Az_claim.append_to_transcript(b"comm_Az_claim", transcript);
242 comm_Bz_claim.append_to_transcript(b"comm_Bz_claim", transcript);
243 comm_Cz_claim.append_to_transcript(b"comm_Cz_claim", transcript);
244 comm_prod_Az_Bz_claims.append_to_transcript(b"comm_prod_Az_Bz_claims", transcript);
245
246 // prove the final step of sum-check #1
247 let taus_bound_rx = tau_claim;
248 let blind_expected_claim_postsc1 = taus_bound_rx * (prod_Az_Bz_blind - Cz_blind);
249 let claim_post_phase1 = (Az_claim * Bz_claim - Cz_claim) * taus_bound_rx;
250 let (proof_eq_sc_phase1, _C1, _C2) = EqualityProof::prove(
251 &gens.gens_sc.gens_1,
252 transcript,
253 random_tape,
254 &claim_post_phase1,
255 &blind_expected_claim_postsc1,
256 &claim_post_phase1,
257 &blind_claim_postsc1,
258 );
259
260 let timer_sc_proof_phase2 = Timer::new("prove_sc_phase_two");
261 // combine the three claims into a single claim
262 let r_A = transcript.challenge_scalar(b"challenege_Az");
263 let r_B = transcript.challenge_scalar(b"challenege_Bz");
264 let r_C = transcript.challenge_scalar(b"challenege_Cz");
265 let claim_phase2 = r_A * Az_claim + r_B * Bz_claim + r_C * Cz_claim;
266 let blind_claim_phase2 = r_A * Az_blind + r_B * Bz_blind + r_C * Cz_blind;
267
268 let evals_ABC = {
269 // compute the initial evaluation table for R(\tau, x)
270 let evals_rx = EqPolynomial::new(rx.clone()).evals();
271 let (evals_A, evals_B, evals_C) =
272 inst.compute_eval_table_sparse(inst.get_num_cons(), z.len(), &evals_rx);
273
274 assert_eq!(evals_A.len(), evals_B.len());
275 assert_eq!(evals_A.len(), evals_C.len());
276 (0..evals_A.len())
277 .map(|i| r_A * evals_A[i] + r_B * evals_B[i] + r_C * evals_C[i])
278 .collect::<Vec<Scalar>>()
279 };
280
281 // another instance of the sum-check protocol
282 let (sc_proof_phase2, ry, claims_phase2, blind_claim_postsc2) = R1CSProof::prove_phase_two(
283 num_rounds_y,
284 &claim_phase2,
285 &blind_claim_phase2,
286 &mut DensePolynomial::new(z),
287 &mut DensePolynomial::new(evals_ABC),
288 &gens.gens_sc,
289 transcript,
290 random_tape,
291 );
292 timer_sc_proof_phase2.stop();
293
294 let timer_polyeval = Timer::new("polyeval");
295 let eval_vars_at_ry = poly_vars.evaluate(&ry[1..].to_vec());
296 let blind_eval = random_tape.random_scalar(b"blind_eval");
297 let (proof_eval_vars_at_ry, comm_vars_at_ry) = PolyEvalProof::prove(
298 &poly_vars,
299 Some(&blinds_vars),
300 &ry[1..].to_vec(),
301 &eval_vars_at_ry,
302 Some(&blind_eval),
303 &gens.gens_pc,
304 transcript,
305 random_tape,
306 );
307 timer_polyeval.stop();
308
309 // prove the final step of sum-check #2
310 let blind_eval_Z_at_ry = (Scalar::one() - ry[0]) * blind_eval;
311 let blind_expected_claim_postsc2 = claims_phase2[1] * blind_eval_Z_at_ry;
312 let claim_post_phase2 = claims_phase2[0] * claims_phase2[1];
313 let (proof_eq_sc_phase2, _C1, _C2) = EqualityProof::prove(
314 &gens.gens_pc.gens.gens_1,
315 transcript,
316 random_tape,
317 &claim_post_phase2,
318 &blind_expected_claim_postsc2,
319 &claim_post_phase2,
320 &blind_claim_postsc2,
321 );
322
323 timer_prove.stop();
324
325 (
326 R1CSProof {
327 comm_vars,
328 sc_proof_phase1,
329 claims_phase2: (
330 comm_Az_claim,
331 comm_Bz_claim,
332 comm_Cz_claim,
333 comm_prod_Az_Bz_claims,
334 ),
335 pok_claims_phase2: (pok_Cz_claim, proof_prod),
336 proof_eq_sc_phase1,
337 sc_proof_phase2,
338 comm_vars_at_ry,
339 proof_eval_vars_at_ry,
340 proof_eq_sc_phase2,
341 },
342 rx,
343 ry,
344 )
345 }
346
347 pub fn verify(
348 &self,
349 num_vars: usize,
350 num_cons: usize,
351 input: &[Scalar],
352 evals: &(Scalar, Scalar, Scalar),
353 transcript: &mut Transcript,
354 gens: &R1CSGens,
355 ) -> Result<(Vec<Scalar>, Vec<Scalar>), ProofVerifyError> {
356 transcript.append_protocol_name(R1CSProof::protocol_name());
357
358 let n = num_vars;
359 // add the commitment to the verifier's transcript
360 self
361 .comm_vars
362 .append_to_transcript(b"poly_commitment", transcript);
363
364 let (num_rounds_x, num_rounds_y) = (num_cons.log2(), (2 * num_vars).log2());
365
366 // derive the verifier's challenge tau
367 let tau = transcript.challenge_vector(b"challenge_tau", num_rounds_x);
368
369 // verify the first sum-check instance
370 let claim_phase1 = Scalar::zero()
371 .commit(&Scalar::zero(), &gens.gens_sc.gens_1)
372 .compress();
373 let (comm_claim_post_phase1, rx) = self
374 .sc_proof_phase1
375 .verify(
376 &claim_phase1,
377 num_rounds_x,
378 3,
379 &gens.gens_sc.gens_1,
380 &gens.gens_sc.gens_4,
381 transcript,
382 )
383 .unwrap();
384
385 // perform the intermediate sum-check test with claimed Az, Bz, and Cz
386 let (comm_Az_claim, comm_Bz_claim, comm_Cz_claim, comm_prod_Az_Bz_claims) = &self.claims_phase2;
387 let (pok_Cz_claim, proof_prod) = &self.pok_claims_phase2;
388
389 assert!(pok_Cz_claim
390 .verify(&gens.gens_sc.gens_1, transcript, &comm_Cz_claim)
391 .is_ok());
392 assert!(proof_prod
393 .verify(
394 &gens.gens_sc.gens_1,
395 transcript,
396 &comm_Az_claim,
397 &comm_Bz_claim,
398 &comm_prod_Az_Bz_claims
399 )
400 .is_ok());
401
402 comm_Az_claim.append_to_transcript(b"comm_Az_claim", transcript);
403 comm_Bz_claim.append_to_transcript(b"comm_Bz_claim", transcript);
404 comm_Cz_claim.append_to_transcript(b"comm_Cz_claim", transcript);
405 comm_prod_Az_Bz_claims.append_to_transcript(b"comm_prod_Az_Bz_claims", transcript);
406
407 let taus_bound_rx: Scalar = (0..rx.len())
408 .map(|i| rx[i] * tau[i] + (Scalar::one() - rx[i]) * (Scalar::one() - tau[i]))
409 .product();
410 let expected_claim_post_phase1 = (taus_bound_rx
411 * (comm_prod_Az_Bz_claims.decompress().unwrap() - comm_Cz_claim.decompress().unwrap()))
412 .compress();
413
414 // verify proof that expected_claim_post_phase1 == claim_post_phase1
415 assert!(self
416 .proof_eq_sc_phase1
417 .verify(
418 &gens.gens_sc.gens_1,
419 transcript,
420 &expected_claim_post_phase1,
421 &comm_claim_post_phase1,
422 )
423 .is_ok());
424
425 // derive three public challenges and then derive a joint claim
426 let r_A = transcript.challenge_scalar(b"challenege_Az");
427 let r_B = transcript.challenge_scalar(b"challenege_Bz");
428 let r_C = transcript.challenge_scalar(b"challenege_Cz");
429
430 // r_A * comm_Az_claim + r_B * comm_Bz_claim + r_C * comm_Cz_claim;
431 let comm_claim_phase2 = GroupElement::vartime_multiscalar_mul(
432 iter::once(&r_A)
433 .chain(iter::once(&r_B))
434 .chain(iter::once(&r_C)),
435 iter::once(&comm_Az_claim)
436 .chain(iter::once(&comm_Bz_claim))
437 .chain(iter::once(&comm_Cz_claim))
438 .map(|pt| pt.decompress().unwrap())
439 .collect::<Vec<GroupElement>>(),
440 )
441 .compress();
442
443 // verify the joint claim with a sum-check protocol
444 let (comm_claim_post_phase2, ry) = self
445 .sc_proof_phase2
446 .verify(
447 &comm_claim_phase2,
448 num_rounds_y,
449 2,
450 &gens.gens_sc.gens_1,
451 &gens.gens_sc.gens_3,
452 transcript,
453 )
454 .unwrap();
455
456 // verify Z(ry) proof against the initial commitment
457 assert!(self
458 .proof_eval_vars_at_ry
459 .verify(
460 &gens.gens_pc,
461 transcript,
462 &ry[1..].to_vec(),
463 &self.comm_vars_at_ry,
464 &self.comm_vars
465 )
466 .is_ok());
467
468 let poly_input_eval = {
469 // constant term
470 let mut input_as_sparse_poly_entries = vec![SparsePolyEntry::new(0, Scalar::one())];
471 //remaining inputs
472 input_as_sparse_poly_entries.extend(
473 (0..input.len())
474 .map(|i| SparsePolyEntry::new(i + 1, input[i]))
475 .collect::<Vec<SparsePolyEntry>>(),
476 );
477 SparsePolynomial::new(n.log2(), input_as_sparse_poly_entries).evaluate(&ry[1..].to_vec())
478 };
479
480 // compute commitment to eval_Z_at_ry = (Scalar::one() - ry[0]) * self.eval_vars_at_ry + ry[0] * poly_input_eval
481 let comm_eval_Z_at_ry = GroupElement::vartime_multiscalar_mul(
482 iter::once(Scalar::one() - ry[0]).chain(iter::once(ry[0])),
483 iter::once(&self.comm_vars_at_ry.decompress().unwrap()).chain(iter::once(
484 &poly_input_eval.commit(&Scalar::zero(), &gens.gens_pc.gens.gens_1),
485 )),
486 );
487
488 // perform the final check in the second sum-check protocol
489 let (eval_A_r, eval_B_r, eval_C_r) = evals;
490 let expected_claim_post_phase2 =
491 ((r_A * eval_A_r + r_B * eval_B_r + r_C * eval_C_r) * comm_eval_Z_at_ry).compress();
492 // verify proof that expected_claim_post_phase1 == claim_post_phase1
493 assert!(self
494 .proof_eq_sc_phase2
495 .verify(
496 &gens.gens_sc.gens_1,
497 transcript,
498 &expected_claim_post_phase2,
499 &comm_claim_post_phase2,
500 )
501 .is_ok());
502
503 Ok((rx, ry))
504 }
505}
506
507#[cfg(test)]
508mod tests {
509 use super::*;
510 use rand::rngs::OsRng;
511
512 fn produce_tiny_r1cs() -> (R1CSInstance, Vec<Scalar>, Vec<Scalar>) {
513 // three constraints over five variables Z1, Z2, Z3, Z4, and Z5
514 // rounded to the nearest power of two
515 let num_cons = 128;
516 let num_vars = 256;
517 let num_inputs = 2;
518
519 // encode the above constraints into three matrices
520 let mut A: Vec<(usize, usize, Scalar)> = Vec::new();
521 let mut B: Vec<(usize, usize, Scalar)> = Vec::new();
522 let mut C: Vec<(usize, usize, Scalar)> = Vec::new();
523
524 let one = Scalar::one();
525 // constraint 0 entries
526 // (Z1 + Z2) * I0 - Z3 = 0;
527 A.push((0, 0, one));
528 A.push((0, 1, one));
529 B.push((0, num_vars + 1, one));
530 C.push((0, 2, one));
531
532 // constraint 1 entries
533 // (Z1 + I1) * (Z3) - Z4 = 0
534 A.push((1, 0, one));
535 A.push((1, num_vars + 2, one));
536 B.push((1, 2, one));
537 C.push((1, 3, one));
538 // constraint 3 entries
539 // Z5 * 1 - 0 = 0
540 A.push((2, 4, one));
541 B.push((2, num_vars, one));
542
543 let inst = R1CSInstance::new(num_cons, num_vars, num_inputs, &A, &B, &C);
544
545 // compute a satisfying assignment
546 let mut csprng: OsRng = OsRng;
547 let i0 = Scalar::random(&mut csprng);
548 let i1 = Scalar::random(&mut csprng);
549 let z1 = Scalar::random(&mut csprng);
550 let z2 = Scalar::random(&mut csprng);
551 let z3 = (z1 + z2) * i0; // constraint 1: (Z1 + Z2) * I0 - Z3 = 0;
552 let z4 = (z1 + i1) * z3; // constraint 2: (Z1 + I1) * (Z3) - Z4 = 0
553 let z5 = Scalar::zero(); //constraint 3
554
555 let mut vars = vec![Scalar::zero(); num_vars];
556 vars[0] = z1;
557 vars[1] = z2;
558 vars[2] = z3;
559 vars[3] = z4;
560 vars[4] = z5;
561
562 let mut input = vec![Scalar::zero(); num_inputs];
563 input[0] = i0;
564 input[1] = i1;
565
566 (inst, vars, input)
567 }
568
569 #[test]
570 fn test_tiny_r1cs() {
571 let (inst, vars, input) = tests::produce_tiny_r1cs();
572 let is_sat = inst.is_sat(&vars, &input);
573 assert_eq!(is_sat, true);
574 }
575
576 #[test]
577 fn test_synthetic_r1cs() {
578 let (inst, vars, input) = R1CSInstance::produce_synthetic_r1cs(1024, 1024, 10);
579 let is_sat = inst.is_sat(&vars, &input);
580 assert_eq!(is_sat, true);
581 }
582
583 #[test]
584 pub fn check_r1cs_proof() {
585 let num_vars = 1024;
586 let num_cons = num_vars;
587 let num_inputs = 10;
588 let (inst, vars, input) = R1CSInstance::produce_synthetic_r1cs(num_cons, num_vars, num_inputs);
589
590 let gens = R1CSGens::new(b"test-m", num_cons, num_vars);
591
592 let mut random_tape = RandomTape::new(b"proof");
593 let mut prover_transcript = Transcript::new(b"example");
594 let (proof, rx, ry) = R1CSProof::prove(
595 &inst,
596 vars,
597 &input,
598 &gens,
599 &mut prover_transcript,
600 &mut random_tape,
601 );
602
603 let inst_evals = inst.evaluate(&rx, &ry);
604
605 let mut verifier_transcript = Transcript::new(b"example");
606 assert!(proof
607 .verify(
608 inst.get_num_vars(),
609 inst.get_num_cons(),
610 &input,
611 &inst_evals,
612 &mut verifier_transcript,
613 &gens,
614 )
615 .is_ok());
616 }
617}