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 (#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.

barretenberg/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.
+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`. 

barretenberg/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<Builder>) {
-        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<std::ptrdiff_t>(RecursionConstraint::AGGREGATION_OBJECT_SIZE));
             }
-
             current_output_aggregation_object = create_recursion_constraints(builder,
                                                                              constraint,
                                                                              current_input_aggregation_object,

barretenberg/cpp/src/barretenberg/dsl/acir_format/recursion_constraint.cpp

@@ -53,20 +53,32 @@ std::array<uint32_t, RecursionConstraint::AGGREGATION_OBJECT_SIZE> create_recurs
         std::vector<bb::fr> 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<std::ptrdiff_t>(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<std::ptrdiff_t>(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<bb::fr> 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);

noir/test_programs/execution_success/double_verify_nested_proof/Nargo.toml

@@ -0,0 +1,7 @@
+[package]
+name = "double_verify_nested_proof"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.24.0"
+
+[dependencies]