Merge pull request #469 from AztecProtocol/jean/precomputed-granular

feat(avm): granular destination selectors for precomputed subtraces

Author: jeanmon

barretenberg/cpp/pil/vm2/bitwise.pil

@@ -60,9 +60,8 @@ namespace constants;
     pol AVM_DYN_GAS_ID_CALLDATACOPY = 1;
     pol AVM_DYN_GAS_ID_RETURNDATACOPY = 2;
     pol AVM_DYN_GAS_ID_TORADIX = 4;
-    pol AVM_DYN_GAS_ID_BITWISE = 8;
-    pol AVM_DYN_GAS_ID_EMITPUBLICLOG = 16;
-    pol AVM_DYN_GAS_ID_SSTORE = 32;
+    pol AVM_DYN_GAS_ID_EMITPUBLICLOG = 8;
+    pol AVM_DYN_GAS_ID_SSTORE = 16;
     pol AVM_EXEC_OP_ID_GETENVVAR = 1;
     pol AVM_EXEC_OP_ID_MOV = 2;
     pol AVM_EXEC_OP_ID_JUMP = 4;

barretenberg/cpp/pil/vm2/constants_gen.pil

@@ -131,7 +131,6 @@ include "opcodes/sstore.pil";
  *     - #[EXEC_SPEC_READ] -> precomputed: read execution spec (gas costs, register info, subtrace dispatch).
  *
  *   Gas (dynamic):
- *     - #[DYN_L2_FACTOR_BITWISE] -> precomputed: tag-based byte length for bitwise gas.
  *     - #[CHECK_RADIX_GT_256] -> gt: compare radix > 256.
  *     - #[GET_P_LIMBS] -> precomputed: lookup num_p_limbs for to_radix gas.
  *     - #[GET_MAX_LIMBS] -> gt: compare num_limbs > num_p_limbs.
@@ -586,38 +585,26 @@ pol commit dyn_gas_id; // from precomputed.pil (#[EXEC_SPEC_READ])
 pol commit sel_gas_calldata_copy; // @boolean
 pol commit sel_gas_returndata_copy; // @boolean
 pol commit sel_gas_to_radix; // @boolean
-pol commit sel_gas_bitwise; // @boolean
 pol commit sel_gas_emit_public_log; // @boolean
 pol commit sel_gas_sstore; // @boolean
 
 // Boolean constraints
 sel_gas_calldata_copy * (1 - sel_gas_calldata_copy) = 0;
 sel_gas_returndata_copy * (1 - sel_gas_returndata_copy) = 0;
 sel_gas_to_radix * (1 - sel_gas_to_radix) = 0;
-sel_gas_bitwise * (1 - sel_gas_bitwise) = 0;
 sel_gas_emit_public_log * (1 - sel_gas_emit_public_log) = 0;
 sel_gas_sstore * (1 - sel_gas_sstore) = 0;
 
 #[DYN_GAS_ID_DECOMPOSITION]
 sel_gas_calldata_copy * constants.AVM_DYN_GAS_ID_CALLDATACOPY +
 sel_gas_returndata_copy * constants.AVM_DYN_GAS_ID_RETURNDATACOPY +
 sel_gas_to_radix * constants.AVM_DYN_GAS_ID_TORADIX +
-sel_gas_bitwise * constants.AVM_DYN_GAS_ID_BITWISE +
 sel_gas_emit_public_log * constants.AVM_DYN_GAS_ID_EMITPUBLICLOG +
 sel_gas_sstore * constants.AVM_DYN_GAS_ID_SSTORE
    // We force the selectors to be 0 if we failed before gas checks
    // or when we are not in the execution subtrace.
 = sel_check_gas * dyn_gas_id;
 
-//////////////////////////////////////////
-// Bitwise, Dynamic L2 Gas Calculation
-//////////////////////////////////////////
-// For bitwise, the tag determines the dynamic_l2_gas_factor
-#[DYN_L2_FACTOR_BITWISE]
-sel_gas_bitwise { mem_tag_reg[0], dynamic_l2_gas_factor }
-in
-precomputed.sel_tag_parameters { precomputed.idx, precomputed.tag_byte_length };
-
 //////////////////////////////////////////
 // ToRadixBE, Dynamic L2 Gas Calculation
 //////////////////////////////////////////
@@ -734,9 +721,9 @@ sel_gas_emit_public_log * (/*log_size=*/ register[0] - dynamic_da_gas_factor) =
 #[DYN_DA_GAS_IS_ZERO]
 (1 - sel_gas_sstore - sel_gas_emit_public_log) * dynamic_da_gas_factor = 0;
 
