diff --git a/barretenberg/cpp/src/barretenberg/benchmark/relations_bench/relations.bench.cpp b/barretenberg/cpp/src/barretenberg/benchmark/relations_bench/relations.bench.cpp index a1877668a7f..6e7069f08ae 100644 --- a/barretenberg/cpp/src/barretenberg/benchmark/relations_bench/relations.bench.cpp +++ b/barretenberg/cpp/src/barretenberg/benchmark/relations_bench/relations.bench.cpp @@ -117,6 +117,7 @@ BENCHMARK(execute_relation_for_values>) BENCHMARK(execute_relation_for_values>); BENCHMARK(execute_relation_for_values>); BENCHMARK(execute_relation_for_values>); +BENCHMARK(execute_relation_for_values>); } // namespace bb::benchmark::relations diff --git a/barretenberg/cpp/src/barretenberg/client_ivc/client_ivc.test.cpp b/barretenberg/cpp/src/barretenberg/client_ivc/client_ivc.test.cpp index 8ad78f0ac0b..8730a8793b0 100644 --- a/barretenberg/cpp/src/barretenberg/client_ivc/client_ivc.test.cpp +++ b/barretenberg/cpp/src/barretenberg/client_ivc/client_ivc.test.cpp @@ -119,7 +119,7 @@ TEST_F(ClientIVCTests, BasicFailure) * @brief Prove and verify accumulation of an arbitrary set of circuits * */ -TEST_F(ClientIVCTests, DISABLED_BasicLarge) +TEST_F(ClientIVCTests, BasicLarge) { ClientIVC ivc; @@ -142,7 +142,7 @@ TEST_F(ClientIVCTests, DISABLED_BasicLarge) * @brief Using a structured trace allows for the accumulation of circuits of varying size * */ -TEST_F(ClientIVCTests, DISABLED_BasicStructured) +TEST_F(ClientIVCTests, BasicStructured) { ClientIVC ivc; ivc.structured_flag = true; diff --git a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.hpp index 7f49af86030..4219d344602 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.hpp @@ -120,15 +120,10 @@ class ECCVMCircuitBuilder { // populate opqueue and mul indices for (const auto& op : raw_ops) { if (op.mul) { - if (op.z1 != 0 || op.z2 != 0) { + if ((op.z1 != 0 || op.z2 != 0) && !op.base_point.is_point_at_infinity()) { msm_opqueue_index.push_back(op_idx); msm_mul_index.emplace_back(msm_count, active_mul_count); - } - if (op.z1 != 0) { - active_mul_count++; - } - if (op.z2 != 0) { - active_mul_count++; + active_mul_count += static_cast(op.z1 != 0) + static_cast(op.z2 != 0); } } else if (active_mul_count > 0) { msm_sizes.push_back(active_mul_count); @@ -138,7 +133,7 @@ class ECCVMCircuitBuilder { op_idx++; } // if last op is a mul we have not correctly computed the total number of msms - if (raw_ops.back().mul) { + if (raw_ops.back().mul && active_mul_count > 0) { msm_sizes.push_back(active_mul_count); msm_count++; } @@ -152,7 +147,7 @@ class ECCVMCircuitBuilder { for (size_t i = start; i < end; i++) { const auto& op = raw_ops[msm_opqueue_index[i]]; auto [msm_index, mul_index] = msm_mul_index[i]; - if (op.z1 != 0) { + if (op.z1 != 0 && !op.base_point.is_point_at_infinity()) { ASSERT(result.size() > msm_index); ASSERT(result[msm_index].size() > mul_index); result[msm_index][mul_index] = (ScalarMul{ @@ -165,7 +160,7 @@ class ECCVMCircuitBuilder { }); mul_index++; } - if (op.z2 != 0) { + if (op.z2 != 0 && !op.base_point.is_point_at_infinity()) { ASSERT(result.size() > msm_index); ASSERT(result[msm_index].size() > mul_index); auto endo_point = AffineElement{ op.base_point.x * FF::cube_root_of_unity(), -op.base_point.y }; diff --git a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.test.cpp b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.test.cpp index b5cb7698360..106dcdb4eae 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.test.cpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_circuit_builder.test.cpp @@ -18,8 +18,10 @@ TEST(ECCVMCircuitBuilderTests, BaseCase) typename G1::element a = generators[0]; typename G1::element b = generators[1]; typename G1::element c = generators[2]; + typename G1::element point_at_infinity = G1::point_at_infinity; Fr x = Fr::random_element(&engine); Fr y = Fr::random_element(&engine); + Fr zero_scalar = 0; std::shared_ptr op_queue = std::make_shared(); @@ -29,14 +31,49 @@ TEST(ECCVMCircuitBuilderTests, BaseCase) op_queue->mul_accumulate(b, y); op_queue->add_accumulate(a); op_queue->mul_accumulate(b, x); + op_queue->no_op(); + op_queue->add_accumulate(b); op_queue->eq_and_reset(); op_queue->add_accumulate(c); op_queue->mul_accumulate(a, x); + op_queue->mul_accumulate(point_at_infinity, x); op_queue->mul_accumulate(b, x); op_queue->eq_and_reset(); op_queue->mul_accumulate(a, x); op_queue->mul_accumulate(b, x); + op_queue->mul_accumulate(point_at_infinity, zero_scalar); op_queue->mul_accumulate(c, x); + op_queue->eq_and_reset(); + op_queue->mul_accumulate(point_at_infinity, zero_scalar); + op_queue->mul_accumulate(point_at_infinity, x); + op_queue->mul_accumulate(point_at_infinity, zero_scalar); + op_queue->add_accumulate(a); + op_queue->eq_and_reset(); + op_queue->add_accumulate(a); + op_queue->add_accumulate(point_at_infinity); + op_queue->eq_and_reset(); + op_queue->add_accumulate(point_at_infinity); + op_queue->eq_and_reset(); + op_queue->mul_accumulate(point_at_infinity, x); + op_queue->mul_accumulate(point_at_infinity, -x); + op_queue->eq_and_reset(); + op_queue->add_accumulate(a); + op_queue->mul_accumulate(point_at_infinity, x); + op_queue->mul_accumulate(point_at_infinity, -x); + op_queue->add_accumulate(a); + op_queue->add_accumulate(a); + op_queue->eq_and_reset(); + + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} + +TEST(ECCVMCircuitBuilderTests, NoOp) +{ + std::shared_ptr op_queue = std::make_shared(); + + op_queue->no_op(); ECCVMCircuitBuilder circuit{ op_queue }; bool result = ECCVMTraceChecker::check(circuit, &engine); @@ -72,6 +109,109 @@ TEST(ECCVMCircuitBuilderTests, Mul) EXPECT_EQ(result, true); } +TEST(ECCVMCircuitBuilderTests, MulInfinity) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element a = generators[0]; + Fr x = Fr::random_element(&engine); + G1::element b = -a * x; + // G1::affine_element c = G1::affine_point_at_infinity; + op_queue->add_accumulate(b); + op_queue->mul_accumulate(a, x); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} + +// Validate we do not trigger edge cases of addition formulae when we have identical mul inputs +TEST(ECCVMCircuitBuilderTests, MulOverIdenticalInputs) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element a = generators[0]; + Fr x = Fr::random_element(&engine); + op_queue->mul_accumulate(a, x); + op_queue->mul_accumulate(a, x); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} + +TEST(ECCVMCircuitBuilderTests, MSMProducesInfinity) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element a = generators[0]; + Fr x = Fr::random_element(&engine); + op_queue->add_accumulate(a); + op_queue->mul_accumulate(a, x); + op_queue->mul_accumulate(a, -x); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} + +TEST(ECCVMCircuitBuilderTests, MSMOverPointAtInfinity) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element point_at_infinity = G1::point_at_infinity; + typename G1::element b = generators[0]; + Fr x = Fr::random_element(&engine); + Fr zero_scalar = 0; + + // validate including points at infinity in a multiscalar multiplication does not effect result + { + op_queue->mul_accumulate(b, x); + op_queue->mul_accumulate(point_at_infinity, x); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); + } + // validate multiplying a point at infinity by nonzero scalar produces point at infinity + { + op_queue->mul_accumulate(point_at_infinity, x); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); + } + // validate multiplying a point by zero produces point at infinity + { + op_queue->mul_accumulate(b, zero_scalar); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); + } + // validate multiplying a point at infinity by zero produces a point at infinity + { + op_queue->mul_accumulate(point_at_infinity, zero_scalar); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); + } + // validate an MSM made entirely of points at infinity / zero scalars produces a point at infinity + { + op_queue->mul_accumulate(point_at_infinity, x); + op_queue->mul_accumulate(b, zero_scalar); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); + } +} + TEST(ECCVMCircuitBuilderTests, ShortMul) { std::shared_ptr op_queue = std::make_shared(); @@ -243,3 +383,67 @@ TEST(ECCVMCircuitBuilderTests, MSM) bool result = ECCVMTraceChecker::check(circuit, &engine); EXPECT_EQ(result, true); } + +TEST(ECCVMCircuitBuilderTests, EqAgainstPointAtInfinity) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element a = generators[0]; + a.self_set_infinity(); + + op_queue->add_accumulate(a); + op_queue->eq_and_reset(); + + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} + +TEST(ECCVMCircuitBuilderTests, AddPointAtInfinity) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element a = generators[0]; + typename G1::element b = generators[0]; + b.self_set_infinity(); + + op_queue->add_accumulate(a); + op_queue->add_accumulate(b); + op_queue->eq_and_reset(); + + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} + +TEST(ECCVMCircuitBuilderTests, AddProducesPointAtInfinity) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element a = generators[0]; + + op_queue->add_accumulate(a); + op_queue->add_accumulate(-a); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} + +TEST(ECCVMCircuitBuilderTests, AddProducesDouble) +{ + std::shared_ptr op_queue = std::make_shared(); + + auto generators = G1::derive_generators("test generators", 3); + typename G1::element a = generators[0]; + + op_queue->add_accumulate(a); + op_queue->add_accumulate(a); + op_queue->eq_and_reset(); + ECCVMCircuitBuilder circuit{ op_queue }; + bool result = ECCVMTraceChecker::check(circuit); + EXPECT_EQ(result, true); +} \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_flavor.hpp b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_flavor.hpp index 5f53b7e1784..c57a92b9894 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_flavor.hpp @@ -8,6 +8,7 @@ #include "barretenberg/flavor/flavor_macros.hpp" #include "barretenberg/flavor/relation_definitions.hpp" #include "barretenberg/polynomials/univariate.hpp" +#include "barretenberg/relations/ecc_vm/ecc_bools_relation.hpp" #include "barretenberg/relations/ecc_vm/ecc_lookup_relation.hpp" #include "barretenberg/relations/ecc_vm/ecc_msm_relation.hpp" #include "barretenberg/relations/ecc_vm/ecc_point_table_relation.hpp" @@ -37,17 +38,17 @@ class ECCVMFlavor { using RelationSeparator = FF; using MSM = bb::eccvm::MSM; - static constexpr size_t NUM_WIRES = 74; + static constexpr size_t NUM_WIRES = 85; // The number of multivariate polynomials on which a sumcheck prover sumcheck operates (including shifts). We often // need containers of this size to hold related data, so we choose a name more agnostic than `NUM_POLYNOMIALS`. // Note: this number does not include the individual sorted list polynomials. - static constexpr size_t NUM_ALL_ENTITIES = 105; + static constexpr size_t NUM_ALL_ENTITIES = 116; // The number of polynomials precomputed to describe a circuit and to aid a prover in constructing a satisfying // assignment of witnesses. We again choose a neutral name. static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 3; // The total number of witness entities not including shifts. - static constexpr size_t NUM_WITNESS_ENTITIES = 76; + static constexpr size_t NUM_WITNESS_ENTITIES = 87; using GrandProductRelations = std::tuple>; // define the tuple of Relations that comprise the Sumcheck relation @@ -56,7 +57,8 @@ class ECCVMFlavor { ECCVMWnafRelation, ECCVMMSMRelation, ECCVMSetRelation, - ECCVMLookupRelation>; + ECCVMLookupRelation, + ECCVMBoolsRelation>; using LookupRelation = ECCVMLookupRelation; static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length(); @@ -109,80 +111,91 @@ class ECCVMFlavor { template class WireEntities { public: DEFINE_FLAVOR_MEMBERS(DataType, - transcript_add, // column 0 - transcript_mul, // column 1 - transcript_eq, // column 2 - transcript_collision_check, // column 3 - transcript_msm_transition, // column 4 - transcript_pc, // column 5 - transcript_msm_count, // column 6 - transcript_Px, // column 7 - transcript_Py, // column 8 - transcript_z1, // column 9 - transcript_z2, // column 10 - transcript_z1zero, // column 11 - transcript_z2zero, // column 12 - transcript_op, // column 13 - transcript_accumulator_x, // column 14 - transcript_accumulator_y, // column 15 - transcript_msm_x, // column 16 - transcript_msm_y, // column 17 - precompute_pc, // column 18 - precompute_point_transition, // column 19 - precompute_round, // column 20 - precompute_scalar_sum, // column 21 - precompute_s1hi, // column 22 - precompute_s1lo, // column 23 - precompute_s2hi, // column 24 - precompute_s2lo, // column 25 - precompute_s3hi, // column 26 - precompute_s3lo, // column 27 - precompute_s4hi, // column 28 - precompute_s4lo, // column 29 - precompute_skew, // column 30 - precompute_dx, // column 31 - precompute_dy, // column 32 - precompute_tx, // column 33 - precompute_ty, // column 34 - msm_transition, // column 35 - msm_add, // column 36 - msm_double, // column 37 - msm_skew, // column 38 - msm_accumulator_x, // column 39 - msm_accumulator_y, // column 40 - msm_pc, // column 41 - msm_size_of_msm, // column 42 - msm_count, // column 43 - msm_round, // column 44 - msm_add1, // column 45 - msm_add2, // column 46 - msm_add3, // column 47 - msm_add4, // column 48 - msm_x1, // column 49 - msm_y1, // column 50 - msm_x2, // column 51 - msm_y2, // column 52 - msm_x3, // column 53 - msm_y3, // column 54 - msm_x4, // column 55 - msm_y4, // column 56 - msm_collision_x1, // column 57 - msm_collision_x2, // column 58 - msm_collision_x3, // column 59 - msm_collision_x4, // column 60 - msm_lambda1, // column 61 - msm_lambda2, // column 62 - msm_lambda3, // column 63 - msm_lambda4, // column 64 - msm_slice1, // column 65 - msm_slice2, // column 66 - msm_slice3, // column 67 - msm_slice4, // column 68 - transcript_accumulator_empty, // column 69 - transcript_reset_accumulator, // column 70 - precompute_select, // column 71 - lookup_read_counts_0, // column 72 - lookup_read_counts_1); // column 73 + transcript_add, // column 0 + transcript_mul, // column 1 + transcript_eq, // column 2 + transcript_msm_transition, // column 3 + transcript_pc, // column 4 + transcript_msm_count, // column 5 + transcript_Px, // column 6 + transcript_Py, // column 7 + transcript_z1, // column 8 + transcript_z2, // column 9 + transcript_z1zero, // column 10 + transcript_z2zero, // column 11 + transcript_op, // column 12 + transcript_accumulator_x, // column 13 + transcript_accumulator_y, // column 14 + transcript_msm_x, // column 15 + transcript_msm_y, // column 16 + precompute_pc, // column 17 + precompute_point_transition, // column 18 + precompute_round, // column 19 + precompute_scalar_sum, // column 20 + precompute_s1hi, // column 21 + precompute_s1lo, // column 22 + precompute_s2hi, // column 23 + precompute_s2lo, // column 24 + precompute_s3hi, // column 25 + precompute_s3lo, // column 26 + precompute_s4hi, // column 27 + precompute_s4lo, // column 28 + precompute_skew, // column 29 + precompute_dx, // column 30 + precompute_dy, // column 31 + precompute_tx, // column 32 + precompute_ty, // column 33 + msm_transition, // column 34 + msm_add, // column 35 + msm_double, // column 36 + msm_skew, // column 37 + msm_accumulator_x, // column 38 + msm_accumulator_y, // column 39 + msm_pc, // column 40 + msm_size_of_msm, // column 41 + msm_count, // column 42 + msm_round, // column 43 + msm_add1, // column 44 + msm_add2, // column 45 + msm_add3, // column 46 + msm_add4, // column 47 + msm_x1, // column 48 + msm_y1, // column 49 + msm_x2, // column 50 + msm_y2, // column 51 + msm_x3, // column 52 + msm_y3, // column 53 + msm_x4, // column 54 + msm_y4, // column 55 + msm_collision_x1, // column 56 + msm_collision_x2, // column 57 + msm_collision_x3, // column 58 + msm_collision_x4, // column 59 + msm_lambda1, // column 60 + msm_lambda2, // column 61 + msm_lambda3, // column 62 + msm_lambda4, // column 63 + msm_slice1, // column 64 + msm_slice2, // column 65 + msm_slice3, // column 66 + msm_slice4, // column 67 + transcript_accumulator_empty, // column 68 + transcript_reset_accumulator, // column 69 + precompute_select, // column 70 + lookup_read_counts_0, // column 71 + lookup_read_counts_1, // column 72 + transcript_base_infinity, // column 73 + transcript_base_x_inverse, // column 74 + transcript_base_y_inverse, // column 75 + transcript_add_x_equal, // column 76 + transcript_add_y_equal, // column 77 + transcript_add_lambda, // column 78 + transcript_msm_intermediate_x, // column 79 + transcript_msm_intermediate_y, // column 80 + transcript_msm_infinity, // column 81 + transcript_msm_x_inverse, // column 82 + transcript_msm_count_zero_at_transition, // column 83 + transcript_msm_count_at_transition_inverse); // column 84 }; /** @@ -391,7 +404,6 @@ class ECCVMFlavor { * lagrange_second: lagrange_second[1] = 1, 0 elsewhere * lagrange_last: lagrange_last[lagrange_last.size() - 1] = 1, 0 elsewhere * transcript_add/mul/eq/reset_accumulator: boolean selectors that toggle add/mul/eq/reset opcodes - * transcript_collision_check: used to ensure any point being added into eccvm accumulator does not trigger * incomplete addition rules * transcript_msm_transition: is current transcript row the final `mul` opcode of a multiscalar @@ -412,6 +424,18 @@ class ECCVMFlavor { * transcript_msm_x: x-coordinate of MSM output * transcript_msm_y: y-coordinate of MSM output * transcript_accumulator_empty: if 1, transcript_accumulator = point at infinity + * transcript_base_infinity: if 1, transcript_Px, transcript_Py is a point at infinity + * transcript_add_x_equal: if adding a point into the accumulator, is 1 if x-coordinates are equal + * transcript_add_y_equal: if adding a point into the accumulator, is 1 if y-coordinates are equal + * transcript_base_x_inverse: to check transcript_add_x_equal (if x-vals not equal inverse exists) + * transcript_base_y_inverse: to check transcript_add_x_equal (if y-vals not equal inverse exists) + * transcript_add_lambda: if adding a point into the accumulator, contains the lambda gradient + * transcript_msm_intermediate_x: if add MSM result into accumulator, is msm_output - offset_generator + * transcript_msm_intermediate_y: if add MSM result into accumulator, is msm_output - offset_generator + * transcript_msm_infinity: is MSM result the point at infinity? + * transcript_msm_x_inverse: used to validate transcript_msm_infinity correct + * transcript_msm_count_zero_at_transition: does an MSM only contain points at infinity/zero scalars + * transcript_msm_count_at_transition_inverse: used to validate transcript_msm_count_zero_at_transition * precompute_pc: point counter for Straus precomputation columns * precompute_select: if 1, evaluate Straus precomputation algorithm at current row * precompute_point_transition: 1 if current row operating on a different point to previous row @@ -516,7 +540,18 @@ class ECCVMFlavor { transcript_accumulator_y[i] = transcript_rows[i].accumulator_y; transcript_msm_x[i] = transcript_rows[i].msm_output_x; transcript_msm_y[i] = transcript_rows[i].msm_output_y; - transcript_collision_check[i] = transcript_rows[i].collision_check; + transcript_base_infinity[i] = transcript_rows[i].base_infinity; + transcript_base_x_inverse[i] = transcript_rows[i].base_x_inverse; + transcript_base_y_inverse[i] = transcript_rows[i].base_y_inverse; + transcript_add_x_equal[i] = transcript_rows[i].transcript_add_x_equal; + transcript_add_y_equal[i] = transcript_rows[i].transcript_add_y_equal; + transcript_add_lambda[i] = transcript_rows[i].transcript_add_lambda; + transcript_msm_intermediate_x[i] = transcript_rows[i].transcript_msm_intermediate_x; + transcript_msm_intermediate_y[i] = transcript_rows[i].transcript_msm_intermediate_y; + transcript_msm_infinity[i] = transcript_rows[i].transcript_msm_infinity; + transcript_msm_x_inverse[i] = transcript_rows[i].transcript_msm_x_inverse; + transcript_msm_count_zero_at_transition[i] = transcript_rows[i].msm_count_zero_at_transition; + transcript_msm_count_at_transition_inverse[i] = transcript_rows[i].msm_count_at_transition_inverse; } }); @@ -528,8 +563,13 @@ class ECCVMFlavor { transcript_accumulator_empty[i] = 1; } } + // in addition, unless the accumulator is reset, it contains the value from the previous row so this + // must be propagated + for (size_t i = transcript_rows.size(); i < dyadic_num_rows; ++i) { + transcript_accumulator_x[i] = transcript_accumulator_x[i - 1]; + transcript_accumulator_y[i] = transcript_accumulator_y[i - 1]; + } - // compute polynomials for point table columns run_loop_in_parallel(point_table_rows.size(), [&](size_t start, size_t end) { for (size_t i = start; i < end; i++) { // first row is always an empty row (to accommodate shifted polynomials which must have 0 as 1st @@ -669,7 +709,6 @@ class ECCVMFlavor { Base::transcript_add = "TRANSCRIPT_ADD"; Base::transcript_mul = "TRANSCRIPT_MUL"; Base::transcript_eq = "TRANSCRIPT_EQ"; - Base::transcript_collision_check = "TRANSCRIPT_COLLISION_CHECK"; Base::transcript_msm_transition = "TRANSCRIPT_MSM_TRANSITION"; Base::transcript_pc = "TRANSCRIPT_PC"; Base::transcript_msm_count = "TRANSCRIPT_MSM_COUNT"; @@ -740,6 +779,18 @@ class ECCVMFlavor { Base::precompute_select = "PRECOMPUTE_SELECT"; Base::lookup_read_counts_0 = "LOOKUP_READ_COUNTS_0"; Base::lookup_read_counts_1 = "LOOKUP_READ_COUNTS_1"; + Base::transcript_base_infinity = "TRANSCRIPT_BASE_INFINITY"; + Base::transcript_base_x_inverse = "TRANSCRIPT_BASE_X_INVERSE"; + Base::transcript_base_y_inverse = "TRANSCRIPT_BASE_Y_INVERSE"; + Base::transcript_add_x_equal = "TRANSCRIPT_ADD_X_EQUAL"; + Base::transcript_add_y_equal = "TRANSCRIPT_ADD_Y_EQUAL"; + Base::transcript_add_lambda = "TRANSCRIPT_ADD_LAMBDA"; + Base::transcript_msm_intermediate_x = "TRANSCRIPT_MSM_INTERMEDIATE_X"; + Base::transcript_msm_intermediate_y = "TRANSCRIPT_MSM_INTERMEDIATE_Y"; + Base::transcript_msm_infinity = "TRANSCRIPT_MSM_INFINITY"; + Base::transcript_msm_x_inverse = "TRANSCRIPT_MSM_X_INVERSE"; + Base::transcript_msm_count_zero_at_transition = "TRANSCRIPT_MSM_COUNT_ZERO_AT_TRANSITION"; + Base::transcript_msm_count_at_transition_inverse = "TRANSCRIPT_MSM_COUNT_AT_TRANSITION_INVERSE"; Base::z_perm = "Z_PERM"; Base::lookup_inverses = "LOOKUP_INVERSES"; // The ones beginning with "__" are only used for debugging @@ -769,7 +820,6 @@ class ECCVMFlavor { Commitment transcript_add_comm; Commitment transcript_mul_comm; Commitment transcript_eq_comm; - Commitment transcript_collision_check_comm; Commitment transcript_msm_transition_comm; Commitment transcript_pc_comm; Commitment transcript_msm_count_comm; @@ -840,6 +890,18 @@ class ECCVMFlavor { Commitment precompute_select_comm; Commitment lookup_read_counts_0_comm; Commitment lookup_read_counts_1_comm; + Commitment transcript_base_infinity_comm; + Commitment transcript_base_x_inverse_comm; + Commitment transcript_base_y_inverse_comm; + Commitment transcript_add_x_equal_comm; + Commitment transcript_add_y_equal_comm; + Commitment transcript_add_lambda_comm; + Commitment transcript_msm_intermediate_x_comm; + Commitment transcript_msm_intermediate_y_comm; + Commitment transcript_msm_infinity_comm; + Commitment transcript_msm_x_inverse_comm; + Commitment transcript_msm_count_zero_at_transition_comm; + Commitment transcript_msm_count_at_transition_inverse_comm; Commitment z_perm_comm; Commitment lookup_inverses_comm; std::vector> sumcheck_univariates; @@ -881,8 +943,6 @@ class ECCVMFlavor { NativeTranscript::proof_data, num_frs_read); transcript_eq_comm = NativeTranscript::template deserialize_from_buffer( NativeTranscript::proof_data, num_frs_read); - transcript_collision_check_comm = NativeTranscript::template deserialize_from_buffer( - NativeTranscript::proof_data, num_frs_read); transcript_msm_transition_comm = NativeTranscript::template deserialize_from_buffer( NativeTranscript::proof_data, num_frs_read); transcript_pc_comm = NativeTranscript::template deserialize_from_buffer( @@ -1023,6 +1083,32 @@ class ECCVMFlavor { NativeTranscript::proof_data, num_frs_read); lookup_read_counts_1_comm = NativeTranscript::template deserialize_from_buffer( NativeTranscript::proof_data, num_frs_read); + transcript_base_infinity_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_base_x_inverse_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_base_y_inverse_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_add_x_equal_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_add_y_equal_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_add_lambda_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_msm_intermediate_x_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_msm_intermediate_y_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_msm_infinity_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_msm_x_inverse_comm = NativeTranscript::template deserialize_from_buffer( + NativeTranscript::proof_data, num_frs_read); + transcript_msm_count_zero_at_transition_comm = + NativeTranscript::template deserialize_from_buffer(NativeTranscript::proof_data, + num_frs_read); + transcript_msm_count_at_transition_inverse_comm = + NativeTranscript::template deserialize_from_buffer(NativeTranscript::proof_data, + num_frs_read); lookup_inverses_comm = NativeTranscript::template deserialize_from_buffer( NativeTranscript::proof_data, num_frs_read); z_perm_comm = NativeTranscript::template deserialize_from_buffer(NativeTranscript::proof_data, @@ -1091,8 +1177,6 @@ class ECCVMFlavor { NativeTranscript::template serialize_to_buffer(transcript_add_comm, NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(transcript_mul_comm, NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(transcript_eq_comm, NativeTranscript::proof_data); - NativeTranscript::template serialize_to_buffer(transcript_collision_check_comm, - NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(transcript_msm_transition_comm, NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(transcript_pc_comm, NativeTranscript::proof_data); @@ -1167,6 +1251,25 @@ class ECCVMFlavor { NativeTranscript::template serialize_to_buffer(precompute_select_comm, NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(lookup_read_counts_0_comm, NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(lookup_read_counts_1_comm, NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_base_infinity_comm, NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_base_x_inverse_comm, + NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_base_y_inverse_comm, + NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_add_x_equal_comm, NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_add_y_equal_comm, NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_add_lambda_comm, NativeTranscript::proof_data); + + NativeTranscript::template serialize_to_buffer(transcript_msm_intermediate_x_comm, + NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_msm_intermediate_y_comm, + NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_msm_infinity_comm, NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_msm_x_inverse_comm, NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_msm_count_zero_at_transition_comm, + NativeTranscript::proof_data); + NativeTranscript::template serialize_to_buffer(transcript_msm_count_at_transition_inverse_comm, + NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(lookup_inverses_comm, NativeTranscript::proof_data); NativeTranscript::template serialize_to_buffer(z_perm_comm, NativeTranscript::proof_data); for (size_t i = 0; i < log_n; ++i) { diff --git a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_trace_checker.cpp b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_trace_checker.cpp index 24c440f3303..65c99f076ae 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_trace_checker.cpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_trace_checker.cpp @@ -66,6 +66,7 @@ bool ECCVMTraceChecker::check(Builder& builder, numeric::RNG* engine_ptr) result = result && evaluate_relation.template operator()>("ECCVMWnafRelation"); result = result && evaluate_relation.template operator()>("ECCVMMSMRelation"); result = result && evaluate_relation.template operator()>("ECCVMSetRelation"); + result = result && evaluate_relation.template operator()>("ECCVMBoolsRelation"); using LookupRelation = ECCVMLookupRelation; typename ECCVMLookupRelation::SumcheckArrayOfValuesOverSubrelations lookup_result; diff --git a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_transcript.test.cpp b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_transcript.test.cpp index 240f74bb0b9..0b2e13a7850 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_transcript.test.cpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_transcript.test.cpp @@ -45,7 +45,6 @@ class ECCVMTranscriptTests : public ::testing::Test { manifest_expected.add_entry(round, "TRANSCRIPT_ADD", frs_per_G); manifest_expected.add_entry(round, "TRANSCRIPT_MUL", frs_per_G); manifest_expected.add_entry(round, "TRANSCRIPT_EQ", frs_per_G); - manifest_expected.add_entry(round, "TRANSCRIPT_COLLISION_CHECK", frs_per_G); manifest_expected.add_entry(round, "TRANSCRIPT_MSM_TRANSITION", frs_per_G); manifest_expected.add_entry(round, "TRANSCRIPT_PC", frs_per_G); manifest_expected.add_entry(round, "TRANSCRIPT_MSM_COUNT", frs_per_G); @@ -116,6 +115,18 @@ class ECCVMTranscriptTests : public ::testing::Test { manifest_expected.add_entry(round, "PRECOMPUTE_SELECT", frs_per_G); manifest_expected.add_entry(round, "LOOKUP_READ_COUNTS_0", frs_per_G); manifest_expected.add_entry(round, "LOOKUP_READ_COUNTS_1", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_BASE_INFINITY", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_BASE_X_INVERSE", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_BASE_Y_INVERSE", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_ADD_X_EQUAL", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_ADD_Y_EQUAL", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_ADD_LAMBDA", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_MSM_INTERMEDIATE_X", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_MSM_INTERMEDIATE_Y", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_MSM_INFINITY", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_MSM_X_INVERSE", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_MSM_COUNT_ZERO_AT_TRANSITION", frs_per_G); + manifest_expected.add_entry(round, "TRANSCRIPT_MSM_COUNT_AT_TRANSITION_INVERSE", frs_per_G); manifest_expected.add_challenge(round, "beta", "gamma"); round++; diff --git a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_verifier.cpp b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_verifier.cpp index 6b9e01b7069..62415b77cc6 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/eccvm_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/eccvm_verifier.cpp @@ -31,7 +31,6 @@ bool ECCVMVerifier::verify_proof(const HonkProof& proof) commitments.transcript_add = receive_commitment(commitment_labels.transcript_add); commitments.transcript_mul = receive_commitment(commitment_labels.transcript_mul); commitments.transcript_eq = receive_commitment(commitment_labels.transcript_eq); - commitments.transcript_collision_check = receive_commitment(commitment_labels.transcript_collision_check); commitments.transcript_msm_transition = receive_commitment(commitment_labels.transcript_msm_transition); commitments.transcript_pc = receive_commitment(commitment_labels.transcript_pc); commitments.transcript_msm_count = receive_commitment(commitment_labels.transcript_msm_count); @@ -102,6 +101,20 @@ bool ECCVMVerifier::verify_proof(const HonkProof& proof) commitments.precompute_select = receive_commitment(commitment_labels.precompute_select); commitments.lookup_read_counts_0 = receive_commitment(commitment_labels.lookup_read_counts_0); commitments.lookup_read_counts_1 = receive_commitment(commitment_labels.lookup_read_counts_1); + commitments.transcript_base_infinity = receive_commitment(commitment_labels.transcript_base_infinity); + commitments.transcript_base_x_inverse = receive_commitment(commitment_labels.transcript_base_x_inverse); + commitments.transcript_base_y_inverse = receive_commitment(commitment_labels.transcript_base_y_inverse); + commitments.transcript_add_x_equal = receive_commitment(commitment_labels.transcript_add_x_equal); + commitments.transcript_add_y_equal = receive_commitment(commitment_labels.transcript_add_y_equal); + commitments.transcript_add_lambda = receive_commitment(commitment_labels.transcript_add_lambda); + commitments.transcript_msm_intermediate_x = receive_commitment(commitment_labels.transcript_msm_intermediate_x); + commitments.transcript_msm_intermediate_y = receive_commitment(commitment_labels.transcript_msm_intermediate_y); + commitments.transcript_msm_infinity = receive_commitment(commitment_labels.transcript_msm_infinity); + commitments.transcript_msm_x_inverse = receive_commitment(commitment_labels.transcript_msm_x_inverse); + commitments.transcript_msm_count_zero_at_transition = + receive_commitment(commitment_labels.transcript_msm_count_zero_at_transition); + commitments.transcript_msm_count_at_transition_inverse = + receive_commitment(commitment_labels.transcript_msm_count_at_transition_inverse); // Get challenge for sorted list batching and wire four memory records auto [beta, gamma] = transcript->template get_challenges("beta", "gamma"); diff --git a/barretenberg/cpp/src/barretenberg/eccvm/msm_builder.hpp b/barretenberg/cpp/src/barretenberg/eccvm/msm_builder.hpp index 69f4871eb91..006e21b7685 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/msm_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/msm_builder.hpp @@ -208,14 +208,15 @@ class ECCVMMSMMBuilder { // accumulator_trace tracks the value of the ECCVM accumulator for each row std::span accumulator_trace(&points_to_normalize[num_point_adds_and_doubles * 3], num_accumulators); - // we start the accumulator at the point at infinity - accumulator_trace[0] = (CycleGroup::affine_point_at_infinity); + // we start the accumulator at the offset generator point. This ensures we can support an MSM that produces a + constexpr auto offset_generator = bb::g1::derive_generators("ECCVM_OFFSET_GENERATOR", 1)[0]; + accumulator_trace[0] = offset_generator; // TODO(https://github.com/AztecProtocol/barretenberg/issues/973): Reinstate multitreading? // populate point trace, and the components of the MSM execution trace that do not relate to affine point // operations for (size_t msm_idx = 0; msm_idx < msms.size(); msm_idx++) { - Element accumulator = CycleGroup::affine_point_at_infinity; + Element accumulator = offset_generator; const auto& msm = msms[msm_idx]; size_t msm_row_index = msm_row_counts[msm_idx]; const size_t msm_size = msm.size(); @@ -252,20 +253,9 @@ class ECCVMMSMMBuilder { ? msm[offset + point_idx].precomputed_table[static_cast(add_state.slice)] : AffineElement{ 0, 0 }; - // predicate logic: - // add_predicate should normally equal add_state.add - // However! if digit_idx == 0 AND row_idx == 0 AND point_idx == 0 this implies we are - // examing the 1st point addition of a new MSM. In this case, we do NOT add the 1st point - // into the accumulator, instead we SET the accumulator to equal the 1st point. - // add_predicate is used to determine whether we add the output of a point addition into the - // accumulator, therefore if digit_idx == 0 AND row_idx == 0 AND point_idx == 0, - // add_predicate = 0 even if add_state.add = true - bool add_predicate = (point_idx == 0 ? (digit_idx != 0 || row_idx != 0) : add_state.add); - - Element p1 = (point_idx == 0) ? Element(add_state.point) : accumulator; - Element p2 = (point_idx == 0) ? accumulator : Element(add_state.point); - - accumulator = add_predicate ? (accumulator + add_state.point) : Element(p1); + Element p1(accumulator); + Element p2(add_state.point); + accumulator = add_state.add ? (accumulator + add_state.point) : Element(p1); p1_trace[trace_index] = p1; p2_trace[trace_index] = p2; p3_trace[trace_index] = accumulator; @@ -386,20 +376,16 @@ class ECCVMMSMMBuilder { for (size_t row_idx = 0; row_idx < num_rows_per_digit; ++row_idx) { auto& row = msm_rows[msm_row_index]; const Element& normalized_accumulator = accumulator_trace[accumulator_index]; - const FF& acc_x = normalized_accumulator.is_point_at_infinity() ? 0 : normalized_accumulator.x; - const FF& acc_y = normalized_accumulator.is_point_at_infinity() ? 0 : normalized_accumulator.y; - row.accumulator_x = acc_x; - row.accumulator_y = acc_y; - + ASSERT(normalized_accumulator.is_point_at_infinity() == 0); + row.accumulator_x = normalized_accumulator.x; + row.accumulator_y = normalized_accumulator.y; for (size_t point_idx = 0; point_idx < ADDITIONS_PER_ROW; ++point_idx) { auto& add_state = row.add_state[point_idx]; - bool add_predicate = (point_idx == 0 ? (digit_idx != 0 || row_idx != 0) : add_state.add); - const auto& inverse = inverse_trace[trace_index]; const auto& p1 = p1_trace[trace_index]; const auto& p2 = p2_trace[trace_index]; - add_state.collision_inverse = add_predicate ? inverse : 0; - add_state.lambda = add_predicate ? (p2.y - p1.y) * inverse : 0; + add_state.collision_inverse = add_state.add ? inverse : 0; + add_state.lambda = add_state.add ? (p2.y - p1.y) * inverse : 0; trace_index++; } accumulator_index++; @@ -427,11 +413,10 @@ class ECCVMMSMMBuilder { for (size_t row_idx = 0; row_idx < num_rows_per_digit; ++row_idx) { MSMRow& row = msm_rows[msm_row_index]; const Element& normalized_accumulator = accumulator_trace[accumulator_index]; + ASSERT(normalized_accumulator.is_point_at_infinity() == 0); const size_t offset = row_idx * ADDITIONS_PER_ROW; - const FF& acc_x = normalized_accumulator.is_point_at_infinity() ? 0 : normalized_accumulator.x; - const FF& acc_y = normalized_accumulator.is_point_at_infinity() ? 0 : normalized_accumulator.y; - row.accumulator_x = acc_x; - row.accumulator_y = acc_y; + row.accumulator_x = normalized_accumulator.x; + row.accumulator_y = normalized_accumulator.y; for (size_t point_idx = 0; point_idx < ADDITIONS_PER_ROW; ++point_idx) { auto& add_state = row.add_state[point_idx]; bool add_predicate = add_state.add ? msm[offset + point_idx].wnaf_skew : false; diff --git a/barretenberg/cpp/src/barretenberg/eccvm/transcript_builder.hpp b/barretenberg/cpp/src/barretenberg/eccvm/transcript_builder.hpp index b3d93d3d1f8..7bb6f8ede60 100644 --- a/barretenberg/cpp/src/barretenberg/eccvm/transcript_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/eccvm/transcript_builder.hpp @@ -31,13 +31,45 @@ class ECCVMTranscriptBuilder { FF accumulator_y = 0; FF msm_output_x = 0; FF msm_output_y = 0; - FF collision_check = 0; + bool base_infinity = 0; + FF base_x_inverse = 0; + FF base_y_inverse = 0; + bool transcript_add_x_equal = false; + bool transcript_add_y_equal = false; + FF transcript_add_lambda = 0; + FF transcript_msm_intermediate_x = 0; + FF transcript_msm_intermediate_y = 0; + bool transcript_msm_infinity = false; + FF transcript_msm_x_inverse = 0; + bool msm_count_zero_at_transition = false; + FF msm_count_at_transition_inverse = 0; }; + + /** + * @brief Computes offset_generator group element + * @details "offset generator" is used when performing multi-scalar-multiplications to ensure an HONEST prover never + * triggers incomplete point addition formulae. + * i.e. we don't need to constrain point doubling or points at infinity when computing an MSM + * The MSM accumulator is initialized to `offset_generator`. When adding the MSM result into the transcript + * accumulator, the contribution of the offset generator to the MSM result is removed (offset_generator * 2^{124}) + * @return AffineElement + */ + static AffineElement offset_generator() + { + static constexpr auto offset_generator_base = CycleGroup::derive_generators("ECCVM_OFFSET_GENERATOR", 1)[0]; + static const AffineElement result = + AffineElement(Element(offset_generator_base) * grumpkin::fq(uint256_t(1) << 124)); + return result; + } + static AffineElement remove_offset_generator(const AffineElement& other) + { + return AffineElement(Element(other) - offset_generator()); + } struct VMState { uint32_t pc = 0; uint32_t count = 0; - AffineElement accumulator = CycleGroup::affine_point_at_infinity; - AffineElement msm_accumulator = CycleGroup::affine_point_at_infinity; + Element accumulator = CycleGroup::affine_point_at_infinity; + Element msm_accumulator = offset_generator(); bool is_accumulator_empty = true; }; struct Opcode { @@ -61,14 +93,25 @@ class ECCVMTranscriptBuilder { const uint32_t total_number_of_muls) { const size_t num_transcript_entries = vm_operations.size() + 2; - + const size_t num_vm_entries = vm_operations.size(); std::vector transcript_state(num_transcript_entries); - std::vector inverse_trace(num_transcript_entries - 2); + + // These vectors track quantities that we need to invert. + // We fill these vectors and then perform batch inversions to amortize the cost of FF inverts + std::vector inverse_trace_x(num_vm_entries); + std::vector inverse_trace_y(num_vm_entries); + std::vector transcript_msm_x_inverse_trace(num_vm_entries); + std::vector add_lambda_denominator(num_vm_entries); + std::vector add_lambda_numerator(num_vm_entries); + std::vector msm_count_at_transition_inverse_trace(num_vm_entries); + std::vector msm_accumulator_trace(num_vm_entries); + std::vector accumulator_trace(num_vm_entries); + std::vector intermediate_accumulator_trace(num_vm_entries); VMState state{ .pc = total_number_of_muls, .count = 0, .accumulator = CycleGroup::affine_point_at_infinity, - .msm_accumulator = CycleGroup::affine_point_at_infinity, + .msm_accumulator = offset_generator(), .is_accumulator_empty = true, }; VMState updated_state; @@ -81,13 +124,20 @@ class ECCVMTranscriptBuilder { const bool is_mul = entry.mul; const bool z1_zero = (entry.mul) ? entry.z1 == 0 : true; const bool z2_zero = (entry.mul) ? entry.z2 == 0 : true; - const uint32_t num_muls = is_mul ? (static_cast(!z1_zero) + static_cast(!z2_zero)) : 0; - + uint32_t num_muls = 0; + auto base_point_infinity = entry.base_point.is_point_at_infinity(); + if (is_mul) { + num_muls = static_cast(!z1_zero) + static_cast(!z2_zero); + if (base_point_infinity) { + num_muls = 0; + } + } updated_state = state; if (entry.reset) { updated_state.is_accumulator_empty = true; - updated_state.msm_accumulator = CycleGroup::affine_point_at_infinity; + updated_state.accumulator = CycleGroup::point_at_infinity; + updated_state.msm_accumulator = offset_generator(); } updated_state.pc = state.pc - num_muls; @@ -97,38 +147,36 @@ class ECCVMTranscriptBuilder { // or next row is irrelevent and current row is a straight MUL bool next_not_msm = last_row ? true : !vm_operations[i + 1].mul; - bool msm_transition = entry.mul && next_not_msm; + bool msm_transition = entry.mul && next_not_msm && (state.count + num_muls > 0); // we reset the count in updated state if we are not accumulating and not doing an msm bool current_msm = entry.mul; bool current_ongoing_msm = entry.mul && !next_not_msm; updated_state.count = current_ongoing_msm ? state.count + num_muls : 0; - if (current_msm) { const auto P = typename CycleGroup::element(entry.base_point); const auto R = typename CycleGroup::element(state.msm_accumulator); updated_state.msm_accumulator = R + P * entry.mul_scalar_full; } - if (entry.mul && next_not_msm) { + if (msm_transition) { if (state.is_accumulator_empty) { - updated_state.accumulator = updated_state.msm_accumulator; + updated_state.accumulator = updated_state.msm_accumulator - offset_generator(); } else { const auto R = typename CycleGroup::element(state.accumulator); - updated_state.accumulator = R + updated_state.msm_accumulator; + updated_state.accumulator = R + updated_state.msm_accumulator - offset_generator(); } - updated_state.is_accumulator_empty = false; + updated_state.is_accumulator_empty = updated_state.accumulator.is_point_at_infinity(); } bool add_accumulate = entry.add; if (add_accumulate) { if (state.is_accumulator_empty) { - updated_state.accumulator = entry.base_point; } else { updated_state.accumulator = typename CycleGroup::element(state.accumulator) + entry.base_point; } - updated_state.is_accumulator_empty = false; + updated_state.is_accumulator_empty = updated_state.accumulator.is_point_at_infinity(); } row.accumulator_empty = state.is_accumulator_empty; row.q_add = entry.add; @@ -138,54 +186,142 @@ class ECCVMTranscriptBuilder { row.msm_transition = msm_transition; row.pc = state.pc; row.msm_count = state.count; - row.base_x = (entry.add || entry.mul || entry.eq) ? entry.base_point.x : 0; - row.base_y = (entry.add || entry.mul || entry.eq) ? entry.base_point.y : 0; + row.msm_count_zero_at_transition = ((state.count + num_muls) == 0) && (entry.mul && next_not_msm); + msm_count_at_transition_inverse_trace[i] = ((state.count + num_muls) == 0) ? 0 : FF(state.count + num_muls); + row.base_x = ((entry.add || entry.mul || entry.eq) && !base_point_infinity) ? entry.base_point.x : 0; + row.base_y = ((entry.add || entry.mul || entry.eq) && !base_point_infinity) ? entry.base_point.y : 0; + row.base_infinity = (entry.add || entry.mul || entry.eq) ? (base_point_infinity ? 1 : 0) : 0; + if (msm_transition) { + Element msm_output = updated_state.msm_accumulator - offset_generator(); + row.transcript_msm_infinity = msm_output.is_point_at_infinity(); + } + row.z1 = (entry.mul) ? entry.z1 : 0; row.z2 = (entry.mul) ? entry.z2 : 0; row.z1_zero = z1_zero; row.z2_zero = z2_zero; row.opcode = Opcode{ .add = entry.add, .mul = entry.mul, .eq = entry.eq, .reset = entry.reset }.value(); - row.accumulator_x = (state.accumulator.is_point_at_infinity()) ? 0 : state.accumulator.x; - row.accumulator_y = (state.accumulator.is_point_at_infinity()) ? 0 : state.accumulator.y; - row.msm_output_x = - msm_transition - ? (updated_state.msm_accumulator.is_point_at_infinity() ? 0 : updated_state.msm_accumulator.x) - : 0; - row.msm_output_y = - msm_transition - ? (updated_state.msm_accumulator.is_point_at_infinity() ? 0 : updated_state.msm_accumulator.y) - : 0; - + accumulator_trace[i] = state.accumulator; + msm_accumulator_trace[i] = msm_transition ? updated_state.msm_accumulator : Element::infinity(); + intermediate_accumulator_trace[i] = + msm_transition ? (updated_state.msm_accumulator - offset_generator()) : Element::infinity(); if (entry.mul && next_not_msm && !row.accumulator_empty) { - ASSERT((row.msm_output_x != row.accumulator_x) && - "eccvm: attempting msm. Result point x-coordinate matches accumulator x-coordinate."); - state.msm_accumulator = CycleGroup::affine_point_at_infinity; - inverse_trace[i] = (row.msm_output_x - row.accumulator_x); - } else if (entry.add && !row.accumulator_empty) { - ASSERT((row.base_x != row.accumulator_x) && - "eccvm: attempting to add points with matching x-coordinates"); - inverse_trace[i] = (row.base_x - row.accumulator_x); - } else { - inverse_trace[i] = (0); + state.msm_accumulator = offset_generator(); } state = updated_state; if (entry.mul && next_not_msm) { - state.msm_accumulator = CycleGroup::affine_point_at_infinity; + state.msm_accumulator = offset_generator(); } } + Element::batch_normalize(&accumulator_trace[0], accumulator_trace.size()); + Element::batch_normalize(&msm_accumulator_trace[0], msm_accumulator_trace.size()); + Element::batch_normalize(&intermediate_accumulator_trace[0], intermediate_accumulator_trace.size()); - FF::batch_invert(&inverse_trace[0], inverse_trace.size()); - for (size_t i = 0; i < inverse_trace.size(); ++i) { - transcript_state[i + 1].collision_check = inverse_trace[i]; + for (size_t i = 0; i < accumulator_trace.size(); ++i) { + if (!accumulator_trace[i].is_point_at_infinity()) { + transcript_state[i + 1].accumulator_x = accumulator_trace[i].x; + transcript_state[i + 1].accumulator_y = accumulator_trace[i].y; + } + if (!msm_accumulator_trace[i].is_point_at_infinity()) { + transcript_state[i + 1].msm_output_x = msm_accumulator_trace[i].x; + transcript_state[i + 1].msm_output_y = msm_accumulator_trace[i].y; + } + if (!intermediate_accumulator_trace[i].is_point_at_infinity()) { + transcript_state[i + 1].transcript_msm_intermediate_x = intermediate_accumulator_trace[i].x; + transcript_state[i + 1].transcript_msm_intermediate_y = intermediate_accumulator_trace[i].y; + } + } + for (size_t i = 0; i < accumulator_trace.size(); ++i) { + auto& row = transcript_state[i + 1]; + const bool msm_transition = row.msm_transition; + const bool add = row.q_add; + if (msm_transition) { + Element msm_output = intermediate_accumulator_trace[i]; + row.transcript_msm_infinity = msm_output.is_point_at_infinity(); + if (!row.transcript_msm_infinity) { + transcript_msm_x_inverse_trace[i] = (msm_accumulator_trace[i].x - offset_generator().x); + } else { + transcript_msm_x_inverse_trace[i] = 0; + } + auto lhsx = msm_output.is_point_at_infinity() ? 0 : msm_output.x; + auto lhsy = msm_output.is_point_at_infinity() ? 0 : msm_output.y; + auto rhsx = accumulator_trace[i].is_point_at_infinity() ? 0 : accumulator_trace[i].x; + auto rhsy = accumulator_trace[i].is_point_at_infinity() ? (0) : accumulator_trace[i].y; + inverse_trace_x[i] = lhsx - rhsx; + inverse_trace_y[i] = lhsy - rhsy; + } else if (add) { + auto lhsx = row.base_x; + auto lhsy = row.base_y; + auto rhsx = accumulator_trace[i].is_point_at_infinity() ? 0 : accumulator_trace[i].x; + auto rhsy = accumulator_trace[i].is_point_at_infinity() ? (0) : accumulator_trace[i].y; + inverse_trace_x[i] = lhsx - rhsx; + inverse_trace_y[i] = lhsy - rhsy; + } else { + inverse_trace_x[i] = 0; + inverse_trace_y[i] = 0; + } + // msm transition = current row is doing a lookup to validate output = msm output + // i.e. next row is not part of MSM and current row is part of MSM + // or next row is irrelevent and current row is a straight MUL + const bb::eccvm::VMOperation& entry = vm_operations[i]; + if (entry.add || msm_transition) { + Element lhs = entry.add ? Element(entry.base_point) : intermediate_accumulator_trace[i]; + Element rhs = accumulator_trace[i]; + FF lhs_y = lhs.y; + FF lhs_x = lhs.x; + FF rhs_y = rhs.y; + FF rhs_x = rhs.x; + if (rhs.is_point_at_infinity()) { + rhs_y = 0; + rhs_x = 0; + } + if (lhs.is_point_at_infinity()) { + lhs_y = 0; + lhs_x = 0; + } + row.transcript_add_x_equal = + lhs_x == rhs_x || (lhs.is_point_at_infinity() && rhs.is_point_at_infinity()); // check infinity? + row.transcript_add_y_equal = + lhs_y == rhs_y || (lhs.is_point_at_infinity() && rhs.is_point_at_infinity()); + if ((lhs_x == rhs_x) && (lhs_y == rhs_y) && !lhs.is_point_at_infinity() && + !rhs.is_point_at_infinity()) { + add_lambda_denominator[i] = lhs_y + lhs_y; + add_lambda_numerator[i] = lhs_x * lhs_x * 3; + } else if ((lhs_x != rhs_x) && !lhs.is_point_at_infinity() && !rhs.is_point_at_infinity()) { + add_lambda_denominator[i] = rhs_x - lhs_x; + add_lambda_numerator[i] = rhs_y - lhs_y; + } else { + add_lambda_numerator[i] = 0; + add_lambda_denominator[i] = 0; + } + } else { + row.transcript_add_x_equal = 0; + row.transcript_add_y_equal = 0; + add_lambda_numerator[i] = 0; + add_lambda_denominator[i] = 0; + } + } + FF::batch_invert(&inverse_trace_x[0], num_vm_entries); + FF::batch_invert(&inverse_trace_y[0], num_vm_entries); + FF::batch_invert(&transcript_msm_x_inverse_trace[0], num_vm_entries); + FF::batch_invert(&add_lambda_denominator[0], num_vm_entries); + FF::batch_invert(&msm_count_at_transition_inverse_trace[0], num_vm_entries); + for (size_t i = 0; i < num_vm_entries; ++i) { + transcript_state[i + 1].base_x_inverse = inverse_trace_x[i]; + transcript_state[i + 1].base_y_inverse = inverse_trace_y[i]; + transcript_state[i + 1].transcript_msm_x_inverse = transcript_msm_x_inverse_trace[i]; + transcript_state[i + 1].transcript_add_lambda = add_lambda_numerator[i] * add_lambda_denominator[i]; + transcript_state[i + 1].msm_count_at_transition_inverse = msm_count_at_transition_inverse_trace[i]; } TranscriptRow& final_row = transcript_state.back(); final_row.pc = updated_state.pc; - final_row.accumulator_x = (updated_state.accumulator.is_point_at_infinity()) ? 0 : updated_state.accumulator.x; - final_row.accumulator_y = (updated_state.accumulator.is_point_at_infinity()) ? 0 : updated_state.accumulator.y; + final_row.accumulator_x = + (updated_state.accumulator.is_point_at_infinity()) ? 0 : AffineElement(updated_state.accumulator).x; + final_row.accumulator_y = + (updated_state.accumulator.is_point_at_infinity()) ? 0 : AffineElement(updated_state.accumulator).y; final_row.accumulator_empty = updated_state.is_accumulator_empty; - return transcript_state; } }; diff --git a/barretenberg/cpp/src/barretenberg/goblin/goblin.hpp b/barretenberg/cpp/src/barretenberg/goblin/goblin.hpp index 61e8eb866f4..95f0ca86435 100644 --- a/barretenberg/cpp/src/barretenberg/goblin/goblin.hpp +++ b/barretenberg/cpp/src/barretenberg/goblin/goblin.hpp @@ -2,6 +2,7 @@ #include "barretenberg/eccvm/eccvm_circuit_builder.hpp" #include "barretenberg/eccvm/eccvm_prover.hpp" +#include "barretenberg/eccvm/eccvm_trace_checker.hpp" #include "barretenberg/eccvm/eccvm_verifier.hpp" #include "barretenberg/goblin/mock_circuits.hpp" #include "barretenberg/plonk_honk_shared/instance_inspector.hpp" diff --git a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_bools_relation.cpp b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_bools_relation.cpp new file mode 100644 index 00000000000..6d765c8a3c4 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_bools_relation.cpp @@ -0,0 +1,74 @@ +#include +#include + +#include "./ecc_bools_relation.hpp" +#include "barretenberg/eccvm/eccvm_flavor.hpp" +#include "barretenberg/flavor/relation_definitions.hpp" + +namespace bb { + +/** + * @brief ECCVMBoolsRelationImpl evaluates the correctness of ECCVM boolean checks + * + * @details There are a lot of columns in ECCVM that are boolean. As these are all low-degree we place them in a + * separate relation class + * @tparam FF + * @tparam ContainerOverSubrelations + * @tparam AllEntities + * @tparam Parameters + */ +template +template +void ECCVMBoolsRelationImpl::accumulate(ContainerOverSubrelations& accumulator, + const AllEntities& in, + const Parameters& /*unused*/, + const FF& scaling_factor) +{ + using Accumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>; + using View = typename Accumulator::View; + + auto z1_zero = View(in.transcript_z1zero); + auto z2_zero = View(in.transcript_z2zero); + auto msm_count_zero_at_transition = View(in.transcript_msm_count_zero_at_transition); + auto q_add = View(in.transcript_add); + auto q_mul = View(in.transcript_mul); + auto q_eq = View(in.transcript_eq); + auto transcript_msm_transition = View(in.transcript_msm_transition); + auto is_accumulator_empty = View(in.transcript_accumulator_empty); + auto q_reset_accumulator = View(in.transcript_reset_accumulator); + auto transcript_Pinfinity = View(in.transcript_base_infinity); + auto transcript_msm_infinity = View(in.transcript_msm_infinity); + auto transcript_add_x_equal = View(in.transcript_add_x_equal); + auto transcript_add_y_equal = View(in.transcript_add_y_equal); + auto precompute_point_transition = View(in.precompute_point_transition); + auto msm_transition = View(in.msm_transition); + auto msm_add = View(in.msm_add); + auto msm_double = View(in.msm_double); + auto msm_skew = View(in.msm_skew); + auto precompute_select = View(in.precompute_select); + + std::get<0>(accumulator) += q_eq * (q_eq - 1) * scaling_factor; + std::get<1>(accumulator) += q_add * (q_add - 1) * scaling_factor; + std::get<2>(accumulator) += q_mul * (q_mul - 1) * scaling_factor; + std::get<3>(accumulator) += q_reset_accumulator * (q_reset_accumulator - 1) * scaling_factor; + std::get<4>(accumulator) += transcript_msm_transition * (transcript_msm_transition - 1) * scaling_factor; + std::get<5>(accumulator) += is_accumulator_empty * (is_accumulator_empty - 1) * scaling_factor; + std::get<6>(accumulator) += z1_zero * (z1_zero - 1) * scaling_factor; + std::get<7>(accumulator) += z2_zero * (z2_zero - 1) * scaling_factor; + std::get<8>(accumulator) += transcript_add_x_equal * (transcript_add_x_equal - 1) * scaling_factor; + std::get<9>(accumulator) += transcript_add_y_equal * (transcript_add_y_equal - 1) * scaling_factor; + std::get<10>(accumulator) += transcript_Pinfinity * (transcript_Pinfinity - 1) * scaling_factor; + std::get<11>(accumulator) += transcript_msm_infinity * (transcript_msm_infinity - 1) * scaling_factor; + std::get<12>(accumulator) += msm_count_zero_at_transition * (msm_count_zero_at_transition - 1) * scaling_factor; + std::get<13>(accumulator) += msm_transition * (msm_transition - 1) * scaling_factor; + std::get<14>(accumulator) += precompute_point_transition * (precompute_point_transition - 1) * scaling_factor; + std::get<15>(accumulator) += msm_add * (msm_add - 1) * scaling_factor; + std::get<16>(accumulator) += msm_double * (msm_double - 1) * scaling_factor; + std::get<17>(accumulator) += msm_skew * (msm_skew - 1) * scaling_factor; + std::get<18>(accumulator) += precompute_select * (precompute_select - 1) * scaling_factor; +} + +template class ECCVMBoolsRelationImpl; +DEFINE_SUMCHECK_RELATION_CLASS(ECCVMBoolsRelationImpl, ECCVMFlavor); + +} // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_bools_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_bools_relation.hpp new file mode 100644 index 00000000000..88d6eef5dc8 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_bools_relation.hpp @@ -0,0 +1,33 @@ +#pragma once + +#include "barretenberg/ecc/curves/bn254/g1.hpp" +#include "barretenberg/ecc/curves/grumpkin/grumpkin.hpp" +#include "barretenberg/relations/relation_types.hpp" + +namespace bb { + +/** + * @brief ECCVMBoolsRelationImpl evaluates the correctness of ECCVM boolean checks + * + * @details There are a lot of columns in ECCVM that are boolean. As these are all low-degree we place them in a + * separate relation class + * @tparam FF + */ +template class ECCVMBoolsRelationImpl { + public: + using FF = FF_; + + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + }; + + template + static void accumulate(ContainerOverSubrelations& accumulator, + const AllEntities& in, + const Parameters& /* unused */, + const FF& scaling_factor); +}; + +template using ECCVMBoolsRelation = Relation>; + +} // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation.cpp b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation.cpp index 51dc6851d75..61e64a7641e 100644 --- a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation.cpp +++ b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_msm_relation.cpp @@ -176,7 +176,6 @@ void ECCVMMSMRelationImpl::accumulate(ContainerOverSubrelations& accumulator auto& selector, auto& relation, auto& collision_relation) { - // (L * (xb - xa) - yb - ya) * s = 0 // L * (1 - s) = 0 // (combine) (L * (xb - xa - 1) - yb - ya) * s + L = 0 relation += selector * (lambda * (xb - xa - 1) - (yb - ya)) + lambda; @@ -189,6 +188,43 @@ void ECCVMMSMRelationImpl::accumulate(ContainerOverSubrelations& accumulator return std::array{ x_out, y_out }; }; + /** + * @brief First Addition relation + * + * The first add operation per row is treated differently. + * Normally we add the point xa/ya with an accumulator xb/yb, + * BUT, if this row STARTS a multiscalar multiplication, + * We need to add the point xa/ya with the "offset generator point" xo/yo + * The offset generator point's purpose is to ensure that no intermediate computations in the MSM will produce + * points at infinity, for an honest Prover. + * (we ensure soundness by validating the x-coordinates of xa/xb are not the same i.e. incomplete addition formula + * edge cases have not been hit) + * Note: this technique is only statistically complete, as there is a chance of an honest Prover creating a + * collision, but this probability is equivalent to solving the discrete logarithm problem + */ + auto first_add = [&](auto& xb, + auto& yb, + auto& xa, + auto& ya, + auto& lambda, + auto& selector, + auto& relation, + auto& collision_relation) { + // N.B. this is brittle - should be curve agnostic but we don't propagate the curve parameter into relations! + constexpr auto offset_generator = bb::g1::derive_generators("ECCVM_OFFSET_GENERATOR", 1)[0]; + constexpr uint256_t oxu = offset_generator.x; + constexpr uint256_t oyu = offset_generator.y; + const Accumulator xo(oxu); + const Accumulator yo(oyu); + + auto x = xo * selector + xb * (-selector + 1); + auto y = yo * selector + yb * (-selector + 1); + relation += lambda * (x - xa) - (y - ya); // degree 3 + collision_relation += (xa - x); + auto x_out = lambda * lambda + (-x - xa); + auto y_out = lambda * (xa - x_out) - ya; + return std::array{ x_out, y_out }; + }; // ADD operations (if row represents ADD round, not SKEW or DOUBLE) Accumulator add_relation(0); Accumulator x1_collision_relation(0); @@ -197,8 +233,7 @@ void ECCVMMSMRelationImpl::accumulate(ContainerOverSubrelations& accumulator Accumulator x4_collision_relation(0); // If msm_transition = 1, we have started a new MSM. We need to treat the current value of [Acc] as the point at // infinity! - auto add_into_accumulator = -msm_transition + 1; - auto [x_t1, y_t1] = add(acc_x, acc_y, x1, y1, lambda1, add_into_accumulator, add_relation, x1_collision_relation); + auto [x_t1, y_t1] = first_add(acc_x, acc_y, x1, y1, lambda1, msm_transition, add_relation, x1_collision_relation); auto [x_t2, y_t2] = add(x2, y2, x_t1, y_t1, lambda2, add2, add_relation, x2_collision_relation); auto [x_t3, y_t3] = add(x3, y3, x_t2, y_t2, lambda3, add3, add_relation, x3_collision_relation); auto [x_t4, y_t4] = add(x4, y4, x_t3, y_t3, lambda4, add4, add_relation, x4_collision_relation); @@ -285,7 +320,7 @@ void ECCVMMSMRelationImpl::accumulate(ContainerOverSubrelations& accumulator // Check x-coordinates do not collide if row is an ADD row or a SKEW row // if either q_add or q_skew = 1, an inverse should exist for each computed relation // Step 1: construct boolean selectors that describe whether we added a point at the current row - const auto add_first_point = add_into_accumulator * q_add + q_skew * skew1_select; + const auto add_first_point = add1 * q_add + q_skew * skew1_select; const auto add_second_point = add2 * q_add + q_skew * skew2_select; const auto add_third_point = add3 * q_add + q_skew * skew3_select; const auto add_fourth_point = add4 * q_add + q_skew * skew4_select; diff --git a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.cpp b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.cpp index 3fa0e512058..078e512692d 100644 --- a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.cpp +++ b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.cpp @@ -294,6 +294,7 @@ Accumulator ECCVMSetRelationImpl::compute_grand_product_denominator(const Al auto z2 = View(in.transcript_z2); auto z1_zero = View(in.transcript_z1zero); auto z2_zero = View(in.transcript_z2zero); + auto base_infinity = View(in.transcript_base_infinity); auto transcript_mul = View(in.transcript_mul); auto lookup_first = (-z1_zero + 1); @@ -304,18 +305,25 @@ Accumulator ECCVMSetRelationImpl::compute_grand_product_denominator(const Al auto transcript_input2 = (transcript_pc - 1) + transcript_Px * endomorphism_base_field_shift * beta - transcript_Py * beta_sqr + z2 * beta_cube; - // | q_mul | z2_zero | z1_zero | lookup | - // | ----- | ------- | ------- | ---------------------- | - // | 0 | - | - | 1 | - // | 1 | 0 | 1 | X + gamma | - // | 1 | 1 | 0 | Y + gamma | - // | 1 | 1 | 1 | (X + gamma)(Y + gamma) | + // | q_mul | z2_zero | z1_zero | base_infinity | lookup | + // | ----- | ------- | ------- | ------------- |----------------------- | + // | 0 | - | - | - | 1 | + // | 1 | 0 | 0 | 0 | 1 | + // | 1 | 0 | 1 | 0 | X + gamma | + // | 1 | 1 | 0 | 0 | Y + gamma | + // | 1 | 1 | 1 | 0 | (X + gamma)(Y + gamma) | + // | 1 | 0 | 0 | 1 | 1 | + // | 1 | 0 | 1 | 1 | 1 | + // | 1 | 1 | 0 | 1 | 1 | + // | 1 | 1 | 1 | 1 | 1 | transcript_input1 = (transcript_input1 + gamma) * lookup_first + (-lookup_first + 1); transcript_input2 = (transcript_input2 + gamma) * lookup_second + (-lookup_second + 1); - // point_table_init_write = degree 2 + // transcript_product = degree 3 + auto transcript_product = (transcript_input1 * transcript_input2) * (-base_infinity + 1) + base_infinity; - auto point_table_init_write = transcript_mul * transcript_input1 * transcript_input2 + (-transcript_mul + 1); - denominator *= point_table_init_write; // degree-13 + // point_table_init_write = degree 4 + auto point_table_init_write = transcript_mul * transcript_product + (-transcript_mul + 1); + denominator *= point_table_init_write; // degree-14 // auto point_table_init_write_1 = transcript_mul * transcript_input1 + (-transcript_mul + 1); // denominator *= point_table_init_write_1; // degree-11 @@ -339,15 +347,16 @@ Accumulator ECCVMSetRelationImpl::compute_grand_product_denominator(const Al auto z1_zero = View(in.transcript_z1zero); auto z2_zero = View(in.transcript_z2zero); auto transcript_mul = View(in.transcript_mul); + auto base_infinity = View(in.transcript_base_infinity); - auto full_msm_count = transcript_msm_count + transcript_mul * ((-z1_zero + 1) + (-z2_zero + 1)); - // auto count_test = transcript_msm_count + // do not add to count if point at infinity! + auto full_msm_count = + transcript_msm_count + transcript_mul * ((-z1_zero + 1) + (-z2_zero + 1)) * (-base_infinity + 1); // msm_result_read = degree 2 auto msm_result_read = transcript_pc_shift + transcript_msm_x * beta + transcript_msm_y * beta_sqr + full_msm_count * beta_cube; - msm_result_read = transcript_msm_transition * (msm_result_read + gamma) + (-transcript_msm_transition + 1); - denominator *= msm_result_read; // degree-17 + denominator *= msm_result_read; // degree-20 } return denominator; } diff --git a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.hpp index 44fd632dee9..2e8393cd661 100644 --- a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_set_relation.hpp @@ -14,8 +14,8 @@ template class ECCVMSetRelationImpl { using FF = FF_; static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 19, // grand product construction sub-relation - 19 // left-shiftable polynomial sub-relation + 21, // grand product construction sub-relation + 21 // left-shiftable polynomial sub-relation }; template static Accumulator convert_to_wnaf(const auto& s0, const auto& s1) diff --git a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.cpp b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.cpp index b2d0f2cedbd..47a0a3f8731 100644 --- a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.cpp +++ b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.cpp @@ -39,6 +39,16 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu using Accumulator = typename std::tuple_element_t<0, ContainerOverSubrelations>; using View = typename Accumulator::View; + static const auto offset_generator = [&]() { + static constexpr auto offset_generator_base = bb::g1::derive_generators("ECCVM_OFFSET_GENERATOR", 1)[0]; + static bb::g1::affine_element result = + bb::g1::affine_element(bb::g1::element(offset_generator_base) * grumpkin::fq(uint256_t(1) << 124)); + static const FF qx = result.x; + static const FF qy = result.y; + static const Accumulator ox(qx); + static const Accumulator oy(qy); + return std::array{ ox, oy }; + }; auto z1 = View(in.transcript_z1); auto z2 = View(in.transcript_z2); auto z1_zero = View(in.transcript_z1zero); @@ -57,8 +67,8 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu auto transcript_accumulator_y_shift = View(in.transcript_accumulator_y_shift); auto transcript_accumulator_x = View(in.transcript_accumulator_x); auto transcript_accumulator_y = View(in.transcript_accumulator_y); - auto transcript_msm_x = View(in.transcript_msm_x); - auto transcript_msm_y = View(in.transcript_msm_y); + auto transcript_msm_x = View(in.transcript_msm_intermediate_x); + auto transcript_msm_y = View(in.transcript_msm_intermediate_y); auto transcript_Px = View(in.transcript_Px); auto transcript_Py = View(in.transcript_Py); auto is_accumulator_empty = View(in.transcript_accumulator_empty); @@ -67,10 +77,18 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu auto is_accumulator_empty_shift = View(in.transcript_accumulator_empty_shift); auto q_reset_accumulator = View(in.transcript_reset_accumulator); auto lagrange_second = View(in.lagrange_second); - auto transcript_collision_check = View(in.transcript_collision_check); + auto transcript_Pinfinity = View(in.transcript_base_infinity); + auto transcript_Px_inverse = View(in.transcript_base_x_inverse); + auto transcript_Py_inverse = View(in.transcript_base_y_inverse); + auto transcript_add_x_equal = View(in.transcript_add_x_equal); + auto transcript_add_y_equal = View(in.transcript_add_y_equal); + auto transcript_add_lambda = View(in.transcript_add_lambda); + auto transcript_msm_infinity = View(in.transcript_msm_infinity); auto is_not_first_row = (-lagrange_first + 1); + auto is_not_last_row = (-lagrange_last + 1); auto is_not_first_or_last_row = (-lagrange_first + -lagrange_last + 1); + auto is_not_infinity = (-transcript_Pinfinity + 1); /** * @brief Validate correctness of z1_zero, z2_zero. * If z1_zero = 0 and operation is a MUL, we will write a scalar mul instruction into our multiplication table. @@ -82,8 +100,8 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu * this will add a scalar mul instruction into the multiplication table, where the scalar multiplier is 0. * This is inefficient but will still produce the correct output. */ - std::get<0>(accumulator) += (z1 * z1_zero) * scaling_factor; // if z1_zero = 1, z1 must be 0 - std::get<1>(accumulator) += (z2 * z2_zero) * scaling_factor; + std::get<0>(accumulator) += (z1 * z1_zero) * scaling_factor; // if z1_zero = 1, z1 must be 0. degree 2 + std::get<1>(accumulator) += (z2 * z2_zero) * scaling_factor; // degree 2 /** * @brief Validate `op` opcode is well formed. @@ -97,7 +115,7 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu tmp += q_eq; tmp += tmp; tmp += q_reset_accumulator; - std::get<2>(accumulator) += (tmp - op) * scaling_factor; + std::get<2>(accumulator) += (tmp - op) * scaling_factor; // degree 1 /** * @brief Validate `pc` is updated correctly. @@ -106,17 +124,32 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu * @note pc starts out at its max value and decrements down to 0. This keeps the degree of the pc polynomial smol */ Accumulator pc_delta = pc - pc_shift; - std::get<3>(accumulator) += - is_not_first_row * (pc_delta - q_mul * ((-z1_zero + 1) + (-z2_zero + 1))) * scaling_factor; + auto num_muls_in_row = ((-z1_zero + 1) + (-z2_zero + 1)) * (-transcript_Pinfinity + 1); + std::get<3>(accumulator) += is_not_first_row * (pc_delta - q_mul * num_muls_in_row) * scaling_factor; // degree 4 /** * @brief Validate `msm_transition` is well-formed. * * If the current row is the last mul instruction in a multiscalar multiplication, msm_transition = 1. * i.e. if q_mul == 1 and q_mul_shift == 0, msm_transition = 1, else is 0 + * We also require that `msm_count + [current msm number] > 0` */ - auto msm_transition_check = q_mul * (-q_mul_shift + 1); - std::get<4>(accumulator) += (msm_transition - msm_transition_check) * scaling_factor; + auto msm_transition_check = q_mul * (-q_mul_shift + 1); // degree 2 + // auto num_muls_total = msm_count + num_muls_in_row; + auto msm_count_zero_at_transition = View(in.transcript_msm_count_zero_at_transition); + auto msm_count_at_transition_inverse = View(in.transcript_msm_count_at_transition_inverse); + + auto msm_count_total = msm_count + num_muls_in_row; // degree 3 + + auto msm_count_zero_at_transition_check = msm_count_zero_at_transition * msm_count_total; + msm_count_zero_at_transition_check += + (msm_count_total * msm_count_at_transition_inverse - 1) * (-msm_count_zero_at_transition + 1); + std::get<4>(accumulator) += msm_transition_check * msm_count_zero_at_transition_check * scaling_factor; // degree 3 + + // Validate msm_transition_msm_count is correct + // ensure msm_transition is zero if count is zero + std::get<5>(accumulator) += + (msm_transition - msm_transition_check * (-msm_count_zero_at_transition + 1)) * scaling_factor; // degree 3 /** * @brief Validate `msm_count` resets when we end a multiscalar multiplication. @@ -124,7 +157,7 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu * (if no msm active, msm_count == 0) * If current row ends an MSM, `msm_count_shift = 0` (msm_count value at next row) */ - std::get<5>(accumulator) += (msm_transition * msm_count_shift) * scaling_factor; + std::get<6>(accumulator) += (msm_transition * msm_count_shift) * scaling_factor; // degree 2 /** * @brief Validate `msm_count` updates correctly for mul operations. @@ -132,96 +165,36 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu * row). */ auto msm_count_delta = msm_count_shift - msm_count; // degree 4 - std::get<6>(accumulator) += is_not_first_row * (-msm_transition + 1) * - (msm_count_delta - q_mul * ((-z1_zero + 1) + (-z2_zero + 1))) * scaling_factor; - - /** - * @brief Add multiscalar multiplication result into transcript accumulator. - * If `msm_transition == 1`, we expect msm output to be present on (transcript_msm_x, transcript_msm_y). - * (this is enforced via a lookup protocol). - * If `is_accumulator_empty == 0`, we ADD msm output into transcript_accumulator. - * If `is_accumulator_empty = =1`, we ASSIGN msm output to transcript_accumulator. - * @note the output of an msm cannot be point at infinity (will create unsatisfiable constraints in - * ecc_msm_relation). We assume this does not affect statistical completeness for honest provers. We should validate - * this! - */ - auto add_msm_into_accumulator = msm_transition * (-is_accumulator_empty + 1); - auto x3 = transcript_accumulator_x_shift; - auto y3 = transcript_accumulator_y_shift; - auto x1 = transcript_accumulator_x; - auto y1 = transcript_accumulator_y; - auto x2 = transcript_msm_x; - auto y2 = transcript_msm_y; - auto tmpx = (x3 + x2 + x1) * (x2 - x1).sqr() - (y2 - y1).sqr(); - auto tmpy = (y3 + y1) * (x2 - x1) - (y2 - y1) * (x1 - x3); - std::get<7>(accumulator) += tmpx * add_msm_into_accumulator * scaling_factor; // degree 5 - std::get<8>(accumulator) += tmpy * add_msm_into_accumulator * scaling_factor; // degree 4 - - /** - * @brief If is_accumulator_empty == 1, assign transcript_accumulator output into accumulator - * - * @note The accumulator point for all operations at row `i` is the accumulator point at row `i + 1`! - */ - auto assign_msm_into_accumulator = msm_transition * is_accumulator_empty; - std::get<9>(accumulator) += assign_msm_into_accumulator * (x3 - x2) * scaling_factor; // degree 3 - std::get<10>(accumulator) += assign_msm_into_accumulator * (y3 - y2) * scaling_factor; - - /** - * @brief Constrain `add` opcode. - * - * add will add the input point in (transcript_Px, transcript_Py) into the accumulator. - * Correctly handles case where accumulator is point at infinity. - * TODO: need to add constraints to rule out point doubling case (x2 != x1) - * TODO: need to assert input point is on the curve! - */ - x2 = transcript_Px; - y2 = transcript_Py; - auto add_into_accumulator = q_add * (-is_accumulator_empty + 1); - tmpx = (x3 + x2 + x1) * (x2 - x1).sqr() - (y2 - y1).sqr(); - tmpy = (y3 + y1) * (x2 - x1) - (y2 - y1) * (x1 - x3); - std::get<11>(accumulator) += tmpx * add_into_accumulator * scaling_factor; // degree 5 - std::get<12>(accumulator) += tmpy * add_into_accumulator * scaling_factor; // degree 4 - auto assign_into_accumulator = q_add * is_accumulator_empty; - std::get<13>(accumulator) += (x3 - x2) * assign_into_accumulator * scaling_factor; // degree 3 - std::get<14>(accumulator) += (y3 - y2) * assign_into_accumulator * scaling_factor; + auto num_counts = ((-z1_zero + 1) + (-z2_zero + 1)) * (-transcript_Pinfinity + 1); + std::get<7>(accumulator) += + is_not_first_row * (-msm_transition + 1) * (msm_count_delta - q_mul * (num_counts)) * scaling_factor; /** * @brief Opcode exclusion tests. We have the following assertions: * 1. If q_mul = 1, (q_add, eq, reset) are zero - * 2. If q_reset = 1, is_accumulator_empty at next row = 1 - * 3. If q_add = 1 OR msm_transition = 1, is_accumulator_empty at next row = 0 - * 4. If q_add = 0 AND msm_transition = 0 AND q_reset_accumulator = 0, is_accumulator at next row = current row - * value - * @note point 3: both q_add = 1, msm_transition = 1 cannot occur because of point 1 (msm_transition only 1 when - * q_mul 1) we can use a slightly more efficient relation than a pure binary OR + * 2. If q_add = 1, (q_mul, eq, reset) are zero + * 3. If q_eq = 1, (q_add, q_mul) are zero (is established by previous 2 checks) */ - std::get<15>(accumulator) += q_mul * (q_add + q_eq + q_reset_accumulator) * scaling_factor; - std::get<16>(accumulator) += q_add * (q_mul + q_eq + q_reset_accumulator) * scaling_factor; - std::get<17>(accumulator) += q_reset_accumulator * (-is_accumulator_empty_shift + 1) * scaling_factor; - std::get<18>(accumulator) += (q_add + msm_transition) * is_accumulator_empty_shift * scaling_factor; - auto accumulator_state_not_modified = -(q_add + msm_transition + q_reset_accumulator) + 1; - std::get<19>(accumulator) += accumulator_state_not_modified * is_not_first_or_last_row * - (is_accumulator_empty_shift - is_accumulator_empty) * scaling_factor; + auto opcode_exclusion_relation = q_mul * (q_add + q_eq + q_reset_accumulator); + opcode_exclusion_relation += q_add * (q_mul + q_eq + q_reset_accumulator); + std::get<8>(accumulator) += opcode_exclusion_relation * scaling_factor; // degree 2 /** * @brief `eq` opcode. - * If eq = 1, assert transcript_Px/y = transcript_accumulator_x/y. - * If eq = 1, assert is_accumulator_empty = 0 (input point cannot be point at infinity) - */ - std::get<20>(accumulator) += q_eq * (transcript_accumulator_x - transcript_Px) * scaling_factor; - std::get<21>(accumulator) += - q_eq * (-is_accumulator_empty + 1) * (transcript_accumulator_y - transcript_Py) * scaling_factor; - std::get<22>(accumulator) += q_eq * is_accumulator_empty * scaling_factor; - - // validate selectors are boolean (put somewhere else? these are low degree) - std::get<23>(accumulator) += (q_eq.sqr() - q_eq) * scaling_factor; - std::get<24>(accumulator) += (q_add.sqr() - q_add) * scaling_factor; - std::get<25>(accumulator) += (q_mul.sqr() - q_mul) * scaling_factor; - std::get<26>(accumulator) += (q_reset_accumulator.sqr() - q_reset_accumulator) * scaling_factor; - std::get<27>(accumulator) += (msm_transition.sqr() - msm_transition) * scaling_factor; - std::get<28>(accumulator) += (is_accumulator_empty.sqr() - is_accumulator_empty) * scaling_factor; - std::get<29>(accumulator) += (z1_zero.sqr() - z1_zero) * scaling_factor; - std::get<30>(accumulator) += (z2_zero.sqr() - z2_zero) * scaling_factor; + * Let lhs = transcript_P and rhs = transcript_accumulator + * If eq = 1, we must validate the following cases: + * IF lhs and rhs are not at infinity THEN lhs == rhs + * ELSE lhs and rhs are BOTH points at infinity + **/ + auto both_infinity = transcript_Pinfinity * is_accumulator_empty; + auto both_not_infinity = (-transcript_Pinfinity + 1) * (-is_accumulator_empty + 1); + auto infinity_exclusion_check = transcript_Pinfinity + is_accumulator_empty - both_infinity - both_infinity; + auto eq_x_diff = transcript_Px - transcript_accumulator_x; + auto eq_y_diff = transcript_Py - transcript_accumulator_y; + auto eq_x_diff_relation = q_eq * (eq_x_diff * both_not_infinity + infinity_exclusion_check); // degree 4 + auto eq_y_diff_relation = q_eq * (eq_y_diff * both_not_infinity + infinity_exclusion_check); // degree 4 + std::get<9>(accumulator) += eq_x_diff_relation * scaling_factor; // degree 4 + std::get<10>(accumulator) += eq_y_diff_relation * scaling_factor; // degree 4 /** * @brief Initial condition check on 1st row. @@ -231,28 +204,229 @@ void ECCVMTranscriptRelationImpl::accumulate(ContainerOverSubrelations& accu * note...actually second row? bleurgh * NOTE: we want pc = 0 at lagrange_last :o */ - std::get<31>(accumulator) += lagrange_second * (-is_accumulator_empty + 1) * scaling_factor; - std::get<32>(accumulator) += lagrange_second * msm_count * scaling_factor; + std::get<11>(accumulator) += lagrange_second * (-is_accumulator_empty + 1) * scaling_factor; // degree 2 + std::get<12>(accumulator) += lagrange_second * msm_count * scaling_factor; // degree 2 /** * @brief On-curve validation checks. * If q_mul = 1 OR q_add = 1 OR q_eq = 1, require (transcript_Px, transcript_Py) is valid ecc point * q_mul/q_add/q_eq mutually exclusive, can represent as sum of 3 */ - const auto validate_on_curve = q_mul; // q_add + q_mul + q_eq; + const auto validate_on_curve = q_mul + q_add + q_mul + q_eq; const auto on_curve_check = transcript_Py * transcript_Py - transcript_Px * transcript_Px * transcript_Px - get_curve_b(); - std::get<33>(accumulator) += validate_on_curve * on_curve_check * scaling_factor; + std::get<13>(accumulator) += validate_on_curve * on_curve_check * is_not_infinity * scaling_factor; // degree 6 /** - * @brief If performing an add, validate x-coordintes of inputs do not collide. - * If adding msm output into accumulator, validate x-coordinates of inputs do not collide + * @brief Validate relations from ECC Group Operations are well formed + * */ - auto x_coordinate_collision_check = - add_msm_into_accumulator * ((transcript_msm_x - transcript_accumulator_x) * transcript_collision_check - FF(1)); - x_coordinate_collision_check += - add_into_accumulator * ((transcript_Px - transcript_accumulator_x) * transcript_collision_check - FF(1)); - std::get<34>(accumulator) += x_coordinate_collision_check * scaling_factor; + { + Accumulator transcript_lambda_relation(0); + auto is_double = transcript_add_x_equal * transcript_add_y_equal; + auto is_add = (-transcript_add_x_equal + 1); + auto add_result_is_infinity = transcript_add_x_equal * (-transcript_add_y_equal + 1); // degree 2 + auto rhs_x = transcript_accumulator_x; + auto rhs_y = transcript_accumulator_y; + auto out_x = transcript_accumulator_x_shift; + auto out_y = transcript_accumulator_y_shift; + auto lambda = transcript_add_lambda; + auto lhs_x = transcript_Px * q_add + transcript_msm_x * msm_transition; + auto lhs_y = transcript_Py * q_add + transcript_msm_y * msm_transition; + auto lhs_infinity = transcript_Pinfinity * q_add + transcript_msm_infinity * msm_transition; + auto rhs_infinity = is_accumulator_empty; + auto result_is_lhs = rhs_infinity * (-lhs_infinity + 1); // degree 2 + auto result_is_rhs = (-rhs_infinity + 1) * lhs_infinity; // degree 2 + auto result_infinity_from_inputs = lhs_infinity * rhs_infinity; // degree 2 + auto result_infinity_from_operation = transcript_add_x_equal * (-transcript_add_y_equal + 1); // degree 2 + // infinity_from_inputs and infinity_from_operation mutually exclusive so we can perform an OR by adding + // (mutually exclusive because if result_infinity_from_inputs then transcript_add_y_equal = 1 (both y are 0) + auto result_is_infinity = result_infinity_from_inputs + result_infinity_from_operation; // degree 2 + auto any_add_is_active = q_add + msm_transition; + + // Valdiate `transcript_add_lambda` is well formed if we are adding msm output into accumulator + { + Accumulator transcript_msm_lambda_relation(0); + auto msm_x = transcript_msm_x; + auto msm_y = transcript_msm_y; + // Group operation is point addition + { + auto lambda_denominator = (rhs_x - msm_x); + auto lambda_numerator = (rhs_y - msm_y); + auto lambda_relation = lambda * lambda_denominator - lambda_numerator; // degree 2 + transcript_msm_lambda_relation += lambda_relation * is_add; // degree 3 + } + // Group operation is point doubling + { + auto lambda_denominator = msm_y + msm_y; + auto lambda_numerator = msm_x * msm_x * 3; + auto lambda_relation = lambda * lambda_denominator - lambda_numerator; // degree 2 + transcript_msm_lambda_relation += lambda_relation * is_double; // degree 4 + } + auto transcript_add_or_dbl_from_msm_output_is_valid = + (-transcript_msm_infinity + 1) * (-is_accumulator_empty + 1); // degree 2 + transcript_msm_lambda_relation *= transcript_add_or_dbl_from_msm_output_is_valid; // degree 6 + // No group operation because of points at infinity + { + auto lambda_relation_invalid = + (transcript_msm_infinity + is_accumulator_empty + add_result_is_infinity); // degree 2 + auto lambda_relation = lambda * lambda_relation_invalid; // degree 4 + transcript_msm_lambda_relation += lambda_relation; // (still degree 6) + } + transcript_lambda_relation = transcript_msm_lambda_relation * msm_transition; // degree 7 + } + // Valdiate `transcript_add_lambda` is well formed if we are adding base point into accumulator + { + Accumulator transcript_add_lambda_relation(0); + auto add_x = transcript_Px; + auto add_y = transcript_Py; + // Group operation is point addition + { + auto lambda_denominator = (rhs_x - add_x); + auto lambda_numerator = (rhs_y - add_y); + auto lambda_relation = lambda * lambda_denominator - lambda_numerator; // degree 2 + transcript_add_lambda_relation += lambda_relation * is_add; // degree 3 + } + // Group operation is point doubling + { + auto lambda_denominator = add_y + add_y; + auto lambda_numerator = add_x * add_x * 3; + auto lambda_relation = lambda * lambda_denominator - lambda_numerator; // degree 2 + transcript_add_lambda_relation += lambda_relation * is_double; // degree 4 + } + auto transcript_add_or_dbl_from_add_output_is_valid = + (-transcript_Pinfinity + 1) * (-is_accumulator_empty + 1); // degree 2 + transcript_add_lambda_relation *= transcript_add_or_dbl_from_add_output_is_valid; // degree 6 + // No group operation because of points at infinity + { + auto lambda_relation_invalid = + (transcript_Pinfinity + is_accumulator_empty + add_result_is_infinity); // degree 2 + auto lambda_relation = lambda * lambda_relation_invalid; // degree 4 + transcript_add_lambda_relation += lambda_relation; // (still degree 6) + } + transcript_lambda_relation += transcript_add_lambda_relation * q_add; + std::get<14>(accumulator) += transcript_lambda_relation * scaling_factor; // degree 7 + } + /** + * @brief Validate transcript_accumulator_x_shift / transcript_accumulator_y_shift are well formed. + * Conditions (one of the following): + * 1. The result of a group operation involving transcript_accumulator and msm_output (q_add = 1) + * 2. The result of a group operation involving transcript_accumulator and transcript_P (msm_transition = + * 1) + * 3. Is equal to transcript_accumulator (no group operation, no reset) + * 4. Is 0 (reset) + */ + { + auto lambda_sqr = lambda * lambda; + // add relation that validates result_infinity_from_operation * result_is_infinity = 0 + + // N.B. these relations rely on the fact that `lambda = 0` if we are not evaluating add/double formula + // (i.e. one or both outputs are points at infinity, or produce a point at infinity) + // This should be validated by the lambda_relation + auto x3 = lambda_sqr - lhs_x - rhs_x; // degree 2 + x3 += result_is_lhs * (rhs_x + lhs_x + lhs_x); // degree 4 + x3 += result_is_rhs * (lhs_x + rhs_x + rhs_x); // degree 4 + x3 += result_is_infinity * (lhs_x + rhs_x); // degree 4 + auto y3 = lambda * (lhs_x - out_x) - lhs_y; // degree 3 + y3 += result_is_lhs * (lhs_y + lhs_y); // degree 4 + y3 += result_is_rhs * (lhs_y + rhs_y); // degree 4 + y3 += result_is_infinity * lhs_y; // degree 4 + + auto propagate_transcript_accumulator = (-q_add - msm_transition - q_reset_accumulator + 1); + auto add_point_x_relation = (x3 - out_x) * any_add_is_active; // degree 5 + add_point_x_relation += + propagate_transcript_accumulator * is_not_last_row * (out_x - transcript_accumulator_x); + // validate out_x = 0 if q_reset_accumulator = 1 + add_point_x_relation += (out_x * q_reset_accumulator); + auto add_point_y_relation = (y3 - out_y) * any_add_is_active; // degree 5 + add_point_y_relation += + propagate_transcript_accumulator * is_not_last_row * (out_y - transcript_accumulator_y); + // validate out_y = 0 if q_reset_accumulator = 1 + add_point_y_relation += (out_y * q_reset_accumulator); + std::get<15>(accumulator) += add_point_x_relation * scaling_factor; // degree 5 + std::get<16>(accumulator) += add_point_y_relation * scaling_factor; // degree 5 + } + + // step 1: subtract offset generator from msm_accumulator + // this might produce a point at infinity + { + const auto offset = offset_generator(); + const auto x1 = offset[0]; + const auto y1 = -offset[1]; + const auto x2 = View(in.transcript_msm_x); + const auto y2 = View(in.transcript_msm_y); + const auto x3 = View(in.transcript_msm_intermediate_x); + const auto y3 = View(in.transcript_msm_intermediate_y); + const auto transcript_msm_infinity = View(in.transcript_msm_infinity); + // cases: + // x2 == x1, y2 == y1 + // x2 != x1 + // (x2 - x1) + const auto x_term = (x3 + x2 + x1) * (x2 - x1) * (x2 - x1) - (y2 - y1) * (y2 - y1); // degree 3 + const auto y_term = (x1 - x3) * (y2 - y1) - (x2 - x1) * (y1 + y3); // degree 2 + // IF msm_infinity = false, transcript_msm_intermediate_x/y is either the result of subtracting offset + // generator from msm_x/y IF msm_infinity = true, transcript_msm_intermediate_x/y is 0 + const auto transcript_offset_generator_subtract_x = + x_term * (-transcript_msm_infinity + 1) + transcript_msm_infinity * x3; // degree 4 + const auto transcript_offset_generator_subtract_y = + y_term * (-transcript_msm_infinity + 1) + transcript_msm_infinity * y3; // degree 3 + std::get<17>(accumulator) += + msm_transition * transcript_offset_generator_subtract_x * scaling_factor; // degree 5 + std::get<18>(accumulator) += + msm_transition * transcript_offset_generator_subtract_y * scaling_factor; // degree 5 + + // validate transcript_msm_infinity is correct + // if transcript_msm_infinity = 1, (x2 == x1) and (y2 + y1 == 0) + const auto x_diff = x2 - x1; + const auto y_sum = y2 + y1; + std::get<19>(accumulator) += msm_transition * transcript_msm_infinity * x_diff * scaling_factor; // degree 3 + std::get<20>(accumulator) += msm_transition * transcript_msm_infinity * y_sum * scaling_factor; // degree 3 + // if transcript_msm_infinity = 1, then x_diff must have an inverse + const auto transcript_msm_x_inverse = View(in.transcript_msm_x_inverse); + const auto inverse_term = (-transcript_msm_infinity + 1) * (x_diff * transcript_msm_x_inverse - 1); + std::get<21>(accumulator) += msm_transition * inverse_term * scaling_factor; // degree 3 + } + + /** + * @brief Validate `is_accumulator_empty` is updated correctly + * An add operation can produce a point at infinity + * Resetting the accumulator produces a point at infinity + * If we are not adding, performing an msm or resetting the accumulator, is_accumulator_empty should not update + */ + auto accumulator_infinity_preserve_flag = (-(q_add + msm_transition + q_reset_accumulator) + 1); // degree 1 + auto accumulator_infinity_preserve = accumulator_infinity_preserve_flag * + (is_accumulator_empty - is_accumulator_empty_shift) * + is_not_first_or_last_row; // degree 3 + auto accumulator_infinity_q_reset = q_reset_accumulator * (-is_accumulator_empty_shift + 1); // degree 2 + auto accumulator_infinity_from_add = + any_add_is_active * (result_is_infinity - is_accumulator_empty_shift); // degree 3 + auto accumulator_infinity_relation = + accumulator_infinity_preserve + + (accumulator_infinity_q_reset + accumulator_infinity_from_add) * is_not_first_row; // degree 4 + std::get<22>(accumulator) += accumulator_infinity_relation * scaling_factor; // degree 4 + + /** + * @brief Validate `transcript_add_x_equal` is well-formed + * If lhs_x == rhs_x, transcript_add_x_equal = 1 + * If transcript_add_x_equal = 0, a valid inverse must exist for (lhs_x - rhs_x) + */ + auto x_diff = lhs_x - rhs_x; // degree 2 + auto x_product = transcript_Px_inverse * (-transcript_add_x_equal + 1) + transcript_add_x_equal; // degree 2 + auto x_constant = transcript_add_x_equal - 1; // degree 1 + auto transcript_add_x_equal_check_relation = (x_diff * x_product + x_constant) * any_add_is_active; // degree 5 + std::get<23>(accumulator) += transcript_add_x_equal_check_relation * scaling_factor; // degree 5 + + /** + * @brief Validate `transcript_add_y_equal` is well-formed + * If lhs_y == rhs_y, transcript_add_y_equal = 1 + * If transcript_add_y_equal = 0, a valid inverse must exist for (lhs_y - rhs_y) + */ + auto y_diff = lhs_y - rhs_y; + auto y_product = transcript_Py_inverse * (-transcript_add_y_equal + 1) + transcript_add_y_equal; + auto y_constant = transcript_add_y_equal - 1; + auto transcript_add_y_equal_check_relation = (y_diff * y_product + y_constant) * any_add_is_active; + std::get<24>(accumulator) += transcript_add_y_equal_check_relation * scaling_factor; // degree 5 + } } template class ECCVMTranscriptRelationImpl; diff --git a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.hpp b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.hpp index ef511e41331..21546026046 100644 --- a/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/ecc_vm/ecc_transcript_relation.hpp @@ -30,8 +30,8 @@ template class ECCVMTranscriptRelationImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, }; template diff --git a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/op_queue/ecc_op_queue.hpp b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/op_queue/ecc_op_queue.hpp index 8de93d520e9..91e64b764a0 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/op_queue/ecc_op_queue.hpp +++ b/barretenberg/cpp/src/barretenberg/stdlib_circuit_builders/op_queue/ecc_op_queue.hpp @@ -374,6 +374,32 @@ class ECCOpQueue { return ultra_op; } + /** + * @brief Write no op (i.e. empty row) + * + */ + UltraOp no_op() + { + // Construct and store the operation in the ultra op format + auto ultra_op = construct_and_populate_ultra_ops(NULL_OP, accumulator); + + // Store raw operation + raw_ops.emplace_back(ECCVMOperation{ + .add = false, + .mul = false, + .eq = false, + .reset = false, + .base_point = { 0, 0 }, + .z1 = 0, + .z2 = 0, + .mul_scalar_full = 0, + }); + num_transcript_rows += 1; + update_cached_msms(raw_ops.back()); + + return ultra_op; + } + /** * @brief Write equality op using internal accumulator point * @@ -415,10 +441,10 @@ class ECCOpQueue { void update_cached_msms(const ECCVMOperation& op) { if (op.mul) { - if (op.z1 != 0) { + if (op.z1 != 0 && !op.base_point.is_point_at_infinity()) { cached_active_msm_count++; } - if (op.z2 != 0) { + if (op.z2 != 0 && !op.base_point.is_point_at_infinity()) { cached_active_msm_count++; } } else if (cached_active_msm_count != 0) {