Assert for add_to_lower_limb
could be ineffective due to overflow
Description
The function add_to_lower_limb
starts like this:
/**
* @brief Add a field element to the lower limb. CAUTION (the element has to be constrained before using this function)
*
* @details Sometimes we need to add a small constrained value to a bigfield element (for example, a boolean value), but
* we don't want to construct a full bigfield element for that as it would take too many gates. If the maximum value of
* the field element being added is small enough, we can simply add it to the lowest limb and increase its maximum
* value. That will create 2 additional constraints instead of 5/3 needed to add 2 bigfield elements and several needed
* to construct a bigfield element.
*
* @tparam Builder Builder
* @tparam T Field Parameters
* @param other Field element that will be added to the lower
* @param other_maximum_value The maximum value of other
* @return bigfield<Builder, T> Result
*/
template <typename Builder, typename T>
bigfield<Builder, T> bigfield<Builder, T>::add_to_lower_limb(const field_t<Builder>& other,
uint256_t other_maximum_value) const
{
reduction_check();
ASSERT((other_maximum_value + binary_basis_limbs[0].maximum_value) <= get_maximum_unreduced_limb_value());
What is needed for the function to work properly is that other_maximum_value + binary_basis_limbs[0].maximum_value
must be smaller or equal to get_maximum_unreduced_limb_value()
. The ASSERT
in the snippet above checks this under the assumption that the sum on the left-hand side does not wrap around (so if the sum is not 1<<256
or larger). While the documenting comments for add_to_lower_limb
suggest that the function is needed for situations in which only a small value such as a boolean is added, the function does not prevent usage with values for other_maximum_value
that are close to the maximum value for 256-bit unsigned integers. In that case, the overflow could actually happen.
To ensure an overflow does not happen, it could additionally be asserted that both other_maximum_value
and binary_basis_limbs[0].maximum_value
are less than or equal to get_maximum_unreduced_limb_value()
. The latter of these two checks is already enforced by reduction_check()
, so it does not need to be repeated.
However, note that the reduction check does not actually ensure that the crucial assert will hold. While it will ensure that binary_basis_limbs[0].maximum_value <= get_maximum_unreduced_limb_value()
, it could happen that binary_basis_limbs[0].maximum_value = get_maximum_unreduced_limb_value()
, in which case even a low value as other_maximum_value=1
will fail the assertion after the reduction check in add_to_lower_limb
.
Impact
Under the unlikely case that a caller uses add_to_lower_limb
with a very large value for other_maximum_value
so that other_maximum_value + binary_basis_limbs[0].maximum_value >= 1<<256
, the function would produce the wrong result.
Furthermore, it is possible that the assert fails even with benign inputs.
Recommendations
To prevent the edge case of a too large other_maximum_value
, we recommend to add an assert such as
template <typename Builder, typename T>
bigfield<Builder, T> bigfield<Builder, T>::add_to_lower_limb(const field_t<Builder>& other,
uint256_t other_maximum_value) const
{
reduction_check();
ASSERT((other_maximum_value + binary_basis_limbs[0].maximum_value) <= get_maximum_unreduced_limb_value());
+ ASSERT(other_maximum_value <= get_maximum_unreduced_limb_value());
Alternatively, perform the existing assert with 512-bit unsigned integers, to ensure a wraparound cannot happen.
To ensure that the main assert will not fail with benign inputs, one might consider doing something like in the following pseudocode:
// First check that the sum won't overflow in Fr
ASSERT((uint512_t)other_maximum_value + (uint512_t)binary_basis_limbs[0].maximum_value < (uint512_t)bb::fr::modulus);
// calculate result
// ...
// reduce result if needed
result.reduction_check();
In this case, the function will only fail if one of the inputs is very unusually large so that the first assert fails. The reduction check on the result at the end will ensure that the lowest-resulting limb will be at most get_maximum_unreduced_limb_value()
.