1use crate::nizk::{groth16::Groth16, NIZKVerifierGadget};
  2use algebra_core::{AffineCurve, Field, PairingEngine, ToConstraintField};
  3use r1cs_core::{ConstraintSynthesizer, ConstraintSystem, SynthesisError};
  4use r1cs_std::prelude::*;
  5
  6use core::{borrow::Borrow, marker::PhantomData};
  7use groth16::{Proof, VerifyingKey};
  8
  9#[derive(Derivative)]
 10#[derivative(Clone(bound = "P::G1Gadget: Clone, P::G2Gadget: Clone"))]
 11pub struct ProofGadget<
 12    PairingE: PairingEngine,
 13    ConstraintF: Field,
 14    P: PairingGadget<PairingE, ConstraintF>,
 15> {
 16    pub a: P::G1Gadget,
 17    pub b: P::G2Gadget,
 18    pub c: P::G1Gadget,
 19}
 20
 21#[derive(Derivative)]
 22#[derivative(Clone(
 23    bound = "P::G1Gadget: Clone, P::GTGadget: Clone, P::G1PreparedGadget: Clone, \
 24             P::G2PreparedGadget: Clone, "
 25))]
 26pub struct VerifyingKeyGadget<
 27    PairingE: PairingEngine,
 28    ConstraintF: Field,
 29    P: PairingGadget<PairingE, ConstraintF>,
 30> {
 31    pub alpha_g1:     P::G1Gadget,
 32    pub beta_g2:      P::G2Gadget,
 33    pub gamma_g2:     P::G2Gadget,
 34    pub delta_g2:     P::G2Gadget,
 35    pub gamma_abc_g1: Vec<P::G1Gadget>,
 36}
 37
 38impl<PairingE: PairingEngine, ConstraintF: Field, P: PairingGadget<PairingE, ConstraintF>>
 39    VerifyingKeyGadget<PairingE, ConstraintF, P>
 40{
 41    pub fn prepare<CS: ConstraintSystem<ConstraintF>>(
 42        &self,
 43        mut cs: CS,
 44    ) -> Result<PreparedVerifyingKeyGadget<PairingE, ConstraintF, P>, SynthesisError> {
 45        let mut cs = cs.ns(|| "Preparing verifying key");
 46        let alpha_g1_pc = P::prepare_g1(&mut cs.ns(|| "Prepare alpha_g1"), &self.alpha_g1)?;
 47        let beta_g2_pc = P::prepare_g2(&mut cs.ns(|| "Prepare beta_g2"), &self.beta_g2)?;
 48
 49        let alpha_g1_beta_g2 = P::pairing(
 50            &mut cs.ns(|| "Precompute e(alpha_g1, beta_g2)"),
 51            alpha_g1_pc,
 52            beta_g2_pc,
 53        )?;
 54
 55        let gamma_g2_neg = self.gamma_g2.negate(&mut cs.ns(|| "Negate gamma_g2"))?;
 56        let gamma_g2_neg_pc = P::prepare_g2(&mut cs.ns(|| "Prepare gamma_g2_neg"), &gamma_g2_neg)?;
 57
 58        let delta_g2_neg = self.delta_g2.negate(&mut cs.ns(|| "Negate delta_g2"))?;
 59        let delta_g2_neg_pc = P::prepare_g2(&mut cs.ns(|| "Prepare delta_g2_neg"), &delta_g2_neg)?;
 60
 61        Ok(PreparedVerifyingKeyGadget {
 62            alpha_g1_beta_g2,
 63            gamma_g2_neg_pc,
 64            delta_g2_neg_pc,
 65            gamma_abc_g1: self.gamma_abc_g1.clone(),
 66        })
 67    }
 68}
 69
 70#[derive(Derivative)]
 71#[derivative(Clone(
 72    bound = "P::G1Gadget: Clone, P::GTGadget: Clone, P::G1PreparedGadget: Clone, \
 73             P::G2PreparedGadget: Clone, "
 74))]
 75pub struct PreparedVerifyingKeyGadget<
 76    PairingE: PairingEngine,
 77    ConstraintF: Field,
 78    P: PairingGadget<PairingE, ConstraintF>,
 79> {
 80    pub alpha_g1_beta_g2: P::GTGadget,
 81    pub gamma_g2_neg_pc:  P::G2PreparedGadget,
 82    pub delta_g2_neg_pc:  P::G2PreparedGadget,
 83    pub gamma_abc_g1:     Vec<P::G1Gadget>,
 84}
 85
 86pub struct Groth16VerifierGadget<PairingE, ConstraintF, P>
 87where
 88    PairingE: PairingEngine,
 89    ConstraintF: Field,
 90    P: PairingGadget<PairingE, ConstraintF>,
 91{
 92    _pairing_engine: PhantomData<PairingE>,
 93    _engine:         PhantomData<ConstraintF>,
 94    _pairing_gadget: PhantomData<P>,
 95}
 96
 97impl<PairingE, ConstraintF, P, C, V> NIZKVerifierGadget<Groth16<PairingE, C, V>, ConstraintF>
 98    for Groth16VerifierGadget<PairingE, ConstraintF, P>
 99where
