diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/goblin_translator_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/goblin_translator_circuit_builder.hpp index 1ef03772898..ef4486e306a 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/goblin_translator_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/goblin_translator_circuit_builder.hpp @@ -13,7 +13,6 @@ #include "barretenberg/numeric/uint256/uint256.hpp" #include "barretenberg/proof_system/arithmetization/arithmetization.hpp" #include "barretenberg/proof_system/op_queue/ecc_op_queue.hpp" -#include "barretenberg/proof_system/types/circuit_type.hpp" #include "circuit_builder_base.hpp" #include #include @@ -25,6 +24,53 @@ namespace proof_system { * @brief GoblinTranslatorCircuitBuilder creates a circuit that evaluates the correctness of the evaluation of * EccOpQueue in Fq while operating in the Fr scalar field * + * @details Goblin Translator Circuit Builder builds a circuit the purpose of which 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 + * + * Goblin 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 p, we: + * 1) Compute a⋅b in integers + * 2) Compute quotient=a⋅b/p + * 3) Show that a⋅b - quotient⋅p - c = 0 mod 2²⁷² + * 4) Show that a⋅b - quotient⋅p - 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, Goblin Translator computes one accumulation ever 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 check 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 Goblin 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 limb + 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. + * */ class GoblinTranslatorCircuitBuilder : public CircuitBuilderBase { // We don't need templating for Goblin