@@ -98,6 +98,13 @@ toolchain: stable
           target: thumbv6m-none-eabi
           override: true
 
+      - name: Install Rust ARM64 (${{ matrix.rust }})
+        uses: actions-rs/toolchain@v1
+        with:
+          toolchain: stable
+          target: aarch64-unknown-none
+          override: true
+
       - uses: actions/cache@v2
         with:
           path: |
@@ -130,8 +137,8 @@
       - name: r1cs-std
         run: |
           cd r1cs-std
-          cargo build -p r1cs-std --no-default-features --target thumbv6m-none-eabi
-          cargo check --examples -p r1cs-std --no-default-features --target thumbv6m-none-eabi
+          cargo build -p r1cs-std --no-default-features --target aarch64-unknown-none
+          cargo check --examples -p r1cs-std --no-default-features --target aarch64-unknown-none
           cd ..
 
       - name: ff-fft
@@ -158,6 +165,6 @@
       - name: crypto-primitives
         run: |
           cd crypto-primitives
-          cargo build -p crypto-primitives --no-default-features --target thumbv6m-none-eabi
-          cargo check --examples -p crypto-primitives --no-default-features --target thumbv6m-none-eabi
+          cargo build -p crypto-primitives --no-default-features --target aarch64-unknown-none
+          cargo check --examples -p crypto-primitives --no-default-features --target aarch64-unknown-none
           cd ..

@@ -38,6 +38,7 @@
 rand = { version = "0.7", default-features = false }
 rayon = { version = "1.0", optional = true }
 derivative = { version = "2.0", features = ["use_core"] }
+tracing = { version = "0.1", default-features = false, features = [ "attributes" ] }
 
 [features]
 default = ["std", "r1cs"]

@@ -24,6 +24,7 @@ type OutputVar = OutputVar<F>;
     type ParametersVar = ParametersVar;
     type RandomnessVar = RandomnessVar<F>;
 
