Barretenberg
The ZK-SNARK library at the core of Aztec
|
#include <bigfield.hpp>
Classes | |
struct | Basis |
struct | Limb |
Represents a single limb of a bigfield element, with its value and maximum value. More... | |
Public Types | |
using | View = bigfield |
using | CoefficientAccumulator = bigfield |
using | TParams = T |
using | native = bb::field< T > |
using | field_ct = field_t< Builder > |
Public Member Functions | |
bigfield (const field_t< Builder > &low_bits, const field_t< Builder > &high_bits, const bool can_overflow=false, const size_t maximum_bitlength=0) | |
Constructs a new bigfield object from two field elements representing the low and high bits. | |
bigfield (Builder *parent_context=nullptr) | |
Constructs a zero bigfield object: all limbs are set to zero. | |
bigfield (Builder *parent_context, const uint256_t &value) | |
Constructs a new bigfield object from a uint256_t value. | |
bigfield (const uint256_t &value) | |
bigfield (const int value) | |
Constructs a new bigfield object from an int value. We first need to to construct a field element from the value to avoid bugs that have to do with the value being negative. | |
bigfield (const unsigned long value) | |
bigfield (const unsigned long long value) | |
bigfield (const native value) | |
Construct a new bigfield object from bb::fq. We first convert to uint256_t as field elements are in Montgomery form internally. | |
bigfield (const byte_array< Builder > &bytes) | |
Constructs a bigfield element from a 256-bit byte array. | |
bigfield (const bigfield &other) | |
bigfield (bigfield &&other) noexcept | |
~bigfield ()=default | |
bigfield & | operator= (const bigfield &other) |
bigfield & | operator= (bigfield &&other) noexcept |
byte_array< Builder > | to_byte_array () const |
Convert the bigfield element to a byte array. Concatenates byte arrays of the high (2L bits) and low (2L bits) parts of the bigfield element. | |
uint512_t | get_value () const |
uint512_t | get_maximum_value () const |
bigfield | add_to_lower_limb (const field_t< Builder > &other, const uint256_t &other_maximum_value) const |
Add a field element to the lower limb. CAUTION (the element has to be constrained before using this function) | |
bigfield | operator+ (const bigfield &other) const |
Adds two bigfield elements. Inputs are reduced to the modulus if necessary. Requires 4 gates if both elements are witnesses. | |
bigfield | add_two (const bigfield &add_a, const bigfield &add_b) const |
Create constraints for summing three bigfield elements efficiently. | |
bigfield | operator- (const bigfield &other) const |
Subtraction operator. | |
bigfield | operator* (const bigfield &other) const |
Evaluate a non-native field multiplication: (a * b = c mod p) where p == target_basis.modulus. | |
bigfield | operator/ (const bigfield &other) const |
bigfield | operator- () const |
Negation operator, works by subtracting this from zero. | |
bigfield | operator+= (const bigfield &other) |
bigfield | operator-= (const bigfield &other) |
bigfield | operator*= (const bigfield &other) |
bigfield | operator/= (const bigfield &other) |
bigfield | sqr () const |
Square operator, computes a * a = c mod p. | |
bigfield | sqradd (const std::vector< bigfield > &to_add) const |
Square and add operator, computes a * a + ...to_add = c mod p. | |
bigfield | pow (const uint32_t exponent) const |
Raise the bigfield element to the power of (out-of-circuit) exponent. | |
bigfield | madd (const bigfield &to_mul, const std::vector< bigfield > &to_add) const |
Compute a * b + ...to_add = c mod p. | |
bigfield | div_without_denominator_check (const bigfield &denominator) |
bigfield | conditional_negate (const bool_t< Builder > &predicate) const |
bigfield | conditional_select (const bigfield &other, const bool_t< Builder > &predicate) const |
Create an element which is equal to either this or other based on the predicate. | |
bool_t< Builder > | operator== (const bigfield &other) const |
Validate whether two bigfield elements are equal to each other. | |
void | assert_is_in_field () const |
void | assert_less_than (const uint256_t &upper_limit) const |
void | assert_equal (const bigfield &other) const |
void | assert_is_not_equal (const bigfield &other) const |
void | self_reduce () const |
bool | is_constant () const |
Check if the bigfield is constant, i.e. its prime limb is constant. | |
bigfield | invert () const |
Inverting function with the assumption that the bigfield element we are calling invert on is not zero. | |
void | convert_constant_to_fixed_witness (Builder *builder) |
void | fix_witness () |
Builder * | get_context () const |
void | set_origin_tag (const bb::OriginTag &tag) const |
bb::OriginTag | get_origin_tag () const |
void | set_free_witness_tag () |
Set the free witness flag for the bigfield. | |
void | unset_free_witness_tag () |
Unset the free witness flag for the bigfield. | |
uint32_t | set_public () const |
Set the witness indices of the binary basis limbs to public. | |
Static Public Member Functions | |
static bigfield | unsafe_construct_from_limbs (const field_t< Builder > &a, const field_t< Builder > &b, const field_t< Builder > &c, const field_t< Builder > &d, const bool can_overflow=false) |
Construct a bigfield element from binary limbs that are already reduced. | |
static bigfield | construct_from_limbs (const field_t< Builder > &a, const field_t< Builder > &b, const field_t< Builder > &c, const field_t< Builder > &d, const bool can_overflow=false) |
Construct a bigfield element from binary limbs that are already reduced and ensure they are range constrained. | |
static bigfield | unsafe_construct_from_limbs (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) |
Construct a bigfield element from binary limbs and a prime basis limb that are already reduced. | |
static bigfield | create_from_u512_as_witness (Builder *ctx, const uint512_t &value, const bool can_overflow=false, const size_t maximum_bitlength=0) |
Creates a bigfield element from a uint512_t. Bigfield element is constructed as a witness and not a circuit constant. | |
static bigfield | from_witness (Builder *ctx, const bb::field< T > &input) |
static void | perform_reductions_for_mult_madd (std::vector< bigfield > &mul_left, std::vector< bigfield > &mul_right, const std::vector< bigfield > &to_add) |
Performs individual reductions on the supplied elements as well as more complex reductions to prevent CRT modulus overflow and to fit the quotient inside the range proof. | |
static bigfield | mult_madd (const std::vector< bigfield > &mul_left, const std::vector< bigfield > &mul_right, const std::vector< bigfield > &to_add, bool fix_remainder_to_zero=false) |
static bigfield | dual_madd (const bigfield &left_a, const bigfield &right_a, const bigfield &left_b, const bigfield &right_b, const std::vector< bigfield > &to_add) |
static bigfield | msub_div (const std::vector< bigfield > &mul_left, const std::vector< bigfield > &mul_right, const bigfield &divisor, const std::vector< bigfield > &to_sub, bool enable_divisor_nz_check=false) |
static bigfield | sum (const std::vector< bigfield > &terms) |
Create constraints for summing these terms. | |
static bigfield | internal_div (const std::vector< bigfield > &numerators, const bigfield &denominator, bool check_for_zero) |
static bigfield | div_without_denominator_check (const std::vector< bigfield > &numerators, const bigfield &denominator) |
static bigfield | div_check_denominator_nonzero (const std::vector< bigfield > &numerators, const bigfield &denominator) |
static bigfield | conditional_assign (const bool_t< Builder > &predicate, const bigfield &lhs, const bigfield &rhs) |
static bigfield | one () |
static bigfield | zero () |
static constexpr bigfield | unreduced_zero () |
Create an unreduced 0 ~ p*k, where p*k is the minimal multiple of modulus that should be reduced. | |
static bigfield | reconstruct_from_public (const std::span< const field_ct, PUBLIC_INPUTS_SIZE > &limbs) |
Reconstruct a bigfield from limbs (generally stored in the public inputs) | |
static constexpr uint512_t | get_maximum_unreduced_value () |
static constexpr uint512_t | get_prohibited_value () |
static constexpr uint1024_t | get_maximum_crt_product () |
Compute the maximum product of two bigfield elements in CRT: M = 2^t * n. | |
static size_t | get_quotient_max_bits (const std::vector< uint1024_t > &remainders_max) |
Compute the maximum number of bits for quotient range proof to protect against CRT underflow. | |
static bool | mul_product_overflows_crt_modulus (const uint1024_t &a_max, const uint1024_t &b_max, const std::vector< bigfield > &to_add) |
static bool | mul_product_overflows_crt_modulus (const std::vector< uint512_t > &as_max, const std::vector< uint512_t > &bs_max, const std::vector< bigfield > &to_add) |
static constexpr uint256_t | get_maximum_unreduced_limb_value () |
static constexpr uint256_t | get_prohibited_limb_value () |
Public Attributes | |
Builder * | context |
std::array< Limb, NUM_LIMBS > | binary_basis_limbs |
Represents a bigfield element in the binary basis. A bigfield element is represented as a combination of 4 binary basis limbs: a = a[0] + a[1] * 2^L + a[2] * 2^2L + a[3] * 2^3L. | |
field_t< Builder > | prime_basis_limb |
Represents a bigfield element in the prime basis: (a mod n) where n is the native modulus. | |
Static Public Attributes | |
static constexpr size_t | PUBLIC_INPUTS_SIZE = BIGFIELD_PUBLIC_INPUTS_SIZE |
static constexpr size_t | NUM_LIMBS = 4 |
static constexpr uint256_t | modulus = (uint256_t(T::modulus_0, T::modulus_1, T::modulus_2, T::modulus_3)) |
static constexpr uint512_t | modulus_u512 = static_cast<uint512_t>(modulus) |
static constexpr uint64_t | NUM_LIMB_BITS = NUM_LIMB_BITS_IN_FIELD_SIMULATION |
static constexpr uint64_t | NUM_LAST_LIMB_BITS = modulus_u512.get_msb() + 1 - (NUM_LIMB_BITS * 3) |
static const uint1024_t | DEFAULT_MAXIMUM_REMAINDER |
static constexpr uint256_t | DEFAULT_MAXIMUM_LIMB = (uint256_t(1) << NUM_LIMB_BITS) - uint256_t(1) |
static constexpr uint256_t | DEFAULT_MAXIMUM_MOST_SIGNIFICANT_LIMB |
static constexpr uint64_t | LOG2_BINARY_MODULUS = NUM_LIMB_BITS * NUM_LIMBS |
static constexpr bool | is_composite = true |
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 |
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 |
static constexpr std::array< bb::fr, NUM_LIMBS > | neg_modulus_limbs |
static constexpr uint64_t | MAX_ADDITION_LOG = 10 |
static constexpr uint64_t | MAXIMUM_LIMB_SIZE_THAT_WOULDNT_OVERFLOW |
static constexpr uint64_t | MAX_UNREDUCED_LIMB_BITS = NUM_LIMB_BITS + 10 |
static constexpr uint64_t | PROHIBITED_LIMB_BITS = MAX_UNREDUCED_LIMB_BITS + 5 |
Private Member Functions | |
std::array< uint32_t, NUM_LIMBS > | get_binary_basis_limb_witness_indices () const |
Get the witness indices of the (normalized) binary basis limbs. | |
void | reduction_check () const |
Check if the bigfield element needs to be reduced. | |
void | sanity_check () const |
Perform a sanity check on a value that is about to interact with another value. | |
std::array< uint256_t, NUM_LIMBS > | get_binary_basis_limb_maximums () |
Get the maximum values of the binary basis limbs. | |
Static Private Member Functions | |
static std::pair< uint512_t, uint512_t > | compute_quotient_remainder_values (const bigfield &a, const bigfield &b, const std::vector< bigfield > &to_add) |
Compute the quotient and remainder values for dividing (a * b + (to_add[0] + ... + to_add[-1])) with p. | |
static uint512_t | compute_maximum_quotient_value (const std::vector< uint512_t > &as, const std::vector< uint512_t > &bs, const std::vector< uint512_t > &to_add) |
Compute the maximum possible value of quotient of a*b+\sum(to_add) | |
static std::pair< bool, size_t > | get_quotient_reduction_info (const std::vector< uint512_t > &as_max, const std::vector< uint512_t > &bs_max, const std::vector< bigfield > &to_add, const std::vector< uint1024_t > &remainders_max={ DEFAULT_MAXIMUM_REMAINDER }) |
Check for 2 conditions (CRT modulus is overflown or the maximum quotient doesn't fit into range proof). Also returns the length of quotient's range proof if there is no need to reduce. | |
static void | 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) |
Evaluate a multiply add identity with several added elements and several remainders. | |
static void | unsafe_evaluate_multiple_multiply_add (const std::vector< bigfield > &input_left, const std::vector< bigfield > &input_right, const std::vector< bigfield > &to_add, const bigfield &input_quotient, const std::vector< bigfield > &input_remainders) |
Evaluate a relation involving multiple multiplications and additions. | |
static void | unsafe_evaluate_square_add (const bigfield &left, const std::vector< bigfield > &to_add, const bigfield "ient, const bigfield &remainder) |
Evaluate a square with several additions. | |
static std::pair< uint512_t, uint512_t > | compute_partial_schoolbook_multiplication (const std::array< uint256_t, NUM_LIMBS > &a_limbs, const std::array< uint256_t, NUM_LIMBS > &b_limbs) |
Compute the partial multiplication of two uint256_t arrays using schoolbook multiplication. | |
Definition at line 21 of file bigfield.hpp.
using bb::stdlib::bigfield< Builder, T >::CoefficientAccumulator = bigfield |
Definition at line 25 of file bigfield.hpp.
using bb::stdlib::bigfield< Builder, T >::field_ct = field_t<Builder> |
Definition at line 28 of file bigfield.hpp.
using bb::stdlib::bigfield< Builder, T >::native = bb::field<T> |
Definition at line 27 of file bigfield.hpp.
using bb::stdlib::bigfield< Builder, T >::TParams = T |
Definition at line 26 of file bigfield.hpp.
using bb::stdlib::bigfield< Builder, T >::View = bigfield |
Definition at line 24 of file bigfield.hpp.
bb::stdlib::bigfield< Builder, T >::bigfield | ( | const field_t< Builder > & | low_bits, |
const field_t< Builder > & | high_bits, | ||
const bool | can_overflow = false , |
||
const size_t | maximum_bitlength = 0 |
||
) |
Constructs a new bigfield object from two field elements representing the low and high bits.
low_bits | The field element representing the low 2L bits of the bigfield. |
high_bits | The field element representing the high 2L bits of the bigfield. |
can_overflow | Whether the bigfield can overflow the modulus. |
maximum_bitlength | The maximum bitlength of the bigfield. If 0, it defaults to |p| (target modulus bitlength). |
Definition at line 44 of file bigfield_impl.hpp.
bb::stdlib::bigfield< Builder, T >::bigfield | ( | Builder * | parent_context = nullptr | ) |
Constructs a zero bigfield object: all limbs are set to zero.
This constructor is used to create a bigfield element without any context. It is useful for creating bigfield elements that will be later assigned to a context.
Definition at line 25 of file bigfield_impl.hpp.
bb::stdlib::bigfield< Builder, T >::bigfield | ( | Builder * | parent_context, |
const uint256_t & | value | ||
) |
Constructs a new bigfield object from a uint256_t value.
parent_context | The circuit context in which the bigfield element will be created. |
value | The uint256_t value to be converted to a bigfield element. |
Definition at line 32 of file bigfield_impl.hpp.
|
inlineexplicit |
Definition at line 117 of file bigfield.hpp.
|
inline |
Constructs a new bigfield object from an int value. We first need to to construct a field element from the value to avoid bugs that have to do with the value being negative.
Definition at line 126 of file bigfield.hpp.
|
inline |
Definition at line 131 of file bigfield.hpp.
|
inline |
Definition at line 136 of file bigfield.hpp.
|
inline |
Construct a new bigfield object from bb::fq. We first convert to uint256_t as field elements are in Montgomery form internally.
value |
Definition at line 146 of file bigfield.hpp.
bb::stdlib::bigfield< Builder, T >::bigfield | ( | const byte_array< Builder > & | bytes | ) |
Constructs a bigfield element from a 256-bit byte array.
This constructor interprets the input byte array as a 256-bit little-endian integer, and decomposes it into 4 limbs as follows:
bytes | The 32-byte input representing the 256-bit integer (little-endian). |
Definition at line 210 of file bigfield_impl.hpp.
bb::stdlib::bigfield< Builder, T >::bigfield | ( | const bigfield< Builder, T > & | other | ) |
Definition at line 117 of file bigfield_impl.hpp.
|
noexcept |
Definition at line 127 of file bigfield_impl.hpp.
|
default |
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::add_to_lower_limb | ( | const field_t< Builder > & | other, |
const uint256_t & | other_maximum_value | ||
) | const |
Add a field element to the lower limb. CAUTION (the element has to be constrained before using this function)
Sometimes we need to add a small constrained value to a bigfield element (for example, a boolean value), but we don't want to construct a full bigfield element for that as it would take too many gates. If the maximum value of the field element being added is small enough, we can simply add it to the lowest limb and increase its maximum value. That will create 2 additional constraints instead of 5/3 needed to add 2 bigfield elements and several needed to construct a bigfield element.
Builder | Builder |
T | Field Parameters |
other | Field element that will be added to the lower |
other_maximum_value | The maximum value of other |
Definition at line 315 of file bigfield_impl.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::add_two | ( | const bigfield< Builder, T > & | add_a, |
const bigfield< Builder, T > & | add_b | ||
) | const |
Create constraints for summing three bigfield elements efficiently.
Builder | |
T |
add_a | |
add_b |
Uses five gates (one for each limb) to add three bigfield elements.
Definition at line 459 of file bigfield_impl.hpp.
void bb::stdlib::bigfield< Builder, T >::assert_equal | ( | const bigfield< Builder, T > & | other | ) | const |
Definition at line 1888 of file bigfield_impl.hpp.
void bb::stdlib::bigfield< Builder, T >::assert_is_in_field | ( | ) | const |
Definition at line 1819 of file bigfield_impl.hpp.
void bb::stdlib::bigfield< Builder, T >::assert_is_not_equal | ( | const bigfield< Builder, T > & | other | ) | const |
Definition at line 1948 of file bigfield_impl.hpp.
void bb::stdlib::bigfield< Builder, T >::assert_less_than | ( | const uint256_t & | upper_limit | ) | const |
Definition at line 1824 of file bigfield_impl.hpp.
|
staticprivate |
Compute the maximum possible value of quotient of a*b+\sum(to_add)
as | Multiplicands |
bs | Multipliers |
to_add | Added elements |
Definition at line 2590 of file bigfield_impl.hpp.
|
staticprivate |
Compute the partial multiplication of two uint256_t arrays using schoolbook multiplication.
a_limbs | |
b_limbs |
Regular schoolbook multiplication of two arrays each with L = 4 limbs will produce a result of size 2 * L - 1 = 7. In this context, we can ignore the last three limbs as those terms have multiplicands: (2^4L, 2^5L, 2^6L) and since we are working modulo 2^t = 2^4L, those terms will always be zero. This is why we call this helper function "partial schoolbook multiplication".
Definition at line 2644 of file bigfield_impl.hpp.
|
staticprivate |
Compute the quotient and remainder values for dividing (a * b + (to_add[0] + ... + to_add[-1])) with p.
a | Left multiplicand |
b | Right multiplier |
to_add | Vector of elements to add |
Definition at line 2568 of file bigfield_impl.hpp.
|
inlinestatic |
Definition at line 594 of file bigfield.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::conditional_negate | ( | const bool_t< Builder > & | predicate | ) | const |
Definition at line 1594 of file bigfield_impl.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::conditional_select | ( | const bigfield< Builder, T > & | other, |
const bool_t< Builder > & | predicate | ||
) | const |
Create an element which is equal to either this or other based on the predicate.
Builder | |
T |
other | The other bigfield element |
predicate | Predicate controlling the result (0 for this, 1 for the other) |
Definition at line 1624 of file bigfield_impl.hpp.
|
inlinestatic |
Construct a bigfield element from binary limbs that are already reduced and ensure they are range constrained.
Definition at line 185 of file bigfield.hpp.
|
inline |
Create a witness form a constant. This way the value of the witness is fixed and public.
Definition at line 677 of file bigfield.hpp.
|
static |
Creates a bigfield element from a uint512_t. Bigfield element is constructed as a witness and not a circuit constant.
ctx | |
value | |
can_overflow | Can the input value have more than log2(modulus) bits? |
maximum_bitlength | Provide the explicit maximum bitlength if known. Otherwise bigfield max value will be either log2(modulus) bits iff can_overflow = false, or (4 * NUM_LIMB_BITS) iff can_overflow = true |
This method is 1 gate more efficient than constructing from 2 field_ct elements.
Definition at line 137 of file bigfield_impl.hpp.
|
static |
Div method with constraints for denominator!=0.
Similar to operator/ but numerator can be linear sum of multiple elements
Definition at line 897 of file bigfield_impl.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::div_without_denominator_check | ( | const bigfield< Builder, T > & | denominator | ) |
Definition at line 886 of file bigfield_impl.hpp.
|
static |
Div method without constraining denominator!=0.
Similar to operator/ but numerator can be linear sum of multiple elements
Definition at line 879 of file bigfield_impl.hpp.
|
static |
Compute (left_a * right_a) + (left_b * right_b) + ...to_add = c mod p
This is cheaper than two multiplication operations, as the above only requires one quotient/remainder
Definition at line 1453 of file bigfield_impl.hpp.
|
inline |
Fix a witness. The value of the witness is constrained with a selector
Definition at line 689 of file bigfield.hpp.
|
inlinestatic |
Definition at line 294 of file bigfield.hpp.
|
inlineprivate |
Get the maximum values of the binary basis limbs.
Definition at line 1100 of file bigfield.hpp.
|
inlineprivate |
Get the witness indices of the (normalized) binary basis limbs.
Definition at line 948 of file bigfield.hpp.
|
inline |
Definition at line 701 of file bigfield.hpp.
|
inlinestaticconstexpr |
Compute the maximum product of two bigfield elements in CRT: M = 2^t * n.
When we multiply two bigfield elements a and b, we need to check that: a * b = q * p + r, where q is the quotient, r is the remainder, and p is the size of the non-native field. With the CRT, we should have both sizes less than the maximum product M = 2^t * n.
Definition at line 811 of file bigfield.hpp.
|
inlinestaticconstexpr |
Definition at line 935 of file bigfield.hpp.
|
inlinestaticconstexpr |
Definition at line 764 of file bigfield.hpp.
uint512_t bb::stdlib::bigfield< Builder, T >::get_maximum_value | ( | ) | const |
Definition at line 305 of file bigfield_impl.hpp.
|
inline |
Definition at line 711 of file bigfield.hpp.
|
inlinestaticconstexpr |
Definition at line 938 of file bigfield.hpp.
|
inlinestaticconstexpr |
Definition at line 794 of file bigfield.hpp.
|
inlinestatic |
Compute the maximum number of bits for quotient range proof to protect against CRT underflow.
When multiplying a and b, we need to check that: a * b = q * p + r, and each side of the equation is less than the maximum product M = 2^t * n. The quotient q is a size of the non-native field, and we need to ensure it fits within the available bits. q * p + r < M ==> q < (M - r_max) / p
remainders_max | Maximum sizes of resulting remainders |
Definition at line 827 of file bigfield.hpp.
|
staticprivate |
Check for 2 conditions (CRT modulus is overflown or the maximum quotient doesn't fit into range proof). Also returns the length of quotient's range proof if there is no need to reduce.
as_max | Vector of left multiplicands' maximum values |
bs_max | Vector of right multiplicands' maximum values |
to_add | Vector of added bigfield values |
Definition at line 2613 of file bigfield_impl.hpp.
uint512_t bb::stdlib::bigfield< Builder, T >::get_value | ( | ) | const |
Definition at line 296 of file bigfield_impl.hpp.
|
static |
Division of a sum with an optional check if divisor is zero. Should not be used outside of class.
numerators | Vector of numerators |
denominator | Denominator |
check_for_zero | If the zero check should be enabled |
Definition at line 794 of file bigfield_impl.hpp.
|
inline |
Inverting function with the assumption that the bigfield element we are calling invert on is not zero.
Definition at line 634 of file bigfield.hpp.
|
inline |
Check if the bigfield is constant, i.e. its prime limb is constant.
We use assertions to ensure that all limbs are consistent in their constant status.
Definition at line 615 of file bigfield.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::madd | ( | const bigfield< Builder, T > & | to_mul, |
const std::vector< bigfield< Builder, T > > & | to_add | ||
) | const |
Compute a * b + ...to_add = c mod p.
to_mul | Bigfield element to multiply by |
to_add | Vector of elements to add |
Definition at line 1058 of file bigfield_impl.hpp.
|
static |
multiply, subtract, divide. This method computes:
result = -(\sum{mul_left[i] * mul_right[i]} + ...to_add) / divisor
Algorithm is constructed in this way to ensure that all computed terms are positive
i.e. we evaluate: result * divisor + (\sum{mul_left[i] * mul_right[i]) + ...to_add) = 0
It is critical that ALL the terms on the LHS are positive to eliminate the possiblity of underflows when calling evaluate_multiple_multiply_add
only requires one quotient and remainder + overflow limbs
We proxy this to mult_madd, so it only requires one quotient and remainder + overflow limbs
Definition at line 1490 of file bigfield_impl.hpp.
|
inlinestatic |
Check that the maximum value of a sum of bigfield productc with added values overflows ctf modulus.
as_max | Vector of multiplicands' maximum values |
b_max | Vector of multipliers' maximum values |
to_add | Vector of field elements to be added |
Definition at line 873 of file bigfield.hpp.
|
inlinestatic |
Check that the maximum value of a bigfield product with added values overflows crt modulus.
a_max | multiplicand maximum value |
b_max | multiplier maximum value |
to_add | vector of field elements to be added |
Definition at line 847 of file bigfield.hpp.
|
static |
Evaluate the sum of products and additional values safely.
mul_left | Vector of bigfield multiplicands |
mul_right | Vector of bigfield multipliers |
to_add | Vector of bigfield elements to add to the sum of products |
Definition at line 1264 of file bigfield_impl.hpp.
|
inlinestatic |
Create a public one constant
Definition at line 639 of file bigfield.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::operator* | ( | const bigfield< Builder, T > & | other | ) | const |
Evaluate a non-native field multiplication: (a * b = c mod p) where p == target_basis.modulus.
other |
We compute quotient term q
and remainder c
and evaluate that: a * b - q * p - c = 0 mod modulus_u512 (binary basis modulus, currently 2**272) a * b - q * p - c = 0 mod circuit modulus We also check that: a * b < M and q * p - c < M, where M = (2^t * n) is CRT modulus.
Definition at line 708 of file bigfield_impl.hpp.
|
inline |
Definition at line 495 of file bigfield.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::operator+ | ( | const bigfield< Builder, T > & | other | ) | const |
Adds two bigfield elements. Inputs are reduced to the modulus if necessary. Requires 4 gates if both elements are witnesses.
Naive addition of two bigfield elements would require 5 gates: 4 gates to add the binary basis limbs and 1 gate to add the prime basis limbs. However, if both elements are witnesses, we can use an optimized addition trick that uses 4 gates instead of 5. In this case, we add the prime basis limbs and one of the binary basis limbs in a single gate.
Builder | |
T |
other |
Definition at line 355 of file bigfield_impl.hpp.
|
inline |
Definition at line 485 of file bigfield.hpp.
|
inline |
Negation operator, works by subtracting this
from zero.
Definition at line 483 of file bigfield.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::operator- | ( | const bigfield< Builder, T > & | other | ) | const |
Subtraction operator.
other |
Uses lazy reduction techniques (similar to operator+) to save on field reductions. Instead of computing *this - other
, we compute a constant X = s * p
and compute: *this + X - other
to ensure we do not underflow. Note that NOT enough to ensure that the integer value of *this + X - other
does not underflow. We must ALSO ensure that each LIMB of the result does not underflow. Based on this condition, we compute the minimum value of s
such that, for each limb i
, the following result is positive: *this.limb[i] + X.limb[i] - other.limb[i] ≥ 0
.
Plookup bigfield subtractoin
We have a special addition gate we can toggle, that will compute: (w_1 + w_4 - w_4_omega + q_arith = 0) This is in addition to the regular addition gate
We can arrange our wires in memory like this:
| 1 | 2 | 3 | 4 | |--—|--—|--—|--—| | b.p | a.0 | b.0 | c.p | (b.p + c.p - a.p = 0) AND (a.0 - b.0 - c.0 = 0) | a.p | a.1 | b.1 | c.0 | (a.1 - b.1 - c.1 = 0) | a.2 | b.2 | c.2 | c.1 | (a.2 - b.2 - c.2 = 0) | a.3 | b.3 | c.3 | — | (a.3 - b.3 - c.3 = 0)
Step 1: For each limb compute the MAXIMUM value we will have to borrow from the next significant limb
i.e. if we assume that *this = 0
and other = other.maximum_value
, how many bits do we need to borrow from the next significant limb to ensure each limb value is positive?
N.B. for this segment maximum_value
really refers to maximum NEGATIVE value of the result
Step 2: Compute the constant value X = m * p
we must add to the result to ensure EVERY limb is >= 0
We need to find a value X
where X.limb[3] > limb_3_maximum_value
. As long as the above holds, we can borrow bits from X.limb[3] to ensure less significant limbs are positive
Start by setting constant_to_add = p
Step 3: Compute offset terms t0, t1, t2, t3 that we add to our result to ensure each limb is positive
t3 represents the value we are BORROWING from constant_to_add.limb[3] t2, t1, t0 are the terms we will ADD to constant_to_add.limb[2], constant_to_add.limb[1], constant_to_add.limb[0]
Borrow propagation table: ┌───────┬─────────────────────────────────┬──────────────────────────────────┐ │ Limb │ Value received FROM next limb │ Value given TO previous limb │ ├───────┼─────────────────────────────────┼──────────────────────────────────┤ │ 0 │ 2^limb_0_borrow_shift │ 0 │ │ 1 │ 2^limb_1_borrow_shift │ 2^(limb_0_borrow_shift - L) │ │ 2 │ 2^limb_2_borrow_shift │ 2^(limb_1_borrow_shift - L) │ │ 3 │ 0 │ 2^(limb_2_borrow_shift - L) │ └───────┴─────────────────────────────────┴──────────────────────────────────┘
i.e. The net value we add to constant_to_add
is 0. We must ensure that: t3 = t0 + (t1 << NUM_LIMB_BITS) + (t2 << NUM_LIMB_BITS * 2)
e.g. the value we borrow to produce t0 is subtracted from t1, the value we borrow from t1 is subtracted from t2 the value we borrow from t2 is equal to t3
Compute the limbs of constant_to_add
, including our offset terms t0, t1, t2, t3 that ensure each result limb is positive
Update the maximum possible value of the result. We assume here that (*this.value) = 0
Compute the binary basis limbs of our result
Compute the prime basis limb of the result
Definition at line 501 of file bigfield_impl.hpp.
|
inline |
Definition at line 490 of file bigfield.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::operator/ | ( | const bigfield< Builder, T > & | other | ) | const |
Division operator: a / b. Creates constraints for division in the circuit and checks b != 0. If you need a variant without the zero check, use div_without_denominator_check
.
other | The denominator. |
To evaluate (a / b = c mod p), we instead evaluate (c * b = a mod p), where p is the target modulus. We also check that b != 0.
Definition at line 752 of file bigfield_impl.hpp.
|
inline |
Definition at line 500 of file bigfield.hpp.
|
noexcept |
Definition at line 285 of file bigfield_impl.hpp.
bigfield< Builder, T > & bb::stdlib::bigfield< Builder, T >::operator= | ( | const bigfield< Builder, T > & | other | ) |
Definition at line 271 of file bigfield_impl.hpp.
bool_t< Builder > bb::stdlib::bigfield< Builder, T >::operator== | ( | const bigfield< Builder, T > & | other | ) | const |
Validate whether two bigfield elements are equal to each other.
To evaluate whether (a == b)
, we use result boolean r
to evaluate the following logic: (n.b all algebra involving bigfield elements is done in the bigfield)
r == 1
, a - b == 0
r == 0
, a - b
posesses an inverse I
i.e. (a - b) * I - 1 == 0
We efficiently evaluate this logic by evaluating a single expression (a - b)*X = Y
We use conditional assignment logic to define X, Y
to be the following: If r == 1
then X = 1, Y = 0
If r == 0
then X = I, Y = 1
This allows us to evaluate operator==
using only 1 bigfield multiplication operation. We can check the product equals 0 or 1 by directly evaluating the binary basis/prime basis limbs of Y. i.e. if r == 1
then (a - b)*X
should have 0 for all limb values if r == 0
then (a - b)*X
should have 1 in the least significant binary basis limb and 0 elsewhere Builder | |
T |
other |
Definition at line 1718 of file bigfield_impl.hpp.
|
static |
Performs individual reductions on the supplied elements as well as more complex reductions to prevent CRT modulus overflow and to fit the quotient inside the range proof.
Builder | builder |
T | basefield |
mul_left | |
mul_right | |
to_add |
Definition at line 1133 of file bigfield_impl.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::pow | ( | const uint32_t | exponent | ) | const |
Raise the bigfield element to the power of (out-of-circuit) exponent.
exponent | The exponent to raise the bigfield element to. |
Uses the square-and-multiply algorithm to compute a^exponent mod p.
NOTE(https://github.com/AztecProtocol/barretenberg/issues/1014) Improve the efficiency of this function using sliding window method.
Definition at line 1005 of file bigfield_impl.hpp.
|
inlinestatic |
Reconstruct a bigfield from limbs (generally stored in the public inputs)
Definition at line 759 of file bigfield.hpp.
|
private |
Check if the bigfield element needs to be reduced.
This function checks if the bigfield element is within the valid range and reduces it if necessary. When multiplying bigfield elements a and b, we need to ensure that each side of the equation: a * b = q * p + r (a) holds modulo the size of the native field n, (b) holds modulo the size of the bigger ring 2^t. (c) is less than the maximum value: M = 2^t * n. This implies a, b must always be less than √M, and their limbs must be less than the maximum limb value.
Given a bigfield element c, this function applies these checks: (i) c < √M (see note below). (ii) each limb (binary basis) of c is less than the maximum limb value.
These checks prevent our field arithmetic from overflowing the native modulus boundary, whilst ensuring we can still use the chinese remainder theorem to validate field multiplications with a reduced number of range checks.
Note: We actually apply a stricter bound, see get_maximum_unreduced_value for an explanation.
Definition at line 1759 of file bigfield_impl.hpp.
|
private |
Perform a sanity check on a value that is about to interact with another value.
ASSERTs that the value of all limbs is less than or equal to the prohibited maximum value. Checks that the maximum value of the whole element is also less than a prohibited maximum value.
Definition at line 1798 of file bigfield_impl.hpp.
void bb::stdlib::bigfield< Builder, T >::self_reduce | ( | ) | const |
Definition at line 1990 of file bigfield_impl.hpp.
|
inline |
Set the free witness flag for the bigfield.
Definition at line 723 of file bigfield.hpp.
|
inline |
Definition at line 703 of file bigfield.hpp.
|
inline |
Set the witness indices of the binary basis limbs to public.
Definition at line 746 of file bigfield.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::sqr | ( | ) | const |
Square operator, computes a * a = c mod p.
Costs the same as operator* as it just sets a = b. NOTE(https://github.com/AztecProtocol/aztec-packages/issues/15089): Can optimize this further to save a gate.
Definition at line 903 of file bigfield_impl.hpp.
bigfield< Builder, T > bb::stdlib::bigfield< Builder, T >::sqradd | ( | const std::vector< bigfield< Builder, T > > & | to_add | ) | const |
Square and add operator, computes a * a + ...to_add = c mod p.
to_add | The bigfield element to add to the square. |
We can chain multiple additions to a square/multiply with a single quotient/remainder. Chaining the additions here is cheaper than calling operator+ because we can combine some gates in evaluate_multiply_add
Definition at line 934 of file bigfield_impl.hpp.
|
static |
Create constraints for summing these terms.
Builder | |
T |
terms |
Definition at line 766 of file bigfield_impl.hpp.
|
inline |
Convert the bigfield element to a byte array. Concatenates byte arrays of the high (2L bits) and low (2L bits) parts of the bigfield element.
Assumes that 2L is divisible by 8, i.e. (NUM_LIMB_BITS * 2) % 8 == 0. Also we check that the bigfield element is in the target field.
Definition at line 363 of file bigfield.hpp.
|
inlinestaticconstexpr |
Create an unreduced 0 ~ p*k, where p*k is the minimal multiple of modulus that should be reduced.
We need it for division. If we always add this element during division, then we never run into the formula-breaking situation
Definition at line 660 of file bigfield.hpp.
|
inlinestatic |
Construct a bigfield element from binary limbs that are already reduced.
This API should only be used by bigfield and other stdlib members for efficiency and with extreme care. We need it in cases where we precompute and reduce the elements, for example, and then put them in a table
Definition at line 157 of file bigfield.hpp.
|
inlinestatic |
Construct a bigfield element from binary limbs and a prime basis limb that are already reduced.
This API should only be used by bigfield and other stdlib members for efficiency and with extreme care. We need it in cases where we precompute and reduce the elements, for example, and then put them in a table
Definition at line 230 of file bigfield.hpp.
|
staticprivate |
Evaluate a relation involving multiple multiplications and additions.
input_left | Vector of left multiplication operands. |
input_right | Vector of right multiplication operands. |
to_add | Vector of elements to add to the product. |
input_quotient | Quotient term. |
input_remainders | Vector of remainders. |
This function evaluates the relationship: (a[0] * b[0] + ... + (a[-1] * b[-1])) + (to_add[0] + .. + to_add[-1]) - q * p - (r[0] + .. + r[-1]) = 0 mod 2^t (a[0] * b[0] + ... + (a[-1] * b[-1])) + (to_add[0] + .. + to_add[-1]) - q * p - (r[0] + .. + r[-1]) = 0 mod n
msub_div
for more details on how this is used.Step 1: Compute the maximum potential value of our product limbs
max_lo = maximum value of limb products that span the range 0 - 2^{3t} max_hi = maximum value of limb products that span the range 2^{2t} - 2^{5t} (t = NUM_LIMB_BITS)
Definition at line 2245 of file bigfield_impl.hpp.
|
staticprivate |
Evaluate a multiply add identity with several added elements and several remainders.
left | Left multiplicand |
right | Right multiplicand |
to_add | Vector of elements to add |
quotient | Quotient term |
remainders | Vector of remainders |
This function evaluates the relationship: a * b + (to_add[0] + .. + to_add[-1]) - q * p - (r[0] + .. + r[-1]) = 0 mod 2^t (binary basis modulus) a * b + (to_add[0] + .. + to_add[-1]) - q * p - (r[0] + .. + r[-1]) = 0 mod n (circuit modulus)
Definition at line 2037 of file bigfield_impl.hpp.
|
staticprivate |
Evaluate a square with several additions.
left | Left multiplicand |
to_add | Vector of elements to add |
quotient | Quotient term |
remainder | Remainder term |
This function evaluates the relationship: (a * a) + (to_add[0] + .. + to_add[-1]) - q * p - r = 0 mod 2^t (binary basis modulus) (a * a) + (to_add[0] + .. + to_add[-1]) - q * p - r = 0 mod n (circuit modulus)
Definition at line 2544 of file bigfield_impl.hpp.
|
inline |
Unset the free witness flag for the bigfield.
Definition at line 734 of file bigfield.hpp.
|
inlinestatic |
Create a public zero constant
Definition at line 648 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 332 of file bigfield.hpp.
|
mutable |
Represents a bigfield element in the binary basis. A bigfield element is represented as a combination of 4 binary basis limbs: a = a[0] + a[1] * 2^L + a[2] * 2^2L + a[3] * 2^3L.
Definition at line 80 of file bigfield.hpp.
Builder* bb::stdlib::bigfield< Builder, T >::context |
Definition at line 74 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 319 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 320 of file bigfield.hpp.
|
inlinestatic |
Definition at line 317 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 323 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 322 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 897 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 928 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 922 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 327 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 326 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 308 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 309 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 347 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 341 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 340 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 339 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 311 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 310 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 72 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 331 of file bigfield.hpp.
|
mutable |
Represents a bigfield element in the prime basis: (a mod n) where n is the native modulus.
Definition at line 85 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 329 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 932 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 31 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 334 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 335 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 336 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 337 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 338 of file bigfield.hpp.
|
staticconstexpr |
Definition at line 333 of file bigfield.hpp.