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

feat(avm2): avm redesign init #10906

Merged
merged 6 commits into from
Jan 11, 2025
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
7 changes: 7 additions & 0 deletions barretenberg/cpp/pil/vm2/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Compile with:

```
~/aztec-packages/bb-pilcom/target/release/bb_pil pil/vm2/execution.pil --name Avm2 -y -o src/barretenberg/vm2/generated && ./format.sh changed
```

while on the `barretenberg/cpp` directory.
21 changes: 21 additions & 0 deletions barretenberg/cpp/pil/vm2/addressing.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// This is a virtual gadget, which is part of the execution trace.
namespace execution(256);

pol commit stack_pointer_val;
pol commit stack_pointer_tag;
Copy link
Contributor

Choose a reason for hiding this comment

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

I am not sure if the naming "stack pointer" is fully appropriate compared to sthg not referring stack such as "base address". I understand that it comes from the way the brillig compiler works.

pol commit sel_addressing_error; // true if any error type
pol commit addressing_error_kind; // TODO: might need to be selectors
pol commit addressing_error_idx; // operand index for error, if any

// whether each operand is an address for the given opcode.
// retrieved from the instruction spec.
pol commit sel_op1_is_address;
pol commit sel_op2_is_address;
pol commit sel_op3_is_address;
pol commit sel_op4_is_address;
// operands after relative resolution
pol commit op1_after_relative;
pol commit op2_after_relative;
pol commit op3_after_relative;
pol commit op4_after_relative;
// operands after indirect resolution are the resolved_operands rop1, ...
16 changes: 16 additions & 0 deletions barretenberg/cpp/pil/vm2/alu.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
namespace alu(256);
Copy link
Contributor

Choose a reason for hiding this comment

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

This is everywhere and a leftover but the "256" is ignored by our toolchain. IIRC this is the trace length in powdr.
Maybe we should decide how to change as this is misleading.


pol commit sel_op_add;
pol commit ia;
pol commit ib;
pol commit ic;
pol commit op;
pol commit ia_addr;
pol commit ib_addr;
pol commit dst_addr;

#[SEL_ADD_BINARY]
sel_op_add * (1 - sel_op_add) = 0;

#[ALU_ADD]
ia + ib = ic;
55 changes: 55 additions & 0 deletions barretenberg/cpp/pil/vm2/execution.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
include "alu.pil";
include "addressing.pil";
include "precomputed.pil";

namespace execution(256);

pol commit sel; // subtrace selector

pol commit ex_opcode;
pol commit indirect;
// operands
pol commit op1;
pol commit op2;
pol commit op3;
pol commit op4;
// resolved operands
pol commit rop1;
pol commit rop2;
pol commit rop3;
pol commit rop4;

pol commit pc;
pol commit clk;
pol commit last;

// Selector constraints
sel * (1 - sel) = 0;
last * (1 - last) = 0;

