Description

The maximum unreduced limb size is computed as follows:

// a (currently generous) upper bound on the log of number of fr additions in any of the class operations
static constexpr uint64_t MAX_ADDITION_LOG = 10;
// the rationale of the expression is we should not overflow Fr when applying any bigfield operation (e.g. *) and
// starting with this max limb size
static constexpr uint64_t MAX_UNREDUCED_LIMB_SIZE = (bb::fr::modulus.get_msb() + 1) / 2 - MAX_ADDITION_LOG;

static constexpr uint256_t get_maximum_unreduced_limb_value() { return uint256_t(1) << MAX_UNREDUCED_LIMB_SIZE; }

Let $r$ be the native prime modulus of the circuit, $p$ the emulated modulus (so bb::fr::modulus) and b = bb::fr::modulus.get_msb().

The intention here seems to be as follows. What is needed is a bound $m$ so that ${\sum }_{i=1}^k{a}_i\cdot b_i<p$ as long as $k\le 2^{10}$ and $a_i,b_i\le m$.

Let us first consider the calculation of $m$ (as get_maximum_unreduced_limb_value()) in the code in the case where the bound for $k$ were $k\le 1$, so we only consider a single summand. This corresponds to MAX_ADDITION_LOG = 0. Then we would have $m=2^{\lfloor \frac{b+1}{2}\rfloor }$. From the definition of $b$, it is the most significant bit of $p$ that is set, so we have $2^b<p<2^{b+1}$. (The reason we have $2^b<p$ and not just $2^b\le p$ is that $p$ is an odd prime.) If we assume that $b$ is odd, then we would have $m^2=2^{b+1}>p$. Thus, the intended property of $m$ would not be satisfied. The issue is the addition of one; if we took $m=2^{\lfloor \frac{b}{2}\rfloor }$ instead, then we would have $m^2\le 2^b<p$.

However, there appears to be another mistake, this time making the bound less sharp, which overcompensates for the just discussed one. Concretely, suppose $m_1$ is a correct bound as above for the one-summand case, so that $m_1^2<p$. Then for the case of up to $2^{10}$ summands, the code uses $m=m_1\cdot 2^{-10}$. Then we get that ${\sum }_{i=1}^k{a}_i\cot b_i\le 2^{10}\cdot m_1^2\cdot 2^{-10\cdot 2}<2^{-10}\cdot p$, so $m$ is smaller than necessary. Instead of reducing the bit width of both factors by 10 bits, only the products need to be reduced in bit width by 10 bits, for which it suffices to reduce the bit width of each factor by five bits, so in MAX_UNREDUCED_LIMB_SIZE, the contribution of MAX_ADDITION_LOG could be divided by two as well.

Impact

The mistake reducing sharpness overcorrects for the other mistake, so there is no impact currently. However, there is a risk that making the MAX_ADDITION_LOG contribution sharp at a later time without correcting the other mistake will cause a bound that violates the required assumption.

Recommendations

We recommend to replace

static constexpr uint64_t MAX_UNREDUCED_LIMB_SIZE = (bb::fr::modulus.get_msb() + 1) / 2 - MAX_ADDITION_LOG;

by

static constexpr uint64_t MAX_UNREDUCED_LIMB_SIZE = (bb::fr::modulus.get_msb() - MAX_ADDITION_LOG) / 2;

Remediation