Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: equality avm circuit #4595

Merged
merged 2 commits into from
Feb 14, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading