Skip to content

Commit

Permalink
refactor(avm): separate alu finalization
Browse files Browse the repository at this point in the history
  • Loading branch information
fcarreiro committed Aug 20, 2024
1 parent 5bff26b commit 62a3b79
Show file tree
Hide file tree
Showing 10 changed files with 568 additions and 645 deletions.
91 changes: 91 additions & 0 deletions barretenberg/cpp/pil/avm/alu.pil
Original file line number Diff line number Diff line change
Expand Up @@ -733,3 +733,94 @@ namespace alu(256);
pol NEXT_SUM_128_HI = u16_r3' + u16_r4' * 2**16 + u16_r5' * 2**32 + u16_r6' * 2**48;
partial_prod_lo = op_div_std * NEXT_SUM_64_LO;
partial_prod_hi = op_div_std * NEXT_SUM_128_HI;

//====== Inter-table Shift Constraints (Lookups) ============================================
// Currently only used for shift operations but can be generalised for other uses.

// Lookup for 2**(ib)
#[LOOKUP_POW_2_0]
sel_shift_which {ib, two_pow_s} in main.sel_rng_8 {main.clk, powers.power_of_2};

// Lookup for 2**(t-ib)
#[LOOKUP_POW_2_1]
sel_shift_which {t_sub_s_bits ,two_pow_t_sub_s} in main.sel_rng_8 {main.clk, powers.power_of_2};

//====== Inter-table Constraints (Range Checks) ============================================
// TODO: Investigate optimising these range checks. Handling non-FF elements should require less range checks.
// One can increase the granularity based on the operation and tag. In the most extreme case,
// a specific selector per register might be introduced.
#[LOOKUP_U8_0]
sel_rng_chk_lookup { u8_r0 } in main.sel_rng_8 { main.clk };

#[LOOKUP_U8_1]
sel_rng_chk_lookup { u8_r1 } in main.sel_rng_8 { main.clk };

#[LOOKUP_U16_0]
sel_rng_chk_lookup { u16_r0 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_1]
sel_rng_chk_lookup { u16_r1 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_2]
sel_rng_chk_lookup { u16_r2 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_3]
sel_rng_chk_lookup { u16_r3 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_4]
sel_rng_chk_lookup { u16_r4 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_5]
sel_rng_chk_lookup { u16_r5 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_6]
sel_rng_chk_lookup { u16_r6 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_7]
sel_rng_chk_lookup { u16_r7 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_8]
sel_rng_chk_lookup { u16_r8 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_9]
sel_rng_chk_lookup { u16_r9 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_10]
sel_rng_chk_lookup { u16_r10 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_11]
sel_rng_chk_lookup { u16_r11 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_12]
sel_rng_chk_lookup { u16_r12 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_13]
sel_rng_chk_lookup { u16_r13 } in main.sel_rng_16 { main.clk };

#[LOOKUP_U16_14]
sel_rng_chk_lookup { u16_r14 } in main.sel_rng_16 { main.clk };

// ==== Additional row range checks for division
#[LOOKUP_DIV_U16_0]
sel_div_rng_chk { div_u16_r0 } in main.sel_rng_16 { main.clk };

#[LOOKUP_DIV_U16_1]
sel_div_rng_chk { div_u16_r1 } in main.sel_rng_16 { main.clk };

#[LOOKUP_DIV_U16_2]
sel_div_rng_chk { div_u16_r2 } in main.sel_rng_16 { main.clk };

#[LOOKUP_DIV_U16_3]
sel_div_rng_chk { div_u16_r3 } in main.sel_rng_16 { main.clk };

#[LOOKUP_DIV_U16_4]
sel_div_rng_chk { div_u16_r4 } in main.sel_rng_16 { main.clk };

#[LOOKUP_DIV_U16_5]
sel_div_rng_chk { div_u16_r5 } in main.sel_rng_16 { main.clk };

#[LOOKUP_DIV_U16_6]
sel_div_rng_chk { div_u16_r6 } in main.sel_rng_16 { main.clk };

#[LOOKUP_DIV_U16_7]
sel_div_rng_chk { div_u16_r7 } in main.sel_rng_16 { main.clk };
91 changes: 0 additions & 91 deletions barretenberg/cpp/pil/avm/main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -628,94 +628,3 @@ namespace main(256);

