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.

Sign up for GitHub

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(avm): ALU <--> MAIN inter table relation on intermediate registers copy #4945

Merged
merged 4 commits into from
Mar 6, 2024
+836 −527
Merged

feat(avm): ALU <--> MAIN inter table relation on intermediate registers copy #4945

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
65ff9d6
4613 - enable permutation check for intermediate registers between ALU
jeanmon Feb 22, 2024
bbaa91b
4613 - remove constrain on intermediate registers set to zero in case of
jeanmon Mar 5, 2024
bf3b50c
4613 - add in_tag and operator selectors in permutation
jeanmon Mar 5, 2024
adfff6f
4613 - fix bug in return_op
jeanmon Mar 6, 2024
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
22 changes: 14 additions & 8 deletions barretenberg/cpp/pil/avm/avm_alu.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,10 @@ namespace avm_alu(256);
pol commit alu_op_div;
pol commit alu_op_not;
pol commit alu_op_eq;
pol commit alu_sel; // 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
pol commit alu_in_tag;

// Flattened boolean instruction tags
pol commit alu_ff_tag;
Expand Down Expand Up @@ -46,6 +50,9 @@ namespace avm_alu(256);
// Carry flag
pol commit alu_cf;

// Compute predicate telling whether there is a row entry in the ALU table.
alu_sel = alu_op_add + alu_op_sub + alu_op_mul + alu_op_not + alu_op_eq;

// ========= Type Constraints =============================================
// TODO: Range constraints
// - for slice registers
Expand All @@ -54,7 +61,6 @@ namespace avm_alu(256);
// Carry flag: We will have to constraint to ensure that the
// arithmetic expressions are not overflowing finite field size
// Remark: Operation selectors are constrained in the main trace.
// TODO: Enforce the equivalence check for the selectors between both tables.

// Boolean flattened instructions tags
alu_ff_tag * (1 - alu_ff_tag) = 0;
Expand All @@ -64,17 +70,17 @@ namespace avm_alu(256);
alu_u64_tag * (1 - alu_u64_tag) = 0;
alu_u128_tag * (1 - alu_u128_tag) = 0;

// Mutual exclusion of the flattened instruction tag.
alu_sel * (alu_ff_tag + alu_u8_tag + alu_u16_tag + alu_u32_tag + alu_u64_tag + alu_u128_tag - 1) = 0;

// Correct flattening of the instruction tag.
alu_in_tag = alu_u8_tag + 2 * alu_u16_tag + 3 * alu_u32_tag + 4 * alu_u64_tag + 5 * alu_u128_tag + 6 * alu_ff_tag;

// Operation selectors are copied from main table and do not need to be constrained here.
// TODO: Ensure mutual exclusion of alu_op_add and alu_op_sub as some relations below
// requires it.
// TODO: Similarly, ensure the mutual exclusion of instruction tags

// ========= Inter-table Constraints ======================================
// TODO: Equivalence between intermediate registers, clk, type flag, operation
// An ALU chiplet flag will be introduced in main trace to select relevant rows.


// ========= EXPLANATIONS =================================================
// ========= ARITHMETIC OPERATION - EXPLANATIONS =================================================
// Main trick for arithmetic operations modulo 2^k is to perform the operation
// over the integers and expressing the result as low + high * 2^k with low
// smaller than 2^k. low is used as the output. This works as long this does
Expand Down
24 changes: 18 additions & 6 deletions barretenberg/cpp/pil/avm/avm_main.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,10 @@ namespace avm_main(256);
// EQ
pol commit sel_op_eq;

// Instruction memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
// Helper selector to characterize an ALU chiplet selector
pol commit alu_sel;

// Instruction memory tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field)
pol commit in_tag;

// Errors
Expand Down Expand Up @@ -104,11 +107,6 @@ namespace avm_main(256);

// TODO: Constrain rwa, rwb, rwc to u32 type and 0 <= in_tag <= 6

// Set intermediate registers to 0 whenever tag_err occurs
tag_err * ia = 0;
tag_err * ib = 0;
tag_err * ic = 0;

// Relation for division over the finite field
// If tag_err == 1 in a division, then ib == 0 and op_err == 1.
#[SUBOP_DIVISION_FF]
Expand Down Expand Up @@ -195,5 +193,19 @@ namespace avm_main(256);
#[equiv_tag_err]
avm_mem.m_tag_err {avm_mem.m_clk} in tag_err {clk};

// Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1,
// the operation is not copied to the ALU table.
// TODO: when division is moved to the alu, we will need to add the selector in the list below:
alu_sel = (sel_op_add + sel_op_sub + sel_op_mul + sel_op_not + sel_op_eq) * (1 - tag_err);

#[equiv_inter_reg_alu]
alu_sel {clk, ia, ib, ic,
sel_op_add, sel_op_sub, sel_op_mul, sel_op_eq,
sel_op_not, in_tag}
is
avm_alu.alu_sel {avm_alu.alu_clk, avm_alu.alu_ia, avm_alu.alu_ib, avm_alu.alu_ic,
avm_alu.alu_op_add, avm_alu.alu_op_sub, avm_alu.alu_op_mul, avm_alu.alu_op_eq,
avm_alu.alu_op_not, avm_alu.alu_in_tag};

// TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like:
// mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}
Loading
Loading