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