feat: add support for u1 in the avm circuit & witgen

avm-transpiler/src/instructions.rs

@@ -94,6 +94,7 @@ impl Default for AvmInstruction {
 #[derive(Copy, Clone, Debug)]
 pub enum AvmTypeTag {
     UNINITIALIZED,
+    UINT1,
     UINT8,
     UINT16,
     UINT32,
@@ -107,6 +108,7 @@ pub enum AvmTypeTag {
 /// Constants (as used by the SET instruction) can have size
 /// different from 32 bits
 pub enum AvmOperand {
+    U1 { value: bool },
     U8 { value: u8 },
     U16 { value: u16 },
     U32 { value: u32 },
@@ -118,6 +120,7 @@ pub enum AvmOperand {
 impl Display for AvmOperand {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
         match self {
+            AvmOperand::U1 { value } => write!(f, " U1:{}", value),
             AvmOperand::U8 { value } => write!(f, " U8:{}", value),
             AvmOperand::U16 { value } => write!(f, " U16:{}", value),
             AvmOperand::U32 { value } => write!(f, " U32:{}", value),
@@ -131,6 +134,7 @@ impl Display for AvmOperand {
 impl AvmOperand {
     pub fn to_be_bytes(&self) -> Vec<u8> {
         match self {
+            AvmOperand::U1 { value } => (if *value { 1 as u8 } else { 0 as u8 }).to_be_bytes().to_vec(),
             AvmOperand::U8 { value } => value.to_be_bytes().to_vec(),
             AvmOperand::U16 { value } => value.to_be_bytes().to_vec(),
             AvmOperand::U32 { value } => value.to_be_bytes().to_vec(),

barretenberg/cpp/pil/avm/alu.pil

@@ -1,3 +1,4 @@
+include "constants_gen.pil";
 include "gadgets/range_check.pil";
 include "gadgets/cmp.pil";
 namespace alu(256);
@@ -12,16 +13,17 @@ namespace alu(256);
     pol commit ic;
     pol commit sel_alu; // Predicate to activate the copy of intermediate registers to ALU table.
 
-    // Instruction tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) copied from Main table
+    // Instruction tag (1: u1, 2: u8, 3: u16, 4: u32, 5: u64, 6: u128, 7: field) copied from Main table
     pol commit in_tag;
 
     // Flattened boolean instruction tags
-    pol commit ff_tag;
+    pol commit u1_tag;
     pol commit u8_tag;
     pol commit u16_tag;
     pol commit u32_tag;
     pol commit u64_tag;
     pol commit u128_tag;
+    pol commit ff_tag;
 
     // Compute predicate telling whether there is a row entry in the ALU table.
     sel_alu = op_add + op_sub + op_mul + op_not + op_eq + op_cast + op_lt + op_lte + op_shr + op_shl + op_div;
@@ -30,18 +32,25 @@ namespace alu(256);
     // Remark: Operation selectors are constrained in the main trace.
 
     // Boolean flattened instructions tags
-    ff_tag * (1 - ff_tag) = 0;
+    u1_tag * (1 - u1_tag) = 0;
     u8_tag * (1 - u8_tag) = 0;
     u16_tag * (1 - u16_tag) = 0;
     u32_tag * (1 - u32_tag) = 0;
     u64_tag * (1 - u64_tag) = 0;
     u128_tag * (1 - u128_tag) = 0;
+    ff_tag * (1 - ff_tag) = 0;
 
     // Mutual exclusion of the flattened instruction tag.
-    sel_alu * (ff_tag + u8_tag + u16_tag + u32_tag + u64_tag + u128_tag - 1) = 0;
+    sel_alu * (u1_tag + u8_tag + u16_tag + u32_tag + u64_tag + u128_tag + ff_tag - 1) = 0;
 
     // Correct flattening of the instruction tag.
-    in_tag = u8_tag + 2 * u16_tag + 3 * u32_tag + 4 * u64_tag + 5 * u128_tag + 6 * ff_tag;
+    in_tag = u1_tag // * 1 (constants.MEM_TAG_U1)
+           + (constants.MEM_TAG_U8 * u8_tag)
+           + (constants.MEM_TAG_U16 * u16_tag)
+           + (constants.MEM_TAG_U32 * u32_tag)
+           + (constants.MEM_TAG_U64 * u64_tag)
+           + (constants.MEM_TAG_U128 * u128_tag)
+           + (constants.MEM_TAG_FF * ff_tag);
 
     // Operation selectors are copied from main table and do not need to be constrained here.
     // Mutual exclusion of op_add and op_sub are derived from their mutual exclusion in the
@@ -59,7 +68,7 @@ namespace alu(256);
     range_check_input_value = (op_add + op_sub + op_mul + op_cast + op_div) * ic + (op_shr * a_hi * NON_TRIVIAL_SHIFT) + (op_shl * a_lo * NON_TRIVIAL_SHIFT);
     // The allowed bit range is defined by the instr tag, unless in shifts where it's different
     range_check_num_bits = 
-        (op_add + op_sub + op_mul + op_cast + op_div) * (u8_tag * 8 + u16_tag * 16 + u32_tag * 32 + u64_tag * 64 + u128_tag * 128) + 
+        (op_add + op_sub + op_mul + op_cast + op_div) * (u1_tag * 1 + u8_tag * 8 + u16_tag * 16 + u32_tag * 32 + u64_tag * 64 + u128_tag * 128) + 
         (op_shl + op_shr) * (MAX_BITS - ib) * NON_TRIVIAL_SHIFT;
 
     // Permutation to the Range Check Gadget
@@ -92,15 +101,16 @@ namespace alu(256);
     // These are useful and commonly used relations / columns used through the file 
 
     // The maximum number of bits as defined by the instr tag
-    pol MAX_BITS = u8_tag * 8 + u16_tag * 16 + u32_tag * 32 + u64_tag * 64 + u128_tag * 128;
+    pol MAX_BITS = u1_tag * 1 + u8_tag * 8 + u16_tag * 16 + u32_tag * 32 + u64_tag * 64 + u128_tag * 128;
     // 2^MAX_BITS
-    pol MAX_BITS_POW = u8_tag * 2**8 + u16_tag * 2**16 + u32_tag * 2**32 + u64_tag * 2**64 + u128_tag * 2**128;
+    pol MAX_BITS_POW = u1_tag * 2 + u8_tag * 2**8 + u16_tag * 2**16 + u32_tag * 2**32 + u64_tag * 2**64 + u128_tag * 2**128;
     pol UINT_MAX = MAX_BITS_POW - 1;
 
     // Value of p - 1
     pol MAX_FIELD_VALUE = 21888242871839275222246405745257275088548364400416034343698204186575808495616;
 
     // Used when we split inputs into lo and hi limbs each of (MAX_BITS / 2)
+    // omitted: u1_tag * 0 (no need for limbs...)
     pol LIMB_BITS_POW = u8_tag * 2**4 + u16_tag * 2**8 + u32_tag * 2**16 + u64_tag * 2**32 + u128_tag * 2**64;
     // Lo and Hi Limbs for ia, ib and ic resp. Useful when performing operations over integers
     pol commit a_lo;
@@ -132,7 +142,8 @@ namespace alu(256);
     a_lo * b_hi + b_lo * a_hi = partial_prod_lo + LIMB_BITS_POW * partial_prod_hi;
 
     // This holds the product over the integers
-    pol PRODUCT = a_lo * b_lo + LIMB_BITS_POW * partial_prod_lo + MAX_BITS_POW * (partial_prod_hi + a_hi * b_hi);
+    // (u1 multiplication only cares about a_lo and b_lo)
+    pol PRODUCT = a_lo * b_lo + (1 - u1_tag) * (LIMB_BITS_POW * partial_prod_lo + MAX_BITS_POW * (partial_prod_hi + a_hi * b_hi));
 
     // =============== ADDITION/SUBTRACTION Operation Constraints ================================================= 
     pol commit op_add;
@@ -243,6 +254,7 @@ namespace alu(256);
 
     // =============== Trivial Shift Operation ================================================= 
     // We use the comparison gadget to test ib > (MAX_BITS - 1)
+    // (always true for u1 - all u1 shifts are trivial)
     (op_shl + op_shr) * (cmp_gadget_input_a - ib) = 0;
     (op_shl + op_shr) * (cmp_gadget_input_b - (MAX_BITS - 1) ) = 0;
 

barretenberg/cpp/pil/avm/binary.pil

@@ -13,7 +13,7 @@ namespace binary(256);
     pol commit acc_ib;
     pol commit acc_ic;
 
-    // This is the instruction tag {1,2,3,4,5} (restricted to not be a field)
+    // This is the instruction tag {1,2,3,4,5,6} (restricted to not be a field)
     // Operations over FF are not supported, it is assumed this exclusion is handled
     // outside of this subtrace.
 
@@ -37,7 +37,7 @@ namespace binary(256);
 
     // 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).
+    // 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]

barretenberg/cpp/pil/avm/constants_gen.pil

@@ -11,6 +11,13 @@ namespace constants(256);
     pol MAX_NULLIFIER_NON_EXISTENT_READ_REQUESTS_PER_CALL = 16;
     pol MAX_L1_TO_L2_MSG_READ_REQUESTS_PER_CALL = 16;
     pol MAX_UNENCRYPTED_LOGS_PER_CALL = 4;
+    pol MEM_TAG_U1 = 1;
+    pol MEM_TAG_U8 = 2;
+    pol MEM_TAG_U16 = 3;
+    pol MEM_TAG_U32 = 4;
+    pol MEM_TAG_U64 = 5;
+    pol MEM_TAG_U128 = 6;
+    pol MEM_TAG_FF = 7;
     pol SENDER_SELECTOR = 0;
     pol ADDRESS_SELECTOR = 1;
     pol STORAGE_ADDRESS_SELECTOR = 1;

barretenberg/cpp/pil/avm/fixed/byte_lookup.pil

@@ -8,6 +8,6 @@ namespace byte_lookup(256);
     pol constant sel_bin;
 
     // These two columns are a mapping between instruction tags and their byte lengths
-    // {U8: 1, U16: 2, ... , U128: 16}
-    pol constant table_in_tags; // Column of U8,U16,...,U128
-    pol constant table_byte_lengths; // Columns of byte lengths 1,2,...,16;
+    // {U1: 1, U8: 1, U16: 2, ... , U128: 16}
+    pol constant table_in_tags; // Column of U1,U8,U16,...,U128
+    pol constant table_byte_lengths; // Columns of byte lengths 1,1,2,...,16;

barretenberg/cpp/pil/avm/main.pil

@@ -146,7 +146,7 @@ namespace main(256);
     // Helper selector to characterize a Binary chiplet selector
     pol commit sel_bin;
 
-    // Instruction memory tags read/write (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field)
+    // Instruction memory tags read/write (1: u1, 2: u8, 3: u16, 4: u32, 5: u64, 6: u128, 7: field)
     pol commit r_in_tag;
     pol commit w_in_tag;
     pol commit alu_in_tag; // Copy of r_in_tag or w_in_tag depending of the operation. It is sent to ALU trace.
@@ -311,17 +311,17 @@ namespace main(256);
     //      values should be written into these memory indices.
     //    - For indirect memory accesses, the memory trace constraints ensure that
     //      loaded values come from memory addresses with tag u32. This is enforced in the memory trace
-    //      where each memory entry with flag sel_resolve_ind_addr_x (for x = a,b,c,d) constrains r_int_tag == 3 (u32).
+    //      where each memory entry with flag sel_resolve_ind_addr_x (for x = a,b,c,d) constrains r_int_tag is u32.
     //
     // - ind_addr_a, ind_addr_b, ind_addr_c, ind_addr_d to u32 type: Should be guaranteed by bytecode validation and
     // instruction decomposition as only immediate 32-bit values should be written into the indirect registers.
     //
-    // - 0 <= r_in_tag, w_in_tag <= 6 // This should be constrained by the operation decomposition.
+    // - 0 <= r_in_tag, w_in_tag <= constants.MEM_TAG_FF // This should be constrained by the operation decomposition.
 
     //====== COMPARATOR OPCODES CONSTRAINTS =====================================
-    // Enforce that the tag for the ouput of EQ opcode is u8 (i.e. equal to 1).
-    #[OUTPUT_U8]
-    (sel_op_eq + sel_op_lte + sel_op_lt) * (w_in_tag - 1) = 0;
+    // Enforce that the tag for the ouput of EQ opcode is u1 (i.e. equal to 1).
+    #[OUTPUT_U1]
+    (sel_op_eq + sel_op_lte + sel_op_lt) * (w_in_tag - constants.MEM_TAG_U1) = 0;
 
     //====== FDIV OPCODE CONSTRAINTS ============================================
     // Relation for division over the finite field
@@ -340,13 +340,13 @@ namespace main(256);
     #[SUBOP_FDIV_ZERO_ERR2]
     (sel_op_fdiv + sel_op_div) * op_err * (1 - inv) = 0;
 
-    // Enforcement that instruction tags are FF (tag constant 6).
+    // Enforcement that instruction tags are FF
     // TODO: These 2 conditions might be removed and enforced through
     //       the bytecode decomposition instead.
     #[SUBOP_FDIV_R_IN_TAG_FF]
-    sel_op_fdiv * (r_in_tag - 6) = 0;
+    sel_op_fdiv * (r_in_tag - constants.MEM_TAG_FF) = 0;
     #[SUBOP_FDIV_W_IN_TAG_FF]
-    sel_op_fdiv * (w_in_tag - 6) = 0;
+    sel_op_fdiv * (w_in_tag - constants.MEM_TAG_FF) = 0;
 
     // op_err cannot be maliciously activated for a non-relevant
     // operation selector, i.e., op_err == 1 ==> sel_op_fdiv || sel_op_XXX || ...

barretenberg/cpp/pil/avm/mem.pil

@@ -1,4 +1,5 @@
 include "main.pil";
+include "constants_gen.pil";
 include "./gadgets/range_check.pil";
 
 namespace mem(256);
@@ -8,7 +9,7 @@ namespace mem(256);
     pol commit addr;
     pol commit space_id;
     pol commit glob_addr;
-    pol commit tag; // Memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
+    pol commit tag; // Memory tag (0: uninitialized, 1: u1, 2: u8, 3: u16, 4: u32, 5: u64, 6: u128, 7:field)
     pol commit val;
     pol commit rw; // Enum: 0 (read), 1 (write)
     pol commit lastAccess; // Boolean (1 when this row is the last of a given address)
@@ -223,11 +224,11 @@ namespace mem(256);
     rw * tag_err = 0;
 
     //====== Indirect Memory Constraints =====================================
-    // Enforce r_in_tag == 3, i.e., r_in_tag must be U32
-    sel_resolve_ind_addr_a * (r_in_tag - 3) = 0;
-    sel_resolve_ind_addr_b * (r_in_tag - 3) = 0;
-    sel_resolve_ind_addr_c * (r_in_tag - 3) = 0;
-    sel_resolve_ind_addr_d * (r_in_tag - 3) = 0;
+    // Enforce r_in_tag is U32
+    sel_resolve_ind_addr_a * (r_in_tag - constants.MEM_TAG_U32) = 0;
+    sel_resolve_ind_addr_b * (r_in_tag - constants.MEM_TAG_U32) = 0;
+    sel_resolve_ind_addr_c * (r_in_tag - constants.MEM_TAG_U32) = 0;
+    sel_resolve_ind_addr_d * (r_in_tag - constants.MEM_TAG_U32) = 0;
 
     // Indirect operation is always a load
     sel_resolve_ind_addr_a * rw = 0;
@@ -236,19 +237,19 @@ namespace mem(256);
     sel_resolve_ind_addr_d * rw = 0;
 
     //====== CALLDATACOPY/RETURN specific constraints ==================================
-    sel_op_slice * (w_in_tag - 6) = 0; // Only write elements of type FF
-    sel_op_slice * (r_in_tag - 6) = 0; // Only read elements of type FF
+    sel_op_slice * (w_in_tag - constants.MEM_TAG_FF) = 0; // Only write elements of type FF
+    sel_op_slice * (r_in_tag - constants.MEM_TAG_FF) = 0; // Only read elements of type FF
 
     //====== POSEIDON2 specific constraints ==================================
-    sel_op_poseidon_read_a * (w_in_tag - 6) = 0; // Only read elements of type FF
-    sel_op_poseidon_read_b * (w_in_tag - 6) = 0; // Only read elements of type FF
-    sel_op_poseidon_read_c * (w_in_tag - 6) = 0; // Only read elements of type FF
-    sel_op_poseidon_read_d * (w_in_tag - 6) = 0; // Only read elements of type FF
-
-    sel_op_poseidon_write_a * (r_in_tag - 6) = 0; // Only write elements of type FF
-    sel_op_poseidon_write_b * (r_in_tag - 6) = 0; // Only write elements of type FF
-    sel_op_poseidon_write_c * (r_in_tag - 6) = 0; // Only write elements of type FF
-    sel_op_poseidon_write_d * (r_in_tag - 6) = 0; // Only write elements of type FF
+    sel_op_poseidon_read_a * (w_in_tag - constants.MEM_TAG_FF) = 0; // Only read elements of type FF
+    sel_op_poseidon_read_b * (w_in_tag - constants.MEM_TAG_FF) = 0; // Only read elements of type FF
+    sel_op_poseidon_read_c * (w_in_tag - constants.MEM_TAG_FF) = 0; // Only read elements of type FF
+    sel_op_poseidon_read_d * (w_in_tag - constants.MEM_TAG_FF) = 0; // Only read elements of type FF
+
+    sel_op_poseidon_write_a * (r_in_tag - constants.MEM_TAG_FF) = 0; // Only write elements of type FF
+    sel_op_poseidon_write_b * (r_in_tag - constants.MEM_TAG_FF) = 0; // Only write elements of type FF
+    sel_op_poseidon_write_c * (r_in_tag - constants.MEM_TAG_FF) = 0; // Only write elements of type FF
+    sel_op_poseidon_write_d * (r_in_tag - constants.MEM_TAG_FF) = 0; // Only write elements of type FF
 
     //====== MOV/CMOV Opcode Tag Constraint =====================================
     // The following constraint ensures that the r_in_tag is set to tag for

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

@@ -107,6 +107,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
                 polys.alu_sel_shift_which.set_if_valid_index(i, rows[i].alu_sel_shift_which);
                 polys.alu_u128_tag.set_if_valid_index(i, rows[i].alu_u128_tag);
                 polys.alu_u16_tag.set_if_valid_index(i, rows[i].alu_u16_tag);
+                polys.alu_u1_tag.set_if_valid_index(i, rows[i].alu_u1_tag);
                 polys.alu_u32_tag.set_if_valid_index(i, rows[i].alu_u32_tag);
                 polys.alu_u64_tag.set_if_valid_index(i, rows[i].alu_u64_tag);
                 polys.alu_u8_tag.set_if_valid_index(i, rows[i].alu_u8_tag);

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

@@ -45,8 +45,10 @@ std::shared_ptr<Flavor::ProvingKey> AvmComposer::compute_proving_key(CircuitCons
     }
 
     // Initialize proving_key
-    const size_t subgroup_size = circuit_constructor.get_circuit_subgroup_size();
-    proving_key = std::make_shared<Flavor::ProvingKey>(subgroup_size, 0);
+    {
+        const size_t subgroup_size = circuit_constructor.get_circuit_subgroup_size();
+        proving_key = std::make_shared<Flavor::ProvingKey>(subgroup_size, 0);
+    }
 
     return proving_key;
 }