Skip to content

Commit

Permalink
feat: equality avm circuit
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyasRidhuan committed Feb 13, 2024
1 parent a7889f8 commit 8378489
Show file tree
Hide file tree
Showing 20 changed files with 2,948 additions and 210 deletions.
24 changes: 24 additions & 0 deletions barretenberg/cpp/pil/avm/avm_alu.pil
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ namespace avm_alu(256);
pol commit alu_op_mul;
pol commit alu_op_div;
pol commit alu_op_not;
pol commit alu_op_eq;

// Flattened boolean instruction tags
pol commit alu_ff_tag;
Expand Down Expand Up @@ -223,4 +224,27 @@ namespace avm_alu(256);
#[ALU_OP_NOT]
alu_op_not * (alu_ia + alu_ic - UINT_MAX) = 0;

// ========= EQUALITY Operation Constraints ===============================
// Equality of two elements is found by performing an "equality to zero" check.
// This relies on the fact than the inverse of a field element exists for all elements except zero
// 1) Given two values a & b, find the difference c = a - b
// 2) If a & b are equal, c == 0 otherwise c != 0
// 3) Field equality to zero can be done as follows
// a) c(e(1 - y) + y) - 1 + e = 0;
// b) where y = c^-1 and e is a boolean value indicating if c == 0
// c) if e == 0; cy = 1 && c has an inverse. if e ==1; c = 0 and we set c_inv = 0;

// Registers Ia and Ib hold the values that equality is to be tested on
pol DIFF = alu_ia - alu_ib;

// Need an additional helper that holds the inverse of the difference;
pol commit alu_op_eq_diff_inv;

// If EQ selector is set, ic needs to be boolean
#[ALU_RES_IS_BOOL]
alu_op_eq * (alu_ic * (1 - alu_ic)) = 0;

#[ALU_OP_EQ]
alu_op_eq * (DIFF * (alu_ic * (1 - alu_op_eq_diff_inv) + alu_op_eq_diff_inv) - 1 + alu_ic) = 0;


7 changes: 5 additions & 2 deletions barretenberg/cpp/pil/avm/avm_main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ namespace avm_main(256);
pol commit sel_op_div;
// NOT
pol commit sel_op_not;
// EQ
pol commit sel_op_eq;

// 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 @@ -64,7 +66,7 @@ namespace avm_main(256);
pol commit rwc;

// Memory index involved into a memory operation per pertaining intermediate register
// We should range constrain it to 32 bits ultimately. For first mini-AVM,
// We should range constrain it to 32 bits ultimately. For first version of the AVM,
// we will assume that these columns are of the right type.
pol commit mem_idx_a;
pol commit mem_idx_b;
Expand All @@ -82,6 +84,7 @@ namespace avm_main(256);
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_op_eq * (1 - sel_op_eq) = 0;

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

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

0 comments on commit 8378489

Please sign in to comment.