Skip to content

Commit

Permalink
6245 - introduce space_id and global address in memory trace
Browse files Browse the repository at this point in the history
  • Loading branch information
@jeanmon
jeanmon committed May 17, 2024
1 parent 7a31896 commit 19785bd
Show file tree
Hide file tree
Showing 14 changed files with 398 additions and 93 deletions.
5 changes: 4 additions & 1 deletion barretenberg/cpp/pil/avm/avm_main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -503,8 +503,11 @@ namespace avm_main(256);
#[LOOKUP_MEM_RNG_CHK_LO]
avm_mem.rng_chk_sel {avm_mem.diff_lo} in sel_rng_16 {clk};

#[LOOKUP_MEM_RNG_CHK_MID]
avm_mem.rng_chk_sel {avm_mem.diff_mid} in sel_rng_16 {clk};

#[LOOKUP_MEM_RNG_CHK_HI]
avm_mem.rng_chk_sel {avm_mem.diff_hi} in sel_rng_16 {clk};
avm_mem.rng_chk_sel {avm_mem.diff_hi} in sel_rng_8 {clk};

//====== Inter-table Shift Constraints (Lookups) ============================================
// Currently only used for shift operations but can be generalised for other uses.
Expand Down
40 changes: 23 additions & 17 deletions barretenberg/cpp/pil/avm/avm_mem.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ namespace avm_mem(256);
pol commit clk;
pol commit tsp; // Timestamp derived form clk and sub-operation types (SUB_CLK)
pol commit addr;
pol commit space_id;
pol commit glob_addr;
pol commit tag; // Memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
pol commit val;
pol commit rw; // Enum: 0 (read), 1 (write)
Expand Down Expand Up @@ -41,9 +43,10 @@ namespace avm_mem(256);

// Helper columns
pol commit one_min_inv; // Extra value to prove r_in_tag != tag with error handling
// pol DIFF: Difference between two consecutive timestamps or two consecutive addresses
pol commit diff_hi; // Higher 16-bit limb of diff.
pol commit diff_lo; // Lower 16-bit limb of diff.
// pol DIFF: 40-bit difference between two consecutive timestamps or two consecutive addresses
pol commit diff_hi; // Higher 8-bit limb of diff.
pol commit diff_mid; // Middle 16-bit limb of diff.
pol commit diff_lo; // Lower 16-bit limb of diff.

// Type constraints
lastAccess * (1 - lastAccess) = 0;
Expand Down Expand Up @@ -94,34 +97,37 @@ namespace avm_mem(256);
#[TIMESTAMP]
tsp = NUM_SUB_CLK * clk + SUB_CLK;

#[GLOBAL_ADDR]
glob_addr = space_id * 2**32 + addr;

#[LAST_ACCESS_FIRST_ROW]
avm_main.first * (1 - lastAccess) = 0;
// Remark: lastAccess == 1 on first row and therefore any relation with the
// multiplicative term (1 - lastAccess) implicitly includes (1 - avm_main.first)
// Similarly, this includes (1 - last) as well.

