Unnecessary assert in mul_product_overflows_crt_modulus

The two functions mul_product_overflows_crt_modulus are used to check if terms of the form ${\sum }_{i=0}^k{a}_i\cdot b_i+{\sum }_{i=0}^l{c}_i$ would overflow modulo the CRT modulus $2^t\cdot r$, where $r$ is the native circuit prime modulus. One variant is for the case in which $k=0$ — otherwise they are identical. The single-product variant is implemented as follows:

static bool mul_product_overflows_crt_modulus(const uint1024_t& a_max,
                                                  const uint1024_t& b_max,
                                                  const std::vector<bigfield>& to_add)
{
    uint1024_t product = a_max * b_max;
    uint1024_t add_term;
    for (const auto& add : to_add) {
        add_term += add.get_maximum_value();
    }
    constexpr uint1024_t maximum_default_bigint = uint1024_t(1) << (NUM_LIMB_BITS * 6 + NUM_LAST_LIMB_BITS * 2);

    // check that the add terms alone cannot overflow the crt modulus. v. unlikely so just forbid circuits that
    // trigger this case
    ASSERT(add_term + maximum_default_bigint < get_maximum_crt_product());
    return ((product + add_term) >= get_maximum_crt_product());
}

It is unclear what the reason of the assertion add_term + maximum_default_bigint < get_maximum_crt_product() is here. The comment suggests the intention to forbid cases in which the sum (${\sum }_{i=0}^l{c}_i$ in the expression at the start) would already overflow. This would be the check add_term < get_maximum_crt_product(), so it is unclear why maximum_default_bigint is added.

Note that we have the following bound for get_maximum_crt_product:

get_maximum_crt_product() = r*2^t = r * 2^(4*68) > (r-1) * 2^(272)

The maximum value an unreduced bigfield could possibly attain is one in which all four binary limbs are r-1. This value is

(r-1)*(1 + 2^68 + 2^(2*68) + 2^(3*68)) < (r-1) * 2^(3*68+1) = (r-1) * 2^205

The number of addition terms needed to overflow the CRT modulus in a sum are thus at least 2^(272-205) = 2^67. This is an unrealistic number of summands, so such an overflow should never happen in practice.

The value of maximum_default_bigint is 2^(2*s), where s is the number of bits of p. Note that s<=256 as the emulated prime can be at most 256 bits. Thus, the number of addition terms needed for add_term + maximum_default_bigint >= get_maximum_crt_product() to be possible is at least

  ((r-1) * 2^272 - 2^512)  /  ((r-1) * 2^205)
> (2^253 * 2^272 - 2^512)  /  (2^254 * 2^205)
= (2^525 - 2^512) / 2^459
> 2^525 / 2^459
= 2^66

This is still an unrealistic number of summands, so the current assert should also never trigger in practice.

The maximum value get_maximum_value() can return for a bigfield element is less than 2^(256+3*68)=2^460, so a product of two such values will be less than 2^920. Thus, an overflow due to adding product is also not possible in practice, as long as a_max and b_max are obtained from such a call to get_maximum_value().