feat(3738): AVM basic arithmetic operations for non ff types

barretenberg/cpp/pil/avm/alu_chip.pil

@@ -0,0 +1,214 @@
+include "avm_mini.pil";
+
+namespace aluChip(256);
+
+    // ========= Table ALU-TR =================================================
+
+    // References to main trace table of sub-operations, clk, intermediate
+    // registers, operation selectors.
+    // TODO: Think on optimizations to decrease the number of such "copied" columns
+    pol commit alu_clk;
+    pol commit alu_ia; // Intermediate registers
+    pol commit alu_ib;
+    pol commit alu_ic;
+    pol commit alu_op_add; // Operation selectors
+    pol commit alu_op_sub;
+    pol commit alu_op_mul;
+    pol commit alu_op_div;
+
+    // Flattened boolean instruction tags
+    pol commit alu_ff_tag;
+    pol commit alu_u8_tag;
+    pol commit alu_u16_tag;
+    pol commit alu_u32_tag;
+    pol commit alu_u64_tag;
+    pol commit alu_u128_tag;
+
+    // 8-bit slice registers
+    pol commit alu_u8_r0;
+    pol commit alu_u8_r1;
+
+    // 16-bit slice registers
+    pol commit alu_u16_r0;
+    pol commit alu_u16_r1;
+    pol commit alu_u16_r2;
+    pol commit alu_u16_r3;
+    pol commit alu_u16_r4;
+    pol commit alu_u16_r5;
+    pol commit alu_u16_r6;
+    pol commit alu_u16_r7;
+
+    // 64-bit slice register
+    pol commit alu_u64_r0;
+
+    // Carry flag
+    pol commit alu_cf;
+
+    // ========= Type Constraints =============================================
+    // TODO: Range constraints for slice registers
+    //       intermediate registers ia and ib (inputs) depending on flag
+    //       Carry flag: We will have to constraint to ensure that the 
+    //                   arithmetic expressions are not overflowing finite field size
+    // Remark: Operation selectors are constrained in the main trace.
+    //         TODO: Enforce the equivalence check for the selectors between both tables.
+
+    // Boolean flattened instructions tags
+    alu_ff_tag * (1 - alu_ff_tag) = 0;
+    alu_u8_tag * (1 - alu_u8_tag) = 0;
+    alu_u16_tag * (1 - alu_u16_tag) = 0;
+    alu_u32_tag * (1 - alu_u32_tag) = 0;
+    alu_u64_tag * (1 - alu_u64_tag) = 0;
+    alu_u128_tag * (1 - alu_u128_tag) = 0;
+
+    // Operation selectors are copied from main table and do not need to be constrained here.
+
+    // ========= Inter-table Constraints ======================================
+    // TODO: Equivalence between intermediate registers, clk, type flag, operation
+    //       An ALU chiplet flag will be introduced in main trace to select relevant rows.
+
+
+    // ========= EXPLANATIONS =================================================
+    // Main trick for arithmetic operations modulo 2^k is to perform the operation
+    // over the integers and expressing the result as low + high * 2^k with low
+    // smaller than 2^k. low is used as the output. This works as long this does
+    // not overflow the underlying finite field order (u128 multiplication will be
+    // handled differently). If we want to prove that c = OP(a,b) where OP denotes
+    // an arithmetic operation modulo 2^k, we need two relations:
+    // (1) low + high * 2^k - OP(a,b) = 0
+    // (2) low - c = 0
+    //
+    // We support u8, u16, u32, u64, u128 types and decompose low into
+    // smaller bit slices, e.g., 16. For instance, low = s_0 + s_1 * 2^16 + s_2 * 2^32 + ...
+    // The slices have to be range constrained and there is a trade-off between the
+    // number of registers and complexity of the range constraints.
+    // TODO: Determine the best slice size allocation. Note that we might choose different
+    // slice sizes for the different types. At this stage, it is still unknown how this
+    // allocation affects the performance.
+    //
+    // Preliminary choice: We use one u8 register to support u8 operations and up to 8 u16
+    // registers for the other types.
+
+
+    // ============= Helper polynomial terms ============================
+    // These are intermediate polynomial terms which are not commited but
+    // serves to express commited polynomials in a more concise way.
+
+    // 16-bit slice partial sums
+    pol sum_16 =  alu_u16_r0;
+    pol sum_32 =  sum_16     + alu_u16_r1 * 2**16;
+    pol sum_64 =  sum_32     + alu_u16_r2 * 2**32 + alu_u16_r3 * 2**48; 
+    pol sum_96 =  sum_64     + alu_u16_r4 * 2**64 + alu_u16_r5 * 2**80;
+    pol sum_128 = sum_96     + alu_u16_r6 * 2**96 + alu_u16_r7 * 2**112;
+
+    // ========= ADDITION Operation Constraints ===============================
+
+    // ff addition
+    #[SUBOP_ADDITION_FF]
+    alu_ff_tag * alu_op_add * (alu_ia + alu_ib - alu_ic) = 0;
+
+    // u8 addition
+    alu_u8_tag * alu_op_add * (alu_u8_r0 + alu_cf * 2**8 - alu_ia - alu_ib) = 0;
+    alu_u8_tag * alu_op_add * (alu_u8_r0 - alu_ic) = 0;
+
+    // u16 addition
+    alu_u16_tag * alu_op_add * (sum_16 + alu_cf * 2**16  - alu_ia - alu_ib) = 0;
+    alu_u16_tag * alu_op_add * (sum_16 - alu_ic) = 0;
+
+    // u32 addition
+    alu_u32_tag * alu_op_add * (sum_32 + alu_cf * 2**32 - alu_ia - alu_ib) = 0;
+    alu_u32_tag * alu_op_add * (sum_32 - alu_ic) = 0;
+
+    // u64 addition
+    alu_u64_tag * alu_op_add * (sum_64 + alu_cf * 2**64 - alu_ia - alu_ib) = 0;
+    alu_u64_tag * alu_op_add * (sum_64 - alu_ic) = 0;
+
+    // u128 addition
+    alu_u128_tag * alu_op_add * (sum_128 + alu_cf * 2**128 - alu_ia - alu_ib) = 0;
+    alu_u128_tag * alu_op_add * (sum_128 - alu_ic) = 0;
+
+    // ========= SUBTRACTION Operation Constraints ===============================
+
+    // a - b = c <==> c + b = a (mod 2^k)
+    // Same constraints as for addition but we swap alu_ia with alu_ic
+
+    // ff subtraction
+    #[SUBOP_SUBTRACTION_FF]
+    alu_ff_tag * alu_op_sub * (alu_ia - alu_ib - alu_ic) = 0;
+
+    // u8 subtraction
+    alu_u8_tag * alu_op_sub * (alu_u8_r0 + alu_cf * 2**8 - alu_ic - alu_ib) = 0;
+    alu_u8_tag * alu_op_sub * (alu_u8_r0 - alu_ia) = 0;
+
+    // u16 subtraction
+    alu_u16_tag * alu_op_sub * (sum_16 + alu_cf * 2**16 - alu_ic - alu_ib) = 0;
+    alu_u16_tag * alu_op_sub * (sum_16 - alu_ia) = 0;
+
+    // u32 subtraction
+    alu_u32_tag * alu_op_sub * (sum_32 + alu_cf * 2**32 - alu_ic - alu_ib) = 0;
+    alu_u32_tag * alu_op_sub * (sum_32 - alu_ia) = 0;
+
+    // u64 subtraction
+    alu_u64_tag * alu_op_sub * (sum_64 + alu_cf * 2**64 - alu_ic - alu_ib) = 0;
+    alu_u64_tag * alu_op_sub * (sum_64 - alu_ia) = 0;
+
+    // u128 subtraction
+    alu_u128_tag * alu_op_sub * (sum_128 + alu_cf * 2**128 - alu_ic - alu_ib) = 0;
+    alu_u128_tag * alu_op_sub * (sum_128 - alu_ia) = 0;
+
+    // ========= MULTIPLICATION Operation Constraints ===============================
+
+    // ff multiplication
+    #[SUBOP_MULTIPLICATION_FF]
+    alu_ff_tag * alu_op_mul * (alu_ia * alu_ib - alu_ic) = 0;
+
+    // We need 2k bits to express the product (a*b) over the integer, i.e., for type uk
+    // we express the product as sum_k (u8 is an exception as we need 8-bit registers)
+
+    // u8 multiplication
+    alu_u8_tag * alu_op_mul * (alu_u8_r0 + alu_u8_r1 * 2**8 - alu_ia * alu_ib) = 0;
+    alu_u8_tag * alu_op_mul * (alu_u8_r0 - alu_ic) = 0;
+
+    // u16 multiplication
+    alu_u16_tag * alu_op_mul * (sum_32 - alu_ia * alu_ib) = 0;
+    alu_u16_tag * alu_op_mul * (sum_16 - alu_ic) = 0;
+
+    // u32 multiplication
+    alu_u32_tag * alu_op_mul * (sum_64 - alu_ia * alu_ib) = 0;
+    alu_u32_tag * alu_op_mul * (sum_32 - alu_ic) = 0;
+
+    // u64 multiplication
+    alu_u64_tag * alu_op_mul * (sum_128 - alu_ia * alu_ib) = 0;
+    alu_u64_tag * alu_op_mul * (sum_64 - alu_ic) = 0;
+
+    // ========= u128 MULTIPLICATION Operation Constraints ===============================
+    //
+    // We express a, b in 64-bit slices: a = a_l + a_h * 2^64
+    //                                   b = b_l + b_h * 2^64
+    // We show that c satisfies: a_l * b_l + (a_h * b_l + a_l * b_h) * 2^64 = R * 2^128 + c
+    // for a R < 2^65. Equivalently:
+    // a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c
+    // for a bit carry flag CF and R' range constrained to 64 bits.
+    // We use two lines in the execution trace. First line represents a 
+    // as decomposed over 16-bit registers. Second line represents b.
+    // Selector flag is only toggled in the first line and we access b through
+    // shifted polynomials.
+    // R' is stored in alu_u64_r0
+
+    // 64-bit higher limb
+    pol sum_high_64 = alu_u16_r4 + alu_u16_r5 * 2**16 + alu_u16_r6 * 2**32 + alu_u16_r7 * 2**48;
+
+    // 64-bit lower limb for next row
+    pol sum_shifted_64 = alu_u16_r0' + alu_u16_r1' * 2**16 + alu_u16_r2' * 2**32 + alu_u16_r3' * 2**48;
+
+    // 64-bit higher limb for next row
+    pol sum_high_shifted_64 = alu_u16_r4' + alu_u16_r5' * 2**16 + alu_u16_r6' * 2**32 + alu_u16_r7' * 2**48;
+
+    // Arithmetic relations
+    alu_u128_tag * alu_op_mul * (sum_64 + sum_high_64 * 2**64 - alu_ia) = 0;
+    alu_u128_tag * alu_op_mul * (sum_shifted_64 + sum_high_shifted_64 * 2**64 - alu_ib) = 0;
+    alu_u128_tag * alu_op_mul * (
+            alu_ia * sum_shifted_64
+          + sum_64 * sum_high_shifted_64 * 2**64
+          - (alu_cf * 2**64 + alu_u64_r0) * 2**128
+          - alu_ic
+        ) = 0;

barretenberg/cpp/pil/avm/avm_mini.pil

@@ -1,5 +1,6 @@
 
 include "mem_trace.pil";
+include "alu_chip.pil";
 
 namespace avmMini(256);
 
@@ -102,18 +103,6 @@ namespace avmMini(256);
     tag_err * ib = 0;
     tag_err * ic = 0;
 
-    // Relation for addition over the finite field
-    #[SUBOP_ADDITION_FF]
-    sel_op_add * (ia + ib - ic) = 0;
-
-    // Relation for subtraction over the finite field
-    #[SUBOP_SUBTRACTION_FF]
-    sel_op_sub * (ia - ib - ic) = 0;
-
-    // Relation for multiplication over the finite field
-    #[SUBOP_MULTIPLICATION_FF]
-    sel_op_mul * (ia * ib - ic) = 0;
-
     // Relation for division over the finite field
     // If tag_err == 1 in a division, then ib == 0 and op_err == 1.
     #[SUBOP_DIVISION_FF]