100    PairingE: PairingEngine,
101    ConstraintF: Field,
102    C: ConstraintSynthesizer<PairingE::Fr>,
103    V: ToConstraintField<PairingE::Fr>,
104    P: PairingGadget<PairingE, ConstraintF>,
105{
106    type VerificationKeyGadget = VerifyingKeyGadget<PairingE, ConstraintF, P>;
107    type ProofGadget = ProofGadget<PairingE, ConstraintF, P>;
108
109    fn check_verify<'a, CS, I, T>(
110        mut cs: CS,
111        vk: &Self::VerificationKeyGadget,
112        mut public_inputs: I,
113        proof: &Self::ProofGadget,
114    ) -> Result<(), SynthesisError>
115    where
116        CS: ConstraintSystem<ConstraintF>,
117        I: Iterator<Item = &'a T>,
118        T: 'a + ToBitsGadget<ConstraintF> + ?Sized,
119    {
120        let pvk = vk.prepare(&mut cs.ns(|| "Prepare vk"))?;
121
122        let g_ic = {
123            let mut cs = cs.ns(|| "Process input");
124            let mut g_ic = pvk.gamma_abc_g1[0].clone();
125            let mut input_len = 1;
126            for (i, (input, b)) in public_inputs
127                .by_ref()
128                .zip(pvk.gamma_abc_g1.iter().skip(1))
129                .enumerate()
130            {
131                let input_bits = input.to_bits(cs.ns(|| format!("Input {}", i)))?;
132                g_ic = b.mul_bits(cs.ns(|| format!("Mul {}", i)), &g_ic, input_bits.iter())?;
133                input_len += 1;
134            }
135            // Check that the input and the query in the verification are of the
136            // same length.
137            assert!(input_len == pvk.gamma_abc_g1.len() && public_inputs.next().is_none());
138            g_ic
139        };
140
141        let test_exp = {
142            let proof_a_prep = P::prepare_g1(cs.ns(|| "Prepare proof a"), &proof.a)?;
143            let proof_b_prep = P::prepare_g2(cs.ns(|| "Prepare proof b"), &proof.b)?;
144            let proof_c_prep = P::prepare_g1(cs.ns(|| "Prepare proof c"), &proof.c)?;
145
146            let g_ic_prep = P::prepare_g1(cs.ns(|| "Prepare g_ic"), &g_ic)?;
147
148            P::miller_loop(
149                cs.ns(|| "Miller loop 1"),
150                &[proof_a_prep, g_ic_prep, proof_c_prep],
151                &[
152                    proof_b_prep,
153                    pvk.gamma_g2_neg_pc.clone(),
154                    pvk.delta_g2_neg_pc.clone(),
155                ],
156            )?
157        };
158
159        let test = P::final_exponentiation(cs.ns(|| "Final Exp"), &test_exp).unwrap();
160
161        test.enforce_equal(cs.ns(|| "Test 1"), &pvk.alpha_g1_beta_g2)?;
162        Ok(())
163    }
164}
165
166impl<PairingE, ConstraintF, P> AllocGadget<VerifyingKey<PairingE>, ConstraintF>
167    for VerifyingKeyGadget<PairingE, ConstraintF, P>
168where
169    PairingE: PairingEngine,
170    ConstraintF: Field,
171    P: PairingGadget<PairingE, ConstraintF>,
172{
173    #[inline]
174    fn alloc<FN, T, CS: ConstraintSystem<ConstraintF>>(
175        mut cs: CS,
176        value_gen: FN,
177    ) -> Result<Self, SynthesisError>
178    where
179        FN: FnOnce() -> Result<T, SynthesisError>,
180        T: Borrow<VerifyingKey<PairingE>>,
181    {
182        value_gen().and_then(|vk| {
183            let VerifyingKey {
184                alpha_g1,
185                beta_g2,
186                gamma_g2,
187                delta_g2,
188                gamma_abc_g1,
189            } = vk.borrow().clone();
190            let alpha_g1 =
191                P::G1Gadget::alloc(cs.ns(|| "alpha_g1"), || Ok(alpha_g1.into_projective()))?;
192            let beta_g2 =
193                P::G2Gadget::alloc(cs.ns(|| "beta_g2"), || Ok(beta_g2.into_projective()))?;
194            let gamma_g2 =
195                P::G2Gadget::alloc(cs.ns(|| "gamma_g2"), || Ok(gamma_g2.into_projective()))?;
196            let delta_g2 =
197                P::G2Gadget::alloc(cs.ns(|| "delta_g2"), || Ok(delta_g2.into_projective()))?;
198
199            let gamma_abc_g1 = gamma_abc_g1
200                .into_iter()
201                .enumerate()
202                .map(|(i, gamma_abc_i)| {
203                    P::G1Gadget::alloc(cs.ns(|| format!("gamma_abc_{}", i)), || {
204                        Ok(gamma_abc_i.into_projective())
205                    })
206                })
207                .collect::<Vec<_>>()
208                .into_iter()
209                .collect::<Result<_, _>>()?;
210            Ok(Self {
211                alpha_g1,
212                beta_g2,
213                gamma_g2,
214                delta_g2,
215                gamma_abc_g1,
216            })
217        })
218    }
219
220    #[inline]
221    fn alloc_input<FN, T, CS: ConstraintSystem<ConstraintF>>(
222        mut cs: CS,
223        value_gen: FN,
224    ) -> Result<Self, SynthesisError>
225    where
226        FN: FnOnce() -> Result<T, SynthesisError>,
227        T: Borrow<VerifyingKey<PairingE>>,
228    {
229        value_gen().and_then(|vk| {
230            let VerifyingKey {
231                alpha_g1,
232                beta_g2,
233                gamma_g2,
234                delta_g2,
235                gamma_abc_g1,
236            } = vk.borrow().clone();
237            let alpha_g1 =
238                P::G1Gadget::alloc_input(cs.ns(|| "alpha_g1"), || Ok(alpha_g1.into_projective()))?;
239            let beta_g2 =
240                P::G2Gadget::alloc_input(cs.ns(|| "beta_g2"), || Ok(beta_g2.into_projective()))?;
241            let gamma_g2 =
242                P::G2Gadget::alloc_input(cs.ns(|| "gamma_g2"), || Ok(gamma_g2.into_projective()))?;
243            let delta_g2 =
244                P::G2Gadget::alloc_input(cs.ns(|| "delta_g2"), || Ok(delta_g2.into_projective()))?;
245
246            let gamma_abc_g1 = gamma_abc_g1
247                .into_iter()
248                .enumerate()
249                .map(|(i, gamma_abc_i)| {
250                    P::G1Gadget::alloc_input(cs.ns(|| format!("gamma_abc_{}", i)), || {
251                        Ok(gamma_abc_i.into_projective())
252                    })
253                })
254                .collect::<Vec<_>>()
255                .into_iter()
256                .collect::<Result<_, _>>()?;
257
258            Ok(Self {
259                alpha_g1,
260                beta_g2,
261                gamma_g2,
262                delta_g2,
263                gamma_abc_g1,
264            })
265        })
266    }
267}
268
269impl<PairingE, ConstraintF, P> AllocGadget<Proof<PairingE>, ConstraintF>
270    for ProofGadget<PairingE, ConstraintF, P>
271where
272    PairingE: PairingEngine,
273    ConstraintF: Field,
274    P: PairingGadget<PairingE, ConstraintF>,
275{
276    #[inline]
277    fn alloc<FN, T, CS: ConstraintSystem<ConstraintF>>(
278        mut cs: CS,
279        value_gen: FN,
280    ) -> Result<Self, SynthesisError>
281    where
282        FN: FnOnce() -> Result<T, SynthesisError>,
283        T: Borrow<Proof<PairingE>>,
284    {
285        value_gen().and_then(|proof| {
286            let Proof { a, b, c } = proof.borrow().clone();
287            let a = P::G1Gadget::alloc_checked(cs.ns(|| "a"), || Ok(a.into_projective()))?;
288            let b = P::G2Gadget::alloc_checked(cs.ns(|| "b"), || Ok(b.into_projective()))?;
289            let c = P::G1Gadget::alloc_checked(cs.ns(|| "c"), || Ok(c.into_projective()))?;
290            Ok(Self { a, b, c })
291        })
292    }
293
294    #[inline]
295    fn alloc_input<FN, T, CS: ConstraintSystem<ConstraintF>>(
296        mut cs: CS,
297        value_gen: FN,
298    ) -> Result<Self, SynthesisError>
299    where
300        FN: FnOnce() -> Result<T, SynthesisError>,
301        T: Borrow<Proof<PairingE>>,
302    {
303        value_gen().and_then(|proof| {
304            let Proof { a, b, c } = proof.borrow().clone();
305            // We don't need to check here because the prime order check can be performed
306            // in plain.
307            let a = P::G1Gadget::alloc_input(cs.ns(|| "a"), || Ok(a.into_projective()))?;
308            let b = P::G2Gadget::alloc_input(cs.ns(|| "b"), || Ok(b.into_projective()))?;
309            let c = P::G1Gadget::alloc_input(cs.ns(|| "c"), || Ok(c.into_projective()))?;
310            Ok(Self { a, b, c })
311        })
312    }
313}
314
315impl<PairingE, ConstraintF, P> ToBytesGadget<ConstraintF>
316    for VerifyingKeyGadget<PairingE, ConstraintF, P>
317where
318    PairingE: PairingEngine,
319    ConstraintF: Field,
320    P: PairingGadget<PairingE, ConstraintF>,
321{
322    #[inline]
323    fn to_bytes<CS: ConstraintSystem<ConstraintF>>(
324        &self,
325        mut cs: CS,
326    ) -> Result<Vec<UInt8>, SynthesisError> {
327        let mut bytes = Vec::new();
328        bytes.extend_from_slice(&self.alpha_g1.to_bytes(&mut cs.ns(|| "alpha_g1 to bytes"))?);
329        bytes.extend_from_slice(&self.beta_g2.to_bytes(&mut cs.ns(|| "beta_g2 to bytes"))?);
330        bytes.extend_from_slice(&self.gamma_g2.to_bytes(&mut cs.ns(|| "gamma_g2 to bytes"))?);
331        bytes.extend_from_slice(&self.delta_g2.to_bytes(&mut cs.ns(|| "delta_g2 to bytes"))?);
332        for (i, g) in self.gamma_abc_g1.iter().enumerate() {
333            let mut cs = cs.ns(|| format!("Iteration {}", i));
334            bytes.extend_from_slice(&g.to_bytes(&mut cs.ns(|| "g"))?);
335        }
336        Ok(bytes)
337    }
338
339    fn to_bytes_strict<CS: ConstraintSystem<ConstraintF>>(
340        &self,
341        cs: CS,
342    ) -> Result<Vec<UInt8>, SynthesisError> {
343        self.to_bytes(cs)
344    }
345}
346
347#[cfg(test)]
348mod test {
349    use groth16::*;
350    use r1cs_core::{ConstraintSynthesizer, ConstraintSystem, SynthesisError};
351
352    use super::*;
353    use algebra::{
354        bls12_377::{Bls12_377, Fq, Fr},
355        test_rng, BitIterator, PrimeField,
356    };
357    use r1cs_std::{
358        bls12_377::PairingGadget as Bls12_377PairingGadget, boolean::Boolean,
359        test_constraint_system::TestConstraintSystem,
360    };
361    use rand::Rng;
362
363    type TestProofSystem = Groth16<Bls12_377, Bench<Fr>, Fr>;
364    type TestVerifierGadget = Groth16VerifierGadget<Bls12_377, Fq, Bls12_377PairingGadget>;
365    type TestProofGadget = ProofGadget<Bls12_377, Fq, Bls12_377PairingGadget>;
366    type TestVkGadget = VerifyingKeyGadget<Bls12_377, Fq, Bls12_377PairingGadget>;
367
368    struct Bench<F: Field> {
369        inputs:          Vec<Option<F>>,
370        num_constraints: usize,
371    }
372
373    impl<F: Field> ConstraintSynthesizer<F> for Bench<F> {
374        fn generate_constraints<CS: ConstraintSystem<F>>(
375            self,
376            cs: &mut CS,
377        ) -> Result<(), SynthesisError> {
378            assert!(self.inputs.len() >= 2);
379            assert!(self.num_constraints >= self.inputs.len());
380
381            let mut variables: Vec<_> = Vec::with_capacity(self.inputs.len());
382            for (i, input) in self.inputs.into_iter().enumerate() {
383                let input_var = cs.alloc_input(
384                    || format!("Input {}", i),
385                    || input.ok_or(SynthesisError::AssignmentMissing),
386                )?;
387                variables.push((input, input_var));
388            }
389
390            for i in 0..self.num_constraints {
391                let new_entry = {
392                    let (input_1_val, input_1_var) = variables[i];
393                    let (input_2_val, input_2_var) = variables[i + 1];
394                    let result_val = input_1_val
395                        .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
396                    let result_var = cs.alloc(
397                        || format!("Result {}", i),
398                        || result_val.ok_or(SynthesisError::AssignmentMissing),
399                    )?;
400                    cs.enforce(
401                        || format!("Enforce constraint {}", i),
402                        |lc| lc + input_1_var,
403                        |lc| lc + input_2_var,
404                        |lc| lc + result_var,
405                    );
406                    (result_val, result_var)
407                };
408                variables.push(new_entry);
409            }
410            Ok(())
411        }
412    }
413
414    #[test]
415    fn groth16_verifier_test() {
416        let num_inputs = 100;
417        let num_constraints = num_inputs;
418        let rng = &mut test_rng();
419        let mut inputs: Vec<Option<Fr>> = Vec::with_capacity(num_inputs);
420        for _ in 0..num_inputs {
421            inputs.push(Some(rng.gen()));
422        }
423        let params = {
424            let c = Bench::<Fr> {
425                inputs: vec![None; num_inputs],
426                num_constraints,
427            };
428
429            generate_random_parameters(c, rng).unwrap()
430        };
431
432        {
433            let proof = {
434                // Create an instance of our circuit (with the
435                // witness)
436                let c = Bench {
437                    inputs: inputs.clone(),
438                    num_constraints,
439                };
440                // Create a groth16 proof with our parameters.
441                create_random_proof(c, &params, rng).unwrap()
442            };
443
444            // assert!(!verify_proof(&pvk, &proof, &[a]).unwrap());
445            let mut cs = TestConstraintSystem::<Fq>::new();
446
447            let inputs: Vec<_> = inputs.into_iter().map(|input| input.unwrap()).collect();
448            let mut input_gadgets = Vec::new();
449
450            {
451                let mut cs = cs.ns(|| "Allocate Input");
452                for (i, input) in inputs.into_iter().enumerate() {
453                    let mut input_bits = BitIterator::new(input.into_repr()).collect::<Vec<_>>();
454                    // Input must be in little-endian, but BitIterator outputs in big-endian.
455                    input_bits.reverse();
456
457                    let input_bits =
458                        Vec::<Boolean>::alloc_input(cs.ns(|| format!("Input {}", i)), || {
459                            Ok(input_bits)
460                        })
461                        .unwrap();
462                    input_gadgets.push(input_bits);
463                }
464            }
465
466            let vk_gadget = TestVkGadget::alloc_input(cs.ns(|| "Vk"), || Ok(&params.vk)).unwrap();
467            let proof_gadget =
468                TestProofGadget::alloc(cs.ns(|| "Proof"), || Ok(proof.clone())).unwrap();
469            println!("Time to verify!\n\n\n\n");
470            <TestVerifierGadget as NIZKVerifierGadget<TestProofSystem, Fq>>::check_verify(
471                cs.ns(|| "Verify"),
472                &vk_gadget,
473                input_gadgets.iter(),
474                &proof_gadget,
475            )
476            .unwrap();
477            if !cs.is_satisfied() {
478                println!("=========================================================");
479                println!("Unsatisfied constraints:");
480                println!("{:?}", cs.which_is_unsatisfied().unwrap());
481                println!("=========================================================");
482            }
483
484            // cs.print_named_objects();
485            assert!(cs.is_satisfied());
486        }
487    }
488}