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

Merged
merged 12 commits into from
Dec 19, 2023
47 changes: 46 additions & 1 deletion barretenberg/cpp/pil/avm/avm_mini.pil
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 @@ -61,6 +73,11 @@ namespace avmMini(256);
sel_op_sub * (1 - sel_op_sub) = 0;
sel_op_mul * (1 - sel_op_mul) = 0;
sel_op_div * (1 - sel_op_div) = 0;
sel_op_div * (1 - sel_op_div) = 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 Did you duplicate this line by mistake?

Copy link
Member Author

Choose a reason for hiding this comment

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

good catch!


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;

Expand Down Expand Up @@ -108,4 +125,32 @@ namespace avmMini(256);
// Same for the relations related to the error activation:
// (ib * inv - 1 + op_div_err) = 0 && op_err * (1 - inv) = 0
// This works in combination with op_div_err * (sel_op_div - 1) = 0;
// Drawback is the need to paralllelize the latter.
// Drawback is the need to paralllelize the latter.


//===== CALL_RETURN ========================================================
Copy link
Member Author

@Maddiaa0 Maddiaa0 Dec 18, 2023

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 jump selector into mema
Copy link
Contributor

Choose a reason for hiding this comment

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

@Maddiaa0 mema is not a defined term. Did you mean mem_idx_a?

Copy link
Member Author

Choose a reason for hiding this comment

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

yes! updated

#[return_pointer_increment]
Copy link
Contributor

Choose a reason for hiding this comment

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

@Maddiaa0 All identifiers for relations in my PR are capitalized. I think it helps with visibility. At least we should agree on using the same notation.

Copy link
Member Author

Choose a reason for hiding this comment

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

done

