Skip to content

Commit

Permalink
feat(avm-mini): call and return opcodes (#3704)
Browse files Browse the repository at this point in the history 
closes: #3697
  • Loading branch information
@Maddiaa0
Maddiaa0 authored Dec 19, 2023
1 parent 739fe90 commit e534204
Show file tree
Hide file tree
Showing 18 changed files with 821 additions and 133 deletions.
57 changes: 56 additions & 1 deletion barretenberg/cpp/pil/avm/avm_mini.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,18 @@ namespace avmMini(256);
pol constant clk(i) { i };
pol constant first = [1] + [0]*; // Used mostly to toggle off the first row consisting
// only in first element of shifted polynomials.

//===== CONTROL FLOW ==========================================================
// Program counter
pol commit pc;
// Return Pointer
pol commit internal_return_ptr;

pol commit sel_internal_call;
pol commit sel_internal_return;

// Halt program execution
pol commit sel_halt;

//===== TABLE SUBOP-TR ========================================================
// Boolean selectors for (sub-)operations. Only one operation is activated at
Expand Down Expand Up @@ -66,6 +78,10 @@ namespace avmMini(256);
sel_op_mul * (1 - sel_op_mul) = 0;
sel_op_div * (1 - sel_op_div) = 0;

sel_internal_call * (1 - sel_internal_call) = 0;
sel_internal_return * (1 - sel_internal_return) = 0;
sel_halt * (1 - sel_halt) = 0;

op_err * (1 - op_err) = 0;
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to memTrace)?

Expand Down Expand Up @@ -131,8 +147,47 @@ namespace avmMini(256);
// This works in combination with op_div_err * (sel_op_div - 1) = 0;
// Drawback is the need to paralllelize the latter.


//===== CALL_RETURN ========================================================
// The program counter in the next row should be equal to the value loaded from the ia register
// This implies that a load from memory must occur at the same time
// Imply that we must load the return location into mem_idx_a

