feat: merge-train/avm (#17702)

BEGIN_COMMIT_OVERRIDE
feat!: apply batch inverses and precomputed inverses for AVM tracegen
(#17669)
feat(avm)!: Reduce the number of registers from 7 to 6 (#17688)
chore(avm): opcode maps should follow ordering of their enum (#17682)
END_COMMIT_OVERRIDE

Author: jeanmon

barretenberg/cpp/pil/vm2/alu.pil

@@ -335,14 +335,13 @@ DIV_OPS_NON_U128 * (ib * ic - (ia - sel_op_div * helper1)) = 0;
 
 sel_op_eq * (1 - sel_op_eq) = 0;
 pol DIFF = ia - ib;
-
-// Use helper1 to invert DIFF.
+pol commit ab_diff_inv; // Helper column for inverting DIFF.
 // ic is a boolean output and ic == 1 <==> a == b.
 // Important: ic boolean constraint is enforced as part of write to memory due to ic_tag == U1 as enforced by #[C_TAG_CHECK].
 
 // sel_op_eq == 1 => [ic == 1 <==> DIFF == 0]
 #[EQ_OP_MAIN]
-sel_op_eq * (1 - sel_tag_err) * (DIFF * (ic * (1 - helper1) + helper1) - 1 + ic) = 0;
+sel_op_eq * (1 - sel_tag_err) * (DIFF * (ic * (1 - ab_diff_inv) + ab_diff_inv) - 1 + ic) = 0;
 
 // LT
 

barretenberg/cpp/pil/vm2/execution.pil

@@ -201,10 +201,10 @@ sel_instruction_fetching_success {
     // subtraces, mem ops, etc (defined later in this file)
     subtrace_id, subtrace_operation_id, dyn_gas_id,
     // register information
-    sel_mem_op_reg[0], sel_mem_op_reg[1], sel_mem_op_reg[2], sel_mem_op_reg[3], sel_mem_op_reg[4], sel_mem_op_reg[5], sel_mem_op_reg[6],
-    rw_reg[0], rw_reg[1], rw_reg[2], rw_reg[3], rw_reg[4], rw_reg[5], rw_reg[6],
-    sel_tag_check_reg[0], sel_tag_check_reg[1], sel_tag_check_reg[2], sel_tag_check_reg[3], sel_tag_check_reg[4], sel_tag_check_reg[5], sel_tag_check_reg[6],
-    expected_tag_reg[0], expected_tag_reg[1], expected_tag_reg[2], expected_tag_reg[3], expected_tag_reg[4], expected_tag_reg[5], expected_tag_reg[6]
+    sel_mem_op_reg[0], sel_mem_op_reg[1], sel_mem_op_reg[2], sel_mem_op_reg[3], sel_mem_op_reg[4], sel_mem_op_reg[5],
+    rw_reg[0], rw_reg[1], rw_reg[2], rw_reg[3], rw_reg[4], rw_reg[5],
+    sel_tag_check_reg[0], sel_tag_check_reg[1], sel_tag_check_reg[2], sel_tag_check_reg[3], sel_tag_check_reg[4], sel_tag_check_reg[5],
+    expected_tag_reg[0], expected_tag_reg[1], expected_tag_reg[2], expected_tag_reg[3], expected_tag_reg[4], expected_tag_reg[5]
 } in
 precomputed.sel_exec_spec {
     // execution opcode
@@ -233,31 +233,27 @@ precomputed.sel_exec_spec {
     precomputed.sel_mem_op_reg[3],
     precomputed.sel_mem_op_reg[4],
     precomputed.sel_mem_op_reg[5],
-    precomputed.sel_mem_op_reg[6],
     // read / write per register
     precomputed.rw_reg[0],
     precomputed.rw_reg[1],
     precomputed.rw_reg[2],
     precomputed.rw_reg[3],
     precomputed.rw_reg[4],
     precomputed.rw_reg[5],
-    precomputed.rw_reg[6],
     // whether we should perform a tag check on the register
     precomputed.sel_tag_check_reg[0],
     precomputed.sel_tag_check_reg[1],
     precomputed.sel_tag_check_reg[2],
     precomputed.sel_tag_check_reg[3],
     precomputed.sel_tag_check_reg[4],
     precomputed.sel_tag_check_reg[5],
-    precomputed.sel_tag_check_reg[6],
     // expected register tag to perform the check against
     precomputed.expected_tag_reg[0],
     precomputed.expected_tag_reg[1],
     precomputed.expected_tag_reg[2],
     precomputed.expected_tag_reg[3],
     precomputed.expected_tag_reg[4],
-    precomputed.expected_tag_reg[5],
-    precomputed.expected_tag_reg[6]
+    precomputed.expected_tag_reg[5]
 };
 
 //////// ADDRESSING ////////
@@ -280,17 +276,17 @@ pol commit sel_should_read_registers;
 sel_should_read_registers = SEL_SHOULD_RESOLVE_ADDRESS * (1 - sel_addressing_error);
 
 // Registers
-pol commit register[7];
+pol commit register[6];
 // Memory Acccesses
-pol commit sel_mem_op_reg[7];
+pol commit sel_mem_op_reg[6];
 // Read / Write selectors
-pol commit rw_reg[7];
+pol commit rw_reg[6];
 // Memory Tag
-pol commit mem_tag_reg[7];
+pol commit mem_tag_reg[6];
 // Whether we should perform a tag check on the register
-pol commit sel_tag_check_reg[7];
+pol commit sel_tag_check_reg[6];
 // Expected tag
-pol commit expected_tag_reg[7];
+pol commit expected_tag_reg[6];
 
 // NOTE: Constraints on the registers are in execution_registers.pil.
 // The "output we want is" sel_register_read_error from execution_registers.pil.

barretenberg/cpp/pil/vm2/execution/registers.pil

@@ -4,12 +4,12 @@ include "../memory.pil";
 namespace execution;
 
 // Input columns from execution.pil:
-// pol commit register[7];
-// pol commit sel_mem_op_reg[7];
-// pol commit rw_reg[7];
-// pol commit mem_tag_reg[7];
-// pol commit sel_tag_check_reg[7];
-// pol commit expected_tag_reg[7];
+// pol commit register[6];
+// pol commit sel_mem_op_reg[6];
+// pol commit rw_reg[6];
+// pol commit mem_tag_reg[6];
+// pol commit sel_tag_check_reg[6];
+// pol commit expected_tag_reg[6];
 //
 // pol commit sel_should_read_registers;    // Register read temporality group.
 // pol commit sel_should_write_registers;   // Register write temporality group.
@@ -46,8 +46,6 @@ sel_op_reg_effective[3] = sel_mem_op_reg[3] * (sel_should_read_registers * (1 -
 sel_op_reg_effective[4] = sel_mem_op_reg[4] * (sel_should_read_registers * (1 - rw_reg[4]) + sel_should_write_registers * rw_reg[4]);
 #[SEL_OP_REG_EFFECTIVE_5]
 sel_op_reg_effective[5] = sel_mem_op_reg[5] * (sel_should_read_registers * (1 - rw_reg[5]) + sel_should_write_registers * rw_reg[5]);
-#[SEL_OP_REG_EFFECTIVE_6]
-sel_op_reg_effective[6] = sel_mem_op_reg[6] * (sel_should_read_registers * (1 - rw_reg[6]) + sel_should_write_registers * rw_reg[6]);
 
 // Observe that the following permutations span both temporality groups.
 // That's why we have to properly activate them with the above selectors, which take into account
@@ -70,9 +68,6 @@ is memory.sel_register_op[4] { memory.clk,      memory.space_id, memory.address,
 #[MEM_OP_5]
 sel_op_reg_effective[5]      { precomputed.clk, context_id,      rop[5],         register[5],  mem_tag_reg[5], rw_reg[5] }
 is memory.sel_register_op[5] { memory.clk,      memory.space_id, memory.address, memory.value, memory.tag,     memory.rw };
-#[MEM_OP_6]
-sel_op_reg_effective[6]      { precomputed.clk, context_id,      rop[6],         register[6],  mem_tag_reg[6], rw_reg[6] }
-is memory.sel_register_op[6] { memory.clk,      memory.space_id, memory.address, memory.value, memory.tag,     memory.rw };
 
 // This error is true iff some final check failed. That is if some tag is not the expected one.
 // Observe that we don't need to know exactly which one failed.
@@ -89,8 +84,7 @@ pol BATCHED_TAGS_DIFF_REG = sel_tag_check_reg[0] * 2**0  * (mem_tag_reg[0] - exp
                           + sel_tag_check_reg[2] * 2**6  * (mem_tag_reg[2] - expected_tag_reg[2])
                           + sel_tag_check_reg[3] * 2**9  * (mem_tag_reg[3] - expected_tag_reg[3])
                           + sel_tag_check_reg[4] * 2**12 * (mem_tag_reg[4] - expected_tag_reg[4])
-                          + sel_tag_check_reg[5] * 2**15 * (mem_tag_reg[5] - expected_tag_reg[5])
-                          + sel_tag_check_reg[6] * 2**18 * (mem_tag_reg[6] - expected_tag_reg[6]);
+                          + sel_tag_check_reg[5] * 2**15 * (mem_tag_reg[5] - expected_tag_reg[5]);
 pol commit batched_tags_diff_inv_reg;
 pol BATCHED_TAGS_DIFF_X_REG = sel_should_read_registers * BATCHED_TAGS_DIFF_REG;  // Forces 0 if we don't read the register.
 pol BATCHED_TAGS_DIFF_Y_REG = batched_tags_diff_inv_reg;

barretenberg/cpp/pil/vm2/keccak_memory.pil

@@ -130,9 +130,9 @@ pol commit ctr_end;
 ctr_end * (1 - ctr_end) = 0;
 
 // We define ctr_end == 1 <==> ctr == AVM_KECCAKF1600_STATE_SIZE (25)
-pol commit ctr_min_state_size_inv;
+pol commit state_size_min_ctr_inv;
 #[CTR_END]
-sel * ((ctr - constants.AVM_KECCAKF1600_STATE_SIZE) * (ctr_end * (1 - ctr_min_state_size_inv) + ctr_min_state_size_inv) + ctr_end - 1) = 0;
+sel * ((constants.AVM_KECCAKF1600_STATE_SIZE - ctr) * (ctr_end * (1 - state_size_min_ctr_inv) + state_size_min_ctr_inv) + ctr_end - 1) = 0;
 
 // Last ctr of a multi-rows processing of a slice
 pol commit last;

barretenberg/cpp/pil/vm2/precomputed.pil

@@ -118,11 +118,11 @@ pol constant exec_opcode_base_da_gas;
 pol constant exec_opcode_dynamic_l2_gas;
 pol constant exec_opcode_dynamic_da_gas;
 // Registers: Memory Access
-pol constant sel_mem_op_reg[7];
-pol constant rw_reg[7];
+pol constant sel_mem_op_reg[6];
+pol constant rw_reg[6];
 // Registers: Tag Check
-pol constant sel_tag_check_reg[7];
-pol constant expected_tag_reg[7];
+pol constant sel_tag_check_reg[6];
+pol constant expected_tag_reg[6];
 // Decomposed Subtrace/Gadget Selector
 pol constant dyn_gas_id;
 pol constant subtrace_id;

barretenberg/cpp/src/barretenberg/vm2/common/aztec_constants.hpp

@@ -175,7 +175,7 @@
 #define AVM_MAX_PROCESSABLE_L2_GAS 6000000
 #define AVM_PC_SIZE_IN_BITS 32
 #define AVM_MAX_OPERANDS 7
-#define AVM_MAX_REGISTERS 7
+#define AVM_MAX_REGISTERS 6
 #define AVM_ADDRESSING_BASE_RESOLUTION_L2_GAS 3
 #define AVM_ADDRESSING_INDIRECT_L2_GAS 3
 #define AVM_ADDRESSING_RELATIVE_L2_GAS 3