fix: incorrect calc of surfeit related value in EmulatedFpVar (#157)

yuxqiu · weikengchen · Pratyush · web-flow · commit 338ab1269771 · 2025-09-12T20:13:58.000Z
* fix: incorrect calc of surfeit related value

* test: add a test

* fix: a typo

---------

Co-authored-by: Weikeng Chen &lt;w.k@berkeley.edu&gt;
Co-authored-by: Pratyush Mishra &lt;pratyush795@gmail.com&gt;
diff --git a/src/fields/emulated_fp/allocated_field_var.rs b/src/fields/emulated_fp/allocated_field_var.rs
@@ -238,12 +238,17 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
             }
         }
 
+        let padding_bit_len = {
+            let mut one = BaseF::ONE.into_bigint();
+            one <<= surfeit as u32;
+            BaseF::from(one)
+        };
         let result = AllocatedEmulatedFpVar::<TargetF, BaseF> {
             cs: self.cs(),
             limbs,
-            num_of_additions_over_normal_form: self.num_of_additions_over_normal_form
-                + (other.num_of_additions_over_normal_form + BaseF::one())
-                + (other.num_of_additions_over_normal_form + BaseF::one()),
+            num_of_additions_over_normal_form: self.num_of_additions_over_normal_form // this_limb
+                + padding_bit_len // pad_non_top_limb / pad_top_limb
+                + BaseF::one(), // pad_to_kp_limb
             is_in_the_normal_form: false,
             target_phantom: PhantomData,
         };
@@ -424,9 +429,19 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
         Ok(AllocatedMulResultVar {
             cs: self.cs(),
             limbs: prod_limbs,
+            // New number is upper bounded by:
+            //
+            // (a+1)2^{bits_per_limb} * (b+1)2^{bits_per_limb} * m = (ab+a+b+1)*m*2^{2*bits_per_limb}
+            //
+            // where `a = self_reduced.num_of_additions_over_normal_form` and
+            //       `b = other_reduced.num_of_additions_over_normal_form`
+            // - why m pair: at cell m, there are m possible pairs (one limb from each var) that can add to cell m
+            //
+            // In theory, we can let `prod_of_num_of_additions = (m(ab+a+b+1)-1)`. But below, we use an overestimation.
             prod_of_num_of_additions: (self_reduced.num_of_additions_over_normal_form
                 + BaseF::one())
-                * (other_reduced.num_of_additions_over_normal_form + BaseF::one()),
+                * (other_reduced.num_of_additions_over_normal_form + BaseF::one())
+                * BaseF::from((params.num_limbs) as u32),
             target_phantom: PhantomData,
         })
     }
@@ -459,13 +474,6 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
         for limb in p_representations.iter() {
             p_gadget_limbs.push(FpVar::<BaseF>::Constant(*limb));
         }
-        let p_gadget = Self {
-            cs: self.cs(),
-            limbs: p_gadget_limbs,
-            num_of_additions_over_normal_form: BaseF::one(),
-            is_in_the_normal_form: false,
-            target_phantom: PhantomData,
-        };
 
         // Get delta = self - other
         let cs = self.cs().or(other.cs()).or(should_enforce.cs());
@@ -489,7 +497,7 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
 
         // Compute k * p
         let mut kp_gadget_limbs = Vec::new();
-        for limb in p_gadget.limbs.iter() {
+        for limb in p_gadget_limbs.iter() {
             kp_gadget_limbs.push(limb * &k_gadget);
         }
 
@@ -911,3 +919,108 @@ impl<TargetF: PrimeField, BaseF: PrimeField> Clone for AllocatedEmulatedFpVar<Ta
         }
     }
 }
