-
Notifications
You must be signed in to change notification settings - Fork 312
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
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. |
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; | ||
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, ... |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
namespace alu(256); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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. |
||
|
||
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; |
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}; |
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. |
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() |
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..."); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 |
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 |
There was a problem hiding this comment.
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.