testudo/src/constraints.rs
src/constraints.rsRaw
1use std::{borrow::Borrow, vec};
2
3use super::scalar::Scalar;
4use crate::{
5 group::Fq,
6 math::Math,
7 sparse_mlpoly::{SparsePolyEntry, SparsePolynomial},
8 unipoly::UniPoly,
9};
10use ark_bls12_377::{constraints::PairingVar as IV, Bls12_377 as I, Fr};
11use ark_crypto_primitives::{
12 snark::BooleanInputVar, CircuitSpecificSetupSNARK, SNARKGadget, SNARK,
13};
14
15use ark_ff::{BitIteratorLE, PrimeField, Zero};
16use ark_groth16::{
17 constraints::{Groth16VerifierGadget, PreparedVerifyingKeyVar, ProofVar},
18 Groth16, PreparedVerifyingKey, Proof as GrothProof,
19};
20
21use ark_poly_commit::multilinear_pc::{
22 data_structures::{Commitment, Proof, VerifierKey},
23 MultilinearPC,
24};
25use ark_r1cs_std::{
26 alloc::{AllocVar, AllocationMode},
27 fields::fp::FpVar,
28 prelude::{Boolean, EqGadget, FieldVar},
29 R1CSVar,
30};
31use ark_relations::r1cs::{ConstraintSynthesizer, ConstraintSystemRef, Namespace, SynthesisError};
32use ark_sponge::{
33 constraints::CryptographicSpongeVar,
34 poseidon::{constraints::PoseidonSpongeVar, PoseidonParameters},
35};
36use rand::{CryptoRng, Rng};
37
38pub struct PoseidonTranscripVar {
39 pub cs: ConstraintSystemRef<Fr>,
40 pub sponge: PoseidonSpongeVar<Fr>,
41 pub params: PoseidonParameters<Fr>,
42}
43
44impl PoseidonTranscripVar {
45 fn new(
46 cs: ConstraintSystemRef<Fr>,
47 params: &PoseidonParameters<Fr>,
48 challenge: Option<Fr>,
49 ) -> Self {
50 let mut sponge = PoseidonSpongeVar::new(cs.clone(), params);
51
52 if let Some(c) = challenge {
53 let c_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(c)).unwrap();
54 sponge.absorb(&c_var).unwrap();
55 }
56
57 Self {
58 cs,
59 sponge,
60 params: params.clone(),
61 }
62 }
63
64 fn append(&mut self, input: &FpVar<Fr>) -> Result<(), SynthesisError> {
65 self.sponge.absorb(&input)
66 }
67
68 fn append_vector(&mut self, input_vec: &[FpVar<Fr>]) -> Result<(), SynthesisError> {
69 for input in input_vec.iter() {
70 self.append(input)?;
71 }
72 Ok(())
73 }
74
75 fn challenge(&mut self) -> Result<FpVar<Fr>, SynthesisError> {
76 let c_var = self.sponge.squeeze_field_elements(1).unwrap().remove(0);
77
78 Ok(c_var)
79 }
80
81 fn challenge_vector(&mut self, len: usize) -> Result<Vec<FpVar<Fr>>, SynthesisError> {
82 let c_vars = self.sponge.squeeze_field_elements(len).unwrap();
83
84 Ok(c_vars)
85 }
86}
87
88#[derive(Clone)]
89pub struct UniPolyVar {
90 pub coeffs: Vec<FpVar<Fr>>,
91}
92
93impl AllocVar<UniPoly, Fr> for UniPolyVar {
94 fn new_variable<T: Borrow<UniPoly>>(
95 cs: impl Into<Namespace<Fr>>,
96 f: impl FnOnce() -> Result<T, SynthesisError>,
97 mode: AllocationMode,
98 ) -> Result<Self, SynthesisError> {
99 f().and_then(|c| {
100 let cs = cs.into();
101 let cp: &UniPoly = c.borrow();
102 let mut coeffs_var = Vec::new();
103 for coeff in cp.coeffs.iter() {
104 let coeff_var = FpVar::<Fr>::new_variable(cs.clone(), || Ok(coeff), mode)?;
105 coeffs_var.push(coeff_var);
106 }
107 Ok(Self { coeffs: coeffs_var })
108 })
109 }
110}
111
112impl UniPolyVar {
113 pub fn eval_at_zero(&self) -> FpVar<Fr> {
114 self.coeffs[0].clone()
115 }
116
117 pub fn eval_at_one(&self) -> FpVar<Fr> {
118 let mut res = self.coeffs[0].clone();
119 for i in 1..self.coeffs.len() {
120 res = &res + &self.coeffs[i];
121 }
122 res
123 }
124
125 // mul without reduce
126 pub fn evaluate(&self, r: &FpVar<Fr>) -> FpVar<Fr> {
127 let mut eval = self.coeffs[0].clone();
128 let mut power = r.clone();
129
130 for i in 1..self.coeffs.len() {
131 eval += &power * &self.coeffs[i];
132 power *= r;
133 }
134 eval
135 }
136}
137
138#[derive(Clone)]
139pub struct SumcheckVerificationCircuit {
140 pub polys: Vec<UniPoly>,
141}
142
143impl SumcheckVerificationCircuit {
144 fn verifiy_sumcheck(
145 &self,
146 poly_vars: &[UniPolyVar],
147 claim_var: &FpVar<Fr>,
148 transcript_var: &mut PoseidonTranscripVar,
149 ) -> Result<(FpVar<Fr>, Vec<FpVar<Fr>>), SynthesisError> {
150 let mut e_var = claim_var.clone();
151 let mut r_vars: Vec<FpVar<Fr>> = Vec::new();
152
153 for (poly_var, _poly) in poly_vars.iter().zip(self.polys.iter()) {
154 let res = poly_var.eval_at_one() + poly_var.eval_at_zero();
155 res.enforce_equal(&e_var)?;
156 transcript_var.append_vector(&poly_var.coeffs)?;
157 let r_i_var = transcript_var.challenge()?;
158 r_vars.push(r_i_var.clone());
159 e_var = poly_var.evaluate(&r_i_var.clone());
160 }
161
162 Ok((e_var, r_vars))
163 }
164}
165
166#[derive(Clone)]
167pub struct SparsePolyEntryVar {
168 idx: usize,
169 val_var: FpVar<Fr>,
170}
171
172impl AllocVar<SparsePolyEntry, Fr> for SparsePolyEntryVar {
173 fn new_variable<T: Borrow<SparsePolyEntry>>(
174 cs: impl Into<Namespace<Fr>>,
175 f: impl FnOnce() -> Result<T, SynthesisError>,
176 _mode: AllocationMode,
177 ) -> Result<Self, SynthesisError> {
178 f().and_then(|s| {
179 let cs = cs.into();
180 let spe: &SparsePolyEntry = s.borrow();
181 let val_var = FpVar::<Fr>::new_witness(cs, || Ok(spe.val))?;
182 Ok(Self {
183 idx: spe.idx,
184 val_var,
185 })
186 })
187 }
188}
189
190#[derive(Clone)]
191pub struct SparsePolynomialVar {
192 num_vars: usize,
193 Z_var: Vec<SparsePolyEntryVar>,
194}
195
196impl AllocVar<SparsePolynomial, Fr> for SparsePolynomialVar {
197 fn new_variable<T: Borrow<SparsePolynomial>>(
198 cs: impl Into<Namespace<Fr>>,
199 f: impl FnOnce() -> Result<T, SynthesisError>,
200 mode: AllocationMode,
201 ) -> Result<Self, SynthesisError> {
202 f().and_then(|s| {
203 let cs = cs.into();
204 let sp: &SparsePolynomial = s.borrow();
205 let mut Z_var = Vec::new();
206 for spe in sp.Z.iter() {
207 let spe_var = SparsePolyEntryVar::new_variable(cs.clone(), || Ok(spe), mode)?;
208 Z_var.push(spe_var);
209 }
210 Ok(Self {
211 num_vars: sp.num_vars,
212 Z_var,
213 })
214 })
215 }
216}
217
218impl SparsePolynomialVar {
219 fn compute_chi(a: &[bool], r_vars: &[FpVar<Fr>]) -> FpVar<Fr> {
220 let mut chi_i_var = FpVar::<Fr>::one();
221 let one = FpVar::<Fr>::one();
222 for (i, r_var) in r_vars.iter().enumerate() {
223 if a[i] {
224 chi_i_var *= r_var;
225 } else {
226 chi_i_var *= &one - r_var;
227 }
228 }
229 chi_i_var
230 }
231
232 pub fn evaluate(&self, r_var: &[FpVar<Fr>]) -> FpVar<Fr> {
233 let mut sum = FpVar::<Fr>::zero();
234 for spe_var in self.Z_var.iter() {
235 // potential problem
236 let bits = &spe_var.idx.get_bits(r_var.len());
237 sum += SparsePolynomialVar::compute_chi(bits, r_var) * &spe_var.val_var;
238 }
239 sum
240 }
241}
242
243#[derive(Clone)]
244pub struct R1CSVerificationCircuit {
245 pub num_vars: usize,
246 pub num_cons: usize,
247 pub input: Vec<Fr>,
248 pub input_as_sparse_poly: SparsePolynomial,
249 pub evals: (Fr, Fr, Fr),
250 pub params: PoseidonParameters<Fr>,
251 pub prev_challenge: Fr,
252 pub claims_phase2: (Scalar, Scalar, Scalar, Scalar),
253 pub eval_vars_at_ry: Fr,
254 pub sc_phase1: SumcheckVerificationCircuit,
255 pub sc_phase2: SumcheckVerificationCircuit,
256 // The point on which the polynomial was evaluated by the prover.
257 pub claimed_ry: Vec<Scalar>,
258 pub claimed_transcript_sat_state: Scalar,
259}
260
261impl R1CSVerificationCircuit {
262 fn new(config: &VerifierConfig) -> Self {
263 Self {
264 num_vars: config.num_vars,
265 num_cons: config.num_cons,
266 input: config.input.clone(),
267 input_as_sparse_poly: config.input_as_sparse_poly.clone(),
268 evals: config.evals,
269 params: config.params.clone(),
270 prev_challenge: config.prev_challenge,
271 claims_phase2: config.claims_phase2,
272 eval_vars_at_ry: config.eval_vars_at_ry,
273 sc_phase1: SumcheckVerificationCircuit {
274 polys: config.polys_sc1.clone(),
275 },
276 sc_phase2: SumcheckVerificationCircuit {
277 polys: config.polys_sc2.clone(),
278 },
279 claimed_ry: config.ry.clone(),
280 claimed_transcript_sat_state: config.transcript_sat_state,
281 }
282 }
283}
284
285impl ConstraintSynthesizer<Fr> for R1CSVerificationCircuit {
286 fn generate_constraints(self, cs: ConstraintSystemRef<Fr>) -> ark_relations::r1cs::Result<()> {
287 let mut transcript_var =
288 PoseidonTranscripVar::new(cs.clone(), &self.params, Some(self.prev_challenge));
289
290 let poly_sc1_vars = self
291 .sc_phase1
292 .polys
293 .iter()
294 .map(|p| UniPolyVar::new_variable(cs.clone(), || Ok(p), AllocationMode::Witness).unwrap())
295 .collect::<Vec<UniPolyVar>>();
296
297 let poly_sc2_vars = self
298 .sc_phase2
299 .polys
300 .iter()
301 .map(|p| UniPolyVar::new_variable(cs.clone(), || Ok(p), AllocationMode::Witness).unwrap())
302 .collect::<Vec<UniPolyVar>>();
303
304 let input_vars = self
305 .input
306 .iter()
307 .map(|i| FpVar::<Fr>::new_variable(cs.clone(), || Ok(i), AllocationMode::Witness).unwrap())
308 .collect::<Vec<FpVar<Fr>>>();
309
310 let claimed_ry_vars = self
311 .claimed_ry
312 .iter()
313 .map(|r| FpVar::<Fr>::new_variable(cs.clone(), || Ok(r), AllocationMode::Input).unwrap())
314 .collect::<Vec<FpVar<Fr>>>();
315
316 transcript_var.append_vector(&input_vars)?;
317
318 let num_rounds_x = self.num_cons.log_2();
319 let _num_rounds_y = (2 * self.num_vars).log_2();
320
321 let tau_vars = transcript_var.challenge_vector(num_rounds_x)?;
322
323 let claim_phase1_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(Fr::zero()))?;
324
325 let (claim_post_phase1_var, rx_var) =
326 self
327 .sc_phase1
328 .verifiy_sumcheck(&poly_sc1_vars, &claim_phase1_var, &mut transcript_var)?;
329
330 let (Az_claim, Bz_claim, Cz_claim, prod_Az_Bz_claims) = &self.claims_phase2;
331
332 let Az_claim_var = FpVar::<Fr>::new_input(cs.clone(), || Ok(Az_claim))?;
333 let Bz_claim_var = FpVar::<Fr>::new_input(cs.clone(), || Ok(Bz_claim))?;
334 let Cz_claim_var = FpVar::<Fr>::new_input(cs.clone(), || Ok(Cz_claim))?;
335 let prod_Az_Bz_claim_var = FpVar::<Fr>::new_input(cs.clone(), || Ok(prod_Az_Bz_claims))?;
336 let one = FpVar::<Fr>::one();
337 let prod_vars: Vec<FpVar<Fr>> = (0..rx_var.len())
338 .map(|i| (&rx_var[i] * &tau_vars[i]) + (&one - &rx_var[i]) * (&one - &tau_vars[i]))
339 .collect();
340 let mut taus_bound_rx_var = FpVar::<Fr>::one();
341
342 for p_var in prod_vars.iter() {
343 taus_bound_rx_var *= p_var;
344 }
345
346 let expected_claim_post_phase1_var =
347 (&prod_Az_Bz_claim_var - &Cz_claim_var) * &taus_bound_rx_var;
348
349 claim_post_phase1_var.enforce_equal(&expected_claim_post_phase1_var)?;
350
351 let r_A_var = transcript_var.challenge()?;
352 let r_B_var = transcript_var.challenge()?;
353 let r_C_var = transcript_var.challenge()?;
354
355 let claim_phase2_var =
356 &r_A_var * &Az_claim_var + &r_B_var * &Bz_claim_var + &r_C_var * &Cz_claim_var;
357
358 let (claim_post_phase2_var, ry_var) =
359 self
360 .sc_phase2
361 .verifiy_sumcheck(&poly_sc2_vars, &claim_phase2_var, &mut transcript_var)?;
362
363 // Because the verifier checks the commitment opening on point ry outside
364 // the circuit, the prover needs to send ry to the verifier (making the
365 // proof size O(log n)). As this point is normally obtained by the verifier
366 // from the second round of sumcheck, the circuit needs to ensure the
367 // claimed point, coming from the prover, is actually the point derived
368 // inside the circuit. These additional checks will be removed
369 // when the commitment verification is done inside the circuit.
370 for (i, r) in claimed_ry_vars.iter().enumerate() {
371 ry_var[i].enforce_equal(r)?;
372 }
373
374 let input_as_sparse_poly_var = SparsePolynomialVar::new_variable(
375 cs.clone(),
376 || Ok(&self.input_as_sparse_poly),
377 AllocationMode::Witness,
378 )?;
379
380 let poly_input_eval_var = input_as_sparse_poly_var.evaluate(&ry_var[1..]);
381
382 let eval_vars_at_ry_var = FpVar::<Fr>::new_input(cs.clone(), || Ok(&self.eval_vars_at_ry))?;
383
384 let eval_Z_at_ry_var =
385 (FpVar::<Fr>::one() - &ry_var[0]) * &eval_vars_at_ry_var + &ry_var[0] * &poly_input_eval_var;
386
387 let (eval_A_r, eval_B_r, eval_C_r) = self.evals;
388
389 let eval_A_r_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(eval_A_r))?;
390 let eval_B_r_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(eval_B_r))?;
391 let eval_C_r_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(eval_C_r))?;
392
393 let scalar_var = &r_A_var * &eval_A_r_var + &r_B_var * &eval_B_r_var + &r_C_var * &eval_C_r_var;
394
395 let expected_claim_post_phase2_var = eval_Z_at_ry_var * scalar_var;
396 claim_post_phase2_var.enforce_equal(&expected_claim_post_phase2_var)?;
397
398 let expected_transcript_state_var = transcript_var.challenge()?;
399 let claimed_transcript_state_var =
400 FpVar::<Fr>::new_input(cs, || Ok(self.claimed_transcript_sat_state))?;
401
402 // Ensure that the prover and verifier transcipt views are consistent at
403 // the end of the satisfiability proof.
404 expected_transcript_state_var.enforce_equal(&claimed_transcript_state_var)?;
405
406 Ok(())
407 }
408}
409
410#[derive(Clone)]
411pub struct VerifierConfig {
412 pub num_vars: usize,
413 pub num_cons: usize,
414 pub input: Vec<Fr>,
415 pub input_as_sparse_poly: SparsePolynomial,
416 pub evals: (Fr, Fr, Fr),
417 pub params: PoseidonParameters<Fr>,
418 pub prev_challenge: Fr,
419 pub claims_phase2: (Fr, Fr, Fr, Fr),
420 pub eval_vars_at_ry: Fr,
421 pub polys_sc1: Vec<UniPoly>,
422 pub polys_sc2: Vec<UniPoly>,
423 pub ry: Vec<Scalar>,
424 pub transcript_sat_state: Scalar,
425}
426#[derive(Clone)]
427pub struct VerifierCircuit {
428 pub inner_circuit: R1CSVerificationCircuit,
429 pub inner_proof: GrothProof<I>,
430 pub inner_vk: PreparedVerifyingKey<I>,
431 pub eval_vars_at_ry: Fr,
432 pub claims_phase2: (Fr, Fr, Fr, Fr),
433 pub ry: Vec<Fr>,
434 pub transcript_sat_state: Scalar,
435}
436
437impl VerifierCircuit {
438 pub fn new<R: Rng + CryptoRng>(
439 config: &VerifierConfig,
440 mut rng: &mut R,
441 ) -> Result<Self, SynthesisError> {
442 let inner_circuit = R1CSVerificationCircuit::new(config);
443 let (pk, vk) = Groth16::<I>::setup(inner_circuit.clone(), &mut rng).unwrap();
444 let proof = Groth16::<I>::prove(&pk, inner_circuit.clone(), &mut rng)?;
445 let pvk = Groth16::<I>::process_vk(&vk).unwrap();
446 Ok(Self {
447 inner_circuit,
448 inner_proof: proof,
449 inner_vk: pvk,
450 eval_vars_at_ry: config.eval_vars_at_ry,
451 claims_phase2: config.claims_phase2,
452 ry: config.ry.clone(),
453 transcript_sat_state: config.transcript_sat_state,
454 })
455 }
456}
457
458impl ConstraintSynthesizer<Fq> for VerifierCircuit {
459 fn generate_constraints(self, cs: ConstraintSystemRef<Fq>) -> ark_relations::r1cs::Result<()> {
460 let proof_var = ProofVar::<I, IV>::new_witness(cs.clone(), || Ok(self.inner_proof.clone()))?;
461 let (v_A, v_B, v_C, v_AB) = self.claims_phase2;
462 let mut pubs = vec![];
463 pubs.extend(self.ry);
464 pubs.extend(vec![v_A, v_B, v_C, v_AB]);
465 pubs.extend(vec![self.eval_vars_at_ry, self.transcript_sat_state]);
466
467 let bits = pubs
468 .iter()
469 .map(|c| {
470 let bits: Vec<bool> = BitIteratorLE::new(c.into_repr().as_ref().to_vec()).collect();
471 Vec::new_witness(cs.clone(), || Ok(bits))
472 })
473 .collect::<Result<Vec<_>, _>>()?;
474 let input_var = BooleanInputVar::<Fr, Fq>::new(bits);
475
476 let vk_var = PreparedVerifyingKeyVar::new_witness(cs, || Ok(self.inner_vk.clone()))?;
477 Groth16VerifierGadget::verify_with_processed_vk(&vk_var, &input_var, &proof_var)?
478 .enforce_equal(&Boolean::constant(true))?;
479 Ok(())
480 }
481}