@@ -273,7 +273,7 @@ template <typename Builder, typename T> bigfield<Builder, T>::bigfield(const byt
273273 const auto res = bigfield::unsafe_construct_from_limbs (limb0, limb1, limb2, limb3, true );
274274
275275 const auto num_last_limb_bits = 256 - (NUM_LIMB_BITS * 3 );
276- res.binary_basis_limbs [3 ].maximum_value = (uint64_t (1 ) << num_last_limb_bits);
276+ res.binary_basis_limbs [3 ].maximum_value = (uint64_t (1 ) << num_last_limb_bits) - 1 ;
277277 *this = res;
278278 set_origin_tag (bytes.get_origin_tag ());
279279}
@@ -1992,14 +1992,14 @@ void bigfield<Builder, T>::unsafe_assert_less_than(const uint256_t& upper_limit,
19921992 r2.get_witness_index (),
19931993 r3.get_witness_index (),
19941994 static_cast <size_t >(NUM_LIMB_BITS),
1995- static_cast <size_t >(NUM_LIMB_BITS ),
1995+ static_cast <size_t >(NUM_LAST_LIMB_BITS ),
19961996 msg == " bigfield::unsafe_assert_less_than" ? " bigfield::unsafe_assert_less_than: r2 or r3 too large" : msg);
19971997}
19981998
19991999// check elements are equal mod p by proving their integer difference is a multiple of p.
20002000// This relies on the minus operator for a-b increasing a by a multiple of p large enough so diff is non-negative
20012001// When one of the elements is a constant and another is a witness we check equality of limbs, so if the witness
2002- // bigfield element is in an unreduced form, it needs to be reduced first. We don't have automatice reduced form
2002+ // bigfield element is in an unreduced form, it needs to be reduced first. We don't have automatic reduced form
20032003// detection for now, so it is up to the circuit writer to detect this
20042004template <typename Builder, typename T>
20052005void bigfield<Builder, T>::assert_equal(const bigfield& other, std::string const & msg) const
@@ -2010,13 +2010,16 @@ void bigfield<Builder, T>::assert_equal(const bigfield& other, std::string const
20102010 BB_ASSERT_EQ (get_value (), other.get_value (), " We expect constants to be less than the target modulus" );
20112011 return ;
20122012 } else if (other.is_constant ()) {
2013- // NOTE(https://github.com/AztecProtocol/barretenberg/issues/998): This can lead to a situation where
2014- // an honest prover cannot satisfy the constraints, because `this` is not reduced, but `other` is, i.e.,
2015- // `this` = kp + r and `other` = r
2016- // where k is a positive integer. In such a case, the prover cannot satisfy the constraints
2017- // because the limb-differences would not be 0 mod r. Therefore, an honest prover needs to make sure that
2018- // `this` is reduced before calling this method. Also `other` should never be greater than the modulus by
2019- // design. As a precaution, we assert that the circuit-constant `other` is less than the modulus.
2013+ // NOTE(https://github.com/AztecProtocol/barretenberg/issues/998): This does a limb-wise integer
2014+ // comparison, so `this` must already be in reduced form (value in [0, p)) before calling this method.
2015+ // If `this = kp + r` and `other = r`, the limbs differ and an honest prover cannot satisfy the
2016+ // constraints. Callers are responsible for calling self_reduce() first when necessary; we omit it
2017+ // here to avoid adding spurious gates in the common case where `this` is already reduced.
2018+ // `other` should never exceed the modulus by design; we assert this as a precaution.
2019+ BB_ASSERT_LT (get_value (),
2020+ modulus_u512,
2021+ " bigfield::assert_equal: 'this' is not reduced (value >= p). Call self_reduce() before comparing "
2022+ " against a constant." );
20202023 BB_ASSERT_LT (other.get_value (), modulus_u512);
20212024 field_t <Builder> t0 = (binary_basis_limbs[0 ].element - other.binary_basis_limbs [0 ].element );
20222025 field_t <Builder> t1 = (binary_basis_limbs[1 ].element - other.binary_basis_limbs [1 ].element );
@@ -2072,8 +2075,10 @@ void bigfield<Builder, T>::assert_equal(const bigfield& other, std::string const
20722075
20732076// construct a proof that points are different mod p, when they are different mod r
20742077// WARNING: This method doesn't have perfect completeness - for points equal mod r (or with certain difference kp
2075- // mod r) but different mod p, you can't construct a proof. The chances of an honest prover running afoul of this
2076- // condition are extremely small (TODO: compute probability) Note also that the number of constraints depends on how
2078+ // mod r) but different mod p, you can't construct a proof. The failure probability is at most
2079+ // (L + R + 1) / r where L = floor(a.max / p), R = floor(b.max / p), r = native field size (~2^254).
2080+ // With max bounded by 2^256 - 1 and p >= 2^249, we get L,R <= 127, so probability < 2^{-246}.
2081+ // Note also that the number of constraints depends on how
20772082// much the values have overflown beyond p e.g. due to an addition chain The function is based on the following.
20782083// Suppose a-b = 0 mod p. Then a-b = k*p for k in a range [-R,L] for largest L and R such that L*p>= a, R*p>=b.
20792084// And also a-b = k*p mod r for such k. Thus we can verify a-b is non-zero mod p by taking the product of such values
@@ -2147,7 +2152,7 @@ template <typename Builder, typename T> void bigfield<Builder, T>::self_reduce()
21472152
21482153 BB_ASSERT_LT ((uint1024_t (1 ) << maximum_quotient_bits) * uint1024_t (modulus_u512) + DEFAULT_MAXIMUM_REMAINDER,
21492154 get_maximum_crt_product ());
2150- quotient.binary_basis_limbs [0 ] = Limb (quotient_limb, uint256_t (1 ) << maximum_quotient_bits);
2155+ quotient.binary_basis_limbs [0 ] = Limb (quotient_limb, ( uint256_t (1 ) << maximum_quotient_bits) - 1 );
21512156 quotient.binary_basis_limbs [1 ] = Limb (field_t <Builder>::from_witness_index (context, context->zero_idx ()), 0 );
21522157 quotient.binary_basis_limbs [2 ] = Limb (field_t <Builder>::from_witness_index (context, context->zero_idx ()), 0 );
21532158 quotient.binary_basis_limbs [3 ] = Limb (field_t <Builder>::from_witness_index (context, context->zero_idx ()), 0 );
0 commit comments