Functioning of evaluate_non_native_field_multiplication

We give a rough overview of how the function evaluate_non_native_field_multiplication in cpp/src/barretenberg/stdlib_circuit_builders/ultra_circuit_builder.cpp is intended to work. Note that this function was out of scope for our audit, so we did not verify in detail whether the actual constraints imposed accurately reflect the intended specification for this function.

The function gets a, b, q, and neg_modulus (which we will call -p from now on) as arguments, each given with four binary limbs $t_0,t_1,t_2,t_3$ (there is also a prime limb, but it is not used in this function), with the value represented given by $t_0+2^{68}\cdot t_1+2^{2\cdot 68}\cdot t_2+2^{3\cdot 68}\cdot t_3$. The binary limbs can hold values wider than 68 bits, however.

The core computation of the function is summarized by the following snippet containing the out-of-circuit calculation of the witnesses, which are then constrained elsewhere in the function:

FF lo_0 = a[0] * b[0] - r[0] + (a[1] * b[0] + a[0] * b[1]) * LIMB_SHIFT;
FF lo_1 = (lo_0 + q[0] * input.neg_modulus[0] + (q[1] * input.neg_modulus[0] + q[0] * input.neg_modulus[1] - r[1]) * LIMB_SHIFT) * LIMB_RSHIFT_2;

FF hi_0 = a[2] * b[0] + a[0] * b[2] + (a[0] * b[3] + a[3] * b[0] - r[3]) * LIMB_SHIFT;
FF hi_1 = hi_0 + a[1] * b[1] - r[2] + (a[1] * b[2] + a[2] * b[1]) * LIMB_SHIFT;
FF hi_2 = (hi_1 + lo_1 + q[2] * input.neg_modulus[0] + (q[3] * input.neg_modulus[0] + q[2] * input.neg_modulus[1]) * LIMB_SHIFT);
FF hi_3 = (hi_2 + (q[0] * input.neg_modulus[3] + q[1] * input.neg_modulus[2]) * LIMB_SHIFT + (q[0] * input.neg_modulus[2] + q[1] * input.neg_modulus[1])) * LIMB_RSHIFT_2;

The constant LIMB_SHIFT has value 1 << 68, and LIMB_RSHIFT_2 is the inverse of 1 << (2*68) in the scalar field ${\mathbb{F}}_r$, where $r$ is the native circuit prime modulus.

Let us assume there are no overflows or underflows in the calculations above so that we may assume calculations happen in integers rather than ${\mathbb{F}}_r$.

Then lo_1 * LIMB_SHIFT^2 is congruent to a*b - p * q - r modulo 2^(2 * 68). Thus, we can ensure that a*b - p * q - r = 0 modulo 2^(2 * 68) as follows. We range check lo_1 to be less than r / 2^(2 * 68). Then, no overflow will happen in the term lo_1 * LIMB_SHIFT^2 so that we obtain that a*b - p * q - r is indeed congruent to a multiple of 2^(2 * 68) modulo 2^(2 * 68) and hence congruent to 0.

If we assume that a*b - p * q - r is congruent to 0 modulo 2^(2 * 68), then hi_3 * LIMB_SHIFT^2 will calculate (a * b - p * q - r) / 2^(2 * 68) modulo 2^(2 * 68). Similarly as before, range checking hi_3 to be less than r / 2^(2 * 68) ensures that (a * b - p * q - r) / 2^(2* 68) is congruent to 0 modulo 2^(2 * 68) and thus that a * b - p * q - r is congruent to 0 modulo 2^(4 * 68).

Note that r / 2^(2 * 68) rounds down to 251264705520246785319773662051664216, which has 118 bits. So a range check for 117 bits would suffice.

What evaluate_non_native_field_multiplication returns are the variable indexes of lo_1 and hi_3. However, the range check is not performed in the function itself but must be handled by the caller. The function is documented as follows:

* @brief Queue up non-native field multiplication data.
*
* @details The data queued represents a non-native field multiplication identity a * b = q * p + r,
* where a, b, q, r are all emulated non-native field elements that are each split across 4 distinct witness variables.
*
* Without this queue some functions, such as bb::stdlib::element::multiple_montgomery_ladder, would
* duplicate non-native field operations, which can be quite expensive. We queue up these operations, and remove
* duplicates in the circuit finishing stage of the proving key computation.
*
* The non-native field modulus, p, is a circuit constant
*
* The return value are the witness indices of the two remainder limbs `lo_1, hi_2`
*
* N.B.: This method does NOT evaluate the prime field component of non-native field multiplications.

These documentation comments do not make clear that the identity a * b = q * p + r is not enforced by the function but that the caller must perform an appropriate range check on the two returned circuit variables. We recommend to make this clearer.