Skip to content

Commit

Permalink
6245: migrate internal call stack to its own address space
Browse files Browse the repository at this point in the history
  • Loading branch information
jeanmon committed May 17, 2024
1 parent 19785bd commit a466b03
Show file tree
Hide file tree
Showing 24 changed files with 576 additions and 340 deletions.
47 changes: 35 additions & 12 deletions barretenberg/cpp/pil/avm/avm_main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
include "avm_mem.pil";
include "avm_alu.pil";
include "avm_binary.pil";
include "constants.pil";
include "avm_kernel.pil";
include "gadgets/avm_conversion.pil";

Expand Down Expand Up @@ -47,6 +48,8 @@ namespace avm_main(256);
pol commit pc;
// Return Pointer
pol commit internal_return_ptr;
// Call Pointer (nested call)
pol commit call_ptr;

pol commit sel_internal_call;
pol commit sel_internal_return;
Expand All @@ -55,6 +58,9 @@ namespace avm_main(256);
// Halt program execution
pol commit sel_halt;

// Memory Space Identifier
pol commit space_id;

//===== MEMORY OPCODES ==========================================================
pol commit sel_mov;
pol commit sel_cmov;
Expand Down Expand Up @@ -330,6 +336,13 @@ namespace avm_main(256);

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

//====== SPACE ID CONSTRAINTS ===============================================
#[SPACE_ID_INTERNAL]
(sel_internal_call + sel_internal_return) * (space_id - constants.INTERNAL_CALL_SPACE_ID) = 0;

#[SPACE_ID_STANDARD_OPCODES]
OPCODE_SELECTORS * (call_ptr - space_id) = 0;

//====== MEMORY OPCODES CONSTRAINTS =========================================

// TODO: consolidate with zero division error handling
Expand Down Expand Up @@ -463,42 +476,52 @@ namespace avm_main(256);
avm_conversion.to_radix_le_sel {avm_conversion.clk, avm_conversion.input, avm_conversion.radix, avm_conversion.num_limbs};

#[PERM_MAIN_MEM_A]
mem_op_a {clk, mem_idx_a, ia, rwa
mem_op_a {clk, space_id, mem_idx_a, ia, rwa
, r_in_tag, w_in_tag, sel_mov_a, sel_cmov}
is
avm_mem.op_a {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw
avm_mem.op_a {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val, avm_mem.rw
, avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.sel_mov_a, avm_mem.sel_cmov};

#[PERM_MAIN_MEM_B]
mem_op_b {clk, mem_idx_b, ib, rwb
mem_op_b {clk, space_id, mem_idx_b, ib, rwb
, r_in_tag, w_in_tag, sel_mov_b, sel_cmov}
is
avm_mem.op_b {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw
avm_mem.op_b {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val, avm_mem.rw
, avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.sel_mov_b, avm_mem.sel_cmov};

#[PERM_MAIN_MEM_C]
mem_op_c {clk, mem_idx_c, ic, rwc, r_in_tag, w_in_tag}
mem_op_c {clk, space_id, mem_idx_c, ic, rwc
, r_in_tag, w_in_tag}
is
avm_mem.op_c {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw, avm_mem.r_in_tag, avm_mem.w_in_tag};
avm_mem.op_c {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val, avm_mem.rw
, avm_mem.r_in_tag, avm_mem.w_in_tag};

#[PERM_MAIN_MEM_D]
mem_op_d {clk, mem_idx_d, id, rwd
mem_op_d {clk, space_id, mem_idx_d, id, rwd
, r_in_tag, w_in_tag, sel_cmov}
is
avm_mem.op_d {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw
avm_mem.op_d {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val, avm_mem.rw
, avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.sel_cmov};

#[PERM_MAIN_MEM_IND_A]
ind_op_a {clk, ind_a, mem_idx_a} is avm_mem.ind_op_a {avm_mem.clk, avm_mem.addr, avm_mem.val};
ind_op_a {clk, space_id, ind_a, mem_idx_a}
is
avm_mem.ind_op_a {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val};

#[PERM_MAIN_MEM_IND_B]
ind_op_b {clk, ind_b, mem_idx_b} is avm_mem.ind_op_b {avm_mem.clk, avm_mem.addr, avm_mem.val};
ind_op_b {clk, space_id, ind_b, mem_idx_b}
is
avm_mem.ind_op_b {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val};

#[PERM_MAIN_MEM_IND_C]
ind_op_c {clk, ind_c, mem_idx_c} is avm_mem.ind_op_c {avm_mem.clk, avm_mem.addr, avm_mem.val};
ind_op_c {clk, space_id, ind_c, mem_idx_c}
is
avm_mem.ind_op_c {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val};

#[PERM_MAIN_MEM_IND_D]
ind_op_d {clk, ind_d, mem_idx_d} is avm_mem.ind_op_d {avm_mem.clk, avm_mem.addr, avm_mem.val};
ind_op_d {clk, space_id, ind_d, mem_idx_d}
is
avm_mem.ind_op_d {avm_mem.clk, avm_mem.space_id, avm_mem.addr, avm_mem.val};

#[LOOKUP_MEM_RNG_CHK_LO]
avm_mem.rng_chk_sel {avm_mem.diff_lo} in sel_rng_16 {clk};
Expand Down
6 changes: 5 additions & 1 deletion barretenberg/cpp/pil/avm/avm_mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,10 @@ namespace avm_mem(256);
#[MEM_FIRST_EMPTY]
avm_main.first * mem_sel = 0;

// Definition of last, i.e., last row with mem_sel activated
#[MEM_LAST]
(1 - last) * mem_sel * (1 - mem_sel') = 0;

// Definition of rng_chk_sel. It is a boolean as mem_sel and last are booleans.
rng_chk_sel = mem_sel * (1 - last);

Expand Down Expand Up @@ -127,7 +131,7 @@ namespace avm_mem(256);
// Therefore, we ensure proper grouping of each global address and each memory access pertaining to a given
// global address is sorted according the arrow of time.
#[DIFF_RNG_CHK_DEC]
rng_chk_sel * (DIFF - diff_hi * 2**32 + diff_mid * 2**16 - diff_lo) = 0;
rng_chk_sel * (DIFF - diff_hi * 2**32 - diff_mid * 2**16 - diff_lo) = 0;

// lastAccess == 0 && rw' == 0 ==> val == val'
// This condition does not apply on the last row.
Expand Down
2 changes: 2 additions & 0 deletions barretenberg/cpp/pil/avm/constants.pil
Original file line number Diff line number Diff line change
Expand Up @@ -27,3 +27,5 @@ namespace constants(256);

pol TRANSACTION_FEE_SELECTOR = 39;

// Other AVM specific constants
pol INTERNAL_CALL_SPACE_ID = 255;
Loading

0 comments on commit a466b03

Please sign in to comment.