arnaucube
arnaucube/ark-r1cs-stdPublic Self-hosted repository
ark-r1cs-std/crypto-primitives/src/nizk/gm17/constraints.rs
crypto-primitives/src/nizk/gm17/constraints.rsRaw
  1use crate::{
  2    nizk::{gm17::Gm17, NIZKVerifierGadget},
  3    Vec,
  4};
  5use algebra_core::{AffineCurve, PairingEngine, ToConstraintField};
  6use r1cs_core::{ConstraintSynthesizer, Namespace, SynthesisError};
  7use r1cs_std::prelude::*;
  8
  9use core::{borrow::Borrow, marker::PhantomData};
 10use gm17::{PreparedVerifyingKey, Proof, VerifyingKey};
 11
 12#[derive(Derivative)]
 13#[derivative(Clone(bound = "P::G1Var: Clone, P::G2Var: Clone"))]
 14pub struct ProofVar<E: PairingEngine, P: PairingVar<E>> {
 15    pub a: P::G1Var,
 16    pub b: P::G2Var,
 17    pub c: P::G1Var,
 18}
 19
 20#[derive(Derivative)]
 21#[derivative(
 22    Clone(bound = "P::G1Var: Clone, P::GTVar: Clone, P::G1PreparedVar: Clone, \
 23    P::G2PreparedVar: Clone, ")
 24)]
 25pub struct VerifyingKeyVar<E: PairingEngine, P: PairingVar<E>> {
 26    pub h_g2: P::G2Var,
 27    pub g_alpha_g1: P::G1Var,
 28    pub h_beta_g2: P::G2Var,
 29    pub g_gamma_g1: P::G1Var,
 30    pub h_gamma_g2: P::G2Var,
 31    pub query: Vec<P::G1Var>,
 32}
 33
 34impl<E: PairingEngine, P: PairingVar<E>> VerifyingKeyVar<E, P> {
 35    pub fn prepare(&self) -> Result<PreparedVerifyingKeyVar<E, P>, SynthesisError> {
 36        let g_alpha_pc = P::prepare_g1(&self.g_alpha_g1)?;
 37        let h_beta_pc = P::prepare_g2(&self.h_beta_g2)?;
 38        let g_gamma_pc = P::prepare_g1(&self.g_gamma_g1)?;
 39        let h_gamma_pc = P::prepare_g2(&self.h_gamma_g2)?;
 40        let h_pc = P::prepare_g2(&self.h_g2)?;
 41        Ok(PreparedVerifyingKeyVar {
 42            g_alpha: self.g_alpha_g1.clone(),
 43            h_beta: self.h_beta_g2.clone(),
 44            g_alpha_pc,
 45            h_beta_pc,
 46            g_gamma_pc,
 47            h_gamma_pc,
 48            h_pc,
 49            query: self.query.clone(),
 50        })
 51    }
 52}
 53
 54#[derive(Derivative)]
 55#[derivative(
 56    Clone(bound = "P::G1Var: Clone, P::GTVar: Clone, P::G1PreparedVar: Clone, \
 57    P::G2PreparedVar: Clone, ")
 58)]
 59pub struct PreparedVerifyingKeyVar<E: PairingEngine, P: PairingVar<E>> {
 60    pub g_alpha: P::G1Var,
 61    pub h_beta: P::G2Var,
 62    pub g_alpha_pc: P::G1PreparedVar,
 63    pub h_beta_pc: P::G2PreparedVar,
 64    pub g_gamma_pc: P::G1PreparedVar,
 65    pub h_gamma_pc: P::G2PreparedVar,
 66    pub h_pc: P::G2PreparedVar,
 67    pub query: Vec<P::G1Var>,
 68}
 69
 70pub struct Gm17VerifierGadget<E, P>
 71where
 72    E: PairingEngine,
 73    P: PairingVar<E>,
 74{
 75    _pairing_engine: PhantomData<E>,
 76    _pairing_gadget: PhantomData<P>,
 77}
 78
 79impl<E, P, C, V> NIZKVerifierGadget<Gm17<E, C, V>, E::Fq> for Gm17VerifierGadget<E, P>
 80where
 81    E: PairingEngine,
 82    C: ConstraintSynthesizer<E::Fr>,
 83    V: ToConstraintField<E::Fr>,
 84    P: PairingVar<E>,
 85{
 86    type PreparedVerificationKeyVar = PreparedVerifyingKeyVar<E, P>;
 87    type VerificationKeyVar = VerifyingKeyVar<E, P>;
 88    type ProofVar = ProofVar<E, P>;
 89
 90    /// Allocates `N::Proof` in `cs` without performing
 91    /// subgroup checks.
 92    fn new_proof_unchecked<T: Borrow<Proof<E>>>(
 93        cs: impl Into<Namespace<E::Fq>>,
 94        f: impl FnOnce() -> Result<T, SynthesisError>,
 95        mode: AllocationMode,
 96    ) -> Result<Self::ProofVar, SynthesisError> {
 97        let ns = cs.into();
 98        let cs = ns.cs();
 99        f().and_then(|proof| {
100            let proof = proof.borrow();
101            let a = CurveVar::new_variable_omit_prime_order_check(
102                cs.ns("Proof.a"),
103                || Ok(proof.a.into_projective()),
104                mode,
105            )?;
106            let b = CurveVar::new_variable_omit_prime_order_check(
107                cs.ns("Proof.b"),
108                || Ok(proof.b.into_projective()),
109                mode,
110            )?;
111            let c = CurveVar::new_variable_omit_prime_order_check(
112                cs.ns("Proof.c"),
113                || Ok(proof.c.into_projective()),
114                mode,
115            )?;
116            Ok(ProofVar { a, b, c })
117        })
118    }
119
120    /// Allocates `N::Proof` in `cs` without performing
121    /// subgroup checks.
122    fn new_verification_key_unchecked<T: Borrow<VerifyingKey<E>>>(
123        cs: impl Into<Namespace<E::Fq>>,
124        f: impl FnOnce() -> Result<T, SynthesisError>,
125        mode: AllocationMode,
126    ) -> Result<Self::VerificationKeyVar, SynthesisError> {
127        let ns = cs.into();
128        let cs = ns.cs();
129        f().and_then(|vk| {
130            let vk = vk.borrow();
131            let g_alpha_g1 = P::G1Var::new_variable_omit_prime_order_check(
132                cs.ns("g_alpha"),
133                || Ok(vk.g_alpha_g1.into_projective()),
134                mode,
135            )?;
136            let h_g2 = P::G2Var::new_variable_omit_prime_order_check(
137                cs.ns("h"),
138                || Ok(vk.h_g2.into_projective()),
139                mode,
140            )?;
141            let h_beta_g2 = P::G2Var::new_variable_omit_prime_order_check(
142                cs.ns("h_beta"),
143                || Ok(vk.h_beta_g2.into_projective()),
144                mode,
145            )?;
146            let g_gamma_g1 = P::G1Var::new_variable_omit_prime_order_check(
147                cs.ns("g_gamma"),
148                || Ok(vk.g_gamma_g1.into_projective()),
149                mode,
150            )?;
151            let h_gamma_g2 = P::G2Var::new_variable_omit_prime_order_check(
152                cs.ns("h_gamma"),
153                || Ok(vk.h_gamma_g2.into_projective()),
154                mode,
155            )?;
156
157            let query = vk
158                .query
159                .iter()
160                .map(|g| {
161                    P::G1Var::new_variable_omit_prime_order_check(
162                        cs.ns("g"),
163                        || Ok(g.into_projective()),
164                        mode,
165                    )
166                })
167                .collect::<Result<Vec<_>, _>>()?;
168            Ok(VerifyingKeyVar {
169                g_alpha_g1,
170                h_g2,
171                h_beta_g2,
172                g_gamma_g1,
173                h_gamma_g2,
174                query,
175            })
176        })
177    }
178
179    fn verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
180        vk: &Self::VerificationKeyVar,
181        input: impl IntoIterator<Item = &'a T>,
182        proof: &Self::ProofVar,
183    ) -> Result<Boolean<E::Fq>, SynthesisError> {
184        let pvk = vk.prepare()?;
185        <Self as NIZKVerifierGadget<Gm17<E, C, V>, E::Fq>>::verify_prepared(&pvk, input, proof)
186    }
187
188    fn verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
189        pvk: &Self::PreparedVerificationKeyVar,
190        input: impl IntoIterator<Item = &'a T>,
191        proof: &Self::ProofVar,
192    ) -> Result<Boolean<E::Fq>, SynthesisError> {
193        let pvk = pvk.clone();
194        // e(A*G^{alpha}, B*H^{beta}) = e(G^{alpha}, H^{beta}) * e(G^{psi}, H^{gamma}) *
195        // e(C, H) where psi = \sum_{i=0}^l input_i pvk.query[i]
196        let g_psi = {
197            let mut g_psi = pvk.query[0].clone();
198            let mut input_len = 1;
199            let mut input = input.into_iter();
200            for (input, b) in input.by_ref().zip(pvk.query.iter().skip(1)) {
201                let input_bits = input.to_bits_le()?;
202                g_psi += b.scalar_mul_le(input_bits.iter())?;
203                input_len += 1;
204            }
205            // Check that the input and the query in the verification are of the
206            // same length.
207            assert!(input_len == pvk.query.len() && input.next().is_none());
208            g_psi
209        };
210
211        let mut test1_a_g_alpha = proof.a.clone();
212        test1_a_g_alpha += pvk.g_alpha.clone();
213        let mut test1_b_h_beta = proof.b.clone();
214        test1_b_h_beta += pvk.h_beta.clone();
215
216        let test1_exp = {
217            test1_a_g_alpha = test1_a_g_alpha.negate()?;
218            let test1_a_g_alpha_prep = P::prepare_g1(&test1_a_g_alpha)?;
219            let test1_b_h_beta_prep = P::prepare_g2(&test1_b_h_beta)?;
220
221            let g_psi_prep = P::prepare_g1(&g_psi)?;
222
223            let c_prep = P::prepare_g1(&proof.c)?;
224
225            P::miller_loop(
226                &[
227                    test1_a_g_alpha_prep,
228                    g_psi_prep,
229                    c_prep,
230                    pvk.g_alpha_pc.clone(),
231                ],
232                &[
233                    test1_b_h_beta_prep,
234                    pvk.h_gamma_pc.clone(),
235                    pvk.h_pc.clone(),
236                    pvk.h_beta_pc.clone(),
237                ],
238            )?
239        };
240
241        let test1 = P::final_exponentiation(&test1_exp).unwrap();
242
243        // e(A, H^{gamma}) = e(G^{gamma}, B)
244        let test2_exp = {
245            let a_prep = P::prepare_g1(&proof.a)?;
246            // pvk.h_gamma_pc
247            //&pvk.g_gamma_pc
248            let proof_b = proof.b.negate()?;
249            let b_prep = P::prepare_g2(&proof_b)?;
250            P::miller_loop(&[a_prep, pvk.g_gamma_pc.clone()], &[pvk.h_gamma_pc, b_prep])?
251        };
252        let test2 = P::final_exponentiation(&test2_exp)?;
253
254        let one = P::GTVar::one();
255        test1.is_eq(&one)?.and(&test2.is_eq(&one)?)
256    }
257}
258
259impl<E, P> AllocVar<PreparedVerifyingKey<E>, E::Fq> for PreparedVerifyingKeyVar<E, P>
260where
261    E: PairingEngine,
262    P: PairingVar<E>,
263    P::G1PreparedVar: AllocVar<E::G1Prepared, E::Fq>,
264    P::G2PreparedVar: AllocVar<E::G2Prepared, E::Fq>,
265{
266    fn new_variable<T: Borrow<PreparedVerifyingKey<E>>>(
267        cs: impl Into<Namespace<E::Fq>>,
268        f: impl FnOnce() -> Result<T, SynthesisError>,
269        mode: AllocationMode,
270    ) -> Result<Self, SynthesisError> {
271        let ns = cs.into();
272        let cs = ns.cs();
273
274        f().and_then(|pvk| {
275            let pvk = pvk.borrow();
276            let g_alpha = P::G1Var::new_variable(cs.ns("g_alpha"), || Ok(pvk.g_alpha), mode)?;
277            let h_beta = P::G2Var::new_variable(cs.ns("h_beta"), || Ok(pvk.h_beta), mode)?;
278            let g_alpha_pc = P::G1PreparedVar::new_variable(
279                cs.ns("g_alpha_pc"),
280                || Ok(pvk.g_alpha.into()),
281                mode,
282            )?;
283            let h_beta_pc =
284                P::G2PreparedVar::new_variable(cs.ns("h_beta_pc"), || Ok(pvk.h_beta.into()), mode)?;
285            let g_gamma_pc =
286                P::G1PreparedVar::new_variable(cs.ns("g_gamma_pc"), || Ok(&pvk.g_gamma_pc), mode)?;
287            let h_gamma_pc =
288                P::G2PreparedVar::new_variable(cs.ns("h_gamma_pc"), || Ok(&pvk.h_gamma_pc), mode)?;
289            let h_pc = P::G2PreparedVar::new_variable(cs.ns("h_pc"), || Ok(&pvk.h_pc), mode)?;
290            let query = Vec::new_variable(cs.ns("query"), || Ok(pvk.query.clone()), mode)?;
291
292            Ok(Self {
293                g_alpha,
294                h_beta,
295                g_alpha_pc,
296                h_beta_pc,
297                g_gamma_pc,
298                h_gamma_pc,
299                h_pc,
300                query,
301            })
302        })
303    }
304}
305
306impl<E, P> AllocVar<VerifyingKey<E>, E::Fq> for VerifyingKeyVar<E, P>
307where
308    E: PairingEngine,
309
310    P: PairingVar<E>,
311{
312    fn new_variable<T: Borrow<VerifyingKey<E>>>(
313        cs: impl Into<Namespace<E::Fq>>,
314        f: impl FnOnce() -> Result<T, SynthesisError>,
315        mode: AllocationMode,
316    ) -> Result<Self, SynthesisError> {
317        let ns = cs.into();
318        let cs = ns.cs();
319
320        f().and_then(|vk| {
321            let vk = vk.borrow();
322            let g_alpha_g1 = P::G1Var::new_variable(cs.ns("g_alpha"), || Ok(vk.g_alpha_g1), mode)?;
323            let h_g2 = P::G2Var::new_variable(cs.ns("h"), || Ok(vk.h_g2), mode)?;
324            let h_beta_g2 = P::G2Var::new_variable(cs.ns("h_beta"), || Ok(vk.h_beta_g2), mode)?;
325            let g_gamma_g1 = P::G1Var::new_variable(cs.ns("g_gamma"), || Ok(&vk.g_gamma_g1), mode)?;
326            let h_gamma_g2 = P::G2Var::new_variable(cs.ns("h_gamma"), || Ok(&vk.h_gamma_g2), mode)?;
327            let query = Vec::new_variable(cs.ns("query"), || Ok(vk.query.clone()), mode)?;
328            Ok(Self {
329                h_g2,
330                g_alpha_g1,
331                h_beta_g2,
332                g_gamma_g1,
333                h_gamma_g2,
334                query,
335            })
336        })
337    }
338}
339
340impl<E, P> AllocVar<Proof<E>, E::Fq> for ProofVar<E, P>
341where
342    E: PairingEngine,
343
344    P: PairingVar<E>,
345{
346    #[inline]
347    fn new_variable<T: Borrow<Proof<E>>>(
348        cs: impl Into<Namespace<E::Fq>>,
349        f: impl FnOnce() -> Result<T, SynthesisError>,
350        mode: AllocationMode,
351    ) -> Result<Self, SynthesisError> {
352        let ns = cs.into();
353        let cs = ns.cs();
354
355        f().and_then(|proof| {
356            let Proof { a, b, c } = proof.borrow().clone();
357            let a = P::G1Var::new_variable(cs.ns("a"), || Ok(a), mode)?;
358            let b = P::G2Var::new_variable(cs.ns("b"), || Ok(b), mode)?;
359            let c = P::G1Var::new_variable(cs.ns("c"), || Ok(c), mode)?;
360            Ok(Self { a, b, c })
361        })
362    }
363}
364
365impl<E, P> ToBytesGadget<E::Fq> for VerifyingKeyVar<E, P>
366where
367    E: PairingEngine,
368
369    P: PairingVar<E>,
370{
371    #[inline]
372    fn to_bytes(&self) -> Result<Vec<UInt8<E::Fq>>, SynthesisError> {
373        let mut bytes = Vec::new();
374        bytes.extend_from_slice(&self.h_g2.to_bytes()?);
375        bytes.extend_from_slice(&self.g_alpha_g1.to_bytes()?);
376        bytes.extend_from_slice(&self.h_beta_g2.to_bytes()?);
377        bytes.extend_from_slice(&self.g_gamma_g1.to_bytes()?);
378        bytes.extend_from_slice(&self.h_gamma_g2.to_bytes()?);
379        for q in &self.query {
380            bytes.extend_from_slice(&q.to_bytes()?);
381        }
382        Ok(bytes)
383    }
384}
385
386#[cfg(test)]
387mod test {
388    use gm17::*;
389    use r1cs_core::{
390        lc, ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
391    };
392
393    use super::*;
394    use algebra::{
395        bls12_377::{Bls12_377, Fq, Fr},
396        test_rng, BitIteratorLE, Field, PrimeField,
397    };
398    use r1cs_std::{bls12_377::PairingVar as Bls12_377PairingVar, boolean::Boolean, Assignment};
399    use rand::Rng;
400
401    type TestProofSystem = Gm17<Bls12_377, Bench<Fr>, Fr>;
402    type TestVerifierGadget = Gm17VerifierGadget<Bls12_377, Bls12_377PairingVar>;
403    type TestProofVar = ProofVar<Bls12_377, Bls12_377PairingVar>;
404    type TestVkVar = VerifyingKeyVar<Bls12_377, Bls12_377PairingVar>;
405
406    struct Bench<F: Field> {
407        inputs: Vec<Option<F>>,
408        num_constraints: usize,
409    }
410
411    impl<F: Field> ConstraintSynthesizer<F> for Bench<F> {
412        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
413            assert!(self.inputs.len() >= 2);
414            assert!(self.num_constraints >= self.inputs.len());
415
416            let mut variables: Vec<_> = Vec::with_capacity(self.inputs.len());
417            for input in self.inputs {
418                let input_var = cs.new_input_variable(|| input.get())?;
419                variables.push((input, input_var));
420            }
421
422            for i in 0..self.num_constraints {
423                let new_entry = {
424                    let (input_1_val, input_1_var) = variables[i];
425                    let (input_2_val, input_2_var) = variables[i + 1];
426                    let result_val = input_1_val
427                        .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
428                    let result_var = cs.new_witness_variable(|| {
429                        result_val.ok_or(SynthesisError::AssignmentMissing)
430                    })?;
431                    cs.enforce_named_constraint(
432                        format!("Enforce constraint {}", i),
433                        lc!() + input_1_var,
434                        lc!() + input_2_var,
435                        lc!() + result_var,
436                    )
437                    .unwrap();
438                    (result_val, result_var)
439                };
440                variables.push(new_entry);
441            }
442            Ok(())
443        }
444    }
445
446    #[test]
447    fn gm17_verifier_test() {
448        let num_inputs = 100;
449        let num_constraints = num_inputs;
450        let rng = &mut test_rng();
451        let mut inputs: Vec<Option<Fr>> = Vec::with_capacity(num_inputs);
452        for _ in 0..num_inputs {
453            inputs.push(Some(rng.gen()));
454        }
455        let params = {
456            let c = Bench::<Fr> {
457                inputs: vec![None; num_inputs],
458                num_constraints,
459            };
460
461            generate_random_parameters(c, rng).unwrap()
462        };
463
464        {
465            let proof = {
466                // Create an instance of our circuit (with the
467                // witness)
468                let c = Bench {
469                    inputs: inputs.clone(),
470                    num_constraints,
471                };
472                // Create a gm17 proof with our parameters.
473                create_random_proof(c, &params, rng).unwrap()
474            };
475
476            // assert!(!verify_proof(&pvk, &proof, &[a]).unwrap());
477            let cs = ConstraintSystem::<Fq>::new_ref();
478
479            let inputs: Vec<_> = inputs.into_iter().map(|input| input.unwrap()).collect();
480            let mut input_gadgets = Vec::new();
481
482            {
483                for (i, input) in inputs.into_iter().enumerate() {
484                    let input_bits: Vec<_> = BitIteratorLE::new(input.into_repr()).collect();
485                    let input_bits =
486                        Vec::<Boolean<Fq>>::new_input(cs.ns(format!("Input {}", i)), || {
487                            Ok(input_bits)
488                        })
489                        .unwrap();
490                    input_gadgets.push(input_bits);
491                }
492            }
493
494            let vk_gadget = TestVkVar::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
495            let proof_gadget =
496                TestProofVar::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
497            println!("Time to verify!\n\n\n\n");
498            <TestVerifierGadget as NIZKVerifierGadget<TestProofSystem, Fq>>::verify(
499                &vk_gadget,
500                &input_gadgets,
501                &proof_gadget,
502            )
503            .unwrap()
504            .enforce_equal(&Boolean::TRUE)
505            .unwrap();
506
507            if !cs.is_satisfied().unwrap() {
508                println!("=========================================================");
509                println!("Unsatisfied constraints:");
510                println!("{:?}", cs.which_is_unsatisfied().unwrap());
511                println!("=========================================================");
512            }
513
514            // cs.print_named_objects();
515            assert!(cs.is_satisfied().unwrap());
516        }
517    }
518}
519
520#[cfg(test)]
521mod test_recursive {
522    use gm17::*;
523    use r1cs_core::{
524        lc, ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
525    };
526
527    use super::*;
528    use algebra::{
529        fields::{FftParameters, FpParameters},
530        mnt4_298::{Fq as MNT4Fq, FqParameters as MNT4FqParameters, Fr as MNT4Fr, MNT4_298},
531        mnt6_298::{Fq as MNT6Fq, FqParameters as MNT6FqParameters, Fr as MNT6Fr, MNT6_298},
532        test_rng, BigInteger, Field, PrimeField,
533    };
534    use r1cs_std::{
535        fields::fp::FpVar, mnt4_298::PairingVar as MNT4_298PairingVar,
536        mnt6_298::PairingVar as MNT6_298PairingVar, uint8::UInt8, Assignment,
537    };
538    use rand::Rng;
539
540    type TestProofSystem1 = Gm17<MNT6_298, Bench<MNT4Fq>, MNT6Fr>;
541    type TestVerifierGadget1 = Gm17VerifierGadget<MNT6_298, MNT6_298PairingVar>;
542    type TestProofVar1 = ProofVar<MNT6_298, MNT6_298PairingVar>;
543    type TestVkVar1 = VerifyingKeyVar<MNT6_298, MNT6_298PairingVar>;
544
545    type TestProofSystem2 = Gm17<MNT4_298, Wrapper, MNT4Fr>;
546    type TestVerifierGadget2 = Gm17VerifierGadget<MNT4_298, MNT4_298PairingVar>;
547    type TestProofVar2 = ProofVar<MNT4_298, MNT4_298PairingVar>;
548    type TestVkVar2 = VerifyingKeyVar<MNT4_298, MNT4_298PairingVar>;
549
550    #[derive(Clone)]
551    struct Bench<F: Field> {
552        inputs: Vec<Option<F>>,
553        num_constraints: usize,
554    }
555
556    impl<F: Field> ConstraintSynthesizer<F> for Bench<F> {
557        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
558            assert!(self.inputs.len() >= 2);
559            assert!(self.num_constraints >= self.inputs.len());
560
561            let mut variables: Vec<_> = Vec::with_capacity(self.inputs.len());
562            for input in self.inputs {
563                let input_var = cs.new_input_variable(|| input.get())?;
564                variables.push((input, input_var));
565            }
566
567            for i in 0..self.num_constraints {
568                let new_entry = {
569                    let (input_1_val, input_1_var) = variables[i];
570                    let (input_2_val, input_2_var) = variables[i + 1];
571                    let result_val = input_1_val
572                        .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
573                    let result_var = cs.new_witness_variable(|| {
574                        result_val.ok_or(SynthesisError::AssignmentMissing)
575                    })?;
576                    cs.enforce_named_constraint(
577                        format!("Enforce constraint {}", i),
578                        lc!() + input_1_var,
579                        lc!() + input_2_var,
580                        lc!() + result_var,
581                    )
582                    .unwrap();
583                    (result_val, result_var)
584                };
585                variables.push(new_entry);
586            }
587            Ok(())
588        }
589    }
590
591    struct Wrapper {
592        inputs: Vec<Option<MNT4Fq>>,
593        params: Parameters<MNT6_298>,
594        proof: Proof<MNT6_298>,
595    }
596
597    impl ConstraintSynthesizer<MNT6Fq> for Wrapper {
598        fn generate_constraints(
599            self,
600            cs: ConstraintSystemRef<MNT6Fq>,
601        ) -> Result<(), SynthesisError> {
602            let params = self.params;
603            let proof = self.proof;
604            let inputs: Vec<_> = self
605                .inputs
606                .into_iter()
607                .map(|input| input.unwrap())
608                .collect();
609            let input_gadgets;
610
611            {
612                // Chain all input values in one large byte array.
613                let input_bytes = inputs
614                    .clone()
615                    .into_iter()
616                    .flat_map(|input| {
617                        input
618                            .into_repr()
619                            .as_ref()
620                            .iter()
621                            .flat_map(|l| l.to_le_bytes().to_vec())
622                            .collect::<Vec<_>>()
623                    })
624                    .collect::<Vec<_>>();
625
626                // Allocate this byte array as input packed into field elements.
627                let input_bytes = UInt8::new_input_vec(cs.ns("Input"), &input_bytes[..])?;
628                // 40 byte
629                let element_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 8;
630                input_gadgets = input_bytes
631                    .chunks(element_size)
632                    .map(|chunk| {
633                        chunk
634                            .iter()
635                            .flat_map(|byte| byte.to_bits_le().unwrap())
636                            .collect::<Vec<_>>()
637                    })
638                    .collect::<Vec<_>>();
639            }
640
641            let vk_gadget = TestVkVar1::new_witness(cs.ns("Vk"), || Ok(&params.vk))?;
642            let proof_gadget =
643                TestProofVar1::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
644            <TestVerifierGadget1 as NIZKVerifierGadget<TestProofSystem1, MNT6Fq>>::verify(
645                &vk_gadget,
646                &input_gadgets,
647                &proof_gadget,
648            )?
649            .enforce_equal(&Boolean::TRUE)?;
650            Ok(())
651        }
652    }
653
654    #[test]
655    fn gm17_recursive_verifier_test() {
656        let num_inputs = 5;
657        let num_constraints = num_inputs;
658        let rng = &mut test_rng();
659        let mut inputs: Vec<Option<MNT4Fq>> = Vec::with_capacity(num_inputs);
660        for _ in 0..num_inputs {
661            inputs.push(Some(rng.gen()));
662        }
663
664        // Generate inner params and proof.
665        let inner_params = {
666            let c = Bench::<MNT4Fq> {
667                inputs: vec![None; num_inputs],
668                num_constraints,
669            };
670
671            generate_random_parameters(c, rng).unwrap()
672        };
673
674        let inner_proof = {
675            // Create an instance of our circuit (with the
676            // witness)
677            let c = Bench {
678                inputs: inputs.clone(),
679                num_constraints,
680            };
681            // Create a gm17 proof with our parameters.
682            create_random_proof(c, &inner_params, rng).unwrap()
683        };
684
685        // Generate outer params and proof.
686        let params = {
687            let c = Wrapper {
688                inputs: inputs.clone(),
689                params: inner_params.clone(),
690                proof: inner_proof.clone(),
691            };
692
693            generate_random_parameters(c, rng).unwrap()
694        };
695
696        {
697            let proof = {
698                // Create an instance of our circuit (with the
699                // witness)
700                let c = Wrapper {
701                    inputs: inputs.clone(),
702                    params: inner_params.clone(),
703                    proof: inner_proof.clone(),
704                };
705                // Create a gm17 proof with our parameters.
706                create_random_proof(c, &params, rng).unwrap()
707            };
708
709            let cs = ConstraintSystem::<MNT4Fq>::new_ref();
710
711            let inputs: Vec<_> = inputs.into_iter().map(|input| input.unwrap()).collect();
712            let mut input_gadgets = Vec::new();
713
714            {
715                let bigint_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 64;
716                let mut input_bits = Vec::new();
717                for (i, input) in inputs.into_iter().enumerate() {
718                    let input_gadget =
719                        FpVar::new_input(cs.ns(format!("Input {}", i)), || Ok(input)).unwrap();
720                    let mut fp_bits = input_gadget.to_bits_le().unwrap();
721
722                    // Use 320 bits per element.
723                    for _ in fp_bits.len()..bigint_size {
724                        fp_bits.push(Boolean::constant(false));
725                    }
726                    input_bits.extend_from_slice(&fp_bits);
727                }
728
729                // Pack input bits into field elements of the underlying circuit.
730                let max_size = 8 * (<MNT6FqParameters as FpParameters>::CAPACITY / 8) as usize;
731                let max_size = max_size as usize;
732                let bigint_size = <MNT6FqParameters as FftParameters>::BigInt::NUM_LIMBS * 64;
733                for chunk in input_bits.chunks(max_size) {
734                    let mut chunk = chunk.to_vec();
735                    let len = chunk.len();
736                    for _ in len..bigint_size {
737                        chunk.push(Boolean::constant(false));
738                    }
739                    input_gadgets.push(chunk);
740                }
741                // assert!(!verify_proof(&pvk, &proof, &[a]).unwrap());
742            }
743
744            let vk_gadget = TestVkVar2::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
745            let proof_gadget =
746                TestProofVar2::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
747            println!("Time to verify!\n\n\n\n");
748            <TestVerifierGadget2 as NIZKVerifierGadget<TestProofSystem2, MNT4Fq>>::verify(
749                &vk_gadget,
750                &input_gadgets,
751                &proof_gadget,
752            )
753            .unwrap()
754            .enforce_equal(&Boolean::TRUE)
755            .unwrap();
756            if !cs.is_satisfied().unwrap() {
757                println!("=========================================================");
758                println!("Unsatisfied constraints:");
759                println!("{:?}", cs.which_is_unsatisfied().unwrap());
760                println!("=========================================================");
761            }
762
763            // cs.print_named_objects();
764            assert!(cs.is_satisfied().unwrap());
765        }
766    }
767}