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): add standalone jump opcode #3781

Merged
merged 4 commits into from
Jan 2, 2024
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
39 changes: 24 additions & 15 deletions barretenberg/cpp/pil/avm/avm_mini.pil
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ namespace avmMini(256);

pol commit sel_internal_call;
pol commit sel_internal_return;
pol commit sel_jump;

// Halt program execution
pol commit sel_halt;
Expand Down Expand Up @@ -80,6 +81,7 @@ namespace avmMini(256);

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

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

//===== CONTROL FLOW =======================================================
//===== JUMP ===============================================================
sel_jump * (pc' - ia) = 0;

//===== 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
//===== INTERNAL_CALL ======================================================
// - The program counter in the next row should be equal to the value loaded from the ia register
// - We then write the return location (pc + 1) into the call stack (in memory)

#[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;

sel_internal_call * (internal_return_ptr' - (internal_return_ptr + 1)) = 0;
sel_internal_call * (internal_return_ptr - mem_idx_b) = 0;
sel_internal_call * (pc' - ia) = 0;
sel_internal_call * ((pc + 1) - ib) = 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;
sel_internal_call * (rwb - 1) = 0;
sel_internal_call * (mem_op_b - 1) = 0;

// We must load the memory pointer to be the internal_return_ptr
//===== INTERNAL_RETURN ===================================================
// - We load the memory pointer to be the internal_return_ptr
// - Constrain then next program counter to be the loaded value
// - decrement 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 * (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 INTERNAL_CALL_STACK_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
Expand All @@ -182,7 +191,7 @@ namespace avmMini(256);

// 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;
(1 - INTERNAL_CALL_STACK_SELECTORS) * (internal_return_ptr' - internal_return_ptr) = 0;

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

Expand Down
68 changes: 0 additions & 68 deletions barretenberg/cpp/pil/avm/avm_mini_opt.pil

This file was deleted.

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 = 37;
static constexpr size_t NUM_WITNESS_ENTITIES = 38;
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 = 45;
static constexpr size_t NUM_ALL_ENTITIES = 46;

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

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

Expand Down Expand Up @@ -91,6 +91,7 @@ class AvmMiniFlavor {
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_jump,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
Expand Down Expand Up @@ -131,6 +132,7 @@ class AvmMiniFlavor {
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_jump,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
Expand Down Expand Up @@ -177,6 +179,7 @@ class AvmMiniFlavor {
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_jump,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
Expand All @@ -199,12 +202,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_tag_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift)
avmMini_internal_return_ptr_shift,
avmMini_pc_shift)

RefVector<DataType> get_wires()
{
Expand All @@ -225,6 +228,7 @@ class AvmMiniFlavor {
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_jump,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
Expand All @@ -247,12 +251,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_tag_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift };
avmMini_internal_return_ptr_shift,
avmMini_pc_shift };
};
RefVector<DataType> get_unshifted()
{
Expand All @@ -273,6 +277,7 @@ class AvmMiniFlavor {
avmMini_internal_return_ptr,
avmMini_sel_internal_call,
avmMini_sel_internal_return,
avmMini_sel_jump,
avmMini_sel_halt,
avmMini_sel_op_add,
avmMini_sel_op_sub,
Expand All @@ -298,18 +303,17 @@ class AvmMiniFlavor {
};
RefVector<DataType> get_to_be_shifted()
{
return {
avmMini_internal_return_ptr, avmMini_pc, memTrace_m_tag, memTrace_m_val, memTrace_m_rw, memTrace_m_addr
};
return { memTrace_m_val, memTrace_m_addr, memTrace_m_tag, memTrace_m_rw, avmMini_internal_return_ptr,
avmMini_pc };
};
RefVector<DataType> get_shifted()
{
return { avmMini_internal_return_ptr_shift,
avmMini_pc_shift,
return { memTrace_m_val_shift,
memTrace_m_addr_shift,
memTrace_m_tag_shift,
memTrace_m_val_shift,
memTrace_m_rw_shift,
memTrace_m_addr_shift };
avmMini_internal_return_ptr_shift,
avmMini_pc_shift };
};
};

Expand All @@ -322,9 +326,8 @@ class AvmMiniFlavor {

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

// The plookup wires that store plookup read data.
Expand Down Expand Up @@ -418,6 +421,7 @@ class AvmMiniFlavor {
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_jump = "AVMMINI_SEL_JUMP";
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";
Expand Down Expand Up @@ -474,6 +478,7 @@ class AvmMiniFlavor {
Commitment avmMini_internal_return_ptr;
Commitment avmMini_sel_internal_call;
Commitment avmMini_sel_internal_return;
Commitment avmMini_sel_jump;
Commitment avmMini_sel_halt;
Commitment avmMini_sel_op_add;
Commitment avmMini_sel_op_sub;
Expand Down Expand Up @@ -530,6 +535,7 @@ class AvmMiniFlavor {
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_jump = 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);
Expand Down Expand Up @@ -590,6 +596,7 @@ class AvmMiniFlavor {
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_jump, 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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -566,6 +566,30 @@ void AvmMiniTraceBuilder::halt()
});
}

/**
* @brief JUMP OPCODE
* Jumps to a new `jmpDest`
* This function must:
* - Set the next program counter to the provided `jmpDest`.
*
* @param jmpDest - The destination to jump to
*/
void AvmMiniTraceBuilder::jump(uint32_t jmpDest)
{
auto clk = mainTrace.size();

mainTrace.push_back(Row{
.avmMini_clk = clk,
.avmMini_pc = FF(pc),
.avmMini_internal_return_ptr = FF(internal_return_ptr),
.avmMini_sel_jump = FF(1),
.avmMini_ia = FF(jmpDest),
});

// Adjust parameters for the next row
pc = jmpDest;
}

/**
* @brief INTERNAL_CALL OPCODE
* This opcode effectively jumps to a new `jmpDest` and stores the return program counter
Expand All @@ -588,18 +612,19 @@ void AvmMiniTraceBuilder::internal_call(uint32_t jmpDest)
internal_call_stack.push(stored_pc);

// Add the return location to the memory trace
storeInMemTrace(IntermRegister::ia, internal_return_ptr, FF(stored_pc), AvmMemoryTag::ff);
storeInMemTrace(IntermRegister::ib, internal_return_ptr, FF(stored_pc), AvmMemoryTag::ff);
memory.at(internal_return_ptr) = stored_pc;

mainTrace.push_back(Row{
.avmMini_clk = clk,
.avmMini_pc = FF(pc),
.avmMini_internal_return_ptr = FF(internal_return_ptr),
.avmMini_sel_internal_call = FF(1),
.avmMini_ia = stored_pc,
.avmMini_mem_op_a = FF(1),
.avmMini_rwa = FF(1),
.avmMini_mem_idx_a = FF(internal_return_ptr),
.avmMini_ia = FF(jmpDest),
.avmMini_ib = stored_pc,
.avmMini_mem_op_b = FF(1),
.avmMini_rwb = FF(1),
.avmMini_mem_idx_b = FF(internal_return_ptr),
});

// Adjust parameters for the next row
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,9 @@ class AvmMiniTraceBuilder {
void div(uint32_t aOffset, uint32_t bOffset, uint32_t dstOffset, AvmMemoryTag inTag);

// Jump to a given program counter.
void jump(uint32_t jmpDest);

// Jump to a given program counter; storing the return location on a call stack.
// TODO(md): this program counter MUST be an operand to the OPCODE.
void internal_call(uint32_t jmpDest);

Expand Down
Loading
Loading