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