Skip to content

Commit

Permalink
feat(avm): non-field sized cmp circuit ops (#9895)
Browse files Browse the repository at this point in the history
Please read [contributing guidelines](CONTRIBUTING.md) and remove this
line.
  • Loading branch information
IlyasRidhuan authored Nov 12, 2024
1 parent 8d49e59 commit 59376d4
Show file tree
Hide file tree
Showing 24 changed files with 1,147 additions and 959 deletions.
12 changes: 8 additions & 4 deletions barretenberg/cpp/pil/avm/alu.pil
Original file line number Diff line number Diff line change
Expand Up @@ -84,17 +84,21 @@ namespace alu(256);
pol commit cmp_gadget_input_b;
pol commit cmp_gadget_result;
pol commit cmp_gadget_gt;
pol commit cmp_gadget_non_ff_gt;

// We use the comparison gadget to test GT for the following operations
cmp_gadget_gt = op_lt + op_lte + op_div + op_shr + op_shl;
pol CMP_GADGET_GT = op_lt + op_lte + op_div + op_shr + op_shl;
cmp_gadget_gt = CMP_GADGET_GT * ff_tag;
cmp_gadget_non_ff_gt = CMP_GADGET_GT * (1 - ff_tag);

// The cmp gadget is on when we are either testing GT or EQ
cmp_gadget_sel - (cmp_gadget_gt + op_eq) = 0;
cmp_gadget_sel - (cmp_gadget_gt + op_eq + cmp_gadget_non_ff_gt) = 0;

// Permutation to the Comparison Gadget
#[PERM_CMP_ALU]
cmp.sel_cmp {cmp.clk, cmp.input_a, cmp.input_b, cmp.result, cmp.op_eq, cmp.op_gt}
cmp.sel_cmp {cmp.clk, cmp.input_a, cmp.input_b, cmp.result, cmp.op_eq, cmp.op_gt, cmp.op_non_ff_gt}
is
cmp_gadget_sel {clk, cmp_gadget_input_a, cmp_gadget_input_b, cmp_gadget_result, op_eq, cmp_gadget_gt };
cmp_gadget_sel {clk, cmp_gadget_input_a, cmp_gadget_input_b, cmp_gadget_result, op_eq, cmp_gadget_gt, cmp_gadget_non_ff_gt };


// =============== HELPER POLYNOMIAL RELATIONS =================================================
Expand Down
21 changes: 20 additions & 1 deletion barretenberg/cpp/pil/avm/gadgets/cmp.pil
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,25 @@ namespace cmp(256);
pol commit input_b;
pol commit result;

// ========= NON FF GT Short-circuit computation ===============================
// If this is a non-ff check, we can short circuit (a > b) by checking
// 0 < a - b - 1 < 2**128 --> i.e. we just check we dont underlow which for "small" sized 128-bit number is just a
// single 128 bit range check
// This will be constrained by the calling function - maybe through instruction decomposition
pol commit op_non_ff_gt;
// Value of a - b
pol commit diff;

pol A_GT_B = input_a - input_b - 1;
pol B_GTE_A = input_b - input_a;
op_non_ff_gt * (diff - (A_GT_B * result) - (B_GTE_A * (1 - result))) = 0;

#[PERM_RNG_NON_FF_CMP]
range_check.cmp_non_ff_rng_chk {range_check.clk, range_check.value}
is
op_non_ff_gt {range_chk_clk, diff};

// ========= FF GT computation ===============================
// We range check two columns per row of the cmp gadget, the lo and hi bit ranges resp.
#[PERM_RNG_CMP_LO]
range_check.cmp_lo_bits_rng_chk {range_check.clk, range_check.value}
Expand All @@ -32,7 +51,7 @@ namespace cmp(256);
pol commit op_eq;
pol commit op_gt;

sel_cmp = op_eq + op_gt;
sel_cmp = op_eq + op_gt + op_non_ff_gt;

// There are some standardised constraints on this gadget
// The result is always a boolean
Expand Down
3 changes: 3 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/range_check.pil
Original file line number Diff line number Diff line change
Expand Up @@ -201,6 +201,9 @@ namespace range_check(256);
// We range check 128 bits in the cmp trace
cmp_lo_bits_rng_chk * (rng_chk_bits - 128) = 0;
cmp_hi_bits_rng_chk * (rng_chk_bits - 128) = 0;
// For non FF
pol commit cmp_non_ff_rng_chk;
cmp_non_ff_rng_chk * (rng_chk_bits - 128) = 0;

// ==== ALU TRACE RANGE CHECKS ====
pol commit alu_rng_chk;
1 change: 0 additions & 1 deletion barretenberg/cpp/pil/avm/gas.pil
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,6 @@ namespace main(256);
// We range check that the absolute value of the differences between each row of l2 and da gas are 32 bits.
pol commit l2_gas_u16_r0;
pol commit l2_gas_u16_r1;
// Do we need DA?
main.abs_l2_rem_gas = l2_gas_u16_r0 + l2_gas_u16_r1 * 2**16;

#[LOOKUP_L2_GAS_RNG_CHK_0]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -139,6 +139,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.alu_cmp_gadget_gt.set_if_valid_index(i, rows[i].alu_cmp_gadget_gt);
polys.alu_cmp_gadget_input_a.set_if_valid_index(i, rows[i].alu_cmp_gadget_input_a);
polys.alu_cmp_gadget_input_b.set_if_valid_index(i, rows[i].alu_cmp_gadget_input_b);
polys.alu_cmp_gadget_non_ff_gt.set_if_valid_index(i, rows[i].alu_cmp_gadget_non_ff_gt);
polys.alu_cmp_gadget_result.set_if_valid_index(i, rows[i].alu_cmp_gadget_result);
polys.alu_cmp_gadget_sel.set_if_valid_index(i, rows[i].alu_cmp_gadget_sel);
polys.alu_ff_tag.set_if_valid_index(i, rows[i].alu_ff_tag);
Expand Down Expand Up @@ -218,11 +219,13 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.cmp_borrow.set_if_valid_index(i, rows[i].cmp_borrow);
polys.cmp_clk.set_if_valid_index(i, rows[i].cmp_clk);
polys.cmp_cmp_rng_ctr.set_if_valid_index(i, rows[i].cmp_cmp_rng_ctr);
polys.cmp_diff.set_if_valid_index(i, rows[i].cmp_diff);
polys.cmp_input_a.set_if_valid_index(i, rows[i].cmp_input_a);
polys.cmp_input_b.set_if_valid_index(i, rows[i].cmp_input_b);
polys.cmp_op_eq.set_if_valid_index(i, rows[i].cmp_op_eq);
polys.cmp_op_eq_diff_inv.set_if_valid_index(i, rows[i].cmp_op_eq_diff_inv);
polys.cmp_op_gt.set_if_valid_index(i, rows[i].cmp_op_gt);
polys.cmp_op_non_ff_gt.set_if_valid_index(i, rows[i].cmp_op_non_ff_gt);
polys.cmp_p_a_borrow.set_if_valid_index(i, rows[i].cmp_p_a_borrow);
polys.cmp_p_b_borrow.set_if_valid_index(i, rows[i].cmp_p_b_borrow);
polys.cmp_p_sub_a_hi.set_if_valid_index(i, rows[i].cmp_p_sub_a_hi);
Expand Down Expand Up @@ -760,6 +763,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.range_check_clk.set_if_valid_index(i, rows[i].range_check_clk);
polys.range_check_cmp_hi_bits_rng_chk.set_if_valid_index(i, rows[i].range_check_cmp_hi_bits_rng_chk);
polys.range_check_cmp_lo_bits_rng_chk.set_if_valid_index(i, rows[i].range_check_cmp_lo_bits_rng_chk);
polys.range_check_cmp_non_ff_rng_chk.set_if_valid_index(i, rows[i].range_check_cmp_non_ff_rng_chk);
polys.range_check_dyn_diff.set_if_valid_index(i, rows[i].range_check_dyn_diff);
polys.range_check_dyn_rng_chk_bits.set_if_valid_index(i, rows[i].range_check_dyn_rng_chk_bits);
polys.range_check_dyn_rng_chk_pow_2.set_if_valid_index(i, rows[i].range_check_dyn_rng_chk_pow_2);
Expand Down
Loading

0 comments on commit 59376d4

Please sign in to comment.