Merge pull request #573 from AztecProtocol/ir/fix-unsourced-forged-writes

fix(avm)!: comments and leftover columns

Author: jeanmon

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

@@ -31,7 +31,7 @@ include "../precomputed.pil";
  * The operands' encoding is determined per opcode by the WIRE_INSTRUCTION_SPEC in precomputed.pil.
  * This specification provides: exec_opcode, instr_size, operand decomposition selectors (sel_op_dc_0..16)
  * and tag metadata (sel_has_tag, sel_tag_is_op2). We use the decomposition selectors to transform the
- * fetched bytecode bytes (bd0..36) into the operands (addressing_mode, op1..7)).
+ * fetched bytecode bytes (bd0..36) into the operands (addressing_mode, op1..5).
  *
  * The remaining work of this trace uses other specification data to handle errors (see ERROR HANDLING).
  *
@@ -57,13 +57,13 @@ include "../precomputed.pil";
  *      sel_instruction_fetching_success {
  *          pc, bytecode_id, exec_opcode,
  *          instr_size, addressing_mode,
- *          op[0], op[1], op[2], op[3], op[4],
-            op[5], op[6]
+ *          op[0], op[1], op[2],
+ *          op[3], op[4]
  *      } in instr_fetching.sel {
  *          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.op1, instr_fetching.op2, instr_fetching.op3,
+ *          instr_fetching.op4, instr_fetching.op5
  *      };
  *
  * ERROR HANDLING:

barretenberg/cpp/pil/vm2/execution/addressing.pil

@@ -10,18 +10,18 @@ include "../gt.pil";
 // (permutation/lookup).
 
 // This gadget constrains the resolution of the operands from instruction fetching.
-// The input operands are op[0], ..., op[6] (from execution.pil).
-// The output operands are rop[0], ..., rop[6] (from execution.pil).
+// The input operands are op[0], ..., op[4] (from execution.pil).
+// The output operands are rop[0], ..., rop[4] (from execution.pil).
 // We guarantee that the resolved operands are either immediates or valid addresses.
 
 // Inputs (from execution.pil):
 //  - SEL_RESOLVE_ADDRESS (alias for sel_instruction_fetching_success)
-//  - sel_op_is_address[7] (via exec spec; derived from ExecInstructionSpec.num_addresses)
+//  - sel_op_is_address[5] (via exec spec; derived from ExecInstructionSpec.num_addresses)
 //  - addressing_mode (via instruction fetching)
-//  - op[7] (via instruction fetching)
+//  - op[5] (via instruction fetching)
 // Outputs (to execution.pil):
 //  - sel_addressing_error
-//  - rop[7]
+//  - rop[5]
 
 // Errors:
 // - sel_base_address_failure: the base address is invalid
