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.

Sign up for GitHub

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

feat(dsl)!: Arbitrary depth recursion #433

Merged
merged 17 commits into from
May 16, 2023
Merged

feat(dsl)!: Arbitrary depth recursion #433

Show file tree
Hide file tree
Changes from 16 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
8599781
merge conflicts and small updates to get acir_proofs test passing wit…
vezenovm May 3, 2023
c1a4367
inline with mv/noir-recursion and working double recursion acir_proof…
vezenovm May 5, 2023
b434c37
cleanup and working towards supporting full nested proofs, still some…
vezenovm May 5, 2023
cd0c726
full recursive composition test working in acir_proofs
vezenovm May 5, 2023
fe8cec5
use two public inptus for inner circuit
vezenovm May 5, 2023
80fcac5
Merge branch 'mv/noir-recursion' into mv/noir-arbitrary-recursion
vezenovm May 5, 2023
371cb4f
Merge branch 'mv/noir-recursion' into mv/noir-arbitrary-recursion
vezenovm May 5, 2023
ad59820
delete commented out unnecessary acir proofs method
vezenovm May 5, 2023
e65950d
made dummy transcript points unique to prevent point collisions
zac-williamson May 7, 2023
a523906
handle nested proofs when exporting dummy transcript, export recursiv…
vezenovm May 12, 2023
dcfcbd9
update bindings on verify_recursive_proof to accept num public inputs
vezenovm May 15, 2023
231c0be
missing acir_format field in tests
vezenovm May 15, 2023
bc6e5c7
missing one more correct acir_format struct in recursion constraint test
vezenovm May 15, 2023
48c8659
merge conflicts with mv/noir-recursion
vezenovm May 15, 2023
82347ce
cleanup and additional comment for recursion_constraint
vezenovm May 15, 2023
9753e44
fix up comment in recursion_constraint
vezenovm May 15, 2023
bdbafc5
remove unnecesary comments when we were including proof outputs as pu…
vezenovm May 16, 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
70 changes: 60 additions & 10 deletions cpp/src/barretenberg/dsl/acir_format/acir_format.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,18 @@ void create_circuit(Composer& composer, const acir_format& constraint_system)
}

// Add recursion constraints
for (const auto& constraint : constraint_system.recursion_constraints) {
create_recursion_constraints<false, false>(composer, constraint);
for (size_t i = 0; i < constraint_system.recursion_constraints.size(); ++i) {
auto& constraint = constraint_system.recursion_constraints[i];
create_recursion_constraints<false>(composer, constraint);

// make sure the verification key records the public input indices of the final recursion output
// (N.B. up to the ACIR description to make sure that the final output aggregation object wires are public
// inputs!)
if (i == constraint_system.recursion_constraints.size() - 1) {
std::vector<uint32_t> proof_output_witness_indices(constraint.output_aggregation_object.begin(),
constraint.output_aggregation_object.end());
composer.set_recursive_proof(proof_output_witness_indices);
}
}
}

Expand Down Expand Up @@ -189,8 +199,18 @@ Composer create_circuit(const acir_format& constraint_system,
}

