Merge pull request #493 from AztecProtocol/mw/avm-max-operands

feat(avm)!: Reduce maximum number of AVM operands

Author: jeanmon

barretenberg/.gitignore

@@ -18,4 +18,5 @@ ts/src/cbind/generated/
 **/generated/
 # ...but these are committed source dirs, not codegen output:
 !cpp/src/barretenberg/flavor/generated/
+!cpp/src/barretenberg/vm2/generated/
 !cpp/src/barretenberg/honk/execution_trace/generated/

barretenberg/cpp/pil/vm2/bytecode/instr_fetching.pil

@@ -10,7 +10,7 @@ include "../precomputed.pil";
  * For our purposes an instruction can be thought of as:
  *    - Opcode (exec_opcode, u8): The operation to perform encoded numerically as defined in our
  *        instruction specification e.g. the SUB operation is mapped to 1.
- *    - Operands ([op1, ..., op7], MemoryValue[]): The inputs and/or outputs of the operation. The
+ *    - Operands ([op1, ..., op5], MemoryValue[]): The inputs and/or outputs of the operation. The
  *        number of operands and their types differs per opcode e.g. FDIV has three; two FF inputs
  *        and one FF output.
  *    - Addressing Mode (addressing_mode, u16): The indirect and relative contributions of the operands
@@ -21,7 +21,7 @@ include "../precomputed.pil";
  * The main work of this trace is to derive the decoded operands of an instruction from raw bytecode
  * bytes and our opcode specification:
  *    - addressing_mode: #[ADDRESSING_MODE_BYTES_DECOMPOSITION]
- *    - [op1, op2, op3, op4, op5, op6, op7]: #[OPXXX_BYTES_DECOMPOSITION]
+ *    - [op1, op2, op3, op4, op5]: #[OPXXX_BYTES_DECOMPOSITION]
  *
  * It copies the relevant bytecode portion from bc_decomposition.pil (#[BYTES_FROM_BC_DEC]):
  *   bd0 = bytecode[pc], bd1 = bytecode[pc+1], ..., bd36 = bytecode[pc+36],
@@ -63,7 +63,7 @@ include "../precomputed.pil";
  *          instr_fetching.pc, instr_fetching.bytecode_id, instr_fetching.exec_opcode,
  *          instr_fetching.instr_size, instr_fetching.addressing_mode,
  *          instr_fetching.op1, instr_fetching.op2, instr_fetching.op3, instr_fetching.op4,
- *          instr_fetching.op5, instr_fetching.op6, instr_fetching.op7
+ *          instr_fetching.op5
  *      };
  *
  * ERROR HANDLING:
@@ -312,7 +312,6 @@ pol commit sel_op_dc_12; // @boolean (by lookup only when sel_pc_in_range == 1)
 pol commit sel_op_dc_13; // @boolean (by lookup only when sel_pc_in_range == 1)
 pol commit sel_op_dc_14; // @boolean (by lookup only when sel_pc_in_range == 1)
 pol commit sel_op_dc_15; // @boolean (by lookup only when sel_pc_in_range == 1)
