testudo/src/r1csproof.rs
src/r1csproof.rsRaw
1#![allow(clippy::too_many_arguments)]
2use crate::group::CompressedGroup;
3use crate::sumcheck::SumcheckInstanceProof;
4
5use super::commitments::{Commitments, MultiCommitGens};
6use super::dense_mlpoly::{
7 DensePolynomial, EqPolynomial, PolyCommitment, PolyCommitmentGens, PolyEvalProof,
8};
9use super::errors::ProofVerifyError;
10use super::group::{
11 CompressGroupElement, DecompressGroupElement, GroupElement, VartimeMultiscalarMul,
12};
13use super::math::Math;
14use super::nizk::{EqualityProof, KnowledgeProof, ProductProof};
15use super::r1csinstance::R1CSInstance;
16use super::random::RandomTape;
17use super::scalar::Scalar;
18use super::sparse_mlpoly::{SparsePolyEntry, SparsePolynomial};
19use super::sumcheck::ZKSumcheckInstanceProof;
20use super::timer::Timer;
21use super::transcript::{AppendToTranscript, ProofTranscript};
22use ark_ec::ProjectiveCurve;
23use ark_ff::PrimeField;
24use ark_serialize::*;
25use ark_std::{One, Zero};
26use core::iter;
27use merlin::Transcript;
28
29#[derive(CanonicalSerialize, CanonicalDeserialize, Debug)]
30pub struct R1CSProof {
31 sc_proof_phase1: SumcheckInstanceProof,
32 claims_phase2: (Scalar, Scalar, Scalar, Scalar),
33 // pok_claims_phase2: (KnowledgeProof, ProductProof),
34 // proof_eq_sc_phase1: EqualityProof,
35 sc_proof_phase2: SumcheckInstanceProof,
36 eval_vars_at_ry: Scalar,
37 // proof_eval_vars_at_ry: PolyEvalProof,
38 // proof_eq_sc_phase2: EqualityProof,
39}
40
41pub struct R1CSSumcheckGens {
42 gens_1: MultiCommitGens,
43 gens_3: MultiCommitGens,
44 gens_4: MultiCommitGens,
45}
46
47// TODO: fix passing gens_1_ref
48impl R1CSSumcheckGens {
49 pub fn new(label: &'static [u8], gens_1_ref: &MultiCommitGens) -> Self {
50 let gens_1 = gens_1_ref.clone();
51 let gens_3 = MultiCommitGens::new(3, label);
52 let gens_4 = MultiCommitGens::new(4, label);
53
54 R1CSSumcheckGens {
55 gens_1,
56 gens_3,
57 gens_4,
58 }
59 }
60}
61
62pub struct R1CSGens {
63 gens_sc: R1CSSumcheckGens,
64 gens_pc: PolyCommitmentGens,
65}
66
67impl R1CSGens {
68 pub fn new(label: &'static [u8], _num_cons: usize, num_vars: usize) -> Self {
69 let num_poly_vars = num_vars.log_2() as usize;
70 let gens_pc = PolyCommitmentGens::new(num_poly_vars, label);
71 let gens_sc = R1CSSumcheckGens::new(label, &gens_pc.gens.gens_1);
72 R1CSGens { gens_sc, gens_pc }
73 }
74}
75
76impl R1CSProof {
77 fn prove_phase_one(
78 num_rounds: usize,
79 evals_tau: &mut DensePolynomial,
80 evals_Az: &mut DensePolynomial,
81 evals_Bz: &mut DensePolynomial,
82 evals_Cz: &mut DensePolynomial,
83 transcript: &mut Transcript,
84 ) -> (SumcheckInstanceProof, Vec<Scalar>, Vec<Scalar>) {
85 let comb_func =
86 |poly_tau_comp: &Scalar,
87 poly_A_comp: &Scalar,
88 poly_B_comp: &Scalar,
89 poly_C_comp: &Scalar|
90 -> Scalar { (*poly_tau_comp) * ((*poly_A_comp) * poly_B_comp - poly_C_comp) };
91
92 let (sc_proof_phase_one, r, claims) = SumcheckInstanceProof::prove_cubic_with_additive_term(
93 &Scalar::zero(), // claim is zero
94 num_rounds,
95 evals_tau,
96 evals_Az,
97 evals_Bz,
98 evals_Cz,
99 comb_func,
100 transcript,
101 );
102
103 (sc_proof_phase_one, r, claims)
104 }
105
106 fn prove_phase_two(
107 num_rounds: usize,
108 claim: &Scalar,
109 evals_z: &mut DensePolynomial,
110 evals_ABC: &mut DensePolynomial,
111 transcript: &mut Transcript,
112 ) -> (SumcheckInstanceProof, Vec<Scalar>, Vec<Scalar>) {
113 let comb_func =
114 |poly_A_comp: &Scalar, poly_B_comp: &Scalar| -> Scalar { (*poly_A_comp) * poly_B_comp };
115 let (sc_proof_phase_two, r, claims) = SumcheckInstanceProof::prove_quad(
116 claim, num_rounds, evals_z, evals_ABC, comb_func, transcript,
117 );
118
119 (sc_proof_phase_two, r, claims)
120 }
121
122 fn protocol_name() -> &'static [u8] {
123 b"R1CS proof"
124 }
125
126 pub fn prove(
127 inst: &R1CSInstance,
128 vars: Vec<Scalar>,
129 input: &[Scalar],
130 gens: &R1CSGens,
131 transcript: &mut Transcript,
132 random_tape: &mut RandomTape,
133 ) -> (R1CSProof, Vec<Scalar>, Vec<Scalar>) {
134 let timer_prove = Timer::new("R1CSProof::prove");
135 transcript.append_protocol_name(R1CSProof::protocol_name());
136
137 // we currently require the number of |inputs| + 1 to be at most number of vars
138 assert!(input.len() < vars.len());
139
140 input.append_to_transcript(b"input", transcript);
141
142 let poly_vars = DensePolynomial::new(vars.clone());
143
144 let timer_sc_proof_phase1 = Timer::new("prove_sc_phase_one");
145
146 // append input to variables to create a single vector z
147 let z = {
148 let num_inputs = input.len();
149 let num_vars = vars.len();
150 let mut z = vars;
151 z.extend(&vec![Scalar::one()]); // add constant term in z
152 z.extend(input);
153 z.extend(&vec![Scalar::zero(); num_vars - num_inputs - 1]); // we will pad with zeros
154 z
155 };
156
157 // derive the verifier's challenge tau
158 let (num_rounds_x, num_rounds_y) = (
159 inst.get_num_cons().log_2() as usize,
160 z.len().log_2() as usize,
161 );
162 let tau = transcript.challenge_vector(b"challenge_tau", num_rounds_x);
163 // compute the initial evaluation table for R(\tau, x)
164 let mut poly_tau = DensePolynomial::new(EqPolynomial::new(tau).evals());
165 let (mut poly_Az, mut poly_Bz, mut poly_Cz) =
166 inst.multiply_vec(inst.get_num_cons(), z.len(), &z);
167
168 let (sc_proof_phase1, rx, _claims_phase1) = R1CSProof::prove_phase_one(
169 num_rounds_x,
170 &mut poly_tau,
171 &mut poly_Az,
172 &mut poly_Bz,
173 &mut poly_Cz,
174 transcript,
175 );
176 assert_eq!(poly_tau.len(), 1);
177 assert_eq!(poly_Az.len(), 1);
178 assert_eq!(poly_Bz.len(), 1);
179 assert_eq!(poly_Cz.len(), 1);
180 timer_sc_proof_phase1.stop();
181
182 let (tau_claim, Az_claim, Bz_claim, Cz_claim) =
183 (&poly_tau[0], &poly_Az[0], &poly_Bz[0], &poly_Cz[0]);
184 let prod_Az_Bz_claims = (*Az_claim) * Bz_claim;
185
186 // prove the final step of sum-check #1
187 let taus_bound_rx = tau_claim;
188 let claim_post_phase1 = ((*Az_claim) * Bz_claim - Cz_claim) * taus_bound_rx;
189
190 let timer_sc_proof_phase2 = Timer::new("prove_sc_phase_two");
191 // combine the three claims into a single claim
192 let r_A = transcript.challenge_scalar(b"challenege_Az");
193 let r_B = transcript.challenge_scalar(b"challenege_Bz");
194 let r_C = transcript.challenge_scalar(b"challenege_Cz");
195 let claim_phase2 = r_A * Az_claim + r_B * Bz_claim + r_C * Cz_claim;
196
197 let evals_ABC = {
198 // compute the initial evaluation table for R(\tau, x)
199 let evals_rx = EqPolynomial::new(rx.clone()).evals();
200 let (evals_A, evals_B, evals_C) =
201 inst.compute_eval_table_sparse(inst.get_num_cons(), z.len(), &evals_rx);
202
203 assert_eq!(evals_A.len(), evals_B.len());
204 assert_eq!(evals_A.len(), evals_C.len());
205 (0..evals_A.len())
206 .map(|i| r_A * evals_A[i] + r_B * evals_B[i] + r_C * evals_C[i])
207 .collect::<Vec<Scalar>>()
208 };
209
210 // another instance of the sum-check protocol
211 let (sc_proof_phase2, ry, claims_phase2) = R1CSProof::prove_phase_two(
212 num_rounds_y,
213 &claim_phase2,
214 &mut DensePolynomial::new(z),
215 &mut DensePolynomial::new(evals_ABC),
216 transcript,
217 );
218 timer_sc_proof_phase2.stop();
219
220 let timer_polyeval = Timer::new("polyeval");
221 let eval_vars_at_ry = poly_vars.evaluate(&ry[1..].to_vec());
222 timer_polyeval.stop();
223
224 timer_prove.stop();
225
226 (
227 R1CSProof {
228 sc_proof_phase1,
229 claims_phase2: (*Az_claim, *Bz_claim, *Cz_claim, prod_Az_Bz_claims),
230 sc_proof_phase2,
231 eval_vars_at_ry,
232 },
233 rx,
234 ry,
235 )
236 }
237
238 pub fn verify(
239 &self,
240 num_vars: usize,
241 num_cons: usize,
242 input: &[Scalar],
243 evals: &(Scalar, Scalar, Scalar),
244 transcript: &mut Transcript,
245 gens: &R1CSGens,
246 ) -> Result<(Vec<Scalar>, Vec<Scalar>), ProofVerifyError> {
247 transcript.append_protocol_name(R1CSProof::protocol_name());
248
249 input.append_to_transcript(b"input", transcript);
250
251 let n = num_vars;
252
253 let (num_rounds_x, num_rounds_y) = (num_cons.log_2() as usize, (2 * num_vars).log_2() as usize);
254
255 // derive the verifier's challenge tau
256 let tau = transcript.challenge_vector(b"challenge_tau", num_rounds_x);
257
258 // verify the first sum-check instance
259 let claim_phase1 = Scalar::zero();
260 let (claim_post_phase1, rx) =
261 self
262 .sc_proof_phase1
263 .verify(claim_phase1, num_rounds_x, 3, transcript)?;
264
265 // perform the intermediate sum-check test with claimed Az, Bz, and Cz
266 let (Az_claim, Bz_claim, Cz_claim, prod_Az_Bz_claims) = &self.claims_phase2;
267
268 let taus_bound_rx: Scalar = (0..rx.len())
269 .map(|i| rx[i] * tau[i] + (Scalar::one() - rx[i]) * (Scalar::one() - tau[i]))
270 .product();
271
272 let expected_claim_post_phase1 = (*prod_Az_Bz_claims - *Cz_claim) * (taus_bound_rx);
273
274 assert_eq!(claim_post_phase1, expected_claim_post_phase1);
275
276 // derive three public challenges and then derive a joint claim
277 let r_A = transcript.challenge_scalar(b"challenege_Az");
278 let r_B = transcript.challenge_scalar(b"challenege_Bz");
279 let r_C = transcript.challenge_scalar(b"challenege_Cz");
280
281 let claim_phase2 = r_A * Az_claim + r_B * Bz_claim + r_C * Cz_claim;
282
283 // verify the joint claim with a sum-check protocol
284 let (claim_post_phase2, ry) =
285 self
286 .sc_proof_phase2
287 .verify(claim_phase2, num_rounds_y, 2, transcript)?;
288
289 let poly_input_eval = {
290 // constant term
291 let mut input_as_sparse_poly_entries = vec![SparsePolyEntry::new(0, Scalar::one())];
292 //remaining inputs
293 input_as_sparse_poly_entries.extend(
294 (0..input.len())
295 .map(|i| SparsePolyEntry::new(i + 1, input[i]))
296 .collect::<Vec<SparsePolyEntry>>(),
297 );
298 SparsePolynomial::new(n.log_2() as usize, input_as_sparse_poly_entries).evaluate(&ry[1..])
299 };
300
301 let eval_Z_at_ry = (Scalar::one() - ry[0]) * self.eval_vars_at_ry + ry[0] * poly_input_eval;
302
303 // perform the final check in the second sum-check protocol
304 let (eval_A_r, eval_B_r, eval_C_r) = evals;
305 let scalar = r_A * eval_A_r + r_B * eval_B_r + r_C * eval_C_r;
306 let expected_claim_post_phase2 = eval_Z_at_ry * scalar;
307
308 assert_eq!(expected_claim_post_phase2, claim_post_phase2);
309
310 Ok((rx, ry))
311 }
312}
313
314#[cfg(test)]
315mod tests {
316 use super::*;
317 use ark_std::UniformRand;
318 use test::Bencher;
319
320 fn produce_tiny_r1cs() -> (R1CSInstance, Vec<Scalar>, Vec<Scalar>) {
321 // three constraints over five variables Z1, Z2, Z3, Z4, and Z5
322 // rounded to the nearest power of two
323 let num_cons = 128;
324 let num_vars = 256;
325 let num_inputs = 2;
326
327 // encode the above constraints into three matrices
328 let mut A: Vec<(usize, usize, Scalar)> = Vec::new();
329 let mut B: Vec<(usize, usize, Scalar)> = Vec::new();
330 let mut C: Vec<(usize, usize, Scalar)> = Vec::new();
331
332 let one = Scalar::one();
333 // constraint 0 entries
334 // (Z1 + Z2) * I0 - Z3 = 0;
335 A.push((0, 0, one));
336 A.push((0, 1, one));
337 B.push((0, num_vars + 1, one));
338 C.push((0, 2, one));
339
340 // constraint 1 entries
341 // (Z1 + I1) * (Z3) - Z4 = 0
342 A.push((1, 0, one));
343 A.push((1, num_vars + 2, one));
344 B.push((1, 2, one));
345 C.push((1, 3, one));
346 // constraint 3 entries
347 // Z5 * 1 - 0 = 0
348 A.push((2, 4, one));
349 B.push((2, num_vars, one));
350
351 let inst = R1CSInstance::new(num_cons, num_vars, num_inputs, &A, &B, &C);
352
353 // compute a satisfying assignment
354 let mut rng = ark_std::rand::thread_rng();
355 let i0 = Scalar::rand(&mut rng);
356 let i1 = Scalar::rand(&mut rng);
357 let z1 = Scalar::rand(&mut rng);
358 let z2 = Scalar::rand(&mut rng);
359 let z3 = (z1 + z2) * i0; // constraint 1: (Z1 + Z2) * I0 - Z3 = 0;
360 let z4 = (z1 + i1) * z3; // constraint 2: (Z1 + I1) * (Z3) - Z4 = 0
361 let z5 = Scalar::zero(); //constraint 3
362
363 let mut vars = vec![Scalar::zero(); num_vars];
364 vars[0] = z1;
365 vars[1] = z2;
366 vars[2] = z3;
367 vars[3] = z4;
368 vars[4] = z5;
369
370 let mut input = vec![Scalar::zero(); num_inputs];
371 input[0] = i0;
372 input[1] = i1;
373
374 (inst, vars, input)
375 }
376
377 #[test]
378 fn test_tiny_r1cs() {
379 let (inst, vars, input) = tests::produce_tiny_r1cs();
380 let is_sat = inst.is_sat(&vars, &input);
381 assert!(is_sat);
382 }
383
384 #[test]
385 fn test_synthetic_r1cs() {
386 let (inst, vars, input) = R1CSInstance::produce_synthetic_r1cs(1024, 1024, 10);
387 let is_sat = inst.is_sat(&vars, &input);
388 assert!(is_sat);
389 }
390
391 #[test]
392 pub fn check_r1cs_proof() {
393 let num_vars = 1024;
394 let num_cons = num_vars;
395 let num_inputs = 10;
396 let (inst, vars, input) = R1CSInstance::produce_synthetic_r1cs(num_cons, num_vars, num_inputs);
397
398 let gens = R1CSGens::new(b"test-m", num_cons, num_vars);
399
400 let mut random_tape = RandomTape::new(b"proof");
401 let mut prover_transcript = Transcript::new(b"example");
402 let (proof, rx, ry) = R1CSProof::prove(
403 &inst,
404 vars,
405 &input,
406 &gens,
407 &mut prover_transcript,
408 &mut random_tape,
409 );
410
411 let inst_evals = inst.evaluate(&rx, &ry);
412
413 let mut verifier_transcript = Transcript::new(b"example");
414 assert!(proof
415 .verify(
416 inst.get_num_vars(),
417 inst.get_num_cons(),
418 &input,
419 &inst_evals,
420 &mut verifier_transcript,
421 &gens,
422 )
423 .is_ok());
424 }
425
426 #[bench]
427 fn bench_r1cs_proof(b: &mut Bencher) {
428 b.iter(|| check_r1cs_proof());
429 }
430}