Skip to content

Commit

Permalink
feat: laying out a new recursion constraint for honk (#6489)
Browse files Browse the repository at this point in the history
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 #6087.

This PR is mostly for setup for AztecProtocol/barretenberg#933.
  • Loading branch information
lucasxia01 committed May 17, 2024
1 parent f360b3f commit af9fea4
Show file tree
Hide file tree
Showing 16 changed files with 1,011 additions and 37 deletions.
7 changes: 7 additions & 0 deletions barretenberg/acir_tests/reset_acir_tests.sh
Original file line number Diff line number Diff line change
@@ -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
137 changes: 130 additions & 7 deletions barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,10 @@ template class DSLBigInts<UltraCircuitBuilder>;
template class DSLBigInts<GoblinUltraCircuitBuilder>;

template <typename Builder>
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) {
Expand Down Expand Up @@ -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<Builder>) {
Expand Down Expand Up @@ -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);
}
Expand Down Expand Up @@ -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<Builder>) {
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<uint32_t, HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE> 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<uint32_t, HonkRecursionConstraint::AGGREGATION_OBJECT_SIZE> 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<uint32_t>(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<std::ptrdiff_t>(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<uint32_t> 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<fq> 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<bb::fr, fq_ct::NUM_LIMBS> 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<uint32_t> proof_output_witness_indices(current_aggregation_object.begin(),
current_aggregation_object.end());
builder.set_recursive_proof(proof_output_witness_indices);
}
}
}

/**
Expand All @@ -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();

Expand All @@ -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<ECCOpQueue>(); // instantiate empty op_queue
Expand All @@ -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>(GoblinUltraCircuitBuilder&, AcirFormat const&, bool);
template void build_constraints<GoblinUltraCircuitBuilder>(GoblinUltraCircuitBuilder&, AcirFormat const&, bool, bool);

} // namespace acir_format
15 changes: 13 additions & 2 deletions barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -54,6 +55,7 @@ struct AcirFormat {
std::vector<MultiScalarMul> multi_scalar_mul_constraints;
std::vector<EcAdd> ec_add_constraints;
std::vector<RecursionConstraint> recursion_constraints;
std::vector<HonkRecursionConstraint> honk_recursion_constraints;
std::vector<BigIntFromLeBytes> bigint_from_le_bytes_constraints;
std::vector<BigIntToLeBytes> bigint_to_le_bytes_constraints;
std::vector<BigIntOperation> bigint_operations;
Expand Down Expand Up @@ -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,
Expand All @@ -102,9 +105,17 @@ using WitnessVector = std::vector<fr, ContainerSlabAllocator<fr>>;
using WitnessVectorStack = std::vector<std::pair<uint32_t, WitnessVector>>;

template <typename Builder = UltraCircuitBuilder>
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 <typename Builder>
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
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 = {},
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 },
Expand Down Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 },
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {},
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {},
Expand Down Expand Up @@ -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 = {},
Expand Down
Loading

0 comments on commit af9fea4

Please sign in to comment.