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