-pol commit sel_op_dc_16; // @boolean (by lookup only when sel_pc_in_range == 1)
 
 #[WIRE_INSTRUCTION_INFO]
 sel_pc_in_range {
@@ -325,8 +324,7 @@ sel_pc_in_range {
      sel_op_dc_0,  sel_op_dc_1,  sel_op_dc_2,  sel_op_dc_3,
      sel_op_dc_4,  sel_op_dc_5,  sel_op_dc_6,  sel_op_dc_7,
      sel_op_dc_8,  sel_op_dc_9,  sel_op_dc_10, sel_op_dc_11,
-     sel_op_dc_12, sel_op_dc_13, sel_op_dc_14, sel_op_dc_15,
-     sel_op_dc_16
+     sel_op_dc_12, sel_op_dc_13, sel_op_dc_14, sel_op_dc_15
 } in
 precomputed.sel_range_8 {
     precomputed.idx,
@@ -338,8 +336,7 @@ precomputed.sel_range_8 {
     precomputed.sel_op_dc_0,  precomputed.sel_op_dc_1,  precomputed.sel_op_dc_2,  precomputed.sel_op_dc_3,
     precomputed.sel_op_dc_4,  precomputed.sel_op_dc_5,  precomputed.sel_op_dc_6,  precomputed.sel_op_dc_7,
     precomputed.sel_op_dc_8,  precomputed.sel_op_dc_9,  precomputed.sel_op_dc_10, precomputed.sel_op_dc_11,
-    precomputed.sel_op_dc_12, precomputed.sel_op_dc_13, precomputed.sel_op_dc_14, precomputed.sel_op_dc_15,
-    precomputed.sel_op_dc_16
+    precomputed.sel_op_dc_12, precomputed.sel_op_dc_13, precomputed.sel_op_dc_14, precomputed.sel_op_dc_15
 };
 
 
@@ -350,29 +347,25 @@ precomputed.sel_range_8 {
 pol commit addressing_mode;
 
 // Operands.
-pol commit op1, op2, op3, op4, op5, op6, op7;
+pol commit op1, op2, op3, op4, op5;
 
 // We derive the operands only when no parsing error (except possibly tag out-of-range) occurs. One might remove
 // this gating but at a cost of some ugliness in the code (witgen would need a partially parsed instruction when
 // the error instr_out_of_range is toggled).
 // The following relations decomposing operands (addressing_mode, op1, ...) into bytes were code-generated by
 // a cpp test in op_decomposition.test.cpp.
 // Remark: Upper-casing the alias needs to be edited manually (not code-generated)!
-pol SEL_OP_DC_17 = sel_op_dc_2 + sel_op_dc_6;
+pol SEL_OP_DC_16 = sel_op_dc_1 + sel_op_dc_5;
 
 #[ADDRESSING_MODE_BYTES_DECOMPOSITION]
-addressing_mode = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd1 * 2**8 + bd2 * 2**0) + SEL_OP_DC_17 * (bd1 * 2**0));
+addressing_mode = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd1 * 2**8 + bd2 * 2**0) + SEL_OP_DC_16 * (bd1 * 2**0));
 #[OP1_BYTES_DECOMPOSITION]
-op1 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd3 * 2**8 + bd4 * 2**0) + sel_op_dc_2 * (bd2 * 2**8 + bd3 * 2**0) + sel_op_dc_6 * (bd2 * 2**0) + sel_op_dc_15 * (bd1 * 2**24 + bd2 * 2**16 + bd3 * 2**8 + bd4 * 2**0));
+op1 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd3 * 2**8 + bd4 * 2**0) + sel_op_dc_1 * (bd2 * 2**8 + bd3 * 2**0) + sel_op_dc_5 * (bd2 * 2**0) + sel_op_dc_14 * (bd1 * 2**24 + bd2 * 2**16 + bd3 * 2**8 + bd4 * 2**0));
 #[OP2_BYTES_DECOMPOSITION]
-op2 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_3 * (bd4 * 2**8 + bd5 * 2**0) + sel_op_dc_6 * (bd3 * 2**0) + sel_op_dc_8 * (bd4 * 2**0) + sel_op_dc_16 * (bd4 * 2**24 + bd5 * 2**16 + bd6 * 2**8 + bd7 * 2**0));
+op2 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_2 * (bd4 * 2**8 + bd5 * 2**0) + sel_op_dc_5 * (bd3 * 2**0) + sel_op_dc_7 * (bd4 * 2**0) + sel_op_dc_15 * (bd4 * 2**24 + bd5 * 2**16 + bd6 * 2**8 + bd7 * 2**0));
 #[OP3_BYTES_DECOMPOSITION]
