@@ -242,12 +242,17 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
242242 }
243243 }
244244
245+ let padding_bit_len = {
246+ let mut one = BaseF :: ONE . into_bigint ( ) ;
247+ one <<= surfeit as u32 ;
248+ BaseF :: from ( one)
249+ } ;
245250 let result = AllocatedEmulatedFpVar :: < TargetF , BaseF > {
246251 cs : self . cs ( ) ,
247252 limbs,
248- num_of_additions_over_normal_form : self . num_of_additions_over_normal_form
249- + ( other . num_of_additions_over_normal_form + BaseF :: one ( ) )
250- + ( other . num_of_additions_over_normal_form + BaseF :: one ( ) ) ,
253+ num_of_additions_over_normal_form : self . num_of_additions_over_normal_form // this_limb
254+ + padding_bit_len // pad_non_top_limb / pad_top_limb
255+ + BaseF :: one ( ) , // pad_to_kp_limb
251256 is_in_the_normal_form : false ,
252257 target_phantom : PhantomData ,
253258 } ;
@@ -428,9 +433,19 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
428433 Ok ( AllocatedMulResultVar {
429434 cs : self . cs ( ) ,
430435 limbs : prod_limbs,
436+ // New number is upper bounded by:
437+ //
438+ // (a+1)2^{bits_per_limb} * (b+1)2^{bits_per_limb} * m = (ab+a+b+1)*m*2^{2*bits_per_limb}
439+ //
440+ // where `a = self_reduced.num_of_additions_over_normal_form` and
441+ // `b = other_reduced.num_of_additions_over_normal_form`
442+ // - why m pair: at cell m, there are m possible pairs (one limb from each var) that can add to cell m
443+ //
444+ // In theory, we can let `prod_of_num_of_additions = (m(ab+a+b+1)-1)`. But below, we use an overestimation.
431445 prod_of_num_of_additions : ( self_reduced. num_of_additions_over_normal_form
432446 + BaseF :: one ( ) )
433- * ( other_reduced. num_of_additions_over_normal_form + BaseF :: one ( ) ) ,
447+ * ( other_reduced. num_of_additions_over_normal_form + BaseF :: one ( ) )
448+ * BaseF :: from ( ( params. num_limbs ) as u32 ) ,
434449 target_phantom : PhantomData ,
435450 } )
436451 }
@@ -464,13 +479,6 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
464479 for limb in p_representations. iter ( ) {
465480 p_gadget_limbs. push ( FpVar :: < BaseF > :: Constant ( * limb) ) ;
466481 }
467- let p_gadget = AllocatedEmulatedFpVar :: < TargetF , BaseF > {
468- cs : self . cs ( ) ,
469- limbs : p_gadget_limbs,
470- num_of_additions_over_normal_form : BaseF :: one ( ) ,
471- is_in_the_normal_form : false ,
472- target_phantom : PhantomData ,
473- } ;
474482
475483 // Get delta = self - other
476484 let cs = self . cs ( ) . or ( other. cs ( ) ) . or ( should_enforce. cs ( ) ) ;
@@ -494,7 +502,7 @@ impl<TargetF: PrimeField, BaseF: PrimeField> AllocatedEmulatedFpVar<TargetF, Bas
494502
495503 // Compute k * p
496504 let mut kp_gadget_limbs = Vec :: new ( ) ;
497- for limb in p_gadget . limbs . iter ( ) {
505+ for limb in p_gadget_limbs . iter ( ) {
498506 kp_gadget_limbs. push ( limb * & k_gadget) ;
499507 }
500508
@@ -916,3 +924,68 @@ impl<TargetF: PrimeField, BaseF: PrimeField> Clone for AllocatedEmulatedFpVar<Ta
916924 }
917925 }
918926}
927+
928+ #[ cfg( test) ]
929+ mod test {
930+ use ark_ec:: { bls12:: Bls12Config , pairing:: Pairing } ;
931+ use ark_relations:: r1cs:: ConstraintSystem ;
932+
933+ use crate :: {
934+ alloc:: AllocVar ,
935+ fields:: {
936+ emulated_fp:: { test:: check_constraint, AllocatedEmulatedFpVar } ,
937+ fp:: FpVar ,
938+ } ,
939+ } ;
940+
941+ #[ test]
942+ fn pr_157_sub ( ) {
943+ type TargetF = <ark_bls12_381:: Config as Bls12Config >:: Fp ;
944+ type BaseF = <ark_bls12_377:: Bls12_377 as Pairing >:: ScalarField ;
945+
946+ let self_limb_values = [
947+ 100 , 2618 , 1428 , 2152 , 2602 , 1242 , 2823 , 511 , 1752 , 2058 , 3599 , 1113 , 3207 , 3601 , 2736 ,
948+ 435 , 1108 , 2965 , 2685 , 1705 , 1016 , 1343 , 1760 , 2039 , 1355 , 1767 , 2355 , 1945 , 3594 ,
949+ 4066 , 1913 , 2646 ,
950+ ] ;
951+ let self_num_of_additions_over_normal_form = 1 ;
952+ let self_is_in_the_normal_form = false ;
953+ let other_limb_values = [
954+ 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 ,
955+ 0 , 0 , 4 ,
956+ ] ;
957+ let other_num_of_additions_over_normal_form = 1 ;
958+ let other_is_in_the_normal_form = false ;
959+
960+ let cs = ConstraintSystem :: new_ref ( ) ;
961+
962+ let left_limb = self_limb_values
963+ . iter ( )
964+ . map ( |v| FpVar :: new_input ( cs. clone ( ) , || Ok ( BaseF :: from ( * v) ) ) . unwrap ( ) )
965+ . collect ( ) ;
966+ let left: AllocatedEmulatedFpVar < TargetF , BaseF > = AllocatedEmulatedFpVar {
967+ cs : cs. clone ( ) ,
968+ limbs : left_limb,
969+ num_of_additions_over_normal_form : BaseF :: from ( self_num_of_additions_over_normal_form) ,
970+ is_in_the_normal_form : self_is_in_the_normal_form,
971+ target_phantom : std:: marker:: PhantomData ,
972+ } ;
973+
974+ let other_limb = other_limb_values
975+ . iter ( )
976+ . map ( |v| FpVar :: new_input ( cs. clone ( ) , || Ok ( BaseF :: from ( * v) ) ) . unwrap ( ) )
977+ . collect ( ) ;
978+ let right: AllocatedEmulatedFpVar < TargetF , BaseF > = AllocatedEmulatedFpVar {
979+ cs : cs. clone ( ) ,
980+ limbs : other_limb,
981+ num_of_additions_over_normal_form : BaseF :: from ( other_num_of_additions_over_normal_form) ,
982+ is_in_the_normal_form : other_is_in_the_normal_form,
983+ target_phantom : std:: marker:: PhantomData ,
984+ } ;
985+
986+ let result = left. sub_without_reduce ( & right) . unwrap ( ) ;
987+ assert ! ( check_constraint( & left) ) ;
988+ assert ! ( check_constraint( & right) ) ;
989+ assert ! ( check_constraint( & result) ) ;
990+ }
991+ }
0 commit comments