Possible shaper bounds

We list some calculations of bounds that could be made sharper.

Maximum value for constant limbs

The Limb structure has a field maximum_value for the maximum value that the wrapped circuit variable may have. From usage in the remaining codebase, it is clear that this is intended as an upper bound that can be reached. However, the constructor of Limb sets maximum_value to one higher than the actual value in the case of a constant:

Limb(const field_t<Builder>& input, const uint256_t max = uint256_t(0))
    : element(input)
{
    if (input.witness_index == IS_CONSTANT) {
        maximum_value = uint256_t(input.additive_constant) + 1;
    } else if (max != uint256_t(0)) {
        maximum_value = max;
    } else {
        maximum_value = DEFAULT_MAXIMUM_LIMB;
    }
}

It would be sharper to use maximum_value = uint256_t(input.additive_constant); in the constant case. However, see also Finding ref↗.

The following member function for Limb produces output that reflects an incorrect meaning of maximum_value; it should use <= or ≤ instead of <:

friend std::ostream& operator<<(std::ostream& os, const Limb& a)
{
    os << "{ " << a.element << " < " << a.maximum_value << " }";
    return os;
}

Lower bound for square root of maximum_product in get_maximum_unreduced_value

The get_maximum_unreduced_value function is intended to return a lower bound for the square root of maximum_product.

static constexpr uint512_t get_maximum_unreduced_value(const size_t num_products = 1)
{
    // return (uint512_t(1) << 256);
    uint1024_t maximum_product = uint1024_t(binary_basis.modulus) * uint1024_t(prime_basis.modulus) / uint1024_t(static_cast<uint64_t>(num_products));
    // TODO: compute square root (the following is a lower bound, so good for the CRT use)
    uint64_t maximum_product_bits = maximum_product.get_msb() - 1;
    return (uint512_t(1) << (maximum_product_bits >> 1)) - uint512_t(1);
}

The bound can be sharpened, as we now explain. In our exposition, we will assume num_products=1, which does not change any of the arguments, though.

The return value must satisfy return_value <= maximum_product^(1/2), if maximum_product is the maximum value that a product is allowed to take. However, as maximum_product, as calculated in the current code, is the CRT modulus, this is actually already too big. To avoid wraparound modulo the CRT modulus, maximum_product should be calculated as follows (pseudocode):

maximum_product = (((binary_basis.modulus * prime_basis.modulus) - 1) / num_products);

Note that due to the remainder of the function not being sharp, this small mistake does not cause any issues in the current code.

Now, with the corrected maximum_product, we must ensure that return_value <= maximum_product^(1/2). Let us assume we have a value for maximum_product_bits so that maximum_product >= 2^maximum_product_bits. Then it follows from this that

2^(maximum_product_bits >> 1) <= 2^(maximum_product_bits / 2) = (2^maximum_product_bits)^(1/2) <= maximum_product^(1/2)

A value for maximum_product_bits that satisfies maximum_product >= 2^maximum_product_bits is maximum_product.get_msb(), as if the i-th bit is set in maximum_product, then we must have 2^i <= maximum_product.

Thus, a sharper bound could be obtained with the following pseudocode:

static constexpr uint512_t get_maximum_unreduced_value(const size_t num_products = 1)
{
    // return (uint512_t(1) << 256);
    uint1024_t maximum_product = ((uint1024_t(binary_basis.modulus) * uint1024_t(prime_basis.modulus)) - 1) / uint1024_t(static_cast<uint64_t>(num_products));
    // TODO: compute square root (the following is a lower bound, so good for the CRT use)
    uint64_t maximum_product_bits = maximum_product.get_msb();
    return (uint512_t(1) << (maximum_product_bits >> 1));
}

Maximum value of last limb in bigfield constructor

In the constructor bigfield<Builder, T>::bigfield(const byte_array<Builder>& bytes), at the end, the bound is computed with

const auto num_last_limb_bits = 256 - (NUM_LIMB_BITS * 3);
res.binary_basis_limbs[3].maximum_value = (uint64_t(1) << num_last_limb_bits);

The maximum value here is not as sharp as it could be. One can be subtracted since maximum_value is an upper bound that can be attained and (uint64_t(1) << num_last_limb_bits) - 1 is the maximum that a value that is num_last_limb_bits-bits wide can attain.

Maximum quotient bits

The get_quotient_max_bits function is implemented as follows:

/**
 * @brief Compute the maximum number of bits for quotient range proof to protect against CRT underflow
 *
 * @param remainders_max Maximum sizes of resulting remainders
 * @return Desired length of range proof
 */
static size_t get_quotient_max_bits(const std::vector<uint1024_t>& remainders_max)
{
    // find q_max * p + ...remainders_max < nT
    uint1024_t base = get_maximum_crt_product();
    for (const auto& r : remainders_max) {
        base -= r;
    }
    base /= modulus_u512;
    return static_cast<size_t>(base.get_msb() - 1);
}

As the comments indicate, it is intended to compute the maximum bit width that ensures that values q with that bit width still satisfy q*p + sum(remainders_max) < CRT modulus.

In the implementation, the intention is to first find the maximum value the product q*p is allowed to take (base after the loop), then divide by p to obtain the maximum value for q, and finally obtain the maximum bits that ensure that numbers with that bit width are less than or equal to the obtained maximum for q.

For the first step, there is a small mistake in the implementation in that base should start with uint1024_t base = get_maximum_crt_product() - 1;, so one smaller than in the current implementation. This is because q*p + sum(remainders_max) is to be strictly smaller than the CRT modulus, not smaller than or equal to it.

This mistake is, however, overcompensated for with a less-strict-than-necessary estimate for the last step. If after division base is the maximum value that is allowed for q, then with b = base.get_msb(), we have that the b-th bit is the most significant bit set in q. Thus, we have 2^b <= q < 2^(b+1). Any value with a bit width less than or equal to b is at most (2^b) - 1 (bits 0 through b-1 set). The upshot is that it is fine to return base.get_msb() instead of base.get_msb() - 1. This is assuming the change reducing the initial value of base by 1 is made as well.