#[RETURN_POINTER_INCREMENT]
sel_internal_call * ( internal_return_ptr' - ( internal_return_ptr + 1)) = 0;
sel_internal_call * ( internal_return_ptr - mem_idx_a) = 0;
sel_internal_call * ((pc + 1) - ia) = 0;

// TODO(md): Below relations may be removed through sub-op table lookup
sel_internal_call * (rwa - 1) = 0;
sel_internal_call * (mem_op_a - 1) = 0;

// We must load the memory pointer to be the internal_return_ptr
#[RETURN_POINTER_DECREMENT]
sel_internal_return * ( internal_return_ptr' - ( internal_return_ptr - 1)) = 0;
sel_internal_return * ( (internal_return_ptr - 1) - mem_idx_a) = 0;
sel_internal_return * (pc' - ia) = 0;

// TODO(md): Below relations may be removed through sub-op table lookup
sel_internal_return * rwa = 0;
sel_internal_return * (mem_op_a - 1) = 0;

//===== CONTROL_FLOW_CONSISTENCY ============================================
pol CONTROL_FLOW_SELECTORS = (first + sel_internal_call + sel_internal_return + sel_halt);
pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul);

// Program counter must increment if not jumping or returning
#[PC_INCREMENT]
(1 - first) * (1 - sel_halt) * OPCODE_SELECTORS * (pc' - (pc + 1)) = 0;

// first == 0 && sel_internal_call == 0 && sel_internal_return == 0 && sel_halt == 0 ==> internal_return_ptr == internal_return_ptr'
#[INTERNAL_RETURN_POINTER_CONSISTENCY]
(1 - CONTROL_FLOW_SELECTORS) * (internal_return_ptr' - internal_return_ptr) = 0;

// TODO: we want to set an initial number for the reserved memory of the jump pointer

// Inter-table Constraints

// TODO: tag_err {clk} IS memTrace.m_tag_err {memTrace.m_clk}
// TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like:
// mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}
// mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}
78 changes: 68 additions & 10 deletions barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,13 +36,13 @@ class AvmMiniFlavor {
using VerifierCommitmentKey = pcs::VerifierCommitmentKey<Curve>;

static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2;
static constexpr size_t NUM_WITNESS_ENTITIES = 32;
static constexpr size_t NUM_WITNESS_ENTITIES = 37;
static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
// We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for
// the unshifted and one for the shifted
static constexpr size_t NUM_ALL_ENTITIES = 38;
static constexpr size_t NUM_ALL_ENTITIES = 45;

using Relations = std::tuple<AvmMini_vm::mem_trace<FF>, AvmMini_vm::avm_mini<FF>>;
using Relations = std::tuple<AvmMini_vm::avm_mini<FF>, AvmMini_vm::mem_trace<FF>>;

static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length<Relations>();

Expand Down Expand Up @@ -87,6 +87,11 @@ class AvmMiniFlavor {
memTrace_m_in_tag,
memTrace_m_tag_err,
memTrace_m_one_min_inv,
avmMini_pc,
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
avmMini_sel_op_mul,
Expand Down Expand Up @@ -122,6 +127,11 @@ class AvmMiniFlavor {
memTrace_m_in_tag,
memTrace_m_tag_err,
memTrace_m_one_min_inv,
avmMini_pc,
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
avmMini_sel_op_mul,
Expand Down Expand Up @@ -163,6 +173,11 @@ class AvmMiniFlavor {
memTrace_m_in_tag,
memTrace_m_tag_err,
memTrace_m_one_min_inv,
avmMini_pc,
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
avmMini_sel_op_mul,
Expand All @@ -184,10 +199,12 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift,
memTrace_m_tag_shift,
memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_rw_shift,
memTrace_m_tag_shift)
memTrace_m_addr_shift)

RefVector<DataType> get_wires()
{
Expand All @@ -204,6 +221,11 @@ class AvmMiniFlavor {
memTrace_m_in_tag,
memTrace_m_tag_err,
memTrace_m_one_min_inv,
avmMini_pc,
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
avmMini_sel_op_mul,
Expand All @@ -225,10 +247,12 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
avmMini_internal_return_ptr_shift,
avmMini_pc_shift,
memTrace_m_tag_shift,
memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_rw_shift,
memTrace_m_tag_shift };
memTrace_m_addr_shift };
};
RefVector<DataType> get_unshifted()
{
Expand All @@ -245,6 +269,11 @@ class AvmMiniFlavor {
memTrace_m_in_tag,
memTrace_m_tag_err,
memTrace_m_one_min_inv,
avmMini_pc,
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
avmMini_sel_op_mul,
Expand All @@ -269,11 +298,18 @@ class AvmMiniFlavor {
};
RefVector<DataType> get_to_be_shifted()
{
return { memTrace_m_val, memTrace_m_addr, memTrace_m_rw, memTrace_m_tag };
return {
avmMini_internal_return_ptr, avmMini_pc, memTrace_m_tag, memTrace_m_val, memTrace_m_rw, memTrace_m_addr
};
};
RefVector<DataType> get_shifted()
{
return { memTrace_m_val_shift, memTrace_m_addr_shift, memTrace_m_rw_shift, memTrace_m_tag_shift };
return { avmMini_internal_return_ptr_shift,
avmMini_pc_shift,
memTrace_m_tag_shift,
memTrace_m_val_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift };
};
};

Expand All @@ -286,7 +322,9 @@ class AvmMiniFlavor {

RefVector<DataType> get_to_be_shifted()
{
return { memTrace_m_val, memTrace_m_addr, memTrace_m_rw, memTrace_m_tag };
return {
avmMini_internal_return_ptr, avmMini_pc, memTrace_m_tag, memTrace_m_val, memTrace_m_rw, memTrace_m_addr
};
};

// The plookup wires that store plookup read data.
Expand Down Expand Up @@ -376,6 +414,11 @@ class AvmMiniFlavor {
Base::memTrace_m_in_tag = "MEMTRACE_M_IN_TAG";
Base::memTrace_m_tag_err = "MEMTRACE_M_TAG_ERR";
Base::memTrace_m_one_min_inv = "MEMTRACE_M_ONE_MIN_INV";
Base::avmMini_pc = "AVMMINI_PC";
Base::avmMini_internal_return_ptr = "AVMMINI_INTERNAL_RETURN_PTR";
Base::avmMini_sel_internal_call = "AVMMINI_SEL_INTERNAL_CALL";
Base::avmMini_sel_internal_return = "AVMMINI_SEL_INTERNAL_RETURN";
Base::avmMini_sel_halt = "AVMMINI_SEL_HALT";
Base::avmMini_sel_op_add = "AVMMINI_SEL_OP_ADD";
Base::avmMini_sel_op_sub = "AVMMINI_SEL_OP_SUB";
Base::avmMini_sel_op_mul = "AVMMINI_SEL_OP_MUL";
Expand Down Expand Up @@ -427,6 +470,11 @@ class AvmMiniFlavor {
Commitment memTrace_m_in_tag;
Commitment memTrace_m_tag_err;
Commitment memTrace_m_one_min_inv;
Commitment avmMini_pc;
Commitment avmMini_internal_return_ptr;
Commitment avmMini_sel_internal_call;
Commitment avmMini_sel_internal_return;
Commitment avmMini_sel_halt;
Commitment avmMini_sel_op_add;
Commitment avmMini_sel_op_sub;
Commitment avmMini_sel_op_mul;
Expand Down Expand Up @@ -478,6 +526,11 @@ class AvmMiniFlavor {
memTrace_m_in_tag = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
memTrace_m_tag_err = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
memTrace_m_one_min_inv = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_pc = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_internal_return_ptr = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_sel_internal_call = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_sel_internal_return = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_sel_halt = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_sel_op_add = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_sel_op_sub = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
avmMini_sel_op_mul = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
Expand Down Expand Up @@ -533,6 +586,11 @@ class AvmMiniFlavor {
serialize_to_buffer<Commitment>(memTrace_m_in_tag, Transcript::proof_data);
serialize_to_buffer<Commitment>(memTrace_m_tag_err, Transcript::proof_data);
serialize_to_buffer<Commitment>(memTrace_m_one_min_inv, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_pc, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_internal_return_ptr, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_sel_internal_call, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_sel_internal_return, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_sel_halt, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_sel_op_add, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_sel_op_sub, Transcript::proof_data);
serialize_to_buffer<Commitment>(avmMini_sel_op_mul, Transcript::proof_data);
Expand Down
4 changes: 1 addition & 3 deletions barretenberg/cpp/src/barretenberg/flavor/generated/Toy_flavor.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,8 +142,6 @@ class ToyFlavor {
using Base::Base;
};

using RowPolynomials = AllEntities<FF>;

/**
* @brief A container for the prover polynomials handles.
*/
Expand All @@ -156,7 +154,7 @@ class ToyFlavor {
ProverPolynomials(ProverPolynomials&& o) noexcept = default;
ProverPolynomials& operator=(ProverPolynomials&& o) noexcept = default;
~ProverPolynomials() = default;
[[nodiscard]] size_t get_polynomial_size() const { return toy_first.size(); }
[[nodiscard]] size_t get_polynomial_size() const { return toy_q_tuple_set.size(); }
/**
* @brief Returns the evaluations of all prover polynomials at one point on the boolean hypercube, which
* represents one row in the execution trace.
Expand Down
76 changes: 41 additions & 35 deletions barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/AvmMini_helper.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,47 +19,53 @@ void log_avmMini_trace(std::vector<Row> const& trace, size_t beg, size_t end)
info("Built circuit with ", trace.size(), " rows");

for (size_t i = beg; i < end; i++) {
info("================================================================================");
info("== ROW ", i);
info("================================================================================");
info("=====================================================================================");
info("== ROW ", i);
info("=====================================================================================");

info("=======MEMORY TRACE=============================================================");
info("m_addr: ", trace.at(i).memTrace_m_addr);
info("m_clk: ", trace.at(i).memTrace_m_clk);
info("m_sub_clk: ", trace.at(i).memTrace_m_sub_clk);
info("m_val: ", trace.at(i).memTrace_m_val);
info("m_rw: ", trace.at(i).memTrace_m_rw);
info("m_tag: ", trace.at(i).memTrace_m_tag);
info("m_in_tag: ", trace.at(i).memTrace_m_in_tag);
info("m_tag_err: ", trace.at(i).memTrace_m_tag_err);
info("m_one_min_inv:", trace.at(i).memTrace_m_one_min_inv);
info("=======MEMORY TRACE==================================================================");
info("m_addr: ", trace.at(i).memTrace_m_addr);
info("m_clk: ", trace.at(i).memTrace_m_clk);
info("m_sub_clk: ", trace.at(i).memTrace_m_sub_clk);
info("m_val: ", trace.at(i).memTrace_m_val);
info("m_rw: ", trace.at(i).memTrace_m_rw);
info("m_tag: ", trace.at(i).memTrace_m_tag);
info("m_in_tag: ", trace.at(i).memTrace_m_in_tag);
info("m_tag_err: ", trace.at(i).memTrace_m_tag_err);
info("m_one_min_inv: ", trace.at(i).memTrace_m_one_min_inv);

info("m_lastAccess: ", trace.at(i).memTrace_m_lastAccess);
info("m_last: ", trace.at(i).memTrace_m_last);
info("m_val_shift: ", trace.at(i).memTrace_m_val_shift);
info("m_lastAccess: ", trace.at(i).memTrace_m_lastAccess);
info("m_last: ", trace.at(i).memTrace_m_last);
info("m_val_shift: ", trace.at(i).memTrace_m_val_shift);

info("=======MAIN TRACE===============================================================");
info("ia: ", trace.at(i).avmMini_ia);
info("ib: ", trace.at(i).avmMini_ib);
info("ic: ", trace.at(i).avmMini_ic);
info("first: ", trace.at(i).avmMini_first);
info("last: ", trace.at(i).avmMini_last);
info("=======CONTROL_FLOW===================================================================");
info("pc: ", trace.at(i).avmMini_pc);
info("internal_call: ", trace.at(i).avmMini_sel_internal_call);
info("internal_return: ", trace.at(i).avmMini_sel_internal_return);
info("internal_return_ptr:", trace.at(i).avmMini_internal_return_ptr);

info("=======MEM_OP_A=================================================================");
info("clk: ", trace.at(i).avmMini_clk);
info("mem_op_a: ", trace.at(i).avmMini_mem_op_a);
info("mem_idx_a: ", trace.at(i).avmMini_mem_idx_a);
info("rwa: ", trace.at(i).avmMini_rwa);
info("=======MAIN TRACE====================================================================");
info("ia: ", trace.at(i).avmMini_ia);
info("ib: ", trace.at(i).avmMini_ib);
info("ic: ", trace.at(i).avmMini_ic);
info("first: ", trace.at(i).avmMini_first);
info("last: ", trace.at(i).avmMini_last);

info("=======MEM_OP_B=================================================================");
info("mem_op_b: ", trace.at(i).avmMini_mem_op_b);
info("mem_idx_b: ", trace.at(i).avmMini_mem_idx_b);
info("rwb: ", trace.at(i).avmMini_rwb);
info("=======MEM_OP_A======================================================================");
info("clk: ", trace.at(i).avmMini_clk);
info("mem_op_a: ", trace.at(i).avmMini_mem_op_a);
info("mem_idx_a: ", trace.at(i).avmMini_mem_idx_a);
info("rwa: ", trace.at(i).avmMini_rwa);

info("=======MEM_OP_C=================================================================");
info("mem_op_c: ", trace.at(i).avmMini_mem_op_c);
info("mem_idx_c: ", trace.at(i).avmMini_mem_idx_c);
info("rwc: ", trace.at(i).avmMini_rwc);
info("=======MEM_OP_B======================================================================");
info("mem_op_b: ", trace.at(i).avmMini_mem_op_b);
info("mem_idx_b: ", trace.at(i).avmMini_mem_idx_b);
info("rwb: ", trace.at(i).avmMini_rwb);

info("=======MEM_OP_C======================================================================");
info("mem_op_c: ", trace.at(i).avmMini_mem_op_c);
info("mem_idx_c: ", trace.at(i).avmMini_mem_idx_c);
info("rwc: ", trace.at(i).avmMini_rwc);
info("\n");
}
}
Expand Down
Loading

0 comments on commit e534204

Please sign in to comment.