-op3 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_4 * (bd6 * 2**8 + bd7 * 2**0) + sel_op_dc_7 * (bd6 * 2**0) + sel_op_dc_9 * (bd5 * 2**248 + bd6 * 2**240 + bd7 * 2**232 + bd8 * 2**224 + bd9 * 2**216 + bd10 * 2**208 + bd11 * 2**200 + bd12 * 2**192 + bd13 * 2**184 + bd14 * 2**176 + bd15 * 2**168 + bd16 * 2**160 + bd17 * 2**152 + bd18 * 2**144 + bd19 * 2**136 + bd20 * 2**128 + bd21 * 2**120 + bd22 * 2**112 + bd23 * 2**104 + bd24 * 2**96 + bd25 * 2**88 + bd26 * 2**80 + bd27 * 2**72 + bd28 * 2**64 + bd29 * 2**56 + bd30 * 2**48 + bd31 * 2**40 + bd32 * 2**32 + bd33 * 2**24 + bd34 * 2**16 + bd35 * 2**8 + bd36 * 2**0) + sel_op_dc_10 * (bd5 * 2**120 + bd6 * 2**112 + bd7 * 2**104 + bd8 * 2**96 + bd9 * 2**88 + bd10 * 2**80 + bd11 * 2**72 + bd12 * 2**64 + bd13 * 2**56 + bd14 * 2**48 + bd15 * 2**40 + bd16 * 2**32 + bd17 * 2**24 + bd18 * 2**16 + bd19 * 2**8 + bd20 * 2**0) + sel_op_dc_11 * (bd5 * 2**56 + bd6 * 2**48 + bd7 * 2**40 + bd8 * 2**32 + bd9 * 2**24 + bd10 * 2**16 + bd11 * 2**8 + bd12 * 2**0) + sel_op_dc_12 * (bd5 * 2**24 + bd6 * 2**16 + bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_13 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_14 * (bd4 * 2**0));
+op3 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_3 * (bd6 * 2**8 + bd7 * 2**0) + sel_op_dc_6 * (bd6 * 2**0) + sel_op_dc_8 * (bd5 * 2**248 + bd6 * 2**240 + bd7 * 2**232 + bd8 * 2**224 + bd9 * 2**216 + bd10 * 2**208 + bd11 * 2**200 + bd12 * 2**192 + bd13 * 2**184 + bd14 * 2**176 + bd15 * 2**168 + bd16 * 2**160 + bd17 * 2**152 + bd18 * 2**144 + bd19 * 2**136 + bd20 * 2**128 + bd21 * 2**120 + bd22 * 2**112 + bd23 * 2**104 + bd24 * 2**96 + bd25 * 2**88 + bd26 * 2**80 + bd27 * 2**72 + bd28 * 2**64 + bd29 * 2**56 + bd30 * 2**48 + bd31 * 2**40 + bd32 * 2**32 + bd33 * 2**24 + bd34 * 2**16 + bd35 * 2**8 + bd36 * 2**0) + sel_op_dc_9 * (bd5 * 2**120 + bd6 * 2**112 + bd7 * 2**104 + bd8 * 2**96 + bd9 * 2**88 + bd10 * 2**80 + bd11 * 2**72 + bd12 * 2**64 + bd13 * 2**56 + bd14 * 2**48 + bd15 * 2**40 + bd16 * 2**32 + bd17 * 2**24 + bd18 * 2**16 + bd19 * 2**8 + bd20 * 2**0) + sel_op_dc_10 * (bd5 * 2**56 + bd6 * 2**48 + bd7 * 2**40 + bd8 * 2**32 + bd9 * 2**24 + bd10 * 2**16 + bd11 * 2**8 + bd12 * 2**0) + sel_op_dc_11 * (bd5 * 2**24 + bd6 * 2**16 + bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_12 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_13 * (bd4 * 2**0));
 #[OP4_BYTES_DECOMPOSITION]
