|
Barretenberg
The ZK-SNARK library at the core of Aztec
|
TranslatorCircuitBuilder creates a circuit that evaluates the correctness of the evaluation of EccOpQueue in Fq while operating in the Fr scalar field (r is the modulus of Fr and q is the modulus of Fq) More...
#include <translator_circuit_builder.hpp>
Classes | |
| struct | AccumulationInput |
| The accumulation input structure contains all the necessary values to initalize an accumulation gate as well as additional values for checking its correctness. More... | |
Public Member Functions | |
| size_t | get_num_constant_gates () const override |
| TranslatorCircuitBuilder (Fq batching_challenge_v_, Fq evaluation_input_x_, bool avm_mode_=false) | |
| Construct a new Translator Circuit Builder object. | |
| TranslatorCircuitBuilder (Fq batching_challenge_v_, Fq evaluation_input_x_, std::shared_ptr< ECCOpQueue > op_queue, bool avm_mode=false) | |
| Construct a new Translator Circuit Builder object and feed op_queue inside. | |
| TranslatorCircuitBuilder ()=default | |
| TranslatorCircuitBuilder (const TranslatorCircuitBuilder &other)=delete | |
| TranslatorCircuitBuilder (TranslatorCircuitBuilder &&other) noexcept | |
| TranslatorCircuitBuilder & | operator= (const TranslatorCircuitBuilder &other)=delete |
| TranslatorCircuitBuilder & | operator= (TranslatorCircuitBuilder &&other) noexcept |
| ~TranslatorCircuitBuilder () override=default | |
| void | create_accumulation_gate (const AccumulationInput &acc_step) |
| Create a single accumulation gate. | |
| void | populate_wires_from_ultra_op (const UltraOp &ultra_op) |
| void | insert_pair_into_wire (WireIds wire_index, Fr first, Fr second) |
| void | feed_ecc_op_queue_into_circuit (const std::shared_ptr< ECCOpQueue > &ecc_op_queue) |
| Generate all the gates required to prove the correctness of batched evalution of column polynomials representing the ECCOpQueue. | |
Public Member Functions inherited from bb::CircuitBuilderBase< bb::fr > | |
| CircuitBuilderBase (size_t size_hint=0, bool is_write_vk_mode=false) | |
| CircuitBuilderBase (const CircuitBuilderBase &other)=default | |
| CircuitBuilderBase (CircuitBuilderBase &&other) noexcept=default | |
| CircuitBuilderBase & | operator= (const CircuitBuilderBase &other)=default |
| CircuitBuilderBase & | operator= (CircuitBuilderBase &&other) noexcept=default |
| virtual | ~CircuitBuilderBase ()=default |
| bool | operator== (const CircuitBuilderBase &other) const=default |
| virtual size_t | get_num_finalized_gates () const |
| virtual size_t | get_num_variables () const |
| size_t | num_gates () const |
| void | increment_num_gates (size_t count=1) |
| const std::unordered_map< uint32_t, uint32_t > & | tau () const |
| uint32_t | zero_idx () const |
| const std::vector< FF > & | get_variables () const |
| FF | get_variable (const uint32_t index) const |
| Get the value of the variable v_{index}. | |
| void | set_variable (const uint32_t index, const FF &value) |
| Set the value of the variable pointed to by a witness index. | |
| const std::vector< uint32_t > & | public_inputs () const |
| void | finalize_public_inputs () |
| Set the _public_inputs_finalized to true to prevent any new public inputs from being added. | |
| void | initialize_public_inputs (const std::vector< uint32_t > &public_inputs) |
| Directly initialize the public inputs vector. | |
| virtual uint32_t | add_variable (const FF &in) |
| Add a variable to variables. | |
| uint32_t | add_variable (const OT &in)=delete |
| virtual uint32_t | add_public_variable (const FF &in) |
| Add a public variable to variables. | |
| uint32_t | add_public_variable (const OT &in)=delete |
| virtual uint32_t | set_public_input (uint32_t witness_index) |
| Make a witness variable public. | |
| virtual void | assert_equal (uint32_t a_idx, uint32_t b_idx, std::string const &msg="assert_equal") |
| size_t | get_circuit_subgroup_size (size_t num_gates) const |
| size_t | num_public_inputs () const |
| virtual void | set_variable_name (uint32_t index, const std::string &name) |
| Assign a name to a variable (equivalence class) | |
| virtual msgpack::sbuffer | export_circuit () |
| Export the existing circuit as msgpack compatible buffer. | |
| bool | failed () const |
| const std::string & | err () const |
| void | failure (std::string msg) |
| bool | is_write_vk_mode () const |
Static Public Member Functions | |
| static std::array< Fr, NUM_BINARY_LIMBS > | split_fq_into_limbs (const Fq &base) |
| A small function to transform a native element Fq into its bigfield representation in Fr scalars. | |
| static void | assert_well_formed_ultra_op (const UltraOp &ultra_op) |
| static void | assert_well_formed_accumulation_input (const AccumulationInput &acc_step) |
| Ensures the accumulation input is well-formed and can be used to create a gate. | |
| static AccumulationInput | generate_witness_values (const UltraOp &ultra_op, const Fq &previous_accumulator, const Fq &batching_challenge_v, const Fq &evaluation_input_x) |
| Given the transcript values from the EccOpQueue, the values of the previous accumulator, batching challenge and input x, compute witness for one step of accumulation. | |
Public Attributes | |
| Fq | batching_challenge_v |
| Fq | evaluation_input_x |
| bool | avm_mode = false |
| std::array< std::vector< uint32_t >, NUM_WIRES > | wires |
Public Attributes inherited from bb::CircuitBuilderBase< bb::fr > | |
| std::vector< uint32_t > | real_variable_index |
| Map from witness index to real variable index. | |
| std::vector< uint32_t > | real_variable_tags |
real_variable_tags is the tagging mechanism for the the multiset-equality check. | |
| uint32_t | current_tag |
| PairingPointsTagging | pairing_points_tagging |
| PairingPoints tagging tool, used to ensure that all pairing points created in this circuit are aggregated together. This is not related to circuit logic. | |
Static Public Attributes | |
| static constexpr size_t | NUM_WIRES = 81 |
| static constexpr size_t | NUM_SELECTORS = 0 |
| static constexpr size_t | DEFAULT_TRANSLATOR_VM_LENGTH = 2048 |
| static constexpr size_t | NUM_LIMB_BITS = 68 |
| static constexpr size_t | NUM_LAST_LIMB_BITS = Fq::modulus.get_msb() + 1 - 3 * NUM_LIMB_BITS |
| static constexpr size_t | NUM_Z_LIMBS = 2 |
| static constexpr size_t | NUM_QUOTIENT_BITS = 256 |
| static constexpr size_t | NUM_LAST_QUOTIENT_LIMB_BITS = 256 - 3 * NUM_LIMB_BITS |
| static constexpr size_t | NUM_Z_BITS = 128 |
| static constexpr size_t | MICRO_LIMB_BITS = 14 |
| static constexpr auto | MAX_MICRO_LIMB_SIZE = (uint256_t(1) << MICRO_LIMB_BITS) - 1 |
| static constexpr size_t | NUM_MICRO_LIMBS = 6 |
| static constexpr size_t | NUM_BINARY_LIMBS = 4 |
| static constexpr size_t | NUM_RELATION_WIDE_LIMBS = 2 |
| static constexpr size_t | RELATION_WIDE_LIMB_BITS = 84 |
| static constexpr uint256_t | MAX_RELATION_WIDE_LIMB_SIZE = uint256_t(1) << RELATION_WIDE_LIMB_BITS |
| static constexpr auto | MICRO_SHIFT = uint256_t(1) << MICRO_LIMB_BITS |
| static constexpr auto | MAX_LOW_WIDE_LIMB_SIZE = (uint256_t(1) << (NUM_LIMB_BITS * 2)) - 1 |
| static constexpr auto | MAX_HIGH_WIDE_LIMB_SIZE = (uint256_t(1) << (NUM_LIMB_BITS + NUM_LAST_LIMB_BITS)) - 1 |
| static constexpr size_t | RESULT_ROW = 8 |
| static constexpr size_t | NUM_NO_OPS_START = 1 |
| static constexpr size_t | NUM_RANDOM_OPS_START = 3 |
| static constexpr size_t | NUM_RANDOM_OPS_END = 2 |
| static constexpr auto | SHIFT_1 = uint256_t(1) << NUM_LIMB_BITS |
| static constexpr auto | SHIFT_2 = uint256_t(1) << (NUM_LIMB_BITS << 1) |
| static constexpr auto | SHIFT_2_INVERSE = Fr(SHIFT_2).invert() |
| static constexpr auto | SHIFT_3 = uint256_t(1) << (NUM_LIMB_BITS * 3) |
| static constexpr uint512_t | MODULUS_U512 = uint512_t(Fq::modulus) |
| static constexpr uint512_t | BINARY_BASIS_MODULUS = uint512_t(1) << (NUM_LIMB_BITS << 2) |
| static constexpr uint512_t | NEGATIVE_PRIME_MODULUS = BINARY_BASIS_MODULUS - MODULUS_U512 |
| static constexpr std::array< Fr, 5 > | NEGATIVE_MODULUS_LIMBS |
| static constexpr std::string_view | NAME_STRING = "TranslatorCircuitBuilder" |
Private Types | |
| using | Fr = bb::fr |
| using | Fq = bb::fq |
Additional Inherited Members | |
Protected Member Functions inherited from bb::CircuitBuilderBase< bb::fr > | |
| void | set_zero_idx (uint32_t value) |
| uint32_t | get_first_variable_in_class (uint32_t index) const |
| Get the index of the first variable in class. | |
| void | assert_valid_variables (const std::vector< uint32_t > &variable_indices) |
| Check whether each variable index points to a witness value in the variables array. | |
Protected Attributes inherited from bb::CircuitBuilderBase< bb::fr > | |
| std::unordered_map< uint32_t, uint32_t > | _tau |
| The permutation on variable tags, as a constituent of the generalized permutation argument. | |
| std::unordered_map< uint32_t, std::string > | variable_names |
TranslatorCircuitBuilder creates a circuit that evaluates the correctness of the evaluation of EccOpQueue in Fq while operating in the Fr scalar field (r is the modulus of Fr and q is the modulus of Fq)
Translator Circuit Builder builds a circuit whose purpose is to calculate the batched evaluation of 5 polynomials in non-native field represented through coefficients in 4 native polynomials (op, x_lo_y_hi, x_hi_z_1, y_lo_z_2):
OP | X_LO | X_HI | Y_LO 0 | Y_HI | Z1 | Z2
OP is supposed to be { 0, 1, 2, 3, 4, 8 }. X_LO and Y_LO need to be < 2¹³⁶, X_HI and Y_LO < 2¹¹⁸, Z1 and Z2 < 2¹²⁸. X_* and Y_* are supposed to be the decompositions of bn254 base fields elements P.x and P.y and are split into two chunks each because the scalar field we are operating on can't fit them
Translator calculates the result of evaluation of a polynomial op + P.x⋅v +P.y⋅v² + z1 ⋅ v³ + z2⋅v⁴ at the given challenge x (evaluation_input_x). For this it uses logic similar to the stdlib bigfield class. We operate in Fr while trying to calculate values in Fq. To show that a⋅b=c mod q, we: 1) Compute a⋅b in integers 2) Compute quotient=a⋅b/q 3) Show that a⋅b - quotient⋅q - c = 0 mod 2²⁷² 4) Show that a⋅b - quotient⋅q - c = 0 mod r (scalar field modulus) This ensures that the logic is sound modulo 2²⁷²⋅r, which means it's correct in integers, if all the values are sufficiently constrained (there is no way to undeflow or overflow)
Concretely, Translator computes one accumulation every two gates: previous_accumulator⋅x + op + P.x⋅v +P.y⋅v² + z1⋅v³ + z2⋅v⁴ = current_accumulator mod p. Because of the nature of polynomial commitment, previous_accumulator is located at higher index than the current_accumulator. Values of x (evaluation_input_x) and v (batching_challenge_v) are precomputed and considered inputs to the relations.
P.x and P.y are deconstructed into 4 limbs (3 68-bit and 1 50-bit) for non-native arithmetic z1 and z2 are deconstructed into 2 limbs each (68 and 60 bits) op is small and doesn't have to be deconstructed
To show the accumulation is correct we also need to provide the quotient and accumulators as witnesses. Accumulator is split the same way as P.x and P.y, but quotient is 256 bits,so the top limb is 52 bits.
Ensuring that the relation mod 2²⁷² is correct is done through splitting this check into two checks modulo 2¹³⁶. First, we check that a proper combination of the values in the lower limbs gives the correct result modulo 2¹³⁶ (by dividing the result by 2¹³⁶ and range constraining it). Then we use the overlow and higher limbs to prove the same modulo 2¹³⁶ again and as a result we get correctness modulo 2²⁷².
One big issue are range constraints. In Translator we check ranges by decomposing LIMBS into special other range constrained MICROLIMBS (have "_CONSTRAINT_" in the name of their wires). These wires always have the range of 14 bits, so when we need to constrain something further we use two wires at once and scale the values (for example, 68 bits are decomposed into 5 14-bit limbs + 1 shifted limb, which is equal to the highest microlimb multiplied by 4). The shifted wires usually have "_TAIL" in the name, but that is not a strict rule. To save space and because of the proving system requirements we put some of the decomposed values from relation limbs (limbs which compute the result of computation modulo 2²⁷² divided by shifts) into constraint wires named after P.x, P.y, accumulator and quotient. This is due to the fact that the highest limb in these four is less than 56 bits, which frees up an extra microlimb.
Definition at line 69 of file translator_circuit_builder.hpp.
|
private |
Definition at line 74 of file translator_circuit_builder.hpp.
|
private |
Definition at line 72 of file translator_circuit_builder.hpp.
| enum bb::TranslatorCircuitBuilder::WireIds : size_t |
There are so many wires that naming them has no sense, it is easier to access them with enums.
Definition at line 85 of file translator_circuit_builder.hpp.
|
inline |
Construct a new Translator Circuit Builder object.
Translator Circuit builder has to be initializaed with evaluation input and batching challenge (they are used to compute witness and to store the value for the prover)
| batching_challenge_v_ | |
| evaluation_input_x_ |
Definition at line 328 of file translator_circuit_builder.hpp.
|
inline |
Construct a new Translator Circuit Builder object and feed op_queue inside.
Translator Circuit builder has to be initialized with evaluation input and batching challenge (they are used to compute witness and to store the value for the prover)
| batching_challenge_v_ | |
| evaluation_input_x_ | |
| op_queue |
Definition at line 347 of file translator_circuit_builder.hpp.
|
default |
|
delete |
|
inlinenoexcept |
Definition at line 360 of file translator_circuit_builder.hpp.
|
overridedefault |
|
static |
Ensures the accumulation input is well-formed and can be used to create a gate.
There are two main types of checks: that members of the AccumulationInput are within the appropriate ranges and that the members containing *limbs have been constructed appropriately from the original values, present in the AccumulationInput.
| acc_step |
Check correctness of limbs values
Definition at line 346 of file translator_circuit_builder.cpp.
|
static |
Definition at line 327 of file translator_circuit_builder.cpp.
| void bb::TranslatorCircuitBuilder::create_accumulation_gate | ( | const AccumulationInput & | acc_step | ) |
Create a single accumulation gate.
An accumulation gate is used to process one UltraOp from the op queue and adds 2 rows in the Translator "trace" (or circuit).
| acc_step | |
| acc_step |
Put several values in sequential wires
Definition at line 427 of file translator_circuit_builder.cpp.
| void bb::TranslatorCircuitBuilder::feed_ecc_op_queue_into_circuit | ( | const std::shared_ptr< ECCOpQueue > & | ecc_op_queue | ) |
Generate all the gates required to prove the correctness of batched evalution of column polynomials representing the ECCOpQueue.
Definition at line 520 of file translator_circuit_builder.cpp.
|
static |
Given the transcript values from the EccOpQueue, the values of the previous accumulator, batching challenge and input x, compute witness for one step of accumulation.
| Fq | |
| Fr |
| ultra_op | The ultra op used to produce the wire data |
| previous_accumulator | The value of the previous accumulator (we assume standard decomposition into limbs) |
| batching_challenge_v | The value of the challenge for batching polynomial evaluations |
| evaluation_input_x | The value at which we evaluate the polynomials |
A small function to transform a uint512_t element into its 4 68-bit limbs in Fr scalars
Split and integer stored in uint512_T into 4 68-bit chunks (we assume that it is lower than 2²⁷²), convert to Fr
A method for splitting wide limbs (P_x_lo, P_y_hi, etc) into two limbs
A method to split a full 68-bit limb into 5 14-bit limb and 1 shifted limb for a more secure constraint
A method to split the top 50-bit limb into 4 14-bit limbs and 1 shifted limb for a more secure constraint (plus there is 1 extra space for other constraints)
A method for splitting the top 60-bit z limb into microlimbs (differs from the 68-bit limb by the shift in the last limb)
Split a 72-bit relation limb into 6 14-bit limbs (we can allow the slack here, since we only need to ensure non-overflow of the modulus)
Definition at line 37 of file translator_circuit_builder.cpp.
|
inlineoverridevirtual |
Implements bb::CircuitBuilderBase< bb::fr >.
Definition at line 80 of file translator_circuit_builder.hpp.
|
inline |
Definition at line 411 of file translator_circuit_builder.hpp.
|
delete |
|
inlinenoexcept |
Definition at line 363 of file translator_circuit_builder.hpp.
| void bb::TranslatorCircuitBuilder::populate_wires_from_ultra_op | ( | const UltraOp & | ultra_op | ) |
Definition at line 403 of file translator_circuit_builder.cpp.
|
inlinestatic |
A small function to transform a native element Fq into its bigfield representation in Fr scalars.
We transform Fq into an integer and then split it into 68-bit limbs, then convert them to Fr.
Definition at line 376 of file translator_circuit_builder.hpp.
| bool bb::TranslatorCircuitBuilder::avm_mode = false |
Definition at line 316 of file translator_circuit_builder.hpp.
| Fq bb::TranslatorCircuitBuilder::batching_challenge_v |
Definition at line 311 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 263 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 181 of file translator_circuit_builder.hpp.
| Fq bb::TranslatorCircuitBuilder::evaluation_input_x |
Definition at line 314 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 231 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 228 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 205 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 222 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 202 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 225 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 260 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 308 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 270 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 266 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 213 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 187 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 196 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 184 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 209 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 237 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 193 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 244 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 240 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 216 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 78 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 77 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 199 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 190 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 219 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 236 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 248 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 251 of file translator_circuit_builder.hpp.
Definition at line 254 of file translator_circuit_builder.hpp.
|
staticconstexpr |
Definition at line 257 of file translator_circuit_builder.hpp.
| std::array<std::vector<uint32_t>, NUM_WIRES> bb::TranslatorCircuitBuilder::wires |
Definition at line 318 of file translator_circuit_builder.hpp.