+
+#[cfg(test)]
+mod test {
+    use ark_ec::{bls12::Bls12Config, pairing::Pairing};
+    use ark_ff::PrimeField;
+    use ark_relations::gr1cs::ConstraintSystem;
+
+    use crate::{
+        alloc::AllocVar,
+        fields::{
+            emulated_fp::{test::check_constraint, AllocatedEmulatedFpVar},
+            fp::FpVar,
+        },
+    };
+
+    #[test]
+    fn pr_157() {
+        type TargetF = <ark_bls12_381::Config as Bls12Config>::Fp;
+        type BaseF = <ark_bls12_377::Bls12_377 as Pairing>::ScalarField;
+
+        let cs = ConstraintSystem::new_ref();
+
+        let l0: AllocatedEmulatedFpVar<TargetF, BaseF> =
+            AllocatedEmulatedFpVar::new_input(cs.clone(), || {
+                Ok(TargetF::from(
+                    TargetF::from(1).into_bigint()
+                        << (<TargetF as PrimeField>::MODULUS_BIT_SIZE - 1),
+                ) + TargetF::from(-1))
+            })
+            .unwrap();
+
+        // Accumulate errors
+        let l1 = l0.sub(&l0).unwrap();
+        let l1 = l1.sub(&l1).unwrap();
+        let l1 = l1.sub(&l1).unwrap();
+        let l1 = l1.sub(&l1).unwrap();
+        let l1 = l1.sub(&l1).unwrap();
+
+        let l2 = l1.add(&l1).unwrap();
+
+        // Increase l1's surfeit
+        // - The goal is to ensure that the number of limbs, as grouped by `group_and_check_equality`,
+        //   falls near the threshold between 17 and 18 limbs.
+        // - This increases the chance that accumulated error in `sub` causes an overflow within
+        //   `group_and_check_equality`.
+        let mut l1 = l1;
+        for _ in 0..(293 - 242) {
+            l1 = l1.add(&l0).unwrap();
+        }
+
+        let _ = l1.mul(&l2).unwrap();
+        assert!(cs.is_satisfied().unwrap());
+    }
+
+    #[test]
+    fn pr_157_sub() {
+        type TargetF = <ark_bls12_381::Config as Bls12Config>::Fp;
+        type BaseF = <ark_bls12_377::Bls12_377 as Pairing>::ScalarField;
+
+        let self_limb_values = [
+            100, 2618, 1428, 2152, 2602, 1242, 2823, 511, 1752, 2058, 3599, 1113, 3207, 3601, 2736,
+            435, 1108, 2965, 2685, 1705, 1016, 1343, 1760, 2039, 1355, 1767, 2355, 1945, 3594,
+            4066, 1913, 2646,
+        ];
+        let self_num_of_additions_over_normal_form = 1;
+        let self_is_in_the_normal_form = false;
+        let other_limb_values = [
+            0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
+            0, 0, 4,
+        ];
+        let other_num_of_additions_over_normal_form = 1;
+        let other_is_in_the_normal_form = false;
+
+        let cs = ConstraintSystem::new_ref();
+
+        let left_limb = self_limb_values
+            .iter()
+            .map(|v| FpVar::new_input(cs.clone(), || Ok(BaseF::from(*v))).unwrap())
+            .collect();
+        let left: AllocatedEmulatedFpVar<TargetF, BaseF> = AllocatedEmulatedFpVar {
+            cs: cs.clone(),
+            limbs: left_limb,
+            num_of_additions_over_normal_form: BaseF::from(self_num_of_additions_over_normal_form),
+            is_in_the_normal_form: self_is_in_the_normal_form,
+            target_phantom: std::marker::PhantomData,
+        };
+
+        let other_limb = other_limb_values
+            .iter()
+            .map(|v| FpVar::new_input(cs.clone(), || Ok(BaseF::from(*v))).unwrap())
+            .collect();
+        let right: AllocatedEmulatedFpVar<TargetF, BaseF> = AllocatedEmulatedFpVar {
+            cs: cs.clone(),
+            limbs: other_limb,
+            num_of_additions_over_normal_form: BaseF::from(other_num_of_additions_over_normal_form),
+            is_in_the_normal_form: other_is_in_the_normal_form,
+            target_phantom: std::marker::PhantomData,
+        };
+
+        let result = left.sub_without_reduce(&right).unwrap();
+        assert!(check_constraint(&left));
+        assert!(check_constraint(&right));
+        assert!(check_constraint(&result));
+    }
+}
diff --git a/src/fields/emulated_fp/allocated_mul_result.rs b/src/fields/emulated_fp/allocated_mul_result.rs
@@ -113,7 +113,7 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedMulResultVar<TargetF, Base
         };
 
         // Step 2: compute surfeit
-        let surfeit = overhead!(self.prod_of_num_of_additions + BaseF::one()) + 1 + 1;
+        let surfeit = overhead!(self.prod_of_num_of_additions + BaseF::one());
 
         // Step 3: allocate k
         let k_bits = {
@@ -284,3 +284,42 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedMulResultVar<TargetF, Base
         }
     }
 }
