feat: merge-train/avm (#15940)

See
[merge-train-readme.md](https://github.com/AztecProtocol/aztec-packages/blob/next/.github/workflows/merge-train-readme.md).

BEGIN_COMMIT_OVERRIDE
feat(avm)!: ALU MUL (#15880)
fix(avm): catch out of gas in execution loop (#15994)
END_COMMIT_OVERRIDE

---------

Co-authored-by: AztecBot <[email protected]>
Co-authored-by: Miranda Wood <[email protected]>
Co-authored-by: Facundo <[email protected]>

Author: 4 people

barretenberg/cpp/pil/vm2/alu.pil

@@ -9,6 +9,7 @@ namespace alu;
 pol commit sel;
 
 pol commit sel_op_add;
+pol commit sel_op_mul;
 pol commit sel_op_eq;
 pol commit sel_op_lt;
 pol commit sel_op_lte;
@@ -37,24 +38,28 @@ pol commit cf;
 pol commit helper1;
 
 // maximum bits the number can hold (i.e. 8 for a u8):
-// TODO(MW): Now unused since we redirect the LT/LTE range checks to GT gadget - remove?
 pol commit max_bits;
 // maximum value the number can hold (i.e. 255 for a u8), we 'mod' by max_value + 1
 pol commit max_value;
 // we need a selector to conditionally lookup ff_gt when inputs a, b are fields:
 pol commit sel_is_ff;
+// we need a selector to conditionally perform u128 multiplication:
+pol commit sel_is_u128;
 
 pol IS_NOT_FF = 1 - sel_is_ff;
+pol IS_NOT_U128 = 1 - sel_is_u128;
 
 sel * (1 - sel) = 0;
 cf * (1 - cf) = 0;
 sel_is_ff * (1 - sel_is_ff) = 0;
+sel_is_u128 * (1 - sel_is_u128) = 0;
 
 // TODO: Consider to gate with (1 - sel_tag_err) for op_id. This might help us remove the (1 - sel_tag_err)
 // in various operation relations below.
 // Note that the op_ids below represent a binary decomposition (see constants_gen.pil):
 #[OP_ID_CHECK]
 op_id = sel_op_add * constants.AVM_EXEC_OP_ID_ALU_ADD
+      + sel_op_mul * constants.AVM_EXEC_OP_ID_ALU_MUL
       + sel_op_eq * constants.AVM_EXEC_OP_ID_ALU_EQ
       + sel_op_lt * constants.AVM_EXEC_OP_ID_ALU_LT
       + sel_op_lte * constants.AVM_EXEC_OP_ID_ALU_LTE
@@ -78,18 +83,28 @@ execution.sel_execute_alu {
 
 // IS_FF CHECKING
 
-// TODO(MW): remove this and check for all (i.e. replace with sel), just being lazy for now. For add, we don't care, for lt we need to differentiate.
 pol CHECK_TAG_FF = sel_op_lt + sel_op_lte + sel_op_not;
 // We prove that sel_is_ff == 1 <==> ia_tag == MEM_TAG_FF
 pol TAG_FF_DIFF = ia_tag - constants.MEM_TAG_FF;
 pol commit tag_ff_diff_inv;
 #[TAG_IS_FF]
 CHECK_TAG_FF * (TAG_FF_DIFF * (sel_is_ff * (1 - tag_ff_diff_inv) + tag_ff_diff_inv) + sel_is_ff - 1) = 0;
 
+// IS_U128 CHECKING
+
+pol CHECK_TAG_U128 = sel_op_mul;
+// We prove that sel_is_u128 == 1 <==> ia_tag == MEM_TAG_U128
+pol TAG_U128_DIFF = ia_tag - constants.MEM_TAG_U128;
+pol commit tag_u128_diff_inv;
+#[TAG_IS_U128]
+CHECK_TAG_U128 * (TAG_U128_DIFF * (sel_is_u128 * (1 - tag_u128_diff_inv) + tag_u128_diff_inv) + sel_is_u128 - 1) = 0;
+
+// Note: if we never need sel_is_ff and sel_is_u128 in the same op, can combine the above checks into one
+
 // TAG CHECKING
 
 // Will become e.g. sel_op_add * ia_tag + (comparison ops) * MEM_TAG_U1 + ....
-pol EXPECTED_C_TAG = (sel_op_add + sel_op_truncate) * ia_tag + (sel_op_eq + sel_op_lt + sel_op_lte) * constants.MEM_TAG_U1;
+pol EXPECTED_C_TAG = (sel_op_add + sel_op_truncate + sel_op_mul) * ia_tag + (sel_op_eq + sel_op_lt + sel_op_lte) * constants.MEM_TAG_U1;
 
 // The tag of c is generated by the opcode and is never wrong.
 // Gating with (1 - sel_tag_err) is necessary because when an error occurs, we have to set the tag to 0,
@@ -123,6 +138,81 @@ sel_op_add * (1 - sel_op_add) = 0;
 #[ALU_ADD]
 sel_op_add * (1 - sel_tag_err) * (ia + ib - ic - cf * (max_value + 1)) = 0;
 
+// MUL
+
+sel_op_mul * (1 - sel_op_mul) = 0;
+
+pol commit c_hi;
+
+// MUL - non u128
+
+#[ALU_MUL_NON_U128]
+sel_op_mul * IS_NOT_U128 * (1 - sel_tag_err)
+    * (
+        ia * ib
+        - ic
+        - (max_value + 1) * c_hi
+    ) = 0;
+
+// MUL - u128
+
+pol commit sel_mul_u128;
+// sel_op_mul & sel_is_u128:
+sel_mul_u128 - sel_is_u128 * sel_op_mul = 0;
+
+// Taken from vm1:
+// We express a, b in 64-bit slices: a = a_l + a_h * 2^64
+//                                   b = b_l + b_h * 2^64
+// => a * b = a_l * b_l + (a_h * b_l + a_l * b_h) * 2^64 + (a_h * b_h) * 2^128 = c_hi_full * 2^128 + c
+// => the 'top bits' are given by (c_hi_full - (a_h * b_h)) * 2^128
+// We can show for a 64 bit c_hi = c_hi_full - (a_h * b_h) % 2^64 that:
+// a_l * b_l + (a_h * b_l + a_l * b_h) * 2^64 = c_hi * 2^128 + c
+// Equivalently (cf = 0 if a_h & b_h = 0):
+// a * b_l + a_l * b_h * 2^64 = (cf * 2^64 + c_hi) * 2^128 + c
+// => no need for a_h in final relation
+
+pol commit a_lo;
+pol commit a_hi;
+pol commit b_lo;
+pol commit b_hi;
+pol TWO_POW_64 = 2 ** 64;
+
+#[A_MUL_DECOMPOSITION]
+sel_mul_u128 * (ia - (a_lo + TWO_POW_64 * a_hi)) = 0;
+#[B_MUL_DECOMPOSITION]
+sel_mul_u128 * (ib - (b_lo + TWO_POW_64 * b_hi)) = 0;
+
+#[ALU_MUL_U128]
+sel_mul_u128 * (1 - sel_tag_err)
+    * (
+        ia * b_lo + a_lo * b_hi * TWO_POW_64            // a * b without the hi bits
+        - ic                                            // c_lo
+        - (max_value + 1) * (cf * TWO_POW_64 + c_hi)    // c_hi * 2^128 + (cf ? 2^192 : 0)
+    ) = 0;
+
+// TODO: Once lookups support expression in tuple, we can inline constant_64 into the lookup.
+// Note: only used for MUL, so gated by sel_op_mul
+pol commit constant_64;
+sel_op_mul * (64 - constant_64) = 0;
+
+#[RANGE_CHECK_MUL_U128_A_LO]
+sel_mul_u128 { a_lo, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
+
+#[RANGE_CHECK_MUL_U128_A_HI]
+sel_mul_u128 { a_hi, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
+
+#[RANGE_CHECK_MUL_U128_B_LO]
+sel_mul_u128 { b_lo, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
+
+#[RANGE_CHECK_MUL_U128_B_HI]
+sel_mul_u128 { b_hi, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
+
+// No need to range_check c_hi for cases other than u128 because we know a and b's size from the tags and have looked
+// up max_value. i.e. we cannot provide a malicious c, c_hi such that a + b - c_hi * 2^n = c passes for n < 128.
+// No need to range_check c_lo = ic because the memory write will ensure ic <= max_value.
+#[RANGE_CHECK_MUL_U128_C_HI]
+sel_mul_u128 { c_hi, constant_64 } in range_check.sel { range_check.value, range_check.rng_chk_bits };
+
 // EQ
 
 sel_op_eq * (1 - sel_op_eq) = 0;
@@ -280,21 +370,21 @@ sel_op_truncate = sel_trunc_non_trivial + sel_trunc_trivial;
 #[TRUNC_TRIVIAL_CASE]
 sel_trunc_trivial * (ia - ic) = 0;
 
-pol commit lo_128; // 128-bit low limb of ia.
-pol commit hi_128; // 128-bit high limb of ia.
+// NOTE: reusing a_lo and a_hi columns from MUL in TRUNC:
+// For truncate, a_lo = 128-bit low limb of ia and a_hi = 128-bit high limb of ia.
 pol commit mid;
 
 #[LARGE_TRUNC_CANONICAL_DEC]
-sel_trunc_gte_128 { ia, lo_128, hi_128 }
+sel_trunc_gte_128 { ia, a_lo, a_hi }
 in
 ff_gt.sel_dec { ff_gt.a, ff_gt.a_lo, ff_gt.a_hi };
 
 #[SMALL_TRUNC_VAL_IS_LO]
-sel_trunc_lt_128 * (lo_128 - ia) = 0;
+sel_trunc_lt_128 * (a_lo - ia) = 0;
 
-// lo_128 = ic + mid * 2^ia_tag_bits, where 2^ia_tag_bits is max_value + 1.
+// a_lo = ic + mid * 2^ia_tag_bits, where 2^ia_tag_bits is max_value + 1.
 #[TRUNC_LO_128_DECOMPOSITION]
-sel_trunc_non_trivial * (ic + mid * (max_value + 1) - lo_128) = 0;
+sel_trunc_non_trivial * (ic + mid * (max_value + 1) - a_lo) = 0;
 
 // TODO: Once lookups support expression in tuple, we can inline mid_bits into the lookup.
 pol commit mid_bits;
@@ -305,4 +395,4 @@ mid_bits = sel_trunc_non_trivial * (128 - max_bits);
 // is supported by our range_check gadget.
 // No need to range_check ic because the memory write will ensure ic <= max_value.
 #[RANGE_CHECK_TRUNC_MID]
-sel_trunc_non_trivial {mid, mid_bits} in range_check.sel { range_check.value, range_check.rng_chk_bits };
+sel_trunc_non_trivial { mid, mid_bits } in range_check.sel { range_check.value, range_check.rng_chk_bits };

barretenberg/cpp/src/barretenberg/vm2/common/instruction_spec.cpp

@@ -431,6 +431,13 @@ const std::unordered_map<ExecutionOpCode, ExecInstructionSpec> EXEC_INSTRUCTION_
                              .add_inputs({ /*a*/ RegisterInfo::ANY_TAG,
                                            /*b*/ RegisterInfo::ANY_TAG })
                              .add_output(/*c*/) } },
+    { ExecutionOpCode::MUL,
+      { .num_addresses = 3,
+        .gas_cost = { .opcode_gas = AVM_MUL_BASE_L2_GAS, .base_da = 0, .dyn_l2 = 0, .dyn_da = 0 },
+        .register_info = RegisterInfo()
+                             .add_inputs({ /*a*/ RegisterInfo::ANY_TAG,
+                                           /*b*/ RegisterInfo::ANY_TAG })
+                             .add_output(/*c*/) } },
     { ExecutionOpCode::EQ,
       { .num_addresses = 3,
         .gas_cost = { .opcode_gas = AVM_EQ_BASE_L2_GAS, .base_da = 0, .dyn_l2 = 0, .dyn_da = 0 },