refactor(avm): extract rng chk from gas and mem

barretenberg/cpp/pil/avm/gadgets/range_check.pil

@@ -1,4 +1,5 @@
 include "../main.pil";
+include "../mem.pil";
 include "../fixed/powers.pil";
 
 namespace range_check(256);
@@ -11,7 +12,7 @@ namespace range_check(256);
     // Witnesses 
     // Value to range check
     pol commit value;
-    // Number of bits to check against
+    // Number of bits to check against (this number must be <=128)
     pol commit rng_chk_bits;
 
     // Bit Size Columns
@@ -186,3 +187,30 @@ namespace range_check(256);
     #[LOOKUP_RNG_CHK_7]
     sel_rng_chk { u16_r7 } in main.sel_rng_16 { main.clk };
 
+    // ===== MEM TRACE RANGE CHECKS =====
+    pol commit mem_rng_chk;
+    // We range check 40 bits in the mem trace
+    mem_rng_chk * (rng_chk_bits - 40) = 0;
+
+    #[PERM_RNG_MEM]
+    mem_rng_chk {clk, value}
+    is
+    mem.sel_rng_chk {mem.tsp, mem.diff};
+
+    // ===== GAS TRACE RANGE CHECKS =====
+    pol commit gas_l2_rng_chk;
+    pol commit gas_da_rng_chk;
+    // We range check 32 bits in the gas trace
+    gas_l2_rng_chk * (rng_chk_bits  - 32) = 0;
+    gas_da_rng_chk * (rng_chk_bits  - 32) = 0;
+
+    #[PERM_RNG_GAS_L2]
+    gas_l2_rng_chk {clk, value}
+    is
+    main.sel_execution_row {main.clk, main.abs_l2_rem_gas };
+
+    #[PERM_RNG_GAS_DA]
+    gas_da_rng_chk {clk, value}
+    is
+    main.sel_execution_row {main.clk, main.abs_da_rem_gas };
+

barretenberg/cpp/pil/avm/gas.pil

@@ -44,10 +44,8 @@ namespace main(256);
     pol commit da_out_of_gas;
 
     // Absolute gas remaining value after the operation in 16-bit high and low limbs
-    pol commit abs_l2_rem_gas_hi;
-    pol commit abs_l2_rem_gas_lo;
-    pol commit abs_da_rem_gas_hi;
-    pol commit abs_da_rem_gas_lo;
+    pol commit abs_l2_rem_gas;
+    pol commit abs_da_rem_gas;
 
     // Boolean constraints
     l2_out_of_gas * (1 - l2_out_of_gas) = 0;
@@ -68,22 +66,10 @@ namespace main(256);
 
     // Prove that XX_out_of_gas == 0 <==> XX_gas_remaining' >= 0
     // TODO: Ensure that remaining gas values are initialized as u32 and that gas l2_gas_op_cost/da_gas_op_cost are u32.
