Skip to content
Closed
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: 39 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/mem_slice.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
include "../main.pil";

namespace slice(256);
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I think I get what this does, my only comment is naming:
calling it slice (or better, mem_slice) makes it look like it's generic but then even the core relations like "addresses should be decreasing" and "cnt management" do use calldatacopy-specific selectors. Should this just be called the calldata gadget?

(I do understand that even if the gadget was a generic slice read/write gadget then there would be some mention of calldata, just like it happens with normal memory... we need at least some selectors for lookups/perms)

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

What will happen for sure is that return opcode will be performed in the same trace. So, there will be specific selectors for calldatacopy and return opcode. Other columns like cnt, and addr, can be re-used. That is why I named it slice. I chose a short prefix, as the namespace is prefixed for any field of this trace.


pol commit clk;

pol commit sel_start_cd_cpy; // Selector to indicate the start of calldatacopy. Used in permutation with the main trace.
pol commit sel_cd_cpy; // Selector for any row involved in a callatacopy operation.
pol commit cnt; // Decreasing counter to track the number of memory operations.
pol commit space_id; // Copied from main trace.
pol commit addr; // Address pertaining to the memory operation.
pol commit val; // Value pertaining to the memory operation.
pol commit cd_offset; // Offset of the calldata element. It is used to get the correct value from calldata.
pol commit one_min_inv; // Helper column to assert zero/non-zero equality of cnt;

sel_cd_cpy * (1 - sel_cd_cpy) = 0;
// TODO: might not be required
sel_start_cd_cpy * (1 - sel_start_cd_cpy) = 0;

// Show that cnt != 0 <==> sel_cd_cpy == 1
// one_min_inv == 1 - cnt^(-1) if cnt != 0 else == 0
#[SLICE_CNT_ZERO_TEST1]
cnt * (1 - one_min_inv) - sel_cd_cpy = 0;
#[SLICE_CNT_ZERO_TEST2]
(1 - sel_cd_cpy) * one_min_inv = 0;

