From af9fea4bbafe1a41b09d9351a34a896db2c8ab7d Mon Sep 17 00:00:00 2001 From: Lucas Xia Date: Fri, 17 May 2024 18:39:32 -0400 Subject: [PATCH] feat: laying out a new recursion constraint for honk (#6489) Create new recursion constraint for honk, which is the same as the plonk recursion constraint, but with a default aggregation object. The default aggregation object work was moved from https://github.com/AztecProtocol/aztec-packages/pull/6087. This PR is mostly for setup for https://github.com/AztecProtocol/barretenberg/issues/933. --- barretenberg/acir_tests/reset_acir_tests.sh | 7 + .../dsl/acir_format/acir_format.cpp | 137 ++++++- .../dsl/acir_format/acir_format.hpp | 15 +- .../dsl/acir_format/acir_format.test.cpp | 6 + .../acir_format/bigint_constraint.test.cpp | 5 + .../dsl/acir_format/block_constraint.test.cpp | 1 + .../dsl/acir_format/ec_operations.test.cpp | 2 + .../dsl/acir_format/ecdsa_secp256k1.test.cpp | 3 + .../dsl/acir_format/ecdsa_secp256r1.test.cpp | 4 + .../acir_format/honk_recursion_constraint.cpp | 370 ++++++++++++++++++ .../acir_format/honk_recursion_constraint.hpp | 76 ++++ .../honk_recursion_constraint.test.cpp | 365 +++++++++++++++++ .../acir_format/poseidon2_constraint.test.cpp | 1 + .../acir_format/recursion_constraint.test.cpp | 39 +- .../acir_format/sha256_constraint.test.cpp | 1 + .../stdlib/primitives/bigfield/bigfield.hpp | 16 +- 16 files changed, 1011 insertions(+), 37 deletions(-) create mode 100644 barretenberg/acir_tests/reset_acir_tests.sh create mode 100644 barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.cpp create mode 100644 barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.hpp create mode 100644 barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.test.cpp diff --git a/barretenberg/acir_tests/reset_acir_tests.sh b/barretenberg/acir_tests/reset_acir_tests.sh new file mode 100644 index 00000000000..e83bea9189e --- /dev/null +++ b/barretenberg/acir_tests/reset_acir_tests.sh @@ -0,0 +1,7 @@ +cd ~/aztec-packages/noir/noir-repo +cargo clean +noirup -p . +cd test_programs && ./rebuild.sh + +cd ~/aztec-packages/barretenberg/acir_tests +rm -rf acir_tests diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp index f74228a115f..3dc7fc15e6c 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp @@ -10,7 +10,10 @@ template class DSLBigInts; template class DSLBigInts; template -void build_constraints(Builder& builder, AcirFormat const& constraint_system, bool has_valid_witness_assignments) +void build_constraints(Builder& builder, + AcirFormat const& constraint_system, + bool has_valid_witness_assignments, + bool honk_recursion) { // Add arithmetic gates for (const auto& constraint : constraint_system.poly_triple_constraints) { @@ -118,6 +121,7 @@ void build_constraints(Builder& builder, AcirFormat const& constraint_system, bo create_bigint_to_le_bytes_constraint(builder, constraint, dsl_bigints); } + // RecursionConstraint // TODO(https://github.com/AztecProtocol/barretenberg/issues/817): disable these for UGH for now since we're not yet // dealing with proper recursion if constexpr (IsGoblinUltraBuilder) { @@ -161,7 +165,7 @@ void build_constraints(Builder& builder, AcirFormat const& constraint_system, bo auto error_string = format( "Public inputs are always stripped from proofs unless we have a recursive proof.\n" "Thus, public inputs attached to a proof must match the recursive aggregation object in size " - "which is {}\n", + "which is ", RecursionConstraint::AGGREGATION_OBJECT_SIZE); throw_or_abort(error_string); } @@ -206,6 +210,121 @@ void build_constraints(Builder& builder, AcirFormat const& constraint_system, bo builder.set_recursive_proof(proof_output_witness_indices); } } + + // HonkRecursionConstraint + // TODO(https://github.com/AztecProtocol/barretenberg/issues/817): disable these for UGH for now since we're not yet + // dealing with proper recursion + if constexpr (IsGoblinUltraBuilder) { + if (!constraint_system.honk_recursion_constraints.empty()) { + info("WARNING: this circuit contains honk_recursion_constraints!"); + } + } else { + // These are set and modified whenever we encounter a recursion opcode + // + // These should not be set by the caller + // TODO(maxim): Check if this is always the case. ie I won't receive a proof that will set the first + // TODO(maxim): input_aggregation_object to be non-zero. + // TODO(maxim): if not, we can add input_aggregation_object to the proof too for all recursive proofs + // TODO(maxim): This might be the case for proof trees where the proofs are created on different machines + std::array current_aggregation_object = { + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 + }; + + // Get the size of proof with no public inputs prepended to it + // This is used while processing recursion constraints to determine whether + // the proof we are verifying contains a recursive proof itself + auto proof_size_no_pub_inputs = recursion_honk_proof_size_without_public_inputs(); + + // Add recursion constraints + for (auto constraint : constraint_system.honk_recursion_constraints) { + // A proof passed into the constraint should be stripped of its public inputs, except in the case where a + // proof contains an aggregation object itself. We refer to this as the `nested_aggregation_object`. The + // verifier circuit requires that the indices to a nested proof aggregation state are a circuit constant. + // The user tells us they how they want these constants set by keeping the nested aggregation object + // attached to the proof as public inputs. As this is the only object that can prepended to the proof if the + // proof is above the expected size (with public inputs stripped) + std::array nested_aggregation_object = {}; + // If the proof has public inputs attached to it, we should handle setting the nested aggregation object + // The public inputs attached to a proof should match the aggregation object in size + if (constraint.proof.size() - proof_size_no_pub_inputs != + HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE) { + auto error_string = format( + "Public inputs are always stripped from proofs unless we have a recursive proof.\n" + "Thus, public inputs attached to a proof must match the recursive aggregation object in size " + "which is ", + HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE); + throw_or_abort(error_string); + } + for (size_t i = 0; i < HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE; ++i) { + // Set the nested aggregation object indices to the current size of the public inputs + // This way we know that the nested aggregation object indices will always be the last + // indices of the public inputs + nested_aggregation_object[i] = static_cast(constraint.public_inputs.size()); + // Attach the nested aggregation object to the end of the public inputs to fill in + // the slot where the nested aggregation object index will point into + constraint.public_inputs.emplace_back(constraint.proof[i]); + } + // Remove the aggregation object so that they can be handled as normal public inputs + // in they way taht the recursion constraint expects + constraint.proof.erase(constraint.proof.begin(), + constraint.proof.begin() + + static_cast(HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE)); + current_aggregation_object = create_honk_recursion_constraints(builder, + constraint, + current_aggregation_object, + nested_aggregation_object, + has_valid_witness_assignments); + } + + // Now that the circuit has been completely built, we add the output aggregation as public + // inputs. + if (!constraint_system.honk_recursion_constraints.empty()) { + + // First add the output aggregation object as public inputs + // Set the indices as public inputs because they are no longer being + // created in ACIR + for (const auto& idx : current_aggregation_object) { + builder.set_public_input(idx); + } + + // Make sure the verification key records the public input indices of the + // final recursion output. + std::vector proof_output_witness_indices(current_aggregation_object.begin(), + current_aggregation_object.end()); + builder.set_recursive_proof(proof_output_witness_indices); + } else if (honk_recursion && + builder.is_recursive_circuit) { // Set a default aggregation object if we don't have one. + // TODO(https://github.com/AztecProtocol/barretenberg/issues/911): These are pairing points extracted from + // a valid proof. This is a workaround because we can't represent the point at infinity in biggroup yet. + fq x0("0x031e97a575e9d05a107acb64952ecab75c020998797da7842ab5d6d1986846cf"); + fq y0("0x178cbf4206471d722669117f9758a4c410db10a01750aebb5666547acf8bd5a4"); + + fq x1("0x0f94656a2ca489889939f81e9c74027fd51009034b3357f0e91b8a11e7842c38"); + fq y1("0x1b52c2020d7464a0c80c0da527a08193fe27776f50224bd6fb128b46c1ddb67f"); + std::vector aggregation_object_fq_values = { x0, y0, x1, y1 }; + size_t agg_obj_indices_idx = 0; + for (fq val : aggregation_object_fq_values) { + const uint256_t x = val; + std::array val_limbs = { + x.slice(0, fq_ct::NUM_LIMB_BITS), + x.slice(fq_ct::NUM_LIMB_BITS, fq_ct::NUM_LIMB_BITS * 2), + x.slice(fq_ct::NUM_LIMB_BITS * 2, fq_ct::NUM_LIMB_BITS * 3), + x.slice(fq_ct::NUM_LIMB_BITS * 3, bb::stdlib::field_conversion::TOTAL_BITS) + }; + for (size_t i = 0; i < fq_ct::NUM_LIMBS; ++i) { + uint32_t idx = builder.add_variable(val_limbs[i]); + builder.set_public_input(idx); + current_aggregation_object[agg_obj_indices_idx] = idx; + agg_obj_indices_idx++; + } + } + // Make sure the verification key records the public input indices of the + // final recursion output. + std::vector proof_output_witness_indices(current_aggregation_object.begin(), + current_aggregation_object.end()); + builder.set_recursive_proof(proof_output_witness_indices); + } + } } /** @@ -218,14 +337,17 @@ void build_constraints(Builder& builder, AcirFormat const& constraint_system, bo * @return Builder */ template <> -UltraCircuitBuilder create_circuit(const AcirFormat& constraint_system, size_t size_hint, WitnessVector const& witness) +UltraCircuitBuilder create_circuit(const AcirFormat& constraint_system, + size_t size_hint, + WitnessVector const& witness, + bool honk_recursion) { Builder builder{ size_hint, witness, constraint_system.public_inputs, constraint_system.varnum, constraint_system.recursive }; bool has_valid_witness_assignments = !witness.empty(); - build_constraints(builder, constraint_system, has_valid_witness_assignments); + build_constraints(builder, constraint_system, has_valid_witness_assignments, honk_recursion); builder.finalize_circuit(); @@ -244,7 +366,8 @@ UltraCircuitBuilder create_circuit(const AcirFormat& constraint_system, size_t s template <> GoblinUltraCircuitBuilder create_circuit(const AcirFormat& constraint_system, [[maybe_unused]] size_t size_hint, - WitnessVector const& witness) + WitnessVector const& witness, + bool honk_recursion) { // Construct a builder using the witness and public input data from acir and with the goblin-owned op_queue auto op_queue = std::make_shared(); // instantiate empty op_queue @@ -253,13 +376,13 @@ GoblinUltraCircuitBuilder create_circuit(const AcirFormat& constraint_system, // Populate constraints in the builder via the data in constraint_system bool has_valid_witness_assignments = !witness.empty(); - acir_format::build_constraints(builder, constraint_system, has_valid_witness_assignments); + acir_format::build_constraints(builder, constraint_system, has_valid_witness_assignments, honk_recursion); builder.finalize_circuit(); return builder; }; -template void build_constraints(GoblinUltraCircuitBuilder&, AcirFormat const&, bool); +template void build_constraints(GoblinUltraCircuitBuilder&, AcirFormat const&, bool, bool); } // namespace acir_format diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.hpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.hpp index 9add17a1451..35d4d1fe6c1 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.hpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.hpp @@ -9,6 +9,7 @@ #include "ec_operations.hpp" #include "ecdsa_secp256k1.hpp" #include "ecdsa_secp256r1.hpp" +#include "honk_recursion_constraint.hpp" #include "keccak_constraint.hpp" #include "logic_constraint.hpp" #include "multi_scalar_mul.hpp" @@ -54,6 +55,7 @@ struct AcirFormat { std::vector multi_scalar_mul_constraints; std::vector ec_add_constraints; std::vector recursion_constraints; + std::vector honk_recursion_constraints; std::vector bigint_from_le_bytes_constraints; std::vector bigint_to_le_bytes_constraints; std::vector bigint_operations; @@ -89,6 +91,7 @@ struct AcirFormat { multi_scalar_mul_constraints, ec_add_constraints, recursion_constraints, + honk_recursion_constraints, poly_triple_constraints, block_constraints, bigint_from_le_bytes_constraints, @@ -102,9 +105,17 @@ using WitnessVector = std::vector>; using WitnessVectorStack = std::vector>; template -Builder create_circuit(const AcirFormat& constraint_system, size_t size_hint = 0, WitnessVector const& witness = {}); +Builder create_circuit(const AcirFormat& constraint_system, + size_t size_hint = 0, + WitnessVector const& witness = {}, + bool honk_recursion = false); template -void build_constraints(Builder& builder, AcirFormat const& constraint_system, bool has_valid_witness_assignments); +void build_constraints(Builder& builder, + AcirFormat const& constraint_system, + bool has_valid_witness_assignments, + bool honk_recursion = false); // honk_recursion means we will honk to recursively verify this + // circuit. This distinction is needed to not add the default + // aggregation object when we're not using the honk RV. } // namespace acir_format diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.test.cpp index 038db2a28f9..cf6df51ea90 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.test.cpp @@ -52,6 +52,7 @@ TEST_F(AcirFormatTests, TestASingleConstraintNoPubInputs) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -170,6 +171,7 @@ TEST_F(AcirFormatTests, TestLogicGateFromNoirCircuit) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -240,6 +242,7 @@ TEST_F(AcirFormatTests, TestSchnorrVerifyPass) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -337,6 +340,7 @@ TEST_F(AcirFormatTests, TestSchnorrVerifySmallRange) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -453,6 +457,7 @@ TEST_F(AcirFormatTests, TestVarKeccak) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -502,6 +507,7 @@ TEST_F(AcirFormatTests, TestKeccakPermutation) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/bigint_constraint.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/bigint_constraint.test.cpp index 1cc86262bd1..923d496fd8d 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/bigint_constraint.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/bigint_constraint.test.cpp @@ -189,6 +189,7 @@ TEST_F(BigIntTests, TestBigIntConstraintMultiple) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -259,6 +260,7 @@ TEST_F(BigIntTests, TestBigIntConstraintSimple) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = { from_le_bytes_constraint_bigint1 }, .bigint_to_le_bytes_constraints = { result2_to_le_bytes }, .bigint_operations = { add_constraint }, @@ -314,6 +316,7 @@ TEST_F(BigIntTests, TestBigIntConstraintReuse) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -373,6 +376,7 @@ TEST_F(BigIntTests, TestBigIntConstraintReuse2) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -453,6 +457,7 @@ TEST_F(BigIntTests, TestBigIntDIV) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = { from_le_bytes_constraint_bigint1, from_le_bytes_constraint_bigint2 }, .bigint_to_le_bytes_constraints = { result3_to_le_bytes }, .bigint_operations = { div_constraint }, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/block_constraint.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/block_constraint.test.cpp index 5d649d8feb3..eb377b5b532 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/block_constraint.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/block_constraint.test.cpp @@ -131,6 +131,7 @@ TEST_F(UltraPlonkRAM, TestBlockConstraint) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/ec_operations.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/ec_operations.test.cpp index 59333ddc0d4..1cd34c076f8 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/ec_operations.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/ec_operations.test.cpp @@ -76,6 +76,7 @@ TEST_F(EcOperations, TestECOperations) .multi_scalar_mul_constraints = {}, .ec_add_constraints = { ec_add_constraint }, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -161,6 +162,7 @@ TEST_F(EcOperations, TestECMultiScalarMul) .multi_scalar_mul_constraints = { msm_constrain }, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256k1.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256k1.test.cpp index 61782002c85..90a5546068d 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256k1.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256k1.test.cpp @@ -111,6 +111,7 @@ TEST_F(ECDSASecp256k1, TestECDSAConstraintSucceed) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -162,6 +163,7 @@ TEST_F(ECDSASecp256k1, TestECDSACompilesForVerifier) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -208,6 +210,7 @@ TEST_F(ECDSASecp256k1, TestECDSAConstraintFail) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256r1.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256r1.test.cpp index de1d0931d8c..257bcf4a2e2 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256r1.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/ecdsa_secp256r1.test.cpp @@ -145,6 +145,7 @@ TEST(ECDSASecp256r1, test_hardcoded) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -198,6 +199,7 @@ TEST(ECDSASecp256r1, TestECDSAConstraintSucceed) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -249,6 +251,7 @@ TEST(ECDSASecp256r1, TestECDSACompilesForVerifier) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -295,6 +298,7 @@ TEST(ECDSASecp256r1, TestECDSAConstraintFail) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.cpp new file mode 100644 index 00000000000..fb46384ce01 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.cpp @@ -0,0 +1,370 @@ +#include "honk_recursion_constraint.hpp" +#include "barretenberg/plonk/proof_system/verification_key/verification_key.hpp" +#include "barretenberg/plonk/transcript/transcript_wrappers.hpp" +#include "barretenberg/stdlib/plonk_recursion/aggregation_state/aggregation_state.hpp" +#include "barretenberg/stdlib/plonk_recursion/verifier/verifier.hpp" +#include "barretenberg/stdlib/primitives/bigfield/constants.hpp" +#include "recursion_constraint.hpp" + +namespace acir_format { + +using namespace bb::plonk; + +/** + * @brief Add constraints required to recursively verify an UltraPlonk proof + * + * @param builder + * @param input + * @tparam has_valid_witness_assignment. Do we have witnesses or are we just generating keys? + * @tparam inner_proof_contains_recursive_proof. Do we expect the inner proof to also have performed recursive + * verification? We need to know this at circuit-compile time. + * + * @note We currently only support HonkRecursionConstraint where inner_proof_contains_recursive_proof = false. + * We would either need a separate ACIR opcode where inner_proof_contains_recursive_proof = true, + * or we need non-witness data to be provided as metadata in the ACIR opcode + */ +std::array create_honk_recursion_constraints( + Builder& builder, + const HonkRecursionConstraint& input, + std::array input_aggregation_object, + std::array nested_aggregation_object, + bool has_valid_witness_assignments) +{ + const auto& nested_aggregation_indices = nested_aggregation_object; + const bool inner_proof_contains_recursive_proof = true; + + // If we do not have a witness, we must ensure that our dummy witness will not trigger + // on-curve errors and inverting-zero errors + { + // get a fake key/proof that satisfies on-curve + inversion-zero checks + const std::vector dummy_key = export_dummy_honk_key_in_recursion_format( + PolynomialManifest(Builder::CIRCUIT_TYPE), inner_proof_contains_recursive_proof); + const auto manifest = Composer::create_manifest(input.public_inputs.size()); + std::vector dummy_proof = + export_dummy_honk_transcript_in_recursion_format(manifest, inner_proof_contains_recursive_proof); + + for (size_t i = 0; i < input.public_inputs.size(); ++i) { + const auto public_input_idx = input.public_inputs[i]; + // if we do NOT have a witness assignment (i.e. are just building the proving/verification keys), + // we add our dummy public input values as Builder variables. + // if we DO have a valid witness assignment, we use the real witness assignment + bb::fr dummy_field = + has_valid_witness_assignments ? builder.get_variable(public_input_idx) : dummy_proof[i]; + // Create a copy constraint between our dummy field and the witness index provided by + // HonkRecursionConstraint. This will make the HonkRecursionConstraint idx equal to `dummy_field`. In the + // case of a valid witness assignment, this does nothing (as dummy_field = real value) In the case of no + // valid witness assignment, this makes sure that the HonkRecursionConstraint witness indices will not + // trigger basic errors (check inputs are on-curve, check we are not inverting 0) + // + // Failing to do these copy constraints on public inputs will trigger these basic errors + // in the case of a nested proof, as an aggregation object is expected to be two G1 points even + // in the case of no valid witness assignments. + builder.assert_equal(builder.add_variable(dummy_field), public_input_idx); + } + // Remove the public inputs from the dummy proof + // The proof supplied to the recursion constraint will already be stripped of public inputs + // while the barretenberg API works with public inputs prepended to the proof. + dummy_proof.erase(dummy_proof.begin(), + dummy_proof.begin() + static_cast(input.public_inputs.size())); + for (size_t i = 0; i < input.proof.size(); ++i) { + const auto proof_field_idx = input.proof[i]; + bb::fr dummy_field = has_valid_witness_assignments ? builder.get_variable(proof_field_idx) : dummy_proof[i]; + builder.assert_equal(builder.add_variable(dummy_field), proof_field_idx); + } + for (size_t i = 0; i < input.key.size(); ++i) { + const auto key_field_idx = input.key[i]; + bb::fr dummy_field = has_valid_witness_assignments ? builder.get_variable(key_field_idx) : dummy_key[i]; + builder.assert_equal(builder.add_variable(dummy_field), key_field_idx); + } + } + + // Construct an in-circuit representation of the verification key. + // For now, the v-key is a circuit constant and is fixed for the circuit. + // (We may need a separate recursion opcode for this to vary, or add more config witnesses to this opcode) + const auto& aggregation_input = input_aggregation_object; + aggregation_state_ct previous_aggregation; + + // If we have previously recursively verified proofs, `inner_aggregation_object_nonzero = true` + // For now this is a complile-time constant i.e. whether this is true/false is fixed for the circuit! + bool inner_aggregation_indices_all_zero = true; + for (const auto& idx : aggregation_input) { + inner_aggregation_indices_all_zero &= (idx == 0); + } + + if (!inner_aggregation_indices_all_zero) { + std::array aggregation_elements; + for (size_t i = 0; i < 4; ++i) { + aggregation_elements[i] = + bn254::BaseField(field_ct::from_witness_index(&builder, aggregation_input[4 * i]), + field_ct::from_witness_index(&builder, aggregation_input[4 * i + 1]), + field_ct::from_witness_index(&builder, aggregation_input[4 * i + 2]), + field_ct::from_witness_index(&builder, aggregation_input[4 * i + 3])); + aggregation_elements[i].assert_is_in_field(); + } + // If we have a previous aggregation object, assign it to `previous_aggregation` so that it is included + // in stdlib::recursion::verify_proof + previous_aggregation.P0 = bn254::Group(aggregation_elements[0], aggregation_elements[1]); + previous_aggregation.P1 = bn254::Group(aggregation_elements[2], aggregation_elements[3]); + previous_aggregation.has_data = true; + } else { + previous_aggregation.has_data = false; + } + + transcript::Manifest manifest = Composer::create_manifest(input.public_inputs.size()); + + std::vector key_fields; + key_fields.reserve(input.key.size()); + for (const auto& idx : input.key) { + auto field = field_ct::from_witness_index(&builder, idx); + key_fields.emplace_back(field); + } + + std::vector proof_fields; + // Prepend the public inputs to the proof fields because this is how the + // core barretenberg library processes proofs (with the public inputs first and not separated) + proof_fields.reserve(input.proof.size() + input.public_inputs.size()); + for (const auto& idx : input.public_inputs) { + auto field = field_ct::from_witness_index(&builder, idx); + proof_fields.emplace_back(field); + } + for (const auto& idx : input.proof) { + auto field = field_ct::from_witness_index(&builder, idx); + proof_fields.emplace_back(field); + } + + // recursively verify the proof + std::shared_ptr vkey = verification_key_ct::from_field_elements( + &builder, key_fields, inner_proof_contains_recursive_proof, nested_aggregation_indices); + vkey->program_width = noir_recursive_settings::program_width; + + Transcript_ct transcript(&builder, manifest, proof_fields, input.public_inputs.size()); + aggregation_state_ct result = bb::stdlib::recursion::verify_proof_( + &builder, vkey, transcript, previous_aggregation); + + // Assign correct witness value to the verification key hash + vkey->hash().assert_equal(field_ct::from_witness_index(&builder, input.key_hash)); + + ASSERT(result.public_inputs.size() == input.public_inputs.size()); + + // Assign the `public_input` field to the public input of the inner proof + for (size_t i = 0; i < input.public_inputs.size(); ++i) { + result.public_inputs[i].assert_equal(field_ct::from_witness_index(&builder, input.public_inputs[i])); + } + + // We want to return an array, so just copy the vector into the array + ASSERT(result.proof_witness_indices.size() == HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE); + std::array resulting_output_aggregation_object; + std::copy(result.proof_witness_indices.begin(), + result.proof_witness_indices.begin() + HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE, + resulting_output_aggregation_object.begin()); + + return resulting_output_aggregation_object; +} + +/** + * @brief When recursively verifying proofs, we represent the verification key using field elements. + * This method exports the key formatted in the manner our recursive verifier expects. + * NOTE: only used by the dsl at the moment. Might be cleaner to make this a dsl function? + * + * @return std::vector + */ +std::vector export_honk_key_in_recursion_format(std::shared_ptr const& vkey) +{ + std::vector output; + output.emplace_back(vkey->domain.root); + output.emplace_back(vkey->domain.domain); + output.emplace_back(vkey->domain.generator); + output.emplace_back(vkey->circuit_size); + output.emplace_back(vkey->num_public_inputs); + output.emplace_back(vkey->contains_recursive_proof); + for (size_t i = 0; i < HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE; ++i) { + if (vkey->recursive_proof_public_input_indices.size() > i) { + output.emplace_back(vkey->recursive_proof_public_input_indices[i]); + } else { + output.emplace_back(0); + ASSERT(vkey->contains_recursive_proof == false); + } + } + for (const auto& descriptor : vkey->polynomial_manifest.get()) { + if (descriptor.source == PolynomialSource::SELECTOR || descriptor.source == PolynomialSource::PERMUTATION) { + const auto element = vkey->commitments.at(std::string(descriptor.commitment_label)); + auto g1_as_fields = export_g1_affine_element_as_fields(element); + output.emplace_back(g1_as_fields.x_lo); + output.emplace_back(g1_as_fields.x_hi); + output.emplace_back(g1_as_fields.y_lo); + output.emplace_back(g1_as_fields.y_hi); + } + } + + verification_key_data vkey_data{ + .circuit_type = static_cast(vkey->circuit_type), + .circuit_size = static_cast(vkey->circuit_size), + .num_public_inputs = static_cast(vkey->num_public_inputs), + .commitments = vkey->commitments, + .contains_recursive_proof = vkey->contains_recursive_proof, + .recursive_proof_public_input_indices = vkey->recursive_proof_public_input_indices, + }; + output.emplace_back(vkey_data.hash_native(0)); // key_hash + return output; +} + +/** + * @brief When recursively verifying proofs, we represent the verification key using field elements. + * This method exports the key formatted in the manner our recursive verifier expects. + * A dummy key is used when building a circuit without a valid witness assignment. + * We want the transcript to contain valid G1 points to prevent on-curve errors being thrown. + * We want a non-zero circuit size as this element will be inverted by the circuit + * and we do not want an "inverting 0" error thrown + * + * @return std::vector + */ +std::vector export_dummy_honk_key_in_recursion_format(const PolynomialManifest& polynomial_manifest, + const bool contains_recursive_proof) +{ + std::vector output; + output.emplace_back(1); // domain.domain (will be inverted) + output.emplace_back(1); // domain.root (will be inverted) + output.emplace_back(1); // domain.generator (will be inverted) + + output.emplace_back(1); // circuit size + output.emplace_back(1); // num public inputs + + output.emplace_back(contains_recursive_proof); // contains_recursive_proof + for (size_t i = 0; i < HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE; ++i) { + output.emplace_back(0); // recursive_proof_public_input_indices + } + + for (const auto& descriptor : polynomial_manifest.get()) { + if (descriptor.source == PolynomialSource::SELECTOR || descriptor.source == PolynomialSource::PERMUTATION) { + // the std::biggroup class creates unsatisfiable constraints when identical points are added/subtracted. + // (when verifying zk proofs this is acceptable as we make sure verification key points are not identical. + // And prover points should contain randomness for an honest Prover). + // This check can also trigger a runtime error due to causing 0 to be inverted. + // When creating dummy verification key points we must be mindful of the above and make sure that each + // transcript point is unique. + auto scalar = bb::fr::random_element(); + const auto element = bb::g1::affine_element(bb::g1::one * scalar); + auto g1_as_fields = export_g1_affine_element_as_fields(element); + output.emplace_back(g1_as_fields.x_lo); + output.emplace_back(g1_as_fields.x_hi); + output.emplace_back(g1_as_fields.y_lo); + output.emplace_back(g1_as_fields.y_hi); + } + } + + output.emplace_back(0); // key_hash + + return output; +} + +/** + * @brief Returns transcript represented as a vector of bb::fr. + * Used to represent recursive proofs (i.e. proof represented as circuit-native field elements) + * + * @return std::vector + */ +std::vector export_honk_transcript_in_recursion_format(const transcript::StandardTranscript& transcript) +{ + std::vector fields; + const auto num_rounds = transcript.get_manifest().get_num_rounds(); + for (size_t i = 0; i < num_rounds; ++i) { + for (const auto& manifest_element : transcript.get_manifest().get_round_manifest(i).elements) { + if (!manifest_element.derived_by_verifier) { + if (manifest_element.num_bytes == 32 && manifest_element.name != "public_inputs") { + fields.emplace_back(transcript.get_field_element(manifest_element.name)); + } else if (manifest_element.num_bytes == 64 && manifest_element.name != "public_inputs") { + const auto group_element = transcript.get_group_element(manifest_element.name); + auto g1_as_fields = export_g1_affine_element_as_fields(group_element); + fields.emplace_back(g1_as_fields.x_lo); + fields.emplace_back(g1_as_fields.x_hi); + fields.emplace_back(g1_as_fields.y_lo); + fields.emplace_back(g1_as_fields.y_hi); + } else { + ASSERT(manifest_element.name == "public_inputs"); + const auto public_inputs_vector = transcript.get_field_element_vector(manifest_element.name); + for (const auto& ele : public_inputs_vector) { + fields.emplace_back(ele); + } + } + } + } + } + return fields; +} + +/** + * @brief Get a dummy fake proof for recursion. All elliptic curve group elements are still valid points to prevent + * errors being thrown. + * + * @param manifest + * @return std::vector + */ +std::vector export_dummy_honk_transcript_in_recursion_format(const transcript::Manifest& manifest, + const bool contains_recursive_proof) +{ + std::vector fields; + const auto num_rounds = manifest.get_num_rounds(); + for (size_t i = 0; i < num_rounds; ++i) { + for (const auto& manifest_element : manifest.get_round_manifest(i).elements) { + if (!manifest_element.derived_by_verifier) { + if (manifest_element.num_bytes == 32 && manifest_element.name != "public_inputs") { + // auto scalar = bb::fr::random_element(); + fields.emplace_back(0); + } else if (manifest_element.num_bytes == 64 && manifest_element.name != "public_inputs") { + // the std::biggroup class creates unsatisfiable constraints when identical points are + // added/subtracted. + // (when verifying zk proofs this is acceptable as we make sure verification key points are not + // identical. And prover points should contain randomness for an honest Prover). This check can + // also trigger a runtime error due to causing 0 to be inverted. When creating dummy proof + // points we must be mindful of the above and make sure that each point is unique. + auto scalar = bb::fr::random_element(); + const auto group_element = bb::g1::affine_element(bb::g1::one * scalar); + auto g1_as_fields = export_g1_affine_element_as_fields(group_element); + fields.emplace_back(g1_as_fields.x_lo); + fields.emplace_back(g1_as_fields.x_hi); + fields.emplace_back(g1_as_fields.y_lo); + fields.emplace_back(g1_as_fields.y_hi); + } else { + ASSERT(manifest_element.name == "public_inputs"); + const size_t num_public_inputs = manifest_element.num_bytes / 32; + // If we have a recursive proofs the public inputs must describe an aggregation object that + // is composed of two valid G1 points on the curve. Without this conditional we will get a + // runtime error that we are attempting to invert 0. + if (contains_recursive_proof) { + // When setting up the ACIR we emplace back the nested aggregation object + // fetched from the proof onto the public inputs. Thus, we can expect the + // nested aggregation object to always be at the end of the public inputs. + for (size_t k = 0; k < num_public_inputs - HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE; + ++k) { + fields.emplace_back(0); + } + for (size_t k = 0; k < HonkRecursionConstraint::NUM_AGGREGATION_ELEMENTS; ++k) { + auto scalar = bb::fr::random_element(); + const auto group_element = bb::g1::affine_element(bb::g1::one * scalar); + auto g1_as_fields = export_g1_affine_element_as_fields(group_element); + fields.emplace_back(g1_as_fields.x_lo); + fields.emplace_back(g1_as_fields.x_hi); + fields.emplace_back(g1_as_fields.y_lo); + fields.emplace_back(g1_as_fields.y_hi); + } + } else { + for (size_t j = 0; j < num_public_inputs; ++j) { + // auto scalar = bb::fr::random_element(); + fields.emplace_back(0); + } + } + } + } + } + } + return fields; +} + +size_t recursion_honk_proof_size_without_public_inputs() +{ + const auto manifest = Composer::create_manifest(0); + auto dummy_transcript = export_dummy_honk_transcript_in_recursion_format(manifest, false); + return dummy_transcript.size(); +} + +} // namespace acir_format diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.hpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.hpp new file mode 100644 index 00000000000..8696e9ef073 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.hpp @@ -0,0 +1,76 @@ +#pragma once +#include "barretenberg/dsl/types.hpp" +#include "barretenberg/plonk/proof_system/verification_key/verification_key.hpp" +#include + +namespace acir_format { + +using namespace bb::plonk; + +/** + * @brief HonkRecursionConstraint struct contains information required to recursively verify a proof! + * + * @details The recursive verifier algorithm produces an 'aggregation object' representing 2 G1 points, expressed as 16 + * witness values. The smart contract Verifier must be aware of this aggregation object in order to complete the full + * recursive verification. If the circuit verifies more than 1 proof, the recursion algorithm will update a pre-existing + * aggregation object (`input_aggregation_object`). + * + * @details We currently require that the inner circuit being verified only has a single public input. If more are + * required, the outer circuit can hash them down to 1 input. + * + * @param verification_key_data The inner circuit vkey. Is converted into circuit witness values (internal to the + * backend) + * @param proof The plonk proof. Is converted into circuit witness values (internal to the backend) + * @param is_aggregation_object_nonzero A flag to tell us whether the circuit has already recursively verified proofs + * (and therefore an aggregation object is present) + * @param public_input The index of the single public input + * @param input_aggregation_object Witness indices of pre-existing aggregation object (if it exists) + * @param output_aggregation_object Witness indices of the aggregation object produced by recursive verification + * @param nested_aggregation_object Public input indices of an aggregation object inside the proof. + * + * @note If input_aggregation_object witness indices are all zero, we interpret this to mean that the inner proof does + * NOT contain a previously recursively verified proof + * @note nested_aggregation_object is used for cases where the proof being verified contains an aggregation object in + * its public inputs! If this is the case, we record the public input locations in `nested_aggregation_object`. If the + * inner proof is of a circuit that does not have a nested aggregation object, these values are all zero. + * + * To outline the interaction between the input_aggergation_object and the nested_aggregation_object take the following + * example: If we have a circuit that verifies 2 proofs A and B, the recursion constraint for B will have an + * input_aggregation_object that points to the aggregation output produced by verifying A. If circuit B also verifies a + * proof, in the above example the recursion constraint for verifying B will have a nested object that describes the + * aggregation object in B’s public inputs as well as an input aggregation object that points to the object produced by + * the previous recursion constraint in the circuit (the one that verifies A) + * + */ +struct HonkRecursionConstraint { + // An aggregation state is represented by two G1 affine elements. Each G1 point has + // two field element coordinates (x, y). Thus, four field elements + static constexpr size_t NUM_AGGREGATION_ELEMENTS = 4; + // Four limbs are used when simulating a non-native field using the bigfield class + static constexpr size_t AGGREGATION_OBJECT_SIZE = + NUM_AGGREGATION_ELEMENTS * NUM_QUOTIENT_PARTS; // 16 field elements + std::vector key; + std::vector proof; + std::vector public_inputs; + uint32_t key_hash; + + friend bool operator==(HonkRecursionConstraint const& lhs, HonkRecursionConstraint const& rhs) = default; +}; + +std::array create_honk_recursion_constraints( + Builder& builder, + const HonkRecursionConstraint& input, + std::array input_aggregation_object, + std::array nested_aggregation_object, + bool has_valid_witness_assignments = false); + +std::vector export_honk_key_in_recursion_format(std::shared_ptr const& vkey); +std::vector export_dummy_honk_key_in_recursion_format(const PolynomialManifest& polynomial_manifest, + bool contains_recursive_proof = 0); + +std::vector export_honk_transcript_in_recursion_format(const transcript::StandardTranscript& transcript); +std::vector export_dummy_honk_transcript_in_recursion_format(const transcript::Manifest& manifest, + const bool contains_recursive_proof); +size_t recursion_honk_proof_size_without_public_inputs(); + +} // namespace acir_format diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.test.cpp new file mode 100644 index 00000000000..7ac1fc58eb0 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/honk_recursion_constraint.test.cpp @@ -0,0 +1,365 @@ +#include "honk_recursion_constraint.hpp" +#include "acir_format.hpp" +#include "barretenberg/plonk/proof_system/types/proof.hpp" +#include "barretenberg/plonk/proof_system/verification_key/verification_key.hpp" + +#include +#include + +using namespace acir_format; +using namespace bb::plonk; + +class AcirHonkRecursionConstraint : public ::testing::Test { + public: + Builder create_inner_circuit() + { + /** + * constraints produced by Noir program: + * fn main(x : u32, y : pub u32) { + * let z = x ^ y; + * + * constrain z != 10; + * } + **/ + RangeConstraint range_a{ + .witness = 0, + .num_bits = 32, + }; + RangeConstraint range_b{ + .witness = 1, + .num_bits = 32, + }; + + LogicConstraint logic_constraint{ + .a = 0, + .b = 1, + .result = 2, + .num_bits = 32, + .is_xor_gate = 1, + }; + poly_triple expr_a{ + .a = 2, + .b = 3, + .c = 0, + .q_m = 0, + .q_l = 1, + .q_r = -1, + .q_o = 0, + .q_c = -10, + }; + poly_triple expr_b{ + .a = 3, + .b = 4, + .c = 5, + .q_m = 1, + .q_l = 0, + .q_r = 0, + .q_o = -1, + .q_c = 0, + }; + poly_triple expr_c{ + .a = 3, + .b = 5, + .c = 3, + .q_m = 1, + .q_l = 0, + .q_r = 0, + .q_o = -1, + .q_c = 0, + + }; + poly_triple expr_d{ + .a = 5, + .b = 0, + .c = 0, + .q_m = 0, + .q_l = -1, + .q_r = 0, + .q_o = 0, + .q_c = 1, + }; + + AcirFormat constraint_system{ .varnum = 6, + .recursive = true, + .num_acir_opcodes = 7, + .public_inputs = { 1, 2 }, + .logic_constraints = { logic_constraint }, + .range_constraints = { range_a, range_b }, + .aes128_constraints = {}, + .sha256_constraints = {}, + .sha256_compression = {}, + .schnorr_constraints = {}, + .ecdsa_k1_constraints = {}, + .ecdsa_r1_constraints = {}, + .blake2s_constraints = {}, + .blake3_constraints = {}, + .keccak_constraints = {}, + .keccak_permutations = {}, + .pedersen_constraints = {}, + .pedersen_hash_constraints = {}, + .poseidon2_constraints = {}, + .multi_scalar_mul_constraints = {}, + .ec_add_constraints = {}, + .recursion_constraints = {}, + .honk_recursion_constraints = {}, + .bigint_from_le_bytes_constraints = {}, + .bigint_to_le_bytes_constraints = {}, + .bigint_operations = {}, + .poly_triple_constraints = { expr_a, expr_b, expr_c, expr_d }, + .quad_constraints = {}, + .block_constraints = {} }; + + uint256_t inverse_of_five = fr(5).invert(); + WitnessVector witness{ + 5, 10, 15, 5, inverse_of_five, 1, + }; + auto builder = create_circuit(constraint_system, /*size_hint*/ 0, witness, /*honk recursion*/ true); + + return builder; + } + + /** + * @brief Create a circuit that recursively verifies one or more inner circuits + * + * @param inner_circuits + * @return Composer + */ + Builder create_outer_circuit(std::vector& inner_circuits) + { + std::vector honk_recursion_constraints; + + size_t witness_offset = 0; + std::vector> witness; + + for (auto& inner_circuit : inner_circuits) { + + auto inner_composer = Composer(); + auto inner_prover = inner_composer.create_prover(inner_circuit); + auto inner_proof = inner_prover.construct_proof(); + auto inner_verifier = inner_composer.create_verifier(inner_circuit); + + const size_t num_inner_public_inputs = inner_circuit.get_public_inputs().size(); + transcript::StandardTranscript transcript(inner_proof.proof_data, + Composer::create_manifest(num_inner_public_inputs), + transcript::HashType::PedersenBlake3s, + 16); + + std::vector proof_witnesses = export_honk_transcript_in_recursion_format(transcript); + // - Save the public inputs so that we can set their values. + // - Then truncate them from the proof because the ACIR API expects proofs without public inputs + std::vector inner_public_input_values( + proof_witnesses.begin(), + proof_witnesses.begin() + static_cast(num_inner_public_inputs - + RecursionConstraint::AGGREGATION_OBJECT_SIZE)); + + // We want to make sure that we do not remove the nested aggregation object. + proof_witnesses.erase(proof_witnesses.begin(), + proof_witnesses.begin() + + static_cast(num_inner_public_inputs - + RecursionConstraint::AGGREGATION_OBJECT_SIZE)); + + std::vector key_witnesses = export_honk_key_in_recursion_format(inner_verifier.key); + bb::fr key_hash = key_witnesses.back(); + key_witnesses.pop_back(); + + const uint32_t key_hash_start_idx = static_cast(witness_offset); + const uint32_t public_input_start_idx = key_hash_start_idx + 1; + const uint32_t proof_indices_start_idx = static_cast( + public_input_start_idx + num_inner_public_inputs - RecursionConstraint::AGGREGATION_OBJECT_SIZE); + const uint32_t key_indices_start_idx = + static_cast(proof_indices_start_idx + proof_witnesses.size()); + + std::vector proof_indices; + std::vector key_indices; + std::vector inner_public_inputs; + for (size_t i = 0; i < proof_witnesses.size(); ++i) { + proof_indices.emplace_back(static_cast(i + proof_indices_start_idx)); + } + const size_t key_size = key_witnesses.size(); + for (size_t i = 0; i < key_size; ++i) { + key_indices.emplace_back(static_cast(i + key_indices_start_idx)); + } + // We keep the nested aggregation object attached to the proof, + // thus we do not explicitly have to keep the public inputs while setting up the initial recursion + // constraint. They will later be attached as public inputs when creating the circuit. + for (size_t i = 0; i < num_inner_public_inputs - RecursionConstraint::AGGREGATION_OBJECT_SIZE; ++i) { + inner_public_inputs.push_back(static_cast(i + public_input_start_idx)); + } + + HonkRecursionConstraint honk_recursion_constraint{ + .key = key_indices, + .proof = proof_indices, + .public_inputs = inner_public_inputs, + .key_hash = key_hash_start_idx, + }; + honk_recursion_constraints.push_back(honk_recursion_constraint); + + witness.emplace_back(key_hash); + for (size_t i = 0; i < proof_indices_start_idx - public_input_start_idx; ++i) { + witness.emplace_back(0); + } + for (const auto& wit : proof_witnesses) { + witness.emplace_back(wit); + } + + for (const auto& wit : key_witnesses) { + witness.emplace_back(wit); + } + + // Set the values for the inner public inputs + // TODO(maxim): check this is wrong I think + // Note: this is confusing, but we minus one here due to the fact that the + // witness values have not taken into account that zero is taken up by the zero_idx + // + // We once again have to check whether we have a nested proof, because if we do have one + // then we could get a segmentation fault as `inner_public_inputs` was never filled with values. + for (size_t i = 0; i < num_inner_public_inputs - RecursionConstraint::AGGREGATION_OBJECT_SIZE; ++i) { + witness[inner_public_inputs[i]] = inner_public_input_values[i]; + } + + witness_offset = key_indices_start_idx + key_witnesses.size(); + } + + AcirFormat constraint_system{ .varnum = static_cast(witness.size()), + .recursive = false, + .num_acir_opcodes = static_cast(honk_recursion_constraints.size()), + .public_inputs = {}, + .logic_constraints = {}, + .range_constraints = {}, + .aes128_constraints = {}, + .sha256_constraints = {}, + .sha256_compression = {}, + .schnorr_constraints = {}, + .ecdsa_k1_constraints = {}, + .ecdsa_r1_constraints = {}, + .blake2s_constraints = {}, + .blake3_constraints = {}, + .keccak_constraints = {}, + .keccak_permutations = {}, + .pedersen_constraints = {}, + .pedersen_hash_constraints = {}, + .poseidon2_constraints = {}, + .multi_scalar_mul_constraints = {}, + .ec_add_constraints = {}, + .recursion_constraints = {}, + .honk_recursion_constraints = honk_recursion_constraints, + .bigint_from_le_bytes_constraints = {}, + .bigint_to_le_bytes_constraints = {}, + .bigint_operations = {}, + .poly_triple_constraints = {}, + .quad_constraints = {}, + .block_constraints = {} }; + + auto outer_circuit = create_circuit(constraint_system, /*size_hint*/ 0, witness, /*honk recursion*/ true); + + return outer_circuit; + } + + protected: + static void SetUpTestSuite() { bb::srs::init_crs_factory("../srs_db/ignition"); } +}; + +TEST_F(AcirHonkRecursionConstraint, TestBasicDoubleHonkRecursionConstraints) +{ + std::vector layer_1_circuits; + layer_1_circuits.push_back(create_inner_circuit()); + + layer_1_circuits.push_back(create_inner_circuit()); + + auto layer_2_circuit = create_outer_circuit(layer_1_circuits); + + info("circuit gates = ", layer_2_circuit.get_num_gates()); + + auto layer_2_composer = Composer(); + auto prover = layer_2_composer.create_ultra_with_keccak_prover(layer_2_circuit); + info("prover gates = ", prover.circuit_size); + auto proof = prover.construct_proof(); + auto verifier = layer_2_composer.create_ultra_with_keccak_verifier(layer_2_circuit); + EXPECT_EQ(verifier.verify_proof(proof), true); +} + +TEST_F(AcirHonkRecursionConstraint, TestOneOuterRecursiveCircuit) +{ + /** + * We want to test the following: + * 1. circuit that verifies a proof of another circuit + * 2. the above, but the inner circuit contains a recursive proof output that we have to aggregate + * 3. the above, but the outer circuit verifies 2 proofs, the aggregation outputs from the 2 proofs (+ the recursive + * proof output from 2) are aggregated together + * + * A = basic circuit + * B = circuit that verifies proof of A + * C = circuit that verifies proof of B and a proof of A + * + * Layer 1 = proof of A + * Layer 2 = verifies proof of A and proof of B + * Layer 3 = verifies proof of C + * + * Attempt at a visual graphic + * =========================== + * + * C + * ^ + * | + * | - B + * ^ ^ + * | | + * | -A + * | + * - A + * + * =========================== + * + * Final aggregation object contains aggregated proofs for 2 instances of A and 1 instance of B + */ + std::vector layer_1_circuits; + layer_1_circuits.push_back(create_inner_circuit()); + info("created first inner circuit"); + + std::vector layer_2_circuits; + layer_2_circuits.push_back(create_inner_circuit()); + info("created second inner circuit"); + + layer_2_circuits.push_back(create_outer_circuit(layer_1_circuits)); + info("created first outer circuit"); + + auto layer_3_circuit = create_outer_circuit(layer_2_circuits); + info("created second outer circuit"); + info("number of gates in layer 3 = ", layer_3_circuit.get_num_gates()); + + auto layer_3_composer = Composer(); + auto prover = layer_3_composer.create_ultra_with_keccak_prover(layer_3_circuit); + info("prover gates = ", prover.circuit_size); + auto proof = prover.construct_proof(); + auto verifier = layer_3_composer.create_ultra_with_keccak_verifier(layer_3_circuit); + EXPECT_EQ(verifier.verify_proof(proof), true); +} + +TEST_F(AcirHonkRecursionConstraint, TestFullRecursiveComposition) +{ + std::vector layer_b_1_circuits; + layer_b_1_circuits.push_back(create_inner_circuit()); + info("created first inner circuit"); + + std::vector layer_b_2_circuits; + layer_b_2_circuits.push_back(create_inner_circuit()); + info("created second inner circuit"); + + std::vector layer_2_circuits; + layer_2_circuits.push_back(create_outer_circuit(layer_b_1_circuits)); + info("created first outer circuit"); + + layer_2_circuits.push_back(create_outer_circuit(layer_b_2_circuits)); + info("created second outer circuit"); + + auto layer_3_circuit = create_outer_circuit(layer_2_circuits); + info("created third outer circuit"); + info("number of gates in layer 3 circuit = ", layer_3_circuit.get_num_gates()); + + auto layer_3_composer = Composer(); + auto prover = layer_3_composer.create_ultra_with_keccak_prover(layer_3_circuit); + info("prover gates = ", prover.circuit_size); + auto proof = prover.construct_proof(); + auto verifier = layer_3_composer.create_ultra_with_keccak_verifier(layer_3_circuit); + EXPECT_EQ(verifier.verify_proof(proof), true); +} diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/poseidon2_constraint.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/poseidon2_constraint.test.cpp index 4922c63cd69..71e2cc2160f 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/poseidon2_constraint.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/poseidon2_constraint.test.cpp @@ -51,6 +51,7 @@ TEST_F(Poseidon2Tests, TestPoseidon2Permutation) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.test.cpp index b837f94ba2a..65e049fe0ca 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.test.cpp @@ -103,6 +103,7 @@ Builder create_inner_circuit() .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, @@ -130,13 +131,9 @@ Builder create_outer_circuit(std::vector& inner_circuits) std::vector recursion_constraints; size_t witness_offset = 0; - std::array output_aggregation_object; std::vector> witness; - size_t circuit_idx = 0; for (auto& inner_circuit : inner_circuits) { - const bool has_input_aggregation_object = circuit_idx > 0; - auto inner_composer = Composer(); auto inner_prover = inner_composer.create_prover(inner_circuit); auto inner_proof = inner_prover.construct_proof(); @@ -162,33 +159,25 @@ Builder create_outer_circuit(std::vector& inner_circuits) if (!has_nested_proof) { proof_witnesses.erase(proof_witnesses.begin(), proof_witnesses.begin() + static_cast(num_inner_public_inputs)); + } else { + proof_witnesses.erase(proof_witnesses.begin(), + proof_witnesses.begin() + + static_cast(num_inner_public_inputs - + RecursionConstraint::AGGREGATION_OBJECT_SIZE)); } const std::vector key_witnesses = export_key_in_recursion_format(inner_verifier.key); const uint32_t key_hash_start_idx = static_cast(witness_offset); const uint32_t public_input_start_idx = key_hash_start_idx + 1; - const uint32_t output_aggregation_object_start_idx = - static_cast(public_input_start_idx + num_inner_public_inputs + (has_nested_proof ? 16 : 0)); - const uint32_t proof_indices_start_idx = output_aggregation_object_start_idx + 16; + const uint32_t proof_indices_start_idx = + static_cast(public_input_start_idx + num_inner_public_inputs - + (has_nested_proof ? RecursionConstraint::AGGREGATION_OBJECT_SIZE : 0)); const uint32_t key_indices_start_idx = static_cast(proof_indices_start_idx + proof_witnesses.size()); std::vector proof_indices; std::vector key_indices; std::vector inner_public_inputs; - std::array input_aggregation_object = {}; - std::array nested_aggregation_object = {}; - if (has_input_aggregation_object) { - input_aggregation_object = output_aggregation_object; - } - for (size_t i = 0; i < 16; ++i) { - output_aggregation_object[i] = (static_cast(i + output_aggregation_object_start_idx)); - } - if (has_nested_proof) { - for (size_t i = 0; i < 16; ++i) { - nested_aggregation_object[i] = inner_circuit.recursive_proof_public_input_indices[i]; - } - } for (size_t i = 0; i < proof_witnesses.size(); ++i) { proof_indices.emplace_back(static_cast(i + proof_indices_start_idx)); } @@ -203,6 +192,10 @@ Builder create_outer_circuit(std::vector& inner_circuits) for (size_t i = 0; i < num_inner_public_inputs; ++i) { inner_public_inputs.push_back(static_cast(i + public_input_start_idx)); } + } else { + for (size_t i = 0; i < num_inner_public_inputs - RecursionConstraint::AGGREGATION_OBJECT_SIZE; ++i) { + inner_public_inputs.push_back(static_cast(i + public_input_start_idx)); + } } RecursionConstraint recursion_constraint{ @@ -234,10 +227,13 @@ Builder create_outer_circuit(std::vector& inner_circuits) for (size_t i = 0; i < num_inner_public_inputs; ++i) { witness[inner_public_inputs[i]] = inner_public_input_values[i]; } + } else { + for (size_t i = 0; i < num_inner_public_inputs - RecursionConstraint::AGGREGATION_OBJECT_SIZE; ++i) { + witness[inner_public_inputs[i]] = inner_public_input_values[i]; + } } witness_offset = key_indices_start_idx + key_witnesses.size(); - circuit_idx++; } AcirFormat constraint_system{ .varnum = static_cast(witness.size()), @@ -262,6 +258,7 @@ Builder create_outer_circuit(std::vector& inner_circuits) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = recursion_constraints, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/dsl/acir_format/sha256_constraint.test.cpp b/barretenberg/cpp/src/barretenberg/dsl/acir_format/sha256_constraint.test.cpp index 5af032bedd1..82fda6f8d81 100644 --- a/barretenberg/cpp/src/barretenberg/dsl/acir_format/sha256_constraint.test.cpp +++ b/barretenberg/cpp/src/barretenberg/dsl/acir_format/sha256_constraint.test.cpp @@ -53,6 +53,7 @@ TEST_F(Sha256Tests, TestSha256Compression) .multi_scalar_mul_constraints = {}, .ec_add_constraints = {}, .recursion_constraints = {}, + .honk_recursion_constraints = {}, .bigint_from_le_bytes_constraints = {}, .bigint_to_le_bytes_constraints = {}, .bigint_operations = {}, diff --git a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/bigfield.hpp b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/bigfield.hpp index 2fc3572cec3..e015988c5c3 100644 --- a/barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/bigfield.hpp +++ b/barretenberg/cpp/src/barretenberg/stdlib/primitives/bigfield/bigfield.hpp @@ -48,6 +48,11 @@ template class bigfield { field_t element; uint256_t maximum_value; }; + static constexpr size_t NUM_LIMBS = 4; + + Builder* context; + mutable Limb binary_basis_limbs[NUM_LIMBS]; + mutable field_t prime_basis_limb; bigfield(const field_t& low_bits, const field_t& high_bits, @@ -121,11 +126,11 @@ template class bigfield { static constexpr uint256_t DEFAULT_MAXIMUM_LIMB = (uint256_t(1) << NUM_LIMB_BITS) - uint256_t(1); static constexpr uint256_t DEFAULT_MAXIMUM_MOST_SIGNIFICANT_LIMB = (uint256_t(1) << NUM_LAST_LIMB_BITS) - uint256_t(1); - static constexpr uint64_t LOG2_BINARY_MODULUS = NUM_LIMB_BITS * 4; + static constexpr uint64_t LOG2_BINARY_MODULUS = NUM_LIMB_BITS * NUM_LIMBS; static constexpr bool is_composite = true; // false only when fr is native static constexpr uint256_t prime_basis_maximum_limb = - uint256_t(modulus_u512.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4)); + uint256_t(modulus_u512.slice(NUM_LIMB_BITS * (NUM_LIMBS - 1), NUM_LIMB_BITS* NUM_LIMBS)); static constexpr Basis prime_basis{ uint512_t(bb::fr::modulus), bb::fr::modulus.get_msb() + 1 }; static constexpr Basis binary_basis{ uint512_t(1) << LOG2_BINARY_MODULUS, LOG2_BINARY_MODULUS }; static constexpr Basis target_basis{ modulus_u512, modulus_u512.get_msb() + 1 }; @@ -136,13 +141,13 @@ template class bigfield { static constexpr bb::fr shift_right_2 = bb::fr(1) / shift_2; static constexpr bb::fr negative_prime_modulus_mod_binary_basis = -bb::fr(uint256_t(modulus_u512)); static constexpr uint512_t negative_prime_modulus = binary_basis.modulus - target_basis.modulus; - static constexpr uint256_t neg_modulus_limbs_u256[4]{ + static constexpr uint256_t neg_modulus_limbs_u256[NUM_LIMBS]{ uint256_t(negative_prime_modulus.slice(0, NUM_LIMB_BITS).lo), uint256_t(negative_prime_modulus.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo), uint256_t(negative_prime_modulus.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo), uint256_t(negative_prime_modulus.slice(NUM_LIMB_BITS * 3, NUM_LIMB_BITS * 4).lo), }; - static constexpr bb::fr neg_modulus_limbs[4]{ + static constexpr bb::fr neg_modulus_limbs[NUM_LIMBS]{ bb::fr(negative_prime_modulus.slice(0, NUM_LIMB_BITS).lo), bb::fr(negative_prime_modulus.slice(NUM_LIMB_BITS, NUM_LIMB_BITS * 2).lo), bb::fr(negative_prime_modulus.slice(NUM_LIMB_BITS * 2, NUM_LIMB_BITS * 3).lo), @@ -428,9 +433,6 @@ template class bigfield { static constexpr uint256_t get_maximum_unreduced_limb_value() { return uint256_t(1) << MAX_UNREDUCED_LIMB_SIZE; } static_assert(MAX_UNREDUCED_LIMB_SIZE < (NUM_LIMB_BITS * 2)); - Builder* context; - mutable Limb binary_basis_limbs[4]; - mutable field_t prime_basis_limb; private: static std::pair compute_quotient_remainder_values(const bigfield& a,