-    sel_execution_row * ((1 - 2 * l2_out_of_gas) * l2_gas_remaining' - 2**16 * abs_l2_rem_gas_hi - abs_l2_rem_gas_lo) = 0;
-    sel_execution_row * ((1 - 2 * da_out_of_gas) * da_gas_remaining' - 2**16 * abs_da_rem_gas_hi - abs_da_rem_gas_lo) = 0;
+    sel_execution_row * ((1 - 2 * l2_out_of_gas) * l2_gas_remaining' - abs_l2_rem_gas) = 0;
+    sel_execution_row * ((1 - 2 * da_out_of_gas) * da_gas_remaining' - abs_da_rem_gas) = 0;
 
     #[LOOKUP_OPCODE_GAS]
     sel_execution_row {opcode_val, base_l2_gas_op_cost, base_da_gas_op_cost, dyn_l2_gas_op_cost, dyn_da_gas_op_cost}
     in
     gas.sel_gas_cost {clk, gas.base_l2_gas_fixed_table, gas.base_da_gas_fixed_table, gas.dyn_l2_gas_fixed_table, gas.dyn_da_gas_fixed_table};
-
-    #[RANGE_CHECK_L2_GAS_HI]
-    sel_execution_row {abs_l2_rem_gas_hi} in sel_rng_16 {clk};
-
-    #[RANGE_CHECK_L2_GAS_LO]
-    sel_execution_row {abs_l2_rem_gas_lo} in sel_rng_16 {clk};
-
-    #[RANGE_CHECK_DA_GAS_HI]
-    sel_execution_row {abs_da_rem_gas_hi} in sel_rng_16 {clk};
-
-    #[RANGE_CHECK_DA_GAS_LO]
-    sel_execution_row {abs_da_rem_gas_lo} in sel_rng_16 {clk};

barretenberg/cpp/pil/avm/main.pil

@@ -619,12 +619,3 @@ namespace main(256);
     sel_resolve_ind_addr_d {clk, space_id, ind_addr_d, mem_addr_d}
     is
     mem.sel_resolve_ind_addr_d {mem.clk, mem.space_id, mem.addr, mem.val};
-
-    #[LOOKUP_MEM_RNG_CHK_LO]
-    mem.sel_rng_chk {mem.diff_lo} in sel_rng_16 {clk};
-
-    #[LOOKUP_MEM_RNG_CHK_MID] 
-    mem.sel_rng_chk {mem.diff_mid} in sel_rng_16 {clk};
-
-    #[LOOKUP_MEM_RNG_CHK_HI]
-    mem.sel_rng_chk {mem.diff_hi} in sel_rng_8 {clk};

barretenberg/cpp/pil/avm/mem.pil

@@ -65,10 +65,8 @@ namespace mem(256);
 
     // Helper columns
     pol commit one_min_inv; // Extra value to prove r_in_tag != tag with error handling
-    // pol DIFF: 40-bit difference between two consecutive timestamps or two consecutive addresses
-    pol commit diff_hi;  // Higher 8-bit limb of diff.
-    pol commit diff_mid; // Middle 16-bit limb of diff.
-    pol commit diff_lo;  // Lower 16-bit limb of diff.
+    // pol DIFF: 
+    pol commit diff; // 40-bit difference between two consecutive timestamps or two consecutive addresses
 
     // Type constraints
     lastAccess * (1 - lastAccess) = 0;
@@ -156,14 +154,14 @@ namespace mem(256);
     // i.e., when sel_rng_chk == 1, we compute the difference:
     // 1) glob_addr' - glob_addr if lastAccess == 1
     // 2) tsp' - tsp   if lastAccess == 0 (i.e., whenever glob_addr' == glob_addr)
-    pol DIFF = lastAccess * (glob_addr' - glob_addr) + (1 - lastAccess) * (tsp' - tsp);
+    sel_rng_chk * (diff - (lastAccess * (glob_addr' - glob_addr) + (1 - lastAccess) * (tsp' - tsp))) = 0;
 
     // We perform a 40-bit range check of DIFF which proves that glob_addr' > glob_addr if lastAccess == 1
     // and tsp' > tsp whenever glob_addr' == glob_addr
     // Therefore, we ensure proper grouping of each global address and each memory access pertaining to a given
     // global address is sorted according the arrow of time.
-    #[DIFF_RNG_CHK_DEC]
-    sel_rng_chk * (DIFF - diff_hi * 2**32 - diff_mid * 2**16 - diff_lo) = 0;
+    // #[DIFF_RNG_CHK_DEC]
+    // sel_rng_chk * (DIFF - diff_hi * 2**32 - diff_mid * 2**16 - diff_lo) = 0;
 
     // lastAccess == 0 && rw' == 0 ==> val == val'
     // This condition does not apply on the last row.

barretenberg/cpp/src/barretenberg/vm/avm/generated/circuit_builder.cpp

@@ -151,10 +151,8 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
         polys.keccakf1600_input[i] = rows[i].keccakf1600_input;
         polys.keccakf1600_output[i] = rows[i].keccakf1600_output;
         polys.keccakf1600_sel_keccakf1600[i] = rows[i].keccakf1600_sel_keccakf1600;
-        polys.main_abs_da_rem_gas_hi[i] = rows[i].main_abs_da_rem_gas_hi;
-        polys.main_abs_da_rem_gas_lo[i] = rows[i].main_abs_da_rem_gas_lo;
-        polys.main_abs_l2_rem_gas_hi[i] = rows[i].main_abs_l2_rem_gas_hi;
-        polys.main_abs_l2_rem_gas_lo[i] = rows[i].main_abs_l2_rem_gas_lo;
+        polys.main_abs_da_rem_gas[i] = rows[i].main_abs_da_rem_gas;
+        polys.main_abs_l2_rem_gas[i] = rows[i].main_abs_l2_rem_gas;
         polys.main_alu_in_tag[i] = rows[i].main_alu_in_tag;
         polys.main_base_da_gas_op_cost[i] = rows[i].main_base_da_gas_op_cost;
         polys.main_base_l2_gas_op_cost[i] = rows[i].main_base_l2_gas_op_cost;
@@ -289,9 +287,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
         polys.main_w_in_tag[i] = rows[i].main_w_in_tag;
         polys.mem_addr[i] = rows[i].mem_addr;
         polys.mem_clk[i] = rows[i].mem_clk;
-        polys.mem_diff_hi[i] = rows[i].mem_diff_hi;
-        polys.mem_diff_lo[i] = rows[i].mem_diff_lo;
-        polys.mem_diff_mid[i] = rows[i].mem_diff_mid;
+        polys.mem_diff[i] = rows[i].mem_diff;
         polys.mem_glob_addr[i] = rows[i].mem_glob_addr;
         polys.mem_last[i] = rows[i].mem_last;
         polys.mem_lastAccess[i] = rows[i].mem_lastAccess;
@@ -615,6 +611,8 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
         polys.range_check_dyn_diff[i] = rows[i].range_check_dyn_diff;
         polys.range_check_dyn_rng_chk_bits[i] = rows[i].range_check_dyn_rng_chk_bits;
         polys.range_check_dyn_rng_chk_pow_2[i] = rows[i].range_check_dyn_rng_chk_pow_2;
+        polys.range_check_gas_da_rng_chk[i] = rows[i].range_check_gas_da_rng_chk;
+        polys.range_check_gas_l2_rng_chk[i] = rows[i].range_check_gas_l2_rng_chk;
         polys.range_check_is_lte_u112[i] = rows[i].range_check_is_lte_u112;
         polys.range_check_is_lte_u128[i] = rows[i].range_check_is_lte_u128;
         polys.range_check_is_lte_u16[i] = rows[i].range_check_is_lte_u16;
@@ -623,6 +621,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
         polys.range_check_is_lte_u64[i] = rows[i].range_check_is_lte_u64;
         polys.range_check_is_lte_u80[i] = rows[i].range_check_is_lte_u80;
         polys.range_check_is_lte_u96[i] = rows[i].range_check_is_lte_u96;
+        polys.range_check_mem_rng_chk[i] = rows[i].range_check_mem_rng_chk;
         polys.range_check_rng_chk_bits[i] = rows[i].range_check_rng_chk_bits;
         polys.range_check_sel_lookup_0[i] = rows[i].range_check_sel_lookup_0;
         polys.range_check_sel_lookup_1[i] = rows[i].range_check_sel_lookup_1;
@@ -697,19 +696,12 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
         polys.lookup_byte_lengths_counts[i] = rows[i].lookup_byte_lengths_counts;
         polys.lookup_byte_operations_counts[i] = rows[i].lookup_byte_operations_counts;
         polys.lookup_opcode_gas_counts[i] = rows[i].lookup_opcode_gas_counts;
-        polys.range_check_l2_gas_hi_counts[i] = rows[i].range_check_l2_gas_hi_counts;
-        polys.range_check_l2_gas_lo_counts[i] = rows[i].range_check_l2_gas_lo_counts;
-        polys.range_check_da_gas_hi_counts[i] = rows[i].range_check_da_gas_hi_counts;
-        polys.range_check_da_gas_lo_counts[i] = rows[i].range_check_da_gas_lo_counts;
         polys.kernel_output_lookup_counts[i] = rows[i].kernel_output_lookup_counts;
         polys.lookup_into_kernel_counts[i] = rows[i].lookup_into_kernel_counts;
         polys.lookup_cd_value_counts[i] = rows[i].lookup_cd_value_counts;
         polys.lookup_ret_value_counts[i] = rows[i].lookup_ret_value_counts;
         polys.incl_main_tag_err_counts[i] = rows[i].incl_main_tag_err_counts;
         polys.incl_mem_tag_err_counts[i] = rows[i].incl_mem_tag_err_counts;
-        polys.lookup_mem_rng_chk_lo_counts[i] = rows[i].lookup_mem_rng_chk_lo_counts;
-        polys.lookup_mem_rng_chk_mid_counts[i] = rows[i].lookup_mem_rng_chk_mid_counts;
-        polys.lookup_mem_rng_chk_hi_counts[i] = rows[i].lookup_mem_rng_chk_hi_counts;
     }
 
     for (auto [shifted, to_be_shifted] : zip_view(polys.get_shifted(), polys.get_to_be_shifted())) {