// If the current row is an execution row, then either
// the next row is an execution row, or the current row is marked as the last row.
// sel => (sel' v last) = 1 iff
// ¬sel v (sel' v last) = 1 iff
// ¬(¬sel v (sel' v last)) = 0 iff
// sel ^ (¬sel' ^ ¬last) = 0 iff
// sel * (1 - sel') * (1 - last) = 0
#[TRACE_CONTINUITY_1]
sel * (1 - sel') * (1 - last) = 0;
// If the current row is not an execution row, then there are no more execution rows after that.
// (not enforced for the first row)
#[TRACE_CONTINUITY_2]
(1 - precomputed.first_row) * (1 - sel) * sel' = 0;
// If the current row is the last row, then the next row is not an execution row.
#[LAST_IS_LAST]
last * sel' = 0;

// These are needed to have a non-empty set of columns for each type.
pol public input;
#[LOOKUP_DUMMY_PRECOMPUTED]
sel {/*will be 1=OR*/ sel, clk, clk, clk} in
precomputed.sel_bitwise {precomputed.bitwise_op_id, precomputed.bitwise_input_a, precomputed.bitwise_input_b, precomputed.bitwise_output};
#[LOOKUP_DUMMY_DYNAMIC] // Just a self-lookup for now, for testing.
sel {op1, op2, op3, op4} in sel {op1, op2, op3, op4};
#[PERM_DUMMY_DYNAMIC] // Just a self-permutation for now, for testing.
sel {op1, op2, op3, op4} is sel {op1, op2, op3, op4};
17 changes: 17 additions & 0 deletions barretenberg/cpp/pil/vm2/precomputed.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// General/shared precomputed columns.
namespace precomputed(256);

// From 0 and incrementing up to the size of the circuit (2^21).
pol constant clk;

// 1 only at row 0.
pol constant first_row;

// AND/OR/XOR of all 8-bit numbers.
// The tables are "stacked". First AND, then OR, then XOR.
// Note: think if we can avoid the selector.
pol constant sel_bitwise; // 1 in the first 3 * 256 rows.
pol constant bitwise_op_id; // identifies if operation is AND/OR/XOR.
pol constant bitwise_input_a; // column of all 8-bit numbers.
pol constant bitwise_input_b; // column of all 8-bit numbers.
pol constant bitwise_output; // output = a AND/OR/XOR b.
2 changes: 2 additions & 0 deletions barretenberg/cpp/src/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,7 @@ add_subdirectory(barretenberg/transcript)
add_subdirectory(barretenberg/translator_vm)
add_subdirectory(barretenberg/ultra_honk)
add_subdirectory(barretenberg/vm)
add_subdirectory(barretenberg/vm2)
add_subdirectory(barretenberg/wasi)
add_subdirectory(barretenberg/world_state)

Expand Down Expand Up @@ -171,6 +172,7 @@ set(BARRETENBERG_TARGET_OBJECTS
if(NOT DISABLE_AZTEC_VM)
# enable AVM
list(APPEND BARRETENBERG_TARGET_OBJECTS $<TARGET_OBJECTS:vm_objects>)
list(APPEND BARRETENBERG_TARGET_OBJECTS $<TARGET_OBJECTS:vm2_objects>)
endif()

if(NOT WASM)
Expand Down
84 changes: 75 additions & 9 deletions barretenberg/cpp/src/barretenberg/bb/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include "barretenberg/bb/file_io.hpp"
#include "barretenberg/client_ivc/client_ivc.hpp"
#include "barretenberg/common/benchmark.hpp"
#include "barretenberg/common/log.hpp"
#include "barretenberg/common/map.hpp"
#include "barretenberg/common/serialize.hpp"
#include "barretenberg/common/timer.hpp"
Expand All @@ -13,7 +14,6 @@
#include "barretenberg/dsl/acir_format/proof_surgeon.hpp"
#include "barretenberg/dsl/acir_proofs/acir_composer.hpp"
#include "barretenberg/dsl/acir_proofs/honk_contract.hpp"
#include "barretenberg/flavor/flavor.hpp"
#include "barretenberg/honk/proof_system/types/proof.hpp"
#include "barretenberg/numeric/bitop/get_msb.hpp"
#include "barretenberg/plonk/proof_system/proving_key/serialize.hpp"
Expand All @@ -24,15 +24,17 @@
#include "barretenberg/stdlib_circuit_builders/ultra_flavor.hpp"
#include "barretenberg/stdlib_circuit_builders/ultra_keccak_flavor.hpp"
#include "barretenberg/stdlib_circuit_builders/ultra_rollup_flavor.hpp"
#include "barretenberg/vm/avm/trace/public_inputs.hpp"
#include <cstdint>

#ifndef DISABLE_AZTEC_VM
#include "barretenberg/vm/avm/generated/flavor.hpp"
#include "barretenberg/vm/avm/trace/common.hpp"
#include "barretenberg/vm/avm/trace/execution.hpp"
#include "barretenberg/vm/avm/trace/public_inputs.hpp"
#include "barretenberg/vm/aztec_constants.hpp"
#include "barretenberg/vm/stats.hpp"
#include "barretenberg/vm2/avm_api.hpp"
#include "barretenberg/vm2/common/aztec_types.hpp"
#include "barretenberg/vm2/common/constants.hpp"
#endif

using namespace bb;
Expand Down Expand Up @@ -671,6 +673,16 @@ void vk_as_fields(const std::string& vk_path, const std::string& output_path)
}

#ifndef DISABLE_AZTEC_VM
void print_avm_stats()
{
#ifdef AVM_TRACK_STATS
info("------- STATS -------");
const auto& stats = avm_trace::Stats::get();
const int levels = std::getenv("AVM_STATS_DEPTH") != nullptr ? std::stoi(std::getenv("AVM_STATS_DEPTH")) : 2;
info(stats.to_string(levels));
#endif
}

/**
* @brief Writes an avm proof and corresponding (incomplete) verification key to files.
*
Expand Down Expand Up @@ -726,12 +738,34 @@ void avm_prove(const std::filesystem::path& public_inputs_path,
write_file(vk_fields_path, { vk_json.begin(), vk_json.end() });
vinfo("vk as fields written to: ", vk_fields_path);

#ifdef AVM_TRACK_STATS
info("------- STATS -------");
const auto& stats = avm_trace::Stats::get();
const int levels = std::getenv("AVM_STATS_DEPTH") != nullptr ? std::stoi(std::getenv("AVM_STATS_DEPTH")) : 2;
info(stats.to_string(levels));
#endif
print_avm_stats();
}

void avm2_prove(const std::filesystem::path& inputs_path, const std::filesystem::path& output_path)
{
avm2::AvmAPI avm;
auto inputs = avm2::AvmAPI::ProvingInputs::from(read_file(inputs_path));

// This is bigger than CIRCUIT_SUBGROUP_SIZE because of BB inefficiencies.
init_bn254_crs(avm2::CIRCUIT_SUBGROUP_SIZE * 2);
auto [proof, vk] = avm.prove(inputs);

// NOTE: As opposed to Avm1 and other proof systems, the public inputs are NOT part of the proof.
write_file(output_path / "proof", to_buffer(proof));
write_file(output_path / "vk", vk);

print_avm_stats();
}

void avm2_check_circuit(const std::filesystem::path& inputs_path)
{
avm2::AvmAPI avm;
auto inputs = avm2::AvmAPI::ProvingInputs::from(read_file(inputs_path));

bool res = avm.check_circuit(inputs);
info("circuit check: ", res ? "success" : "failure");

print_avm_stats();
}

/**
Expand Down Expand Up @@ -783,8 +817,28 @@ bool avm_verify(const std::filesystem::path& proof_path, const std::filesystem::

const bool verified = AVM_TRACK_TIME_V("verify/all", avm_trace::Execution::verify(vk, proof));
vinfo("verified: ", verified);

print_avm_stats();
return verified;
}

// NOTE: The proof should NOT include the public inputs.
bool avm2_verify(const std::filesystem::path& proof_path,
const std::filesystem::path& public_inputs_path,
const std::filesystem::path& vk_path)
{
const auto proof = many_from_buffer<fr>(read_file(proof_path));
std::vector<uint8_t> vk_bytes = read_file(vk_path);
auto public_inputs = avm2::PublicInputs::from(read_file(public_inputs_path));

init_bn254_crs(1);
avm2::AvmAPI avm;
bool res = avm.verify(proof, public_inputs, vk_bytes);
info("verification: ", res ? "success" : "failure");

print_avm_stats();
return res;
}
#endif

/**
Expand Down Expand Up @@ -1382,6 +1436,18 @@ int main(int argc, char* argv[])
std::string output_path = get_option(args, "-o", "./target");
write_recursion_inputs_honk<UltraRollupFlavor>(bytecode_path, witness_path, output_path, recursive);
#ifndef DISABLE_AZTEC_VM
} else if (command == "avm2_prove") {
std::filesystem::path inputs_path = get_option(args, "--avm-inputs", "./target/avm_inputs.bin");
// This outputs both files: proof and vk, under the given directory.
std::filesystem::path output_path = get_option(args, "-o", "./proofs");
avm2_prove(inputs_path, output_path);
} else if (command == "avm2_check_circuit") {
std::filesystem::path inputs_path = get_option(args, "--avm-inputs", "./target/avm_inputs.bin");
avm2_check_circuit(inputs_path);
} else if (command == "avm2_verify") {
std::filesystem::path public_inputs_path =
get_option(args, "--avm-public-inputs", "./target/avm_public_inputs.bin");
return avm2_verify(proof_path, public_inputs_path, vk_path) ? 0 : 1;
} else if (command == "avm_prove") {
std::filesystem::path avm_public_inputs_path =
get_option(args, "--avm-public-inputs", "./target/avm_public_inputs.bin");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -170,6 +170,9 @@ template <typename Fq_, typename Fr_, typename Params> class alignas(64) affine_
}
Fq x;
Fq y;

// Note: this serialization from typescript does not support infinity.
MSGPACK_FIELDS(x, y);
};

template <typename B, typename Fq_, typename Fr_, typename Params>
Expand Down
3 changes: 3 additions & 0 deletions barretenberg/cpp/src/barretenberg/vm2/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
if(NOT DISABLE_AZTEC_VM)
barretenberg_module(vm2 sumcheck stdlib_honk_verifier)
endif()
58 changes: 58 additions & 0 deletions barretenberg/cpp/src/barretenberg/vm2/avm_api.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
#include "barretenberg/vm2/avm_api.hpp"

#include "barretenberg/vm/stats.hpp"
#include "barretenberg/vm2/proving_helper.hpp"
#include "barretenberg/vm2/simulation_helper.hpp"
#include "barretenberg/vm2/tracegen_helper.hpp"

namespace bb::avm2 {

using namespace bb::avm2::simulation;

std::pair<AvmAPI::AvmProof, AvmAPI::AvmVerificationKey> AvmAPI::prove(const AvmAPI::ProvingInputs& inputs)
{
// Simulate.
info("Simulating...");
Copy link
Contributor

Choose a reason for hiding this comment

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

I guess that these tracing occurences at info level will be migrated to verbose level?

AvmSimulationHelper simulation_helper(inputs);
auto events = AVM_TRACK_TIME_V("simulation/all", simulation_helper.simulate());

// Generate trace.
info("Generating trace...");
AvmTraceGenHelper tracegen_helper;
auto trace = AVM_TRACK_TIME_V("tracegen/all", tracegen_helper.generate_trace(std::move(events)));

// Prove.
info("Proving...");
AvmProvingHelper proving_helper;
auto [proof, vk] = AVM_TRACK_TIME_V("proving/all", proving_helper.prove(std::move(trace)));

info("Done!");
return { std::move(proof), std::move(vk) };
}

bool AvmAPI::check_circuit(const AvmAPI::ProvingInputs& inputs)
{
// Simulate.
info("Simulating...");
AvmSimulationHelper simulation_helper(inputs);
auto events = AVM_TRACK_TIME_V("simulation/all", simulation_helper.simulate());

// Generate trace.
info("Generating trace...");
AvmTraceGenHelper tracegen_helper;
auto trace = AVM_TRACK_TIME_V("tracegen/all", tracegen_helper.generate_trace(std::move(events)));

// Check circuit.
info("Checking circuit...");
AvmProvingHelper proving_helper;
return proving_helper.check_circuit(std::move(trace));
}

bool AvmAPI::verify(const AvmProof& proof, const PublicInputs& pi, const AvmVerificationKey& vk_data)
{
info("Verifying...");
AvmProvingHelper proving_helper;
return AVM_TRACK_TIME_V("verifing/all", proving_helper.verify(proof, pi, vk_data));
}

} // namespace bb::avm2
24 changes: 24 additions & 0 deletions barretenberg/cpp/src/barretenberg/vm2/avm_api.hpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
#pragma once

#include <tuple>

#include "barretenberg/vm2/common/avm_inputs.hpp"
#include "barretenberg/vm2/proving_helper.hpp"

namespace bb::avm2 {

class AvmAPI {
public:
using AvmProof = AvmProvingHelper::Proof;
using AvmVerificationKey = std::vector<uint8_t>;
using ProvingInputs = AvmProvingInputs;

AvmAPI() = default;

// NOTE: The public inputs are NOT part of the proof.
std::pair<AvmProof, AvmVerificationKey> prove(const ProvingInputs& inputs);
bool check_circuit(const ProvingInputs& inputs);
bool verify(const AvmProof& proof, const PublicInputs& pi, const AvmVerificationKey& vk_data);
};

} // namespace bb::avm2
Loading
Loading