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