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