fix: bigfield veridise audit fixes (#16842)

Summary of the fixes based on the audit of the `bigfield` class by
Veridise (on commit
[480f49d](https://github.com/AztecProtocol/aztec-packages/tree/480f49dad314ea4e753ff1e5180992a16926d2b3)):

#### [V-AZT-VUL-001: Missing zero-check for division by constant]()

Added an assertion that triggers when the divisor is a constant zero and
the flag `check_for_zero` is set to true. Also added a test that
validates this behaviour.

Response: Fixed in
bbf2f73

#### [V-AZT-VUL-002: Incomplete ‘assert_is_not_equal‘ assumes random
distribution]()

The function `assert_is_not_equal` is no longer exposed as a public
function (via noir). In fact, none of the non-native field methods (and
group operations) are exposed to developers via noir. Noir instead uses
the natively written
[noir-bignum](https://github.com/noir-lang/noir-bignum) library. (The
`bigint_constraint.cpp` file that contains the interface for non-native
field methods between noir and barretenberg is yet to be removed from
the repository, this will be done in an upcoming PR.)

Response: Acknowledged 

#### [V-AZT-VUL-003: borrow_lo rounds down]()

Updated the computation of `borrow_lo_value` to use ceiling instead of
floor:
```cpp
uint256_t borrow_lo_value = (max_remainders_lo + ((uint256_t(1) << (2 * NUM_LIMB_BITS)) - 1)) >> (2 * NUM_LIMB_BITS);
```

Response: Fixed in
c1bdd88

#### [V-AZT-VUL-004: Unsafe default for `msub_div()`]()

Changed the default value of `enable_divisor_nz_check` to `true` and
explicitly pass it as `false` in its usage in the `biggroup` class. In a
few instances, passing this parameter as `false` can lead to incorrect
handling of the point at infinity, added TODOs at such places. These
instances will be analysed separately to avoid any unexpected behaviour.

Response: Fixed in
25e820c,
usage of `msub_div` will be analysed separately

#### [V-AZT-VUL-005: Limbs with a maximum value of 0 trigger compilation
failure]()

In the function `decompose_into_default_range` we have an assertion:
```cpp
ASSERT(num_bits > 0)
``` 
because number of bits (of a circuit variable) being 0 does not really
make sense. The only case when `carry_hi_msb` or `carry_lo_msb` can be 0
is when:
```cpp
template <typename Builder, typename T>
void bigfield<Builder, T>::unsafe_evaluate_multiply_add(const bigfield& input_left,
                                                        const bigfield& input_to_mul,
                                                        const std::vector<bigfield>& to_add,
                                                        const bigfield& input_quotient,
                                                        const std::vector<bigfield>& input_remainders)
```
is called with `input_to_mul` as constant 0 and/or `input_quotient` as
constant 0. In the usage of the function `unsafe_evaluate_multiply_add`
(or `unsafe_evaluate_multiple_multiply_add`) the `input_quotient` is
always a circuit witness. This ensures that the `carry_lo_msb > 0` and
`carry_hi_msb > 0` (added assertions to verify this empirically).

Response: We think it does not make sense to support `num_bits = 0` in
range constraint functions, but open to discussion on this if there's
any way `carry_lo_msb` or `carry_hi_msb` can actually be 0 in practice.

#### [V-AZT-VUL-006: Off-by-one comparison of
maximum_unreduced_limb_value]()

Changed the definition of `get_maximum_unreduced_limb_value()` to $2^Q -
1$ (from $2^Q$).

Response: Fixed in
3da35ba

#### [V-AZT-VUL-007: Maintainability Improvements]()

1. Removed unused constants:
    - `bigfield.prime_basis_maximum_limb`
    - `bigfield.shift_right_1`
    - `bigfield.shift_right_2`