#[LOOKUP_MEM_RNG_CHK_HI]
mem.sel_rng_chk {mem.diff_hi} in sel_rng_8 {clk};

//====== Inter-table Shift Constraints (Lookups) ============================================
// Currently only used for shift operations but can be generalised for other uses.

// Lookup for 2**(ib)
#[LOOKUP_POW_2_0]
alu.sel_shift_which {alu.ib, alu.two_pow_s} in sel_rng_8 {clk, powers.power_of_2};

// Lookup for 2**(t-ib)
#[LOOKUP_POW_2_1]
alu.sel_shift_which {alu.t_sub_s_bits , alu.two_pow_t_sub_s} in sel_rng_8 {clk, powers.power_of_2};

//====== Inter-table Constraints (Range Checks) ============================================
// TODO: Investigate optimising these range checks. Handling non-FF elements should require less range checks.
// One can increase the granularity based on the operation and tag. In the most extreme case,
// a specific selector per register might be introduced.
#[LOOKUP_U8_0]
alu.sel_rng_chk_lookup { alu.u8_r0 } in sel_rng_8 { clk };

#[LOOKUP_U8_1]
alu.sel_rng_chk_lookup { alu.u8_r1 } in sel_rng_8 { clk };

#[LOOKUP_U16_0]
alu.sel_rng_chk_lookup { alu.u16_r0 } in sel_rng_16 { clk };

#[LOOKUP_U16_1]
alu.sel_rng_chk_lookup { alu.u16_r1 } in sel_rng_16 { clk };

#[LOOKUP_U16_2]
alu.sel_rng_chk_lookup { alu.u16_r2 } in sel_rng_16 { clk };

#[LOOKUP_U16_3]
alu.sel_rng_chk_lookup { alu.u16_r3 } in sel_rng_16 { clk };

#[LOOKUP_U16_4]
alu.sel_rng_chk_lookup { alu.u16_r4 } in sel_rng_16 { clk };

#[LOOKUP_U16_5]
alu.sel_rng_chk_lookup { alu.u16_r5 } in sel_rng_16 { clk };

#[LOOKUP_U16_6]
alu.sel_rng_chk_lookup { alu.u16_r6 } in sel_rng_16 { clk };

#[LOOKUP_U16_7]
alu.sel_rng_chk_lookup { alu.u16_r7 } in sel_rng_16 { clk };

#[LOOKUP_U16_8]
alu.sel_rng_chk_lookup { alu.u16_r8 } in sel_rng_16 { clk };

#[LOOKUP_U16_9]
alu.sel_rng_chk_lookup { alu.u16_r9 } in sel_rng_16 { clk };

#[LOOKUP_U16_10]
alu.sel_rng_chk_lookup { alu.u16_r10 } in sel_rng_16 { clk };

#[LOOKUP_U16_11]
alu.sel_rng_chk_lookup { alu.u16_r11 } in sel_rng_16 { clk };

#[LOOKUP_U16_12]
alu.sel_rng_chk_lookup { alu.u16_r12 } in sel_rng_16 { clk };

#[LOOKUP_U16_13]
alu.sel_rng_chk_lookup { alu.u16_r13 } in sel_rng_16 { clk };

#[LOOKUP_U16_14]
alu.sel_rng_chk_lookup { alu.u16_r14 } in sel_rng_16 { clk };

// ==== Additional row range checks for division
#[LOOKUP_DIV_U16_0]
alu.sel_div_rng_chk { alu.div_u16_r0 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_1]
alu.sel_div_rng_chk { alu.div_u16_r1 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_2]
alu.sel_div_rng_chk { alu.div_u16_r2 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_3]
alu.sel_div_rng_chk { alu.div_u16_r3 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_4]
alu.sel_div_rng_chk { alu.div_u16_r4 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_5]
alu.sel_div_rng_chk { alu.div_u16_r5 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_6]
alu.sel_div_rng_chk { alu.div_u16_r6 } in sel_rng_16 { clk };