+
+#[cfg(test)]
+mod test {
+    use ark_ec::{bls12::Bls12Config, pairing::Pairing};
+    use ark_ff::PrimeField;
+    use ark_relations::gr1cs::ConstraintSystem;
+
+    use crate::{
+        alloc::AllocVar,
+        fields::emulated_fp::{
+            test::{check_constraint, check_mulres_constraint},
+            AllocatedEmulatedFpVar,
+        },
+    };
+
+    #[test]
+    fn pr_157_mul() {
+        type TargetF = <ark_bls12_381::Config as Bls12Config>::Fp;
+        type BaseF = <ark_bls12_377::Bls12_377 as Pairing>::ScalarField;
+
+        let cs = ConstraintSystem::new_ref();
+
+        let left: AllocatedEmulatedFpVar<TargetF, BaseF> =
+            AllocatedEmulatedFpVar::new_input(cs.clone(), || {
+                Ok(TargetF::from(
+                    TargetF::from(1).into_bigint()
+                        << (<TargetF as PrimeField>::MODULUS_BIT_SIZE - 1),
+                ) + TargetF::from(-1))
+            })
+            .unwrap();
+
+        let right: AllocatedEmulatedFpVar<TargetF, BaseF> = left.clone();
+
+        let result = left.mul_without_reduce(&right).unwrap();
+        assert!(check_constraint(&left));
+        assert!(check_constraint(&right));
+        assert!(check_mulres_constraint(&result));
+    }
+}
diff --git a/src/fields/emulated_fp/mod.rs b/src/fields/emulated_fp/mod.rs
@@ -152,6 +152,7 @@ macro_rules! overhead {
         use ark_ff::BigInteger;
         let num = $x;
         let num_bits = num.into_bigint().to_bits_be();
+
         let mut skipped_bits = 0;
         for b in num_bits.iter() {
             if *b == false {
@@ -168,10 +169,13 @@ macro_rules! overhead {
             }
         }
 
-        if is_power_of_2 {
-            num_bits.len() - skipped_bits
+        // let log(0) = 0 in our case
+        if num == BaseF::zero() {
+            0
+        } else if is_power_of_2 {
+            num_bits.len() - skipped_bits - 1
         } else {
-            num_bits.len() - skipped_bits + 1
+            num_bits.len() - skipped_bits
         }
     }};
 }
@@ -200,3 +204,45 @@ pub use field_var::*;
 
 mod mul_result;
 pub use mul_result::*;
+
+#[cfg(test)]
+mod test {
+    use ark_ff::PrimeField;
+
+    use crate::{
+        fields::emulated_fp::{params::get_params, AllocatedEmulatedFpVar},
+        GR1CSVar,
+    };
+
+    use super::AllocatedMulResultVar;
+
+    pub(crate) fn check_constraint<TargetF: PrimeField, BaseF: PrimeField>(
+        emulated_fpvar: &AllocatedEmulatedFpVar<TargetF, BaseF>,
+    ) -> bool {
+        let limb_values = emulated_fpvar.limbs.value().unwrap();
+        let params = get_params(
+            TargetF::MODULUS_BIT_SIZE as usize,
+            BaseF::MODULUS_BIT_SIZE as usize,
+            emulated_fpvar.get_optimization_type(),
+        );
+        let bits_per_limb = params.bits_per_limb;
+        let upper_bound = (emulated_fpvar.num_of_additions_over_normal_form + BaseF::one())
+            * (BaseF::from(BaseF::from(1).into_bigint() << bits_per_limb as u32) + BaseF::from(-1));
+        return !limb_values.iter().any(|value| value > &upper_bound);
+    }
+
+    pub(crate) fn check_mulres_constraint<TargetF: PrimeField, BaseF: PrimeField>(
+        emulated_fpvar: &AllocatedMulResultVar<TargetF, BaseF>,
+    ) -> bool {
+        let limb_values: Vec<_> = emulated_fpvar.limbs.value().unwrap();
+        let params = get_params(
+            TargetF::MODULUS_BIT_SIZE as usize,
+            BaseF::MODULUS_BIT_SIZE as usize,
+            emulated_fpvar.get_optimization_type(),
+        );
+        let bits_per_limb = params.bits_per_limb * 2;
+        let upper_bound = (emulated_fpvar.prod_of_num_of_additions + BaseF::one())
+            * (BaseF::from(BaseF::from(1).into_bigint() << bits_per_limb as u32) + BaseF::from(-1));
+        return !limb_values.iter().any(|value| value > &upper_bound);
+    }
+}
diff --git a/src/fields/emulated_fp/reduce.rs b/src/fields/emulated_fp/reduce.rs
@@ -155,24 +155,34 @@ impl<TargetF: PrimeField, BaseF: PrimeField> Reducer<TargetF, BaseF> {
             elem.get_optimization_type(),
         );
 