2. Renamed `negative_prime_modulus_mod_binary_basis` to
`negative_prime_modulus_mod_native_basis` and use that while checking
the prime limb consistency (in `evaluate_polynomial_identity`)
3. Used `NUM_LIMBS` instead of hard-coded 4.
4. Fixed comments (using $L$ instead of $t$)
5. Changed the definition of `get_maximum_unreduced_value()` to a form
$(2^N - 1)$ and use the comparison operators correctly
6. Fixed `static constexpr uint64_t MAX_UNREDUCED_LIMB_BITS =
NUM_LIMB_BITS + MAX_ADDITION_LOG`
7. Got rid of variable `neg_prime`
8. Used `is_constant()` instead of iterating over each limb to check
constant-ness in `operator+` and `operator-`.
9. Removed duplicate/redundant assertion: `ASSERT(input_left.size() ==
input_right.size() && input_left.size() < 1024);`
10. Fixed misc comments

Response: Fixed in
e2024df

#### [V-AZT-VUL-008: Incorrect term used during calculation on bound of
upper limb]()

Corrected the calculation of the resultant maximum bound of the upper
and lower limbs:

$$D_{\textsf{hi}} < 2^{2Q + L + \textcolor{red}{3}},$$
$$D_{\textsf{lo}} < 2^{2Q + L + \textcolor{red}{2}}.$$ 

Response: Fixed in
f41813e

#### [V-AZT-VUL-009: Optimization Improvements]()

1. In the function `add_two`, we could add another `if` condition when
two of the three inputs are constant and reduced by the prime. But the
current implementation should handle that implicitly on calling
`add_two` on each limb. Note that no additional gates would be added
since each `add_two` call on limbs would just update additive constants
on the witness.
2. Agree with the observation but we think its fine to have redundant
reductions in constant case as that would cause negligible impact on
prover performance.
3. It is a good suggestion to use a tighter bound for range constraint
on the quotient when reduction is not necessary. However, while creating
the quotient witness using the constructor:
    ```cpp
    template <typename Builder, typename T>
bigfield<Builder, T> bigfield<Builder,
T>::create_from_u512_as_witness(Builder* ctx,
const uint512_t& value,
const bool can_overflow,
const size_t maximum_bitlength)
    ```
when `can_overflow` is set to `false`, `maximum_bitlength` must be
greater than $3L$. This assertion breaks if we use tighter range
constraint on the quotient. This needs to be investigated further.

Author: suyash67

barretenberg/cpp/scripts/test_civc_standalone_vks_havent_changed.sh

@@ -13,7 +13,7 @@ cd ..
 # - Generate a hash for versioning: sha256sum bb-civc-inputs.tar.gz
 # - Upload the compressed results: aws s3 cp bb-civc-inputs.tar.gz s3://aztec-ci-artifacts/protocol/bb-civc-inputs-[hash(0:8)].tar.gz
 # Note: In case of the "Test suite failed to run ... Unexpected token 'with' " error, need to run: docker pull aztecprotocol/build:3.0
