Undocumented assumption regarding meaning of bigfield fields

Every bigfield consists of four binary limbs and a prime limb. The prime limb directly determines a value modulo the native circuit field modulus $r$. The binary limbs are interpreted as an integer similarly to four digits of an integer in $2^{68}$-ary representation. Thus, if the limbs are $l_0,l_1,l_2,l_3$, then the value will be ${\sum }_{i=0}^3{l}_i\cdot 2^{i\cdot 68}$. However, unlike true $2^{68}$-ary representation, the limbs can also be bigger than or equal to $2^{68}$; the represented integer is still given by the above sum.

The documentation contains passages like the following:

So technically, if we could perform operations modulo some number $m$ with $m>p^2$, then it would be enough to compute values modulo $p$. How do we get a modulus $m>p^2$, when we have just operations modulo $p$. Well, let's imagine for a second that we can implement operations modulo some number $z>p$, such that $z\ast n>p^2$ and $z$ and $n$ are coprime. Then we can use Chinese Remainder Theorem to implement operations modulo $z\ast n$. If you don't know how CRT works, you can read about it under spoiler.

In this quote, $n$ refers to the native modulus of the circuit (which we refer to by $r$), and $p$ refers to the emulated modulus. Given this documentation, the reader might think that it is possible to use bigfield instances in which the value is given by the CRT of the values modulo the prime and binary modulus $2^t=2^{4\cdot 68}$. For example, if one were to want to construct the value $2^t$ modulo $p$, it may be reasonable to think that one can do so by setting the binary limbs to zero and the prime limb to $2^t\mathrm{mod}r$. The CRT of those values would then be the intended $2^t$. The quote also suggests that the integer represented by the binary limbs will be interpreted as representing a value modulo $2^t$.

However, the code differs from this interpretation in two ways.

Firstly, the values stored in the limbs are not interpreted using a CRT. Instead, only the value obtained from the binary limbs is used as the value of the bigfield element. The prime limb is then assumed to be the reduction of that value modulo the native modulus. This can be seen, for example, in the often-used function get_value, in which the return value depends only on the binary limbs, with the prime limb not being used:

template <typename Builder, typename T> uint512_t bigfield<Builder, T>::get_value() const
{
    uint512_t t0 = uint256_t(binary_basis_limbs[0].element.get_value());
    uint512_t t1 = uint256_t(binary_basis_limbs[1].element.get_value());
    uint512_t t2 = uint256_t(binary_basis_limbs[2].element.get_value());
    uint512_t t3 = uint256_t(binary_basis_limbs[3].element.get_value());
    return t0 + (t1 << (NUM_LIMB_BITS)) + (t2 << (2 * NUM_LIMB_BITS)) + (t3 << (3 * NUM_LIMB_BITS));
}

The prime limb is thus treated as redundant information. In principle, the prime limb could thus be removed from the bigfield class and recomputed wherever it is needed internally in computations, which happens when checking multiplicative relations of bigfield elements. However, recomputation of the prime limb costs about two gates. If many multiplications are using the same factors, computing the prime limb only once instead of recomputing it each time can thus save gates. Furthermore, on some operations, such as addition, it only costs a single gate to compute the prime limb of the result from the prime limbs of the inputs. The purpose of the prime limb is thus not to store data but to essentially cache the value represented by the binary limbs modulo $r$ as a performance improvement.

Secondly, the integer represented by the binary limbs is used as is and not interpreted as a congruence class modulo $2^t$. If it were treated as a congruence class modulo $2^t$, we would expect the smallest nonnegative representative to be used to convert to a number modulo $p$. In other words, if $l_0,l_1,l_2,l_3$ are the binary limbs, then the value modulo $p$ represented by this would be expected to be $\left(\left({\sum }_{i=0}^3{l}_i\cdot 2^{i\cdot 68}\right)\mathrm{mod}{2}^t\right)\mathrm{mod}p$. However, the code actually interprets those limbs as representing $\left({\sum }_{i=0}^3{l}_i\cdot 2^{i\cdot 68}\right)\mathrm{mod}p$.

