Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore(dsl): Abstract nested aggregation object from ACIR #3765

Merged
merged 27 commits into from
Dec 21, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
b4d82ff
add comment about `add_recursive_proof` being suspicious
kevaundray Dec 3, 2023
ac146a4
create and process input_aggregation object and output_aggregation_ob…
kevaundray Dec 3, 2023
92e247d
`create_recursion_constraints` now takes in the input and nested aggr…
kevaundray Dec 3, 2023
f36661d
add comment on removing the is_recursive flag
kevaundray Dec 3, 2023
738fb17
modify `create_recursion_constraints` to append the public inputs to …
kevaundray Dec 3, 2023
cab6ef6
update double_verify_proof program
kevaundray Dec 3, 2023
7a4e9be
update double_verify_proof
kevaundray Dec 3, 2023
7acd611
fix: set input_aggregation for next iteration
kevaundray Dec 3, 2023
a85ba41
fix: remove public inputs from proof
kevaundray Dec 3, 2023
c11d812
set the public input values for the inner circuit in tests
kevaundray Dec 4, 2023
c589331
fix: remove output aggregation being set as public input twice
kevaundray Dec 4, 2023
40eaf29
Merge branch 'master' into kw/modify-recursion-interface
kevaundray Dec 4, 2023
19ae424
Merge branch 'master' into kw/modify-recursion-interface
kevaundray Dec 5, 2023
d0065a3
Merge branch 'master' into kw/modify-recursion-interface
kevaundray Dec 7, 2023
12baf28
Merge branch 'master' into kw/modify-recursion-interface
kevaundray Dec 9, 2023
50666b8
Merge branch 'master' into kw/modify-recursion-interface
kevaundray Dec 16, 2023
ebcdc29
Update noir/test_programs/execution_success/double_verify_proof/src/m…
kevaundray Dec 18, 2023
e8aec35
Merge branch 'master' into kw/modify-recursion-interface
kevaundray Dec 18, 2023
5cb0181
merge conflicts w/ master after 3729
vezenovm Dec 19, 2023
a8cf735
move nested_aggregation_object to be a part of the proof
vezenovm Dec 21, 2023
6a05231
cleanup test prints
vezenovm Dec 21, 2023
50b486f
more print cleanup
vezenovm Dec 21, 2023
c77c0e5
merge w/ master
vezenovm Dec 21, 2023
b6e4699
last little cleanup
vezenovm Dec 21, 2023
0da144e
cleanup and remove old testing code
vezenovm Dec 21, 2023
8b5c39a
bring back prover gate counts:
vezenovm Dec 21, 2023
09dfc2c
rename transcript_in_recursion_format_size to recursion_proof_size_wi…
vezenovm Dec 21, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
66 changes: 50 additions & 16 deletions barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include "barretenberg/dsl/acir_format/pedersen.hpp"
#include "barretenberg/dsl/acir_format/recursion_constraint.hpp"
#include "barretenberg/proof_system/circuit_builder/ultra_circuit_builder.hpp"
#include <cstddef>

