Skip to content

Commit

Permalink
feat: bitwise_not avm circuit (#4548)
Browse files Browse the repository at this point in the history 
Adds the bitwise not ciricuit in the avm.

Closes #4454

---------

Co-authored-by: Ilyas Ridhuan <[email protected]>
  • Loading branch information
@IlyasRidhuan
IlyasRidhuan and IlyasRidhuan authored Feb 13, 2024
1 parent 30d3b96 commit 3a7d31b
Show file tree
Hide file tree
Showing 25 changed files with 792 additions and 315 deletions.
65 changes: 45 additions & 20 deletions barretenberg/cpp/pil/avm/alu_chip.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ namespace aluChip(256);
pol commit alu_op_sub;
pol commit alu_op_mul;
pol commit alu_op_div;
pol commit alu_op_not;

// Flattened boolean instruction tags
pol commit alu_ff_tag;
Expand Down Expand Up @@ -107,12 +108,12 @@ namespace aluChip(256);
// serves to an algebraic expression of commited polynomials in a more concise way.

// Bit slices partial sums
pol sum_8 = alu_u8_r0;
pol sum_16 = sum_8 + alu_u8_r1 * 2**8;
pol sum_32 = sum_16 + alu_u16_r0 * 2**16;
pol sum_64 = sum_32 + alu_u16_r1 * 2**32 + alu_u16_r2 * 2**48;
pol sum_96 = sum_64 + alu_u16_r3 * 2**64 + alu_u16_r4 * 2**80;
pol sum_128 = sum_96 + alu_u16_r5 * 2**96 + alu_u16_r6 * 2**112;
pol SUM_8 = alu_u8_r0;
pol SUM_16 = SUM_8 + alu_u8_r1 * 2**8;
pol SUM_32 = SUM_16 + alu_u16_r0 * 2**16;
pol SUM_64 = SUM_32 + alu_u16_r1 * 2**32 + alu_u16_r2 * 2**48;
pol SUM_96 = SUM_64 + alu_u16_r3 * 2**64 + alu_u16_r4 * 2**80;
pol SUM_128 = SUM_96 + alu_u16_r5 * 2**96 + alu_u16_r6 * 2**112;

// ========= ADDITION/SUBTRACTION Operation Constraints ===============================
//
Expand All @@ -134,13 +135,13 @@ namespace aluChip(256);
// The second relation will consist in showing that sum_N - c = 0 for N = 8, 16, 32, 64, 128.

#[ALU_ADD_SUB_1]
(alu_op_add + alu_op_sub) * (sum_128 - alu_ia + alu_ff_tag * alu_ic) + (alu_op_add - alu_op_sub) * (alu_cf * 2**128 - alu_ib) = 0;
(alu_op_add + alu_op_sub) * (SUM_128 - alu_ia + alu_ff_tag * alu_ic) + (alu_op_add - alu_op_sub) * (alu_cf * 2**128 - alu_ib) = 0;

// Helper polynomial
pol sum_tag = alu_u8_tag * sum_8 + alu_u16_tag * sum_16 + alu_u32_tag * sum_32 + alu_u64_tag * sum_64 + alu_u128_tag * sum_128;
pol SUM_TAG = alu_u8_tag * SUM_8 + alu_u16_tag * SUM_16 + alu_u32_tag * SUM_32 + alu_u64_tag * SUM_64 + alu_u128_tag * SUM_128;

#[ALU_ADD_SUB_2]
(alu_op_add + alu_op_sub) * (sum_tag + alu_ff_tag * alu_ia - alu_ic) + alu_ff_tag * (alu_op_add - alu_op_sub) * alu_ib = 0;
(alu_op_add + alu_op_sub) * (SUM_TAG + alu_ff_tag * alu_ia - alu_ic) + alu_ff_tag * (alu_op_add - alu_op_sub) * alu_ib = 0;

// ========= MULTIPLICATION Operation Constraints ===============================

Expand All @@ -155,13 +156,13 @@ namespace aluChip(256);
// We group relations for u8, u16, u32, u64 together.

// Helper polynomial
pol sum_tag_no_128 = alu_u8_tag * sum_8 + alu_u16_tag * sum_16 + alu_u32_tag * sum_32 + alu_u64_tag * sum_64;
pol SUM_TAG_NO_128 = alu_u8_tag * SUM_8 + alu_u16_tag * SUM_16 + alu_u32_tag * SUM_32 + alu_u64_tag * SUM_64;

#[ALU_MUL_COMMON_1]
(1 - alu_ff_tag - alu_u128_tag) * alu_op_mul * (sum_128 - alu_ia * alu_ib) = 0;
(1 - alu_ff_tag - alu_u128_tag) * alu_op_mul * (SUM_128 - alu_ia * alu_ib) = 0;

#[ALU_MUL_COMMON_2]
alu_op_mul * (sum_tag_no_128 - (1 - alu_ff_tag - alu_u128_tag) * alu_ic) = 0;
alu_op_mul * (SUM_TAG_NO_128 - (1 - alu_ff_tag - alu_u128_tag) * alu_ic) = 0;

// ========= u128 MULTIPLICATION Operation Constraints ===============================
//
Expand All @@ -178,24 +179,48 @@ namespace aluChip(256);
// R' is stored in alu_u64_r0

// 64-bit lower limb
pol sum_low_64 = alu_u16_r0 + alu_u16_r1 * 2**16 + alu_u16_r2 * 2**32 + alu_u16_r3 * 2**48;
pol SUM_LOW_64 = alu_u16_r0 + alu_u16_r1 * 2**16 + alu_u16_r2 * 2**32 + alu_u16_r3 * 2**48;

// 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;
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_low_shifted_64 = alu_u16_r0' + alu_u16_r1' * 2**16 + alu_u16_r2' * 2**32 + alu_u16_r3' * 2**48;
pol SUM_LOW_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;
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_low_64 + sum_high_64 * 2**64 - alu_ia) = 0;
alu_u128_tag * alu_op_mul * (sum_low_shifted_64 + sum_high_shifted_64 * 2**64 - alu_ib) = 0;
alu_u128_tag * alu_op_mul * (SUM_LOW_64 + SUM_HIGH_64 * 2**64 - alu_ia) = 0;
alu_u128_tag * alu_op_mul * (SUM_LOW_SHIFTED_64 + SUM_HIGH_SHIFTED_64 * 2**64 - alu_ib) = 0;
#[ALU_MULTIPLICATION_OUT_U128]
alu_u128_tag * alu_op_mul * (
alu_ia * sum_low_shifted_64
+ sum_low_64 * sum_high_shifted_64 * 2**64
alu_ia * SUM_LOW_SHIFTED_64
+ SUM_LOW_64 * SUM_HIGH_SHIFTED_64 * 2**64
- (alu_cf * 2**64 + alu_u64_r0) * 2**128
- alu_ic
) = 0;

