feat: avm lookup and/or/xor (#5338)

lookup op for and/or and xor, plus a refactor of the test to use TEST_Ps

barretenberg/cpp/pil/avm/avm_binary.pil

@@ -0,0 +1,81 @@
+
+include "avm_byte_lookup.pil";
+include "avm_main.pil";
+
+namespace avm_binary(256);
+
+    pol commit bin_clk;
+
+    // Selector for Binary Operation
+    pol commit bin_sel;
+    bin_sel * (1 - bin_sel) = 0;
+
+    // Byte recomposition column, the value in these columns are part of the equivalence
+    // check to main wherever Start is set to 1.
+    pol commit acc_ia;
+    pol commit acc_ib;
+    pol commit acc_ic;
+
+    // This is the instruction tag {1,2,3,4,5} (restricted to not be a field)
+    // Operations over FF are not supported, it is assumed this exclusion is handled
+    // outside of this subtrace.
+
+    // Constraints come from equiv to main_trace
+    pol commit in_tag;
+
+    // Selectors for binary operations, correctness checked by permutation to the main trace.
+    // Op Id is restricted to be the same during the same computation (i.e. between Starts)
+    pol commit op_id;
+    #[OP_ID_REL]
+    (op_id' - op_id) * mem_tag_ctr = 0;
+
+    // Little Endian bitwise decomposition of accumulators (which are processed top-down),
+    // constrained to be U8 given by the lookup to the avm_byte_lookup
+    pol commit bin_ia_bytes;
+    pol commit bin_ib_bytes;
+    pol commit bin_ic_bytes;
+
+    pol commit start; // Identifies when we want to capture the output to the main trace.
+
+
+    // To support dynamically sized memory operands we use a counter against a lookup
+    // This decrementing counter goes from [MEM_TAG, 0] where MEM_TAG is the number of bytes in the
+    // corresponding integer. i.e. MEM_TAG is between 1 (U8) and 16(U128).
+    // Consistency can be achieved with a lookup table between the instr_tag and bytes_length
+    pol commit mem_tag_ctr;
+    #[MEM_TAG_REL]
+    (mem_tag_ctr' - mem_tag_ctr + 1) * mem_tag_ctr = 0;
+
+    // Bin_sel is a boolean that is set to 1 if mem_tag_ctr != 0.
+    // This is checked by two relation conditions and utilising mem_tag_ctr_inv
+    pol commit mem_tag_ctr_inv;
+
+    // bin_sel is set to 1 when mem_tag_ctr != 0, and 0 otherwise.
+    // we constrain it such that bin_sel = mem_tag_ctr * mem_tag_ctr_inv unless mem_tag_ctr = 0 the bin_sel = 0
+    // In here we use the consolidated equality relation because it doesnt require us to enforce
+    // this additional relation: mem_tag_ctr_inv = 1 when mem_tag_ctr = 0. (allows default zero value in trace)
+    #[BIN_SEL_CTR_REL]
+    mem_tag_ctr * ((1 - bin_sel) * (1 - mem_tag_ctr_inv) + mem_tag_ctr_inv) - bin_sel = 0;
+
+    // Forces accumulator to start at zero when mem_tag_ctr == 0
+    (1 - bin_sel) * acc_ia = 0; 
+    (1 - bin_sel) * acc_ib = 0; 
+    (1 - bin_sel) * acc_ic = 0;
+
+    #[LOOKUP_BYTE_LENGTHS]
+    start {in_tag, mem_tag_ctr} 
+    in 
+    avm_byte_lookup.bin_sel {avm_byte_lookup.table_in_tags, avm_byte_lookup.table_byte_lengths};
+
+    #[LOOKUP_BYTE_OPERATIONS]
+    bin_sel {op_id, bin_ia_bytes, bin_ib_bytes, bin_ic_bytes}
+    in 
+    avm_byte_lookup.bin_sel {avm_byte_lookup.table_op_id, avm_byte_lookup.table_input_a, avm_byte_lookup.table_input_b, avm_byte_lookup.table_output};
+
+    #[ACC_REL_A]
+    (acc_ia - bin_ia_bytes - 256 * acc_ia') * mem_tag_ctr = 0;
+    #[ACC_REL_B]
+    (acc_ib - bin_ib_bytes - 256 * acc_ib') * mem_tag_ctr = 0;
+     #[ACC_REL_C]
+    (acc_ic - bin_ic_bytes - 256 * acc_ic') * mem_tag_ctr = 0;
+

barretenberg/cpp/pil/avm/avm_byte_lookup.pil

@@ -0,0 +1,16 @@
+
+namespace avm_byte_lookup(256);
+    // These columns are commited for now, but will be migrated to constant/fixed when
+    // we support more *exotic* code generation options
+    pol commit table_op_id; // identifies if operation is AND/OR/XOR
+    pol commit table_input_a; // column of all 8-bit numbers
+    pol commit table_input_b; // column of all 8-bit numbers
+    pol commit table_output; // output = a AND/OR/XOR b
+    // Selector to indicate when to utilise the lookup table
+    // TODO: Support for 1-sided lookups may make this redundant.
+    pol commit bin_sel;
+
+    // These two columns are a mapping between instruction tags and their byte lengths
+    // {U8: 1, U16: 2, ... , U128: 16}
+    pol commit table_in_tags; // Column of U8,U16,...,U128
+    pol commit table_byte_lengths; // Columns of byte lengths 1,2,...,16;

barretenberg/cpp/pil/avm/avm_main.pil

@@ -1,6 +1,7 @@
 
 include "avm_mem.pil";
 include "avm_alu.pil";
+include "avm_binary.pil";
 
 namespace avm_main(256);
 
@@ -41,10 +42,19 @@ namespace avm_main(256);
     pol commit sel_op_not;
     // EQ
     pol commit sel_op_eq;
+    // AND
+    pol commit sel_op_and;
+    // OR
+    pol commit sel_op_or;
+    // XOR
+    pol commit sel_op_xor;
 
     // Helper selector to characterize an ALU chiplet selector
     pol commit alu_sel;
 
+    // Helper selector to characterize a Binary chiplet selector
+    pol commit bin_sel;
+
     // Instruction memory tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field)
     pol commit in_tag;
 
@@ -102,6 +112,9 @@ namespace avm_main(256);
     sel_op_div * (1 - sel_op_div) = 0;
     sel_op_not * (1 - sel_op_not) = 0;
     sel_op_eq * (1 - sel_op_eq) = 0;
+    sel_op_and * (1 - sel_op_and) = 0;
+    sel_op_or * (1 - sel_op_or) = 0;
+    sel_op_xor * (1 - sel_op_xor) = 0;
 
     sel_internal_call * (1 - sel_internal_call) = 0;
     sel_internal_return * (1 - sel_internal_return) = 0;
@@ -202,7 +215,7 @@ namespace avm_main(256);
 
     //===== CONTROL_FLOW_CONSISTENCY ============================================
     pol INTERNAL_CALL_STACK_SELECTORS = (first + sel_internal_call + sel_internal_return + sel_halt);
-    pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul + sel_op_not + sel_op_eq);
+    pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul + sel_op_not + sel_op_eq + sel_op_and + sel_op_or + sel_op_xor);
 
     // Program counter must increment if not jumping or returning
     #[PC_INCREMENT]
@@ -239,6 +252,26 @@ namespace avm_main(256);
                      avm_alu.alu_op_add, avm_alu.alu_op_sub, avm_alu.alu_op_mul, avm_alu.alu_op_eq,
                      avm_alu.alu_op_not, avm_alu.alu_in_tag};
 
+
+    // Based on the boolean selectors, we derive the binary op id to lookup in the table;
+    // TODO: Check if having 4 columns (op_id + 3 boolean selectors) is more optimal that just using the op_id
+    // but with a higher degree constraint: op_id * (op_id - 1) * (op_id - 2)
+    pol commit bin_op_id;
+    #[BIN_SEL_1]
+    bin_op_id = sel_op_or + 2 * sel_op_xor; // sel_op_and excluded since op_id = 0 for op_and
+
+    // Only 1 of the binary selectors should be set (i.e. Mutual Exclusivity)
+    // Bin_sel is not explicitly constrained to be boolean, however this is enforced through
+    // the operation decomposition step during bytecode unpacking.
+    #[BIN_SEL_2]
+    bin_sel = sel_op_and + sel_op_or + sel_op_xor;
+
+    #[PERM_MAIN_BIN]
+    bin_sel {ia, ib, ic, bin_op_id, in_tag}
+    is
+    avm_binary.start {avm_binary.acc_ia, avm_binary.acc_ib, avm_binary.acc_ic,
+                      avm_binary.op_id, avm_binary.in_tag};
+
     #[PERM_MAIN_MEM_A]
     mem_op_a {clk, mem_idx_a, ia, rwa, in_tag, sel_mov}
     is
@@ -267,4 +300,4 @@ namespace avm_main(256);
     #[PERM_MAIN_MEM_IND_C]
     ind_op_c {clk, ind_c, mem_idx_c}
     is
-    avm_mem.m_ind_op_c {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val};
+    avm_mem.m_ind_op_c {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val};

barretenberg/cpp/pil/avm/avm_mem.pil

@@ -147,4 +147,4 @@ namespace avm_mem(256);
     // Finally, the following constraint guarantees that m_tag is correct for
     // the output.
     #[MOV_SAME_TAG]
-    m_sel_mov * m_tag_err = 0; // Equivalent to m_sel_mov * (m_in_tag - m_tag) = 0
+    m_sel_mov * m_tag_err = 0; // Equivalent to m_sel_mov * (m_in_tag - m_tag) = 0

barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp

@@ -7,77 +7,77 @@
 namespace bb::Avm_vm {
 
 template <typename FF> struct Avm_aluRow {
-    FF avm_alu_alu_u16_r7_shift{};
-    FF avm_alu_alu_u8_tag{};
-    FF avm_alu_alu_u128_tag{};
-    FF avm_alu_alu_ib{};
+    FF avm_alu_alu_u8_r0{};
+    FF avm_alu_alu_op_eq_diff_inv{};
+    FF avm_alu_alu_op_eq{};
+    FF avm_alu_alu_u16_r3{};
+    FF avm_alu_alu_u64_r0{};
     FF avm_alu_alu_u16_r4{};
-    FF avm_alu_alu_u16_r0{};
+    FF avm_alu_alu_u16_r3_shift{};
+    FF avm_alu_alu_u16_r6_shift{};
+    FF avm_alu_alu_u16_r0_shift{};
     FF avm_alu_alu_u16_r1_shift{};
-    FF avm_alu_alu_op_mul{};
-    FF avm_alu_alu_u16_tag{};
-    FF avm_alu_alu_u16_r2{};
     FF avm_alu_alu_u16_r1{};
-    FF avm_alu_alu_u16_r3{};
     FF avm_alu_alu_in_tag{};
-    FF avm_alu_alu_u8_r1{};
-    FF avm_alu_alu_u16_r7{};
+    FF avm_alu_alu_cf{};
+    FF avm_alu_alu_op_not{};
     FF avm_alu_alu_u16_r6{};
-    FF avm_alu_alu_op_eq{};
-    FF avm_alu_alu_u64_tag{};
+    FF avm_alu_alu_ib{};
+    FF avm_alu_alu_op_add{};
+    FF avm_alu_alu_u128_tag{};
+    FF avm_alu_alu_u16_r2_shift{};
+    FF avm_alu_alu_sel{};
+    FF avm_alu_alu_u16_r7_shift{};
+    FF avm_alu_alu_u16_r7{};
+    FF avm_alu_alu_u16_r0{};
+    FF avm_alu_alu_u32_tag{};
     FF avm_alu_alu_ia{};
     FF avm_alu_alu_ic{};
+    FF avm_alu_alu_u8_tag{};
+    FF avm_alu_alu_u8_r1{};
+    FF avm_alu_alu_u16_r4_shift{};
     FF avm_alu_alu_u16_r5_shift{};
-    FF avm_alu_alu_op_eq_diff_inv{};
-    FF avm_alu_alu_op_add{};
+    FF avm_alu_alu_u16_r2{};
+    FF avm_alu_alu_op_mul{};
     FF avm_alu_alu_ff_tag{};
-    FF avm_alu_alu_u16_r5{};
-    FF avm_alu_alu_u32_tag{};
-    FF avm_alu_alu_u16_r6_shift{};
+    FF avm_alu_alu_u64_tag{};
     FF avm_alu_alu_op_sub{};
-    FF avm_alu_alu_u16_r0_shift{};
-    FF avm_alu_alu_u16_r4_shift{};
-    FF avm_alu_alu_u8_r0{};
-    FF avm_alu_alu_op_not{};
-    FF avm_alu_alu_u16_r2_shift{};
-    FF avm_alu_alu_u16_r3_shift{};
-    FF avm_alu_alu_u64_r0{};
-    FF avm_alu_alu_sel{};
-    FF avm_alu_alu_cf{};
+    FF avm_alu_alu_u16_tag{};
+    FF avm_alu_alu_u16_r5{};
 };
 
 inline std::string get_relation_label_avm_alu(int index)
 {
     switch (index) {
-    case 19:
-        return "ALU_RES_IS_BOOL";
-
     case 20:
         return "ALU_OP_EQ";
 
     case 13:
         return "ALU_MUL_COMMON_2";
 
-    case 11:
-        return "ALU_MULTIPLICATION_FF";
-
-    case 10:
-        return "ALU_ADD_SUB_2";
-
     case 16:
         return "ALU_MULTIPLICATION_OUT_U128";
 
     case 18:
         return "ALU_OP_NOT";
 
+    case 19:
+        return "ALU_RES_IS_BOOL";
+
+    case 11:
+        return "ALU_MULTIPLICATION_FF";
+
+    case 12:
+        return "ALU_MUL_COMMON_1";
+
     case 9:
         return "ALU_ADD_SUB_1";
 
     case 17:
         return "ALU_FF_NOT_XOR";
 
-    case 12:
-        return "ALU_MUL_COMMON_1";
+    case 10:
+        return "ALU_ADD_SUB_2";
     }
     return std::to_string(index);
 }