sel_internal_call * ( internal_return_ptr' - ( internal_return_ptr + 1)) = 0; // we increment our jump selector
Copy link
Contributor

Choose a reason for hiding this comment

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

@Maddiaa0 We might use another term than "jump selector" as the operations are not named JUMP anymore.

sel_internal_call * ( internal_return_ptr - mem_idx_a) = 0;
sel_internal_call * (rwa - 1) = 0; // it must be a write
Copy link
Contributor

Choose a reason for hiding this comment

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

@Maddiaa0 In the original design, it was meant that there would be a fixed tuple lookup mapping an operation to the corresponding sub-operations included load/store. In this case, relations

sel_internal_call * (rwa - 1) = 0;
sel_internal_call * (mem_op_a - 1) = 0;

would not be required. I did not introduce such ones for the arithmetic operations.
Could you keep them and add in comments a TODO mentioning that we might fill mem_op_a and rwa through a lookup of the OP-SUBOP table? (see https://hackmd.io/iKq8n9MBTu2hD3C4r_n_Hg#Precomputed-Table-OP-SUBOP)

Copy link
Member Author

Choose a reason for hiding this comment

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

Oh awesome !

sel_internal_call * (mem_op_a - 1) = 0;
sel_internal_call * ((pc + 1) - ia) = 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; // We decrement out jump selector
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
sel_internal_return * ( internal_return_ptr' - ( internal_return_ptr - 1)) = 0; // We decrement out jump selector
sel_internal_return * ( internal_return_ptr' - ( internal_return_ptr - 1)) = 0; // We decrement our jump selector

sel_internal_return * ( (internal_return_ptr - 1) - mem_idx_a) = 0;
sel_internal_return * (pc' - ia) = 0;
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;

// Program counter must increment if not jumping or returning
#[pc_increment]
(1-first) * (1- sel_halt) * (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul) * (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 Please be consistent with spacing between arithmetic operations:

(1 - first) * (1 - sel_halt) * ....


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


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

111 changes: 91 additions & 20 deletions barretenberg/cpp/src/barretenberg/flavor/generated/AvmMini_flavor.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,11 @@ class AvmMiniFlavor {
using VerifierCommitmentKey = pcs::VerifierCommitmentKey<Curve>;

static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2;
static constexpr size_t NUM_WITNESS_ENTITIES = 25;
static constexpr size_t NUM_WITNESS_ENTITIES = 30;
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 = 30;
static constexpr size_t NUM_ALL_ENTITIES = 37;

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

Expand Down Expand Up @@ -82,6 +82,11 @@ class AvmMiniFlavor {
memTrace_m_val,
memTrace_m_lastAccess,
memTrace_m_rw,
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 @@ -104,13 +109,36 @@ class AvmMiniFlavor {

RefVector<DataType> get_wires()
{
return {
memTrace_m_clk, memTrace_m_sub_clk, memTrace_m_addr, memTrace_m_val, memTrace_m_lastAccess,
memTrace_m_rw, avmMini_sel_op_add, avmMini_sel_op_sub, avmMini_sel_op_mul, avmMini_sel_op_div,
avmMini_op_err, avmMini_inv, avmMini_ia, avmMini_ib, avmMini_ic,
avmMini_mem_op_a, avmMini_mem_op_b, avmMini_mem_op_c, avmMini_rwa, avmMini_rwb,
avmMini_rwc, avmMini_mem_idx_a, avmMini_mem_idx_b, avmMini_mem_idx_c, avmMini_last
};
return { memTrace_m_clk,
memTrace_m_sub_clk,
memTrace_m_addr,
memTrace_m_val,
memTrace_m_lastAccess,
memTrace_m_rw,
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,
avmMini_sel_op_div,
avmMini_op_err,
avmMini_inv,
avmMini_ia,
avmMini_ib,
avmMini_ic,
avmMini_mem_op_a,
avmMini_mem_op_b,
avmMini_mem_op_c,
avmMini_rwa,
avmMini_rwb,
avmMini_rwc,
avmMini_mem_idx_a,
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last };
};
RefVector<DataType> get_sorted_polynomials() { return {}; };
};
Expand All @@ -126,6 +154,11 @@ class AvmMiniFlavor {
memTrace_m_val,
memTrace_m_lastAccess,
memTrace_m_rw,
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 @@ -145,9 +178,11 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
memTrace_m_val_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift,
memTrace_m_val_shift)
avmMini_pc_shift,
avmMini_internal_return_ptr_shift)

RefVector<DataType> get_wires()
{
Expand All @@ -159,6 +194,11 @@ class AvmMiniFlavor {
memTrace_m_val,
memTrace_m_lastAccess,
memTrace_m_rw,
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 @@ -178,9 +218,11 @@ class AvmMiniFlavor {
avmMini_mem_idx_b,
avmMini_mem_idx_c,
avmMini_last,
memTrace_m_val_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift,
memTrace_m_val_shift };
avmMini_pc_shift,
avmMini_internal_return_ptr_shift };
};
RefVector<DataType> get_unshifted()
{
Expand All @@ -192,6 +234,11 @@ class AvmMiniFlavor {
memTrace_m_val,
memTrace_m_lastAccess,
memTrace_m_rw,
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 @@ -212,10 +259,17 @@ class AvmMiniFlavor {
avmMini_mem_idx_c,
avmMini_last };
};
RefVector<DataType> get_to_be_shifted() { return { memTrace_m_rw, memTrace_m_addr, memTrace_m_val }; };
RefVector<DataType> get_to_be_shifted()
{
return { memTrace_m_val, memTrace_m_rw, memTrace_m_addr, avmMini_pc, avmMini_internal_return_ptr };
};
RefVector<DataType> get_shifted()
{
return { memTrace_m_rw_shift, memTrace_m_addr_shift, memTrace_m_val_shift };
return { memTrace_m_val_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift,
avmMini_pc_shift,
avmMini_internal_return_ptr_shift };
};
};

Expand All @@ -228,13 +282,9 @@ class AvmMiniFlavor {

RefVector<DataType> get_to_be_shifted()
{
return {
memTrace_m_rw,
memTrace_m_addr,
memTrace_m_val,

};
return { memTrace_m_val, memTrace_m_rw, memTrace_m_addr, avmMini_pc, avmMini_internal_return_ptr };
};

// The plookup wires that store plookup read data.
std::array<PolynomialHandle, 0> get_table_column_wires() { return {}; };
};
Expand All @@ -261,7 +311,7 @@ class AvmMiniFlavor {
ProverPolynomials(ProverPolynomials&& o) noexcept = default;
ProverPolynomials& operator=(ProverPolynomials&& o) noexcept = default;
~ProverPolynomials() = default;
[[nodiscard]] size_t get_polynomial_size() const { return avmMini_clk.size(); }
[[nodiscard]] size_t get_polynomial_size() const { return memTrace_m_clk.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 All @@ -275,6 +325,7 @@ class AvmMiniFlavor {
return result;
}
};

using RowPolynomials = AllEntities<FF>;

class PartiallyEvaluatedMultivariates : public AllEntities<Polynomial> {
Expand Down Expand Up @@ -316,6 +367,11 @@ class AvmMiniFlavor {
Base::memTrace_m_val = "MEMTRACE_M_VAL";
Base::memTrace_m_lastAccess = "MEMTRACE_M_LASTACCESS";
Base::memTrace_m_rw = "MEMTRACE_M_RW";
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 @@ -360,6 +416,11 @@ class AvmMiniFlavor {
Commitment memTrace_m_val;
Commitment memTrace_m_lastAccess;
Commitment memTrace_m_rw;
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 @@ -404,6 +465,11 @@ class AvmMiniFlavor {
memTrace_m_val = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
memTrace_m_lastAccess = deserialize_from_buffer<Commitment>(Transcript::proof_data, num_bytes_read);
memTrace_m_rw = 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 @@ -452,6 +518,11 @@ class AvmMiniFlavor {
serialize_to_buffer<Commitment>(memTrace_m_val, Transcript::proof_data);
serialize_to_buffer<Commitment>(memTrace_m_lastAccess, Transcript::proof_data);
serialize_to_buffer<Commitment>(memTrace_m_rw, 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
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
Original file line number Diff line number Diff line change
Expand Up @@ -19,38 +19,44 @@ 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("=====================================================================================");
info("== ROW ", i);
info("================================================================================");

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_lastAccess: ", trace.at(i).memTrace_m_lastAccess);
info("m_rw: ", trace.at(i).memTrace_m_rw);
info("m_val_shift: ", trace.at(i).memTrace_m_val_shift);
info("first: ", trace.at(i).avmMini_first);
info("last: ", trace.at(i).avmMini_last);

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("ia: ", trace.at(i).avmMini_ia);
info("rwa: ", trace.at(i).avmMini_rwa);

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("ib: ", trace.at(i).avmMini_ib);
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("ic: ", trace.at(i).avmMini_ic);
info("rwc: ", trace.at(i).avmMini_rwc);
info("=====================================================================================");

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_lastAccess: ", trace.at(i).memTrace_m_lastAccess);
info("m_rw: ", trace.at(i).memTrace_m_rw);
info("m_val_shift: ", trace.at(i).memTrace_m_val_shift);
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("ia: ", trace.at(i).avmMini_ia);
info("rwa: ", trace.at(i).avmMini_rwa);

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("ib: ", trace.at(i).avmMini_ib);
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("ic: ", trace.at(i).avmMini_ic);
info("rwc: ", trace.at(i).avmMini_rwc);
info("\n");
}
}
Expand Down
Loading