fix: variable modulus subtraction padding (#1200)

* fix: correctly compute overflow

* fix: ensure padding value to be big

* fix: panic when next overflow would overflow the native

* fix: use big.Int not to overflow uint64

* perf: address comment that can merge two range checks

std/math/emulated/custommod.go

@@ -48,6 +48,13 @@ func (f *Field[T]) modSub(a, b *Element[T], modulus *Element[T]) *Element[T] {
 	// instead of assuming T as a constant. And when doing as a hint, then need
 	// to assert that the padding is a multiple of the modulus (done inside callSubPaddingHint)
 	nextOverflow := max(b.overflow+1, a.overflow) + 1
+	if nextOverflow > f.maxOverflow() {
+		// TODO: in general we should handle it more gracefully, but this method
+		// is only used in ModAssertIsEqual which in turn is only used in tests,
+		// then for now we avoid automatic overflow handling (like we have for fixed modulus case).
+		// We only panic here so that the user would know to manually handle the overflow.
+		panic("next overflow would overflow the native field")
+	}
 	nbLimbs := max(len(a.Limbs), len(b.Limbs))
 	limbs := make([]frontend.Variable, nbLimbs)
 	padding := f.computeSubPaddingHint(b.overflow, uint(nbLimbs), modulus)

std/math/emulated/hints.go

@@ -188,17 +188,32 @@ func subPaddingHint(mod *big.Int, inputs, outputs []*big.Int) error {
 }
 
 func (f *Field[T]) computeSubPaddingHint(overflow uint, nbLimbs uint, modulus *Element[T]) *Element[T] {
+	// we compute the subtraction padding hint in-circuit. The padding has satisfy:
+	// 1. padding % modulus = 0
+	// 2. padding[i] >= (1 << (bits+overflow))
+	// 3. padding[i] + a[i] < native_field for all valid a[i] (defined by overflow)
 	var fp T
 	inputs := []frontend.Variable{fp.NbLimbs(), fp.BitsPerLimb(), overflow, nbLimbs}
 	inputs = append(inputs, modulus.Limbs...)
+	// compute the actual padding value
 	res, err := f.api.NewHint(subPaddingHint, int(nbLimbs), inputs...)
 	if err != nil {
 		panic(fmt.Sprintf("sub padding hint: %v", err))
 	}
+	maxLimb := new(big.Int).Lsh(big.NewInt(1), fp.BitsPerLimb()+overflow)
+	maxLimb.Sub(maxLimb, big.NewInt(1))
 	for i := range res {
-		f.checker.Check(res[i], int(fp.BitsPerLimb()+overflow+1))
+		// we can check conditions 2 and 3 together by subtracting the maximum
+		// value which can be subtracted from the padding. The result should not
+		// underflow (in which case the width of the subtraction result could be
+		// at least native_width-overflow) and should be nbBits+overflow+1 bits
+		// wide (as expected padding is one bit wider than the maximum allowed
+		// subtraction limb).
+		f.checker.Check(f.api.Sub(res[i], maxLimb), int(fp.BitsPerLimb()+overflow+1))
 	}
-	padding := f.newInternalElement(res, fp.BitsPerLimb()+overflow+1)
+
+	// ensure that condition 1 holds
+	padding := f.newInternalElement(res, overflow+1)
 	f.checkZero(padding, modulus)
 	return padding
 }