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

fix(dsl): Add full recursive verification test #4658

Merged
merged 7 commits into from
Feb 19, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
10 changes: 6 additions & 4 deletions barretenberg/acir_tests/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
14 changes: 10 additions & 4 deletions barretenberg/cpp/src/barretenberg/dsl/acir_format/acir_format.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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
Expand All @@ -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,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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);
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "double_verify_nested_proof"
type = "bin"
authors = [""]
compiler_version = ">=0.24.0"

[dependencies]
Loading
Loading