#[SLICE_CNT_DECREMENT]
sel_cd_cpy * (cnt - 1 - cnt') = 0;

#[ADDR_CNT_INCREMENT]
sel_cd_cpy * (addr + 1 - addr') = 0;
#[CD_OFFSET_INCREMENT]
sel_cd_cpy * (cd_offset + 1 - cd_offset') = 0;

#[LOOKUP_CD_VALUE]
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I wonder if this one shouldn't be in main.pil? It really depends. If this is a calldata-specific gadget, then no. If this is a generic slice gadget, maybe yes? (very optional, I'm ok if things stay as they are)

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

This is very calldata-specific. Calladata column being defined in the main trace, we could have defined this permutation there as well. I thought due to the specificity, we keep it here.

sel_cd_cpy {cd_offset, val} in main.sel_calldata {main.clk, main.calldata};

#[PERM_CD_MEM]
sel_cd_cpy {clk, space_id, addr, val} is mem.sel_op_cd_cpy {mem.clk, mem.space_id, mem.addr, mem.val};
26 changes: 23 additions & 3 deletions barretenberg/cpp/pil/avm/main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ include "gadgets/sha256.pil";
include "gadgets/poseidon2.pil";
include "gadgets/keccakf1600.pil";
include "gadgets/pedersen.pil";
include "gadgets/mem_slice.pil";

namespace main(256);
//===== CONSTANT POLYNOMIALS ==================================================
Expand All @@ -20,6 +21,7 @@ namespace main(256);

//===== PUBLIC COLUMNS=========================================================
pol public calldata;
pol commit sel_calldata; // Selector used for lookup in calldata. TODO: Might be removed or made constant.

//===== KERNEL INPUTS =========================================================
// Kernel lookup selector opcodes
Expand Down Expand Up @@ -139,6 +141,9 @@ namespace main(256);
pol commit sel_op_keccak;
pol commit sel_op_pedersen;

//===== Memory Slice Gadget Selectors =========================================
pol commit sel_op_calldata_copy;

//===== Fix Range Checks Selectors=============================================
// We re-use the clk column for the lookup values of 8-bit resp. 16-bit range check.
pol commit sel_rng_8; // Boolean selector for the 8-bit range check lookup
Expand Down Expand Up @@ -321,6 +326,8 @@ namespace main(256);
sel_op_halt * (1 - sel_op_halt) = 0;
sel_op_external_call * (1 - sel_op_external_call) = 0;

sel_op_calldata_copy * (1 - sel_op_calldata_copy) = 0;

// Might be removed if derived from opcode based on a lookup of constants
sel_op_mov * ( 1 - sel_op_mov) = 0;
sel_op_cmov * ( 1 - sel_op_cmov) = 0;
Expand Down Expand Up @@ -473,12 +480,13 @@ namespace main(256);
pol SEL_ALL_BINARY = sel_op_and + sel_op_or + sel_op_xor;
pol SEL_ALL_GADGET = sel_op_radix_le + sel_op_sha256 + sel_op_poseidon2 + sel_op_keccak + sel_op_pedersen;
pol SEL_ALL_MEMORY = sel_op_cmov + sel_op_mov;
pol SEL_ALL_MEM_SLICE = sel_op_calldata_copy;
pol OPCODE_SELECTORS = sel_op_fdiv + SEL_ALU_ALL + SEL_ALL_BINARY + SEL_ALL_MEMORY + SEL_ALL_GADGET
+ KERNEL_INPUT_SELECTORS + KERNEL_OUTPUT_SELECTORS + SEL_ALL_LEFTGAS;
+ KERNEL_INPUT_SELECTORS + KERNEL_OUTPUT_SELECTORS + SEL_ALL_LEFTGAS + SEL_ALL_MEM_SLICE;

// TODO: sel_gas_accounting_active is activating gas accounting on a given row. All opcode with selectors
// are activated through the relation below. The other opcodes which are implemented purely
// through memory sub-operations such as CALLDATACOPY, RETURN, SET are activated by
// through memory sub-operations such as RETURN, SET are activated by
// setting a newly introduced boolean sel_mem_op_activate_gas which is set in witness generation.
// We should remove this shortcut and constrain this activation through bytecode decomposition.
// Alternatively, we introduce a boolean selector for the three opcodes mentioned above.
Expand Down Expand Up @@ -656,13 +664,20 @@ namespace main(256);
// We increment the side effect counter by 1
KERNEL_OUTPUT_SELECTORS * (kernel.side_effect_counter' - (kernel.side_effect_counter + 1)) = 0;

//===== Memory Slice Constraints ============================================
pol commit sel_cd_cpy_gadget; // Selector to activate the calldatacopy operation in the gadget (#[PERM_MAIN_CD_COPY]).

// Activate only if tag_err is disabled
sel_cd_cpy_gadget = sel_op_calldata_copy * (1 - tag_err);

//====== Inter-table Constraints ============================================

#[KERNEL_OUTPUT_LOOKUP]
sel_q_kernel_output_lookup {kernel.kernel_out_offset, ia, kernel.side_effect_counter, ib} in kernel.q_public_input_kernel_out_add_to_table {clk, kernel.kernel_value_out, kernel.kernel_side_effect_out, kernel.kernel_metadata_out};

#[LOOKUP_INTO_KERNEL]
sel_q_kernel_lookup { main.ia, kernel.kernel_in_offset } in kernel.q_public_input_kernel_add_to_table { kernel.kernel_inputs, clk };

//====== Inter-table Constraints ============================================
#[INCL_MAIN_TAG_ERR]
mem.tag_err {mem.clk} in tag_err {clk};

Expand Down Expand Up @@ -723,6 +738,11 @@ namespace main(256);
is
pedersen.sel_pedersen {pedersen.clk, pedersen.input};

#[PERM_MAIN_CD_COPY]
sel_cd_cpy_gadget {ia, ib, mem_addr_c}
is
slice.sel_start_cd_cpy {slice.cd_offset, slice.cnt, slice.addr};

#[PERM_MAIN_MEM_A]
sel_mem_op_a {clk, space_id, mem_addr_a, ia, rwa, r_in_tag, w_in_tag, sel_mov_ia_to_ic, sel_op_cmov}
is
Expand Down
19 changes: 17 additions & 2 deletions barretenberg/cpp/pil/avm/mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,9 @@ namespace mem(256);
pol commit sel_resolve_ind_addr_c;
pol commit sel_resolve_ind_addr_d;

// Selector for calldata_copy memory operations triggered from memory slice gadget.
pol commit sel_op_cd_cpy;

// Selectors related to MOV/CMOV opcodes (copied from main trace for loading operation on intermediated register ia/ib)
// Boolean constraint is performed in main trace.
pol commit sel_mov_ia_to_ic;
Expand All @@ -57,6 +60,7 @@ namespace mem(256);
sel_op_b * (1 - sel_op_b) = 0;
sel_op_c * (1 - sel_op_c) = 0;
sel_op_d * (1 - sel_op_d) = 0;
sel_op_cd_cpy * (1 - sel_op_cd_cpy) = 0;
sel_resolve_ind_addr_a * (1 - sel_resolve_ind_addr_a) = 0;
sel_resolve_ind_addr_b * (1 - sel_resolve_ind_addr_b) = 0;
sel_resolve_ind_addr_c * (1 - sel_resolve_ind_addr_c) = 0;
Expand All @@ -66,8 +70,9 @@ namespace mem(256);
// 2) Ensure that tag, r_in_tag, w_in_tag are properly constrained by the main trace and/or bytecode decomposition

// Definition of sel_mem
sel_mem = sel_op_a + sel_op_b + sel_op_c + sel_op_d +
sel_resolve_ind_addr_a + sel_resolve_ind_addr_b + sel_resolve_ind_addr_c + sel_resolve_ind_addr_d;
sel_mem = sel_op_a + sel_op_b + sel_op_c + sel_op_d
+ sel_resolve_ind_addr_a + sel_resolve_ind_addr_b + sel_resolve_ind_addr_c + sel_resolve_ind_addr_d
+ sel_op_cd_cpy;
// Maximum one memory operation enabled per row
sel_mem * (sel_mem - 1) = 0; // TODO: might be infered by the main trace

Expand Down Expand Up @@ -99,6 +104,11 @@ namespace mem(256);
pol SUB_CLK = sel_mem * (sel_resolve_ind_addr_b + sel_op_b + 2 * (sel_resolve_ind_addr_c + sel_op_c) + 3 * (sel_resolve_ind_addr_d + sel_op_d) + 4 * (1 - IND_OP + rw));
// We need the sel_mem factor as the right factor is not zero when all columns are zero.

// Calldata_copy memory slice operations will have a sub_clk value of 8 as rw == 1 which is outside of the range of
// indirect memory operations. This is crucial as a main trace entry for calldata_copy triggers an indirect memory
// load operation for intermediate register c. The write slice memory operations will have the same sub_clk which in
// this particular case is not a problem as all addresses are different.

#[TIMESTAMP]
tsp = NUM_SUB_CLK * clk + SUB_CLK;

Expand Down Expand Up @@ -154,6 +164,7 @@ namespace mem(256);
#[MEM_ZERO_INIT]
lastAccess * (1 - rw') * val' = 0;

// TODO: Verfiy that skip_check_tag cannot be enabled maliciously by the prover.
// Skip check tag
#[SKIP_CHECK_TAG]
skip_check_tag = sel_op_cmov * (sel_op_d + sel_op_a * (1-sel_mov_ia_to_ic) + sel_op_b * (1-sel_mov_ib_to_ic));
Expand Down Expand Up @@ -207,6 +218,10 @@ namespace mem(256);
sel_resolve_ind_addr_c * rw = 0;
sel_resolve_ind_addr_d * rw = 0;

//====== CALLDATACOPY specific constraints ==================================
sel_op_cd_cpy * (rw - 1) = 0;
sel_op_cd_cpy * (w_in_tag - 6) = 0; // Only write elements of type FF

//====== MOV/CMOV Opcode Tag Constraint =====================================
// The following constraint ensures that the r_in_tag is set to tag for
// the load operation pertaining to Ia resp. Ib.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -184,6 +184,8 @@
[[maybe_unused]] auto main_rwd = View(new_term.main_rwd); \
[[maybe_unused]] auto main_sel_alu = View(new_term.main_sel_alu); \
[[maybe_unused]] auto main_sel_bin = View(new_term.main_sel_bin); \
[[maybe_unused]] auto main_sel_calldata = View(new_term.main_sel_calldata); \
[[maybe_unused]] auto main_sel_cd_cpy_gadget = View(new_term.main_sel_cd_cpy_gadget); \
[[maybe_unused]] auto main_sel_gas_accounting_active = View(new_term.main_sel_gas_accounting_active); \
[[maybe_unused]] auto main_sel_last = View(new_term.main_sel_last); \
[[maybe_unused]] auto main_sel_mem_op_a = View(new_term.main_sel_mem_op_a); \
Expand All @@ -197,6 +199,7 @@
[[maybe_unused]] auto main_sel_op_address = View(new_term.main_sel_op_address); \
[[maybe_unused]] auto main_sel_op_and = View(new_term.main_sel_op_and); \
[[maybe_unused]] auto main_sel_op_block_number = View(new_term.main_sel_op_block_number); \
[[maybe_unused]] auto main_sel_op_calldata_copy = View(new_term.main_sel_op_calldata_copy); \
[[maybe_unused]] auto main_sel_op_cast = View(new_term.main_sel_op_cast); \
[[maybe_unused]] auto main_sel_op_chain_id = View(new_term.main_sel_op_chain_id); \
[[maybe_unused]] auto main_sel_op_cmov = View(new_term.main_sel_op_cmov); \
Expand Down Expand Up @@ -273,6 +276,7 @@
[[maybe_unused]] auto mem_sel_op_a = View(new_term.mem_sel_op_a); \
[[maybe_unused]] auto mem_sel_op_b = View(new_term.mem_sel_op_b); \
[[maybe_unused]] auto mem_sel_op_c = View(new_term.mem_sel_op_c); \
[[maybe_unused]] auto mem_sel_op_cd_cpy = View(new_term.mem_sel_op_cd_cpy); \
[[maybe_unused]] auto mem_sel_op_cmov = View(new_term.mem_sel_op_cmov); \
[[maybe_unused]] auto mem_sel_op_d = View(new_term.mem_sel_op_d); \
[[maybe_unused]] auto mem_sel_resolve_ind_addr_a = View(new_term.mem_sel_resolve_ind_addr_a); \
Expand Down Expand Up @@ -301,11 +305,22 @@
[[maybe_unused]] auto sha256_output = View(new_term.sha256_output); \
[[maybe_unused]] auto sha256_sel_sha256_compression = View(new_term.sha256_sel_sha256_compression); \
[[maybe_unused]] auto sha256_state = View(new_term.sha256_state); \
[[maybe_unused]] auto slice_addr = View(new_term.slice_addr); \
[[maybe_unused]] auto slice_cd_offset = View(new_term.slice_cd_offset); \
[[maybe_unused]] auto slice_clk = View(new_term.slice_clk); \
[[maybe_unused]] auto slice_cnt = View(new_term.slice_cnt); \
[[maybe_unused]] auto slice_one_min_inv = View(new_term.slice_one_min_inv); \
[[maybe_unused]] auto slice_sel_cd_cpy = View(new_term.slice_sel_cd_cpy); \
[[maybe_unused]] auto slice_sel_start_cd_cpy = View(new_term.slice_sel_start_cd_cpy); \
[[maybe_unused]] auto slice_space_id = View(new_term.slice_space_id); \
[[maybe_unused]] auto slice_val = View(new_term.slice_val); \
[[maybe_unused]] auto perm_cd_mem = View(new_term.perm_cd_mem); \
[[maybe_unused]] auto perm_main_alu = View(new_term.perm_main_alu); \
[[maybe_unused]] auto perm_main_bin = View(new_term.perm_main_bin); \
[[maybe_unused]] auto perm_main_conv = View(new_term.perm_main_conv); \
[[maybe_unused]] auto perm_main_pos2_perm = View(new_term.perm_main_pos2_perm); \
[[maybe_unused]] auto perm_main_pedersen = View(new_term.perm_main_pedersen); \
[[maybe_unused]] auto perm_main_cd_copy = View(new_term.perm_main_cd_copy); \
[[maybe_unused]] auto perm_main_mem_a = View(new_term.perm_main_mem_a); \
[[maybe_unused]] auto perm_main_mem_b = View(new_term.perm_main_mem_b); \
[[maybe_unused]] auto perm_main_mem_c = View(new_term.perm_main_mem_c); \
Expand All @@ -316,6 +331,7 @@
[[maybe_unused]] auto perm_main_mem_ind_addr_d = View(new_term.perm_main_mem_ind_addr_d); \
[[maybe_unused]] auto lookup_byte_lengths = View(new_term.lookup_byte_lengths); \
[[maybe_unused]] auto lookup_byte_operations = View(new_term.lookup_byte_operations); \
[[maybe_unused]] auto lookup_cd_value = View(new_term.lookup_cd_value); \
[[maybe_unused]] auto lookup_opcode_gas = View(new_term.lookup_opcode_gas); \
[[maybe_unused]] auto range_check_l2_gas_hi = View(new_term.range_check_l2_gas_hi); \
[[maybe_unused]] auto range_check_l2_gas_lo = View(new_term.range_check_l2_gas_lo); \
Expand Down Expand Up @@ -357,6 +373,7 @@
[[maybe_unused]] auto lookup_div_u16_7 = View(new_term.lookup_div_u16_7); \
[[maybe_unused]] auto lookup_byte_lengths_counts = View(new_term.lookup_byte_lengths_counts); \
[[maybe_unused]] auto lookup_byte_operations_counts = View(new_term.lookup_byte_operations_counts); \
[[maybe_unused]] auto lookup_cd_value_counts = View(new_term.lookup_cd_value_counts); \
[[maybe_unused]] auto lookup_opcode_gas_counts = View(new_term.lookup_opcode_gas_counts); \
[[maybe_unused]] auto range_check_l2_gas_hi_counts = View(new_term.range_check_l2_gas_hi_counts); \
[[maybe_unused]] auto range_check_l2_gas_lo_counts = View(new_term.range_check_l2_gas_lo_counts); \
Expand Down Expand Up @@ -468,4 +485,7 @@
[[maybe_unused]] auto mem_sel_mem_shift = View(new_term.mem_sel_mem_shift); \
[[maybe_unused]] auto mem_tag_shift = View(new_term.mem_tag_shift); \
[[maybe_unused]] auto mem_tsp_shift = View(new_term.mem_tsp_shift); \
[[maybe_unused]] auto mem_val_shift = View(new_term.mem_val_shift);
[[maybe_unused]] auto mem_val_shift = View(new_term.mem_val_shift); \
[[maybe_unused]] auto slice_addr_shift = View(new_term.slice_addr_shift); \
[[maybe_unused]] auto slice_cd_offset_shift = View(new_term.slice_cd_offset_shift); \
[[maybe_unused]] auto slice_cnt_shift = View(new_term.slice_cnt_shift);
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
#pragma once

#include "barretenberg/relations/generic_lookup/generic_lookup_relation.hpp"

#include <cstddef>
#include <tuple>

namespace bb {

class lookup_cd_value_lookup_settings {
public:
static constexpr size_t READ_TERMS = 1;
static constexpr size_t WRITE_TERMS = 1;
static constexpr size_t READ_TERM_TYPES[READ_TERMS] = { 0 };
static constexpr size_t WRITE_TERM_TYPES[WRITE_TERMS] = { 0 };
static constexpr size_t LOOKUP_TUPLE_SIZE = 2;
static constexpr size_t INVERSE_EXISTS_POLYNOMIAL_DEGREE = 4;
static constexpr size_t READ_TERM_DEGREE = 0;
static constexpr size_t WRITE_TERM_DEGREE = 0;

template <typename AllEntities> static inline auto inverse_polynomial_is_computed_at_row(const AllEntities& in)
{
return (in.slice_sel_cd_cpy == 1 || in.main_sel_calldata == 1);
}

template <typename Accumulator, typename AllEntities>
static inline auto compute_inverse_exists(const AllEntities& in)
{
using View = typename Accumulator::View;
const auto is_operation = View(in.slice_sel_cd_cpy);
const auto is_table_entry = View(in.main_sel_calldata);
return (is_operation + is_table_entry - is_operation * is_table_entry);
}

template <typename AllEntities> static inline auto get_const_entities(const AllEntities& in)
{
return std::forward_as_tuple(in.lookup_cd_value,
in.lookup_cd_value_counts,
in.slice_sel_cd_cpy,
in.main_sel_calldata,
in.slice_cd_offset,
in.slice_val,
in.main_clk,
in.main_calldata);
}

template <typename AllEntities> static inline auto get_nonconst_entities(AllEntities& in)
{
return std::forward_as_tuple(in.lookup_cd_value,
in.lookup_cd_value_counts,
in.slice_sel_cd_cpy,
in.main_sel_calldata,
in.slice_cd_offset,
in.slice_val,
in.main_clk,
in.main_calldata);
}
};

template <typename FF_>
class lookup_cd_value_relation : public GenericLookupRelation<lookup_cd_value_lookup_settings, FF_> {
public:
static constexpr const char* NAME = "lookup_cd_value";
};
template <typename FF_> using lookup_cd_value = GenericLookup<lookup_cd_value_lookup_settings, FF_>;

} // namespace bb
Loading