@@ -253,7 +253,7 @@ sel_op_do_overflow_check[4] { op_after_relative[4], highest_address, sel_relativ
 
 // Whether a given operand should be indirection-resolved.
 // We only do this if the indirect bit is set AND nothing else failed so far (for this operand).
-// Recall that from #[NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_i] (i = 0, ..., 6), we have:
+// Recall that from #[NOT_RELATIVE_OR_BASE_FAILURE_NO_OVERFLOW_i] (i = 0, ..., 4), we have:
 // `sel_base_address_failure == 1` ==> `sel_relative_overflow[i] == 0` and therefore they are mutually exclusive.
 pol commit sel_apply_indirection[5]; // @boolean (from definition and above remark)
 #[INDIRECT_GATING_0]

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

@@ -10,7 +10,7 @@ namespace execution;
 // pol commit rw_reg[6]; // Read / Write (only if sel_mem_op_reg[i] = 1)
 // pol commit sel_tag_check_reg[6]; // Tag check (only for read)
 // pol commit expected_tag_reg[6]; // Expected tag (only if sel_tag_check_reg[i] = 1)
-// pol commit rop[6]; // Resolved operands (for read/write), always addresses here.
+// pol commit rop[5]; // Resolved operands (for read/write), always addresses here.
 //
 // Inputs for write, Outputs for read:
 // pol commit register[6];

barretenberg/cpp/pil/vm2/memory.pil

@@ -110,24 +110,21 @@ sel = 0;
 
 // Permutation selectors (execution/addressing.pil).
 pol commit sel_addressing_base; // @boolean
-pol commit sel_addressing_indirect[7]; // @boolean
+pol commit sel_addressing_indirect[5]; // @boolean
 sel_addressing_base * (1 - sel_addressing_base) = 0;
 sel_addressing_indirect[0] * (1 - sel_addressing_indirect[0]) = 0;
 sel_addressing_indirect[1] * (1 - sel_addressing_indirect[1]) = 0;
 sel_addressing_indirect[2] * (1 - sel_addressing_indirect[2]) = 0;
 sel_addressing_indirect[3] * (1 - sel_addressing_indirect[3]) = 0;
 sel_addressing_indirect[4] * (1 - sel_addressing_indirect[4]) = 0;
-sel_addressing_indirect[5] * (1 - sel_addressing_indirect[5]) = 0;
-sel_addressing_indirect[6] * (1 - sel_addressing_indirect[6]) = 0;
 
 // Permutation selectors (execution/registers.pil)
-pol commit sel_register_op[6]; // @boolean
+pol commit sel_register_op[5]; // @boolean
 sel_register_op[0] * (1 - sel_register_op[0]) = 0;
 sel_register_op[1] * (1 - sel_register_op[1]) = 0;
 sel_register_op[2] * (1 - sel_register_op[2]) = 0;
 sel_register_op[3] * (1 - sel_register_op[3]) = 0;
 sel_register_op[4] * (1 - sel_register_op[4]) = 0;
-sel_register_op[5] * (1 - sel_register_op[5]) = 0;
 
 // Permutation selectors (data_copy.pil).
 pol commit sel_data_copy_read; // @boolean
@@ -189,10 +186,9 @@ sel_to_radix_write * (1 - sel_to_radix_write) = 0;
 sel = // Addressing.
       sel_addressing_base
     + sel_addressing_indirect[0] + sel_addressing_indirect[1] + sel_addressing_indirect[2] + sel_addressing_indirect[3]
-    + sel_addressing_indirect[4] + sel_addressing_indirect[5] + sel_addressing_indirect[6]
+    + sel_addressing_indirect[4]
     // Registers.
     + sel_register_op[0] + sel_register_op[1] + sel_register_op[2] + sel_register_op[3] + sel_register_op[4]
-    + sel_register_op[5]
     // Data Copy.
     + sel_data_copy_read
     + sel_data_copy_write

barretenberg/cpp/pil/vm2/precomputed.pil

@@ -297,17 +297,17 @@ pol constant p_decomposition_limb;
 // ===== Section 9: Execution instruction spec (EXECUTION_INSTRUCTION_SPEC) =====
 // Each valid row encodes: gas costs (L2 opcode, base DA, dynamic L2, dynamic DA),
 // per-register flags (memory access, read/write, tag check, expected tag) for 6 registers,
-// subtrace/gadget dispatch IDs, dynamic gas ID, and address-operand flags for 7 operands.
+// subtrace/gadget dispatch IDs, dynamic gas ID, and address-operand flags for 5 operands.
 // Used by the execution subtrace to dispatch and constrain instruction behavior.
 //
 // Example trace (idx encodes the ExecutionOpCode; array columns use [a,b,...] notation):
 //
-//   idx              | sel_exec_spec | opcode_gas | base_da | dyn_l2 | dyn_da | mem_op[0..5]       | rw[0..5]           | subtrace_id | sub_op_id | dyn_gas_id | is_addr[0..6]
+//   idx              | sel_exec_spec | opcode_gas | base_da | dyn_l2 | dyn_da | mem_op[0..5]       | rw[0..5]           | subtrace_id | sub_op_id | dyn_gas_id | is_addr[0..4]
 //   -----------------+---------------+------------+---------+--------+--------+--------------------+--------------------+-------------+-----------+------------+----------------------
-//   0 (ADD)          |             1 |         12 |       0 |      0 |      0 | [1,1,1,0,0,0]      | [0,0,1,0,0,0]      |           1 |         1 |          0 | [1,1,1,0,0,0,0]
-//   1 (SUB)          |             1 |         12 |       0 |      0 |      0 | [1,1,1,0,0,0]      | [0,0,1,0,0,0]      |           1 |         2 |          0 | [1,1,1,0,0,0,0]
+//   0 (ADD)          |             1 |         12 |       0 |      0 |      0 | [1,1,1,0,0,0]      | [0,0,1,0,0,0]      |           1 |         1 |          0 | [1,1,1,0,0]
+//   1 (SUB)          |             1 |         12 |       0 |      0 |      0 | [1,1,1,0,0,0]      | [0,0,1,0,0,0]      |           1 |         2 |          0 | [1,1,1,0,0]
 //   ...              |           ... |        ... |     ... |    ... |    ... | ...                | ...                |         ... |       ... |        ... | ...
-//   45 (TORADIXBE)   |             1 |         24 |       0 |      3 |      0 | [1,1,1,1,0,0]      | [0,0,0,0,0,0]      |          13 |         0 |          4 | [1,1,1,1,1,0,0]
+//   45 (TORADIXBE)   |             1 |         24 |       0 |      3 |      0 | [1,1,1,1,0,0]      | [0,0,0,0,0,0]      |          13 |         0 |          4 | [1,1,1,1,1]
 
 pol constant sel_exec_spec;
 // Gas Costs
@@ -348,9 +348,9 @@ pol constant sel_op_is_address[5];
 //       1 |                  1 |              3  (operand 0 indirect)
 //       3 |                  1 |              9  (operand 0 indirect + relative)
 //     ... |                  1 |            ...
-//    4095 |                  1 |             39  (operands 0-5 indirect + relative)
+//    1023 |                  1 |             33  (operands 0-4 indirect + relative; this is the max gas value for addressing)
 //     ... |                  1 |            ...
-//   65535 |                  1 |             45  (all 7 operands indirect + relative)
+//   65535 |                  1 |             33  (all bits above operand 4 are ignored, see addressing.pil for why this table still needs to be 16-bits)
 
 pol constant sel_addressing_gas;
 pol constant addressing_gas;

barretenberg/cpp/src/barretenberg/aztec/aztec_constants.hpp

@@ -179,7 +179,7 @@
 #define AVM_PUBLIC_INPUTS_COLUMN_2_LENGTH 522
 #define AVM_PUBLIC_INPUTS_COLUMN_3_LENGTH 99
 #define AVM_PUBLIC_INPUTS_COLUMNS_COMBINED_LENGTH 9989
-#define AVM_V2_PROOF_LENGTH_IN_FIELDS 15383
+#define AVM_V2_PROOF_LENGTH_IN_FIELDS 15368
 #define TX_DA_GAS_OVERHEAD 96
 #define PUBLIC_TX_L2_GAS_OVERHEAD 540000
 #define AVM_MAX_PROCESSABLE_L2_GAS 6000000

barretenberg/cpp/src/barretenberg/vm2/constraining/recursion/two_layer_avm_recursive_verifier.hpp

@@ -23,7 +23,7 @@
 
 namespace bb::avm2 {
 
-static constexpr size_t NUM_AVM_ULTRA_OPS = 3085;
+static constexpr size_t NUM_AVM_ULTRA_OPS = 3082;
 static_assert(2 * NUM_AVM_ULTRA_OPS < (1 << CONST_TRANSLATOR_MINI_CIRCUIT_LOG_SIZE) - NUM_DISABLED_ROWS_IN_SUMCHECK,
               "AVM ultra ops land in the range reserved for randomness in the Translator mini circuit. If this "
               "assertion fails, we need to increase CONST_TRANSLATOR_MINI_CIRCUIT_LOG_SIZE.");

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/addressing.test.cpp

@@ -325,7 +325,6 @@ TEST(AddressingConstrainingTest, RelativeOverflowCheck)
             { C::execution_sel_op_is_relative_wire_0_, 1 },
             { C::execution_sel_op_is_relative_wire_2_, 1 },
             { C::execution_sel_op_is_relative_wire_4_, 1 },
-            { C::execution_sel_op_is_relative_wire_6_, 1 },
             { C::execution_sel_op_is_address_0_, 1 },
             { C::execution_sel_op_is_address_2_, 1 },
             { C::execution_sel_op_is_address_4_, 1 },
@@ -350,7 +349,7 @@ TEST(AddressingConstrainingTest, RelativeOverflowCheck)
     });
 
     // GT trace.
-    for (uint32_t i = 0; i < 7; i++) {
+    for (uint32_t i = 0; i < AVM_MAX_OPERANDS; i++) {
         trace.set(C::gt_sel, i, 1);
         trace.set(C::gt_input_a, i, resolved_addrs[i]);
         trace.set(C::gt_input_b, i, AVM_HIGHEST_MEM_ADDRESS);

barretenberg/cpp/src/barretenberg/vm2/generated/columns.hpp

@@ -141,10 +141,10 @@ namespace bb::avm2 {
 
 struct AvmFlavorVariables {
     static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 117;
-    static constexpr size_t NUM_WITNESS_ENTITIES = 2925;
+    static constexpr size_t NUM_WITNESS_ENTITIES = 2922;
     static constexpr size_t NUM_SHIFTED_ENTITIES = 364;
-    static constexpr size_t NUM_WIRES = 2488;
-    static constexpr size_t NUM_ALL_ENTITIES = 3406;
+    static constexpr size_t NUM_WIRES = 2485;
+    static constexpr size_t NUM_ALL_ENTITIES = 3403;
 
     // Need to be templated for recursive verifier
     template <typename FF_>