As a concrete example, if we were to store the integer $2^t$ in the binary limbs, then the code will treat this as $2^t\mathrm{mod}p$ and not as $\left(2^t\mathrm{mod}{2}^t\right)\mathrm{mod}p=0\mathrm{mod}p=0$. This can also be seen with the following test case:

static void test_zellic_binary_modulus()
{
    size_t shift = 68;
    std::cout << "\nIn Zellic binary modulus test!" << std::endl;
    auto builder = Builder();
    fq_ct num(
        witness_ct(&builder, fr(uint256_t(0))),
        witness_ct(&builder, fr(uint256_t(0))),
        witness_ct(&builder, fr(uint256_t(0))),
        witness_ct(&builder, fr(uint256_t(1) << shift)),
        witness_ct(&builder, fr(uint256_t(0))),
        true
    );
    ASSERT(num.binary_basis_limbs[0].element.get_value() == 0);
    ASSERT(num.binary_basis_limbs[1].element.get_value() == 0);
    ASSERT(num.binary_basis_limbs[2].element.get_value() == 0);
    ASSERT(num.binary_basis_limbs[3].element.get_value() == uint256_t(1)<<shift);
    num.binary_basis_limbs[0].maximum_value = 0;
    num.binary_basis_limbs[1].maximum_value = 0;
    num.binary_basis_limbs[2].maximum_value = 0;
    num.binary_basis_limbs[3].maximum_value = uint256_t(1)<<shift;
    info("\nbefore reduction:");
    for (size_t limb_index = 0; limb_index < 4 ; limb_index++) {
        info("Limb ", limb_index, ": ", num.binary_basis_limbs[limb_index]);
    }
    num.self_reduce();
    info("\nafter reduction:");
    for (size_t limb_index = 0; limb_index < 4 ; limb_index++) {
        info("Limb ", limb_index, ": ", num.binary_basis_limbs[limb_index]);
    }
    bool result = CircuitChecker::check(builder);
    EXPECT_EQ(result, true);
}

With an interpretation of binary and prime limbs via CRT, setting them independently should be possible. And if they need to be consistent but the binary limbs are reduced modulo $2^t=2^{4\cdot 68}$, then making the prime limb zero would be consistent with the binary limbs representing $2^t$.

However, neither of those are the case, as can be seen by the fact that this test case will fail:

[ RUN      ] stdlib_bigfield/1.zellicbinarymodulus

In Zellic binary modulus test!

before reduction:
Limb 0: { 0x0000000000000000000000000000000000000000000000000000000000000000 < 0x0000000000000000000000000000000000000000000000000000000000000000 }
Limb 1: { 0x0000000000000000000000000000000000000000000000000000000000000000 < 0x0000000000000000000000000000000000000000000000000000000000000000 }
Limb 2: { 0x0000000000000000000000000000000000000000000000000000000000000000 < 0x0000000000000000000000000000000000000000000000000000000000000000 }
Limb 3: { 0x0000000000000000000000000000000000000000000000100000000000000000 < 0x0000000000000000000000000000000000000000000000100000000000000000 }

after reduction:
Limb 0: { 0x0000000000000000000000000000000000000000000000002e0850a4e1bc3b4f < 0x00000000000000000000000000000000000000000000000fffffffffffffffff }
Limb 1: { 0x00000000000000000000000000000000000000000000000b87d765f422f21d2d < 0x00000000000000000000000000000000000000000000000fffffffffffffffff }
Limb 2: { 0x00000000000000000000000000000000000000000000000b955105616bf7c17a < 0x00000000000000000000000000000000000000000000000fffffffffffffffff }
Limb 3: { 0x0000000000000000000000000000000000000000000000000000d42a313121fe < 0x0000000000000000000000000000000000000000000000000003ffffffffffff }
Failed Arithmetic relation at row idx = 1744
Failed at block idx = 1
/home/user/aztec-packages/barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/
bigfield.test.cpp:368: Failure
Expected equality of these values:
  result
    Which is: false
  true
[  FAILED  ] stdlib_bigfield/1.zellicbinarymodulus, where TypeParam = bb::UltraCircuitBuilder_<bb::UltraArith<bb::field<bb::Bn254FrParams> > > (29 ms)

We recommend to clearly document the correct interpretation of the binary and prime limbs as used by the implementation of the bigfield class.