#[LOOKUP_DIV_U16_7]
alu.sel_div_rng_chk { alu.div_u16_r7 } in sel_rng_16 { clk };
Original file line number Diff line number Diff line change
Expand Up @@ -627,22 +627,6 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.slice_sel_start[i] = rows[i].slice_sel_start;
polys.slice_space_id[i] = rows[i].slice_space_id;
polys.slice_val[i] = rows[i].slice_val;
polys.lookup_byte_lengths_counts[i] = rows[i].lookup_byte_lengths_counts;
polys.lookup_byte_operations_counts[i] = rows[i].lookup_byte_operations_counts;
polys.lookup_opcode_gas_counts[i] = rows[i].lookup_opcode_gas_counts;
polys.range_check_l2_gas_hi_counts[i] = rows[i].range_check_l2_gas_hi_counts;
polys.range_check_l2_gas_lo_counts[i] = rows[i].range_check_l2_gas_lo_counts;
polys.range_check_da_gas_hi_counts[i] = rows[i].range_check_da_gas_hi_counts;
polys.range_check_da_gas_lo_counts[i] = rows[i].range_check_da_gas_lo_counts;
polys.kernel_output_lookup_counts[i] = rows[i].kernel_output_lookup_counts;
polys.lookup_into_kernel_counts[i] = rows[i].lookup_into_kernel_counts;
polys.lookup_cd_value_counts[i] = rows[i].lookup_cd_value_counts;
polys.lookup_ret_value_counts[i] = rows[i].lookup_ret_value_counts;
polys.incl_main_tag_err_counts[i] = rows[i].incl_main_tag_err_counts;
polys.incl_mem_tag_err_counts[i] = rows[i].incl_mem_tag_err_counts;
polys.lookup_mem_rng_chk_lo_counts[i] = rows[i].lookup_mem_rng_chk_lo_counts;
polys.lookup_mem_rng_chk_mid_counts[i] = rows[i].lookup_mem_rng_chk_mid_counts;
polys.lookup_mem_rng_chk_hi_counts[i] = rows[i].lookup_mem_rng_chk_hi_counts;
polys.lookup_pow_2_0_counts[i] = rows[i].lookup_pow_2_0_counts;
polys.lookup_pow_2_1_counts[i] = rows[i].lookup_pow_2_1_counts;
polys.lookup_u8_0_counts[i] = rows[i].lookup_u8_0_counts;
Expand Down Expand Up @@ -670,6 +654,22 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.lookup_div_u16_5_counts[i] = rows[i].lookup_div_u16_5_counts;
polys.lookup_div_u16_6_counts[i] = rows[i].lookup_div_u16_6_counts;
polys.lookup_div_u16_7_counts[i] = rows[i].lookup_div_u16_7_counts;
polys.lookup_byte_lengths_counts[i] = rows[i].lookup_byte_lengths_counts;
polys.lookup_byte_operations_counts[i] = rows[i].lookup_byte_operations_counts;
polys.lookup_opcode_gas_counts[i] = rows[i].lookup_opcode_gas_counts;
polys.range_check_l2_gas_hi_counts[i] = rows[i].range_check_l2_gas_hi_counts;
polys.range_check_l2_gas_lo_counts[i] = rows[i].range_check_l2_gas_lo_counts;
polys.range_check_da_gas_hi_counts[i] = rows[i].range_check_da_gas_hi_counts;
polys.range_check_da_gas_lo_counts[i] = rows[i].range_check_da_gas_lo_counts;
polys.kernel_output_lookup_counts[i] = rows[i].kernel_output_lookup_counts;
polys.lookup_into_kernel_counts[i] = rows[i].lookup_into_kernel_counts;
polys.lookup_cd_value_counts[i] = rows[i].lookup_cd_value_counts;
polys.lookup_ret_value_counts[i] = rows[i].lookup_ret_value_counts;
polys.incl_main_tag_err_counts[i] = rows[i].incl_main_tag_err_counts;
polys.incl_mem_tag_err_counts[i] = rows[i].incl_mem_tag_err_counts;
polys.lookup_mem_rng_chk_lo_counts[i] = rows[i].lookup_mem_rng_chk_lo_counts;
polys.lookup_mem_rng_chk_mid_counts[i] = rows[i].lookup_mem_rng_chk_mid_counts;
polys.lookup_mem_rng_chk_hi_counts[i] = rows[i].lookup_mem_rng_chk_hi_counts;
}

for (auto [shifted, to_be_shifted] : zip_view(polys.get_shifted(), polys.get_to_be_shifted())) {
Expand Down
Loading

0 comments on commit 62a3b79

Please sign in to comment.