-// Except BITWISE, TORADIX, EMITPUBLICLOG, CALLDATACOPY, RETURNDATACOPY, all opcodes have a zero dynamic l2 gas.
+// Except TORADIX, EMITPUBLICLOG, CALLDATACOPY, RETURNDATACOPY, all opcodes have a zero dynamic l2 gas.
 #[DYN_L2_GAS_IS_ZERO]
-(1 - sel_gas_bitwise - sel_gas_to_radix - sel_gas_emit_public_log - sel_gas_calldata_copy - sel_gas_returndata_copy) * dynamic_l2_gas_factor = 0;
+(1 - sel_gas_to_radix - sel_gas_emit_public_log - sel_gas_calldata_copy - sel_gas_returndata_copy) * dynamic_l2_gas_factor = 0;
 
 /**************************************************************************************************
  *  Temporality group 5: Opcode execution
@@ -1087,11 +1074,11 @@ sel_exec_dispatch_bitwise {
     register[0], mem_tag_reg[0],
     register[1], mem_tag_reg[1],
     register[2], mem_tag_reg[2]
-} in bitwise.start {
+} in bitwise.sel_bitwise_opcode {
     bitwise.op_id, bitwise.err,
-    bitwise.acc_ia, bitwise.tag_a,
-    bitwise.acc_ib, bitwise.tag_b,
-    bitwise.acc_ic, bitwise.tag_c
+    bitwise.ia, bitwise.tag_a,
+    bitwise.ib, bitwise.tag_b,
+    bitwise.ic, bitwise.tag_c
 };
 
 // CAST DISPATCHING

barretenberg/cpp/pil/vm2/execution.pil

@@ -283,11 +283,11 @@ diff = limb[0] + limb[1] * 2**16 + limb[2] * 2**32;
 // Range check each limb to 16 bits, proving diff is in [0, 2^48).
 // Only checked on active non-last rows (sel_rng_chk gating).
 #[RANGE_CHECK_LIMB_0]
-sel_rng_chk { limb[0] } in precomputed.sel_range_16 { precomputed.idx };
+sel_rng_chk { limb[0] } in precomputed.sel_range_16_active { precomputed.idx };
 #[RANGE_CHECK_LIMB_1]
-sel_rng_chk { limb[1] } in precomputed.sel_range_16 { precomputed.idx };
+sel_rng_chk { limb[1] } in precomputed.sel_range_16_active { precomputed.idx };
 #[RANGE_CHECK_LIMB_2]
-sel_rng_chk { limb[2] } in precomputed.sel_range_16 { precomputed.idx };
+sel_rng_chk { limb[2] } in precomputed.sel_range_16_active { precomputed.idx };
 
 ////////////////////////////////////////////////
 // Memory Initialization

barretenberg/cpp/pil/vm2/keccakf1600.pil

@@ -23,7 +23,7 @@
  *
  * Valid selectors determining the row ranges:
  *   - sel_range_8:                rows [0, 2^8)   — 8-bit range checks and power-of-2 lookups
- *   - sel_range_16:               rows [0, 2^16)  — 16-bit range checks
+ *   - sel_range_16:               rows [0, 2^16)  — 16-bit range checks (used also for bitwise and addressing gas lookups)
  *   - sel_sha256_compression:     SHA-256 round constants
  *   - sel_tag_parameters:         memory tag metadata (byte length, max bits, max value)
  *   - sel_to_radix_p_limb_counts: safe limb counts for radix decomposition
@@ -33,6 +33,13 @@
  *   - sel_phase:                  transaction execution phase properties
  *   - sel_keccak:                 keccak round constants
  *
+ * The above selectors are fixed (precomputed) and do not change per transaction/program. For optimization reasons,
+ * we introduce committed granular destination selectors for:
+ * - 16-bit range check: sel_range_16_active
+ * - bitwise: sel_bitwise
+ * - addressing gas: sel_addressing_gas
+ * Therefore, the lookup's log-derivative inverse is materialised over the used entries instead of the full 2^16-row table.
+ *
  * The columns are organized into several logical groups:
  *
  * 1. General-purpose columns: row index, zero column, first-row selector.
@@ -112,6 +119,11 @@ pol constant first_row;
 pol constant sel_range_8;  // 1 in the first 2^8 rows [0, 2^8)
 pol constant sel_range_16; // 1 in the first 2^16 rows [0, 2^16)
 
+// Granular destination selector for the 16-bit range-check lookups.
+pol commit sel_range_16_active; // @boolean
+sel_range_16_active * (1 - sel_range_16_active) = 0;
+// Relation #[GRANULAR_SELECTORS_ON_RANGE_16] ensures that `sel_range_16_active == 1 ==> sel_range_16 == 1`.
+
 // ===== Section 3: Bitwise lookup tables =====
 // Precomputed AND/OR/XOR results for all pairs of 8-bit inputs (256x256 = 65536 rows).
 // Row index = (input_a << 8) | input_b, so all 65536 pairs are covered.
@@ -137,6 +149,11 @@ pol constant bitwise_output_and; // output = a AND b.
 pol constant bitwise_output_or; // output = a OR b.
 pol constant bitwise_output_xor; // output = a XOR b.
 
+// Granular destination selector for the byte-operations lookup (#[BYTE_OPERATIONS]).
+pol commit sel_bitwise; // @boolean
+sel_bitwise * (1 - sel_bitwise) = 0;
+// Relation #[GRANULAR_SELECTORS_ON_RANGE_16] ensures that `sel_bitwise == 1 ==> sel_range_16 == 1`.
+
 // ===== Section 4: Power of 2 table =====
 // Lookup table for 2^idx, populated for idx in [0, 255]. Note the [0, 255] property is guaranteed by the
 // use of sel_range_8 as the dst selector (since idx actually goes from [0, 65536]).
@@ -342,7 +359,7 @@ pol constant sel_op_is_address[5];
 //   => 1 indirect + 2 relative => gas = 3 + 1*3 + 2*3 = 12
 //
 // Example trace:
-//   idx   | sel_addressing_gas | addressing_gas
+//   idx   |     sel_range_16   | addressing_gas
 //   ------+--------------------+---------------
 //       0 |                  1 |              0  (no indirect/relative operands)
 //       1 |                  1 |              3  (operand 0 indirect)
@@ -352,7 +369,14 @@ pol constant sel_op_is_address[5];
 //     ... |                  1 |            ...
 //   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;
+// Granular destination selector for the addressing-gas lookup (#[ADDRESSING_GAS_READ]). This is sound
+// because the addressing_gas value column is populated over the entire
+// [0, 2^16) range (every 16-bit bitmask), so any row toggled within sel_range_16 carries a valid gas value;
+// a static assertion in precomputed_trace.cpp guarantees the table spans 2^16 rows.
+pol commit sel_addressing_gas; // @boolean
+sel_addressing_gas * (1 - sel_addressing_gas) = 0;
+// Relation #[GRANULAR_SELECTORS_ON_RANGE_16] ensures that `sel_addressing_gas == 1 ==> sel_range_16 == 1`.
+
 pol constant addressing_gas;
 
 // ===== Section 11: Phase table =====
@@ -444,3 +468,7 @@ pol constant is_deployer;
 pol constant is_class_id;
 pol constant is_init_hash;
 pol constant is_immutables_hash;
+
+// Granular destination selectors must be on sel_range_16 range.
+#[GRANULAR_SELECTORS_ON_RANGE_16]
+(sel_range_16_active + sel_bitwise + sel_addressing_gas) * (1 - sel_range_16) = 0;

barretenberg/cpp/pil/vm2/memory.pil

@@ -59,18 +59,18 @@ include "precomputed.pil";
  *
  * Interactions (this gadget as source -- lookups into precomputed tables):
  *
- * | Lookup Name          | Selector                  | LHS Tuple                               | RHS (precomputed)               |
- * |----------------------|---------------------------|-----------------------------------------|---------------------------------|
- * | #[DYN_RNG_CHK_POW_2] | sel                       | { dyn_rng_chk_bits, dyn_rng_chk_pow_2 } | sel_range_8 { idx, power_of_2 } |
- * | #[DYN_DIFF_IS_U16]   | sel                       | { dyn_diff }                            | sel_range_16 { idx }            |
- * | #[R0_IS_U16]         | sel_r0_16_bit_rng_lookup  | { u16_r0 }                              | sel_range_16 { idx }            |
- * | #[R1_IS_U16]         | sel_r1_16_bit_rng_lookup  | { u16_r1 }                              | sel_range_16 { idx }            |
- * | #[R2_IS_U16]         | sel_r2_16_bit_rng_lookup  | { u16_r2 }                              | sel_range_16 { idx }            |
- * | #[R3_IS_U16]         | sel_r3_16_bit_rng_lookup  | { u16_r3 }                              | sel_range_16 { idx }            |
- * | #[R4_IS_U16]         | sel_r4_16_bit_rng_lookup  | { u16_r4 }                              | sel_range_16 { idx }            |
- * | #[R5_IS_U16]         | sel_r5_16_bit_rng_lookup  | { u16_r5 }                              | sel_range_16 { idx }            |
- * | #[R6_IS_U16]         | sel_r6_16_bit_rng_lookup  | { u16_r6 }                              | sel_range_16 { idx }            |
- * | #[R7_IS_U16]         | sel                       | { u16_r7 }                              | sel_range_16 { idx }            |
+ * | Lookup Name          | Selector                  | LHS Tuple                               | RHS (precomputed)                 |
+ * |----------------------|---------------------------|-----------------------------------------|-----------------------------------|
+ * | #[DYN_RNG_CHK_POW_2] | sel                       | { dyn_rng_chk_bits, dyn_rng_chk_pow_2 } | sel_range_8 { idx, power_of_2 }   |
+ * | #[DYN_DIFF_IS_U16]   | sel                       | { dyn_diff }                            | sel_range_16_active { idx }       |
+ * | #[R0_IS_U16]         | sel_r0_16_bit_rng_lookup  | { u16_r0 }                              | sel_range_16_active { idx }       |
+ * | #[R1_IS_U16]         | sel_r1_16_bit_rng_lookup  | { u16_r1 }                              | sel_range_16_active { idx }       |
+ * | #[R2_IS_U16]         | sel_r2_16_bit_rng_lookup  | { u16_r2 }                              | sel_range_16_active { idx }       |
+ * | #[R3_IS_U16]         | sel_r3_16_bit_rng_lookup  | { u16_r3 }                              | sel_range_16_active { idx }       |
+ * | #[R4_IS_U16]         | sel_r4_16_bit_rng_lookup  | { u16_r4 }                              | sel_range_16_active { idx }       |
+ * | #[R5_IS_U16]         | sel_r5_16_bit_rng_lookup  | { u16_r5 }                              | sel_range_16_active { idx }       |
+ * | #[R6_IS_U16]         | sel_r6_16_bit_rng_lookup  | { u16_r6 }                              | sel_range_16_active { idx }       |
+ * | #[R7_IS_U16]         | sel                       | { u16_r7 }                              | sel_range_16_active { idx }       |
  *
  * Soundness argument summary:
  * 1) #[CHECK_RECOMPOSITION] forces value = sum of (u16_r_i * 2^(16*i)) + u16_r7 * 2^(16*k),
@@ -274,7 +274,7 @@ namespace range_check;
     // The value of dyn_diff has to be between [0, 2^16)
     // To check we did not underflow we just range check it
     #[DYN_DIFF_IS_U16]
-    sel { dyn_diff } in precomputed.sel_range_16 { precomputed.idx };
+    sel { dyn_diff } in precomputed.sel_range_16_active { precomputed.idx };
 
     ////////////////////////////////////////////////
     // Cumulative Lookup Selectors and 16-bit Range Check Lookups
@@ -312,18 +312,18 @@ namespace range_check;
     sel_r6_16_bit_rng_lookup - CUM_LTE_128 = 0;
 
     #[R0_IS_U16]
-    sel_r0_16_bit_rng_lookup { u16_r0 } in precomputed.sel_range_16 { precomputed.idx };
+    sel_r0_16_bit_rng_lookup { u16_r0 } in precomputed.sel_range_16_active { precomputed.idx };
     #[R1_IS_U16]
-    sel_r1_16_bit_rng_lookup { u16_r1 } in precomputed.sel_range_16 { precomputed.idx };
+    sel_r1_16_bit_rng_lookup { u16_r1 } in precomputed.sel_range_16_active { precomputed.idx };
     #[R2_IS_U16]
-    sel_r2_16_bit_rng_lookup { u16_r2 } in precomputed.sel_range_16 { precomputed.idx };
+    sel_r2_16_bit_rng_lookup { u16_r2 } in precomputed.sel_range_16_active { precomputed.idx };
     #[R3_IS_U16]
-    sel_r3_16_bit_rng_lookup { u16_r3 } in precomputed.sel_range_16 { precomputed.idx };
+    sel_r3_16_bit_rng_lookup { u16_r3 } in precomputed.sel_range_16_active { precomputed.idx };
     #[R4_IS_U16]
-    sel_r4_16_bit_rng_lookup { u16_r4 } in precomputed.sel_range_16 { precomputed.idx };
+    sel_r4_16_bit_rng_lookup { u16_r4 } in precomputed.sel_range_16_active { precomputed.idx };
     #[R5_IS_U16]
-    sel_r5_16_bit_rng_lookup { u16_r5 } in precomputed.sel_range_16 { precomputed.idx };
+    sel_r5_16_bit_rng_lookup { u16_r5 } in precomputed.sel_range_16_active { precomputed.idx };
     #[R6_IS_U16]
-    sel_r6_16_bit_rng_lookup { u16_r6 } in precomputed.sel_range_16 { precomputed.idx };
+    sel_r6_16_bit_rng_lookup { u16_r6 } in precomputed.sel_range_16_active { precomputed.idx };
     #[R7_IS_U16]
-    sel { u16_r7 } in precomputed.sel_range_16 { precomputed.idx };
+    sel { u16_r7 } in precomputed.sel_range_16_active { precomputed.idx };