// Add recursion constraints
for (const auto& constraint : constraint_system.recursion_constraints) {
create_recursion_constraints<false, false>(composer, constraint);
for (size_t i = 0; i < constraint_system.recursion_constraints.size(); ++i) {
auto& constraint = constraint_system.recursion_constraints[i];
create_recursion_constraints<false>(composer, constraint);

// make sure the verification key records the public input indices of the final recursion output
// (N.B. up to the ACIR description to make sure that the final output aggregation object wires are public
// inputs!)
if (i == constraint_system.recursion_constraints.size() - 1) {
std::vector<uint32_t> proof_output_witness_indices(constraint.output_aggregation_object.begin(),
constraint.output_aggregation_object.end());
composer.set_recursive_proof(proof_output_witness_indices);
}
}

return composer;
Expand Down Expand Up @@ -288,8 +308,18 @@ Composer create_circuit_with_witness(const acir_format& constraint_system,
}

// Add recursion constraints
for (const auto& constraint : constraint_system.recursion_constraints) {
create_recursion_constraints<true, false>(composer, constraint);
for (size_t i = 0; i < constraint_system.recursion_constraints.size(); ++i) {
auto& constraint = constraint_system.recursion_constraints[i];
create_recursion_constraints<true>(composer, constraint);

// make sure the verification key records the public input indices of the final recursion output
// (N.B. up to the ACIR description to make sure that the final output aggregation object wires are public
// inputs!)
if (i == constraint_system.recursion_constraints.size() - 1) {
std::vector<uint32_t> proof_output_witness_indices(constraint.output_aggregation_object.begin(),
constraint.output_aggregation_object.end());
composer.set_recursive_proof(proof_output_witness_indices);
}
}

return composer;
Expand Down Expand Up @@ -384,8 +414,18 @@ Composer create_circuit_with_witness(const acir_format& constraint_system, std::
}

// Add recursion constraints
for (const auto& constraint : constraint_system.recursion_constraints) {
create_recursion_constraints<true, false>(composer, constraint);
for (size_t i = 0; i < constraint_system.recursion_constraints.size(); ++i) {
auto& constraint = constraint_system.recursion_constraints[i];
create_recursion_constraints<true>(composer, constraint);

// make sure the verification key records the public input indices of the final recursion output
// (N.B. up to the ACIR description to make sure that the final output aggregation object wires are public
// inputs!)
if (i == constraint_system.recursion_constraints.size() - 1) {
std::vector<uint32_t> proof_output_witness_indices(constraint.output_aggregation_object.begin(),
constraint.output_aggregation_object.end());
composer.set_recursive_proof(proof_output_witness_indices);
}
}

return composer;
Expand Down Expand Up @@ -478,8 +518,18 @@ void create_circuit_with_witness(Composer& composer, const acir_format& constrai
}

// Add recursion constraints
for (const auto& constraint : constraint_system.recursion_constraints) {
create_recursion_constraints<true, false>(composer, constraint);
for (size_t i = 0; i < constraint_system.recursion_constraints.size(); ++i) {
auto& constraint = constraint_system.recursion_constraints[i];
create_recursion_constraints<true>(composer, constraint);

// make sure the verification key records the public input indices of the final recursion output
// (N.B. up to the ACIR description to make sure that the final output aggregation object wires are public
// inputs!)
if (i == constraint_system.recursion_constraints.size() - 1) {
std::vector<uint32_t> proof_output_witness_indices(constraint.output_aggregation_object.begin(),
constraint.output_aggregation_object.end());
composer.set_recursive_proof(proof_output_witness_indices);
}
}
}

Expand Down
37 changes: 23 additions & 14 deletions cpp/src/barretenberg/dsl/acir_format/recursion_constraint.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,19 +22,26 @@ void generate_dummy_proof() {}
* 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
*/
template <bool has_valid_witness_assignment, bool inner_proof_contains_recursive_proof>
template <bool has_valid_witness_assignment>
void create_recursion_constraints(Composer& composer, const RecursionConstraint& input)
{
const auto& nested_aggregation_indices = input.nested_aggregation_object;
bool nested_aggregation_indices_all_zero = true;
for (const auto& idx : nested_aggregation_indices) {
nested_aggregation_indices_all_zero &= (idx == 0);
}
const bool inner_proof_contains_recursive_proof = !nested_aggregation_indices_all_zero;

// 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<fr> dummy_key = plonk::verification_key::export_dummy_key_in_recursion_format(
PolynomialManifest(Composer::type), inner_proof_contains_recursive_proof);
const auto manifest = Composer::create_unrolled_manifest(1);
const auto manifest = Composer::create_unrolled_manifest(input.public_inputs.size());
const std::vector<barretenberg::fr> dummy_proof =
transcript::StandardTranscript::export_dummy_transcript_in_recursion_format(manifest);
transcript::StandardTranscript::export_dummy_transcript_in_recursion_format(
manifest, inner_proof_contains_recursive_proof);
for (size_t i = 0; i < input.proof.size(); ++i) {
const auto proof_field_idx = input.proof[i];
// if we do NOT have a witness assignment (i.e. are just building the proving/verification keys),
Expand Down Expand Up @@ -88,23 +95,25 @@ void create_recursion_constraints(Composer& composer, const RecursionConstraint&
previous_aggregation.has_data = false;
}

transcript::Manifest manifest = Composer::create_unrolled_manifest(1);
transcript::Manifest manifest = Composer::create_unrolled_manifest(input.public_inputs.size());

std::vector<field_ct> key_fields;
key_fields.reserve(input.key.size());
for (const auto& idx : input.key) {
key_fields.emplace_back(field_ct::from_witness_index(&composer, idx));
}

std::vector<field_ct> proof_fields;
proof_fields.reserve(input.proof.size());
for (const auto& idx : input.proof) {
proof_fields.emplace_back(field_ct::from_witness_index(&composer, idx));
}

// recursively verify the proof
std::shared_ptr<verification_key_ct> vkey =
verification_key_ct::template from_field_pt_vector<inner_proof_contains_recursive_proof>(&composer, key_fields);
std::shared_ptr<verification_key_ct> vkey = verification_key_ct::from_field_pt_vector(
&composer, key_fields, inner_proof_contains_recursive_proof, nested_aggregation_indices);
vkey->program_width = noir_recursive_settings::program_width;
Transcript_ct transcript(&composer, manifest, proof_fields, 1);
Transcript_ct transcript(&composer, manifest, proof_fields, input.public_inputs.size());
aggregation_state_ct result = proof_system::plonk::stdlib::recursion::verify_proof_<bn254, noir_recursive_settings>(
&composer, vkey, transcript, previous_aggregation);

Expand All @@ -113,12 +122,14 @@ void create_recursion_constraints(Composer& composer, const RecursionConstraint&

// Assign the output aggregation object to the proof public inputs (16 field elements representing two
// G1 points)
result.add_proof_outputs_as_public_inputs();
// result.add_proof_outputs_as_public_inputs();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// result.add_proof_outputs_as_public_inputs();

Copy link
Contributor Author

@vezenovm vezenovm May 16, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I forgot about this commented out code. Do you think I should just remove the comment above as well? It may be confusing to leave it otherwise?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I removed the entire comment for now but can add it back in the main PR if a further explanation is deemed necessary


ASSERT(result.public_inputs.size() == 1);
ASSERT(result.public_inputs.size() == input.public_inputs.size());

// Assign the `public_input` field to the public input of the inner proof
result.public_inputs[0].assert_equal(field_ct::from_witness_index(&composer, input.public_input));
for (size_t i = 0; i < input.public_inputs.size(); ++i) {
result.public_inputs[i].assert_equal(field_ct::from_witness_index(&composer, input.public_inputs[i]));
}

// Assign the recursive proof outputs to `output_aggregation_object`
for (size_t i = 0; i < result.proof_witness_indices.size(); ++i) {
Expand All @@ -128,9 +139,7 @@ void create_recursion_constraints(Composer& composer, const RecursionConstraint&
}
}

template void create_recursion_constraints<false, false>(Composer&, const RecursionConstraint&);
template void create_recursion_constraints<false, true>(Composer&, const RecursionConstraint&);
template void create_recursion_constraints<true, false>(Composer&, const RecursionConstraint&);
template void create_recursion_constraints<true, true>(Composer&, const RecursionConstraint&);
template void create_recursion_constraints<false>(Composer&, const RecursionConstraint&);
template void create_recursion_constraints<true>(Composer&, const RecursionConstraint&);

} // namespace acir_format
33 changes: 23 additions & 10 deletions cpp/src/barretenberg/dsl/acir_format/recursion_constraint.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,51 +24,64 @@ namespace acir_format {
* (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 indecies of the aggregation object produced by recursive verification
* @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
* 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 RecursionConstraint {
static constexpr size_t AGGREGATION_OBJECT_SIZE = 16; // 16 field elements
std::vector<uint32_t> key;
std::vector<uint32_t> proof;
uint32_t public_input;
std::vector<uint32_t> public_inputs;
uint32_t key_hash;
std::array<uint32_t, AGGREGATION_OBJECT_SIZE> input_aggregation_object;
std::array<uint32_t, AGGREGATION_OBJECT_SIZE> output_aggregation_object;
std::array<uint32_t, AGGREGATION_OBJECT_SIZE> nested_aggregation_object;

friend bool operator==(RecursionConstraint const& lhs, RecursionConstraint const& rhs) = default;
};

template <bool has_valid_witness_assignment = false, bool inner_proof_contains_recursive_proof = false>
template <bool has_valid_witness_assignment = false>
void create_recursion_constraints(Composer& composer, const RecursionConstraint& input);

extern template void create_recursion_constraints<false, false>(Composer&, const RecursionConstraint&);
extern template void create_recursion_constraints<false, true>(Composer&, const RecursionConstraint&);
extern template void create_recursion_constraints<true, false>(Composer&, const RecursionConstraint&);
extern template void create_recursion_constraints<true, true>(Composer&, const RecursionConstraint&);
extern template void create_recursion_constraints<false>(Composer&, const RecursionConstraint&);
extern template void create_recursion_constraints<true>(Composer&, const RecursionConstraint&);

template <typename B> inline void read(B& buf, RecursionConstraint& constraint)
{
using serialize::read;
read(buf, constraint.key);
read(buf, constraint.proof);
read(buf, constraint.public_input);
read(buf, constraint.public_inputs);
read(buf, constraint.key_hash);
read(buf, constraint.input_aggregation_object);
read(buf, constraint.output_aggregation_object);
read(buf, constraint.nested_aggregation_object);
}

template <typename B> inline void write(B& buf, RecursionConstraint const& constraint)
{
using serialize::write;
write(buf, constraint.key);
write(buf, constraint.proof);
write(buf, constraint.public_input);
write(buf, constraint.public_inputs);
write(buf, constraint.key_hash);
write(buf, constraint.input_aggregation_object);
write(buf, constraint.output_aggregation_object);
write(buf, constraint.nested_aggregation_object);
}

} // namespace acir_format
Loading