+    #[tracing::instrument(target = "r1cs", skip(input, r))]
     fn commit(
         _: &Self::ParametersVar,
         input: &[UInt8<F>],
@@ -43,6 +44,7 @@ }
 }
 
 impl<ConstraintF: Field> AllocVar<(), ConstraintF> for ParametersVar {
+    #[tracing::instrument(target = "r1cs", skip(_cs, _f))]
     fn new_variable<T: Borrow<()>>(
         _cs: impl Into<Namespace<ConstraintF>>,
         _f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -53,6 +55,7 @@ }
 }
 
 impl<ConstraintF: PrimeField> AllocVar<[u8; 32], ConstraintF> for RandomnessVar<ConstraintF> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<[u8; 32]>>(
         cs: impl Into<Namespace<ConstraintF>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -111,7 +114,7 @@ let randomness_var = RandomnessVar(randomness_var);
 
         let parameters_var =
             <TestCOMMGadget as CommitmentGadget<TestCOMM, Fr>>::ParametersVar::new_witness(
-                cs.ns("gadget_parameters"),
+                r1cs_core::ns!(cs, "gadget_parameters"),
                 || Ok(&parameters),
             )
             .unwrap();

@@ -53,6 +53,7 @@ type OutputVar = GG;
     type ParametersVar = ParametersVar<C, GG>;
     type RandomnessVar = RandomnessVar<ConstraintF<C>>;
 
+    #[tracing::instrument(target = "r1cs", skip(parameters, r))]
     fn commit(
         parameters: &Self::ParametersVar,
         input: &[UInt8<ConstraintF<C>>],
@@ -183,13 +184,13 @@ }
 
         let randomness_var =
             <TestCOMMGadget as CommitmentGadget<TestCOMM, Fq>>::RandomnessVar::new_witness(
-                cs.ns("gadget_randomness"),
+                r1cs_core::ns!(cs, "gadget_randomness"),
                 || Ok(&randomness),
             )
             .unwrap();
         let parameters_var =
             <TestCOMMGadget as CommitmentGadget<TestCOMM, Fq>>::ParametersVar::new_witness(
-                cs.ns("gadget_parameters"),
+                r1cs_core::ns!(cs, "gadget_parameters"),
                 || Ok(&parameters),
             )
             .unwrap();

@@ -51,6 +51,7 @@ {
     type OutputVar = AffineVar<P, F>;
     type ParametersVar = ParametersVar<P, W>;
 
+    #[tracing::instrument(target = "r1cs", skip(parameters, input))]
     fn evaluate(
         parameters: &Self::ParametersVar,
         input: &[UInt8<ConstraintF<P>>],
@@ -91,6 +92,7 @@ where
     P: TEModelParameters,
     W: Window,
 {
+    #[tracing::instrument(target = "r1cs", skip(_cs, f))]
     fn new_variable<T: Borrow<Parameters<P>>>(
         _cs: impl Into<Namespace<ConstraintF<P>>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -158,7 +160,7 @@ let primitive_result = TestCRH::evaluate(&parameters, &input).unwrap();
 
         let parameters_var =
             <TestCRHGadget as FixedLengthCRHGadget<TestCRH, Fr>>::ParametersVar::new_witness(
-                cs.ns("parameters_var"),
+                r1cs_core::ns!(cs, "parameters_var"),
                 || Ok(&parameters),
             )
             .unwrap();

@@ -87,6 +87,7 @@ {
     type OutputVar = IG::OutputVar;
     type ParametersVar = ped_constraints::CRHParametersVar<C, GG>;
 
+    #[tracing::instrument(target = "r1cs", skip(parameters, input))]
     fn evaluate(
         parameters: &Self::ParametersVar,
         input: &[UInt8<ConstraintF<C>>],

@@ -45,6 +45,7 @@ {
     type OutputVar = GG;
     type ParametersVar = CRHParametersVar<C, GG>;
 
+    #[tracing::instrument(target = "r1cs", skip(parameters, input))]
     fn evaluate(
         parameters: &Self::ParametersVar,
         input: &[UInt8<ConstraintF<C>>],
@@ -78,6 +79,7 @@ C: ProjectiveCurve,
     GG: CurveVar<C, ConstraintF<C>>,
     for<'a> &'a GG: GroupOpsBounds<'a, C, GG>,
 {
+    #[tracing::instrument(target = "r1cs", skip(_cs, f))]
     fn new_variable<T: Borrow<Parameters<C>>>(
         _cs: impl Into<Namespace<ConstraintF<C>>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -138,7 +140,8 @@ let parameters = TestCRH::setup(rng).unwrap();
         let primitive_result = TestCRH::evaluate(&parameters, &input).unwrap();
 
         let parameters_var =
-            CRHParametersVar::new_constant(cs.ns("CRH Parameters"), &parameters).unwrap();
+            CRHParametersVar::new_constant(r1cs_core::ns!(cs, "CRH Parameters"), &parameters)
+                .unwrap();
 
         let result_var = TestCRHGadget::evaluate(&parameters_var, &input_var).unwrap();
 

@@ -25,6 +25,7 @@ ConstraintF: Field,
     CRHGadget: FixedLengthCRHGadget<P::H, ConstraintF>,
     <CRHGadget::OutputVar as R1CSVar<ConstraintF>>::Value: PartialEq,
 {
+    #[tracing::instrument(target = "r1cs", skip(self, parameters, root, leaf))]
     pub fn check_membership(
         &self,
         parameters: &CRHGadget::ParametersVar,
@@ -39,7 +40,7 @@ let leaf_hash = CRHGadget::evaluate(parameters, &leaf_bits)?;
         let cs = leaf_hash.cs().or(root.cs()).unwrap();
 
         // Check if leaf is one of the bottom-most siblings.
-        let leaf_is_left = Boolean::new_witness(cs.ns("leaf_is_left"), || {
+        let leaf_is_left = Boolean::new_witness(r1cs_core::ns!(cs, "leaf_is_left"), || {
             Ok(leaf_hash.value()?.eq(&self.path[0].0.value()?))
         })?;
 
@@ -48,24 +49,20 @@ leaf_hash.is_eq(&leaf_is_left.select(&self.path[0].0, &self.path[0].1)?)?;
 
         // Check levels between leaf level and root.
         let mut previous_hash = leaf_hash;
-        let mut i = 0;
         for &(ref left_hash, ref right_hash) in &self.path {
             // Check if the previous_hash matches the correct current hash.
-            let previous_is_left = Boolean::new_witness(cs.ns("previous_is_left"), || {
-                Ok(previous_hash.value()?.eq(&left_hash.value()?))
-            })?;
+            let previous_is_left =
+                Boolean::new_witness(r1cs_core::ns!(cs, "previous_is_left"), || {
+                    Ok(previous_hash.value()?.eq(&left_hash.value()?))
+                })?;
 
-            let ns = cs.ns(format!(
-                "enforcing that inner hash is correct at i-th level{}",
-                i
-            ));
+            let ns = r1cs_core::ns!(cs, "enforcing that inner hash is correct");
             let equality_cmp = previous_is_left.select(left_hash, right_hash)?;
             result = result.and(&previous_hash.is_eq(&equality_cmp)?)?;
             drop(ns);
 
             previous_hash =
                 hash_inner_node::<P::H, CRHGadget, ConstraintF>(parameters, left_hash, right_hash)?;
-            i += 1;
         }
 
         result.and(&root.is_eq(&previous_hash)?)
@@ -106,8 +103,16 @@ let cs = ns.cs();
         f().and_then(|val| {
             let mut path = Vec::new();
             for &(ref l, ref r) in val.borrow().path.iter() {
-                let l_hash = HGadget::OutputVar::new_variable(cs.ns("l_child"), || Ok(l), mode)?;
-                let r_hash = HGadget::OutputVar::new_variable(cs.ns("r_child"), || Ok(r), mode)?;
+                let l_hash = HGadget::OutputVar::new_variable(
+                    r1cs_core::ns!(cs, "l_child"),
+                    || Ok(l),
+                    mode,
+                )?;
+                let r_hash = HGadget::OutputVar::new_variable(
+                    r1cs_core::ns!(cs, "r_child"),
+                    || Ok(r),
+                    mode,
+                )?;
                 path.push((l_hash, r_hash));
             }
             Ok(PathVar { path })
@@ -157,15 +162,14 @@
         let crh_parameters = H::setup(&mut rng).unwrap();
         let tree = JubJubMerkleTree::new(crh_parameters.clone(), leaves).unwrap();
         let root = tree.root();
-        let mut satisfied = true;
+        let cs = ConstraintSystem::<Fq>::new_ref();
         for (i, leaf) in leaves.iter().enumerate() {
-            let cs = ConstraintSystem::<Fq>::new_ref();
             let proof = tree.generate_proof(i, &leaf).unwrap();
             assert!(proof.verify(&crh_parameters, &root, &leaf).unwrap());
 
             // Allocate Merkle Tree Root
             let root = <HG as FixedLengthCRHGadget<H, _>>::OutputVar::new_witness(
-                cs.ns("new_digest"),
+                r1cs_core::ns!(cs, "new_digest"),
                 || {
                     if use_bad_root {
                         Ok(<H as FixedLengthCRH>::Output::default())
@@ -181,7 +185,7 @@ println!("constraints from digest: {}", constraints_from_digest);
 
             // Allocate Parameters for CRH
             let crh_parameters = <HG as FixedLengthCRHGadget<H, Fq>>::ParametersVar::new_constant(
-                cs.ns("new_parameter"),
+                r1cs_core::ns!(cs, "new_parameter"),
                 &crh_parameters,
             )
             .unwrap();
@@ -200,7 +204,9 @@ cs.num_constraints() - constraints_from_parameters - constraints_from_digest;
             println!("constraints from leaf: {}", constraints_from_leaf);
 
             // Allocate Merkle Tree Path
-            let cw = PathVar::<_, HG, _>::new_witness(cs.ns("new_witness"), || Ok(&proof)).unwrap();
+            let cw =
+                PathVar::<_, HG, _>::new_witness(r1cs_core::ns!(cs, "new_witness"), || Ok(&proof))
+                    .unwrap();
             for (i, (l, r)) in cw.path.iter().enumerate() {
                 assert_eq!(l.value().unwrap(), proof.path[i].0);
                 assert_eq!(r.value().unwrap(), proof.path[i].1);
@@ -216,13 +222,6 @@ cw.check_membership(&crh_parameters, &root, &leaf_g)
                 .unwrap()
                 .enforce_equal(&Boolean::TRUE)
                 .unwrap();
-            if !cs.is_satisfied().unwrap() {
-                satisfied = false;
-                println!(
-                    "Unsatisfied constraint: {}",
-                    cs.which_is_unsatisfied().unwrap()
-                );
-            }
             let setup_constraints = constraints_from_leaf
                 + constraints_from_digest
                 + constraints_from_parameters
@@ -233,7 +232,7 @@ cs.num_constraints() - setup_constraints
             );
         }
 
-        assert!(satisfied);
+        assert!(cs.is_satisfied().unwrap());
     }
 
     #[test]

@@ -15,6 +15,7 @@ /// Optionally allocates `N::Proof` in `cs` without performing
     /// subgroup checks.
     ///
     /// The default implementation doesn't omit these checks.
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_proof_unchecked<T: Borrow<N::Proof>>(
         cs: impl Into<Namespace<ConstraintF>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -27,6 +28,7 @@ /// Optionally allocates `N::VerificationParameters` in `cs`
     /// without performing subgroup checks.
     ///
     /// The default implementation doesn't omit these checks.
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_verification_key_unchecked<T: Borrow<N::VerificationParameters>>(
         cs: impl Into<Namespace<ConstraintF>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,

@@ -32,6 +32,7 @@ pub query: Vec<P::G1Var>,
 }
 
 impl<E: PairingEngine, P: PairingVar<E>> VerifyingKeyVar<E, P> {
+    #[tracing::instrument(target = "r1cs", skip(self))]
     pub fn prepare(&self) -> Result<PreparedVerifyingKeyVar<E, P>, SynthesisError> {
         let g_alpha_pc = P::prepare_g1(&self.g_alpha_g1)?;
         let h_beta_pc = P::prepare_g2(&self.h_beta_g2)?;
@@ -89,6 +90,7 @@ type ProofVar = ProofVar<E, P>;
 
     /// Allocates `N::Proof` in `cs` without performing
     /// subgroup checks.
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_proof_unchecked<T: Borrow<Proof<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -99,17 +101,17 @@ let cs = ns.cs();
         f().and_then(|proof| {
             let proof = proof.borrow();
             let a = CurveVar::new_variable_omit_prime_order_check(
-                cs.ns("Proof.a"),
+                r1cs_core::ns!(cs, "Proof.a"),
                 || Ok(proof.a.into_projective()),
                 mode,
             )?;
             let b = CurveVar::new_variable_omit_prime_order_check(
-                cs.ns("Proof.b"),
+                r1cs_core::ns!(cs, "Proof.b"),
                 || Ok(proof.b.into_projective()),
                 mode,
             )?;
             let c = CurveVar::new_variable_omit_prime_order_check(
-                cs.ns("Proof.c"),
+                r1cs_core::ns!(cs, "Proof.c"),
                 || Ok(proof.c.into_projective()),
                 mode,
             )?;
@@ -119,6 +121,7 @@ }
 
     /// Allocates `N::Proof` in `cs` without performing
     /// subgroup checks.
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_verification_key_unchecked<T: Borrow<VerifyingKey<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -129,27 +132,27 @@ let cs = ns.cs();
         f().and_then(|vk| {
             let vk = vk.borrow();
             let g_alpha_g1 = P::G1Var::new_variable_omit_prime_order_check(
-                cs.ns("g_alpha"),
+                r1cs_core::ns!(cs, "g_alpha"),
                 || Ok(vk.g_alpha_g1.into_projective()),
                 mode,
             )?;
             let h_g2 = P::G2Var::new_variable_omit_prime_order_check(
-                cs.ns("h"),
+                r1cs_core::ns!(cs, "h"),
                 || Ok(vk.h_g2.into_projective()),
                 mode,
             )?;
             let h_beta_g2 = P::G2Var::new_variable_omit_prime_order_check(
-                cs.ns("h_beta"),
+                r1cs_core::ns!(cs, "h_beta"),
                 || Ok(vk.h_beta_g2.into_projective()),
                 mode,
             )?;
             let g_gamma_g1 = P::G1Var::new_variable_omit_prime_order_check(
-                cs.ns("g_gamma"),
+                r1cs_core::ns!(cs, "g_gamma"),
                 || Ok(vk.g_gamma_g1.into_projective()),
                 mode,
             )?;
             let h_gamma_g2 = P::G2Var::new_variable_omit_prime_order_check(
-                cs.ns("h_gamma"),
+                r1cs_core::ns!(cs, "h_gamma"),
                 || Ok(vk.h_gamma_g2.into_projective()),
                 mode,
             )?;
@@ -159,7 +162,7 @@ .query
                 .iter()
                 .map(|g| {
                     P::G1Var::new_variable_omit_prime_order_check(
-                        cs.ns("g"),
+                        r1cs_core::ns!(cs, "g"),
                         || Ok(g.into_projective()),
                         mode,
                     )
@@ -176,6 +179,7 @@ })
         })
     }
 
+    #[tracing::instrument(target = "r1cs", skip(vk, input, proof))]
     fn verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
         vk: &Self::VerificationKeyVar,
         input: impl IntoIterator<Item = &'a T>,
@@ -185,6 +189,7 @@ let pvk = vk.prepare()?;
         <Self as NIZKVerifierGadget<Gm17<E, C, V>, E::Fq>>::verify_prepared(&pvk, input, proof)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(pvk, input, proof))]
     fn verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
         pvk: &Self::PreparedVerificationKeyVar,
         input: impl IntoIterator<Item = &'a T>,
@@ -263,6 +268,7 @@ P: PairingVar<E>,
     P::G1PreparedVar: AllocVar<E::G1Prepared, E::Fq>,
     P::G2PreparedVar: AllocVar<E::G2Prepared, E::Fq>,
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<PreparedVerifyingKey<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -273,21 +279,34 @@ let cs = ns.cs();
 
         f().and_then(|pvk| {
             let pvk = pvk.borrow();
-            let g_alpha = P::G1Var::new_variable(cs.ns("g_alpha"), || Ok(pvk.g_alpha), mode)?;
-            let h_beta = P::G2Var::new_variable(cs.ns("h_beta"), || Ok(pvk.h_beta), mode)?;
+            let g_alpha =
+                P::G1Var::new_variable(r1cs_core::ns!(cs, "g_alpha"), || Ok(pvk.g_alpha), mode)?;
+            let h_beta =
+                P::G2Var::new_variable(r1cs_core::ns!(cs, "h_beta"), || Ok(pvk.h_beta), mode)?;
             let g_alpha_pc = P::G1PreparedVar::new_variable(
-                cs.ns("g_alpha_pc"),
+                r1cs_core::ns!(cs, "g_alpha_pc"),
                 || Ok(pvk.g_alpha.into()),
                 mode,
             )?;
-            let h_beta_pc =
-                P::G2PreparedVar::new_variable(cs.ns("h_beta_pc"), || Ok(pvk.h_beta.into()), mode)?;
-            let g_gamma_pc =
-                P::G1PreparedVar::new_variable(cs.ns("g_gamma_pc"), || Ok(&pvk.g_gamma_pc), mode)?;
-            let h_gamma_pc =
-                P::G2PreparedVar::new_variable(cs.ns("h_gamma_pc"), || Ok(&pvk.h_gamma_pc), mode)?;
-            let h_pc = P::G2PreparedVar::new_variable(cs.ns("h_pc"), || Ok(&pvk.h_pc), mode)?;
-            let query = Vec::new_variable(cs.ns("query"), || Ok(pvk.query.clone()), mode)?;
+            let h_beta_pc = P::G2PreparedVar::new_variable(
+                r1cs_core::ns!(cs, "h_beta_pc"),
+                || Ok(pvk.h_beta.into()),
+                mode,
+            )?;
+            let g_gamma_pc = P::G1PreparedVar::new_variable(
+                r1cs_core::ns!(cs, "g_gamma_pc"),
+                || Ok(&pvk.g_gamma_pc),
+                mode,
+            )?;
+            let h_gamma_pc = P::G2PreparedVar::new_variable(
+                r1cs_core::ns!(cs, "h_gamma_pc"),
+                || Ok(&pvk.h_gamma_pc),
+                mode,
+            )?;
+            let h_pc =
+                P::G2PreparedVar::new_variable(r1cs_core::ns!(cs, "h_pc"), || Ok(&pvk.h_pc), mode)?;
+            let query =
+                Vec::new_variable(r1cs_core::ns!(cs, "query"), || Ok(pvk.query.clone()), mode)?;
 
             Ok(Self {
                 g_alpha,
@@ -309,6 +328,7 @@ E: PairingEngine,
 
     P: PairingVar<E>,
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<VerifyingKey<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -319,12 +339,17 @@ let cs = ns.cs();
 
         f().and_then(|vk| {
             let vk = vk.borrow();
-            let g_alpha_g1 = P::G1Var::new_variable(cs.ns("g_alpha"), || Ok(vk.g_alpha_g1), mode)?;
-            let h_g2 = P::G2Var::new_variable(cs.ns("h"), || Ok(vk.h_g2), mode)?;
-            let h_beta_g2 = P::G2Var::new_variable(cs.ns("h_beta"), || Ok(vk.h_beta_g2), mode)?;
-            let g_gamma_g1 = P::G1Var::new_variable(cs.ns("g_gamma"), || Ok(&vk.g_gamma_g1), mode)?;
-            let h_gamma_g2 = P::G2Var::new_variable(cs.ns("h_gamma"), || Ok(&vk.h_gamma_g2), mode)?;
-            let query = Vec::new_variable(cs.ns("query"), || Ok(vk.query.clone()), mode)?;
+            let g_alpha_g1 =
+                P::G1Var::new_variable(r1cs_core::ns!(cs, "g_alpha"), || Ok(vk.g_alpha_g1), mode)?;
+            let h_g2 = P::G2Var::new_variable(r1cs_core::ns!(cs, "h"), || Ok(vk.h_g2), mode)?;
+            let h_beta_g2 =
+                P::G2Var::new_variable(r1cs_core::ns!(cs, "h_beta"), || Ok(vk.h_beta_g2), mode)?;
+            let g_gamma_g1 =
+                P::G1Var::new_variable(r1cs_core::ns!(cs, "g_gamma"), || Ok(&vk.g_gamma_g1), mode)?;
+            let h_gamma_g2 =
+                P::G2Var::new_variable(r1cs_core::ns!(cs, "h_gamma"), || Ok(&vk.h_gamma_g2), mode)?;
+            let query =
+                Vec::new_variable(r1cs_core::ns!(cs, "query"), || Ok(vk.query.clone()), mode)?;
             Ok(Self {
                 h_g2,
                 g_alpha_g1,
@@ -344,6 +369,7 @@
     P: PairingVar<E>,
 {
     #[inline]
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<Proof<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -354,9 +380,9 @@ let cs = ns.cs();
 
         f().and_then(|proof| {
             let Proof { a, b, c } = proof.borrow().clone();
-            let a = P::G1Var::new_variable(cs.ns("a"), || Ok(a), mode)?;
-            let b = P::G2Var::new_variable(cs.ns("b"), || Ok(b), mode)?;
-            let c = P::G1Var::new_variable(cs.ns("c"), || Ok(c), mode)?;
+            let a = P::G1Var::new_variable(cs.clone(), || Ok(a), mode)?;
+            let b = P::G2Var::new_variable(cs.clone(), || Ok(b), mode)?;
+            let c = P::G1Var::new_variable(r1cs_core::ns!(cs, "c"), || Ok(c), mode)?;
             Ok(Self { a, b, c })
         })
     }
@@ -428,8 +454,7 @@ .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
                     let result_var = cs.new_witness_variable(|| {
                         result_val.ok_or(SynthesisError::AssignmentMissing)
                     })?;
-                    cs.enforce_named_constraint(
-                        format!("Enforce constraint {}", i),
+                    cs.enforce_constraint(
                         lc!() + input_1_var,
                         lc!() + input_2_var,
                         lc!() + result_var,
@@ -480,10 +505,10 @@ let inputs: Vec<_> = inputs.into_iter().map(|input| input.unwrap()).collect();
             let mut input_gadgets = Vec::new();
 
             {
-                for (i, input) in inputs.into_iter().enumerate() {
+                for input in inputs.into_iter() {
                     let input_bits: Vec<_> = BitIteratorLE::new(input.into_repr()).collect();
                     let input_bits =
-                        Vec::<Boolean<Fq>>::new_input(cs.ns(format!("Input {}", i)), || {
+                        Vec::<Boolean<Fq>>::new_input(r1cs_core::ns!(cs, "Input"), || {
                             Ok(input_bits)
                         })
                         .unwrap();
@@ -491,9 +516,11 @@ input_gadgets.push(input_bits);
                 }
             }
 
-            let vk_gadget = TestVkVar::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
+            let vk_gadget =
+                TestVkVar::new_input(r1cs_core::ns!(cs, "Vk"), || Ok(&params.vk)).unwrap();
             let proof_gadget =
-                TestProofVar::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
+                TestProofVar::new_witness(r1cs_core::ns!(cs, "Proof"), || Ok(proof.clone()))
+                    .unwrap();
             println!("Time to verify!\n\n\n\n");
             <TestVerifierGadget as NIZKVerifierGadget<TestProofSystem, Fq>>::verify(
                 &vk_gadget,
@@ -573,8 +600,7 @@ .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
                     let result_var = cs.new_witness_variable(|| {
                         result_val.ok_or(SynthesisError::AssignmentMissing)
                     })?;
-                    cs.enforce_named_constraint(
-                        format!("Enforce constraint {}", i),
+                    cs.enforce_constraint(
                         lc!() + input_1_var,
                         lc!() + input_2_var,
                         lc!() + result_var,
@@ -624,7 +650,8 @@ })
                     .collect::<Vec<_>>();
 
                 // Allocate this byte array as input packed into field elements.
-                let input_bytes = UInt8::new_input_vec(cs.ns("Input"), &input_bytes[..])?;
+                let input_bytes =
+                    UInt8::new_input_vec(r1cs_core::ns!(cs, "Input"), &input_bytes[..])?;
                 // 40 byte
                 let element_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 8;
                 input_gadgets = input_bytes
@@ -638,9 +665,10 @@ })
                     .collect::<Vec<_>>();
             }
 
-            let vk_gadget = TestVkVar1::new_witness(cs.ns("Vk"), || Ok(&params.vk))?;
+            let vk_gadget = TestVkVar1::new_witness(r1cs_core::ns!(cs, "Vk"), || Ok(&params.vk))?;
             let proof_gadget =
-                TestProofVar1::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
+                TestProofVar1::new_witness(r1cs_core::ns!(cs, "Proof"), || Ok(proof.clone()))
+                    .unwrap();
             <TestVerifierGadget1 as NIZKVerifierGadget<TestProofSystem1, MNT6Fq>>::verify(
                 &vk_gadget,
                 &input_gadgets,
@@ -714,9 +742,9 @@
             {
                 let bigint_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 64;
                 let mut input_bits = Vec::new();
-                for (i, input) in inputs.into_iter().enumerate() {
+                for input in inputs.into_iter() {
                     let input_gadget =
-                        FpVar::new_input(cs.ns(format!("Input {}", i)), || Ok(input)).unwrap();
+                        FpVar::new_input(r1cs_core::ns!(cs, "Input"), || Ok(input)).unwrap();
                     let mut fp_bits = input_gadget.to_bits_le().unwrap();
 
                     // Use 320 bits per element.
@@ -741,9 +769,11 @@ }
                 // assert!(!verify_proof(&pvk, &proof, &[a]).unwrap());
             }
 
-            let vk_gadget = TestVkVar2::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
+            let vk_gadget =
+                TestVkVar2::new_input(r1cs_core::ns!(cs, "Vk"), || Ok(&params.vk)).unwrap();
             let proof_gadget =
-                TestProofVar2::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
+                TestProofVar2::new_witness(r1cs_core::ns!(cs, "Proof"), || Ok(proof.clone()))
+                    .unwrap();
             println!("Time to verify!\n\n\n\n");
             <TestVerifierGadget2 as NIZKVerifierGadget<TestProofSystem2, MNT4Fq>>::verify(
                 &vk_gadget,

@@ -83,6 +83,7 @@ type ProofVar = ProofVar<E, P>;
 
     /// Allocates `N::Proof` in `cs` without performing
     /// subgroup checks.
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_proof_unchecked<T: Borrow<Proof<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -93,17 +94,17 @@ let cs = ns.cs();
         f().and_then(|proof| {
             let proof = proof.borrow();
             let a = CurveVar::new_variable_omit_prime_order_check(
-                cs.ns("Proof.a"),
+                r1cs_core::ns!(cs, "Proof.a"),
                 || Ok(proof.a.into_projective()),
                 mode,
             )?;
             let b = CurveVar::new_variable_omit_prime_order_check(
-                cs.ns("Proof.b"),
+                r1cs_core::ns!(cs, "Proof.b"),
                 || Ok(proof.b.into_projective()),
                 mode,
             )?;
             let c = CurveVar::new_variable_omit_prime_order_check(
-                cs.ns("Proof.c"),
+                r1cs_core::ns!(cs, "Proof.c"),
                 || Ok(proof.c.into_projective()),
                 mode,
             )?;
@@ -113,6 +114,7 @@ }
 
     /// Allocates `N::Proof` in `cs` without performing
     /// subgroup checks.
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_verification_key_unchecked<T: Borrow<VerifyingKey<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -123,22 +125,22 @@ let cs = ns.cs();
         f().and_then(|vk| {
             let vk = vk.borrow();
             let alpha_g1 = P::G1Var::new_variable_omit_prime_order_check(
-                cs.ns("alpha_g1"),
+                r1cs_core::ns!(cs, "alpha_g1"),
                 || Ok(vk.alpha_g1.into_projective()),
                 mode,
             )?;
             let beta_g2 = P::G2Var::new_variable_omit_prime_order_check(
-                cs.ns("beta_g2"),
+                r1cs_core::ns!(cs, "beta_g2"),
                 || Ok(vk.beta_g2.into_projective()),
                 mode,
             )?;
             let gamma_g2 = P::G2Var::new_variable_omit_prime_order_check(
-                cs.ns("gamma_g2"),
+                r1cs_core::ns!(cs, "gamma_g2"),
                 || Ok(vk.gamma_g2.into_projective()),
                 mode,
             )?;
             let delta_g2 = P::G2Var::new_variable_omit_prime_order_check(
-                cs.ns("delta_g2"),
+                r1cs_core::ns!(cs, "delta_g2"),
                 || Ok(vk.delta_g2.into_projective()),
                 mode,
             )?;
@@ -148,7 +150,7 @@ .gamma_abc_g1
                 .iter()
                 .map(|g| {
                     P::G1Var::new_variable_omit_prime_order_check(
-                        cs.ns("g"),
+                        r1cs_core::ns!(cs, "g"),
                         || Ok(g.into_projective()),
                         mode,
                     )
@@ -164,6 +166,7 @@ })
         })
     }
 
+    #[tracing::instrument(target = "r1cs", skip(vk, input, proof))]
     fn verify<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
         vk: &Self::VerificationKeyVar,
         input: impl IntoIterator<Item = &'a T>,
@@ -173,6 +176,7 @@ let pvk = vk.prepare()?;
         <Self as NIZKVerifierGadget<Groth16<E, C, V>, E::Fq>>::verify_prepared(&pvk, input, proof)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(pvk, public_inputs, proof))]
     fn verify_prepared<'a, T: 'a + ToBitsGadget<E::Fq> + ?Sized>(
         pvk: &Self::PreparedVerificationKeyVar,
         public_inputs: impl IntoIterator<Item = &'a T>,
@@ -222,6 +226,7 @@ where
     E: PairingEngine,
     P: PairingVar<E>,
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<PreparedVerifyingKey<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -233,25 +238,28 @@
         f().and_then(|pvk| {
             let pvk = pvk.borrow();
             let alpha_g1_beta_g2 = P::GTVar::new_variable(
-                cs.ns("alpha_g1_beta_g2"),
+                r1cs_core::ns!(cs, "alpha_g1_beta_g2"),
                 || Ok(pvk.alpha_g1_beta_g2),
                 mode,
             )?;
 
             let gamma_g2_neg_pc = P::G2PreparedVar::new_variable(
-                cs.ns("gamma_g2_neg_pc"),
+                r1cs_core::ns!(cs, "gamma_g2_neg_pc"),
                 || Ok(pvk.gamma_g2_neg_pc.clone()),
                 mode,
             )?;
 
             let delta_g2_neg_pc = P::G2PreparedVar::new_variable(
-                cs.ns("delta_g2_neg_pc"),
+                r1cs_core::ns!(cs, "delta_g2_neg_pc"),
                 || Ok(pvk.delta_g2_neg_pc.clone()),
                 mode,
             )?;
 
-            let gamma_abc_g1 =
-                Vec::new_variable(cs.ns("gamma_abc_g1"), || Ok(pvk.gamma_abc_g1.clone()), mode)?;
+            let gamma_abc_g1 = Vec::new_variable(
+                r1cs_core::ns!(cs, "gamma_abc_g1"),
+                || Ok(pvk.gamma_abc_g1.clone()),
+                mode,
+            )?;
 
             Ok(Self {
                 alpha_g1_beta_g2,
@@ -269,6 +277,7 @@ E: PairingEngine,
 
     P: PairingVar<E>,
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<VerifyingKey<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -285,10 +294,14 @@ gamma_g2,
                 delta_g2,
                 gamma_abc_g1,
             } = vk.borrow().clone();
-            let alpha_g1 = P::G1Var::new_variable(cs.ns("alpha_g1"), || Ok(alpha_g1), mode)?;
-            let beta_g2 = P::G2Var::new_variable(cs.ns("beta_g2"), || Ok(beta_g2), mode)?;
-            let gamma_g2 = P::G2Var::new_variable(cs.ns("gamma_g2"), || Ok(gamma_g2), mode)?;
-            let delta_g2 = P::G2Var::new_variable(cs.ns("delta_g2"), || Ok(delta_g2), mode)?;
+            let alpha_g1 =
+                P::G1Var::new_variable(r1cs_core::ns!(cs, "alpha_g1"), || Ok(alpha_g1), mode)?;
+            let beta_g2 =
+                P::G2Var::new_variable(r1cs_core::ns!(cs, "beta_g2"), || Ok(beta_g2), mode)?;
+            let gamma_g2 =
+                P::G2Var::new_variable(r1cs_core::ns!(cs, "gamma_g2"), || Ok(gamma_g2), mode)?;
+            let delta_g2 =
+                P::G2Var::new_variable(r1cs_core::ns!(cs, "delta_g2"), || Ok(delta_g2), mode)?;
 
             let gamma_abc_g1 = Vec::new_variable(cs.clone(), || Ok(gamma_abc_g1), mode)?;
             Ok(Self {
@@ -307,6 +320,7 @@ where
     E: PairingEngine,
     P: PairingVar<E>,
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<Proof<E>>>(
         cs: impl Into<Namespace<E::Fq>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -317,9 +331,9 @@ let cs = ns.cs();
 
         f().and_then(|proof| {
             let Proof { a, b, c } = proof.borrow().clone();
-            let a = P::G1Var::new_variable(cs.ns("a"), || Ok(a), mode)?;
-            let b = P::G2Var::new_variable(cs.ns("b"), || Ok(b), mode)?;
-            let c = P::G1Var::new_variable(cs.ns("c"), || Ok(c), mode)?;
+            let a = P::G1Var::new_variable(r1cs_core::ns!(cs, "a"), || Ok(a), mode)?;
+            let b = P::G2Var::new_variable(r1cs_core::ns!(cs, "b"), || Ok(b), mode)?;
+            let c = P::G1Var::new_variable(r1cs_core::ns!(cs, "c"), || Ok(c), mode)?;
             Ok(Self { a, b, c })
         })
     }
@@ -331,6 +345,7 @@ E: PairingEngine,
     P: PairingVar<E>,
 {
     #[inline]
+    #[tracing::instrument(target = "r1cs", skip(self))]
     fn to_bytes(&self) -> Result<Vec<UInt8<E::Fq>>, SynthesisError> {
         let mut bytes = Vec::new();
         bytes.extend_from_slice(&self.alpha_g1.to_bytes()?);
@@ -389,8 +404,7 @@ .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
                     let result_var = cs.new_witness_variable(|| {
                         result_val.ok_or(SynthesisError::AssignmentMissing)
                     })?;
-                    cs.enforce_named_constraint(
-                        format!("Enforce constraint {}", i),
+                    cs.enforce_constraint(
                         lc!() + input_1_var,
                         lc!() + input_2_var,
                         lc!() + result_var,
@@ -441,11 +455,11 @@ let inputs: Vec<_> = inputs.into_iter().map(|input| input.unwrap()).collect();
             let mut input_gadgets = Vec::new();
 
             {
-                for (i, input) in inputs.into_iter().enumerate() {
+                for input in inputs.into_iter() {
                     let input_bits = BitIteratorLE::new(input.into_repr()).collect::<Vec<_>>();
 
                     let input_bits =
-                        Vec::<Boolean<Fq>>::new_input(cs.ns(format!("Input {}", i)), || {
+                        Vec::<Boolean<Fq>>::new_input(r1cs_core::ns!(cs, "Input"), || {
                             Ok(input_bits)
                         })
                         .unwrap();
@@ -453,9 +467,11 @@ input_gadgets.push(input_bits);
                 }
             }
 
-            let vk_gadget = TestVkVar::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
+            let vk_gadget =
+                TestVkVar::new_input(r1cs_core::ns!(cs, "Vk"), || Ok(&params.vk)).unwrap();
             let proof_gadget =
-                TestProofVar::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
+                TestProofVar::new_witness(r1cs_core::ns!(cs, "Proof"), || Ok(proof.clone()))
+                    .unwrap();
             println!("Time to verify!\n\n\n\n");
             <TestVerifierGadget as NIZKVerifierGadget<TestProofSystem, Fq>>::verify(
                 &vk_gadget,
@@ -534,8 +550,7 @@ .and_then(|input_1| input_2_val.map(|input_2| input_1 * &input_2));
                     let result_var = cs.new_witness_variable(|| {
                         result_val.ok_or(SynthesisError::AssignmentMissing)
                     })?;
-                    cs.enforce_named_constraint(
-                        format!("Enforce constraint {}", i),
+                    cs.enforce_constraint(
                         lc!() + input_1_var,
                         lc!() + input_2_var,
                         lc!() + result_var,
@@ -585,7 +600,8 @@ })
                     .collect::<Vec<_>>();
 
                 // Allocate this byte array as input packed into field elements.
-                let input_bytes = UInt8::new_input_vec(cs.ns("Input"), &input_bytes[..])?;
+                let input_bytes =
+                    UInt8::new_input_vec(r1cs_core::ns!(cs, "Input"), &input_bytes[..])?;
                 // 40 byte
                 let element_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 8;
                 input_gadgets = input_bytes
@@ -599,9 +615,10 @@ })
                     .collect::<Vec<_>>();
             }
 
-            let vk_gadget = TestVkVar1::new_witness(cs.ns("Vk"), || Ok(&params.vk))?;
+            let vk_gadget = TestVkVar1::new_witness(r1cs_core::ns!(cs, "Vk"), || Ok(&params.vk))?;
             let proof_gadget =
-                TestProofVar1::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
+                TestProofVar1::new_witness(r1cs_core::ns!(cs, "Proof"), || Ok(proof.clone()))
+                    .unwrap();
             <TestVerifierGadget1 as NIZKVerifierGadget<TestProofSystem1, MNT6Fq>>::verify(
                 &vk_gadget,
                 &input_gadgets,
@@ -675,9 +692,9 @@
             {
                 let bigint_size = <MNT4FqParameters as FftParameters>::BigInt::NUM_LIMBS * 64;
                 let mut input_bits = Vec::new();
-                for (i, input) in inputs.into_iter().enumerate() {
+                for input in inputs.into_iter() {
                     let input_gadget =
-                        FpVar::new_input(cs.ns(format!("Input {}", i)), || Ok(input)).unwrap();
+                        FpVar::new_input(r1cs_core::ns!(cs, "Input"), || Ok(input)).unwrap();
                     let mut fp_bits = input_gadget.to_bits_le().unwrap();
 
                     // Use 320 bits per element.
@@ -702,9 +719,11 @@ }
                 // assert!(!verify_proof(&pvk, &proof, &[a]).unwrap());
             }
 
-            let vk_gadget = TestVkVar2::new_input(cs.ns("Vk"), || Ok(&params.vk)).unwrap();
+            let vk_gadget =
+                TestVkVar2::new_input(r1cs_core::ns!(cs, "Vk"), || Ok(&params.vk)).unwrap();
             let proof_gadget =
-                TestProofVar2::new_witness(cs.ns("Proof"), || Ok(proof.clone())).unwrap();
+                TestProofVar2::new_witness(r1cs_core::ns!(cs, "Proof"), || Ok(proof.clone()))
+                    .unwrap();
             println!("Time to verify!\n\n\n\n");
             <TestVerifierGadget2 as NIZKVerifierGadget<TestProofSystem2, MNT4Fq>>::verify(
                 &vk_gadget,

@@ -91,12 +91,7 @@ let input = cs.new_input_variable(|| Ok(self.x.unwrap()))?;
                 let sum = cs.new_input_variable(|| Ok(self.sum.unwrap()))?;
                 let witness = cs.new_witness_variable(|| Ok(self.w.unwrap()))?;
 
-                cs.enforce_named_constraint(
-                    "enforce sum",
-                    lc!() + sum,
-                    lc!() + Variable::One,
-                    lc!() + input + witness,
-                )?;
+                cs.enforce_constraint(lc!() + sum, lc!() + Variable::One, lc!() + input + witness)?;
                 Ok(())
             }
         }

@@ -294,12 +294,14 @@ #[derive(Clone, Debug)]
 pub struct OutputVar<ConstraintF: PrimeField>(pub Vec<UInt8<ConstraintF>>);
 
 impl<ConstraintF: PrimeField> EqGadget<ConstraintF> for OutputVar<ConstraintF> {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError> {
         self.0.is_eq(&other.0)
     }
 
     /// If `should_enforce == true`, enforce that `self` and `other` are equal; else,
     /// enforce a vacuously true statement.
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -310,6 +312,7 @@ }
 
     /// If `should_enforce == true`, enforce that `self` and `other` are not equal; else,
     /// enforce a vacuously true statement.
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -329,6 +332,7 @@ }
 }
 
 impl<ConstraintF: PrimeField> AllocVar<[u8; 32], ConstraintF> for OutputVar<ConstraintF> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<[u8; 32]>>(
         cs: impl Into<Namespace<ConstraintF>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -362,10 +366,14 @@
 impl<F: PrimeField> PRFGadget<Blake2s, F> for Blake2sGadget {
     type OutputVar = OutputVar<F>;
 
-    fn new_seed(cs: ConstraintSystemRef<F>, seed: &[u8; 32]) -> Vec<UInt8<F>> {
-        UInt8::new_witness_vec(cs.ns("New Blake2s seed"), seed).unwrap()
+    #[tracing::instrument(target = "r1cs", skip(cs))]
+    fn new_seed(cs: impl Into<Namespace<F>>, seed: &[u8; 32]) -> Vec<UInt8<F>> {
+        let ns = cs.into();
+        let cs = ns.cs();
+        UInt8::new_witness_vec(r1cs_core::ns!(cs, "New Blake2s seed"), seed).unwrap()
     }
 
+    #[tracing::instrument(target = "r1cs", skip(seed, input))]
     fn evaluate(seed: &[UInt8<F>], input: &[UInt8<F>]) -> Result<Self::OutputVar, SynthesisError> {
         assert_eq!(seed.len(), 32);
         let input: Vec<_> = seed
@@ -398,7 +406,7 @@ #[test]
     fn test_blake2s_constraints() {
         let cs = ConstraintSystem::<Fr>::new_ref();
         let input_bits: Vec<_> = (0..512)
-            .map(|i| Boolean::new_witness(cs.ns(format!("input bit {}", i)), || Ok(true)).unwrap())
+            .map(|_| Boolean::new_witness(r1cs_core::ns!(cs, "input bit"), || Ok(true)).unwrap())
             .collect();
         evaluate_blake2s(&input_bits).unwrap();
         assert!(cs.is_satisfied().unwrap());
@@ -420,10 +428,11 @@ let mut input = [0u8; 32];
         rng.fill(&mut input);
 
         let seed_var = Blake2sGadget::new_seed(cs.clone(), &seed);
-        let input_var = UInt8::new_witness_vec(cs.ns("declare_input"), &input).unwrap();
+        let input_var =
+            UInt8::new_witness_vec(r1cs_core::ns!(cs, "declare_input"), &input).unwrap();
         let out = B2SPRF::evaluate(&seed, &input).unwrap();
         let actual_out_var = <Blake2sGadget as PRFGadget<_, Fr>>::OutputVar::new_witness(
-            cs.ns("declare_output"),
+            r1cs_core::ns!(cs, "declare_output"),
             || Ok(out),
         )
         .unwrap();
@@ -449,8 +458,8 @@ let cs = ConstraintSystem::<Fr>::new_ref();
         let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
         let input_bits: Vec<_> = (0..512)
             .map(|_| Boolean::constant(rng.gen()))
-            .chain((0..512).map(|i| {
-                Boolean::new_witness(cs.ns(format!("input bit {}", i)), || Ok(true)).unwrap()
+            .chain((0..512).map(|_| {
+                Boolean::new_witness(r1cs_core::ns!(cs, "input bit"), || Ok(true)).unwrap()
             }))
             .collect();
         evaluate_blake2s(&input_bits).unwrap();
@@ -488,9 +497,9 @@ let cs = ConstraintSystem::<Fr>::new_ref();
 
             let mut input_bits = vec![];
 
-            for (byte_i, input_byte) in data.into_iter().enumerate() {
+            for input_byte in data.into_iter() {
                 for bit_i in 0..8 {
-                    let cs = cs.ns(format!("input bit {} {}", byte_i, bit_i));
+                    let cs = r1cs_core::ns!(cs, "input bit");
 
                     input_bits.push(
                         Boolean::new_witness(cs, || Ok((input_byte >> bit_i) & 1u8 == 1u8))

@@ -2,7 +2,7 @@ use algebra_core::Field;
 use core::fmt::Debug;
 
 use crate::{prf::PRF, Vec};
-use r1cs_core::{ConstraintSystemRef, SynthesisError};
+use r1cs_core::{Namespace, SynthesisError};
 
 use r1cs_std::prelude::*;
 
@@ -14,7 +14,7 @@ + R1CSVar<F, Value = P::Output>
         + Clone
         + Debug;
 
-    fn new_seed(cs: ConstraintSystemRef<F>, seed: &P::Seed) -> Vec<UInt8<F>>;
+    fn new_seed(cs: impl Into<Namespace<F>>, seed: &P::Seed) -> Vec<UInt8<F>>;
 
     fn evaluate(seed: &[UInt8<F>], input: &[UInt8<F>]) -> Result<Self::OutputVar, SynthesisError>;
 }

@@ -56,6 +56,7 @@ {
     type ParametersVar = ParametersVar<C, GC>;
     type PublicKeyVar = PublicKeyVar<C, GC>;
 
+    #[tracing::instrument(target = "r1cs", skip(parameters, public_key, randomness))]
     fn randomize(
         parameters: &Self::ParametersVar,
         public_key: &Self::PublicKeyVar,

@@ -25,6 +25,7 @@ [dependencies]
 algebra = { path = "../algebra", default-features = false }
 r1cs-core = { path = "../r1cs-core", default-features = false }
 derivative = { version = "2", features = ["use_core"] }
+tracing = { version = "0.1", default-features = false, features = [ "attributes" ] }
 
 [dev-dependencies]
 rand = { version = "0.7", default-features = false }

@@ -34,6 +34,7 @@ f: impl FnOnce() -> Result<T, SynthesisError>,
         mode: AllocationMode,
     ) -> Result<Self, SynthesisError>;
 
+    #[tracing::instrument(target = "r1cs", skip(cs, t))]
     fn new_constant(
         cs: impl Into<Namespace<F>>,
         t: impl Borrow<V>,
@@ -41,6 +42,7 @@ ) -> Result<Self, SynthesisError> {
         Self::new_variable(cs, || Ok(t), AllocationMode::Constant)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_input<T: Borrow<V>>(
         cs: impl Into<Namespace<F>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -48,6 +50,7 @@ ) -> Result<Self, SynthesisError> {
         Self::new_variable(cs, f, AllocationMode::Input)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_witness<T: Borrow<V>>(
         cs: impl Into<Namespace<F>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,

@@ -50,6 +50,7 @@ }
 
     /// Performs an XOR operation over the two operands, returning
     /// an `AllocatedBit`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn xor(&self, b: &Self) -> Result<Self, SynthesisError> {
         let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
             Ok(self.value()? ^ b.value()?)
@@ -81,6 +82,7 @@ }
 
     /// Performs an AND operation over the two operands, returning
     /// an `AllocatedBit`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn and(&self, b: &Self) -> Result<Self, SynthesisError> {
         let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
             Ok(self.value()? & b.value()?)
@@ -99,6 +101,7 @@ }
 
     /// Performs an OR operation over the two operands, returning
     /// an `AllocatedBit`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn or(&self, b: &Self) -> Result<Self, SynthesisError> {
         let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
             Ok(self.value()? | b.value()?)
@@ -116,6 +119,7 @@ Ok(result)
     }
 
     /// Calculates `a AND (NOT b)`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn and_not(&self, b: &Self) -> Result<Self, SynthesisError> {
         let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
             Ok(self.value()? & !b.value()?)
@@ -133,6 +137,7 @@ Ok(result)
     }
 
     /// Calculates `(NOT a) AND (NOT b)`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn nor(&self, b: &Self) -> Result<Self, SynthesisError> {
         let result = Self::new_witness_without_booleanity_check(self.cs.clone(), || {
             Ok(!(self.value()? | b.value()?))
@@ -184,12 +189,7 @@
             // Constrain: (1 - a) * a = 0
             // This constrains a to be either 0 or 1.
 
-            cs.enforce_named_constraint(
-                "Booleanity check",
-                lc!() + Variable::One - variable,
-                lc!() + variable,
-                lc!(),
-            )?;
+            cs.enforce_constraint(lc!() + Variable::One - variable, lc!() + variable, lc!())?;
 
             Ok(Self { variable, cs })
         }
@@ -197,6 +197,7 @@ }
 }
 
 impl<F: Field> CondSelectGadget<F> for AllocatedBit<F> {
+    #[tracing::instrument(target = "r1cs")]
     fn conditionally_select(
         cond: &Boolean<F>,
         true_val: &Self,
@@ -287,8 +288,10 @@ Boolean::Not(ref v) => Boolean::Is(v.clone()),
         }
     }
 }
+
 impl<F: Field> Boolean<F> {
     /// Perform XOR over two boolean operands
+    #[tracing::instrument(target = "r1cs")]
     pub fn xor<'a>(&'a self, b: &'a Self) -> Result<Self, SynthesisError> {
         use Boolean::*;
         match (self, b) {
@@ -304,6 +307,7 @@ }
     }
 
     /// Perform OR over two boolean operands
+    #[tracing::instrument(target = "r1cs")]
     pub fn or<'a>(&'a self, b: &'a Self) -> Result<Self, SynthesisError> {
         use Boolean::*;
         match (self, b) {
@@ -318,6 +322,7 @@ }
     }
 
     /// Perform AND over two boolean operands
+    #[tracing::instrument(target = "r1cs")]
     pub fn and<'a>(&'a self, b: &'a Self) -> Result<Self, SynthesisError> {
         use Boolean::*;
         match (self, b) {
@@ -334,6 +339,7 @@ (&Is(ref a), &Is(ref b)) => Ok(Is(a.and(b)?)),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn kary_and(bits: &[Self]) -> Result<Self, SynthesisError> {
         assert!(!bits.is_empty());
         let mut cur: Option<Self> = None;
@@ -348,6 +354,7 @@
         Ok(cur.expect("should not be 0"))
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn kary_or(bits: &[Self]) -> Result<Self, SynthesisError> {
         assert!(!bits.is_empty());
         let mut cur: Option<Self> = None;
@@ -362,11 +369,13 @@
         Ok(cur.expect("should not be 0"))
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn kary_nand(bits: &[Self]) -> Result<Self, SynthesisError> {
         Ok(Self::kary_and(bits)?.not())
     }
 
     /// Assert that at least one input is false.
+    #[tracing::instrument(target = "r1cs")]
     fn enforce_kary_nand(bits: &[Self]) -> Result<(), SynthesisError> {
         use Boolean::*;
         let r = Self::kary_nand(bits)?;
@@ -384,6 +393,7 @@
     /// Enforces that `bits`, when interpreted as a integer, is less than `F::characteristic()`,
     /// That is, interpret bits as a little-endian integer, and enforce that this integer
     /// is "in the field F".
+    #[tracing::instrument(target = "r1cs")]
     pub fn enforce_in_field_le(bits: &[Self]) -> Result<(), SynthesisError> {
         // `bits` < F::characteristic() <==> `bits` <= F::characteristic() -1
         let mut b = F::characteristic().to_vec();
@@ -401,6 +411,7 @@ }
 
     /// Enforces that `bits` is less than or equal to `element`,
     /// when both are interpreted as (little-endian) integers.
+    #[tracing::instrument(target = "r1cs", skip(element))]
     pub fn enforce_smaller_or_equal_than_le<'a>(
         bits: &[Self],
         element: impl AsRef<[u64]>,
@@ -455,6 +466,7 @@
         Ok(current_run)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(first, second))]
     pub fn select<T: CondSelectGadget<F>>(
         &self,
         first: &T,
@@ -485,6 +497,7 @@ }
 }
 
 impl<F: Field> EqGadget<F> for Boolean<F> {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
         // self | other | XNOR(self, other) | self == other
         // -----|-------|-------------------|--------------
@@ -495,6 +508,7 @@ //   1  |   1   |         1         |      1
         Ok(self.xor(other)?.not())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -530,6 +544,7 @@ }
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -572,6 +587,7 @@ }
 
 impl<F: Field> ToBytesGadget<F> for Boolean<F> {
     /// Outputs `1u8` if `self` is true, and `0u8` otherwise.
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
         let mut bits = vec![self.clone()];
         bits.extend(vec![Boolean::constant(false); 7]);
@@ -582,6 +598,7 @@ }
 }
 
 impl<F: Field> CondSelectGadget<F> for Boolean<F> {
+    #[tracing::instrument(target = "r1cs")]
     fn conditionally_select(
         cond: &Boolean<F>,
         true_val: &Self,
@@ -670,8 +687,8 @@ fn test_xor() -> Result<(), SynthesisError> {
         for a_val in [false, true].iter().copied() {
             for b_val in [false, true].iter().copied() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
-                let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
-                let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
+                let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
+                let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
                 let c = AllocatedBit::xor(&a, &b)?;
                 assert_eq!(c.value()?, a_val ^ b_val);
 
@@ -689,8 +706,8 @@ fn test_or() -> Result<(), SynthesisError> {
         for a_val in [false, true].iter().copied() {
             for b_val in [false, true].iter().copied() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
-                let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
-                let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
+                let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
+                let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
                 let c = AllocatedBit::or(&a, &b)?;
                 assert_eq!(c.value()?, a_val | b_val);
 
@@ -708,8 +725,8 @@ fn test_and() -> Result<(), SynthesisError> {
         for a_val in [false, true].iter().copied() {
             for b_val in [false, true].iter().copied() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
-                let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
-                let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
+                let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
+                let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
                 let c = AllocatedBit::and(&a, &b)?;
                 assert_eq!(c.value()?, a_val & b_val);
 
@@ -727,8 +744,8 @@ fn test_and_not() -> Result<(), SynthesisError> {
         for a_val in [false, true].iter().copied() {
             for b_val in [false, true].iter().copied() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
-                let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
-                let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
+                let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
+                let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
                 let c = AllocatedBit::and_not(&a, &b)?;
                 assert_eq!(c.value()?, a_val & !b_val);
 
@@ -746,8 +763,8 @@ fn test_nor() -> Result<(), SynthesisError> {
         for a_val in [false, true].iter().copied() {
             for b_val in [false, true].iter().copied() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
-                let a = AllocatedBit::new_witness(cs.ns("a"), || Ok(a_val))?;
-                let b = AllocatedBit::new_witness(cs.ns("b"), || Ok(b_val))?;
+                let a = AllocatedBit::new_witness(cs.clone(), || Ok(a_val))?;
+                let b = AllocatedBit::new_witness(cs.clone(), || Ok(b_val))?;
                 let c = AllocatedBit::nor(&a, &b)?;
                 assert_eq!(c.value()?, !a_val & !b_val);
 
@@ -768,8 +785,8 @@ for a_neg in [false, true].iter().cloned() {
                     for b_neg in [false, true].iter().cloned() {
                         let cs = ConstraintSystem::<Fr>::new_ref();
 
-                        let mut a = Boolean::new_witness(cs.ns("a"), || Ok(a_bool))?;
-                        let mut b = Boolean::new_witness(cs.ns("b"), || Ok(b_bool))?;
+                        let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
+                        let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
 
                         if a_neg {
                             a = a.not();
@@ -822,8 +839,8 @@ // Now test if constraint system is satisfied even
                         // when we don't want to enforce the condition.
                         let cs = ConstraintSystem::<Fr>::new_ref();
 
-                        let mut a = Boolean::new_witness(cs.ns("a"), || Ok(a_bool))?;
-                        let mut b = Boolean::new_witness(cs.ns("b"), || Ok(b_bool))?;
+                        let mut a = Boolean::new_witness(cs.clone(), || Ok(a_bool))?;
+                        let mut b = Boolean::new_witness(cs.clone(), || Ok(b_bool))?;
 
                         if a_neg {
                             a = a.not();
@@ -832,7 +849,8 @@ if b_neg {
                             b = b.not();
                         }
 
-                        let false_cond = Boolean::new_witness(cs.ns("cond"), || Ok(false))?;
+                        let false_cond =
+                            Boolean::new_witness(r1cs_core::ns!(cs, "cond"), || Ok(false))?;
                         a.conditional_enforce_equal(&b, &false_cond)?;
 
                         assert!(cs.is_satisfied().unwrap());
@@ -887,12 +905,10 @@ OpType::NegatedAllocatedFalse,
     ];
 
     fn construct<F: Field>(
-        cs: impl Into<Namespace<F>>,
+        ns: Namespace<F>,
         operand: OpType,
-        name: &'static str,
     ) -> Result<Boolean<F>, SynthesisError> {
-        let ns = cs.into();
-        let cs = ns.cs().ns(name);
+        let cs = ns.cs();
 
         let b = match operand {
             OpType::True => Boolean::constant(true),
@@ -911,8 +927,8 @@ for first_operand in VARIANTS.iter().cloned() {
             for second_operand in VARIANTS.iter().cloned() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
 
-                let a = construct(cs.clone(), first_operand, "a")?;
-                let b = construct(cs.clone(), second_operand, "b")?;
+                let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
+                let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
                 let c = Boolean::xor(&a, &b)?;
 
                 assert!(cs.is_satisfied().unwrap());
@@ -1041,9 +1057,9 @@ for first_operand in VARIANTS.iter().cloned() {
                 for second_operand in VARIANTS.iter().cloned() {
                     let cs = ConstraintSystem::<Fr>::new_ref();
 
-                    let cond = construct(cs.clone(), condition, "cond")?;
-                    let a = construct(cs.clone(), first_operand, "a")?;
-                    let b = construct(cs.clone(), second_operand, "b")?;
+                    let cond = construct(r1cs_core::ns!(cs, "cond"), condition)?;
+                    let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
+                    let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
                     let c = cond.select(&a, &b)?;
 
                     assert!(
@@ -1073,8 +1089,8 @@ for first_operand in VARIANTS.iter().cloned() {
             for second_operand in VARIANTS.iter().cloned() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
 
-                let a = construct(cs.clone(), first_operand, "a")?;
-                let b = construct(cs.clone(), second_operand, "b")?;
+                let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
+                let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
                 let c = a.or(&b)?;
 
                 assert!(cs.is_satisfied().unwrap());
@@ -1194,8 +1210,8 @@ for first_operand in VARIANTS.iter().cloned() {
             for second_operand in VARIANTS.iter().cloned() {
                 let cs = ConstraintSystem::<Fr>::new_ref();
 
-                let a = construct(cs.clone(), first_operand, "a")?;
-                let b = construct(cs.clone(), second_operand, "b")?;
+                let a = construct(r1cs_core::ns!(cs, "a"), first_operand)?;
+                let b = construct(r1cs_core::ns!(cs, "b"), second_operand)?;
                 let c = a.and(&b)?;
 
                 assert!(cs.is_satisfied().unwrap());

@@ -104,6 +104,7 @@
                     Self { value, bits }
                 }
 
+                #[tracing::instrument(target = "r1cs", skip(self))]
                 pub fn rotr(&self, by: usize) -> Self {
                     let by = by % $size;
 
@@ -123,6 +124,7 @@ }
                 }
 
                 /// XOR this `$name` with another `$name`
+                #[tracing::instrument(target = "r1cs", skip(self))]
                 pub fn xor(&self, other: &Self) -> Result<Self, SynthesisError> {
                     let new_value = match (self.value, other.value) {
                         (Some(a), Some(b)) => Some(a ^ b),
@@ -143,6 +145,7 @@ })
                 }
 
                 /// Perform modular addition of several `$name` objects.
+                #[tracing::instrument(target = "r1cs")]
                 pub fn addmany(operands: &[Self]) -> Result<Self, SynthesisError>
                 where
                     F: PrimeField,
@@ -261,7 +264,7 @@ }
             }
 
             impl<ConstraintF: Field> ToBytesGadget<ConstraintF> for $name<ConstraintF> {
-                #[inline]
+                #[tracing::instrument(target = "r1cs", skip(self))]
                 fn to_bytes(&self) -> Result<Vec<UInt8<ConstraintF>>, SynthesisError> {
                     Ok(self
                         .to_bits_le()
@@ -272,10 +275,12 @@ }
             }
 
             impl<ConstraintF: Field> EqGadget<ConstraintF> for $name<ConstraintF> {
+                #[tracing::instrument(target = "r1cs", skip(self))]
                 fn is_eq(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError> {
                     self.bits.as_slice().is_eq(&other.bits)
                 }
 
+                #[tracing::instrument(target = "r1cs", skip(self))]
                 fn conditional_enforce_equal(
                     &self,
                     other: &Self,
@@ -284,6 +289,7 @@ ) -> Result<(), SynthesisError> {
                     self.bits.conditional_enforce_equal(&other.bits, condition)
                 }
 
+                #[tracing::instrument(target = "r1cs", skip(self))]
                 fn conditional_enforce_not_equal(
                     &self,
                     other: &Self,
@@ -446,10 +452,10 @@ let d: $native = rng.gen();
 
                         let mut expected = (a ^ b).wrapping_add(c).wrapping_add(d);
 
-                        let a_bit = $name::new_witness(cs.ns("a_bit"), || Ok(a))?;
+                        let a_bit = $name::new_witness(r1cs_core::ns!(cs, "a_bit"), || Ok(a))?;
                         let b_bit = $name::constant(b);
                         let c_bit = $name::constant(c);
-                        let d_bit = $name::new_witness(cs.ns("d_bit"), || Ok(d))?;
+                        let d_bit = $name::new_witness(r1cs_core::ns!(cs, "d_bit"), || Ok(d))?;
 
                         let r = a_bit.xor(&b_bit).unwrap();
                         let r = $name::addmany(&[r, c_bit, d_bit]).unwrap();

@@ -117,6 +117,7 @@ }
 
     /// Converts a little-endian byte order representation of bits into a
     /// `UInt8`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn from_bits_le(bits: &[Boolean<F>]) -> Self {
         assert_eq!(bits.len(), 8);
 
@@ -134,6 +135,7 @@ Self { value, bits }
     }
 
     /// XOR this `UInt8` with another `UInt8`
+    #[tracing::instrument(target = "r1cs")]
     pub fn xor(&self, other: &Self) -> Result<Self, SynthesisError> {
         let new_value = match (self.value, other.value) {
             (Some(a), Some(b)) => Some(a ^ b),
@@ -155,10 +157,12 @@ }
 }
 
 impl<ConstraintF: Field> EqGadget<ConstraintF> for UInt8<ConstraintF> {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(&self, other: &Self) -> Result<Boolean<ConstraintF>, SynthesisError> {
         self.bits.as_slice().is_eq(&other.bits)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -167,6 +171,7 @@ ) -> Result<(), SynthesisError> {
         self.bits.conditional_enforce_equal(&other.bits, condition)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -214,7 +219,7 @@ #[test]
     fn test_uint8_from_bits_to_bits() -> Result<(), SynthesisError> {
         let cs = ConstraintSystem::<Fr>::new_ref();
         let byte_val = 0b01110001;
-        let byte = UInt8::new_witness(cs.ns("alloc value"), || Ok(byte_val)).unwrap();
+        let byte = UInt8::new_witness(r1cs_core::ns!(cs, "alloc value"), || Ok(byte_val)).unwrap();
         let bits = byte.to_bits_le()?;
         for (i, bit) in bits.iter().enumerate() {
             assert_eq!(bit.value()?, (byte_val >> i) & 1 == 1)
@@ -226,7 +231,7 @@ #[test]
     fn test_uint8_new_input_vec() -> Result<(), SynthesisError> {
         let cs = ConstraintSystem::<Fr>::new_ref();
         let byte_vals = (64u8..128u8).collect::<Vec<_>>();
-        let bytes = UInt8::new_input_vec(cs.ns("alloc value"), &byte_vals).unwrap();
+        let bytes = UInt8::new_input_vec(r1cs_core::ns!(cs, "alloc value"), &byte_vals).unwrap();
         dbg!(bytes.value())?;
         for (native, variable) in byte_vals.into_iter().zip(bytes) {
             let bits = variable.to_bits_le()?;
@@ -287,9 +292,9 @@ let c: u8 = rng.gen();
 
             let mut expected = a ^ b ^ c;
 
-            let a_bit = UInt8::new_witness(cs.ns("a_bit"), || Ok(a)).unwrap();
+            let a_bit = UInt8::new_witness(r1cs_core::ns!(cs, "a_bit"), || Ok(a)).unwrap();
             let b_bit = UInt8::constant(b);
-            let c_bit = UInt8::new_witness(cs.ns("c_bit"), || Ok(c)).unwrap();
+            let c_bit = UInt8::new_witness(r1cs_core::ns!(cs, "c_bit"), || Ok(c)).unwrap();
 
             let r = a_bit.xor(&b_bit).unwrap();
             let r = r.xor(&c_bit).unwrap();

@@ -13,6 +13,7 @@ }
 
     /// If `should_enforce == true`, enforce that `self` and `other` are equal; else,
     /// enforce a vacuously true statement.
+    #[tracing::instrument(target = "r1cs", skip(self, other))]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -23,12 +24,14 @@ .conditional_enforce_equal(&Boolean::constant(true), should_enforce)
     }
 
     /// Enforce that `self` and `other` are equal.
+    #[tracing::instrument(target = "r1cs", skip(self, other))]
     fn enforce_equal(&self, other: &Self) -> Result<(), SynthesisError> {
         self.conditional_enforce_equal(other, &Boolean::constant(true))
     }
 
     /// If `should_enforce == true`, enforce that `self` and `other` are not equal; else,
     /// enforce a vacuously true statement.
+    #[tracing::instrument(target = "r1cs", skip(self, other))]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -39,12 +42,14 @@ .conditional_enforce_equal(&Boolean::constant(true), should_enforce)
     }
 
     /// Enforce that `self` and `other` are not equal.
+    #[tracing::instrument(target = "r1cs", skip(self, other))]
     fn enforce_not_equal(&self, other: &Self) -> Result<(), SynthesisError> {
         self.conditional_enforce_not_equal(other, &Boolean::constant(true))
     }
 }
 
 impl<T: EqGadget<F> + R1CSVar<F>, F: Field> EqGadget<F> for [T] {
+    #[tracing::instrument(target = "r1cs", skip(self, other))]
     fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
         assert_eq!(self.len(), other.len());
         assert!(!self.is_empty());
@@ -55,6 +60,7 @@ }
         Boolean::kary_and(&results)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(self, other))]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -67,6 +73,7 @@ }
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs", skip(self, other))]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,

@@ -147,6 +147,7 @@ Self::new(c0, c1, c2)
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn double(&self) -> Result<Self, SynthesisError> {
         let c0 = self.c0.double()?;
         let c1 = self.c1.double()?;
@@ -155,6 +156,7 @@ Ok(Self::new(c0, c1, c2))
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn negate(&self) -> Result<Self, SynthesisError> {
         let mut result = self.clone();
         result.c0.negate_in_place()?;
@@ -169,6 +171,7 @@ /// (Devegili OhEig Scott Dahab --- Multiplication and Squaring on
     /// Abstract Pairing-Friendly
     /// Fields.pdf; Section 4 (CH-SQR2))
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn square(&self) -> Result<Self, SynthesisError> {
         let a = self.c0.clone();
         let b = self.c1.clone();
@@ -188,6 +191,7 @@
         Ok(Self::new(c0, c1, c2))
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
         // Karatsuba multiplication for cubic extensions:
         //     v0 = A.c0 * B.c0
@@ -237,6 +241,7 @@ a0_plus_a2.mul_equals(&b0_plus_b2, &to_check)?;
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn frobenius_map(&self, power: usize) -> Result<Self, SynthesisError> {
         let mut result = self.clone();
         result.c0.frobenius_map_in_place(power)?;
@@ -247,6 +252,7 @@ P::mul_base_field_vars_by_frob_coeff(&mut result.c1, &mut result.c2, power);
         Ok(result)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn inverse(&self) -> Result<Self, SynthesisError> {
         let cs = self.cs().get()?.clone();
         let one = Self::new_constant(cs.clone(), CubicExtField::one())?;
@@ -342,6 +348,7 @@ BF: FieldVar<P::BaseField, P::BasePrimeField>,
     for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
     P: CubicExtVarParams<BF>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(&self, other: &Self) -> Result<Boolean<P::BasePrimeField>, SynthesisError> {
         let b0 = self.c0.is_eq(&other.c0)?;
         let b1 = self.c1.is_eq(&other.c1)?;
@@ -350,6 +357,7 @@ b0.and(&b1)?.and(&b2)
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -362,6 +370,7 @@ Ok(())
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -380,6 +389,7 @@ BF: FieldVar<P::BaseField, P::BasePrimeField>,
     for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
     P: CubicExtVarParams<BF>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bits_le(&self) -> Result<Vec<Boolean<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_bits_le()?;
         let mut c1 = self.c1.to_bits_le()?;
@@ -389,6 +399,7 @@ c0.append(&mut c2);
         Ok(c0)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bits_le(&self) -> Result<Vec<Boolean<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_non_unique_bits_le()?;
         let mut c1 = self.c1.to_non_unique_bits_le()?;
@@ -405,6 +416,7 @@ BF: FieldVar<P::BaseField, P::BasePrimeField>,
     for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
     P: CubicExtVarParams<BF>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_bytes()?;
         let mut c1 = self.c1.to_bytes()?;
@@ -415,6 +427,7 @@
         Ok(c0)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_non_unique_bytes()?;
         let mut c1 = self.c1.to_non_unique_bytes()?;
@@ -434,6 +447,7 @@ for<'a> &'a BF: FieldOpsBounds<'a, P::BaseField, BF>,
     P: CubicExtVarParams<BF>,
 {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditionally_select(
         cond: &Boolean<P::BasePrimeField>,
         true_value: &Self,
@@ -455,6 +469,7 @@ P: CubicExtVarParams<BF>,
 {
     type TableConstant = CubicExtField<P>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn two_bit_lookup(
         b: &[Boolean<P::BasePrimeField>],
         c: &[Self::TableConstant],
@@ -478,6 +493,7 @@ P: CubicExtVarParams<BF>,
 {
     type TableConstant = CubicExtField<P>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn three_bit_cond_neg_lookup(
         b: &[Boolean<P::BasePrimeField>],
         b0b1: &Boolean<P::BasePrimeField>,
@@ -517,9 +533,9 @@ Err(AssignmentMissing),
             ),
         };
 
-        let c0 = BF::new_variable(cs.ns("c0"), || c0, mode)?;
-        let c1 = BF::new_variable(cs.ns("c1"), || c1, mode)?;
-        let c2 = BF::new_variable(cs.ns("c2"), || c2, mode)?;
+        let c0 = BF::new_variable(r1cs_core::ns!(cs, "c0"), || c0, mode)?;
+        let c1 = BF::new_variable(r1cs_core::ns!(cs, "c1"), || c1, mode)?;
+        let c2 = BF::new_variable(r1cs_core::ns!(cs, "c2"), || c2, mode)?;
         Ok(Self::new(c0, c1, c2))
     }
 }

@@ -14,6 +14,7 @@ /// constraint system will not be satisfied otherwise. If `self` should
     /// also be checked for equality, e.g. `self <= other` instead of `self < other`, set
     /// `should_also_check_quality` to `true`. This variant verifies `self` and `other`
     /// are `<= (p-1)/2`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn enforce_cmp(
         &self,
         other: &FpVar<F>,
@@ -29,6 +30,7 @@ /// constraint system will not be satisfied otherwise. If `self` should
     /// also be checked for equality, e.g. `self <= other` instead of `self < other`, set
     /// `should_also_check_quality` to `true`. This variant assumes `self` and `other`
     /// are `<= (p-1)/2` and does not generate constraints to verify that.
+    #[tracing::instrument(target = "r1cs")]
     pub fn enforce_cmp_unchecked(
         &self,
         other: &FpVar<F>,
@@ -45,6 +47,7 @@ /// constraint system will be satisfied in any case. If `self` should
     /// also be checked for equality, e.g. `self <= other` instead of `self < other`, set
     /// `should_also_check_quality` to `true`. This variant verifies `self` and `other`
     /// are `<= (p-1)/2`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn is_cmp(
         &self,
         other: &FpVar<F>,
@@ -61,6 +64,7 @@ /// constraint system will be satisfied in any case. If `self` should
     /// also be checked for equality, e.g. `self <= other` instead of `self < other`, set
     /// `should_also_check_quality` to `true`. This variant assumes `self` and `other`
     /// are `<= (p-1)/2` and does not generate constraints to verify that.
+    #[tracing::instrument(target = "r1cs")]
     pub fn is_cmp_unchecked(
         &self,
         other: &FpVar<F>,
@@ -92,6 +96,7 @@ Ok((left.clone(), right_for_check))
     }
 
     // Helper function to enforce `self <= (p-1)/2`.
+    #[tracing::instrument(target = "r1cs")]
     pub fn enforce_smaller_or_equal_than_mod_minus_one_div_two(
         &self,
     ) -> Result<(), SynthesisError> {
@@ -172,9 +177,9 @@ }
         for i in 0..10 {
             let cs = ConstraintSystem::<Fr>::new_ref();
             let a = rand_in_range(&mut rng);
-            let a_var = FpVar::<Fr>::new_witness(cs.ns("a"), || Ok(a)).unwrap();
+            let a_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(a)).unwrap();
             let b = rand_in_range(&mut rng);
-            let b_var = FpVar::<Fr>::new_witness(cs.ns("b"), || Ok(b)).unwrap();
+            let b_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(b)).unwrap();
 
             match a.cmp(&b) {
                 Ordering::Less => {
@@ -198,9 +203,9 @@
         for _i in 0..10 {
             let cs = ConstraintSystem::<Fr>::new_ref();
             let a = rand_in_range(&mut rng);
-            let a_var = FpVar::<Fr>::new_witness(cs.ns("a"), || Ok(a)).unwrap();
+            let a_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(a)).unwrap();
             let b = rand_in_range(&mut rng);
-            let b_var = FpVar::<Fr>::new_witness(cs.ns("b"), || Ok(b)).unwrap();
+            let b_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(b)).unwrap();
 
             match b.cmp(&a) {
                 Ordering::Less => {
@@ -220,7 +225,7 @@
         for _i in 0..10 {
             let cs = ConstraintSystem::<Fr>::new_ref();
             let a = rand_in_range(&mut rng);
-            let a_var = FpVar::<Fr>::new_witness(cs.ns("a"), || Ok(a)).unwrap();
+            let a_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(a)).unwrap();
             a_var.enforce_cmp(&a_var, Ordering::Less, false).unwrap();
 
             assert!(!cs.is_satisfied().unwrap());
@@ -229,7 +234,7 @@
         for _i in 0..10 {
             let cs = ConstraintSystem::<Fr>::new_ref();
             let a = rand_in_range(&mut rng);
-            let a_var = FpVar::<Fr>::new_witness(cs.ns("a"), || Ok(a)).unwrap();
+            let a_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(a)).unwrap();
             a_var.enforce_cmp(&a_var, Ordering::Less, true).unwrap();
             assert!(cs.is_satisfied().unwrap());
         }

@@ -92,6 +92,7 @@ pub fn value(&self) -> Result<F, SynthesisError> {
         self.cs.assigned_value(self.variable).get()
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn add(&self, other: &Self) -> Self {
         let value = match (self.value, other.value) {
             (Some(val1), Some(val2)) => Some(val1 + &val2),
@@ -105,6 +106,7 @@ .unwrap();
         AllocatedFp::new(value, variable, self.cs.clone())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn sub(&self, other: &Self) -> Self {
         let value = match (self.value, other.value) {
             (Some(val1), Some(val2)) => Some(val1 - &val2),
@@ -118,6 +120,7 @@ .unwrap();
         AllocatedFp::new(value, variable, self.cs.clone())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn mul(&self, other: &Self) -> Self {
         let product = AllocatedFp::new_witness(self.cs.clone(), || {
             Ok(self.value.get()? * &other.value.get()?)
@@ -133,6 +136,7 @@ .unwrap();
         product
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn add_constant(&self, other: F) -> Self {
         if other.is_zero() {
             self.clone()
@@ -146,10 +150,12 @@ AllocatedFp::new(value, variable, self.cs.clone())
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn sub_constant(&self, other: F) -> Self {
         self.add_constant(-other)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn mul_constant(&self, other: F) -> Self {
         if other.is_one() {
             self.clone()
@@ -160,31 +166,33 @@ AllocatedFp::new(value, variable, self.cs.clone())
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn double(&self) -> Result<Self, SynthesisError> {
         let value = self.value.map(|val| val.double());
         let variable = self.cs.new_lc(lc!() + self.variable + self.variable)?;
         Ok(Self::new(value, variable, self.cs.clone()))
     }
 
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     pub fn negate(&self) -> Self {
         let mut result = self.clone();
         result.negate_in_place();
         result
     }
 
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     pub fn negate_in_place(&mut self) -> &mut Self {
         self.value.as_mut().map(|val| *val = -(*val));
         self.variable = self.cs.new_lc(lc!() - self.variable).unwrap();
         self
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn square(&self) -> Result<Self, SynthesisError> {
         Ok(self.mul(self))
     }
 
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     pub fn inverse(&self) -> Result<Self, SynthesisError> {
         let inverse = Self::new_witness(self.cs.clone(), || {
             Ok(self.value.get()?.inverse().unwrap_or(F::zero()))
@@ -198,10 +206,12 @@ )?;
         Ok(inverse)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn frobenius_map(&self, _: usize) -> Result<Self, SynthesisError> {
         Ok(self.clone())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
         self.cs.enforce_constraint(
             lc!() + self.variable,
@@ -210,6 +220,7 @@ lc!() + result.variable,
         )
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn square_equals(&self, result: &Self) -> Result<(), SynthesisError> {
         self.cs.enforce_constraint(
             lc!() + self.variable,
@@ -223,6 +234,7 @@ ///
     /// # Constraint cost
     ///
     /// Consumes three constraints
+    #[tracing::instrument(target = "r1cs")]
     pub fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
         Ok(self.is_neq(other)?.not())
     }
@@ -232,6 +244,7 @@ ///
     /// # Constraint cost
     ///
     /// Consumes three constraints
+    #[tracing::instrument(target = "r1cs")]
     pub fn is_neq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
         let is_not_equal = Boolean::new_witness(self.cs.clone(), || {
             Ok(self.value.get()? != other.value.get()?)
@@ -298,7 +311,7 @@ )?;
         Ok(is_not_equal)
     }
 
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     pub fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -311,7 +324,7 @@ lc!(),
         )
     }
 
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     pub fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -340,12 +353,14 @@
 impl<F: PrimeField> ToBitsGadget<F> for AllocatedFp<F> {
     /// Outputs the unique bit-wise decomposition of `self` in *little-endian*
     /// form.
+    #[tracing::instrument(target = "r1cs")]
     fn to_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
         let bits = self.to_non_unique_bits_le()?;
         Boolean::enforce_in_field_le(&bits)?;
         Ok(bits)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
         let cs = self.cs.clone();
         use algebra::BitIteratorBE;
@@ -390,6 +405,7 @@
 impl<F: PrimeField> ToBytesGadget<F> for AllocatedFp<F> {
     /// Outputs the unique byte decomposition of `self` in *little-endian*
     /// form.
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
         let num_bits = F::BigInt::NUM_LIMBS * 64;
         let mut bits = self.to_bits_le()?;
@@ -402,6 +418,7 @@ .collect();
         Ok(bytes)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
         let num_bits = F::BigInt::NUM_LIMBS * 64;
         let mut bits = self.to_non_unique_bits_le()?;
@@ -417,6 +434,7 @@ }
 
 impl<F: PrimeField> CondSelectGadget<F> for AllocatedFp<F> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditionally_select(
         cond: &Boolean<F>,
         true_val: &Self,
@@ -452,6 +470,7 @@ /// Uses two bits to perform a lookup into a table
 /// `b` is little-endian: `b[0]` is LSB.
 impl<F: PrimeField> TwoBitLookupGadget<F> for AllocatedFp<F> {
     type TableConstant = F;
+    #[tracing::instrument(target = "r1cs")]
     fn two_bit_lookup(b: &[Boolean<F>], c: &[Self::TableConstant]) -> Result<Self, SynthesisError> {
         debug_assert_eq!(b.len(), 2);
         debug_assert_eq!(c.len(), 4);
@@ -479,6 +498,7 @@
 impl<F: PrimeField> ThreeBitCondNegLookupGadget<F> for AllocatedFp<F> {
     type TableConstant = F;
 
+    #[tracing::instrument(target = "r1cs")]
     fn three_bit_cond_neg_lookup(
         b: &[Boolean<F>],
         b0b1: &Boolean<F>,
@@ -561,6 +581,7 @@ fn one() -> Self {
         Self::Constant(F::one())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn double(&self) -> Result<Self, SynthesisError> {
         match self {
             Self::Constant(c) => Ok(Self::Constant(c.double())),
@@ -568,6 +589,7 @@ Self::Var(v) => Ok(Self::Var(v.double()?)),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn negate(&self) -> Result<Self, SynthesisError> {
         match self {
             Self::Constant(c) => Ok(Self::Constant(-*c)),
@@ -575,6 +597,7 @@ Self::Var(v) => Ok(Self::Var(v.negate())),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn square(&self) -> Result<Self, SynthesisError> {
         match self {
             Self::Constant(c) => Ok(Self::Constant(c.square())),
@@ -583,6 +606,7 @@ }
     }
 
     /// Enforce that `self * other == result`.
+    #[tracing::instrument(target = "r1cs")]
     fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
         use FpVar::*;
         match (self, other, result) {
@@ -600,6 +624,7 @@ }
     }
 
     /// Enforce that `self * self == result`.
+    #[tracing::instrument(target = "r1cs")]
     fn square_equals(&self, result: &Self) -> Result<(), SynthesisError> {
         use FpVar::*;
         match (self, result) {
@@ -618,6 +643,7 @@ (Var(v1), Var(v2)) => v1.square_equals(v2),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn inverse(&self) -> Result<Self, SynthesisError> {
         match self {
             FpVar::Var(v) => v.inverse().map(FpVar::Var),
@@ -629,6 +655,7 @@ /// Returns (self / denominator), but requires fewer constraints than
     /// self * denominator.inverse()
     /// It is up to the caller to ensure that denominator is non-zero,
     /// since in that case the result is unconstrained.
+    #[tracing::instrument(target = "r1cs")]
     fn mul_by_inverse(&self, denominator: &Self) -> Result<Self, SynthesisError> {
         use FpVar::*;
         match (self, denominator) {
@@ -639,6 +666,7 @@ (Var(s), Var(d)) => Ok(Var(d.inverse()?.mul(s))),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn frobenius_map(&self, power: usize) -> Result<Self, SynthesisError> {
         match self {
             FpVar::Var(v) => v.frobenius_map(power).map(FpVar::Var),
@@ -650,6 +678,7 @@ }
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn frobenius_map_in_place(&mut self, power: usize) -> Result<&mut Self, SynthesisError> {
         *self = self.frobenius_map(power)?;
         Ok(self)
@@ -727,6 +756,7 @@ /****************************************************************************/
 /****************************************************************************/
 
 impl<F: PrimeField> EqGadget<F> for FpVar<F> {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
         match (self, other) {
             (Self::Constant(c1), Self::Constant(c2)) => Ok(Boolean::Constant(c1 == c2)),
@@ -739,7 +769,7 @@ (Self::Var(v1), Self::Var(v2)) => v1.is_eq(v2),
         }
     }
 
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -756,7 +786,7 @@ (Self::Var(v1), Self::Var(v2)) => v1.conditional_enforce_equal(v2, should_enforce),
         }
     }
 
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -775,6 +805,7 @@ }
 }
 
 impl<F: PrimeField> ToBitsGadget<F> for FpVar<F> {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
         match self {
             Self::Constant(_) => self.to_non_unique_bits_le(),
@@ -782,6 +813,7 @@ Self::Var(v) => v.to_bits_le(),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bits_le(&self) -> Result<Vec<Boolean<F>>, SynthesisError> {
         use algebra::BitIteratorLE;
         match self {
@@ -796,6 +828,7 @@
 impl<F: PrimeField> ToBytesGadget<F> for FpVar<F> {
     /// Outputs the unique byte decomposition of `self` in *little-endian*
     /// form.
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
         match self {
             Self::Constant(c) => Ok(UInt8::constant_vec(&to_bytes![c].unwrap())),
@@ -803,6 +836,7 @@ Self::Var(v) => v.to_bytes(),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<F>>, SynthesisError> {
         match self {
             Self::Constant(c) => Ok(UInt8::constant_vec(&to_bytes![c].unwrap())),
@@ -812,7 +846,7 @@ }
 }
 
 impl<F: PrimeField> CondSelectGadget<F> for FpVar<F> {
-    #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditionally_select(
         cond: &Boolean<F>,
         true_value: &Self,
@@ -852,6 +886,7 @@ /// `b` is little-endian: `b[0]` is LSB.
 impl<F: PrimeField> TwoBitLookupGadget<F> for FpVar<F> {
     type TableConstant = F;
 
+    #[tracing::instrument(target = "r1cs")]
     fn two_bit_lookup(b: &[Boolean<F>], c: &[Self::TableConstant]) -> Result<Self, SynthesisError> {
         debug_assert_eq!(b.len(), 2);
         debug_assert_eq!(c.len(), 4);
@@ -869,6 +904,7 @@
 impl<F: PrimeField> ThreeBitCondNegLookupGadget<F> for FpVar<F> {
     type TableConstant = F;
 
+    #[tracing::instrument(target = "r1cs")]
     fn three_bit_cond_neg_lookup(
         b: &[Boolean<F>],
         b0b1: &Boolean<F>,

@@ -181,9 +181,9 @@
         let mut rng = test_rng();
         let a_native = F::rand(&mut rng);
         let b_native = F::rand(&mut rng);
-        let a = AF::new_witness(cs.ns("generate_a"), || Ok(a_native))?;
-        let b = AF::new_witness(cs.ns("generate_b"), || Ok(b_native))?;
-        let b_const = AF::new_constant(cs.ns("b_as_constant"), b_native)?;
+        let a = AF::new_witness(r1cs_core::ns!(cs, "generate_a"), || Ok(a_native))?;
+        let b = AF::new_witness(r1cs_core::ns!(cs, "generate_b"), || Ok(b_native))?;
+        let b_const = AF::new_constant(r1cs_core::ns!(cs, "b_as_constant"), b_native)?;
 
         let zero = AF::zero();
         let zero_native = zero.value()?;
@@ -318,13 +318,13 @@ assert!(cs.is_satisfied().unwrap());
 
         let f = F::from(1u128 << 64);
         let f_bits = algebra::BitIteratorLE::new(&[0u64, 1u64]).collect::<Vec<_>>();
-        let fv = AF::new_witness(cs.ns("alloc u128"), || Ok(f))?;
+        let fv = AF::new_witness(r1cs_core::ns!(cs, "alloc u128"), || Ok(f))?;
         assert_eq!(fv.to_bits_le()?.value().unwrap()[..128], f_bits[..128]);
         assert!(cs.is_satisfied().unwrap());
 
         let r_native: F = UniformRand::rand(&mut test_rng());
 
-        let r = AF::new_witness(cs.ns("r_native"), || Ok(r_native)).unwrap();
+        let r = AF::new_witness(r1cs_core::ns!(cs, "r_native"), || Ok(r_native)).unwrap();
         let _ = r.to_non_unique_bits_le()?;
         assert!(cs.is_satisfied().unwrap());
         let _ = r.to_bits_le()?;
@@ -369,7 +369,7 @@ let cs = ConstraintSystem::<ConstraintF>::new_ref();
         let mut rng = XorShiftRng::seed_from_u64(1231275789u64);
         for i in 0..=maxpower {
             let mut a = F::rand(&mut rng);
-            let mut a_gadget = AF::new_witness(cs.ns(format!("a_gadget_{:?}", i)), || Ok(a))?;
+            let mut a_gadget = AF::new_witness(r1cs_core::ns!(cs, "a"), || Ok(a))?;
             a_gadget.frobenius_map_in_place(i)?;
             a.frobenius_map(i);
 

@@ -70,6 +70,7 @@ }
 
     /// This is only to be used when the element is *known* to be in the cyclotomic subgroup.
     #[inline]
+    #[tracing::instrument(target = "r1cs", skip(exponent))]
     pub fn cyclotomic_exp(&self, exponent: impl AsRef<[u64]>) -> Result<Self, SynthesisError>
     where
         Self: FieldVar<QuadExtField<P>, P::BasePrimeField>,
@@ -175,6 +176,7 @@ Self::new(c0, c1)
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn double(&self) -> Result<Self, SynthesisError> {
         let c0 = self.c0.double()?;
         let c1 = self.c1.double()?;
@@ -182,6 +184,7 @@ Ok(Self::new(c0, c1))
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn negate(&self) -> Result<Self, SynthesisError> {
         let mut result = self.clone();
         result.c0.negate_in_place()?;
@@ -190,6 +193,7 @@ Ok(result)
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn square(&self) -> Result<Self, SynthesisError> {
         // From Libsnark/fp2_gadget.tcc
         // Complex multiplication for Fp2:
@@ -213,6 +217,7 @@
         Ok(Self::new(c0, c1))
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn mul_equals(&self, other: &Self, result: &Self) -> Result<(), SynthesisError> {
         // Karatsuba multiplication for Fp2:
         //     v0 = A.c0 * B.c0
@@ -245,6 +250,7 @@
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn frobenius_map(&self, power: usize) -> Result<Self, SynthesisError> {
         let mut result = self.clone();
         result.c0.frobenius_map_in_place(power)?;
@@ -253,6 +259,7 @@ P::mul_base_field_var_by_frob_coeff(&mut result.c1, power);
         Ok(result)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn inverse(&self) -> Result<Self, SynthesisError> {
         let one = Self::new_constant(self.cs().get()?.clone(), QuadExtField::one())?;
         let inverse = Self::new_witness(self.cs().get()?.clone(), || {
@@ -344,6 +351,7 @@ BF: FieldVar<P::BaseField, P::BasePrimeField>,
     for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
     P: QuadExtVarParams<BF>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(&self, other: &Self) -> Result<Boolean<P::BasePrimeField>, SynthesisError> {
         let b0 = self.c0.is_eq(&other.c0)?;
         let b1 = self.c1.is_eq(&other.c1)?;
@@ -351,6 +359,7 @@ b0.and(&b1)
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -362,6 +371,7 @@ Ok(())
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -380,6 +390,7 @@ BF: FieldVar<P::BaseField, P::BasePrimeField>,
     for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
     P: QuadExtVarParams<BF>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bits_le(&self) -> Result<Vec<Boolean<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_bits_le()?;
         let mut c1 = self.c1.to_bits_le()?;
@@ -387,6 +398,7 @@ c0.append(&mut c1);
         Ok(c0)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bits_le(&self) -> Result<Vec<Boolean<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_non_unique_bits_le()?;
         let mut c1 = self.c1.to_non_unique_bits_le()?;
@@ -401,6 +413,7 @@ BF: FieldVar<P::BaseField, P::BasePrimeField>,
     for<'b> &'b BF: FieldOpsBounds<'b, P::BaseField, BF>,
     P: QuadExtVarParams<BF>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_bytes()?;
         let mut c1 = self.c1.to_bytes()?;
@@ -408,6 +421,7 @@ c0.append(&mut c1);
         Ok(c0)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::BasePrimeField>>, SynthesisError> {
         let mut c0 = self.c0.to_non_unique_bytes()?;
         let mut c1 = self.c1.to_non_unique_bytes()?;
@@ -443,6 +457,7 @@ P: QuadExtVarParams<BF>,
 {
     type TableConstant = QuadExtField<P>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn two_bit_lookup(
         b: &[Boolean<P::BasePrimeField>],
         c: &[Self::TableConstant],
@@ -464,6 +479,7 @@ P: QuadExtVarParams<BF>,
 {
     type TableConstant = QuadExtField<P>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn three_bit_cond_neg_lookup(
         b: &[Boolean<P::BasePrimeField>],
         b0b1: &Boolean<P::BasePrimeField>,
@@ -498,8 +514,8 @@ Err(SynthesisError::AssignmentMissing),
             ),
         };
 
-        let c0 = BF::new_variable(cs.ns("c0"), || c0, mode)?;
-        let c1 = BF::new_variable(cs.ns("c1"), || c1, mode)?;
+        let c0 = BF::new_variable(r1cs_core::ns!(cs, "c0"), || c0, mode)?;
+        let c1 = BF::new_variable(r1cs_core::ns!(cs, "c1"), || c1, mode)?;
         Ok(Self::new(c0, c1))
     }
 }

@@ -6,7 +6,7 @@ },
     fields::Field,
     BitIteratorBE, One,
 };
-use r1cs_core::SynthesisError;
+use r1cs_core::{Namespace, SynthesisError};
 
 use crate::{
     fields::{fp::FpVar, fp2::Fp2Var, FieldVar},
@@ -53,9 +53,13 @@ let ns = cs.into();
         let cs = ns.cs();
         let g1_prep = f().map(|b| b.borrow().0);
 
-        let x = FpVar::new_variable(cs.ns("x"), || g1_prep.map(|g| g.x), mode)?;
-        let y = FpVar::new_variable(cs.ns("y"), || g1_prep.map(|g| g.y), mode)?;
-        let infinity = Boolean::new_variable(cs.ns("inf"), || g1_prep.map(|g| g.infinity), mode)?;
+        let x = FpVar::new_variable(r1cs_core::ns!(cs, "x"), || g1_prep.map(|g| g.x), mode)?;
+        let y = FpVar::new_variable(r1cs_core::ns!(cs, "y"), || g1_prep.map(|g| g.y), mode)?;
+        let infinity = Boolean::new_variable(
+            r1cs_core::ns!(cs, "inf"),
+            || g1_prep.map(|g| g.infinity),
+            mode,
+        )?;
         let g = AffineVar::new(x, y, infinity);
         Ok(Self(g))
     }
@@ -63,6 +67,7 @@ }
 
 impl<P: Bls12Parameters> ToBytesGadget<P::Fp> for G1PreparedVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut bytes = self.0.x.to_bytes()?;
         let y_bytes = self.0.y.to_bytes()?;
@@ -72,6 +77,7 @@ bytes.extend_from_slice(&inf_bytes);
         Ok(bytes)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut bytes = self.0.x.to_bytes()?;
         let y_bytes = self.0.y.to_bytes()?;
@@ -94,6 +100,7 @@ pub ell_coeffs: Vec<LCoeff<P>>,
 }
 
 impl<P: Bls12Parameters> AllocVar<G2Prepared<P>, P::Fp> for G2PreparedVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f, mode))]
     fn new_variable<T: Borrow<G2Prepared<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -116,7 +123,7 @@ .collect::<Vec<_>>()
         });
 
         let l = Vec::new_variable(
-            cs.ns("l"),
+            r1cs_core::ns!(cs, "l"),
             || {
                 g2_prep
                     .clone()
@@ -125,7 +132,7 @@ },
             mode,
         )?;
         let r = Vec::new_variable(
-            cs.ns("r"),
+            r1cs_core::ns!(cs, "r"),
             || g2_prep.map(|c| c.iter().map(|(_, r)| *r).collect::<Vec<_>>()),
             mode,
         )?;
@@ -136,6 +143,7 @@ }
 
 impl<P: Bls12Parameters> ToBytesGadget<P::Fp> for G2PreparedVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut bytes = Vec::new();
         for coeffs in &self.ell_coeffs {
@@ -145,6 +153,7 @@ }
         Ok(bytes)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut bytes = Vec::new();
         for coeffs in &self.ell_coeffs {
@@ -156,6 +165,7 @@ }
 }
 
 impl<P: Bls12Parameters> G2PreparedVar<P> {
+    #[tracing::instrument(target = "r1cs")]
     pub fn from_group_var(q: &G2Var<P>) -> Result<Self, SynthesisError> {
         let q = q.to_affine()?;
         let two_inv = P::Fp::one().double().inverse().unwrap();
@@ -175,6 +185,7 @@
         Ok(Self { ell_coeffs })
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn double(r: &mut G2AffineVar<P>, two_inv: &P::Fp) -> Result<LCoeff<P>, SynthesisError> {
         let a = r.y.inverse()?;
         let mut b = r.x.square()?;
@@ -198,6 +209,7 @@ TwistType::D => Ok((f, e)),
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn add(r: &mut G2AffineVar<P>, q: &G2AffineVar<P>) -> Result<LCoeff<P>, SynthesisError> {
         let a = (&q.x - &r.x).inverse()?;
         let b = &q.y - &r.y;

@@ -31,6 +31,7 @@ pub y_twist: Fp2Var<P::Fp2Params>,
 }
 
 impl<P: MNT4Parameters> AllocVar<G1Prepared<P>, P::Fp> for G1PreparedVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<G1Prepared<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -41,10 +42,18 @@ let cs = ns.cs();
 
         let g1_prep = f().map(|b| *b.borrow());
 
-        let x = FpVar::new_variable(cs.ns("x"), || g1_prep.map(|g| g.x), mode)?;
-        let y = FpVar::new_variable(cs.ns("y"), || g1_prep.map(|g| g.y), mode)?;
-        let x_twist = Fp2Var::new_variable(cs.ns("x_twist"), || g1_prep.map(|g| g.x_twist), mode)?;
-        let y_twist = Fp2Var::new_variable(cs.ns("y_twist"), || g1_prep.map(|g| g.y_twist), mode)?;
+        let x = FpVar::new_variable(r1cs_core::ns!(cs, "x"), || g1_prep.map(|g| g.x), mode)?;
+        let y = FpVar::new_variable(r1cs_core::ns!(cs, "y"), || g1_prep.map(|g| g.y), mode)?;
+        let x_twist = Fp2Var::new_variable(
+            r1cs_core::ns!(cs, "x_twist"),
+            || g1_prep.map(|g| g.x_twist),
+            mode,
+        )?;
+        let y_twist = Fp2Var::new_variable(
+            r1cs_core::ns!(cs, "y_twist"),
+            || g1_prep.map(|g| g.y_twist),
+            mode,
+        )?;
         Ok(Self {
             x,
             y,
@@ -70,6 +79,7 @@ y_twist,
         })
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn from_group_var(q: &G1Var<P>) -> Result<Self, SynthesisError> {
         let q = q.to_affine()?;
         let x_twist = Fp2Var::new(&q.x * P::TWIST.c0, &q.x * P::TWIST.c1);
@@ -85,6 +95,7 @@ }
 
 impl<P: MNT4Parameters> ToBytesGadget<P::Fp> for G1PreparedVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_bytes()?;
         let mut y = self.y.to_bytes()?;
@@ -97,6 +108,7 @@ x.append(&mut y_twist);
         Ok(x)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_non_unique_bytes()?;
         let mut y = self.y.to_non_unique_bytes()?;
@@ -124,6 +136,7 @@ pub addition_coefficients: Vec<AteAdditionCoefficientsVar<P>>,
 }
 
 impl<P: MNT4Parameters> AllocVar<G2Prepared<P>, P::Fp> for G2PreparedVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<G2Prepared<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -135,19 +148,25 @@
         let g2_prep = f().map(|b| b.borrow().clone());
         let g2 = g2_prep.as_ref().map_err(|e| *e);
 
-        let x = Fp2Var::new_variable(cs.ns("x"), || g2.map(|g| g.x), mode)?;
-        let y = Fp2Var::new_variable(cs.ns("y"), || g2.map(|g| g.y), mode)?;
-        let x_over_twist =
-            Fp2Var::new_variable(cs.ns("x_over_twist"), || g2.map(|g| g.x_over_twist), mode)?;
-        let y_over_twist =
-            Fp2Var::new_variable(cs.ns("y_over_twist"), || g2.map(|g| g.y_over_twist), mode)?;
+        let x = Fp2Var::new_variable(r1cs_core::ns!(cs, "x"), || g2.map(|g| g.x), mode)?;
+        let y = Fp2Var::new_variable(r1cs_core::ns!(cs, "y"), || g2.map(|g| g.y), mode)?;
+        let x_over_twist = Fp2Var::new_variable(
+            r1cs_core::ns!(cs, "x_over_twist"),
+            || g2.map(|g| g.x_over_twist),
+            mode,
+        )?;
+        let y_over_twist = Fp2Var::new_variable(
+            r1cs_core::ns!(cs, "y_over_twist"),
+            || g2.map(|g| g.y_over_twist),
+            mode,
+        )?;
         let double_coefficients = Vec::new_variable(
-            cs.ns("double coeffs"),
+            r1cs_core::ns!(cs, "double coeffs"),
             || g2.map(|g| g.double_coefficients.clone()),
             mode,
         )?;
         let addition_coefficients = Vec::new_variable(
-            cs.ns("add coeffs"),
+            r1cs_core::ns!(cs, "add coeffs"),
             || g2.map(|g| g.addition_coefficients.clone()),
             mode,
         )?;
@@ -164,6 +183,7 @@ }
 
 impl<P: MNT4Parameters> ToBytesGadget<P::Fp> for G2PreparedVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_bytes()?;
         let mut y = self.y.to_bytes()?;
@@ -183,6 +203,7 @@ }
         Ok(x)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_non_unique_bytes()?;
         let mut y = self.y.to_non_unique_bytes()?;
@@ -229,6 +250,7 @@ addition_coefficients,
         })
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn from_group_var(q: &G2Var<P>) -> Result<Self, SynthesisError> {
         let twist_inv = P::TWIST.inverse().unwrap();
         let q = q.to_affine()?;
@@ -308,6 +330,7 @@ pub c_l: Fp2Var<P::Fp2Params>,
 }
 
 impl<P: MNT4Parameters> AllocVar<AteDoubleCoefficients<P>, P::Fp> for AteDoubleCoefficientsVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<AteDoubleCoefficients<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -319,10 +342,10 @@
         let c_prep = f().map(|c| c.borrow().clone());
         let c = c_prep.as_ref().map_err(|e| *e);
 
-        let c_h = Fp2Var::new_variable(cs.ns("c_h"), || c.map(|c| c.c_h), mode)?;
-        let c_4c = Fp2Var::new_variable(cs.ns("c_4c"), || c.map(|c| c.c_4c), mode)?;
-        let c_j = Fp2Var::new_variable(cs.ns("c_j"), || c.map(|c| c.c_j), mode)?;
-        let c_l = Fp2Var::new_variable(cs.ns("c_l"), || c.map(|c| c.c_l), mode)?;
+        let c_h = Fp2Var::new_variable(r1cs_core::ns!(cs, "c_h"), || c.map(|c| c.c_h), mode)?;
+        let c_4c = Fp2Var::new_variable(r1cs_core::ns!(cs, "c_4c"), || c.map(|c| c.c_4c), mode)?;
+        let c_j = Fp2Var::new_variable(r1cs_core::ns!(cs, "c_j"), || c.map(|c| c.c_j), mode)?;
+        let c_l = Fp2Var::new_variable(r1cs_core::ns!(cs, "c_l"), || c.map(|c| c.c_l), mode)?;
         Ok(Self {
             c_h,
             c_4c,
@@ -334,6 +357,7 @@ }
 
 impl<P: MNT4Parameters> ToBytesGadget<P::Fp> for AteDoubleCoefficientsVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_h = self.c_h.to_bytes()?;
         let mut c_4c = self.c_4c.to_bytes()?;
@@ -346,6 +370,7 @@ c_h.append(&mut c_l);
         Ok(c_h)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_h = self.c_h.to_non_unique_bytes()?;
         let mut c_4c = self.c_4c.to_non_unique_bytes()?;
@@ -386,6 +411,7 @@
 impl<P: MNT4Parameters> AllocVar<AteAdditionCoefficients<P>, P::Fp>
     for AteAdditionCoefficientsVar<P>
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<AteAdditionCoefficients<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -397,14 +423,15 @@
         let c_prep = f().map(|c| c.borrow().clone());
         let c = c_prep.as_ref().map_err(|e| *e);
 
-        let c_l1 = Fp2Var::new_variable(cs.ns("c_l1"), || c.map(|c| c.c_l1), mode)?;
-        let c_rz = Fp2Var::new_variable(cs.ns("c_rz"), || c.map(|c| c.c_rz), mode)?;
+        let c_l1 = Fp2Var::new_variable(r1cs_core::ns!(cs, "c_l1"), || c.map(|c| c.c_l1), mode)?;
+        let c_rz = Fp2Var::new_variable(r1cs_core::ns!(cs, "c_rz"), || c.map(|c| c.c_rz), mode)?;
         Ok(Self { c_l1, c_rz })
     }
 }
 
 impl<P: MNT4Parameters> ToBytesGadget<P::Fp> for AteAdditionCoefficientsVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_l1 = self.c_l1.to_bytes()?;
         let mut c_rz = self.c_rz.to_bytes()?;
@@ -413,6 +440,7 @@ c_l1.append(&mut c_rz);
         Ok(c_l1)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_l1 = self.c_l1.to_non_unique_bytes()?;
         let mut c_rz = self.c_rz.to_non_unique_bytes()?;

@@ -44,6 +44,7 @@ y_twist,
         })
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn from_group_var(q: &G1Var<P>) -> Result<Self, SynthesisError> {
         let q = q.to_affine()?;
         let zero = FpVar::<P::Fp>::zero();
@@ -60,6 +61,7 @@ }
 }
 
 impl<P: MNT6Parameters> AllocVar<G1Prepared<P>, P::Fp> for G1PreparedVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<G1Prepared<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -70,10 +72,18 @@ let cs = ns.cs();
 
         let g1_prep = f().map(|b| *b.borrow());
 
-        let x = FpVar::new_variable(cs.ns("x"), || g1_prep.map(|g| g.x), mode)?;
-        let y = FpVar::new_variable(cs.ns("y"), || g1_prep.map(|g| g.y), mode)?;
-        let x_twist = Fp3Var::new_variable(cs.ns("x_twist"), || g1_prep.map(|g| g.x_twist), mode)?;
-        let y_twist = Fp3Var::new_variable(cs.ns("y_twist"), || g1_prep.map(|g| g.y_twist), mode)?;
+        let x = FpVar::new_variable(r1cs_core::ns!(cs, "x"), || g1_prep.map(|g| g.x), mode)?;
+        let y = FpVar::new_variable(r1cs_core::ns!(cs, "y"), || g1_prep.map(|g| g.y), mode)?;
+        let x_twist = Fp3Var::new_variable(
+            r1cs_core::ns!(cs, "x_twist"),
+            || g1_prep.map(|g| g.x_twist),
+            mode,
+        )?;
+        let y_twist = Fp3Var::new_variable(
+            r1cs_core::ns!(cs, "y_twist"),
+            || g1_prep.map(|g| g.y_twist),
+            mode,
+        )?;
         Ok(Self {
             x,
             y,
@@ -85,6 +95,7 @@ }
 
 impl<P: MNT6Parameters> ToBytesGadget<P::Fp> for G1PreparedVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_bytes()?;
         let mut y = self.y.to_bytes()?;
@@ -97,6 +108,7 @@ x.append(&mut y_twist);
         Ok(x)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_non_unique_bytes()?;
         let mut y = self.y.to_non_unique_bytes()?;
@@ -123,6 +135,7 @@ pub addition_coefficients: Vec<AteAdditionCoefficientsVar<P>>,
 }
 
 impl<P: MNT6Parameters> AllocVar<G2Prepared<P>, P::Fp> for G2PreparedVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<G2Prepared<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -134,19 +147,25 @@
         let g2_prep = f().map(|b| b.borrow().clone());
         let g2 = g2_prep.as_ref().map_err(|e| *e);
 
-        let x = Fp3Var::new_variable(cs.ns("x"), || g2.map(|g| g.x), mode)?;
-        let y = Fp3Var::new_variable(cs.ns("y"), || g2.map(|g| g.y), mode)?;
-        let x_over_twist =
-            Fp3Var::new_variable(cs.ns("x_over_twist"), || g2.map(|g| g.x_over_twist), mode)?;
-        let y_over_twist =
-            Fp3Var::new_variable(cs.ns("y_over_twist"), || g2.map(|g| g.y_over_twist), mode)?;
+        let x = Fp3Var::new_variable(r1cs_core::ns!(cs, "x"), || g2.map(|g| g.x), mode)?;
+        let y = Fp3Var::new_variable(r1cs_core::ns!(cs, "y"), || g2.map(|g| g.y), mode)?;
+        let x_over_twist = Fp3Var::new_variable(
+            r1cs_core::ns!(cs, "x_over_twist"),
+            || g2.map(|g| g.x_over_twist),
+            mode,
+        )?;
+        let y_over_twist = Fp3Var::new_variable(
+            r1cs_core::ns!(cs, "y_over_twist"),
+            || g2.map(|g| g.y_over_twist),
+            mode,
+        )?;
         let double_coefficients = Vec::new_variable(
-            cs.ns("double coeffs"),
+            r1cs_core::ns!(cs, "double coeffs"),
             || g2.map(|g| g.double_coefficients.clone()),
             mode,
         )?;
         let addition_coefficients = Vec::new_variable(
-            cs.ns("add coeffs"),
+            r1cs_core::ns!(cs, "add coeffs"),
             || g2.map(|g| g.addition_coefficients.clone()),
             mode,
         )?;
@@ -163,6 +182,7 @@ }
 
 impl<P: MNT6Parameters> ToBytesGadget<P::Fp> for G2PreparedVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_bytes()?;
         let mut y = self.y.to_bytes()?;
@@ -182,6 +202,7 @@ }
         Ok(x)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut x = self.x.to_non_unique_bytes()?;
         let mut y = self.y.to_non_unique_bytes()?;
@@ -228,6 +249,7 @@ addition_coefficients,
         })
     }
 
+    #[tracing::instrument(target = "r1cs")]
     pub fn from_group_var(q: &G2Var<P>) -> Result<Self, SynthesisError> {
         let q = q.to_affine()?;
         let twist_inv = P::TWIST.inverse().unwrap();
@@ -307,6 +329,7 @@ pub c_l: Fp3Var<P::Fp3Params>,
 }
 
 impl<P: MNT6Parameters> AllocVar<AteDoubleCoefficients<P>, P::Fp> for AteDoubleCoefficientsVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<AteDoubleCoefficients<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -318,10 +341,10 @@
         let c_prep = f().map(|c| c.borrow().clone());
         let c = c_prep.as_ref().map_err(|e| *e);
 
-        let c_h = Fp3Var::new_variable(cs.ns("c_h"), || c.map(|c| c.c_h), mode)?;
-        let c_4c = Fp3Var::new_variable(cs.ns("c_4c"), || c.map(|c| c.c_4c), mode)?;
-        let c_j = Fp3Var::new_variable(cs.ns("c_j"), || c.map(|c| c.c_j), mode)?;
-        let c_l = Fp3Var::new_variable(cs.ns("c_l"), || c.map(|c| c.c_l), mode)?;
+        let c_h = Fp3Var::new_variable(r1cs_core::ns!(cs, "c_h"), || c.map(|c| c.c_h), mode)?;
+        let c_4c = Fp3Var::new_variable(r1cs_core::ns!(cs, "c_4c"), || c.map(|c| c.c_4c), mode)?;
+        let c_j = Fp3Var::new_variable(r1cs_core::ns!(cs, "c_j"), || c.map(|c| c.c_j), mode)?;
+        let c_l = Fp3Var::new_variable(r1cs_core::ns!(cs, "c_l"), || c.map(|c| c.c_l), mode)?;
         Ok(Self {
             c_h,
             c_4c,
@@ -333,6 +356,7 @@ }
 
 impl<P: MNT6Parameters> ToBytesGadget<P::Fp> for AteDoubleCoefficientsVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_h = self.c_h.to_bytes()?;
         let mut c_4c = self.c_4c.to_bytes()?;
@@ -345,6 +369,7 @@ c_h.append(&mut c_l);
         Ok(c_h)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_h = self.c_h.to_non_unique_bytes()?;
         let mut c_4c = self.c_4c.to_non_unique_bytes()?;
@@ -383,6 +408,7 @@
 impl<P: MNT6Parameters> AllocVar<AteAdditionCoefficients<P>, P::Fp>
     for AteAdditionCoefficientsVar<P>
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<T: Borrow<AteAdditionCoefficients<P>>>(
         cs: impl Into<Namespace<P::Fp>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -394,14 +420,15 @@
         let c_prep = f().map(|c| c.borrow().clone());
         let c = c_prep.as_ref().map_err(|e| *e);
 
-        let c_l1 = Fp3Var::new_variable(cs.ns("c_l1"), || c.map(|c| c.c_l1), mode)?;
-        let c_rz = Fp3Var::new_variable(cs.ns("c_rz"), || c.map(|c| c.c_rz), mode)?;
+        let c_l1 = Fp3Var::new_variable(r1cs_core::ns!(cs, "c_l1"), || c.map(|c| c.c_l1), mode)?;
+        let c_rz = Fp3Var::new_variable(r1cs_core::ns!(cs, "c_rz"), || c.map(|c| c.c_rz), mode)?;
         Ok(Self { c_l1, c_rz })
     }
 }
 
 impl<P: MNT6Parameters> ToBytesGadget<P::Fp> for AteAdditionCoefficientsVar<P> {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_l1 = self.c_l1.to_bytes()?;
         let mut c_rz = self.c_rz.to_bytes()?;
@@ -410,6 +437,7 @@ c_l1.append(&mut c_rz);
         Ok(c_l1)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(&self) -> Result<Vec<UInt8<P::Fp>>, SynthesisError> {
         let mut c_l1 = self.c_l1.to_non_unique_bytes()?;
         let mut c_rz = self.c_rz.to_non_unique_bytes()?;

@@ -118,6 +118,7 @@ }
     }
 
     /// Convert this point into affine form.
+    #[tracing::instrument(target = "r1cs")]
     pub fn to_affine(&self) -> Result<AffineVar<P, F>, SynthesisError> {
         let cs = self.cs().unwrap_or(ConstraintSystemRef::None);
         let mode = if self.is_constant() {
@@ -131,7 +132,7 @@ let zero_x = F::zero();
         let zero_y = F::one();
 
         let non_zero_x = F::new_variable(
-            cs.ns("non-zero x"),
+            r1cs_core::ns!(cs, "non-zero x"),
             || {
                 let z_inv = self.z.value()?.inverse().unwrap_or(P::BaseField::zero());
                 Ok(self.x.value()? * &z_inv)
@@ -139,7 +140,7 @@ },
             mode,
         )?;
         let non_zero_y = F::new_variable(
-            cs.ns("non-zero y"),
+            r1cs_core::ns!(cs, "non-zero y"),
             || {
                 let z_inv = self.z.value()?.inverse().unwrap_or(P::BaseField::zero());
                 Ok(self.y.value()? * &z_inv)
@@ -154,6 +155,7 @@
     /// Allocates a new variable without performing an on-curve check, which is
     /// useful if the variable is known to be on the curve (eg., if the point
     /// is a constant or is a public input).
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     pub fn new_variable_omit_on_curve_check(
         cs: impl Into<Namespace<<P::BaseField as Field>::BasePrimeField>>,
         f: impl FnOnce() -> Result<SWProjective<P>, SynthesisError>,
@@ -182,9 +184,9 @@ Err(SynthesisError::AssignmentMissing),
             ),
         };
 
-        let x = F::new_variable(cs.ns("x"), || x, mode)?;
-        let y = F::new_variable(cs.ns("y"), || y, mode)?;
-        let z = F::new_variable(cs.ns("z"), || z, mode)?;
+        let x = F::new_variable(r1cs_core::ns!(cs, "x"), || x, mode)?;
+        let y = F::new_variable(r1cs_core::ns!(cs, "y"), || y, mode)?;
+        let z = F::new_variable(r1cs_core::ns!(cs, "z"), || z, mode)?;
 
         Ok(Self::new(x, y, z))
     }
@@ -210,6 +212,7 @@ fn is_zero(&self) -> Result<Boolean<<P::BaseField as Field>::BasePrimeField>, SynthesisError> {
         self.z.is_zero()
     }
 
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable_omit_prime_order_check(
         cs: impl Into<Namespace<<P::BaseField as Field>::BasePrimeField>>,
         f: impl FnOnce() -> Result<SWProjective<P>, SynthesisError>,
@@ -252,6 +255,7 @@ /// Does so by multiplying by the prime order, and checking that the result
     /// is unchanged.
     // TODO: at the moment this doesn't work, because the addition and doubling
     // formulae are incomplete for even-order points.
+    #[tracing::instrument(target = "r1cs")]
     fn enforce_prime_order(&self) -> Result<(), SynthesisError> {
         let r_minus_1 = (-P::ScalarField::one()).into_repr();
 
@@ -268,6 +272,7 @@ Ok(())
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn double_in_place(&mut self) -> Result<(), SynthesisError> {
         // Complete doubling formula from Renes-Costello-Batina 2015
         // Algorithm 3
@@ -306,6 +311,7 @@ self.z = z;
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn negate(&self) -> Result<Self, SynthesisError> {
         Ok(Self::new(self.x.clone(), self.y.negate()?, self.z.clone()))
     }
@@ -413,6 +419,7 @@ F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditionally_select(
         cond: &Boolean<<P::BaseField as Field>::BasePrimeField>,
         true_value: &Self,
@@ -432,6 +439,7 @@ P: SWModelParameters,
     F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(
         &self,
         other: &Self,
@@ -444,6 +452,7 @@ both_are_zero.or(&coordinates_equal)
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -460,6 +469,7 @@ Ok(())
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -534,7 +544,7 @@ // equals the identity.
 
                 let (mut ge, iter) = if cofactor_weight < modulus_minus_1_weight {
                     let ge = Self::new_variable_omit_prime_order_check(
-                        cs.ns("Witness without subgroup check with cofactor mul"),
+                        r1cs_core::ns!(cs, "Witness without subgroup check with cofactor mul"),
                         || f().map(|g| g.borrow().into_affine().mul_by_cofactor_inv().into()),
                         mode,
                     )?;
@@ -544,7 +554,7 @@ BitIteratorBE::without_leading_zeros(cofactor.as_slice()),
                     )
                 } else {
                     let ge = Self::new_variable_omit_prime_order_check(
-                        cs.ns("Witness without subgroup check with `r` check"),
+                        r1cs_core::ns!(cs, "Witness without subgroup check with `r` check"),
                         || {
                             f().map(|g| {
                                 let g = g.into_affine();
@@ -605,6 +615,7 @@ P: SWModelParameters,
     F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bits_le(
         &self,
     ) -> Result<Vec<Boolean<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -616,6 +627,7 @@ bits.push(g.infinity);
         Ok(bits)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bits_le(
         &self,
     ) -> Result<Vec<Boolean<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -634,6 +646,7 @@ P: SWModelParameters,
     F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(
         &self,
     ) -> Result<Vec<UInt8<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -646,6 +659,7 @@ bytes.extend_from_slice(&inf_bytes);
         Ok(bytes)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(
         &self,
     ) -> Result<Vec<UInt8<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -683,18 +697,16 @@ let a_affine = a.into_affine();
     let b_affine = b.into_affine();
 
     println!("Allocating things");
-    let ns = cs.ns("allocating variables");
-    println!("{:?}", cs.current_namespace());
-    let mut gadget_a = GG::new_witness(cs.ns("a"), || Ok(a))?;
-    let gadget_b = GG::new_witness(cs.ns("b"), || Ok(b))?;
-    println!("{:?}", cs.current_namespace());
-    ns.leave_namespace();
+    let ns = r1cs_core::ns!(cs, "allocating variables");
+    let mut gadget_a = GG::new_witness(cs.clone(), || Ok(a))?;
+    let gadget_b = GG::new_witness(cs.clone(), || Ok(b))?;
+    drop(ns);
     println!("Done Allocating things");
     assert_eq!(gadget_a.value()?.into_affine().x, a_affine.x);
     assert_eq!(gadget_a.value()?.into_affine().y, a_affine.y);
     assert_eq!(gadget_b.value()?.into_affine().x, b_affine.x);
     assert_eq!(gadget_b.value()?.into_affine().y, b_affine.y);
-    assert_eq!(cs.which_is_unsatisfied(), None);
+    assert_eq!(cs.which_is_unsatisfied().unwrap(), None);
 
     println!("Checking addition");
     // Check addition
@@ -729,7 +741,8 @@ let native_result = aa.into_affine().mul(scalar);
     let native_result = native_result.into_affine();
 
     let scalar: Vec<bool> = BitIteratorLE::new(scalar.into_repr()).collect();
-    let input: Vec<Boolean<_>> = Vec::new_witness(cs.ns("bits"), || Ok(scalar)).unwrap();
+    let input: Vec<Boolean<_>> =
+        Vec::new_witness(r1cs_core::ns!(cs, "bits"), || Ok(scalar)).unwrap();
     let result = gadget_a.scalar_mul_le(input.iter())?;
     let result_val = result.value()?.into_affine();
     assert_eq!(

@@ -66,6 +66,7 @@ _params: PhantomData,
             }
         }
 
+        #[tracing::instrument(target = "r1cs")]
         pub fn from_edwards_to_coords(
             p: &TEAffine<P>,
         ) -> Result<(P::BaseField, P::BaseField), SynthesisError> {
@@ -83,20 +84,22 @@
             Ok((montgomery_point.x, montgomery_point.y))
         }
 
+        #[tracing::instrument(target = "r1cs")]
         pub fn new_witness_from_edwards(
             cs: ConstraintSystemRef<<P::BaseField as Field>::BasePrimeField>,
             p: &TEAffine<P>,
         ) -> Result<Self, SynthesisError> {
             let montgomery_coords = Self::from_edwards_to_coords(p)?;
-            let u = F::new_witness(cs.ns("u"), || Ok(montgomery_coords.0))?;
-            let v = F::new_witness(cs.ns("v"), || Ok(montgomery_coords.1))?;
+            let u = F::new_witness(r1cs_core::ns!(cs, "u"), || Ok(montgomery_coords.0))?;
+            let v = F::new_witness(r1cs_core::ns!(cs, "v"), || Ok(montgomery_coords.1))?;
             Ok(Self::new(u, v))
         }
 
+        #[tracing::instrument(target = "r1cs")]
         pub fn into_edwards(&self) -> Result<AffineVar<P, F>, SynthesisError> {
             let cs = self.cs().unwrap_or(ConstraintSystemRef::None);
             // Compute u = x / y
-            let u = F::new_witness(cs.ns("u"), || {
+            let u = F::new_witness(r1cs_core::ns!(cs, "u"), || {
                 let y_inv = self
                     .y
                     .value()?
@@ -107,7 +110,7 @@ })?;
 
             u.mul_equals(&self.y, &self.x)?;
 
-            let v = F::new_witness(cs.ns("v"), || {
+            let v = F::new_witness(r1cs_core::ns!(cs, "v"), || {
                 let mut t0 = self.x.value()?;
                 let mut t1 = t0;
                 t0 -= &P::BaseField::one();
@@ -131,6 +134,8 @@ F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
         for<'b> &'b F: FieldOpsBounds<'b, P::BaseField, F>,
     {
         type Output = MontgomeryAffineVar<P, F>;
+
+        #[tracing::instrument(target = "r1cs")]
         fn add(self, other: &'a Self) -> Self::Output {
             let cs = [&self, other].cs();
             let mode = if cs.is_none() || matches!(cs, Some(ConstraintSystemRef::None)) {
@@ -144,7 +149,7 @@ let coeff_b = P::MontgomeryModelParameters::COEFF_B;
             let coeff_a = P::MontgomeryModelParameters::COEFF_A;
 
             let lambda = F::new_variable(
-                cs.ns("lambda"),
+                r1cs_core::ns!(cs, "lambda"),
                 || {
                     let n = other.y.value()? - &self.y.value()?;
                     let d = other.x.value()? - &self.x.value()?;
@@ -159,7 +164,7 @@ lambda_d.mul_equals(&lambda, &lambda_n).unwrap();
 
             // Compute x'' = B*lambda^2 - A - x - x'
             let xprime = F::new_variable(
-                cs.ns("xprime"),
+                r1cs_core::ns!(cs, "xprime"),
                 || {
                     Ok(lambda.value()?.square() * &coeff_b
                         - &coeff_a
@@ -176,7 +181,7 @@ let lambda_b = &lambda * coeff_b;
             lambda_b.mul_equals(&lambda, &xprime_lc).unwrap();
 
             let yprime = F::new_variable(
-                cs.ns("yprime"),
+                r1cs_core::ns!(cs, "yprime"),
                 || {
                     Ok(-(self.y.value()?
                         + &(lambda.value()? * &(xprime.value()? - &self.x.value()?))))
@@ -224,6 +229,7 @@
     /// Allocates a new variable without performing an on-curve check, which is
     /// useful if the variable is known to be on the curve (eg., if the point
     /// is a constant or is a public input).
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     pub fn new_variable_omit_on_curve_check<T: Into<TEAffine<P>>>(
         cs: impl Into<Namespace<<P::BaseField as Field>::BasePrimeField>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -243,8 +249,8 @@ Err(SynthesisError::AssignmentMissing),
             ),
         };
 
-        let x = F::new_variable(cs.ns("x"), || x, mode)?;
-        let y = F::new_variable(cs.ns("y"), || y, mode)?;
+        let x = F::new_variable(r1cs_core::ns!(cs, "x"), || x, mode)?;
+        let y = F::new_variable(r1cs_core::ns!(cs, "y"), || y, mode)?;
 
         Ok(Self::new(x, y))
     }
@@ -294,6 +300,7 @@ fn is_zero(&self) -> Result<Boolean<<P::BaseField as Field>::BasePrimeField>, SynthesisError> {
         self.x.is_zero()?.and(&self.x.is_one()?)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable_omit_prime_order_check(
         cs: impl Into<Namespace<<P::BaseField as Field>::BasePrimeField>>,
         f: impl FnOnce() -> Result<TEProjective<P>, SynthesisError>,
@@ -325,6 +332,7 @@ /// Enforce that `self` is in the prime-order subgroup.
     ///
     /// Does so by multiplying by the prime order, and checking that the result
     /// is unchanged.
+    #[tracing::instrument(target = "r1cs")]
     fn enforce_prime_order(&self) -> Result<(), SynthesisError> {
         let r_minus_1 = (-P::ScalarField::one()).into_repr();
 
@@ -341,6 +349,7 @@ Ok(())
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn double_in_place(&mut self) -> Result<(), SynthesisError> {
         if let Some(cs) = self.cs() {
             let a = P::COEFF_A;
@@ -353,7 +362,7 @@
             let a_x2 = &x2 * a;
 
             // Compute x3 = (2xy) / (ax^2 + y^2)
-            let x3 = F::new_witness(cs.ns("x3"), || {
+            let x3 = F::new_witness(r1cs_core::ns!(cs, "x3"), || {
                 let t0 = xy.value()?.double();
                 let t1 = a * &x2.value()? + &y2.value()?;
                 Ok(t0 * &t1.inverse().ok_or(SynthesisError::DivisionByZero)?)
@@ -365,7 +374,7 @@ x3.mul_equals(&a_x2_plus_y2, &two_xy)?;
 
             // Compute y3 = (y^2 - ax^2) / (2 - ax^2 - y^2)
             let two = P::BaseField::one().double();
-            let y3 = F::new_witness(cs.ns("y3"), || {
+            let y3 = F::new_witness(r1cs_core::ns!(cs, "y3"), || {
                 let a_x2 = a * &x2.value()?;
                 let t0 = y2.value()? - &a_x2;
                 let t1 = two - &a_x2 - &y2.value()?;
@@ -384,10 +393,12 @@ }
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn negate(&self) -> Result<Self, SynthesisError> {
         Ok(Self::new(self.x.negate()?, self.y.clone()))
     }
 
+    #[tracing::instrument(target = "r1cs", skip(scalar_bits_with_base_powers))]
     fn precomputed_base_scalar_mul_le<'a, I, B>(
         &mut self,
         scalar_bits_with_base_powers: I,
@@ -430,6 +441,7 @@
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs", skip(bases, scalars))]
     fn precomputed_base_3_bit_signed_digit_scalar_mul<'a, I, J, B>(
         bases: &[B],
         scalars: &[J],
@@ -519,6 +531,7 @@ TableConstant = P::BaseField,
         >,
     for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<Point: Borrow<TEProjective<P>>>(
         cs: impl Into<Namespace<<P::BaseField as Field>::BasePrimeField>>,
         f: impl FnOnce() -> Result<Point, SynthesisError>,
@@ -559,7 +572,7 @@ // equals the identity.
 
                 let (mut ge, iter) = if cofactor_weight < modulus_minus_1_weight {
                     let ge = Self::new_variable_omit_prime_order_check(
-                        cs.ns("Witness without subgroup check with cofactor mul"),
+                        r1cs_core::ns!(cs, "Witness without subgroup check with cofactor mul"),
                         || f().map(|g| g.borrow().into_affine().mul_by_cofactor_inv().into()),
                         mode,
                     )?;
@@ -569,7 +582,7 @@ BitIteratorBE::without_leading_zeros(cofactor.as_slice()),
                     )
                 } else {
                     let ge = Self::new_variable_omit_prime_order_check(
-                        cs.ns("Witness without subgroup check with `r` check"),
+                        r1cs_core::ns!(cs, "Witness without subgroup check with `r` check"),
                         || {
                             f().map(|g| {
                                 let g = g.into_affine();
@@ -623,6 +636,7 @@ TableConstant = P::BaseField,
         >,
     for<'a> &'a F: FieldOpsBounds<'a, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs", skip(cs, f))]
     fn new_variable<Point: Borrow<TEAffine<P>>>(
         cs: impl Into<Namespace<<P::BaseField as Field>::BasePrimeField>>,
         f: impl FnOnce() -> Result<Point, SynthesisError>,
@@ -671,7 +685,7 @@ // Compute C = d*v0*v1
             let v2 = &v0 * &v1 * d;
 
             // Compute x3 = (v0 + v1) / (1 + v2)
-            let x3 = F::new_witness(cs.ns("x3"), || {
+            let x3 = F::new_witness(r1cs_core::ns!(cs, "x3"), || {
                 let t0 = v0.value()? + &v1.value()?;
                 let t1 = P::BaseField::one() + &v2.value()?;
                 Ok(t0 * &t1.inverse().ok_or(SynthesisError::DivisionByZero)?)
@@ -682,7 +696,7 @@ let v0_plus_v1 = &v0 + &v1;
             x3.mul_equals(&v2_plus_one, &v0_plus_v1).unwrap();
 
             // Compute y3 = (U + a * v0 - v1) / (1 - v2)
-            let y3 = F::new_witness(cs.ns("y3"), || {
+            let y3 = F::new_witness(r1cs_core::ns!(cs, "y3"), || {
                 let t0 = u.value()? + &(a * &v0.value()?) - &v1.value()?;
                 let t1 = P::BaseField::one() - &v2.value()?;
                 Ok(t0 * &t1.inverse().ok_or(SynthesisError::DivisionByZero)?)
@@ -761,6 +775,7 @@ F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'b> &'b F: FieldOpsBounds<'b, P::BaseField, F>,
 {
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditionally_select(
         cond: &Boolean<<P::BaseField as Field>::BasePrimeField>,
         true_value: &Self,
@@ -779,6 +794,7 @@ P: TEModelParameters,
     F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'b> &'b F: FieldOpsBounds<'b, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn is_eq(
         &self,
         other: &Self,
@@ -789,6 +805,7 @@ x_equal.and(&y_equal)
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -800,6 +817,7 @@ Ok(())
     }
 
     #[inline]
+    #[tracing::instrument(target = "r1cs")]
     fn conditional_enforce_not_equal(
         &self,
         other: &Self,
@@ -817,6 +835,7 @@ P: TEModelParameters,
     F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'b> &'b F: FieldOpsBounds<'b, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bits_le(
         &self,
     ) -> Result<Vec<Boolean<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -826,6 +845,7 @@ x_bits.extend_from_slice(&y_bits);
         Ok(x_bits)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bits_le(
         &self,
     ) -> Result<Vec<Boolean<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -843,6 +863,7 @@ P: TEModelParameters,
     F: FieldVar<P::BaseField, <P::BaseField as Field>::BasePrimeField>,
     for<'b> &'b F: FieldOpsBounds<'b, P::BaseField, F>,
 {
+    #[tracing::instrument(target = "r1cs")]
     fn to_bytes(
         &self,
     ) -> Result<Vec<UInt8<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -852,6 +873,7 @@ x_bytes.extend_from_slice(&y_bytes);
         Ok(x_bytes)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn to_non_unique_bytes(
         &self,
     ) -> Result<Vec<UInt8<<P::BaseField as Field>::BasePrimeField>>, SynthesisError> {
@@ -887,18 +909,16 @@ let a_affine = a.into_affine();
     let b_affine = b.into_affine();
 
     println!("Allocating things");
-    let ns = cs.ns("allocating variables");
-    println!("{:?}", cs.current_namespace());
-    let mut gadget_a = GG::new_witness(cs.ns("a"), || Ok(a))?;
-    let gadget_b = GG::new_witness(cs.ns("b"), || Ok(b))?;
-    println!("{:?}", cs.current_namespace());
-    ns.leave_namespace();
+    let ns = r1cs_core::ns!(cs, "allocating variables");
+    let mut gadget_a = GG::new_witness(cs.clone(), || Ok(a))?;
+    let gadget_b = GG::new_witness(cs.clone(), || Ok(b))?;
+    drop(ns);
     println!("Done Allocating things");
     assert_eq!(gadget_a.value()?.into_affine().x, a_affine.x);
     assert_eq!(gadget_a.value()?.into_affine().y, a_affine.y);
     assert_eq!(gadget_b.value()?.into_affine().x, b_affine.x);
     assert_eq!(gadget_b.value()?.into_affine().y, b_affine.y);
-    assert_eq!(cs.which_is_unsatisfied(), None);
+    assert_eq!(cs.which_is_unsatisfied()?, None);
 
     println!("Checking addition");
     // Check addition
@@ -933,7 +953,8 @@ let native_result = AffineCurve::mul(&aa.into_affine(), scalar);
     let native_result = native_result.into_affine();
 
     let scalar: Vec<bool> = BitIteratorLE::new(scalar.into_repr()).collect();
-    let input: Vec<Boolean<_>> = Vec::new_witness(cs.ns("bits"), || Ok(scalar)).unwrap();
+    let input: Vec<Boolean<_>> =
+        Vec::new_witness(r1cs_core::ns!(cs, "bits"), || Ok(scalar)).unwrap();
     let result = gadget_a.scalar_mul_le(input.iter())?;
     let result_val = result.value()?.into_affine();
     assert_eq!(

@@ -47,6 +47,7 @@ fn constant(other: C) -> Self;
 
     fn zero() -> Self;
 
+    #[tracing::instrument(target = "r1cs")]
     fn is_zero(&self) -> Result<Boolean<ConstraintF>, SynthesisError> {
         self.is_eq(&Self::zero())
     }
@@ -62,6 +63,7 @@
     /// Enforce that `self` is in the prime-order subgroup.
     fn enforce_prime_order(&self) -> Result<(), SynthesisError>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn double(&self) -> Result<Self, SynthesisError> {
         let mut result = self.clone();
         result.double_in_place()?;
@@ -74,6 +76,7 @@ fn negate(&self) -> Result<Self, SynthesisError>;
 
     /// Computes `bits * self`, where `bits` is a little-endian
     /// `Boolean` representation of a scalar.
+    #[tracing::instrument(target = "r1cs", skip(bits))]
     fn scalar_mul_le<'a>(
         &self,
         bits: impl Iterator<Item = &'a Boolean<ConstraintF>>,
@@ -93,6 +96,7 @@ /// representation of the scalar.
     ///
     /// The base powers are precomputed power-of-two multiples of a single
     /// base.
+    #[tracing::instrument(target = "r1cs", skip(scalar_bits_with_base_powers))]
     fn precomputed_base_scalar_mul_le<'a, I, B>(
         &mut self,
         scalar_bits_with_base_powers: I,
@@ -109,6 +113,7 @@ }
         Ok(())
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn precomputed_base_3_bit_signed_digit_scalar_mul<'a, I, J, B>(
         _: &[B],
         _: &[J],
@@ -123,6 +128,7 @@ }
 
     /// Computes a `\sum I_j * B_j`, where `I_j` is a `Boolean`
     /// representation of the j-th scalar.
+    #[tracing::instrument(target = "r1cs", skip(bases, scalars))]
     fn precomputed_base_multiscalar_mul_le<'a, T, I, B>(
         bases: &[B],
         scalars: I,
@@ -160,8 +166,8 @@
         let mut rng = test_rng();
         let a_native = C::rand(&mut rng);
         let b_native = C::rand(&mut rng);
-        let a = GG::new_witness(cs.ns("generate_a"), || Ok(a_native)).unwrap();
-        let b = GG::new_witness(cs.ns("generate_b"), || Ok(b_native)).unwrap();
+        let a = GG::new_witness(r1cs_core::ns!(cs, "generate_a"), || Ok(a_native)).unwrap();
+        let b = GG::new_witness(r1cs_core::ns!(cs, "generate_b"), || Ok(b_native)).unwrap();
 
         let zero = GG::zero();
         assert_eq!(zero.value()?, zero.value()?);

@@ -1,4 +1,5 @@
-// Implements AddAssign on Self by deferring to an implementation on &Self
+#[allow(unused_braces)]
+// Implements arithmetic operations with generic bounds.
 #[macro_export]
 macro_rules! impl_ops {
     (
@@ -36,6 +37,8 @@ $($bounds)*
         {
             type Output = $type;
 
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $fn(self, other: Self) -> Self::Output {
                 $impl(self, other)
             }
@@ -47,6 +50,8 @@ $($bounds)*
         {
             type Output = $type;
 
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $fn(self, other: $type) -> Self::Output {
                 core::ops::$trait::$fn(self, &other)
             }
@@ -58,6 +63,8 @@ $($bounds)*
         {
             type Output = $type;
 
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $fn(self, other: &'a $type) -> Self::Output {
                 core::ops::$trait::$fn(&self, other)
             }
@@ -70,6 +77,8 @@ $($bounds)*
         {
             type Output = $type;
 
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $fn(self, other: $type) -> Self::Output {
                 core::ops::$trait::$fn(&self, &other)
             }
@@ -80,6 +89,8 @@ where
 
             $($bounds)*
         {
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $assign_fn(&mut self, other: $type) {
                 let result = core::ops::$trait::$fn(&*self, &other);
                 *self = result
@@ -91,6 +102,8 @@ where
 
             $($bounds)*
         {
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $assign_fn(&mut self, other: &'a $type) {
                 let result = core::ops::$trait::$fn(&*self, other);
                 *self = result
@@ -104,6 +117,8 @@ $($bounds)*
         {
             type Output = $type;
 
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $fn(self, other: $native) -> Self::Output {
                 $constant_impl(self, other)
             }
@@ -116,6 +131,8 @@ $($bounds)*
         {
             type Output = $type;
 
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $fn(self, other: $native) -> Self::Output {
                 core::ops::$trait::$fn(&self, other)
             }
@@ -127,6 +144,8 @@
             $($bounds)*
         {
 
+            #[tracing::instrument(target = "r1cs", skip(self))]
+            #[allow(unused_braces)]
             fn $assign_fn(&mut self, other: $native) {
                 let result = core::ops::$trait::$fn(&*self, other);
                 *self = result

@@ -18,6 +18,7 @@ type Fp2V<P> = Fp2Var<<P as Bls12Parameters>::Fp2Params>;
 
 impl<P: Bls12Parameters> PairingVar<P> {
     // Evaluate the line function at point p.
+    #[tracing::instrument(target = "r1cs")]
     fn ell(
         f: &mut Fp12Var<P::Fp12Params>,
         coeffs: &(Fp2V<P>, Fp2V<P>),
@@ -49,6 +50,7 @@ }
         }
     }
 
+    #[tracing::instrument(target = "r1cs")]
     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 {
@@ -65,6 +67,7 @@ type G1PreparedVar = G1PreparedVar<P>;
     type G2PreparedVar = G2PreparedVar<P>;
     type GTVar = Fp12Var<P::Fp12Params>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn miller_loop(
         ps: &[Self::G1PreparedVar],
         qs: &[Self::G2PreparedVar],
@@ -96,6 +99,7 @@
         Ok(f)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn final_exponentiation(f: &Self::GTVar) -> Result<Self::GTVar, SynthesisError> {
         // Computing the final exponentation following
         // https://eprint.iacr.org/2016/130.pdf.
@@ -152,10 +156,12 @@ Ok(y5)
         })
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn prepare_g1(p: &Self::G1Var) -> Result<Self::G1PreparedVar, SynthesisError> {
         Self::G1PreparedVar::from_group_var(p)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn prepare_g2(q: &Self::G2Var) -> Result<Self::G2PreparedVar, SynthesisError> {
         Self::G2PreparedVar::from_group_var(q)
     }

@@ -22,6 +22,7 @@ type Fp4G<P> = Fp4Var<<P as MNT4Parameters>::Fp4Params>;
 pub type GTVar<P> = Fp4G<P>;
 
 impl<P: MNT4Parameters> PairingVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(r))]
     pub(crate) fn doubling_step_for_flipped_miller_loop(
         r: &G2ProjectiveExtendedVar<P>,
     ) -> Result<(G2ProjectiveExtendedVar<P>, AteDoubleCoefficientsVar<P>), SynthesisError> {
@@ -57,6 +58,7 @@
         Ok((r2, coeff))
     }
 
+    #[tracing::instrument(target = "r1cs", skip(r))]
     pub(crate) fn mixed_addition_step_for_flipped_miller_loop(
         x: &Fp2G<P>,
         y: &Fp2G<P>,
@@ -89,6 +91,7 @@
         Ok((r2, coeff))
     }
 
+    #[tracing::instrument(target = "r1cs", skip(p, q))]
     pub fn ate_miller_loop(
         p: &G1PreparedVar<P>,
         q: &G2PreparedVar<P>,
@@ -138,6 +141,7 @@
         Ok(f)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(value))]
     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)?;
@@ -145,6 +149,7 @@ 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)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(elt, elt_inv))]
     fn final_exponentiation_first_chunk(
         elt: &Fp4G<P>,
         elt_inv: &Fp4G<P>,
@@ -157,6 +162,7 @@ // elt_q2_over_elt = elt^(q^2-1)
         Ok(elt_q2 * elt_inv)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(elt, elt_inv))]
     fn final_exponentiation_last_chunk(
         elt: &Fp4G<P>,
         elt_inv: &Fp4G<P>,
@@ -185,6 +191,7 @@ type G1PreparedVar = G1PreparedVar<P>;
     type G2PreparedVar = G2PreparedVar<P>;
     type GTVar = GTVar<P>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn miller_loop(
         ps: &[Self::G1PreparedVar],
         qs: &[Self::G2PreparedVar],
@@ -197,14 +204,17 @@
         Ok(result)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn final_exponentiation(r: &Self::GTVar) -> Result<Self::GTVar, SynthesisError> {
         Self::final_exponentiation(r)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn prepare_g1(p: &Self::G1Var) -> Result<Self::G1PreparedVar, SynthesisError> {
         Self::G1PreparedVar::from_group_var(p)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn prepare_g2(q: &Self::G2Var) -> Result<Self::G2PreparedVar, SynthesisError> {
         Self::G2PreparedVar::from_group_var(q)
     }

@@ -22,6 +22,7 @@ type Fp6G<P> = Fp6Var<<P as MNT6Parameters>::Fp6Params>;
 pub type GTVar<P> = Fp6G<P>;
 
 impl<P: MNT6Parameters> PairingVar<P> {
+    #[tracing::instrument(target = "r1cs", skip(r))]
     pub(crate) fn doubling_step_for_flipped_miller_loop(
         r: &G2ProjectiveExtendedVar<P>,
     ) -> Result<(G2ProjectiveExtendedVar<P>, AteDoubleCoefficientsVar<P>), SynthesisError> {
@@ -52,6 +53,7 @@
         Ok((r2, coeff))
     }
 
+    #[tracing::instrument(target = "r1cs", skip(r))]
     pub(crate) fn mixed_addition_step_for_flipped_miller_loop(
         x: &Fp3G<P>,
         y: &Fp3G<P>,
@@ -84,6 +86,7 @@
         Ok((r2, coeff))
     }
 
+    #[tracing::instrument(target = "r1cs", skip(p, q))]
     pub fn ate_miller_loop(
         p: &G1PreparedVar<P>,
         q: &G2PreparedVar<P>,
@@ -134,6 +137,7 @@
         Ok(f)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     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)?;
@@ -141,6 +145,7 @@ 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)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(elt, elt_inv))]
     fn final_exponentiation_first_chunk(
         elt: &Fp6G<P>,
         elt_inv: &Fp6G<P>,
@@ -157,6 +162,7 @@ // beta = elt^((q^3-1)*(q+1)
         Ok(alpha * &elt_q3_over_elt)
     }
 
+    #[tracing::instrument(target = "r1cs", skip(elt, elt_inv))]
     fn final_exponentiation_last_chunk(
         elt: &Fp6G<P>,
         elt_inv: &Fp6G<P>,
@@ -181,6 +187,7 @@ type G1PreparedVar = G1PreparedVar<P>;
     type G2PreparedVar = G2PreparedVar<P>;
     type GTVar = GTVar<P>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn miller_loop(
         ps: &[Self::G1PreparedVar],
         qs: &[Self::G2PreparedVar],
@@ -193,14 +200,17 @@
         Ok(result)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn final_exponentiation(r: &Self::GTVar) -> Result<Self::GTVar, SynthesisError> {
         Self::final_exponentiation(r)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn prepare_g1(p: &Self::G1Var) -> Result<Self::G1PreparedVar, SynthesisError> {
         Self::G1PreparedVar::from_group_var(p)
     }
 
+    #[tracing::instrument(target = "r1cs")]
     fn prepare_g2(q: &Self::G2Var) -> Result<Self::G2PreparedVar, SynthesisError> {
         Self::G2PreparedVar::from_group_var(q)
     }

@@ -33,6 +33,7 @@ ) -> Result<Self::GTVar, SynthesisError>;
 
     fn final_exponentiation(p: &Self::GTVar) -> Result<Self::GTVar, SynthesisError>;
 
+    #[tracing::instrument(target = "r1cs")]
     fn pairing(
         p: Self::G1PreparedVar,
         q: Self::G2PreparedVar,
@@ -43,6 +44,7 @@ }
 
     /// Computes a product of pairings.
     #[must_use]
+    #[tracing::instrument(target = "r1cs")]
     fn product_of_pairings(
         p: &[Self::G1PreparedVar],
         q: &[Self::G2PreparedVar],
@@ -84,10 +86,10 @@ sa *= s;
         let mut sb = b;
         sb *= s;
 
-        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 a_g = P::G1Var::new_witness(cs.clone(), || Ok(a.into_affine()))?;
+        let b_g = P::G2Var::new_witness(cs.clone(), || Ok(b.into_affine()))?;
+        let sa_g = P::G1Var::new_witness(cs.clone(), || Ok(sa.into_affine()))?;
+        let sb_g = P::G2Var::new_witness(cs.clone(), || Ok(sb.into_affine()))?;
 
         let mut preparation_num_constraints = cs.num_constraints();
         let a_prep_g = P::prepare_g1(&a_g)?;