-op4 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd9 * 2**8 + bd10 * 2**0) + sel_op_dc_5 * (bd8 * 2**8 + bd9 * 2**0));
+op4 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd9 * 2**8 + bd10 * 2**0) + sel_op_dc_4 * (bd8 * 2**8 + bd9 * 2**0));
 #[OP5_BYTES_DECOMPOSITION]
-op5 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd11 * 2**8 + bd12 * 2**0) + sel_op_dc_5 * (bd10 * 2**8 + bd11 * 2**0));
-#[OP6_BYTES_DECOMPOSITION]
-op6 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_1 * (bd13 * 2**8 + bd14 * 2**0));
-#[OP7_BYTES_DECOMPOSITION]
-op7 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_1 * (bd15 * 2**8 + bd16 * 2**0));
+op5 = (1 - PARSING_ERROR_EXCEPT_TAG_ERROR) * (sel_op_dc_0 * (bd11 * 2**8 + bd12 * 2**0) + sel_op_dc_4 * (bd10 * 2**8 + bd11 * 2**0));

barretenberg/cpp/pil/vm2/execution.pil

@@ -378,7 +378,7 @@ pol commit sel_instruction_fetching_failure; // @boolean (by definition below)
 
 pol commit exec_opcode;
 pol commit addressing_mode;
-pol commit op[7];  // operands
+pol commit op[5];  // operands
 
 // We now proceed to fetch the instruction.
 
@@ -419,9 +419,7 @@ sel_instruction_fetching_success {
     op[1],
     op[2],
     op[3],
-    op[4],
-    op[5],
-    op[6]
+    op[4]
 } in instr_fetching.sel {
     instr_fetching.pc,
     instr_fetching.bytecode_id,
@@ -432,9 +430,7 @@ sel_instruction_fetching_success {
     instr_fetching.op2,
     instr_fetching.op3,
     instr_fetching.op4,
-    instr_fetching.op5,
-    instr_fetching.op6,
-    instr_fetching.op7
+    instr_fetching.op5
 };
 
 /**************************************************************************************************
@@ -457,8 +453,6 @@ sel_instruction_fetching_success {
     sel_op_is_address[2],
     sel_op_is_address[3],
     sel_op_is_address[4],
-    sel_op_is_address[5],
-    sel_op_is_address[6],
     // decomposed selectors
     subtrace_id,
     subtrace_operation_id,
@@ -468,7 +462,7 @@ sel_instruction_fetching_success {
     sel_mem_op_reg[1],
     sel_mem_op_reg[2],
     sel_mem_op_reg[3],
-    sel_mem_op_reg[4],
+    sel_mem_op_reg[4], // TODO(MW): Remove when reducing max registers
     sel_mem_op_reg[5],
     // read / write per register
     rw_reg[0],
@@ -506,8 +500,6 @@ precomputed.sel_exec_spec {
     precomputed.sel_op_is_address[2],
     precomputed.sel_op_is_address[3],
     precomputed.sel_op_is_address[4],
-    precomputed.sel_op_is_address[5],
-    precomputed.sel_op_is_address[6],
     // decomposed selectors
     precomputed.subtrace_id,
     precomputed.subtrace_operation_id,
@@ -549,7 +541,7 @@ precomputed.sel_exec_spec {
 pol SEL_RESOLVE_ADDRESS = sel_instruction_fetching_success;
 
 // resolved operands
-pol commit rop[7];
+pol commit rop[5];
 
 // NOTE: Constraints on the resolved operands are in addressing.pil.
 // The "output we want" is sel_addressing_error from addressing.pil.
@@ -565,6 +557,10 @@ sel_read_registers = SEL_RESOLVE_ADDRESS - sel_addressing_error;
 
 // Registers
 pol commit register[6];
+
+// TODO(MW): Remove when reducing max registers (below prevents IsolatedCommittedColumn)
+sel_read_registers * register[5] = 0;
+
 // Memory Accesses
 pol commit sel_mem_op_reg[6]; // @boolean (when `sel_instruction_fetching_success == 1`)
 // Read / Write selectors