namespace acir_format {

Expand Down Expand Up @@ -158,24 +159,56 @@ void build_constraints(Builder& builder, acir_format const& constraint_system, b
// These are set and modified whenever we encounter a recursion opcode
//
// These should not be set by the caller
// TODO: Check if this is always the case. ie I won't receive a proof that will set the first
// TODO input_aggregation_object to be non-zero.
// TODO: if not, we can add input_aggregation_object to the proof too for all recursive proofs
// TODO: This might be the case for proof trees where the proofs are created on different machines
// 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, RecursionConstraint::AGGREGATION_OBJECT_SIZE> current_input_aggregation_object = {
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
};
std::array<uint32_t, RecursionConstraint::AGGREGATION_OBJECT_SIZE> current_output_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_proof_size_without_public_inputs();

// Add recursion constraints
for (size_t i = 0; i < constraint_system.recursion_constraints.size(); ++i) {
auto& constraint = constraint_system.recursion_constraints[i];
for (auto constraint : constraint_system.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, RecursionConstraint::AGGREGATION_OBJECT_SIZE> nested_aggregation_object = {};
// If the proof has public inputs attached to it, we should handle setting the nested aggregation object
if (constraint.proof.size() > proof_size_no_pub_inputs) {
// The public inputs attached to a proof should match the aggregation object in size
ASSERT(constraint.proof.size() - proof_size_no_pub_inputs ==
RecursionConstraint::AGGREGATION_OBJECT_SIZE);
for (size_t i = 0; i < RecursionConstraint::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>(RecursionConstraint::AGGREGATION_OBJECT_SIZE));
}

current_output_aggregation_object = create_recursion_constraints(builder,
constraint,
current_input_aggregation_object,
constraint.nested_aggregation_object,
nested_aggregation_object,
has_valid_witness_assignments);
current_input_aggregation_object = current_output_aggregation_object;
}
Expand Down Expand Up @@ -241,25 +274,26 @@ void create_circuit_with_witness(Builder& builder, acir_format const& constraint

/**
* @brief Apply an offset to the indices stored in the wires
* @details This method is needed due to the following: Noir constructs "wires" as indices into a "witness" vector. This
* is analogous to the wires and variables vectors in bberg builders. Were it not for the addition of constant variables
* in the constructors of a builder (e.g. zero), we would simply have noir.wires = builder.wires and noir.witness =
* builder.variables. To account for k-many constant variables in the first entries of the variables array, we have
* something like variables = variables.append(noir.witness). Accordingly, the indices in noir.wires have to be
* incremented to account for the offset at which noir.wires was placed into variables.
* @details This method is needed due to the following: Noir constructs "wires" as indices into a "witness" vector.
* This is analogous to the wires and variables vectors in bberg builders. Were it not for the addition of constant
* variables in the constructors of a builder (e.g. zero), we would simply have noir.wires = builder.wires and
* noir.witness = builder.variables. To account for k-many constant variables in the first entries of the variables
* array, we have something like variables = variables.append(noir.witness). Accordingly, the indices in noir.wires
* have to be incremented to account for the offset at which noir.wires was placed into variables.
*
* @tparam Builder
* @param builder
*/
template <typename Builder> void apply_wire_index_offset(Builder& builder)
{
// For now, noir has a hard coded witness index offset = 1. Once this is removed, this pre-applied offset goes away
// For now, noir has a hard coded witness index offset = 1. Once this is removed, this pre-applied offset goes
// away
const uint32_t pre_applied_noir_offset = 1;
auto offset = static_cast<uint32_t>(builder.num_vars_added_in_constructor - pre_applied_noir_offset);
info("Applying offset = ", offset);

// Apply the offset to the indices stored the wires that were generated from acir. (Do not apply the offset to those
// values that were added in the builder constructor).
// Apply the offset to the indices stored the wires that were generated from acir. (Do not apply the offset to
// those values that were added in the builder constructor).
size_t start_index = builder.num_vars_added_in_constructor;
for (auto& wire : builder.wires) {
for (size_t idx = start_index; idx < wire.size(); ++idx) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,6 @@ std::array<uint32_t, RecursionConstraint::AGGREGATION_OBJECT_SIZE> create_recurs
Builder& builder,
const RecursionConstraint& input,
std::array<uint32_t, RecursionConstraint::AGGREGATION_OBJECT_SIZE> input_aggregation_object,
// TODO: does this need to be a part of the recursion opcode?
// TODO: or can we figure it out from the vk?
// TODO: either way we could probably have the user explicitly provide it
// TODO: in Noir.
// Note: this is not being used in Noir at the moment
std::array<uint32_t, RecursionConstraint::AGGREGATION_OBJECT_SIZE> nested_aggregation_object,
bool has_valid_witness_assignments)
{
Expand Down Expand Up @@ -141,6 +136,7 @@ std::array<uint32_t, RecursionConstraint::AGGREGATION_OBJECT_SIZE> create_recurs
std::shared_ptr<verification_key_ct> 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 = proof_system::plonk::stdlib::recursion::verify_proof_<bn254, noir_recursive_settings>(
&builder, vkey, transcript, previous_aggregation);
Expand Down Expand Up @@ -358,6 +354,13 @@ std::vector<barretenberg::fr> export_dummy_transcript_in_recursion_format(const
return fields;
}

size_t recursion_proof_size_without_public_inputs()
{
const auto manifest = Composer::create_manifest(0);
auto dummy_transcript = export_dummy_transcript_in_recursion_format(manifest, false);
return dummy_transcript.size();
}

G1AsFields export_g1_affine_element_as_fields(const barretenberg::g1::affine_element& group_element)
{
const uint256_t x = group_element.x;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -53,13 +53,14 @@ struct RecursionConstraint {
std::vector<uint32_t> proof;
std::vector<uint32_t> public_inputs;
uint32_t key_hash;
// TODO:This is now unused, but we keep it here for backwards compatibility
// TODO(maxim):This is now unused, but we keep it here for backwards compatibility
std::array<uint32_t, AGGREGATION_OBJECT_SIZE> input_aggregation_object;
// TODO: This is now unused, but we keep it here for backwards compatibility
// TODO(maxim): This is now unused, but we keep it here for backwards compatibility
std::array<uint32_t, AGGREGATION_OBJECT_SIZE> output_aggregation_object;
// TODO: This is currently not being used on the Noir level at all
// TODO: we don't have a way to specify that the proof we are creating contains a
// TODO: aggregation object (ie it is also verifying a proof)
// TODO(maxim): This is currently not being used on the Noir level at all,
// TODO(maxim): but we keep it here for backwards compatibility
// TODO(maxim): The object is now currently contained by the `proof` field
// TODO(maxim): and is handled when serializing ACIR to a barretenberg circuit
std::array<uint32_t, AGGREGATION_OBJECT_SIZE> nested_aggregation_object;

friend bool operator==(RecursionConstraint const& lhs, RecursionConstraint const& rhs) = default;
Expand All @@ -79,6 +80,7 @@ std::vector<barretenberg::fr> export_dummy_key_in_recursion_format(const Polynom
std::vector<barretenberg::fr> export_transcript_in_recursion_format(const transcript::StandardTranscript& transcript);
std::vector<barretenberg::fr> export_dummy_transcript_in_recursion_format(const transcript::Manifest& manifest,
const bool contains_recursive_proof);
size_t recursion_proof_size_without_public_inputs();

// In order to interact with a recursive aggregation state inside of a circuit, we need to represent its internal G1
// elements as field elements. This happens in multiple locations when creating a recursion constraint. The struct and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -139,8 +139,8 @@ Builder create_outer_circuit(std::vector<Builder>& inner_circuits)
auto inner_verifier = inner_composer.create_verifier(inner_circuit);

const bool has_nested_proof = inner_verifier.key->contains_recursive_proof;
const size_t num_inner_public_inputs = inner_circuit.get_public_inputs().size();

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,
Expand All @@ -149,11 +149,16 @@ Builder create_outer_circuit(std::vector<Builder>& inner_circuits)
std::vector<barretenberg::fr> proof_witnesses = export_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<barretenberg::fr> inner_public_input_values(
proof_witnesses.begin(), proof_witnesses.begin() + static_cast<std::ptrdiff_t>(num_inner_public_inputs));
proof_witnesses.erase(proof_witnesses.begin(),
proof_witnesses.begin() + static_cast<std::ptrdiff_t>(num_inner_public_inputs));

// We want to make sure that we do not remove the nested aggregation object in the case of the proof we want to
// recursively verify contains a recursive proof itself. We are safe to keep all the inner public inputs
// as in these tests the outer circuits do not have public inputs themselves
if (!has_nested_proof) {
proof_witnesses.erase(proof_witnesses.begin(),
proof_witnesses.begin() + static_cast<std::ptrdiff_t>(num_inner_public_inputs));
}

const std::vector<barretenberg::fr> key_witnesses = export_key_in_recursion_format(inner_verifier.key);

Expand Down Expand Up @@ -187,8 +192,13 @@ Builder create_outer_circuit(std::vector<Builder>& inner_circuits)
for (size_t i = 0; i < key_size; ++i) {
key_indices.emplace_back(static_cast<uint32_t>(i + key_indices_start_idx));
}
for (size_t i = 0; i < num_inner_public_inputs; ++i) {
inner_public_inputs.push_back(static_cast<uint32_t>(i + public_input_start_idx));
// In the case of a nested proof 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.
if (!has_nested_proof) {
for (size_t i = 0; i < num_inner_public_inputs; ++i) {
inner_public_inputs.push_back(static_cast<uint32_t>(i + public_input_start_idx));
}
}

RecursionConstraint recursion_constraint{
Expand All @@ -201,21 +211,30 @@ Builder create_outer_circuit(std::vector<Builder>& inner_circuits)
.nested_aggregation_object = nested_aggregation_object,
};
recursion_constraints.push_back(recursion_constraint);

for (size_t i = 0; i < proof_indices_start_idx - witness_offset; ++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
// 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
for (size_t i = 0; i < num_inner_public_inputs; ++i) {
witness[inner_public_inputs[i] - 1] = inner_public_input_values[i];
//
// 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.
if (!has_nested_proof) {
for (size_t i = 0; i < num_inner_public_inputs; ++i) {
witness[inner_public_inputs[i] - 1] = inner_public_input_values[i];
}
}

witness_offset = key_indices_start_idx + key_witnesses.size();
circuit_idx++;
}
Expand Down