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 conditional_verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
180        vk: &Self::VerificationKeyVar,
181        input: impl Iterator<Item = &'a T>,
182        proof: &Self::ProofVar,
183        condition: &Boolean<E::Fq>,
184    ) -> Result<(), SynthesisError> {
185        let pvk = vk.prepare()?;
186        <Self as NIZKVerifierGadget<Gm17<E, C, V>, E::Fq>>::conditional_verify_prepared(
187            &pvk, input, proof, condition,
188        )
189    }
190
191    fn conditional_verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
192        pvk: &Self::PreparedVerificationKeyVar,
193        mut input: impl Iterator<Item = &'a T>,
194        proof: &Self::ProofVar,
195        condition: &Boolean<E::Fq>,
196    ) -> Result<(), SynthesisError> {
197        let pvk = pvk.clone();
198        // e(A*G^{alpha}, B*H^{beta}) = e(G^{alpha}, H^{beta}) * e(G^{psi}, H^{gamma}) *
199        // e(C, H) where psi = \sum_{i=0}^l input_i pvk.query[i]
200        let g_psi = {
201            let mut g_psi = pvk.query[0].clone();
202            let mut input_len = 1;
203            for (input, b) in input.by_ref().zip(pvk.query.iter().skip(1)) {
204                let input_bits = input.to_bits()?;
205                g_psi += b.mul_bits(input_bits.iter())?;
206                input_len += 1;
207            }
208            // Check that the input and the query in the verification are of the
209            // same length.
210            assert!(input_len == pvk.query.len() && input.next().is_none());
211            g_psi
212        };
213
214        let mut test1_a_g_alpha = proof.a.clone();
215        test1_a_g_alpha += pvk.g_alpha.clone();
216        let mut test1_b_h_beta = proof.b.clone();
217        test1_b_h_beta += pvk.h_beta.clone();
218
219        let test1_exp = {
220            test1_a_g_alpha = test1_a_g_alpha.negate()?;
221            let test1_a_g_alpha_prep = P::prepare_g1(&test1_a_g_alpha)?;
222            let test1_b_h_beta_prep = P::prepare_g2(&test1_b_h_beta)?;
223
224            let g_psi_prep = P::prepare_g1(&g_psi)?;
225
226            let c_prep = P::prepare_g1(&proof.c)?;
227
228            P::miller_loop(
229                &[
230                    test1_a_g_alpha_prep,
231                    g_psi_prep,
232                    c_prep,
233                    pvk.g_alpha_pc.clone(),
234                ],
235                &[
236                    test1_b_h_beta_prep,
237                    pvk.h_gamma_pc.clone(),
238                    pvk.h_pc.clone(),
239                    pvk.h_beta_pc.clone(),
240                ],
241            )?
242        };
243
244        let test1 = P::final_exponentiation(&test1_exp).unwrap();
245
246        // e(A, H^{gamma}) = e(G^{gamma}, B)
247        let test2_exp = {
248            let a_prep = P::prepare_g1(&proof.a)?;
249            // pvk.h_gamma_pc
250            //&pvk.g_gamma_pc
251            let proof_b = proof.b.negate()?;
252            let b_prep = P::prepare_g2(&proof_b)?;
253            P::miller_loop(&[a_prep, pvk.g_gamma_pc.clone()], &[pvk.h_gamma_pc, b_prep])?
254        };
255        let test2 = P::final_exponentiation(&test2_exp)?;
256
257        let one = P::GTVar::one();
258        test1.conditional_enforce_equal(&one, condition)?;
259        test2.conditional_enforce_equal(&one, condition)?;
260        Ok(())
261    }
262}
263
264impl<E, P> AllocVar<PreparedVerifyingKey<E>, E::Fq> for PreparedVerifyingKeyVar<E, P>
265where
266    E: PairingEngine,
267    P: PairingVar<E>,
268    P::G1PreparedVar: AllocVar<E::G1Prepared, E::Fq>,
269    P::G2PreparedVar: AllocVar<E::G2Prepared, E::Fq>,
270{
271    fn new_variable<T: Borrow<PreparedVerifyingKey<E>>>(
272        cs: impl Into<Namespace<E::Fq>>,
273        f: impl FnOnce() -> Result<T, SynthesisError>,
274        mode: AllocationMode,
275    ) -> Result<Self, SynthesisError> {
276        let ns = cs.into();
277        let cs = ns.cs();
278
279        f().and_then(|pvk| {
280            let pvk = pvk.borrow();
281            let g_alpha = P::G1Var::new_variable(cs.ns("g_alpha"), || Ok(pvk.g_alpha), mode)?;
282            let h_beta = P::G2Var::new_variable(cs.ns("h_beta"), || Ok(pvk.h_beta), mode)?;
283            let g_alpha_pc = P::G1PreparedVar::new_variable(
284                cs.ns("g_alpha_pc"),
285                || Ok(pvk.g_alpha.into()),
286                mode,
287            )?;
288            let h_beta_pc =
289                P::G2PreparedVar::new_variable(cs.ns("h_beta_pc"), || Ok(pvk.h_beta.into()), mode)?;
290            let g_gamma_pc =
291                P::G1PreparedVar::new_variable(cs.ns("g_gamma_pc"), || Ok(&pvk.g_gamma_pc), mode)?;
292            let h_gamma_pc =
293                P::G2PreparedVar::new_variable(cs.ns("h_gamma_pc"), || Ok(&pvk.h_gamma_pc), mode)?;
294            let h_pc = P::G2PreparedVar::new_variable(cs.ns("h_pc"), || Ok(&pvk.h_pc), mode)?;
295            let query = Vec::new_variable(cs.ns("query"), || Ok(pvk.query.clone()), mode)?;
296
297            Ok(Self {
298                g_alpha,
299                h_beta,
300                g_alpha_pc,
301                h_beta_pc,
302                g_gamma_pc,
303                h_gamma_pc,
304                h_pc,
305                query,
306            })
307        })
308    }
309}
310
311impl<E, P> AllocVar<VerifyingKey<E>, E::Fq> for VerifyingKeyVar<E, P>
312where
313    E: PairingEngine,
314
315    P: PairingVar<E>,
316{
317    fn new_variable<T: Borrow<VerifyingKey<E>>>(
318        cs: impl Into<Namespace<E::Fq>>,
319        f: impl FnOnce() -> Result<T, SynthesisError>,
320        mode: AllocationMode,
321    ) -> Result<Self, SynthesisError> {
322        let ns = cs.into();
323        let cs = ns.cs();
324
325        f().and_then(|vk| {
326            let vk = vk.borrow();
327            let g_alpha_g1 = P::G1Var::new_variable(cs.ns("g_alpha"), || Ok(vk.g_alpha_g1), mode)?;
328            let h_g2 = P::G2Var::new_variable(cs.ns("h"), || Ok(vk.h_g2), mode)?;
329            let h_beta_g2 = P::G2Var::new_variable(cs.ns("h_beta"), || Ok(vk.h_beta_g2), mode)?;
330            let g_gamma_g1 = P::G1Var::new_variable(cs.ns("g_gamma"), || Ok(&vk.g_gamma_g1), mode)?;
331            let h_gamma_g2 = P::G2Var::new_variable(cs.ns("h_gamma"), || Ok(&vk.h_gamma_g2), mode)?;
332            let query = Vec::new_variable(cs.ns("query"), || Ok(vk.query.clone()), mode)?;
333            Ok(Self {
334                h_g2,
335                g_alpha_g1,
336                h_beta_g2,
337                g_gamma_g1,
338                h_gamma_g2,
339                query,
340            })
341        })
342    }
343}
344
345impl<E, P> AllocVar<Proof<E>, E::Fq> for ProofVar<E, P>
346where
347    E: PairingEngine,
348
349    P: PairingVar<E>,
350{
351    #[inline]
352    fn new_variable<T: Borrow<Proof<E>>>(
353        cs: impl Into<Namespace<E::Fq>>,
354        f: impl FnOnce() -> Result<T, SynthesisError>,
355        mode: AllocationMode,
356    ) -> Result<Self, SynthesisError> {
357        let ns = cs.into();
358        let cs = ns.cs();
359
360        f().and_then(|proof| {
361            let Proof { a, b, c } = proof.borrow().clone();
362            let a = P::G1Var::new_variable(cs.ns("a"), || Ok(a), mode)?;
363            let b = P::G2Var::new_variable(cs.ns("b"), || Ok(b), mode)?;
364            let c = P::G1Var::new_variable(cs.ns("c"), || Ok(c), mode)?;
365            Ok(Self { a, b, c })
366        })
367    }
368}
369
370impl<E, P> ToBytesGadget<E::Fq> for VerifyingKeyVar<E, P>
371where
372    E: PairingEngine,
373
374    P: PairingVar<E>,
375{
376    #[inline]
377    fn to_bytes(&self) -> Result<Vec<UInt8<E::Fq>>, SynthesisError> {
378        let mut bytes = Vec::new();
379        bytes.extend_from_slice(&self.h_g2.to_bytes()?);
380        bytes.extend_from_slice(&self.g_alpha_g1.to_bytes()?);
381        bytes.extend_from_slice(&self.h_beta_g2.to_bytes()?);
382        bytes.extend_from_slice(&self.g_gamma_g1.to_bytes()?);
383        bytes.extend_from_slice(&self.h_gamma_g2.to_bytes()?);
384        for q in &self.query {
385            bytes.extend_from_slice(&q.to_bytes()?);
386        }
387        Ok(bytes)
388    }
389}
390
391#[cfg(test)]
392mod test {
393    use gm17::*;
394    use r1cs_core::{
395        lc, ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
396    };
397
398    use super::*;
399    use algebra::{
400        bls12_377::{Bls12_377, Fq, Fr},
401        test_rng, BitIterator, Field, PrimeField,
402    };
403    use r1cs_std::{bls12_377::PairingVar as Bls12_377PairingVar, boolean::Boolean, Assignment};
404    use rand::Rng;
405
406    type TestProofSystem = Gm17<Bls12_377, Bench<Fr>, Fr>;
407    type TestVerifierGadget = Gm17VerifierGadget<Bls12_377, Bls12_377PairingVar>;
408    type TestProofVar = ProofVar<Bls12_377, Bls12_377PairingVar>;
409    type TestVkVar = VerifyingKeyVar<Bls12_377, Bls12_377PairingVar>;
410
411    struct Bench<F: Field> {
412        inputs: Vec<Option<F>>,
413        num_constraints: usize,
414    }
415
416    impl<F: Field> ConstraintSynthesizer<F> for Bench<F> {
417        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
418            assert!(self.inputs.len() >= 2);
419            assert!(self.num_constraints >= self.inputs.len());
420
421            let mut variables: Vec<_> = Vec::with_capacity(self.inputs.len());
422            for input in self.inputs {
423                let input_var = cs.new_input_variable(|| input.get())?;
424                variables.push((input, input_var));
425            }
426
427            for i in 0..self.num_constraints {
428                let new_entry = {
429                    let (input_1_val, input_1_var) = variables[i];
430                    let (input_2_val, input_2_var) = variables[i + 1];
431                    let result_val = input_1_val
432                        .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
433                    let result_var = cs.new_witness_variable(|| {
434                        result_val.ok_or(SynthesisError::AssignmentMissing)
435                    })?;
436                    cs.enforce_named_constraint(
437                        format!("Enforce constraint {}", i),
438                        lc!() + input_1_var,
439                        lc!() + input_2_var,
440                        lc!() + result_var,
441                    )
442                    .unwrap();
443                    (result_val, result_var)
444                };
445                variables.push(new_entry);
446            }
447            Ok(())
448        }
449    }
450
451    #[test]
452    fn gm17_verifier_test() {
453        let num_inputs = 100;
454        let num_constraints = num_inputs;
455        let rng = &mut test_rng();
456        let mut inputs: Vec<Option<Fr>> = Vec::with_capacity(num_inputs);
457        for _ in 0..num_inputs {
458            inputs.push(Some(rng.gen()));
459        }
460        let params = {
461            let c = Bench::<Fr> {
462                inputs: vec![None; num_inputs],
463                num_constraints,
464            };
465
466            generate_random_parameters(c, rng).unwrap()
467        };
468
469        {
470            let proof = {
471                // Create an instance of our circuit (with the
472                // witness)
473                let c = Bench {
474                    inputs: inputs.clone(),
475                    num_constraints,
476                };
477                // Create a gm17 proof with our parameters.
478                create_random_proof(c, &params, rng).unwrap()
479            };
480
481            // assert!(!verify_proof(&pvk, &proof, &[a]).unwrap());
482            let cs = ConstraintSystem::<Fq>::new_ref();
483
484            let inputs: Vec<_> = inputs.into_iter().map(|input| input.unwrap()).collect();
485            let mut input_gadgets = Vec::new();
486
487            {
488                for (i, input) in inputs.into_iter().enumerate() {
489                    let mut input_bits = BitIterator::new(input.into_repr()).collect::<Vec<_>>();
490                    // Input must be in little-endian, but BitIterator outputs in big-endian.
491                    input_bits.reverse();
492
493                    let input_bits =
494                        Vec::<Boolean<Fq>>::new_input(cs.ns(format!("Input {}", i)), || {
495                            Ok(input_bits)
496                        })
497                        .unwrap();
498                    input_gadgets.push(input_bits);
499                }
500            }
501
502            let vk_gadget = TestVkVar::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
503            let proof_gadget =
504                TestProofVar::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
505            println!("Time to verify!\n\n\n\n");
506            <TestVerifierGadget as NIZKVerifierGadget<TestProofSystem, Fq>>::verify(
507                &vk_gadget,
508                input_gadgets.iter(),
509                &proof_gadget,
510            )
511            .unwrap();
512            if !cs.is_satisfied().unwrap() {
513                println!("=========================================================");
514                println!("Unsatisfied constraints:");
515                println!("{:?}", cs.which_is_unsatisfied().unwrap());
516                println!("=========================================================");
517            }
518
519            // cs.print_named_objects();
520            assert!(cs.is_satisfied().unwrap());
521        }
522    }
523}
524
525#[cfg(test)]
526mod test_recursive {
527    use gm17::*;
528    use r1cs_core::{
529        lc, ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
530    };
531
532    use super::*;
533    use algebra::{
534        fields::{FftParameters, FpParameters},
535        mnt4_298::{Fq as MNT4Fq, FqParameters as MNT4FqParameters, Fr as MNT4Fr, MNT4_298},
536        mnt6_298::{Fq as MNT6Fq, FqParameters as MNT6FqParameters, Fr as MNT6Fr, MNT6_298},
537        test_rng, BigInteger, Field, PrimeField,
538    };
539    use r1cs_std::{
540        fields::fp::FpVar, mnt4_298::PairingVar as MNT4_298PairingVar,
541        mnt6_298::PairingVar as MNT6_298PairingVar, uint8::UInt8, Assignment,
542    };
543    use rand::Rng;
544
545    type TestProofSystem1 = Gm17<MNT6_298, Bench<MNT4Fq>, MNT6Fr>;
546    type TestVerifierGadget1 = Gm17VerifierGadget<MNT6_298, MNT6_298PairingVar>;
547    type TestProofVar1 = ProofVar<MNT6_298, MNT6_298PairingVar>;
548    type TestVkVar1 = VerifyingKeyVar<MNT6_298, MNT6_298PairingVar>;
549
550    type TestProofSystem2 = Gm17<MNT4_298, Wrapper, MNT4Fr>;
551    type TestVerifierGadget2 = Gm17VerifierGadget<MNT4_298, MNT4_298PairingVar>;
552    type TestProofVar2 = ProofVar<MNT4_298, MNT4_298PairingVar>;
553    type TestVkVar2 = VerifyingKeyVar<MNT4_298, MNT4_298PairingVar>;
554
555    #[derive(Clone)]
556    struct Bench<F: Field> {
557        inputs: Vec<Option<F>>,
558        num_constraints: usize,
559    }
560
561    impl<F: Field> ConstraintSynthesizer<F> for Bench<F> {
562        fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
563            assert!(self.inputs.len() >= 2);
564            assert!(self.num_constraints >= self.inputs.len());
565
566            let mut variables: Vec<_> = Vec::with_capacity(self.inputs.len());
567            for input in self.inputs {
568                let input_var = cs.new_input_variable(|| input.get())?;
569                variables.push((input, input_var));
570            }
571
572            for i in 0..self.num_constraints {
573                let new_entry = {
574                    let (input_1_val, input_1_var) = variables[i];
575                    let (input_2_val, input_2_var) = variables[i + 1];
576                    let result_val = input_1_val
577                        .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
578                    let result_var = cs.new_witness_variable(|| {
579                        result_val.ok_or(SynthesisError::AssignmentMissing)
580                    })?;
581                    cs.enforce_named_constraint(
582                        format!("Enforce constraint {}", i),
583                        lc!() + input_1_var,
584                        lc!() + input_2_var,
585                        lc!() + result_var,
586                    )
587                    .unwrap();
588                    (result_val, result_var)
589                };
590                variables.push(new_entry);
591            }
592            Ok(())
593        }
594    }
595
596    struct Wrapper {
597        inputs: Vec<Option<MNT4Fq>>,
598        params: Parameters<MNT6_298>,
599        proof: Proof<MNT6_298>,
600    }
601
602    impl ConstraintSynthesizer<MNT6Fq> for Wrapper {
603        fn generate_constraints(
604            self,
605            cs: ConstraintSystemRef<MNT6Fq>,
606        ) -> Result<(), SynthesisError> {
607            let params = self.params;
608            let proof = self.proof;
609            let inputs: Vec<_> = self
610                .inputs
611                .into_iter()
612                .map(|input| input.unwrap())
613                .collect();
614            let input_gadgets;
615
616            {
617                // Chain all input values in one large byte array.
618                let input_bytes = inputs
619                    .clone()
620                    .into_iter()
621                    .flat_map(|input| {
622                        input
623                            .into_repr()
624                            .as_ref()
625                            .iter()
626                            .flat_map(|l| l.to_le_bytes().to_vec())
627                            .collect::<Vec<_>>()
628                    })
629                    .collect::<Vec<_>>();
630
631                // Allocate this byte array as input packed into field elements.
632                let input_bytes = UInt8::new_input_vec(cs.ns("Input"), &input_bytes[..])?;
633                // 40 byte
634                let element_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 8;
635                input_gadgets = input_bytes
636                    .chunks(element_size)
637                    .map(|chunk| {
638                        chunk
639                            .iter()
640                            .flat_map(|byte| byte.into_bits_le())
641                            .collect::<Vec<_>>()
642                    })
643                    .collect::<Vec<_>>();
644            }
645
646            let vk_gadget = TestVkVar1::new_witness(cs.ns("Vk"), || Ok(&params.vk))?;
647            let proof_gadget =
648                TestProofVar1::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
649            <TestVerifierGadget1 as NIZKVerifierGadget<TestProofSystem1, MNT6Fq>>::verify(
650                &vk_gadget,
651                input_gadgets.iter(),
652                &proof_gadget,
653            )?;
654            Ok(())
655        }
656    }
657
658    #[test]
659    fn gm17_recursive_verifier_test() {
660        let num_inputs = 5;
661        let num_constraints = num_inputs;
662        let rng = &mut test_rng();
663        let mut inputs: Vec<Option<MNT4Fq>> = Vec::with_capacity(num_inputs);
664        for _ in 0..num_inputs {
665            inputs.push(Some(rng.gen()));
666        }
667
668        // Generate inner params and proof.
669        let inner_params = {
670            let c = Bench::<MNT4Fq> {
671                inputs: vec![None; num_inputs],
672                num_constraints,
673            };
674
675            generate_random_parameters(c, rng).unwrap()
676        };
677
678        let inner_proof = {
679            // Create an instance of our circuit (with the
680            // witness)
681            let c = Bench {
682                inputs: inputs.clone(),
683                num_constraints,
684            };
685            // Create a gm17 proof with our parameters.
686            create_random_proof(c, &inner_params, rng).unwrap()
687        };
688
689        // Generate outer params and proof.
690        let params = {
691            let c = Wrapper {
692                inputs: inputs.clone(),
693                params: inner_params.clone(),
694                proof: inner_proof.clone(),
695            };
696
697            generate_random_parameters(c, rng).unwrap()
698        };
699
700        {
701            let proof = {
702                // Create an instance of our circuit (with the
703                // witness)
704                let c = Wrapper {
705                    inputs: inputs.clone(),
706                    params: inner_params.clone(),
707                    proof: inner_proof.clone(),
708                };
709                // Create a gm17 proof with our parameters.
710                create_random_proof(c, &params, rng).unwrap()
711            };
712
713            let cs = ConstraintSystem::<MNT4Fq>::new_ref();
714
715            let inputs: Vec<_> = inputs.into_iter().map(|input| input.unwrap()).collect();
716            let mut input_gadgets = Vec::new();
717
718            {
719                let bigint_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 64;
720                let mut input_bits = Vec::new();
721                for (i, input) in inputs.into_iter().enumerate() {
722                    let input_gadget =
723                        FpVar::new_input(cs.ns(format!("Input {}", i)), || Ok(input)).unwrap();
724                    let mut fp_bits = input_gadget.to_bits().unwrap();
725
726                    // FpVar::to_bits outputs a big-endian binary representation of
727                    // fe_gadget's value, so we have to reverse it to get the little-endian
728                    // form.
729                    fp_bits.reverse();
730
731                    // Use 320 bits per element.
732                    for _ in fp_bits.len()..bigint_size {
733                        fp_bits.push(Boolean::constant(false));
734                    }
735                    input_bits.extend_from_slice(&fp_bits);
736                }
737
738                // Pack input bits into field elements of the underlying circuit.
739                let max_size = 8 * (<MNT6FqParameters as FpParameters>::CAPACITY / 8) as usize;
740                let max_size = max_size as usize;
741                let bigint_size = <MNT6FqParameters as FftParameters>::BigInt::NUM_LIMBS * 64;
742                for chunk in input_bits.chunks(max_size) {
743                    let mut chunk = chunk.to_vec();
744                    let len = chunk.len();
745                    for _ in len..bigint_size {
746                        chunk.push(Boolean::constant(false));
747                    }
748                    input_gadgets.push(chunk);
749                }
750                // assert!(!verify_proof(&pvk, &proof, &[a]).unwrap());
751            }
752
753            let vk_gadget = TestVkVar2::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
754            let proof_gadget =
755                TestProofVar2::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
756            println!("Time to verify!\n\n\n\n");
757            <TestVerifierGadget2 as NIZKVerifierGadget<TestProofSystem2, MNT4Fq>>::verify(
758                &vk_gadget,
759                input_gadgets.iter(),
760                &proof_gadget,
761            )
762            .unwrap();
763            if !cs.is_satisfied().unwrap() {
764                println!("=========================================================");
765                println!("Unsatisfied constraints:");
766                println!("{:?}", cs.which_is_unsatisfied().unwrap());
767                println!("=========================================================");
768            }
769
770            // cs.print_named_objects();
771            assert!(cs.is_satisfied().unwrap());
772        }
773    }
774}