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.

Sign up for GitHub

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(avm-mini): call and return opcodes #3704

Merged
merged 12 commits into from
Dec 19, 2023
Merged

feat(avm-mini): call and return opcodes #3704

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
d3b3ccd
feat: call and return pil
Maddiaa0 Dec 14, 2023
77a5425
fix: only increment pc on opcode
Maddiaa0 Dec 15, 2023
17057c8
fix: add halt flag to stop pc progression
Maddiaa0 Dec 18, 2023
abf939d
temp
Maddiaa0 Dec 18, 2023
33984c9
Merge branch 'jm/merging-master-avm-main-12-2023' into md/jump-ret
Maddiaa0 Dec 18, 2023
64b5f10
feat: add tests
Maddiaa0 Dec 18, 2023
cfe5b71
fix: store the incremented return destination in the call stack
Maddiaa0 Dec 18, 2023
97480e1
fix: constrain selectors are boolean
Maddiaa0 Dec 18, 2023
75c772d
fix: pr review comments
Maddiaa0 Dec 19, 2023
a607e9a
Merge branch 'avm-main' into md/jump-ret
Maddiaa0 Dec 19, 2023
b392b2e
🧹
Maddiaa0 Dec 19, 2023
4e54074
🧹
Maddiaa0 Dec 19, 2023
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
57 changes: 56 additions & 1 deletion barretenberg/cpp/pil/avm/avm_mini.pil
View file
Open in desktop
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 ========================================================
Copy link
Member Author

@Maddiaa0 Maddiaa0 Dec 18, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

do i need to assert the internal call counter does not change between calls?

resolved

// 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;
Copy link
Contributor

Choose a reason for hiding this comment

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

Same remark as above related to the OP-SUBOP table.

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;

Copy link
Contributor

Choose a reason for hiding this comment

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

@Maddiaa0 Should not we have a constraint on internal_return_ptr value staying constant for all other operations? Otherwise, we could change maliciously the index between to internal_return/call, no?

Copy link
Member Author

Choose a reason for hiding this comment

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

#3704 (comment) yes! I wondered this. I shall implement it

// 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;
Copy link
Contributor

Choose a reason for hiding this comment

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

I suggest a comment line on top of the relation with this:
// first == 0 && sel_internal_call == 0 && sel_internal_return == 0 && sel_halt == 0 ==> internal_return_ptr == internal_return_ptr'


// 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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading