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): calldatacopy and return gadget #7415

Merged
merged 12 commits into from
Jul 10, 2024
77 changes: 77 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/mem_slice.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
include "../main.pil";

namespace slice(256);

pol commit clk;

pol commit sel_start; // Selector to indicate the start of calldatacopy/return. Used in permutation with the main trace.
pol commit sel_cd_cpy; // Selector for any row involved in a callatacopy operation.
pol commit sel_return; // Selector for any row involved in a return operation.
pol commit sel_mem_active; // Selector for any row involved in a memory 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 col_offset; // Offset of the public column element. It is used to get the correct value from calldata/returndata.
pol commit one_min_inv; // Helper column to assert zero/non-zero equality of cnt;

// We use a counter corresponding to the number of memory operations. The counter
// is initialized by copying the size argument from the main trace. The counter column
// is shared for CALLDATACOPY and RETURN opcodes. The counter is decreased until
// it reaches the value zero. Each row with a non-zero counter corresponds to
// a memory operation. The following relations ensure that exactly one operation
// selector sel_cd_cpy/sel_return is activated per row with a non-zero counter and
// that within a given operation the pertaining selector is enabled. (One prevents
// to activate sel_return during a callatacopy operation and vice-versa.)

sel_mem_active = sel_cd_cpy + sel_return;

// Instruction decomposition guarantees that sel_cd_cpy and sel_return are mutually exclusive on
// the first row of the calldatcopy/return operation.

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

#[SLICE_CNT_DECREMENT]
sel_mem_active * (cnt - 1 - cnt') = 0;
#[ADDR_INCREMENT]
sel_mem_active * (addr + 1 - addr') = 0;
#[COL_OFFSET_INCREMENT]
sel_mem_active * (col_offset + 1 - col_offset') = 0;
#[SAME_CLK]
sel_mem_active * (clk - clk') = 0;
#[SAME_SPACE_ID]
sel_mem_active * (space_id - space_id') = 0;
#[SAME_SEL_RETURN]
sel_mem_active * sel_mem_active' * (sel_return - sel_return') = 0;
#[SAME_SEL_CD_CPY]
sel_mem_active * sel_mem_active' * (sel_cd_cpy - sel_cd_cpy') = 0;

#[SEL_MEM_INACTIVE]
(1 - sel_mem_active) * sel_mem_active' * (1 - sel_start') = 0;

// The above relation is crucial to prevent a malicious prover of adding extra active rows
// after the row with cnt == 0 unless another operation starts (sel_start == 1). This relation
// implies that whenever sel_mem_active == 0 and sel_start' != 1, sel_mem_active' == 0.
// Note that the malicious prover can fill other columns such as clk or even sel_cd_cpy
// but as long sel_mem_active == 0, it does not lead to any memory operations. The latter
// is guarded by sel_mem_active in #[PERM_SLICE_MEM] below.

#[LOOKUP_CD_VALUE]
sel_cd_cpy {col_offset, val} in main.sel_calldata {main.clk, main.calldata};

#[PERM_SLICE_MEM]
sel_mem_active {clk, space_id, addr, val, sel_cd_cpy}
is
mem.sel_op_slice {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};

// Caution: sel_op_slice disables the tag check during a read. This is required for the RETURN opcode
// but could have bad consequences if one adds additional "read" operations as part of this gadget.
// In such a case, we have to disable tag check specifically for RETURN opcode.

#[LOOKUP_RET_VALUE]
sel_return {col_offset, val} in main.sel_returndata {main.clk, main.returndata};
30 changes: 27 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,9 @@ 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.
pol public returndata;
pol commit sel_returndata; // Selector used for lookup in returndata. TODO: Might be removed or made constant.

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

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

//===== 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 +329,9 @@ 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;
sel_op_external_return * (1 - sel_op_external_return) = 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 +484,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 + sel_op_external_return;
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 +668,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_slice_gadget; // Selector to activate a slice gadget operation in the gadget (#[PERM_MAIN_SLICE]).

// Activate only if tag_err is disabled
sel_slice_gadget = (sel_op_calldata_copy + sel_op_external_return) * (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 +742,11 @@ namespace main(256);
is
pedersen.sel_pedersen {pedersen.clk, pedersen.input};

#[PERM_MAIN_SLICE]
sel_slice_gadget {clk, space_id, ia, ib, mem_addr_c, sel_op_calldata_copy, sel_op_external_return}
is
slice.sel_start {slice.clk, slice.space_id, slice.col_offset, slice.cnt, slice.addr, slice.sel_cd_cpy, slice.sel_return};

#[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
24 changes: 20 additions & 4 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/return memory operations triggered from memory slice gadget.
pol commit sel_op_slice;

// 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_slice * (1 - sel_op_slice) = 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_slice;
// 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,12 @@ 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. Similarly return memory slice operations
// will have a sub_clk value of 4.

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

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

// Skip check tag
// TODO: Verfiy that skip_check_tag cannot be enabled maliciously by the prover.
// Skip check tag enabled for some MOV/CMOV opcodes and RETURN opcode (sel_op_slice)
#[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));
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)) + sel_op_slice;

// Memory tag consistency check for load operations, i.e., rw == 0.
// We want to prove that r_in_tag == tag <==> tag_err == 0
Expand Down Expand Up @@ -207,6 +219,10 @@ namespace mem(256);
sel_resolve_ind_addr_c * rw = 0;
sel_resolve_ind_addr_d * rw = 0;

//====== CALLDATACOPY/RETURN specific constraints ==================================
sel_op_slice * (w_in_tag - 6) = 0; // Only write elements of type FF
sel_op_slice * (r_in_tag - 6) = 0; // Only read 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
Loading
Loading