Skip to content

Commit

Permalink
feat(avm): calldatacopy and return gadget (#7415)
Browse files Browse the repository at this point in the history
Resolves #7381
Resolves #7211
  • Loading branch information
jeanmon authored Jul 10, 2024
1 parent 108fc5f commit ec39e4e
Show file tree
Hide file tree
Showing 43 changed files with 4,018 additions and 1,377 deletions.
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

1 comment on commit ec39e4e

@AztecBot
Copy link
Collaborator

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'C++ Benchmark'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.05.

Benchmark suite Current: ec39e4e Previous: b496080 Ratio
Goblin::merge(t) 206457037 ns/iter 194725246 ns/iter 1.06

This comment was automatically generated by workflow using github-action-benchmark.

CC: @ludamad @codygunton

Please sign in to comment.