From 644f1eca7110ec158fbddb38959b1e186be3a428 Mon Sep 17 00:00:00 2001 From: Maxim Vezenov Date: Mon, 19 Feb 2024 16:26:50 +0000 Subject: [PATCH] fix(dsl): Add full recursive verification test (#4658) This PR adds a test that does a full recursive verification similar to `TestFullRecursiveComposition` under `recursion_constraint.test.cpp` but using Noir. A couple bugs fixes were done to enable the new `double_verify_nested_proof` test: - We have an assert in the recursion constraint that checks `num_public_inputs == RecursionConstraint::AGGREGATION_OBJECT_SIZE` when generating the dummy transcript for when we do not have valid witness assignments. If we want to recursively verify a recursive proof that itself has extra public inputs this assertion makes that impossible (in fact the cpp test does not use any public inputs for `TestFullRecursiveComposition` and this may be why this assertion wasn't hit earlier). - After moving to a definition of a proof as separate from its public inputs in (https://github.com/AztecProtocol/aztec-packages/pull/3528) we were missing the accurate copy constraints in the case of no valid witness assignment. In the case of a nested proof the public inputs will contain an aggregation object for which we expect two accurate G1 points. Otherwise, even with the removed assertion above we will always hit a "trying to invert 0" error when working without valid witness assignments. --- acir_tests/README.md | 10 +++--- .../dsl/acir_format/acir_format.cpp | 14 +++++--- .../dsl/acir_format/recursion_constraint.cpp | 33 ++++++++++++++----- 3 files changed, 41 insertions(+), 16 deletions(-) diff --git a/acir_tests/README.md b/acir_tests/README.md index 8bdf7fa658..e356cc0074 100644 --- a/acir_tests/README.md +++ b/acir_tests/README.md @@ -43,18 +43,20 @@ The `all_cmds` flow tests all the supported commands on the binary. Slower, but $ FLOW=all_cmds ./run_acir_tests.sh 1_mul ``` -## Regenerating witness for `double_verify_proof` +## Regenerating witness for `double_verify_proof` and `double_verify_nested_proof` `double_verify_proof` has inputs that are proof system specific such as the circuit verification key and the proofs themselves which are being recursively verified. Certain proof system changes can sometimes lead to the key or inner proofs now being invalid. This means we have to generate the proof specific inputs using our backend and pass it back into `double_verify_proof` to regenerate the accurate witness. The following is a temporary solution to manually regenerate the inputs for `double_verify_proof` on a specific Noir branch. -First find `acir_tests/gen_inner_proof_inputs.sh`. Change the $BRANCH env var to your working branch and $PROOF_NAME to your first input you want to recursively verify. The script is going to generate the proof system specific verification key output and proof for the `assert_statement` test. +First find `acir_tests/gen_inner_proof_inputs.sh`. Change the $BRANCH env var to your working branch and $PROOF_NAME to your first input you want to recursively verify. The script is going to generate the proof system specific verification key output and proof for the `assert_statement_recursive` test. To run: ``` ./gen_inner_proof_inputs.sh ``` -To generate a new input you can run the script again. To generate a new file under `assert_statement/proofs/` be sure to change the $PROOF_NAME inside of the script. +To generate a new input you can run the script again. To generate a new file under `assert_statement_recursive/proofs/` be sure to change the $PROOF_NAME inside of the script. -You can then copy these inputs over to your working branch in Noir and regenerate the witness for `double_verify_proof`. You can then change the branch in `run_acir_tests.sh` to this Noir working branch as well and `double_verify_proof` should pass. \ No newline at end of file +You can then copy these inputs over to your working branch in Noir and regenerate the witness for `double_verify_proof`. You can then change the branch in `run_acir_tests.sh` to this Noir working branch as well and `double_verify_proof` should pass. + +The same process should then be repeated, but now `double_verify_proof` will be the circuit for which we will be generating recursive inputs using `gen_inner_proof_inputs.sh`. The recursive artifacts should then supplied as inputs to `double_verify_nested_proof`. \ No newline at end of file diff --git a/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp b/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp index 47ca2e460a..fd2f23fe0f 100644 --- a/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp +++ b/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp @@ -113,7 +113,7 @@ void build_constraints(Builder& builder, AcirFormat const& constraint_system, bo // 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 (IsGoblinBuilder) { - if (constraint_system.recursion_constraints.size() > 0) { + if (!constraint_system.recursion_constraints.empty()) { info("WARNING: this circuit contains recursion_constraints!"); } } else { @@ -148,8 +148,15 @@ void build_constraints(Builder& builder, AcirFormat const& constraint_system, bo // 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); + if (constraint.proof.size() - proof_size_no_pub_inputs != + RecursionConstraint::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 {}\n", + RecursionConstraint::AGGREGATION_OBJECT_SIZE); + throw_or_abort(error_string); + } 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 @@ -165,7 +172,6 @@ void build_constraints(Builder& builder, AcirFormat const& constraint_system, bo constraint.proof.begin() + static_cast(RecursionConstraint::AGGREGATION_OBJECT_SIZE)); } - current_output_aggregation_object = create_recursion_constraints(builder, constraint, current_input_aggregation_object, diff --git a/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.cpp b/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.cpp index 8b154172a6..b457f9c555 100644 --- a/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.cpp +++ b/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.cpp @@ -53,20 +53,32 @@ std::array create_recurs std::vector dummy_proof = export_dummy_transcript_in_recursion_format(manifest, inner_proof_contains_recursive_proof); - // Remove the public inputs from the dummy 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]; + 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 proof values as Builder variables. + // 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(proof_field_idx) : dummy_proof[i]; + 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 RecursionConstraint. // This will make the RecursionConstraint 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 RecursionConstraint 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) { @@ -329,7 +341,12 @@ std::vector export_dummy_transcript_in_recursion_format(const transcript // 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) { - ASSERT(num_public_inputs == RecursionConstraint::AGGREGATION_OBJECT_SIZE); + // 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 - RecursionConstraint::AGGREGATION_OBJECT_SIZE; ++k) { + fields.emplace_back(0); + } for (size_t k = 0; k < RecursionConstraint::NUM_AGGREGATION_ELEMENTS; ++k) { auto scalar = bb::fr::random_element(); const auto group_element = bb::g1::affine_element(bb::g1::one * scalar);