Description

The functioning of bigfield functions rely crucially on the assumption that the prime limb is consistent with the unsigned integer stored in the binary limbs. See the discussion in section ref↗. Breaking this assumption would allow for proving incorrect relations in, for example, unsafe_evaluate_multiply_add, where equality is checked separately modulo $2^t$ (using the binary limbs) and modulo $r$ (using the prime limbs), which can ultimately mean proving, for example, incorrect products.

However, the following constructor does not ensure that the prime limb is consistent with the binary limbs:

// we assume the limbs have already been normalized!
bigfield(const field_t<Builder>& a,
         const field_t<Builder>& b,
         const field_t<Builder>& c,
         const field_t<Builder>& d,
         const field_t<Builder>& prime_limb,
         const bool can_overflow = false)
{
    context = a.context;
    binary_basis_limbs[0] = Limb(field_t(a));
    binary_basis_limbs[1] = Limb(field_t(b));
    binary_basis_limbs[2] = Limb(field_t(c));
    binary_basis_limbs[3] =
        Limb(field_t(d), can_overflow ? DEFAULT_MAXIMUM_LIMB : DEFAULT_MAXIMUM_MOST_SIGNIFICANT_LIMB);
    prime_basis_limb = prime_limb;
};

Impact

Further computations are based on the crucial assumption that the prime limb is consistent with the binary limbs. Violation of that assumption can, for example, allow proving an incorrect product of such a bigfield element with another.

Recommendations

Constrain prime_limb to be consistent with the binary limbs. Alternatively, document clearly that the caller is responsible for ensuring this.

Additionally, for defense in depth, we recommend to assert consistency of the binary limbs with the prime limb in bigfield<Builder, T>::get_value() and for the inputs in the functions that check things separately for binary and prime modulus, such as unsafe_evaluate_multiply_add.

Remediation