Skip to content

Commit

Permalink
feat: equality avm circuit (#4595)
Browse files Browse the repository at this point in the history
Avm equality circuit

---------

Co-authored-by: Ilyas Ridhuan <ilyas@aztecprotocol.com>
  • Loading branch information
IlyasRidhuan and IlyasRidhuan committed Feb 14, 2024
1 parent 382626c commit aad7b45
Show file tree
Hide file tree
Showing 20 changed files with 2,972 additions and 201 deletions.
28 changes: 28 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,31 @@ namespace avm_alu(256);
#[ALU_OP_NOT]
alu_op_not * (alu_ia + alu_ic - UINT_MAX) = 0;

// ========= EQUALITY Operation Constraints ===============================
// TODO: Note this method differs from the approach taken for "equality to zero" checks
// in handling the error tags found in avm_main and avm_mem files. The predicted relation difference
// is minor and when we optimise we will harmonise the methods based on actual performance.

// Equality of two elements is found by performing an "equality to zero" check.
// This relies on the fact that the inverse of a field element exists for all elements except zero
// 1) Given two values x & y, find the difference z = x - y
// 2) If x & y are equal, z == 0 otherwise z != 0
// 3) Field equality to zero can be done as follows
// a) z(e(x - w) + w) - 1 + e = 0;
// b) where w = z^-1 and e is a boolean value indicating if z == 0
// c) if e == 0; zw = 1 && z has an inverse. If e == 1; z == 0 and we set w = 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 aad7b45

Please sign in to comment.