// ========= BITWISE NOT Operation Constraints ===============================
// Constrain mem_tag to not be FF (BITWISE NOT doesn't make sense for FF)
// TODO decide if it is done here or in another trace

// Do not allow alu_ff_tag to be set if we are doing bitwise
pol BITWISE_SEL = alu_op_not; // Add more bitwise operations
#[ALU_FF_NOT_XOR]
BITWISE_SEL * alu_ff_tag = 0;

// The value 2^k - 1
pol UINT_MAX = alu_u8_tag * 2**8 +
alu_u16_tag * 2**16 +
alu_u32_tag * 2**32 +
alu_u64_tag * 2**64 +
alu_u128_tag * 2**128 - 1;

// BITWISE NOT relation is: a + ~a = 2^k - 1
// Or (a + ~a - 2^k + 1) = 0;
// value of "a" stored in alu_ia and "~a" stored in alu_ic
#[ALU_OP_NOT]
alu_op_not * (alu_ia + alu_ic - UINT_MAX) = 0;


5 changes: 4 additions & 1 deletion barretenberg/cpp/pil/avm/avm_mini.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,8 @@ namespace avmMini(256);
pol commit sel_op_mul;
// DIV
pol commit sel_op_div;
// NOT
pol commit sel_op_not;

// Instruction memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
pol commit in_tag;
Expand Down Expand Up @@ -79,6 +81,7 @@ namespace avmMini(256);
sel_op_sub * (1 - sel_op_sub) = 0;
sel_op_mul * (1 - sel_op_mul) = 0;
sel_op_div * (1 - sel_op_div) = 0;
sel_op_not * (1 - sel_op_not) = 0;

sel_internal_call * (1 - sel_internal_call) = 0;
sel_internal_return * (1 - sel_internal_return) = 0;
Expand Down Expand Up @@ -172,7 +175,7 @@ namespace avmMini(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);
pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul + sel_op_not);

// Program counter must increment if not jumping or returning
#[PC_INCREMENT]
Expand Down
Loading

0 comments on commit 3a7d31b

Please sign in to comment.