// lastAccess == 0 ==> addr' == addr
// lastAccess == 0 ==> glob_addr' == glob_addr
// Optimization: We removed the term (1 - avm_main.first)
#[MEM_LAST_ACCESS_DELIMITER]
(1 - lastAccess) * (addr' - addr) = 0;
(1 - lastAccess) * (glob_addr' - glob_addr) = 0;

// We need: lastAccess == 1 ==> addr' > addr
// The above implies: addr' == addr ==> lastAccess == 0
// We need: lastAccess == 1 ==> glob_addr' > glob_addr
// The above implies: glob_addr' == glob_addr ==> lastAccess == 0
// This condition does not apply on the last row.

// In addition, we need addr' == addr ==> tsp' > tsp
// In addition, we need glob_addr' == glob_addr ==> tsp' > tsp
// For all rows pertaining to the memory trace (mem_sel == 1) except the last one,
// i.e., when rng_chk_sel == 1, we compute the difference:
// 1) addr' - addr if lastAccess == 1
// 2) tsp' - tsp if lastAccess == 0 (i.e., whenever addr' == addr)
pol DIFF = lastAccess * (addr' - addr) + (1 - lastAccess) * (tsp' - tsp);

// We perform a 32-bit range check of DIFF which proves that addr' > addr if lastAccess == 1
// and tsp' > tsp whenever addr' == addr
// Therefore, we ensure proper grouping of each address and each memory access pertaining to a given
// address is sorted according the arrow of time.
// 1) glob_addr' - glob_addr if lastAccess == 1
// 2) tsp' - tsp if lastAccess == 0 (i.e., whenever glob_addr' == glob_addr)
pol DIFF = lastAccess * (glob_addr' - glob_addr) + (1 - lastAccess) * (tsp' - tsp);

// We perform a 40-bit range check of DIFF which proves that glob_addr' > glob_addr if lastAccess == 1
// and tsp' > tsp whenever glob_addr' == glob_addr
// 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**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
99 changes: 57 additions & 42 deletions barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_mem.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,12 @@ namespace bb::Avm_vm {
template <typename FF> struct Avm_memRow {
FF avm_main_first{};
FF avm_mem_addr{};
FF avm_mem_addr_shift{};
FF avm_mem_clk{};
FF avm_mem_diff_hi{};
FF avm_mem_diff_lo{};
FF avm_mem_diff_mid{};
FF avm_mem_glob_addr{};
FF avm_mem_glob_addr_shift{};
FF avm_mem_ind_op_a{};
FF avm_mem_ind_op_b{};
FF avm_mem_ind_op_c{};
Expand All @@ -34,6 +36,7 @@ template <typename FF> struct Avm_memRow {
FF avm_mem_sel_mov_a{};
FF avm_mem_sel_mov_b{};
FF avm_mem_skip_check_tag{};
FF avm_mem_space_id{};
FF avm_mem_tag{};
FF avm_mem_tag_err{};
FF avm_mem_tag_shift{};
Expand All @@ -57,39 +60,42 @@ inline std::string get_relation_label_avm_mem(int index)
return "TIMESTAMP";

case 18:
return "LAST_ACCESS_FIRST_ROW";
return "GLOBAL_ADDR";

case 19:
return "MEM_LAST_ACCESS_DELIMITER";
return "LAST_ACCESS_FIRST_ROW";

case 20:
return "DIFF_RNG_CHK_DEC";
return "MEM_LAST_ACCESS_DELIMITER";

case 21:
return "MEM_READ_WRITE_VAL_CONSISTENCY";
return "DIFF_RNG_CHK_DEC";

case 22:
return "MEM_READ_WRITE_TAG_CONSISTENCY";
return "MEM_READ_WRITE_VAL_CONSISTENCY";

case 23:
return "MEM_ZERO_INIT";
return "MEM_READ_WRITE_TAG_CONSISTENCY";

case 24:
return "SKIP_CHECK_TAG";
return "MEM_ZERO_INIT";

case 25:
return "MEM_IN_TAG_CONSISTENCY_1";
return "SKIP_CHECK_TAG";

case 26:
return "MEM_IN_TAG_CONSISTENCY_2";
return "MEM_IN_TAG_CONSISTENCY_1";

case 27:
return "MEM_IN_TAG_CONSISTENCY_2";

case 28:
return "NO_TAG_ERR_WRITE_OR_SKIP";

case 29:
case 30:
return "NO_TAG_ERR_WRITE";

case 38:
case 39:
return "MOV_SAME_TAG";
}
return std::to_string(index);
Expand All @@ -99,9 +105,9 @@ template <typename FF_> class avm_memImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 39> SUBRELATION_PARTIAL_LENGTHS{
static constexpr std::array<size_t, 40> SUBRELATION_PARTIAL_LENGTHS{
3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 3, 4, 3, 3, 4, 3, 3,
4, 4, 4, 4, 4, 5, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
3, 4, 4, 4, 4, 4, 5, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3,
};

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -271,35 +277,35 @@ template <typename FF_> class avm_memImpl {
{
Avm_DECLARE_VIEWS(18);

auto tmp = (avm_main_first * (-avm_mem_lastAccess + FF(1)));
auto tmp = (avm_mem_glob_addr - ((avm_mem_space_id * FF(4294967296UL)) + avm_mem_addr));
tmp *= scaling_factor;
std::get<18>(evals) += tmp;
}
// Contribution 19
{
Avm_DECLARE_VIEWS(19);

auto tmp = ((-avm_mem_lastAccess + FF(1)) * (avm_mem_addr_shift - avm_mem_addr));
auto tmp = (avm_main_first * (-avm_mem_lastAccess + FF(1)));
tmp *= scaling_factor;
std::get<19>(evals) += tmp;
}
// Contribution 20
{
Avm_DECLARE_VIEWS(20);

auto tmp = (avm_mem_rng_chk_sel * ((((avm_mem_lastAccess * (avm_mem_addr_shift - avm_mem_addr)) +
((-avm_mem_lastAccess + FF(1)) * (avm_mem_tsp_shift - avm_mem_tsp))) -
(avm_mem_diff_hi * FF(65536))) -
avm_mem_diff_lo));
auto tmp = ((-avm_mem_lastAccess + FF(1)) * (avm_mem_glob_addr_shift - avm_mem_glob_addr));
tmp *= scaling_factor;
std::get<20>(evals) += tmp;
}
// Contribution 21
{
Avm_DECLARE_VIEWS(21);

auto tmp =
(((-avm_mem_lastAccess + FF(1)) * (-avm_mem_rw_shift + FF(1))) * (avm_mem_val_shift - avm_mem_val));
auto tmp = (avm_mem_rng_chk_sel * (((((avm_mem_lastAccess * (avm_mem_glob_addr_shift - avm_mem_glob_addr)) +
((-avm_mem_lastAccess + FF(1)) * (avm_mem_tsp_shift - avm_mem_tsp))) -
(avm_mem_diff_hi * FF(4294967296UL))) +
(avm_mem_diff_mid * FF(65536))) -
avm_mem_diff_lo));
tmp *= scaling_factor;
std::get<21>(evals) += tmp;
}
Expand All @@ -308,141 +314,150 @@ template <typename FF_> class avm_memImpl {
Avm_DECLARE_VIEWS(22);

auto tmp =
(((-avm_mem_lastAccess + FF(1)) * (-avm_mem_rw_shift + FF(1))) * (avm_mem_tag_shift - avm_mem_tag));
(((-avm_mem_lastAccess + FF(1)) * (-avm_mem_rw_shift + FF(1))) * (avm_mem_val_shift - avm_mem_val));
tmp *= scaling_factor;
std::get<22>(evals) += tmp;
}
// Contribution 23
{
Avm_DECLARE_VIEWS(23);

auto tmp = ((avm_mem_lastAccess * (-avm_mem_rw_shift + FF(1))) * avm_mem_val_shift);
auto tmp =
(((-avm_mem_lastAccess + FF(1)) * (-avm_mem_rw_shift + FF(1))) * (avm_mem_tag_shift - avm_mem_tag));
tmp *= scaling_factor;
std::get<23>(evals) += tmp;
}
// Contribution 24
{
Avm_DECLARE_VIEWS(24);

auto tmp = (avm_mem_skip_check_tag -
(avm_mem_sel_cmov * ((avm_mem_op_d + (avm_mem_op_a * (-avm_mem_sel_mov_a + FF(1)))) +
(avm_mem_op_b * (-avm_mem_sel_mov_b + FF(1))))));
auto tmp = ((avm_mem_lastAccess * (-avm_mem_rw_shift + FF(1))) * avm_mem_val_shift);
tmp *= scaling_factor;
std::get<24>(evals) += tmp;
}
// Contribution 25
{
Avm_DECLARE_VIEWS(25);

auto tmp = (((-avm_mem_skip_check_tag + FF(1)) * (-avm_mem_rw + FF(1))) *
(((avm_mem_r_in_tag - avm_mem_tag) * (-avm_mem_one_min_inv + FF(1))) - avm_mem_tag_err));
auto tmp = (avm_mem_skip_check_tag -
(avm_mem_sel_cmov * ((avm_mem_op_d + (avm_mem_op_a * (-avm_mem_sel_mov_a + FF(1)))) +
(avm_mem_op_b * (-avm_mem_sel_mov_b + FF(1))))));
tmp *= scaling_factor;
std::get<25>(evals) += tmp;
}
// Contribution 26
{
Avm_DECLARE_VIEWS(26);

auto tmp = ((-avm_mem_tag_err + FF(1)) * avm_mem_one_min_inv);
auto tmp = (((-avm_mem_skip_check_tag + FF(1)) * (-avm_mem_rw + FF(1))) *
(((avm_mem_r_in_tag - avm_mem_tag) * (-avm_mem_one_min_inv + FF(1))) - avm_mem_tag_err));
tmp *= scaling_factor;
std::get<26>(evals) += tmp;
}
// Contribution 27
{
Avm_DECLARE_VIEWS(27);

auto tmp = ((avm_mem_skip_check_tag + avm_mem_rw) * avm_mem_tag_err);
auto tmp = ((-avm_mem_tag_err + FF(1)) * avm_mem_one_min_inv);
tmp *= scaling_factor;
std::get<27>(evals) += tmp;
}
// Contribution 28
{
Avm_DECLARE_VIEWS(28);

auto tmp = (avm_mem_rw * (avm_mem_w_in_tag - avm_mem_tag));
auto tmp = ((avm_mem_skip_check_tag + avm_mem_rw) * avm_mem_tag_err);
tmp *= scaling_factor;
std::get<28>(evals) += tmp;
}
// Contribution 29
{
Avm_DECLARE_VIEWS(29);

auto tmp = (avm_mem_rw * avm_mem_tag_err);
auto tmp = (avm_mem_rw * (avm_mem_w_in_tag - avm_mem_tag));
tmp *= scaling_factor;
std::get<29>(evals) += tmp;
}
// Contribution 30
{
Avm_DECLARE_VIEWS(30);

auto tmp = (avm_mem_ind_op_a * (avm_mem_r_in_tag - FF(3)));
auto tmp = (avm_mem_rw * avm_mem_tag_err);
tmp *= scaling_factor;
std::get<30>(evals) += tmp;
}
// Contribution 31
{
Avm_DECLARE_VIEWS(31);

auto tmp = (avm_mem_ind_op_b * (avm_mem_r_in_tag - FF(3)));
auto tmp = (avm_mem_ind_op_a * (avm_mem_r_in_tag - FF(3)));
tmp *= scaling_factor;
std::get<31>(evals) += tmp;
}
// Contribution 32
{
Avm_DECLARE_VIEWS(32);

auto tmp = (avm_mem_ind_op_c * (avm_mem_r_in_tag - FF(3)));
auto tmp = (avm_mem_ind_op_b * (avm_mem_r_in_tag - FF(3)));
tmp *= scaling_factor;
std::get<32>(evals) += tmp;
}
// Contribution 33
{
Avm_DECLARE_VIEWS(33);

auto tmp = (avm_mem_ind_op_d * (avm_mem_r_in_tag - FF(3)));
auto tmp = (avm_mem_ind_op_c * (avm_mem_r_in_tag - FF(3)));
tmp *= scaling_factor;
std::get<33>(evals) += tmp;
}
// Contribution 34
{
Avm_DECLARE_VIEWS(34);

auto tmp = (avm_mem_ind_op_a * avm_mem_rw);
auto tmp = (avm_mem_ind_op_d * (avm_mem_r_in_tag - FF(3)));
tmp *= scaling_factor;
std::get<34>(evals) += tmp;
}
// Contribution 35
{
Avm_DECLARE_VIEWS(35);

auto tmp = (avm_mem_ind_op_b * avm_mem_rw);
auto tmp = (avm_mem_ind_op_a * avm_mem_rw);
tmp *= scaling_factor;
std::get<35>(evals) += tmp;
}
// Contribution 36
{
Avm_DECLARE_VIEWS(36);

auto tmp = (avm_mem_ind_op_c * avm_mem_rw);
auto tmp = (avm_mem_ind_op_b * avm_mem_rw);
tmp *= scaling_factor;
std::get<36>(evals) += tmp;
}
// Contribution 37
{
Avm_DECLARE_VIEWS(37);

auto tmp = (avm_mem_ind_op_d * avm_mem_rw);
auto tmp = (avm_mem_ind_op_c * avm_mem_rw);
tmp *= scaling_factor;
std::get<37>(evals) += tmp;
}
// Contribution 38
{
Avm_DECLARE_VIEWS(38);

auto tmp = ((avm_mem_sel_mov_a + avm_mem_sel_mov_b) * avm_mem_tag_err);
auto tmp = (avm_mem_ind_op_d * avm_mem_rw);
tmp *= scaling_factor;
std::get<38>(evals) += tmp;
}
// Contribution 39
{
Avm_DECLARE_VIEWS(39);

auto tmp = ((avm_mem_sel_mov_a + avm_mem_sel_mov_b) * avm_mem_tag_err);
tmp *= scaling_factor;
std::get<39>(evals) += tmp;
}
}
};

Expand Down
Loading

0 comments on commit 19785bd

Please sign in to comment.