Update pairings in `r1cs-std`.

r1cs-std/src/pairing/bls12/mod.rs

@@ -1,10 +1,10 @@
-use r1cs_core::{ConstraintSystem, SynthesisError};
+use r1cs_core::SynthesisError;
 
-use super::PairingGadget as PG;
+use super::PairingVar as PG;
 
 use crate::{
-    fields::{fp::FpGadget, fp12::Fp12Gadget, fp2::Fp2Gadget, FieldGadget},
-    groups::bls12::{G1Gadget, G1PreparedGadget, G2Gadget, G2PreparedGadget},
+    fields::{fp::FpVar, fp12::Fp12Var, fp2::Fp2Var, FieldVar},
+    groups::bls12::{G1AffineVar, G1PreparedVar, G1Var, G2PreparedVar, G2Var},
 };
 use algebra::{
     curves::bls12::{Bls12, Bls12Parameters, TwistType},
@@ -12,168 +12,151 @@ use algebra::{
 };
 use core::marker::PhantomData;
 
-pub struct PairingGadget<P: Bls12Parameters>(PhantomData<P>);
+pub struct PairingVar<P: Bls12Parameters>(PhantomData<P>);
 
-type Fp2G<P> = Fp2Gadget<<P as Bls12Parameters>::Fp2Params, <P as Bls12Parameters>::Fp>;
+type Fp2V<P> = Fp2Var<<P as Bls12Parameters>::Fp2Params>;
 
-impl<P: Bls12Parameters> PairingGadget<P> {
+impl<P: Bls12Parameters> PairingVar<P> {
     // Evaluate the line function at point p.
-    fn ell<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        f: &mut Fp12Gadget<P::Fp12Params, P::Fp>,
-        coeffs: &(Fp2G<P>, Fp2G<P>),
-        p: &G1Gadget<P>,
+    fn ell(
+        f: &mut Fp12Var<P::Fp12Params>,
+        coeffs: &(Fp2V<P>, Fp2V<P>),
+        p: &G1AffineVar<P>,
     ) -> Result<(), SynthesisError> {
-        let zero = FpGadget::<P::Fp>::zero(cs.ns(|| "fpg zero"))?;
+        let zero = FpVar::<P::Fp>::zero();
 
         match P::TWIST_TYPE {
             TwistType::M => {
                 let c0 = coeffs.0.clone();
                 let mut c1 = coeffs.1.clone();
-                let c2 = Fp2G::<P>::new(p.y.clone(), zero);
+                let c2 = Fp2V::<P>::new(p.y.clone(), zero);
 
-                c1.c0 = c1.c0.mul(cs.ns(|| "mul c1.c0"), &p.x)?;
-                c1.c1 = c1.c1.mul(cs.ns(|| "mul c1.c1"), &p.x)?;
-                *f = f.mul_by_014(cs.ns(|| "sparse mul f"), &c0, &c1, &c2)?;
+                c1.c0 = c1.c0 * &p.x;
+                c1.c1 = c1.c1 * &p.x;
+                *f = f.mul_by_014(&c0, &c1, &c2)?;
                 Ok(())
             }
             TwistType::D => {
-                let c0 = Fp2G::<P>::new(p.y.clone(), zero);
+                let c0 = Fp2V::<P>::new(p.y.clone(), zero);
                 let mut c1 = coeffs.0.clone();
                 let c2 = coeffs.1.clone();
 
-                c1.c0 = c1.c0.mul(cs.ns(|| "mul c1.c0"), &p.x)?;
-                c1.c1 = c1.c1.mul(cs.ns(|| "mul c1.c1"), &p.x)?;
-                *f = f.mul_by_034(cs.ns(|| "sparse mul f"), &c0, &c1, &c2)?;
+                c1.c0 = c1.c0 * &p.x;
+                c1.c1 = c1.c1 * &p.x;
+                *f = f.mul_by_034(&c0, &c1, &c2)?;
                 Ok(())
             }
         }
     }
 
-    fn exp_by_x<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        f: &Fp12Gadget<P::Fp12Params, P::Fp>,
-    ) -> Result<Fp12Gadget<P::Fp12Params, P::Fp>, SynthesisError> {
-        let mut result = f.cyclotomic_exp(cs.ns(|| "exp_by_x"), P::X)?;
+    fn exp_by_x(f: &Fp12Var<P::Fp12Params>) -> Result<Fp12Var<P::Fp12Params>, SynthesisError> {
+        let mut result = f.optimized_cyclotomic_exp(P::X)?;
         if P::X_IS_NEGATIVE {
-            result.conjugate_in_place(cs.ns(|| "conjugate"))?;
+            result = result.unitary_inverse()?;
         }
         Ok(result)
     }
 }
 
-impl<P: Bls12Parameters> PG<Bls12<P>, P::Fp> for PairingGadget<P> {
-    type G1Gadget = G1Gadget<P>;
-    type G2Gadget = G2Gadget<P>;
-    type G1PreparedGadget = G1PreparedGadget<P>;
-    type G2PreparedGadget = G2PreparedGadget<P>;
-    type GTGadget = Fp12Gadget<P::Fp12Params, P::Fp>;
-
-    fn miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        ps: &[Self::G1PreparedGadget],
-        qs: &[Self::G2PreparedGadget],
-    ) -> Result<Self::GTGadget, SynthesisError> {
+impl<P: Bls12Parameters> PG<Bls12<P>, P::Fp> for PairingVar<P> {
+    type G1Var = G1Var<P>;
+    type G2Var = G2Var<P>;
+    type G1PreparedVar = G1PreparedVar<P>;
+    type G2PreparedVar = G2PreparedVar<P>;
+    type GTVar = Fp12Var<P::Fp12Params>;
+
+    fn miller_loop(
+        ps: &[Self::G1PreparedVar],
+        qs: &[Self::G2PreparedVar],
+    ) -> Result<Self::GTVar, SynthesisError> {
         let mut pairs = vec![];
         for (p, q) in ps.iter().zip(qs.iter()) {
             pairs.push((p, q.ell_coeffs.iter()));
         }
-        let mut f = Self::GTGadget::one(cs.ns(|| "one"))?;
+        let mut f = Self::GTVar::one();
 
-        for (j, i) in BitIterator::new(P::X).skip(1).enumerate() {
-            let mut cs = cs.ns(|| format!("Iteration {}", j));
-            f.square_in_place(cs.ns(|| "square"))?;
+        for i in BitIterator::new(P::X).skip(1) {
+            f.square_in_place()?;
 
-            for (k, &mut (p, ref mut coeffs)) in pairs.iter_mut().enumerate() {
-                let cs = cs.ns(|| format!("Double input {}", k));
-                Self::ell(cs, &mut f, coeffs.next().unwrap(), &p.0)?;
+            for &mut (p, ref mut coeffs) in pairs.iter_mut() {
+                Self::ell(&mut f, coeffs.next().unwrap(), &p.0)?;
             }
 
             if i {
-                for (k, &mut (p, ref mut coeffs)) in pairs.iter_mut().enumerate() {
-                    let cs = cs.ns(|| format!("Addition input {}", k));
-                    Self::ell(cs, &mut f, &coeffs.next().unwrap(), &p.0)?;
+                for &mut (p, ref mut coeffs) in pairs.iter_mut() {
+                    Self::ell(&mut f, &coeffs.next().unwrap(), &p.0)?;
                 }
             }
         }
 
         if P::X_IS_NEGATIVE {
-            f.conjugate_in_place(cs.ns(|| "f conjugate"))?;
+            f = f.unitary_inverse()?;
         }
 
         Ok(f)
     }
 
-    fn final_exponentiation<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        f: &Self::GTGadget,
-    ) -> Result<Self::GTGadget, SynthesisError> {
+    fn final_exponentiation(f: &Self::GTVar) -> Result<Self::GTVar, SynthesisError> {
         // Computing the final exponentation following
         // https://eprint.iacr.org/2016/130.pdf.
         // We don't use their "faster" formula because it is difficult to make
         // it work for curves with odd `P::X`.
         // Hence we implement the slower algorithm from Table 1 below.
 
-        let f1 = f.frobenius_map(cs.ns(|| "frobmap 1"), 6)?;
+        let f1 = f.frobenius_map(6)?;
 
-        f.inverse(cs.ns(|| "inverse 1")).and_then(|mut f2| {
+        f.inverse().and_then(|mut f2| {
             // f2 = f^(-1);
             // r = f^(p^6 - 1)
             let mut r = f1;
-            r.mul_in_place(cs.ns(|| "r = f1 * f2"), &f2)?;
+            r *= &f2;
 
             // f2 = f^(p^6 - 1)
             f2 = r.clone();
             // r = f^((p^6 - 1)(p^2))
-            r.frobenius_map_in_place(cs.ns(|| "frobenius map 2"), 2)?;
+            r.frobenius_map_in_place(2)?;
 
             // r = f^((p^6 - 1)(p^2) + (p^6 - 1))
             // r = f^((p^6 - 1)(p^2 + 1))
-            r.mul_in_place(cs.ns(|| "mul 0"), &f2)?;
+            r *= &f2;
 
             // Hard part of the final exponentation is below:
             // From https://eprint.iacr.org/2016/130.pdf, Table 1
-            let mut y0 = r.cyclotomic_square(cs.ns(|| "cyclotomic_sq 1"))?;
-            y0.conjugate_in_place(&mut cs.ns(|| "conjugate 2"))?;
-
-            let mut y5 = Self::exp_by_x(&mut cs.ns(|| "exp_by_x 1"), &r)?;
-
-            let mut y1 = y5.cyclotomic_square(&mut cs.ns(|| "square 1"))?;
-            let mut y3 = y0.mul(&mut cs.ns(|| "mul 1"), &y5)?;
-            y0 = Self::exp_by_x(cs.ns(|| "exp_by_x 2"), &y3)?;
-            let y2 = Self::exp_by_x(cs.ns(|| "exp_by_x 3"), &y0)?;
-            let mut y4 = Self::exp_by_x(cs.ns(|| "exp_by_x 4"), &y2)?;
-            y4.mul_in_place(cs.ns(|| "mul 2"), &y1)?;
-            y1 = Self::exp_by_x(cs.ns(|| "exp_by_x 5"), &y4)?;
-            y3.conjugate_in_place(cs.ns(|| "conjugate 3"))?;
-            y1.mul_in_place(cs.ns(|| "mul 3"), &y3)?;
-            y1.mul_in_place(cs.ns(|| "mul 4"), &r)?;
+            let mut y0 = r.cyclotomic_square()?;
+            y0 = y0.unitary_inverse()?;
+
+            let mut y5 = Self::exp_by_x(&r)?;
+
+            let mut y1 = y5.cyclotomic_square()?;
+            let mut y3 = y0 * &y5;
+            y0 = Self::exp_by_x(&y3)?;
+            let y2 = Self::exp_by_x(&y0)?;
+            let mut y4 = Self::exp_by_x(&y2)?;
+            y4 *= &y1;
+            y1 = Self::exp_by_x(&y4)?;
+            y3 = y3.unitary_inverse()?;
+            y1 *= &y3;
+            y1 *= &r;
             y3 = r.clone();
-            y3.conjugate_in_place(cs.ns(|| "conjugate 4"))?;
-            y0.mul_in_place(cs.ns(|| "mul 5"), &r)?;
-            y0.frobenius_map_in_place(cs.ns(|| "frobmap 3"), 3)?;
-            y4.mul_in_place(cs.ns(|| "mul 6"), &y3)?;
-            y4.frobenius_map_in_place(cs.ns(|| "frobmap 4"), 1)?;
-            y5.mul_in_place(cs.ns(|| "mul 7"), &y2)?;
-            y5.frobenius_map_in_place(cs.ns(|| "frobmap 5"), 2)?;
-            y5.mul_in_place(cs.ns(|| "mul 8"), &y0)?;
-            y5.mul_in_place(cs.ns(|| "mul 9"), &y4)?;
-            y5.mul_in_place(cs.ns(|| "mul 10"), &y1)?;
+            y3 = y3.unitary_inverse()?;
+            y0 *= &r;
+            y0.frobenius_map_in_place(3)?;
+            y4 *= &y3;
+            y4.frobenius_map_in_place(1)?;
+            y5 *= &y2;
+            y5.frobenius_map_in_place(2)?;
+            y5 *= &y0;
+            y5 *= &y4;
+            y5 *= &y1;
             Ok(y5)
         })
     }
 
-    fn prepare_g1<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        p: &Self::G1Gadget,
-    ) -> Result<Self::G1PreparedGadget, SynthesisError> {
-        Self::G1PreparedGadget::from_affine(cs, p)
+    fn prepare_g1(p: &Self::G1Var) -> Result<Self::G1PreparedVar, SynthesisError> {
+        Self::G1PreparedVar::from_group_var(p)
     }
 
-    fn prepare_g2<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        q: &Self::G2Gadget,
-    ) -> Result<Self::G2PreparedGadget, SynthesisError> {
-        Self::G2PreparedGadget::from_affine(cs, q)
+    fn prepare_g2(q: &Self::G2Var) -> Result<Self::G2PreparedVar, SynthesisError> {
+        Self::G2PreparedVar::from_group_var(q)
     }
 }

r1cs-std/src/pairing/mnt4/mod.rs

@@ -1,12 +1,12 @@
-use r1cs_core::{ConstraintSystem, SynthesisError};
+use r1cs_core::SynthesisError;
 
-use super::PairingGadget as PG;
+use super::PairingVar as PG;
 
 use crate::{
-    fields::{fp::FpGadget, fp2::Fp2Gadget, fp4::Fp4Gadget, FieldGadget},
+    fields::{fp::FpVar, fp2::Fp2Var, fp4::Fp4Var, FieldVar},
     groups::mnt4::{
-        AteAdditionCoefficientsGadget, AteDoubleCoefficientsGadget, G1Gadget, G1PreparedGadget,
-        G2Gadget, G2PreparedGadget, G2ProjectiveExtendedGadget,
+        AteAdditionCoefficientsVar, AteDoubleCoefficientsVar, G1PreparedVar, G1Var, G2PreparedVar,
+        G2ProjectiveExtendedVar, G2Var,
     },
 };
 use algebra::{
@@ -15,74 +15,39 @@ use algebra::{
 };
 use core::marker::PhantomData;
 
-pub struct PairingGadget<P: MNT4Parameters>(PhantomData<P>);
-
-type Fp2G<P> = Fp2Gadget<<P as MNT4Parameters>::Fp2Params, <P as MNT4Parameters>::Fp>;
-type Fp4G<P> = Fp4Gadget<<P as MNT4Parameters>::Fp4Params, <P as MNT4Parameters>::Fp>;
-pub type GTGadget<P> = Fp4G<P>;
-
-impl<P: MNT4Parameters> PairingGadget<P> {
-    pub(crate) fn doubling_step_for_flipped_miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        r: &G2ProjectiveExtendedGadget<P>,
-    ) -> Result<
-        (
-            G2ProjectiveExtendedGadget<P>,
-            AteDoubleCoefficientsGadget<P>,
-        ),
-        SynthesisError,
-    > {
-        let a = r.t.square(cs.ns(|| "r.t^2"))?;
-        let b = r.x.square(cs.ns(|| "r.x^2"))?;
-        let c = r.y.square(cs.ns(|| "r.y^2"))?;
-        let d = c.square(cs.ns(|| "c^2"))?;
-        let mut e = r.x.add(cs.ns(|| "r.x + c"), &c)?;
-        e.square_in_place(cs.ns(|| "(r.x + c)^2"))?;
-        e.sub_in_place(cs.ns(|| "(r.x + c)^2 - b"), &b)?;
-        e.sub_in_place(cs.ns(|| "(r.x + c)^2 - b - d"), &d)?;
-
-        let mut f = b.double(cs.ns(|| "b + b"))?;
-        f.add_in_place(cs.ns(|| "b + b + b"), &b)?;
-        let twist_a = a.mul_by_constant(cs.ns(|| "TWIST_COEFF_A * a"), &P::TWIST_COEFF_A)?;
-        f.add_in_place(cs.ns(|| "(b + b + b) + (TWIST_COEFF_A * a)"), &twist_a)?;
-        let g = f.square(cs.ns(|| "f^2"))?;
-
-        let d_eight = d
-            .double(cs.ns(|| "2 * d"))?
-            .double(cs.ns(|| "4 * d"))?
-            .double(cs.ns(|| "8 * d"))?;
-
-        let e2 = e.double(cs.ns(|| "2 * e"))?;
-        let e4 = e2.double(cs.ns(|| "4 * e"))?;
-        let x = g.sub(cs.ns(|| "- (e + e + e + e) + g"), &e4)?;
-
-        let mut y = e2.sub(cs.ns(|| "e + e - x"), &x)?;
-        y.mul_in_place(cs.ns(|| "f * (e + e - x)"), &f)?;
-        y.sub_in_place(cs.ns(|| "- d_eight + f * (e + e - x)"), &d_eight)?;
-        let mut z = r.y.add(cs.ns(|| "r.y + r.z"), &r.z)?;
-        z.square_in_place(cs.ns(|| "(r.y + r.z)^2"))?;
-        z.sub_in_place(cs.ns(|| "(r.y + r.z)^2 - c"), &c)?;
-        let z2 = r.z.square(cs.ns(|| "r.z^2"))?;
-        z.sub_in_place(cs.ns(|| "(r.y + r.z)^2 - c - r.z^2"), &z2)?;
-        let t = z.square(cs.ns(|| "z^2"))?;
-
-        let r2 = G2ProjectiveExtendedGadget { x, y, z, t };
-
-        let c_h =
-            r2.z.add(cs.ns(|| "r2.z + r.t"), &r.t)?
-                .square(cs.ns(|| "(r2.z + r.t)^2"))?
-                .sub(cs.ns(|| "(r2.z + r.t)^2 - r2.t"), &r2.t)?
-                .sub(cs.ns(|| "(r2.z + r.t)^2 - r2.t - a"), &a)?;
-        let c_4c = c.double(cs.ns(|| "2 * c"))?.double(cs.ns(|| "4 * c"))?;
-        let mut c_j = f.add(cs.ns(|| "f + r.t"), &r.t)?;
-        c_j.square_in_place(cs.ns(|| "(f + r.t)^2"))?;
-        c_j.sub_in_place(cs.ns(|| "(f + r.t)^2 - g"), &g)?;
-        c_j.sub_in_place(cs.ns(|| "(f + r.t)^2 - g - a"), &a)?;
-        let mut c_l = f.add(cs.ns(|| "f + r.x"), &r.x)?;
-        c_l.square_in_place(cs.ns(|| "(f + r.x)^2"))?;
-        c_l.sub_in_place(cs.ns(|| "(f + r.x)^2 - g"), &g)?;
-        c_l.sub_in_place(cs.ns(|| "(f + r.x)^2 - g - b"), &b)?;
-        let coeff = AteDoubleCoefficientsGadget {
+pub struct PairingVar<P: MNT4Parameters>(PhantomData<P>);
+
+type Fp2G<P> = Fp2Var<<P as MNT4Parameters>::Fp2Params>;
+type Fp4G<P> = Fp4Var<<P as MNT4Parameters>::Fp4Params>;
+pub type GTVar<P> = Fp4G<P>;
+
+impl<P: MNT4Parameters> PairingVar<P> {
+    pub(crate) fn doubling_step_for_flipped_miller_loop(
+        r: &G2ProjectiveExtendedVar<P>,
+    ) -> Result<(G2ProjectiveExtendedVar<P>, AteDoubleCoefficientsVar<P>), SynthesisError> {
+        let a = r.t.square()?;
+        let b = r.x.square()?;
+        let c = r.y.square()?;
+        let d = c.square()?;
+        let e = (&r.x + &c).square()? - &b - &d;
+        let f = (b.double()? + &b) + &a * P::TWIST_COEFF_A;
+        let g = f.square()?;
+
+        let d_eight = d.double()?.double()?.double()?;
+
+        let e2 = e.double()?;
+        let x = &g - &e2.double()?;
+
+        let y = &f * (&e2 - &x) - &d_eight;
+        let z = (&r.y + &r.z).square()? - &c - &r.z.square()?;
+        let t = z.square()?;
+
+        let r2 = G2ProjectiveExtendedVar { x, y, z, t };
+        let c_h = (&r2.z + &r.t).square()? - &r2.t - &a;
+        let c_4c = c.double()?.double()?;
+        let c_j = (&f + &r.t).square()? - &g - &a;
+        let c_l = (&f + &r.x).square()? - &g - &b;
+        let coeff = AteDoubleCoefficientsVar {
             c_h,
             c_4c,
             c_j,
@@ -92,76 +57,52 @@ impl PairingGadget {
         Ok((r2, coeff))
     }
 
-    pub(crate) fn mixed_addition_step_for_flipped_miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
+    pub(crate) fn mixed_addition_step_for_flipped_miller_loop(
         x: &Fp2G<P>,
         y: &Fp2G<P>,
-        r: &G2ProjectiveExtendedGadget<P>,
-    ) -> Result<
-        (
-            G2ProjectiveExtendedGadget<P>,
-            AteAdditionCoefficientsGadget<P>,
-        ),
-        SynthesisError,
-    > {
-        let a = y.square(cs.ns(|| "y^2"))?;
-        let b = r.t.mul(cs.ns(|| "r.t * x"), &x)?;
-        let mut d = r.z.add(cs.ns(|| "r.z + y"), &y)?;
-        d.square_in_place(cs.ns(|| "(r.z + y)^2"))?;
-        d.sub_in_place(cs.ns(|| "(r.z + y)^2 - a"), &a)?;
-        d.sub_in_place(cs.ns(|| "(r.z + y)^2 - a - r.t"), &r.t)?;
-        d.mul_in_place(cs.ns(|| "((r.z + y)^2 - a - r.t) * r.t"), &r.t)?;
-        let h = b.sub(cs.ns(|| "b - r.x"), &r.x)?;
-        let i = h.square(cs.ns(|| "h^2"))?;
-        let e = i.double(cs.ns(|| "2 * i"))?.double(cs.ns(|| "4 * i"))?;
-        let j = h.mul(cs.ns(|| "h * e"), &e)?;
-        let v = r.x.mul(cs.ns(|| "r.x * e"), &e)?;
-        let ry2 = r.y.double(cs.ns(|| "r.y + r.y"))?;
-        let l1 = d.sub(cs.ns(|| "d - (r.y + r.y)"), &ry2)?;
-
-        let v2 = v.double(cs.ns(|| "v + v"))?;
-        let x = l1
-            .square(cs.ns(|| "l1^2"))?
-            .sub(cs.ns(|| "l1^2 - j"), &j)?
-            .sub(cs.ns(|| "l1^2 - j - (v + v)"), &v2)?;
-        let v_minus_x = v.sub(cs.ns(|| "v - x"), &x)?;
-        let j_ry2 = j.mul(cs.ns(|| "j * (r.y + r.y)"), &ry2)?;
-        let y = l1
-            .mul(cs.ns(|| "l1 * (v - x)"), &v_minus_x)?
-            .sub(cs.ns(|| "l1 * (v - x) - (j * (r.y + r.y)"), &j_ry2)?;
-        let mut z = r.z.add(cs.ns(|| "r.z + h"), &h)?;
-        z.square_in_place(cs.ns(|| "(r.z + h)^2"))?;
-        z.sub_in_place(cs.ns(|| "(r.z + h)^2 - r.t"), &r.t)?;
-        z.sub_in_place(cs.ns(|| "(r.z + h)^2 - r.t - i"), &i)?;
-        let t = z.square(cs.ns(|| "z^2"))?;
-
-        let r2 = G2ProjectiveExtendedGadget {
+        r: &G2ProjectiveExtendedVar<P>,
+    ) -> Result<(G2ProjectiveExtendedVar<P>, AteAdditionCoefficientsVar<P>), SynthesisError> {
+        let a = y.square()?;
+        let b = &r.t * x;
+        let d = ((&r.z + y).square()? - &a - &r.t) * &r.t;
+        let h = &b - &r.x;
+        let i = h.square()?;
+        let e = i.double()?.double()?;
+        let j = &h * &e;
+        let v = &r.x * &e;
+        let ry2 = r.y.double()?;
+        let l1 = &d - &ry2;
+
+        let x = l1.square()? - &j - &v.double()?;
+        let y = &l1 * &(&v - &x) - j * &ry2;
+        let z = (&r.z + &h).square()? - &r.t - &i;
+        let t = z.square()?;
+
+        let r2 = G2ProjectiveExtendedVar {
             x,
             y,
             z: z.clone(),
             t,
         };
-        let coeff = AteAdditionCoefficientsGadget { c_l1: l1, c_rz: z };
+        let coeff = AteAdditionCoefficientsVar { c_l1: l1, c_rz: z };
 
         Ok((r2, coeff))
     }
 
-    pub fn ate_miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        p: &G1PreparedGadget<P>,
-        q: &G2PreparedGadget<P>,
+    pub fn ate_miller_loop(
+        p: &G1PreparedVar<P>,
+        q: &G2PreparedVar<P>,
     ) -> Result<Fp4G<P>, SynthesisError> {
-        let mut l1_coeff = Fp2G::<P>::new(p.x.clone(), FpGadget::<P::Fp>::zero(cs.ns(|| "zero"))?);
-        l1_coeff.sub_in_place(cs.ns(|| "l1_coeff"), &q.x_over_twist)?;
+        let l1_coeff = Fp2G::<P>::new(p.x.clone(), FpVar::<P::Fp>::zero()) - &q.x_over_twist;
 
-        let mut f = Fp4G::<P>::one(cs.ns(|| "one"))?;
+        let mut f = Fp4G::<P>::one();
 
         let mut dbl_idx: usize = 0;
         let mut add_idx: usize = 0;
 
         let mut found_one = false;
 
-        for (j, bit) in BitIterator::new(P::ATE_LOOP_COUNT).enumerate() {
+        for bit in BitIterator::new(P::ATE_LOOP_COUNT) {
             // code below gets executed for all bits (EXCEPT the MSB itself) of
             // mnt6_param_p (skipping leading zeros) in MSB to LSB order
             if !found_one && bit {
@@ -171,102 +112,61 @@ impl PairingGadget {
                 continue;
             }
 
-            let mut cs = cs.ns(|| format!("bit {}", j));
-
             let dc = &q.double_coefficients[dbl_idx];
             dbl_idx += 1;
 
-            let c_j_x_twist = dc.c_j.mul(cs.ns(|| "dc.c_j * p.x_twist"), &p.x_twist)?;
-            let c0 = dc.c_l.sub(cs.ns(|| "-dc.c_4c + dc.c_l"), &dc.c_4c)?.sub(
-                cs.ns(|| "-dc.c_4c - (dc.c_j * p.x_twist) + dc.c_l"),
-                &c_j_x_twist,
-            )?;
-            let c1 = dc.c_h.mul(cs.ns(|| "dc.c_h * p.y_twist"), &p.y_twist)?;
-            let g_rr_at_p = Fp4G::<P>::new(c0, c1);
+            let g_rr_at_p = Fp4G::<P>::new(
+                &dc.c_l - &dc.c_4c - &dc.c_j * &p.x_twist,
+                &dc.c_h * &p.y_twist,
+            );
 
-            f = f
-                .square(cs.ns(|| "f^2"))?
-                .mul(cs.ns(|| "f^2 * g_rr_at_p"), &g_rr_at_p)?;
+            f = f.square()? * &g_rr_at_p;
 
             if bit {
                 let ac = &q.addition_coefficients[add_idx];
                 add_idx += 1;
 
-                let l1_coeff_c_l1 = l1_coeff.mul(cs.ns(|| "l1_coeff * ac.c_l1"), &ac.c_l1)?;
                 let g_rq_at_p = Fp4G::<P>::new(
-                    ac.c_rz.mul(cs.ns(|| "ac.c_rz * p.y_twist"), &p.y_twist)?,
-                    q.y_over_twist
-                        .mul(cs.ns(|| "q.y_over_twist * ac.c_rz"), &ac.c_rz)?
-                        .add(
-                            cs.ns(|| "q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1)"),
-                            &l1_coeff_c_l1,
-                        )?
-                        .negate(cs.ns(|| "-(q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1))"))?,
+                    &ac.c_rz * &p.y_twist,
+                    (&q.y_over_twist * &ac.c_rz + &l1_coeff * &ac.c_l1).negate()?,
                 );
-                f.mul_in_place(cs.ns(|| "f *= g_rq_at_p"), &g_rq_at_p)?;
+                f *= &g_rq_at_p;
             }
         }
 
         if P::ATE_IS_LOOP_COUNT_NEG {
             let ac = &q.addition_coefficients[add_idx];
 
-            let l1_coeff_c_l1 = l1_coeff.mul(cs.ns(|| "l1_coeff * ac.c_l1"), &ac.c_l1)?;
             let g_rnegr_at_p = Fp4G::<P>::new(
-                ac.c_rz.mul(cs.ns(|| "ac.c_rz * p.y_twist"), &p.y_twist)?,
-                q.y_over_twist
-                    .mul(cs.ns(|| "q.y_over_twist * ac.c_rz"), &ac.c_rz)?
-                    .add(
-                        cs.ns(|| "q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1)"),
-                        &l1_coeff_c_l1,
-                    )?
-                    .negate(cs.ns(|| "-(q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1))"))?,
+                &ac.c_rz * &p.y_twist,
+                (&q.y_over_twist * &ac.c_rz + &l1_coeff * &ac.c_l1).negate()?,
             );
-            f = f
-                .mul(cs.ns(|| "f * g_rnegr_at_p"), &g_rnegr_at_p)?
-                .inverse(cs.ns(|| "inverse f"))?;
+            f = (&f * &g_rnegr_at_p).inverse()?;
         }
 
         Ok(f)
     }
 
-    pub fn final_exponentiation<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        value: &Fp4G<P>,
-    ) -> Result<GTGadget<P>, SynthesisError> {
-        let value_inv = value.inverse(cs.ns(|| "value inverse"))?;
-        let value_to_first_chunk = Self::final_exponentiation_first_chunk(
-            cs.ns(|| "value_to_first_chunk"),
-            value,
-            &value_inv,
-        )?;
-        let value_inv_to_first_chunk = Self::final_exponentiation_first_chunk(
-            cs.ns(|| "value_inv_to_first_chunk"),
-            &value_inv,
-            value,
-        )?;
-        Self::final_exponentiation_last_chunk(
-            cs.ns(|| "final_exp_last_chunk"),
-            &value_to_first_chunk,
-            &value_inv_to_first_chunk,
-        )
+    pub fn final_exponentiation(value: &Fp4G<P>) -> Result<GTVar<P>, SynthesisError> {
+        let value_inv = value.inverse()?;
+        let value_to_first_chunk = Self::final_exponentiation_first_chunk(value, &value_inv)?;
+        let value_inv_to_first_chunk = Self::final_exponentiation_first_chunk(&value_inv, value)?;
+        Self::final_exponentiation_last_chunk(&value_to_first_chunk, &value_inv_to_first_chunk)
     }
 
-    fn final_exponentiation_first_chunk<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
+    fn final_exponentiation_first_chunk(
         elt: &Fp4G<P>,
         elt_inv: &Fp4G<P>,
     ) -> Result<Fp4G<P>, SynthesisError> {
         // (q^2-1)
 
         // elt_q2 = elt^(q^2)
-        let mut elt_q2 = elt.clone();
-        elt_q2.frobenius_map_in_place(cs.ns(|| "frobenius 2"), 2)?;
+        let elt_q2 = elt.unitary_inverse()?;
         // elt_q2_over_elt = elt^(q^2-1)
-        elt_q2.mul(cs.ns(|| "elt_q2 * elt_inv"), elt_inv)
+        Ok(elt_q2 * elt_inv)
     }
 
-    fn final_exponentiation_last_chunk<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
+    fn final_exponentiation_last_chunk(
         elt: &Fp4G<P>,
         elt_inv: &Fp4G<P>,
     ) -> Result<Fp4G<P>, SynthesisError> {
@@ -274,65 +174,47 @@ impl PairingGadget {
         let elt_inv_clone = elt_inv.clone();
 
         let mut elt_q = elt.clone();
-        elt_q.frobenius_map_in_place(cs.ns(|| "frobenius 1"), 1)?;
+        elt_q.frobenius_map_in_place(1)?;
 
-        let w1_part = elt_q.cyclotomic_exp(cs.ns(|| "w1_part"), &P::FINAL_EXPONENT_LAST_CHUNK_1)?;
-        let w0_part;
-        if P::FINAL_EXPONENT_LAST_CHUNK_W0_IS_NEG {
-            w0_part = elt_inv_clone
-                .cyclotomic_exp(cs.ns(|| "w0_part"), &P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?;
+        let w1_part = elt_q.cyclotomic_exp(&P::FINAL_EXPONENT_LAST_CHUNK_1)?;
+        let w0_part = if P::FINAL_EXPONENT_LAST_CHUNK_W0_IS_NEG {
+            elt_inv_clone.cyclotomic_exp(&P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?
         } else {
-            w0_part = elt_clone
-                .cyclotomic_exp(cs.ns(|| "w0_part"), &P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?;
-        }
+            elt_clone.cyclotomic_exp(&P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?
+        };
 
-        w1_part.mul(cs.ns(|| "w1_part * w0_part"), &w0_part)
+        Ok(w1_part * &w0_part)
     }
 }
 
-impl<P: MNT4Parameters> PG<MNT4<P>, P::Fp> for PairingGadget<P> {
-    type G1Gadget = G1Gadget<P>;
-    type G2Gadget = G2Gadget<P>;
-    type G1PreparedGadget = G1PreparedGadget<P>;
-    type G2PreparedGadget = G2PreparedGadget<P>;
-    type GTGadget = GTGadget<P>;
-
-    fn miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        ps: &[Self::G1PreparedGadget],
-        qs: &[Self::G2PreparedGadget],
-    ) -> Result<Self::GTGadget, SynthesisError> {
-        let mut result = Fp4G::<P>::one(cs.ns(|| "one"))?;
-        for (i, (p, q)) in ps.iter().zip(qs.iter()).enumerate() {
-            let miller =
-                Self::ate_miller_loop(cs.ns(|| format!("ate miller loop iteration {}", i)), p, q)?;
-            result.mul_in_place(
-                cs.ns(|| format!("mul ate miller loop iteration {}", i)),
-                &miller,
-            )?;
+impl<P: MNT4Parameters> PG<MNT4<P>, P::Fp> for PairingVar<P> {
+    type G1Var = G1Var<P>;
+    type G2Var = G2Var<P>;
+    type G1PreparedVar = G1PreparedVar<P>;
+    type G2PreparedVar = G2PreparedVar<P>;
+    type GTVar = GTVar<P>;
+
+    fn miller_loop(
+        ps: &[Self::G1PreparedVar],
+        qs: &[Self::G2PreparedVar],
+    ) -> Result<Self::GTVar, SynthesisError> {
+        let mut result = Fp4G::<P>::one();
+        for (p, q) in ps.iter().zip(qs) {
+            result *= Self::ate_miller_loop(p, q)?;
         }
 
         Ok(result)
     }
 
-    fn final_exponentiation<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        r: &Self::GTGadget,
-    ) -> Result<Self::GTGadget, SynthesisError> {
-        Self::final_exponentiation(cs, r)
+    fn final_exponentiation(r: &Self::GTVar) -> Result<Self::GTVar, SynthesisError> {
+        Self::final_exponentiation(r)
     }
 
-    fn prepare_g1<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        p: &Self::G1Gadget,
-    ) -> Result<Self::G1PreparedGadget, SynthesisError> {
-        Self::G1PreparedGadget::from_affine(cs, p)
+    fn prepare_g1(p: &Self::G1Var) -> Result<Self::G1PreparedVar, SynthesisError> {
+        Self::G1PreparedVar::from_group_var(p)
     }
 
-    fn prepare_g2<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        q: &Self::G2Gadget,
-    ) -> Result<Self::G2PreparedGadget, SynthesisError> {
-        Self::G2PreparedGadget::from_affine(cs, q)
+    fn prepare_g2(q: &Self::G2Var) -> Result<Self::G2PreparedVar, SynthesisError> {
+        Self::G2PreparedVar::from_group_var(q)
     }
 }

r1cs-std/src/pairing/mnt6/mod.rs

@@ -1,12 +1,12 @@
-use r1cs_core::{ConstraintSystem, SynthesisError};
+use r1cs_core::SynthesisError;
 
-use super::PairingGadget as PG;
+use super::PairingVar as PG;
 
 use crate::{
-    fields::{fp::FpGadget, fp3::Fp3Gadget, fp6_2over3::Fp6Gadget, FieldGadget},
+    fields::{fp::FpVar, fp3::Fp3Var, fp6_2over3::Fp6Var, FieldVar},
     groups::mnt6::{
-        AteAdditionCoefficientsGadget, AteDoubleCoefficientsGadget, G1Gadget, G1PreparedGadget,
-        G2Gadget, G2PreparedGadget, G2ProjectiveExtendedGadget,
+        AteAdditionCoefficientsVar, AteDoubleCoefficientsVar, G1PreparedVar, G1Var, G2PreparedVar,
+        G2ProjectiveExtendedVar, G2Var,
     },
 };
 use algebra::{
@@ -15,154 +15,90 @@ use algebra::{
 };
 use core::marker::PhantomData;
 
-pub struct PairingGadget<P: MNT6Parameters>(PhantomData<P>);
-
-type Fp3G<P> = Fp3Gadget<<P as MNT6Parameters>::Fp3Params, <P as MNT6Parameters>::Fp>;
-type Fp6G<P> = Fp6Gadget<<P as MNT6Parameters>::Fp6Params, <P as MNT6Parameters>::Fp>;
-pub type GTGadget<P> = Fp6G<P>;
-
-impl<P: MNT6Parameters> PairingGadget<P> {
-    pub(crate) fn doubling_step_for_flipped_miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        r: &G2ProjectiveExtendedGadget<P>,
-    ) -> Result<
-        (
-            G2ProjectiveExtendedGadget<P>,
-            AteDoubleCoefficientsGadget<P>,
-        ),
-        SynthesisError,
-    > {
-        let a = r.t.square(cs.ns(|| "r.t^2"))?;
-        let b = r.x.square(cs.ns(|| "r.x^2"))?;
-        let c = r.y.square(cs.ns(|| "r.y^2"))?;
-        let d = c.square(cs.ns(|| "c^2"))?;
-        let mut e = r.x.add(cs.ns(|| "r.x + c"), &c)?;
-        e.square_in_place(cs.ns(|| "(r.x + c)^2"))?;
-        e.sub_in_place(cs.ns(|| "(r.x + c)^2 - b"), &b)?;
-        e.sub_in_place(cs.ns(|| "(r.x + c)^2 - b - d"), &d)?;
-
-        let mut f = b.double(cs.ns(|| "b + b"))?;
-        f.add_in_place(cs.ns(|| "b + b + b"), &b)?;
-        let twist_a = a.mul_by_constant(cs.ns(|| "TWIST_COEFF_A * a"), &P::TWIST_COEFF_A)?;
-        f.add_in_place(cs.ns(|| "(b + b + b) + (TWIST_COEFF_A * a)"), &twist_a)?;
-        let g = f.square(cs.ns(|| "f^2"))?;
-
-        let d_eight = d
-            .double(cs.ns(|| "2 * d"))?
-            .double(cs.ns(|| "4 * d"))?
-            .double(cs.ns(|| "8 * d"))?;
-
-        let e2 = e.double(cs.ns(|| "2 * e"))?;
-        let e4 = e2.double(cs.ns(|| "4 * e"))?;
-        let x = g.sub(cs.ns(|| "- (e + e + e + e) + g"), &e4)?;
-
-        let mut y = e2.sub(cs.ns(|| "e + e - x"), &x)?;
-        y.mul_in_place(cs.ns(|| "f * (e + e - x)"), &f)?;
-        y.sub_in_place(cs.ns(|| "- d_eight + f * (e + e - x)"), &d_eight)?;
-        let mut z = r.y.add(cs.ns(|| "r.y + r.z"), &r.z)?;
-        z.square_in_place(cs.ns(|| "(r.y + r.z)^2"))?;
-        z.sub_in_place(cs.ns(|| "(r.y + r.z)^2 - c"), &c)?;
-        let z2 = r.z.square(cs.ns(|| "r.z^2"))?;
-        z.sub_in_place(cs.ns(|| "(r.y + r.z)^2 - c - r.z^2"), &z2)?;
-        let t = z.square(cs.ns(|| "z^2"))?;
-
-        let r2 = G2ProjectiveExtendedGadget { x, y, z, t };
-
-        let c_h =
-            r2.z.add(cs.ns(|| "r2.z + r.t"), &r.t)?
-                .square(cs.ns(|| "(r2.z + r.t)^2"))?
-                .sub(cs.ns(|| "(r2.z + r.t)^2 - r2.t"), &r2.t)?
-                .sub(cs.ns(|| "(r2.z + r.t)^2 - r2.t - a"), &a)?;
-        let c_4c = c.double(cs.ns(|| "2 * c"))?.double(cs.ns(|| "4 * c"))?;
-        let mut c_j = f.add(cs.ns(|| "f + r.t"), &r.t)?;
-        c_j.square_in_place(cs.ns(|| "(f + r.t)^2"))?;
-        c_j.sub_in_place(cs.ns(|| "(f + r.t)^2 - g"), &g)?;
-        c_j.sub_in_place(cs.ns(|| "(f + r.t)^2 - g - a"), &a)?;
-        let mut c_l = f.add(cs.ns(|| "f + r.x"), &r.x)?;
-        c_l.square_in_place(cs.ns(|| "(f + r.x)^2"))?;
-        c_l.sub_in_place(cs.ns(|| "(f + r.x)^2 - g"), &g)?;
-        c_l.sub_in_place(cs.ns(|| "(f + r.x)^2 - g - b"), &b)?;
-        let coeff = AteDoubleCoefficientsGadget {
-            c_h,
-            c_4c,
-            c_j,
-            c_l,
+pub struct PairingVar<P: MNT6Parameters>(PhantomData<P>);
+
+type Fp3G<P> = Fp3Var<<P as MNT6Parameters>::Fp3Params>;
+type Fp6G<P> = Fp6Var<<P as MNT6Parameters>::Fp6Params>;
+pub type GTVar<P> = Fp6G<P>;
+
+impl<P: MNT6Parameters> PairingVar<P> {
+    pub(crate) fn doubling_step_for_flipped_miller_loop(
+        r: &G2ProjectiveExtendedVar<P>,
+    ) -> Result<(G2ProjectiveExtendedVar<P>, AteDoubleCoefficientsVar<P>), SynthesisError> {
+        let a = r.t.square()?;
+        let b = r.x.square()?;
+        let c = r.y.square()?;
+        let d = c.square()?;
+        let e = (&r.x + &c).square()? - &b - &d;
+        let f = b.double()? + &b + &(&a * P::TWIST_COEFF_A);
+        let g = f.square()?;
+
+        let d_eight = d.double()?.double()?.double()?;
+
+        let e2 = e.double()?;
+        let x = &g - e2.double()?;
+        let y = &f * (e2 - &x) - d_eight;
+        let z = (&r.y + &r.z).square()? - &c - &r.z.square()?;
+        let t = z.square()?;
+
+        let r2 = G2ProjectiveExtendedVar { x, y, z, t };
+        let coeff = AteDoubleCoefficientsVar {
+            c_h: (&r2.z + &r.t).square()? - &r2.t - &a,
+            c_4c: c.double()?.double()?,
+            c_j: (&f + &r.t).square()? - &g - &a,
+            c_l: (&f + &r.x).square()? - &g - &b,
         };
 
         Ok((r2, coeff))
     }
 
-    pub(crate) fn mixed_addition_step_for_flipped_miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
+    pub(crate) fn mixed_addition_step_for_flipped_miller_loop(
         x: &Fp3G<P>,
         y: &Fp3G<P>,
-        r: &G2ProjectiveExtendedGadget<P>,
-    ) -> Result<
-        (
-            G2ProjectiveExtendedGadget<P>,
-            AteAdditionCoefficientsGadget<P>,
-        ),
-        SynthesisError,
-    > {
-        let a = y.square(cs.ns(|| "y^2"))?;
-        let b = r.t.mul(cs.ns(|| "r.t * x"), &x)?;
-        let mut d = r.z.add(cs.ns(|| "r.z + y"), &y)?;
-        d.square_in_place(cs.ns(|| "(r.z + y)^2"))?;
-        d.sub_in_place(cs.ns(|| "(r.z + y)^2 - a"), &a)?;
-        d.sub_in_place(cs.ns(|| "(r.z + y)^2 - a - r.t"), &r.t)?;
-        d.mul_in_place(cs.ns(|| "((r.z + y)^2 - a - r.t) * r.t"), &r.t)?;
-        let h = b.sub(cs.ns(|| "b - r.x"), &r.x)?;
-        let i = h.square(cs.ns(|| "h^2"))?;
-        let e = i.double(cs.ns(|| "2 * i"))?.double(cs.ns(|| "4 * i"))?;
-        let j = h.mul(cs.ns(|| "h * e"), &e)?;
-        let v = r.x.mul(cs.ns(|| "r.x * e"), &e)?;
-        let ry2 = r.y.double(cs.ns(|| "r.y + r.y"))?;
-        let l1 = d.sub(cs.ns(|| "d - (r.y + r.y)"), &ry2)?;
-
-        let v2 = v.double(cs.ns(|| "v + v"))?;
-        let x = l1
-            .square(cs.ns(|| "l1^2"))?
-            .sub(cs.ns(|| "l1^2 - j"), &j)?
-            .sub(cs.ns(|| "l1^2 - j - (v + v)"), &v2)?;
-        let v_minus_x = v.sub(cs.ns(|| "v - x"), &x)?;
-        let j_ry2 = j.mul(cs.ns(|| "j * (r.y + r.y)"), &ry2)?;
-        let y = l1
-            .mul(cs.ns(|| "l1 * (v - x)"), &v_minus_x)?
-            .sub(cs.ns(|| "l1 * (v - x) - (j * (r.y + r.y)"), &j_ry2)?;
-        let mut z = r.z.add(cs.ns(|| "r.z + h"), &h)?;
-        z.square_in_place(cs.ns(|| "(r.z + h)^2"))?;
-        z.sub_in_place(cs.ns(|| "(r.z + h)^2 - r.t"), &r.t)?;
-        z.sub_in_place(cs.ns(|| "(r.z + h)^2 - r.t - i"), &i)?;
-        let t = z.square(cs.ns(|| "z^2"))?;
-
-        let r2 = G2ProjectiveExtendedGadget {
+        r: &G2ProjectiveExtendedVar<P>,
+    ) -> Result<(G2ProjectiveExtendedVar<P>, AteAdditionCoefficientsVar<P>), SynthesisError> {
+        let a = y.square()?;
+        let b = &r.t * x;
+        let d = ((&r.z + y).square()? - &a - &r.t) * &r.t;
+        let h = &b - &r.x;
+        let i = h.square()?;
+        let e = i.double()?.double()?;
+        let j = &h * &e;
+        let v = &r.x * &e;
+        let ry2 = r.y.double()?;
+        let l1 = &d - &ry2;
+
+        let x = l1.square()? - &j - &v.double()?;
+        let y = &l1 * &(&v - &x) - &j * ry2;
+        let z = (&r.z + &h).square()? - &r.t - &i;
+        let t = z.square()?;
+
+        let r2 = G2ProjectiveExtendedVar {
             x,
             y,
             z: z.clone(),
             t,
         };
-        let coeff = AteAdditionCoefficientsGadget { c_l1: l1, c_rz: z };
+        let coeff = AteAdditionCoefficientsVar { c_l1: l1, c_rz: z };
 
         Ok((r2, coeff))
     }
 
-    pub fn ate_miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        p: &G1PreparedGadget<P>,
-        q: &G2PreparedGadget<P>,
+    pub fn ate_miller_loop(
+        p: &G1PreparedVar<P>,
+        q: &G2PreparedVar<P>,
     ) -> Result<Fp6G<P>, SynthesisError> {
-        let zero = FpGadget::<P::Fp>::zero(cs.ns(|| "zero"))?;
-        let mut l1_coeff = Fp3G::<P>::new(p.x.clone(), zero.clone(), zero);
-        l1_coeff.sub_in_place(cs.ns(|| "l1_coeff"), &q.x_over_twist)?;
+        let zero = FpVar::<P::Fp>::zero();
+        let l1_coeff = Fp3Var::new(p.x.clone(), zero.clone(), zero) - &q.x_over_twist;
 
-        let mut f = Fp6G::<P>::one(cs.ns(|| "one"))?;
+        let mut f = Fp6G::<P>::one();
 
         let mut dbl_idx: usize = 0;
         let mut add_idx: usize = 0;
 
         let mut found_one = false;
 
-        for (j, bit) in BitIterator::new(P::ATE_LOOP_COUNT).enumerate() {
+        for bit in BitIterator::new(P::ATE_LOOP_COUNT) {
             // code below gets executed for all bits (EXCEPT the MSB itself) of
             // mnt6_param_p (skipping leading zeros) in MSB to LSB order
             if !found_one && bit {
@@ -172,173 +108,109 @@ impl PairingGadget {
                 continue;
             }
 
-            let mut cs = cs.ns(|| format!("bit {}", j));
-
             let dc = &q.double_coefficients[dbl_idx];
             dbl_idx += 1;
 
-            let c_j_x_twist = dc.c_j.mul(cs.ns(|| "dc.c_j * p.x_twist"), &p.x_twist)?;
-            let c0 = dc.c_l.sub(cs.ns(|| "-dc.c_4c + dc.c_l"), &dc.c_4c)?.sub(
-                cs.ns(|| "-dc.c_4c - (dc.c_j * p.x_twist) + dc.c_l"),
-                &c_j_x_twist,
-            )?;
-            let c1 = dc.c_h.mul(cs.ns(|| "dc.c_h * p.y_twist"), &p.y_twist)?;
-            let g_rr_at_p = Fp6G::<P>::new(c0, c1);
+            let g_rr_at_p = Fp6Var::new(
+                &dc.c_l - &dc.c_4c - &dc.c_j * &p.x_twist,
+                &dc.c_h * &p.y_twist,
+            );
 
-            f = f
-                .square(cs.ns(|| "f^2"))?
-                .mul(cs.ns(|| "f^2 * g_rr_at_p"), &g_rr_at_p)?;
+            f = f.square()? * &g_rr_at_p;
 
             if bit {
                 let ac = &q.addition_coefficients[add_idx];
                 add_idx += 1;
 
-                let l1_coeff_c_l1 = l1_coeff.mul(cs.ns(|| "l1_coeff * ac.c_l1"), &ac.c_l1)?;
-                let g_rq_at_p = Fp6G::<P>::new(
-                    ac.c_rz.mul(cs.ns(|| "ac.c_rz * p.y_twist"), &p.y_twist)?,
-                    q.y_over_twist
-                        .mul(cs.ns(|| "q.y_over_twist * ac.c_rz"), &ac.c_rz)?
-                        .add(
-                            cs.ns(|| "q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1)"),
-                            &l1_coeff_c_l1,
-                        )?
-                        .negate(cs.ns(|| "-(q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1))"))?,
+                let g_rq_at_p = Fp6Var::new(
+                    &ac.c_rz * &p.y_twist,
+                    (&q.y_over_twist * &ac.c_rz + &(&l1_coeff * &ac.c_l1)).negate()?,
                 );
-                f.mul_in_place(cs.ns(|| "f *= g_rq_at_p"), &g_rq_at_p)?;
+                f *= &g_rq_at_p;
             }
         }
 
         if P::ATE_IS_LOOP_COUNT_NEG {
             let ac = &q.addition_coefficients[add_idx];
 
-            let l1_coeff_c_l1 = l1_coeff.mul(cs.ns(|| "l1_coeff * ac.c_l1"), &ac.c_l1)?;
-            let g_rnegr_at_p = Fp6G::<P>::new(
-                ac.c_rz.mul(cs.ns(|| "ac.c_rz * p.y_twist"), &p.y_twist)?,
-                q.y_over_twist
-                    .mul(cs.ns(|| "q.y_over_twist * ac.c_rz"), &ac.c_rz)?
-                    .add(
-                        cs.ns(|| "q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1)"),
-                        &l1_coeff_c_l1,
-                    )?
-                    .negate(cs.ns(|| "-(q.y_over_twist * ac.c_rz + (l1_coeff * ac.c_l1))"))?,
+            let g_rnegr_at_p = Fp6Var::new(
+                &ac.c_rz * &p.y_twist,
+                (&q.y_over_twist * &ac.c_rz + &(l1_coeff * &ac.c_l1)).negate()?,
             );
-            f = f
-                .mul(cs.ns(|| "f * g_rnegr_at_p"), &g_rnegr_at_p)?
-                .inverse(cs.ns(|| "inverse f"))?;
+            f = (f * &g_rnegr_at_p).inverse()?;
         }
 
         Ok(f)
     }
 
-    pub fn final_exponentiation<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        value: &Fp6G<P>,
-    ) -> Result<GTGadget<P>, SynthesisError> {
-        let value_inv = value.inverse(cs.ns(|| "value inverse"))?;
-        let value_to_first_chunk = Self::final_exponentiation_first_chunk(
-            cs.ns(|| "value_to_first_chunk"),
-            value,
-            &value_inv,
-        )?;
-        let value_inv_to_first_chunk = Self::final_exponentiation_first_chunk(
-            cs.ns(|| "value_inv_to_first_chunk"),
-            &value_inv,
-            value,
-        )?;
-        Self::final_exponentiation_last_chunk(
-            cs.ns(|| "final_exp_last_chunk"),
-            &value_to_first_chunk,
-            &value_inv_to_first_chunk,
-        )
+    pub fn final_exponentiation(value: &Fp6G<P>) -> Result<GTVar<P>, SynthesisError> {
+        let value_inv = value.inverse()?;
+        let value_to_first_chunk = Self::final_exponentiation_first_chunk(value, &value_inv)?;
+        let value_inv_to_first_chunk = Self::final_exponentiation_first_chunk(&value_inv, value)?;
+        Self::final_exponentiation_last_chunk(&value_to_first_chunk, &value_inv_to_first_chunk)
     }
 
-    fn final_exponentiation_first_chunk<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
+    fn final_exponentiation_first_chunk(
         elt: &Fp6G<P>,
         elt_inv: &Fp6G<P>,
     ) -> Result<Fp6G<P>, SynthesisError> {
         // (q^3-1)*(q+1)
 
         // elt_q3 = elt^(q^3)
-        let mut elt_q3 = elt.clone();
-        elt_q3.frobenius_map_in_place(cs.ns(|| "frobenius 3"), 3)?;
+        let elt_q3 = elt.unitary_inverse()?;
         // elt_q3_over_elt = elt^(q^3-1)
-        let elt_q3_over_elt = elt_q3.mul(cs.ns(|| "elt_q3 * elt_inv"), elt_inv)?;
+        let elt_q3_over_elt = elt_q3 * elt_inv;
         // alpha = elt^((q^3-1) * q)
-        let mut alpha = elt_q3_over_elt.clone();
-        alpha.frobenius_map_in_place(cs.ns(|| "frobenius 1"), 1)?;
+        let alpha = elt_q3_over_elt.frobenius_map(1)?;
         // beta = elt^((q^3-1)*(q+1)
-        alpha.mul(cs.ns(|| "alpha * elt_q3_over_elt"), &elt_q3_over_elt)
+        Ok(alpha * &elt_q3_over_elt)
     }
 
-    fn final_exponentiation_last_chunk<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
+    fn final_exponentiation_last_chunk(
         elt: &Fp6G<P>,
         elt_inv: &Fp6G<P>,
     ) -> Result<Fp6G<P>, SynthesisError> {
-        let elt_clone = elt.clone();
-        let elt_inv_clone = elt_inv.clone();
-
-        let mut elt_q = elt.clone();
-        elt_q.frobenius_map_in_place(cs.ns(|| "frobenius 1"), 1)?;
+        let elt_q = elt.frobenius_map(1)?;
 
-        let w1_part = elt_q.cyclotomic_exp(cs.ns(|| "w1_part"), &P::FINAL_EXPONENT_LAST_CHUNK_1)?;
-        let w0_part;
-        if P::FINAL_EXPONENT_LAST_CHUNK_W0_IS_NEG {
-            w0_part = elt_inv_clone
-                .cyclotomic_exp(cs.ns(|| "w0_part"), &P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?;
+        let w1_part = elt_q.cyclotomic_exp(&P::FINAL_EXPONENT_LAST_CHUNK_1)?;
+        let w0_part = if P::FINAL_EXPONENT_LAST_CHUNK_W0_IS_NEG {
+            elt_inv.cyclotomic_exp(&P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?
         } else {
-            w0_part = elt_clone
-                .cyclotomic_exp(cs.ns(|| "w0_part"), &P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?;
-        }
+            elt.cyclotomic_exp(&P::FINAL_EXPONENT_LAST_CHUNK_ABS_OF_W0)?
+        };
 
-        w1_part.mul(cs.ns(|| "w1_part * w0_part"), &w0_part)
+        Ok(w1_part * &w0_part)
     }
 }
 
-impl<P: MNT6Parameters> PG<MNT6<P>, P::Fp> for PairingGadget<P> {
-    type G1Gadget = G1Gadget<P>;
-    type G2Gadget = G2Gadget<P>;
-    type G1PreparedGadget = G1PreparedGadget<P>;
-    type G2PreparedGadget = G2PreparedGadget<P>;
-    type GTGadget = GTGadget<P>;
-
-    fn miller_loop<CS: ConstraintSystem<P::Fp>>(
-        mut cs: CS,
-        ps: &[Self::G1PreparedGadget],
-        qs: &[Self::G2PreparedGadget],
-    ) -> Result<Self::GTGadget, SynthesisError> {
-        let mut result = Fp6G::<P>::one(cs.ns(|| "one"))?;
-        for (i, (p, q)) in ps.iter().zip(qs.iter()).enumerate() {
-            let miller =
-                Self::ate_miller_loop(cs.ns(|| format!("ate miller loop iteration {}", i)), p, q)?;
-            result.mul_in_place(
-                cs.ns(|| format!("mul ate miller loop iteration {}", i)),
-                &miller,
-            )?;
+impl<P: MNT6Parameters> PG<MNT6<P>, P::Fp> for PairingVar<P> {
+    type G1Var = G1Var<P>;
+    type G2Var = G2Var<P>;
+    type G1PreparedVar = G1PreparedVar<P>;
+    type G2PreparedVar = G2PreparedVar<P>;
+    type GTVar = GTVar<P>;
+
+    fn miller_loop(
+        ps: &[Self::G1PreparedVar],
+        qs: &[Self::G2PreparedVar],
+    ) -> Result<Self::GTVar, SynthesisError> {
+        let mut result = Fp6G::<P>::one();
+        for (p, q) in ps.iter().zip(qs) {
+            result *= Self::ate_miller_loop(p, q)?;
         }
 
         Ok(result)
     }
 
-    fn final_exponentiation<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        r: &Self::GTGadget,
-    ) -> Result<Self::GTGadget, SynthesisError> {
-        Self::final_exponentiation(cs, r)
+    fn final_exponentiation(r: &Self::GTVar) -> Result<Self::GTVar, SynthesisError> {
+        Self::final_exponentiation(r)
     }
 
-    fn prepare_g1<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        p: &Self::G1Gadget,
-    ) -> Result<Self::G1PreparedGadget, SynthesisError> {
-        Self::G1PreparedGadget::from_affine(cs, p)
+    fn prepare_g1(p: &Self::G1Var) -> Result<Self::G1PreparedVar, SynthesisError> {
+        Self::G1PreparedVar::from_group_var(p)
     }
 
-    fn prepare_g2<CS: ConstraintSystem<P::Fp>>(
-        cs: CS,
-        q: &Self::G2Gadget,
-    ) -> Result<Self::G2PreparedGadget, SynthesisError> {
-        Self::G2PreparedGadget::from_affine(cs, q)
+    fn prepare_g2(q: &Self::G2Var) -> Result<Self::G2PreparedVar, SynthesisError> {
+        Self::G2PreparedVar::from_group_var(q)
     }
 }

r1cs-std/src/pairing/mod.rs

@@ -1,82 +1,78 @@
 use crate::prelude::*;
 use algebra::{Field, PairingEngine};
 use core::fmt::Debug;
-use r1cs_core::{ConstraintSystem, SynthesisError};
+use r1cs_core::SynthesisError;
 
 pub mod bls12;
 pub mod mnt4;
 pub mod mnt6;
 
-pub trait PairingGadget<PairingE: PairingEngine, ConstraintF: Field> {
-    type G1Gadget: GroupGadget<PairingE::G1Projective, ConstraintF>;
-    type G2Gadget: GroupGadget<PairingE::G2Projective, ConstraintF>;
-    type G1PreparedGadget: AllocGadget<PairingE::G1Prepared, ConstraintF>
-        + ToBytesGadget<ConstraintF>
+pub trait PairingVar<E: PairingEngine, ConstraintF: Field = <E as PairingEngine>::Fq> {
+    type G1Var: CurveVar<E::G1Projective, ConstraintF>
+        + AllocVar<E::G1Projective, ConstraintF>
+        + AllocVar<E::G1Affine, ConstraintF>;
+    type G2Var: CurveVar<E::G2Projective, ConstraintF>
+        + AllocVar<E::G2Projective, ConstraintF>
+        + AllocVar<E::G2Affine, ConstraintF>;
+
+    type GTVar: FieldVar<E::Fqk, ConstraintF>;
+
+    type G1PreparedVar: ToBytesGadget<ConstraintF>
+        + AllocVar<E::G1Prepared, ConstraintF>
         + Clone
         + Debug;
-    type G2PreparedGadget: AllocGadget<PairingE::G2Prepared, ConstraintF>
-        + ToBytesGadget<ConstraintF>
+    type G2PreparedVar: ToBytesGadget<ConstraintF>
+        + AllocVar<E::G2Prepared, ConstraintF>
         + Clone
         + Debug;
-    type GTGadget: FieldGadget<PairingE::Fqk, ConstraintF> + Clone;
-
-    fn miller_loop<CS: ConstraintSystem<ConstraintF>>(
-        cs: CS,
-        p: &[Self::G1PreparedGadget],
-        q: &[Self::G2PreparedGadget],
-    ) -> Result<Self::GTGadget, SynthesisError>;
-
-    fn final_exponentiation<CS: ConstraintSystem<ConstraintF>>(
-        cs: CS,
-        p: &Self::GTGadget,
-    ) -> Result<Self::GTGadget, SynthesisError>;
-
-    fn pairing<CS: ConstraintSystem<ConstraintF>>(
-        mut cs: CS,
-        p: Self::G1PreparedGadget,
-        q: Self::G2PreparedGadget,
-    ) -> Result<Self::GTGadget, SynthesisError> {
-        let tmp = Self::miller_loop(cs.ns(|| "miller loop"), &[p], &[q])?;
-        Self::final_exponentiation(cs.ns(|| "final_exp"), &tmp)
+
+    fn miller_loop(
+        p: &[Self::G1PreparedVar],
+        q: &[Self::G2PreparedVar],
+    ) -> Result<Self::GTVar, SynthesisError>;
+
+    fn final_exponentiation(p: &Self::GTVar) -> Result<Self::GTVar, SynthesisError>;
+
+    fn pairing(
+        p: Self::G1PreparedVar,
+        q: Self::G2PreparedVar,
+    ) -> Result<Self::GTVar, SynthesisError> {
+        let tmp = Self::miller_loop(&[p], &[q])?;
+        Self::final_exponentiation(&tmp)
     }
 
     /// Computes a product of pairings.
     #[must_use]
-    fn product_of_pairings<CS: ConstraintSystem<ConstraintF>>(
-        mut cs: CS,
-        p: &[Self::G1PreparedGadget],
-        q: &[Self::G2PreparedGadget],
-    ) -> Result<Self::GTGadget, SynthesisError> {
-        let miller_result = Self::miller_loop(&mut cs.ns(|| "Miller loop"), p, q)?;
-        Self::final_exponentiation(&mut cs.ns(|| "Final Exp"), &miller_result)
+    fn product_of_pairings(
+        p: &[Self::G1PreparedVar],
+        q: &[Self::G2PreparedVar],
+    ) -> Result<Self::GTVar, SynthesisError> {
+        let miller_result = Self::miller_loop(p, q)?;
+        Self::final_exponentiation(&miller_result)
     }
 
-    fn prepare_g1<CS: ConstraintSystem<ConstraintF>>(
-        cs: CS,
-        q: &Self::G1Gadget,
-    ) -> Result<Self::G1PreparedGadget, SynthesisError>;
+    fn prepare_g1(q: &Self::G1Var) -> Result<Self::G1PreparedVar, SynthesisError>;
 
-    fn prepare_g2<CS: ConstraintSystem<ConstraintF>>(
-        cs: CS,
-        q: &Self::G2Gadget,
-    ) -> Result<Self::G2PreparedGadget, SynthesisError>;
+    fn prepare_g2(q: &Self::G2Var) -> Result<Self::G2PreparedVar, SynthesisError>;
 }
 
 #[cfg(test)]
 pub(crate) mod tests {
-    use crate::{
-        bits::boolean::Boolean, prelude::*, test_constraint_system::TestConstraintSystem, Vec,
+    use crate::{prelude::*, Vec};
+    use algebra::{
+        test_rng, BitIterator, Field, PairingEngine, PrimeField, ProjectiveCurve, UniformRand,
     };
-    use algebra::{test_rng, BitIterator, Field, PairingEngine, PrimeField, UniformRand};
-    use r1cs_core::ConstraintSystem;
+    use r1cs_core::{ConstraintSystem, SynthesisError};
 
     #[allow(dead_code)]
-    pub(crate) fn bilinearity_test<
-        E: PairingEngine,
-        ConstraintF: Field,
-        P: PairingGadget<E, ConstraintF>,
-    >() {
-        let mut cs = TestConstraintSystem::<ConstraintF>::new();
+    pub(crate) fn bilinearity_test<E: PairingEngine, P: PairingVar<E>>(
+    ) -> Result<(), SynthesisError>
+    where
+        for<'a> &'a P::G1Var: GroupOpsBounds<'a, E::G1Projective, P::G1Var>,
+        for<'a> &'a P::G2Var: GroupOpsBounds<'a, E::G2Projective, P::G2Var>,
+        for<'a> &'a P::GTVar: FieldOpsBounds<'a, E::Fqk, P::GTVar>,
+    {
+        let cs = ConstraintSystem::<E::Fq>::new_ref();
 
         let mut rng = test_rng();
         let a = E::G1Projective::rand(&mut rng);
@@ -88,25 +84,42 @@ pub(crate) mod tests {
         let mut sb = b;
         sb *= s;
 
-        let a_g = P::G1Gadget::alloc(&mut cs.ns(|| "a"), || Ok(a)).unwrap();
-        let b_g = P::G2Gadget::alloc(&mut cs.ns(|| "b"), || Ok(b)).unwrap();
-        let sa_g = P::G1Gadget::alloc(&mut cs.ns(|| "sa"), || Ok(sa)).unwrap();
-        let sb_g = P::G2Gadget::alloc(&mut cs.ns(|| "sb"), || Ok(sb)).unwrap();
-
-        let a_prep_g = P::prepare_g1(&mut cs.ns(|| "a_prep"), &a_g).unwrap();
-        let b_prep_g = P::prepare_g2(&mut cs.ns(|| "b_prep"), &b_g).unwrap();
+        let a_g = P::G1Var::new_witness(cs.ns("a"), || Ok(a.into_affine()))?;
+        let b_g = P::G2Var::new_witness(cs.ns("b"), || Ok(b.into_affine()))?;
+        let sa_g = P::G1Var::new_witness(cs.ns("sa"), || Ok(sa.into_affine()))?;
+        let sb_g = P::G2Var::new_witness(cs.ns("sb"), || Ok(sb.into_affine()))?;
+
+        let mut preparation_num_constraints = cs.num_constraints();
+        let a_prep_g = P::prepare_g1(&a_g)?;
+        let b_prep_g = P::prepare_g2(&b_g)?;
+        preparation_num_constraints = cs.num_constraints() - preparation_num_constraints;
+        println!(
+            "Preparation num constraints: {}",
+            preparation_num_constraints
+        );
 
-        let sa_prep_g = P::prepare_g1(&mut cs.ns(|| "sa_prep"), &sa_g).unwrap();
-        let sb_prep_g = P::prepare_g2(&mut cs.ns(|| "sb_prep"), &sb_g).unwrap();
+        let sa_prep_g = P::prepare_g1(&sa_g)?;
+        let sb_prep_g = P::prepare_g2(&sb_g)?;
 
         let (ans1_g, ans1_n) = {
-            let ans_g = P::pairing(cs.ns(|| "pair(sa, b)"), sa_prep_g, b_prep_g.clone()).unwrap();
+            let ml_constraints = cs.num_constraints();
+            let ml_g = P::miller_loop(&[sa_prep_g], &[b_prep_g.clone()])?;
+            println!(
+                "ML num constraints: {}",
+                cs.num_constraints() - ml_constraints
+            );
+            let fe_constraints = cs.num_constraints();
+            let ans_g = P::final_exponentiation(&ml_g)?;
+            println!(
+                "FE num constraints: {}",
+                cs.num_constraints() - fe_constraints
+            );
             let ans_n = E::pairing(sa, b);
             (ans_g, ans_n)
         };
 
         let (ans2_g, ans2_n) = {
-            let ans_g = P::pairing(cs.ns(|| "pair(a, sb)"), a_prep_g.clone(), sb_prep_g).unwrap();
+            let ans_g = P::pairing(a_prep_g.clone(), sb_prep_g)?;
             let ans_n = E::pairing(a, sb);
             (ans_g, ans_n)
         };
@@ -116,47 +129,32 @@ pub(crate) mod tests {
                 .map(Boolean::constant)
                 .collect::<Vec<_>>();
 
-            let mut ans_g = P::pairing(cs.ns(|| "pair(a, b)"), a_prep_g, b_prep_g).unwrap();
+            let mut ans_g = P::pairing(a_prep_g, b_prep_g)?;
             let mut ans_n = E::pairing(a, b);
             ans_n = ans_n.pow(s.into_repr());
-            ans_g = ans_g.pow(cs.ns(|| "pow"), &s_iter).unwrap();
+            ans_g = ans_g.pow(&s_iter)?;
 
             (ans_g, ans_n)
         };
 
-        assert_eq!(ans1_n, ans2_n, "Failed ans1_native == ans2_native");
-        assert_eq!(ans2_n, ans3_n, "Failed ans2_native == ans3_native");
-        assert_eq!(
-            ans1_g.get_value(),
-            ans3_g.get_value(),
-            "Failed ans1 == ans3"
-        );
-        assert_eq!(
-            ans1_g.get_value(),
-            ans2_g.get_value(),
-            "Failed ans1 == ans2"
-        );
-        assert_eq!(
-            ans2_g.get_value(),
-            ans3_g.get_value(),
-            "Failed ans2 == ans3"
-        );
+        ans1_g.enforce_equal(&ans2_g)?;
+        ans2_g.enforce_equal(&ans3_g)?;
 
-        ans1_g
-            .enforce_equal(&mut cs.ns(|| "ans1 == ans2?"), &ans2_g)
-            .unwrap();
-        ans2_g
-            .enforce_equal(&mut cs.ns(|| "ans2 == ans3?"), &ans3_g)
-            .unwrap();
+        assert_eq!(ans1_g.value()?, ans1_n, "Failed native test 1");
+        assert_eq!(ans2_g.value()?, ans2_n, "Failed native test 2");
+        assert_eq!(ans3_g.value()?, ans3_n, "Failed native test 3");
 
-        assert_eq!(ans1_g.get_value().unwrap(), ans1_n, "Failed native test 1");
-        assert_eq!(ans2_g.get_value().unwrap(), ans2_n, "Failed native test 2");
-        assert_eq!(ans3_g.get_value().unwrap(), ans3_n, "Failed native test 3");
+        assert_eq!(ans1_n, ans2_n, "Failed ans1_native == ans2_native");
+        assert_eq!(ans2_n, ans3_n, "Failed ans2_native == ans3_native");
+        assert_eq!(ans1_g.value()?, ans3_g.value()?, "Failed ans1 == ans3");
+        assert_eq!(ans1_g.value()?, ans2_g.value()?, "Failed ans1 == ans2");
+        assert_eq!(ans2_g.value()?, ans3_g.value()?, "Failed ans2 == ans3");
 
-        if !cs.is_satisfied() {
+        if !cs.is_satisfied().unwrap() {
             println!("Unsatisfied: {:?}", cs.which_is_unsatisfied());
         }
 
-        assert!(cs.is_satisfied(), "cs is not satisfied");
+        assert!(cs.is_satisfied().unwrap(), "cs is not satisfied");
+        Ok(())
     }
 }