-        if 2 * params.bits_per_limb + ark_std::log2(params.num_limbs) as usize
-            > BaseF::MODULUS_BIT_SIZE as usize - 1
+        // `2 * params.bits_per_limb + ark_std::log2(params.num_limbs + 1)` needs to be `<= BaseF::MODULUS_BIT_SIZE as usize - 4`
+        // - see `group_and_check_equality` for more details
+        if 2 * params.bits_per_limb + ark_std::log2(params.num_limbs + 1) as usize
+            >= BaseF::MODULUS_BIT_SIZE as usize - 3
         {
             panic!("The current limb parameters do not support multiplication.");
         }
 
         loop {
+            // this needs to be adjusted if we modify `prod_of_num_of_additions` for `AllocatedMulResultVar`
+            // - see `mul_without_reduce` in `src/fields/emulated_fp/allocated_field_var.rs`
             let prod_of_num_of_additions = (elem.num_of_additions_over_normal_form + BaseF::one())
                 * (elem_other.num_of_additions_over_normal_form + BaseF::one());
-            let overhead_limb = overhead!(prod_of_num_of_additions.mul(
-                &BaseF::from_bigint(<BaseF as PrimeField>::BigInt::from(
-                    (params.num_limbs) as u64
-                ))
-                .unwrap()
-            ));
-            let bits_per_mulresult_limb = 2 * (params.bits_per_limb + 1) + overhead_limb;
+            let overhead_limb = overhead!(
+                BaseF::one()
+                    + prod_of_num_of_additions.mul(
+                        &BaseF::from_bigint(<BaseF as PrimeField>::BigInt::from(
+                            (params.num_limbs) as u64
+                        ))
+                        .unwrap()
+                    )
+            );
 
-            if bits_per_mulresult_limb < BaseF::MODULUS_BIT_SIZE as usize {
+            let bits_per_mulresult_limb = 2 * params.bits_per_limb + overhead_limb;
+
+            // we need `bits_per_mulresult_limb <= MODULUS_BIT_SIZE - 4`
+            // - see `group_and_check_equality` for more details
+            if bits_per_mulresult_limb < (BaseF::MODULUS_BIT_SIZE - 3) as usize {
                 break;
             }
 
@@ -211,6 +221,22 @@ impl<TargetF: PrimeField, BaseF: PrimeField> Reducer<TargetF, BaseF> {
         let zero = FpVar::<BaseF>::zero();
 
         let mut limb_pairs = Vec::<(FpVar<BaseF>, FpVar<BaseF>)>::new();
+
+        // this size is closely related to the grouped limb size, padding size, pre_mul_reduce and post_add_reduce
+        //
+        // it should be carefully chosen so that 1) no overflow/underflow can happen in this function and 2) num_limb_in_a_group
+        // is always >=1.
+        //
+        // 1. for this function
+        // - pad_limb has bit size BaseF::MODULUS_BIT_SIZE - 1
+        // - left/right_total_limb has bit size BaseF::MODULUS_BIT_SIZE - 3
+        // - carry has even smaller size
+        // - so, their sum has bit size <= BaseF::MODULUS_BIT_SIZE - 1
+        //
+        // 2. for pre_mul_reduce
+        // - it enforces `2 * bits_per_limb + surfeit <= BaseF::MODULUS_BIT_SIZE - 4`
+        //   - 2 * bits_per_limb in that function == 2 * (bits_per_limb - shift_per_limb) == shift_per_limb
+        // - so, num_limb_in_a_group is >= 1 for mul
         let num_limb_in_a_group = (BaseF::MODULUS_BIT_SIZE as usize
             - 1
             - surfeit
@@ -240,6 +266,8 @@ impl<TargetF: PrimeField, BaseF: PrimeField> Reducer<TargetF, BaseF> {
         let mut groupped_limb_pairs = Vec::<(FpVar<BaseF>, FpVar<BaseF>, usize)>::new();
 
         for limb_pairs_in_a_group in limb_pairs.chunks(num_limb_in_a_group) {
+            // bit size = num_limb_in_a_group * shift_per_limb + bits_per_limb + true surfeit + 1
+            //     <= BaseF::MODULUS_BIT_SIZE - 3
             let mut left_total_limb = zero.clone();
             let mut right_total_limb = zero.clone();
 
@@ -267,6 +295,9 @@ impl<TargetF: PrimeField, BaseF: PrimeField> Reducer<TargetF, BaseF> {
         {
             let mut pad_limb_repr = BaseF::ONE.into_bigint();
 
+            // use padding to avoid underflow
+            //
+            // bit size = BaseF::MODULUS_BIT_SIZE - 1
             pad_limb_repr <<= (surfeit
                 + (bits_per_limb - shift_per_limb)
                 + shift_per_limb * num_limb_in_this_group