-pinned_short_hash="e70f08be"
+pinned_short_hash="8ba25b76"
 pinned_civc_inputs_url="https://aztec-ci-artifacts.s3.us-east-2.amazonaws.com/protocol/bb-civc-inputs-${pinned_short_hash}.tar.gz"
 
 function compress_and_upload {

barretenberg/cpp/src/barretenberg/stdlib/eccvm_verifier/eccvm_recursive_verifier.test.cpp

@@ -139,7 +139,7 @@ class ECCVMRecursiveTests : public ::testing::Test {
         }
 
         // Check that the size of the recursive verifier is consistent with historical expectation
-        uint32_t NUM_GATES_EXPECTED = 213775;
+        uint32_t NUM_GATES_EXPECTED = 216360;
         ASSERT_EQ(static_cast<uint32_t>(outer_circuit.get_num_finalized_gates()), NUM_GATES_EXPECTED)
             << "Ultra-arithmetized ECCVM Recursive verifier gate count changed! Update this value if you are sure this "
                "is expected.";

barretenberg/cpp/src/barretenberg/stdlib/honk_verifier/ultra_recursive_verifier.test.cpp

@@ -293,7 +293,7 @@ template <typename RecursiveFlavor> class RecursiveVerifierTest : public testing
         }
         // Check the size of the recursive verifier
         if constexpr (std::same_as<RecursiveFlavor, MegaZKRecursiveFlavor_<UltraCircuitBuilder>>) {
-            uint32_t NUM_GATES_EXPECTED = 801953;
+            uint32_t NUM_GATES_EXPECTED = 808803;
             ASSERT_EQ(static_cast<uint32_t>(outer_circuit.get_num_finalized_gates()), NUM_GATES_EXPECTED)
                 << "MegaZKHonk Recursive verifier changed in Ultra gate count! Update this value if you "
                    "are sure this is expected.";

barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/README.md

@@ -413,34 +413,34 @@ $$
 >
 > $$
 > \begin{aligned}
-> \textcolor{orange}{D_{\textsf{lo}}} &= (2^{Q} - 1)^2 + 2 \cdot (2^{Q} - 1)^2 \cdot 2^L \ < \ 2^{2Q + L + 1}, \\
-> \textcolor{orange}{D_{\textsf{hi}}} &= 3 \cdot (2^{Q} - 1)^2 + 4 \cdot (2^{Q} - 1)^2 \cdot 2^L \ < \ 2^{2Q + L + 2}.
+> \textcolor{orange}{D_{\textsf{lo}}} &= (2^{Q} - 1)^2 + 2 \cdot (2^{Q} - 1)^2 \cdot 2^L \ < \ 2^{2Q + L + 2}, \\
+> \textcolor{orange}{D_{\textsf{hi}}} &= 3 \cdot (2^{Q} - 1)^2 + 4 \cdot (2^{Q} - 1)^2 \cdot 2^L \ < \ 2^{2Q + L + 3}.
 > \end{aligned}
 > $$
 >
 > Clearly, maximum value of $\textcolor{orange}{D_{\textsf{hi}}}$ determines the overall maximum of the two outputs of multiplication:
 >
 > $$
-> \textsf{max}(\textcolor{orange}{D_{\textsf{lo}}}, \textcolor{orange}{D_{\textsf{hi}}}) < 2^{2Q + L + 2}.
+> \textsf{max}(\textcolor{orange}{D_{\textsf{lo}}}, \textcolor{orange}{D_{\textsf{hi}}}) < 2^{2Q + L + 3}.
 > $$
 >
 > This is the maximum value of the resulting limbs of a single product $d = a \cdot b$. Suppose we have $2^k$ such products, then the maximum value of the limbs of the sum of these products would be:
 >
 > $$
 > \begin{aligned}
-> \sum_{i=1}^{2^k} \textcolor{orange}{D_{\textsf{hi}, i}} & \ < \ 2^{k + 2Q + L + 2}.
+> \sum_{i=1}^{2^k} \textcolor{orange}{D_{\textsf{hi}, i}} & \ < \ 2^{k + 2Q + L + 3}.
 > \end{aligned}
 > $$
 >
 > We require that this value must not exceed the native field modulus $n$. Hence, we need to ensure that:
 >
 > $$
 > \begin{aligned}
-> 2^{k + 2Q + L + 2} &< n \quad \implies \quad \boxed{Q < \frac{\text{log}_2(n) - L - k - 2}{2}}.
+> 2^{k + 2Q + L + 3} &< n \quad \implies \quad \boxed{Q < \frac{\text{log}_2(n) - L - k - 3}{2}}.
 > \end{aligned}
 > $$
 >
-> This means that the maximum limb size that must be allowed is $Q = \left\lfloor\frac{253.5 - 68 - 10 - 2}{2}\right\rfloor = 86$.
+> This means that the maximum limb size that must be allowed is $Q = \left\lfloor\frac{253.5 - 68 - 10 - 3}{2}\right\rfloor = 86$.
 >
 > .
 

barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/bigfield.hpp

@@ -55,7 +55,7 @@ template <typename Builder, typename T> class bigfield {
         }
         friend std::ostream& operator<<(std::ostream& os, const Limb& a)
         {
-            os << "{ " << a.element << " < " << a.maximum_value << " }";
+            os << "{ " << a.element << " <= " << a.maximum_value << " }";
             return os;
         }
         Limb(const Limb& other) = default;
@@ -326,29 +326,25 @@ template <typename Builder, typename T> class bigfield {
     static constexpr size_t MAXIMUM_SUMMAND_COUNT_LOG = 4;
     static constexpr size_t MAXIMUM_SUMMAND_COUNT = 1 << MAXIMUM_SUMMAND_COUNT_LOG;
 
-    static constexpr uint256_t prime_basis_maximum_limb =
-        modulus_u512.slice(NUM_LIMB_BITS * (NUM_LIMBS - 1), NUM_LIMB_BITS* NUM_LIMBS).lo;
     static constexpr Basis prime_basis{ uint512_t(bb::fr::modulus), bb::fr::modulus.get_msb() + 1 };
     static constexpr Basis binary_basis{ uint512_t(1) << LOG2_BINARY_MODULUS, LOG2_BINARY_MODULUS };
     static constexpr Basis target_basis{ modulus_u512, static_cast<size_t>(modulus_u512.get_msb() + 1) };
     static constexpr bb::fr shift_1 = bb::fr(uint256_t(1) << NUM_LIMB_BITS);
     static constexpr bb::fr shift_2 = bb::fr(uint256_t(1) << (NUM_LIMB_BITS * 2));
     static constexpr bb::fr shift_3 = bb::fr(uint256_t(1) << (NUM_LIMB_BITS * 3));
-    static constexpr bb::fr shift_right_1 = bb::fr(1) / shift_1;
-    static constexpr bb::fr shift_right_2 = bb::fr(1) / shift_2;
-    static constexpr bb::fr negative_prime_modulus_mod_binary_basis = -bb::fr(uint256_t(modulus_u512));
-    static constexpr uint512_t negative_prime_modulus = binary_basis.modulus - target_basis.modulus;
-    static constexpr std::array<uint256_t, NUM_LIMBS> neg_modulus_limbs_u256{
-        negative_prime_modulus.slice(0, NUM_LIMB_BITS).lo,
-        negative_prime_modulus.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo,
-        negative_prime_modulus.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo,
-        negative_prime_modulus.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo,
+    static constexpr bb::fr negative_prime_modulus_mod_native_basis = -bb::fr(uint256_t(target_basis.modulus));
+    static constexpr uint512_t negative_prime_modulus_mod_binary_basis = binary_basis.modulus - target_basis.modulus;
+    static constexpr std::array<uint256_t, NUM_LIMBS> neg_modulus_mod_binary_basis_limbs_u256{
+        negative_prime_modulus_mod_binary_basis.slice(0, NUM_LIMB_BITS).lo,
+        negative_prime_modulus_mod_binary_basis.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo,
+        negative_prime_modulus_mod_binary_basis.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo,
+        negative_prime_modulus_mod_binary_basis.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo,
     };
-    static constexpr std::array<bb::fr, NUM_LIMBS> neg_modulus_limbs{
-        bb::fr(negative_prime_modulus.slice(0, NUM_LIMB_BITS).lo),
-        bb::fr(negative_prime_modulus.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo),
-        bb::fr(negative_prime_modulus.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo),
-        bb::fr(negative_prime_modulus.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo),
+    static constexpr std::array<bb::fr, NUM_LIMBS> neg_modulus_mod_binary_basis_limbs{
+        bb::fr(negative_prime_modulus_mod_binary_basis.slice(0, NUM_LIMB_BITS).lo),
+        bb::fr(negative_prime_modulus_mod_binary_basis.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo),
+        bb::fr(negative_prime_modulus_mod_binary_basis.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo),
+        bb::fr(negative_prime_modulus_mod_binary_basis.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo),
     };
 
     /**
@@ -568,7 +564,7 @@ template <typename Builder, typename T> class bigfield {
                              const std::vector<bigfield>& mul_right,
                              const bigfield& divisor,
                              const std::vector<bigfield>& to_sub,
-                             bool enable_divisor_nz_check = false);
+                             bool enable_divisor_nz_check = true);
 
     static bigfield sum(const std::vector<bigfield>& terms);
     static bigfield internal_div(const std::vector<bigfield>& numerators,
@@ -770,7 +766,7 @@ template <typename Builder, typename T> class bigfield {
         //
         // a * b = q * p + r
         //
-        // where p is the quotient, r is the remainder, and p is the size of the non-native field.
+        // where q is the quotient, r is the remainder, and p is the size of the non-native field.
         // The CRT requires that we check that the equation:
         // (a) holds modulo the size of the native field n,
         // (b) holds modulo the size of the bigger ring 2^t,
@@ -787,7 +783,7 @@ template <typename Builder, typename T> class bigfield {
         // Note: We use a further safer bound of 2^((t + m - 1) / 2). We use -1 to stay safer,
         // because it provides additional space to avoid the overflow, but get_msb() by itself should be enough.
         uint64_t maximum_product_bits = maximum_product.get_msb() - 1;
-        return (uint512_t(1) << (maximum_product_bits >> 1));
+        return (uint512_t(1) << (maximum_product_bits >> 1)) - uint512_t(1);
     }
 
     // If we encounter this maximum value of a bigfield we stop execution
@@ -915,24 +911,27 @@ template <typename Builder, typename T> class bigfield {
     //           = 2^k * (3 * 2^2Q) + 2^k * 2^L * (4 * 2^2Q)
     //           < 2^k * (2^L + 1) * (4 * 2^2Q)
     //           < n
-    // ==> 2^k * 2^L * 2^(2Q + 2) < n
-    // ==> 2Q + 2 < (log(n) - k - L)
-    // ==> Q < ((log(n) - k - L) - 2) / 2
+    // ==> 2^k * 2^L * 2^(2Q + 3) < n
+    // ==> 2Q + 3 < (log(n) - k - L)
+    // ==> Q < ((log(n) - k - L) - 3) / 2
     //
     static constexpr uint64_t MAXIMUM_LIMB_SIZE_THAT_WOULDNT_OVERFLOW =
-        (bb::fr::modulus.get_msb() - MAX_ADDITION_LOG - NUM_LIMB_BITS - 2) / 2;
+        (bb::fr::modulus.get_msb() - MAX_ADDITION_LOG - NUM_LIMB_BITS - 3) / 2;
 
     // If the logarithm of the maximum value of a limb is more than this, we need to reduce.
     // We allow an element to be added to itself 10 times, so we allow the limb to grow by 10 bits.
     // Number 10 is arbitrary, there's no actual usecase for adding 1024 elements together.
-    static constexpr uint64_t MAX_UNREDUCED_LIMB_BITS = NUM_LIMB_BITS + 10;
+    static constexpr uint64_t MAX_UNREDUCED_LIMB_BITS = NUM_LIMB_BITS + MAX_ADDITION_LOG;
 
     // If we reach this size of a limb, we stop execution (as safety measure). This should never reach during addition
     // as we would reduce the limbs before they reach this size.
     static constexpr uint64_t PROHIBITED_LIMB_BITS = MAX_UNREDUCED_LIMB_BITS + 5;
 
     // If we encounter this maximum value of a bigfield we need to reduce it.
-    static constexpr uint256_t get_maximum_unreduced_limb_value() { return uint256_t(1) << MAX_UNREDUCED_LIMB_BITS; }
+    static constexpr uint256_t get_maximum_unreduced_limb_value()
+    {
+        return ((uint256_t(1) << MAX_UNREDUCED_LIMB_BITS) - uint256_t(1));
+    }
 
     // If we encounter this maximum value of a limb we stop execution
     static constexpr uint256_t get_prohibited_limb_value() { return uint256_t(1) << PROHIBITED_LIMB_BITS; }

barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/bigfield_edge_cases.test.cpp

@@ -80,7 +80,7 @@ template <typename BigField> class stdlib_bigfield_edge_cases : public testing::
         uint512_t(fq_ct::modulus),                // p
     };
 
-    inline static const std::array<uint512_t, 9> values_larger_than_bigfield = {
+    inline static const std::array<uint512_t, 10> values_larger_than_bigfield = {
         uint512_t(fq_ct::modulus) + uint512_t(1),
         uint512_t(fq_ct::modulus) + uint512_t(fr::modulus),
         (uint512_t(1) << 256) - 1,
@@ -89,6 +89,7 @@ template <typename BigField> class stdlib_bigfield_edge_cases : public testing::
         uint512_t(fq_ct::get_maximum_unreduced_value()) - 1,
         uint512_t(fq_ct::get_maximum_unreduced_value()),
         uint512_t(fq_ct::get_maximum_unreduced_value()) + 1,
+        uint512_t(fq_ct::get_maximum_unreduced_value()) + 2,
         (uint512_t(1) << (stdlib::NUM_LIMB_BITS_IN_FIELD_SIMULATION * 4)) - 1,
     };
 
@@ -126,16 +127,16 @@ template <typename BigField> class stdlib_bigfield_edge_cases : public testing::
         fq_ct combined_a = fq_ct::unsafe_construct_from_limbs(limb_0, limb_1, limb_2, limb_3, true);
         combined_a.binary_basis_limbs[3].maximum_value = other_mask;
 
-        // Check that individual limbs are less than maximum unreduced limb value
-        const bool limbs_less_than_max = (limb_0_native < fq_ct::get_maximum_unreduced_limb_value()) &&
-                                         (limb_1_native < fq_ct::get_maximum_unreduced_limb_value()) &&
-                                         (limb_2_native < fq_ct::get_maximum_unreduced_limb_value()) &&
-                                         (limb_3_native < fq_ct::get_maximum_unreduced_limb_value());
+        // Check that individual limbs are ≤ than maximum unreduced limb value
+        const bool limbs_less_than_max = (limb_0_native <= fq_ct::get_maximum_unreduced_limb_value()) &&
+                                         (limb_1_native <= fq_ct::get_maximum_unreduced_limb_value()) &&
+                                         (limb_2_native <= fq_ct::get_maximum_unreduced_limb_value()) &&
+                                         (limb_3_native <= fq_ct::get_maximum_unreduced_limb_value());
         EXPECT_EQ(limbs_less_than_max, true);
 
         // Check that the combined max value is greater than the maximum unreduced bigfield value
         EXPECT_GT(combined_a.get_maximum_value(),      // 2^68 * 2^68 * 2^68 * 2^61 = 2^265
-                  fq_ct::get_maximum_unreduced_value() // sqrt(2^272 * |Fr|) ≈ 2^(263) or 2^(264)
+                  fq_ct::get_maximum_unreduced_value() // sqrt(2^272 * |Fr|) ≈ (2^(263) - 1) or (2^(264) - 1)
         );
 
         // Squaring op must perform self-reduction
@@ -144,7 +145,7 @@ template <typename BigField> class stdlib_bigfield_edge_cases : public testing::
 
         // Check that original combined value is now reduced
         EXPECT_EQ(combined_a.get_value() < reduction_upper_bound, true); // reduced value < 2^s
-        EXPECT_EQ(combined_a.get_maximum_value() < fq_ct::get_maximum_unreduced_value(), true);
+        EXPECT_EQ(combined_a.get_maximum_value() <= fq_ct::get_maximum_unreduced_value(), true);
 
         bool result = CircuitChecker::check(builder);
         EXPECT_EQ(result, true);
@@ -176,14 +177,14 @@ template <typename BigField> class stdlib_bigfield_edge_cases : public testing::
             (uint256_t(1) << fq_ct::MAX_UNREDUCED_LIMB_BITS) + 1000; // > 2^78
 
         // Check that the combined max value is less than the maximum unreduced bigfield value
-        EXPECT_EQ(combined_a.get_maximum_value() < fq_ct::get_maximum_unreduced_value(), true);
+        EXPECT_EQ(combined_a.get_maximum_value() <= fq_ct::get_maximum_unreduced_value(), true);
 
         // Perform a squaring which should trigger reduction
         combined_a.sqr();
 
         // Check that the original combined value is now reduced
         EXPECT_EQ(combined_a.get_value() < reduction_upper_bound, true);
-        EXPECT_EQ(combined_a.get_maximum_value() < fq_ct::get_maximum_unreduced_value(), true);
+        EXPECT_EQ(combined_a.get_maximum_value() <= fq_ct::get_maximum_unreduced_value(), true);
 
         // Check the circuit is valid
         bool result = CircuitChecker::check(builder);
@@ -444,6 +445,87 @@ template <typename BigField> class stdlib_bigfield_edge_cases : public testing::
         bool result = CircuitChecker::check(builder);
         EXPECT_EQ(result, true);
     }
+
+    static void test_divide_by_zero_fails()
+    {
+        Builder builder = Builder();
+        {
+            // numerator and denominator both are witnesses
+            auto [a_native, a_ct] = get_random_witness(&builder, false);
+            fq_ct zero = fq_ct::create_from_u512_as_witness(&builder, uint512_t(0), true);
+            fq_ct zero_modulus = fq_ct::create_from_u512_as_witness(&builder, uint512_t(fq_ct::modulus), true);
+
+            // Division by zero should trigger an assertion failure
+            fq_ct output = a_ct / zero;
+            fq_ct output_modulus = a_ct / zero_modulus;
+
+            // outputs are irrelevant
+            EXPECT_EQ(output.get_value(), 0);
+            EXPECT_EQ(output_modulus.get_value(), 0);
+
+            bool result = CircuitChecker::check(builder);
+            EXPECT_EQ(result, false);
+            EXPECT_EQ(builder.err(), "bigfield: prime limb identity failed");
+        }
+        {
+            // numerator is constant, denominator is witness
+            fq_native a_native = fq_native::random_element();
+            fq_ct a_ct(&builder, uint256_t(a_native));
+            fq_ct zero = fq_ct::create_from_u512_as_witness(&builder, uint512_t(0), true);
+
+            // Division by zero should trigger an assertion failure
+            fq_ct output = a_ct / zero;
+
+            // outputs are irrelevant
+            EXPECT_EQ(output.get_value(), 0);
+
+            bool result = CircuitChecker::check(builder);
+            EXPECT_EQ(result, false);
+            EXPECT_EQ(builder.err(), "bigfield: prime limb identity failed");
+        }
+        {
+            // numerator is empty, denominator is witness
+            fq_ct zero = fq_ct::create_from_u512_as_witness(&builder, uint512_t(0), true);
+
+            // Division by zero should trigger an assertion failure
+            fq_ct output = fq_ct::div_check_denominator_nonzero({}, zero);
+
+            // outputs are irrelevant
+            EXPECT_EQ(output.get_value(), 0);
+
+            bool result = CircuitChecker::check(builder);
+            EXPECT_EQ(result, false);
+            EXPECT_EQ(builder.err(), "bigfield: prime limb diff is zero, but expected non-zero");
+        }
+        {
+            // numerator is witness, denominator is constant
+            [[maybe_unused]] auto [a_native, a_ct] = get_random_witness(&builder, false);
+            fq_ct constant_zero = fq_ct(&builder, uint256_t(0));
+
+#ifndef NDEBUG
+            // In debug mode, we should hit an assertion failure
+            EXPECT_THROW_OR_ABORT(a_ct / constant_zero, "bigfield: prime limb diff is zero, but expected non-zero");
+#endif
+        }
+        {
+            // numerator and denominator both are constant
+            fq_native a_native = fq_native::random_element();
+            fq_ct a_ct(&builder, uint256_t(a_native));
+
+#ifndef NDEBUG
+            fq_ct constant_zero = fq_ct(&builder, uint256_t(0));
+            EXPECT_THROW_OR_ABORT(a_ct / constant_zero, "bigfield: division by zero in constant division");
+#endif
+        }
+        {
+            // numerator is empty, denominator is constant
+#ifndef NDEBUG
+            fq_ct constant_zero = fq_ct(&builder, uint256_t(0));
+            EXPECT_THROW_OR_ABORT(fq_ct::div_check_denominator_nonzero({}, constant_zero),
+                                  "bigfield: prime limb diff is zero, but expected non-zero");
+#endif
+        }
+    }
 };
 
 // Define types for which the above tests will be constructed.
@@ -512,3 +594,8 @@ TYPED_TEST(stdlib_bigfield_edge_cases, assert_equal_edge_case)
 {
     TestFixture::test_assert_equal_edge_case();
 }
+
+TYPED_TEST(stdlib_bigfield_edge_cases, divide_by_zero_fails)
+{
+    TestFixture::test_divide_by_zero_fails();
+}