docs: update package documentation

std/math/emulated/doc.go

@@ -86,52 +86,29 @@ then the overflow value f' for the sum is computed as
 
 The complexity of native limb-wise multiplication is k^2. This translates
 directly to the complexity in the number of constraints in the constraint
-system. However, alternatively, when instead computing the limb values
-off-circuit and constructing a system of k linear equations, we can ensure that
-the product was computed correctly.
+system.
 
-Let the factors be
+For multiplication, we would instead use polynomial representation of the elements:
 
 	x = ∑_{i=0}^k x_i 2^{w i}
-
-and
-
 	y = ∑_{i=0}^k y_i 2^{w i}.
 
-For computing the product, we compute off-circuit the limbs
-
-	z_i = ∑_{j, j'>0, j+j'=i, j+j'≤2k-2} x_{j} y_{j'}, // in MultiplicationHint()
-
-and assert in-circuit
-
-	∑_{i=0}^{2k-2} z_i c^i = (∑_{i=0}^k x_i) (∑_{i=0}^k y_i), ∀ c ∈ {1, ..., 2k-1}.
-
-Computing the overflow for the multiplication result is slightly more
-complicated. The overflow for
-
-	x_{j} y_{j'}
-
-is
-
-	w+f+f'+1.
-
-Naively, as the limbs of the result are summed over all 0 ≤ i ≤ 2k-2, then the
-overflow of the limbs should be
-
-	w+f+f'+2k-1.
+as
 
-For computing the number of bits and thus in the overflow, we can instead look
-at the maximal possible value. This can be computed by
+	x(X) = ∑_{i=0}^k x_i X^i
+	y(X) = ∑_{i=0}^k y_i X^i.
 
-	(2^{2w+f+f'+2}-1)*(2k-1).
+If the multiplication result modulo r is c, then the following holds:
 
-Its bitlength is
+	x * y = c + z*r.
 
-	2w+f+f'+1+log_2(2k-1),
+We can check the correctness of the multiplication by checking the following
+identity at a random point:
 
-which leads to maximal overflow of
+	x(X) * y(X) = c(X) + z(X) * r(X) + (2^w' - X) e(X),
 
-	w+f+f'+1+log_2(2k-1).
+where e(X) is a polynomial used for carrying the overflows of the left- and
+right-hand side of the above equation.
 
 # Subtraction
 

std/math/emulated/field_mul.go

@@ -9,6 +9,48 @@ import (
 	"github.com/consensys/gnark/std/multicommit"
 )
 
+// mulCheck represents a single multiplication check. Instead of doing a
+// multiplication exactly where called, we compute the result using hint and
+// return it. Additionally, we store the correctness check for later checking
+// (together with every other multiplication) to share the verifier challenge
+// computation.
+//
+// With this approach this is important that we do not change the [Element]
+// values after they are returned from [mulMod] as mulCheck keeps pointers and
+// the check will fail if the values refered to by the pointers change. By
+// following the [Field] public methods this shouldn't happend as we always take
+// and return pointers, and to change the values the user has to explicitly
+// dereference.
+//
+// We store the values a, b, r, k, c. They are as follows:
+//   - a, b - the inputs what we are multiplying. Do not have to be reduced.
+//   - r - the multiplication result reduced modulo the emulation parameter.
+//   - k - the quotient for integer multiplication a*b divided by emulation parameter.
+//   - c - element representing carry. Used only for aligning the limb widths.
+//
+// Given these values, the following holds:
+//
+//	a * b = r * k*p
+//
+// But for asserting that the previous equation holds, we instead use the
+// polynomial representation of the elements. If a non-native element a is given
+// by its limbs
+//
+//	a = (a_0, ..., a_n)
+//
+// then
+//
+//	a(X) = \sum_i a_i * X^i.
+//
+// Now, the multiplication check instead becomes
+//
+//	a(X) * b(X) = r(X) + k(X) * p(X) + (2^t-X) c(X),
+//
+// which can be checked only at a single random point. Here we need an
+// additional polynomial c(X) which is used for carrying the overflow bits to
+// the consecutive limbs. By subtracting 2^t c(X) we can remove the bits from
+// the corresponding coefficients in r(X)+k(X)*p(X) and by adding X c(X) we can
+// add the bits to X(r(X) + k(X) * p(X)) (i.e. to the next coefficient).
 type mulCheck[T FieldParams] struct {
 	f *Field[T]
 	// a * b = r + k*p + c
@@ -18,23 +60,34 @@ type mulCheck[T FieldParams] struct {
 	c    *Element[T] // carry
 }
 
+// evalRound1 evaluates first c(X), r(X) and k(X) at a given random point at[0].
+// In the first round we do not assume that any of them is already evaluated as
+// they come directly from hint.
 func (mc *mulCheck[T]) evalRound1(api frontend.API, at []frontend.Variable) {
 	mc.c = mc.f.evalWithChallenge(mc.c, at)
 	mc.r = mc.f.evalWithChallenge(mc.r, at)
 	mc.k = mc.f.evalWithChallenge(mc.k, at)
 }
 
+// evalRound2 now evaluates a and b at a given random point at[0]. However, it
+// may happen that a or b is equal to r from a previous mulcheck. In that case
+// we can reuse the evaluation to save constraints.
 func (mc *mulCheck[T]) evalRound2(api frontend.API, at []frontend.Variable) {
 	mc.a = mc.f.evalWithChallenge(mc.a, at)
 	mc.b = mc.f.evalWithChallenge(mc.b, at)
 }
 
+// check checks a(ch) * b(ch) = r(ch) + k(ch) * p(ch) + (2^t - ch) c(ch). As the
+// computation of p(ch) and (2^t-ch) can be shared over all mulCheck instances,
+// then we get them already evaluated as peval and coef.
 func (mc *mulCheck[T]) check(api frontend.API, peval, coef frontend.Variable) {
 	ls := api.Mul(mc.a.evaluation, mc.b.evaluation)
 	rs := api.Add(mc.r.evaluation, api.Mul(peval, mc.k.evaluation), api.Mul(mc.c.evaluation, coef))
 	api.AssertIsEqual(ls, rs)
 }
 
+// cleanEvaluations cleans the cached evaluation values. This is necessary for
+// ensuring the circuit stability over many compilations.
 func (mc *mulCheck[T]) cleanEvaluations() {
 	mc.a.evaluation = 0
 	mc.a.isEvaluated = false
@@ -48,7 +101,9 @@ func (mc *mulCheck[T]) cleanEvaluations() {
 	mc.c.isEvaluated = false
 }
 
-func (f *Field[T]) mulMod(a, b *Element[T], nextOverflow uint) *Element[T] {
+// mulMod returns a*b mod r. In practice it computes the result using a hint and
+// defers the actual multiplication check.
+func (f *Field[T]) mulMod(a, b *Element[T], _ uint) *Element[T] {
 	f.enforceWidthConditional(a)
 	f.enforceWidthConditional(b)
 	k, r, c, err := f.callMulHint(a, b)
@@ -67,6 +122,10 @@ func (f *Field[T]) mulMod(a, b *Element[T], nextOverflow uint) *Element[T] {
 	return r
 }
 
+// evalWithChallenge represents element a as a polynomial a(X) and evaluates at
+// at[0]. For efficiency, we use already evaluated powers of at[0] given by at.
+// It stores the evaluation result inside the Element and marks it as evaluated.
+// If the method is called for already evaluated a then returns the known value.
 func (f *Field[T]) evalWithChallenge(a *Element[T], at []frontend.Variable) *Element[T] {
 	if a.isEvaluated {
 		return a
@@ -83,6 +142,8 @@ func (f *Field[T]) evalWithChallenge(a *Element[T], at []frontend.Variable) *Ele
 	return a
 }
 
+// performMulChecks should be deferred to actually perform all the
+// multiplication checks.
 func (f *Field[T]) performMulChecks(api frontend.API) error {
 	// use given api. We are in defer and API may be different to what we have
 	// stored.
@@ -107,7 +168,9 @@ func (f *Field[T]) performMulChecks(api frontend.API) error {
 		toCommit = append(toCommit, f.mulChecks[i].k.Limbs...)
 		toCommit = append(toCommit, f.mulChecks[i].c.Limbs...)
 	}
+	// we give all the inputs as inputs to obtain random verifier challenge.
 	multicommit.WithCommitment(api, func(api frontend.API, commitment frontend.Variable) error {
+		// for efficiency, we compute all powers of the challenge as slice at.
 		coefsLen := 0
 		for i := range f.mulChecks {
 			coefsLen = max(coefsLen, len(f.mulChecks[i].c.Limbs))
@@ -118,17 +181,21 @@ func (f *Field[T]) performMulChecks(api frontend.API) error {
 			at[i] = api.Mul(prev, commitment)
 			prev = at[i]
 		}
+		// evaluate all r, k, c
 		for i := range f.mulChecks {
 			f.mulChecks[i].evalRound1(api, at)
 		}
 		// assuming r is input to some other multiplication, then is already evaluated
 		for i := range f.mulChecks {
 			f.mulChecks[i].evalRound2(api, at)
 		}
+		// evaluate p(X) at challenge
 		pval := f.evalWithChallenge(f.Modulus(), at)
+		// compute (2^t-X) at challenge
 		coef := big.NewInt(1)
 		coef.Lsh(coef, f.fParams.BitsPerLimb())
 		ccoef := api.Sub(coef, commitment)
+		// verify all mulchecks
 		for i := range f.mulChecks {
 			f.mulChecks[i].check(api, pval.evaluation, ccoef)
 		}
@@ -142,6 +209,7 @@ func (f *Field[T]) performMulChecks(api frontend.API) error {
 	return nil
 }
 
+// callMulHint uses hint to compute r, k and c.
 func (f *Field[T]) callMulHint(a, b *Element[T]) (quo, rem, carries *Element[T], err error) {
 	// inputs is always nblimbs
 	// quotient may be larger if inputs have overflow
@@ -246,23 +314,20 @@ func mulHint(field *big.Int, inputs, outputs []*big.Int) error {
 	return nil
 }
 
-// Mul computes a*b and returns it. It doesn't reduce the output and it may be
-// larger than the modulus. The returned Element has as many limbs as the inputs
-// together. If the result wouldn't fit into Element, then locally reduces the
-// inputs first. Doesn't mutate inputs.
-//
-// Even though this method skips reduction and allows for multiplication chains,
-// then in most cases it is more efficient to use [Field[T].MulMod] as reducing
-// Element with 2 times the limbs is 2 times more expensive.
+// Mul computes a*b and reduces it modulo the field order. The returned Element
+// has default number of limbs and zero overflow. If the result wouldn't fit
+// into Element, then locally reduces the inputs first. Doesn't mutate inputs.
 //
 // For multiplying by a constant, use [Field[T].MulConst] method which is more
 // efficient.
 func (f *Field[T]) Mul(a, b *Element[T]) *Element[T] {
 	return f.reduceAndOp(f.mulMod, f.mulPreCond, a, b)
 }
 
-// Mul computes a*b and reduces it modulo the field order. The returned Element
+// MulMod computes a*b and reduces it modulo the field order. The returned Element
 // has default number of limbs and zero overflow.
+//
+// Equivalent to [Field[T].Mul], kept for backwards compatibility.
 func (f *Field[T]) MulMod(a, b *Element[T]) *Element[T] {
 	return f.reduceAndOp(f.mulMod, f.mulPreCond, a, b)
 }
@@ -321,6 +386,8 @@ func (f *Field[T]) mulPreCond(a, b *Element[T]) (nextOverflow uint, err error) {
 }
 
 func (f *Field[T]) mul(a, b *Element[T], nextOverflow uint) *Element[T] {
+	// TODO: kept for [AssertIsEqual]. Consider if this can be removed and we
+	// can use MulMod for equality assertion.
 	ba, aConst := f.constantValue(a)
 	bb, bConst := f.constantValue(b)
 	if aConst && bConst {