Skip to content

Commit

Permalink
feat(avm): integrate new range and cmp gadgets (#8165)
Browse files Browse the repository at this point in the history 
```
time AVM_ENABLE_FULL_PROVING=1 ./bb avm_prove --avm-bytecode /tmp/bb-dY93DM/tmp-ygXEjA/avm_bytecode.bin --avm-calldata /tmp/bb-dY93DM/tmp-ygXEjA/avm_calldata.bin --avm-public-inputs /tmp/bb-dY93DM/tmp-ygXEjA/avm_public_inputs.bin --avm-hints /tmp/bb-dY93DM/tmp-ygXEjA/avm_hints.bin -o /tmp/bb-dY93DM/tmp-ygXEjA/ -v
bb command is: avm_prove
bytecode size: 38126
calldata size: 6
public_inputs size: 691
hints.storage_value_hints size: 2
hints.note_hash_exists_hints size: 0
hints.nullifier_exists_hints size: 1
hints.l1_to_l2_message_exists_hints size: 0
hints.externalcall_hints size: 0
hints.contract_instance_hints size: 0
initializing crs with size: 1048576
using cached crs of size 33554433 at "/mnt/user-data/ilyas/.bb-crs/bn254_g1.dat"
Deserialized 3322 instructions
------- GENERATING TRACE -------
Trace sizes before padding:
        main_trace_size: 65535
        mem_trace_size: 2084
        alu_trace_size: 410
        range_check_size: 65536
        conv_trace_size: 1
        bin_trace_size: 0
        sha256_trace_size: 0
        poseidon2_trace_size: 0
        pedersen_trace_size: 4
        gas_trace_size: 890
        fixed_gas_table_size: 66
        slice_trace_size: 7
        range_check_trace_size: 4266
        cmp_trace_size: 39
Built trace size: 65536
Number of columns: 696
Number of non-zero elements: 236111/45613056 (0%)
Relation degrees:
        alu: [5°: 2, 4°: 6, 3°: 11, 2°: 24, 1°: 5]
        binary: [3°: 1, 2°: 9]
        cmp: [4°: 3, 3°: 1, 2°: 21, 1°: 2]
        conversion: [2°: 1]
        gas: [4°: 2, 3°: 2, 2°: 2]
        keccakf1600: [2°: 1]
        kernel: [3°: 3, 2°: 41]
        main: [4°: 3, 3°: 7, 2°: 101, 1°: 3]
        mem: [5°: 1, 3°: 8, 2°: 41, 1°: 2]
        mem_slice: [3°: 3, 2°: 7, 1°: 1]
        pedersen: [2°: 1]
        poseidon2: [6°: 256, 2°: 17]
        range_check: [3°: 1, 2°: 15, 1°: 9]
        sha256: [2°: 1]
Trace size after padding: 2^16
------- PROVING EXECUTION -------
vk fields size: 66
circuit size: 0x0000000000000000000000000000000000000000000000000000000000010000
num of pub inputs: 0x0000000000000000000000000000000000000000000000000000000000000000
proof written to: "/tmp/bb-dY93DM/tmp-ygXEjA/proof"
vk written to: "/tmp/bb-dY93DM/tmp-ygXEjA/vk"
vk as fields written to: "/tmp/bb-dY93DM/tmp-ygXEjA/vk_fields.json"
------- STATS -------
prove/all_ms: 6953
prove/create_composer_ms: 0
prove/create_prover_ms: 1988
prove/create_verifier_ms: 41
prove/execute_log_derivative_inverse_commitments_round_ms: 344
prove/execute_log_derivative_inverse_round_ms: 205
prove/execute_pcs_rounds_ms: 760
prove/execute_relation_check_rounds_ms: 727
prove/execute_wire_commitments_round_ms: 616
prove/gen_trace_ms: 2150

AVM_ENABLE_FULL_PROVING=1 ./bb avm_prove --avm-bytecode  --avm-calldata        71.13s user 69.17s system 1579% cpu 8.882 total
```
  • Loading branch information
@IlyasRidhuan
IlyasRidhuan authored Aug 29, 2024
1 parent bf7a99d commit 2e1be18
Show file tree
Hide file tree
Showing 59 changed files with 3,012 additions and 5,741 deletions.
966 changes: 212 additions & 754 deletions barretenberg/cpp/pil/avm/alu.pil
View file

Large diffs are not rendered by default.

238 changes: 238 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/cmp.pil
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,238 @@
include "./range_check.pil";
// This module handles comparisons (equality and GT)
// GT also enables us to support LT (by swapping the inputs of GT) and LTE (by inverting the result of GT)

// TODO: See if we can make this faster for non-FF GT ops

namespace cmp(256);
pol commit clk;

// ========= Initialize Range Check Gadget ===============================
// We need this as a unique key to the range check gadget
pol commit range_chk_clk;
sel_rng_chk * (range_chk_clk - (clk * 2**8 + cmp_rng_ctr)) = 0;
// These are the i/o for the gadget
pol commit input_a;
pol commit input_b;
pol commit result;

// 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}
is
sel_rng_chk {range_chk_clk, a_lo};

#[PERM_RNG_CMP_HI]
range_check.cmp_hi_bits_rng_chk {range_check.clk, range_check.value}
is
sel_rng_chk {range_chk_clk, a_hi};

// These are the selectors that will be useful
pol commit sel_cmp;
pol commit op_eq;
pol commit op_gt;

sel_cmp = op_eq + op_gt;

// There are some standardised constraints on this gadget
// The result is always a boolean
#[CMP_RES_IS_BOOL]
(result * (1 - result)) = 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 main and 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 input_a and input_b hold the values that equality is to be tested on
pol DIFF = input_a - input_b;

// Need an additional helper that holds the inverse of the difference;
pol commit op_eq_diff_inv;

#[CMP_OP_EQ]
op_eq * (DIFF * (result * (1 - op_eq_diff_inv) + op_eq_diff_inv) - 1 + result) = 0;


// ========= GT Operation Constraints ===============================
// There are two routines that we utilise as part of this GT check
// (1) Decomposition into two 128-bit limbs, lo and hi respectively and a borrow (1 or 0);
// (2) 128 bit-range checks when checking an arithmetic operation has not overflowed the field.

// ========= COMPARISON OPERATION - EXPLANATIONS =================================================
// To simplify the comparison circuit, we implement a GreaterThan(GT) circuit. This is ideal since
// if we need a LT operation, we just swap the inputs and if we need the LTE operation, we just NOT the GT constraint
// Given the inputs x, y and q where x & y are integers in the range [0,...,p-1] and q is the boolean result to the query (x > y).
// Then there are two scenarios:
// (1) (x > y) -> x - y - 1 = result, where 0 <= result. i.e. the result does not underflow the field.
// (2)!(x > y) -> (x <= y) = y - x = result, where the same applies as above.

// Check the result of input_a > input_b;
pol POW_128 = 2 ** 128;
pol P_LO = 53438638232309528389504892708671455232; // Lower 128 bits of (p - 1)
pol P_HI = 64323764613183177041862057485226039389; // Upper 128 bits of (p - 1)

pol commit borrow;
pol commit a_lo;
pol commit a_hi;
#[INPUT_DECOMP_1]
op_gt * ( input_a - (a_lo + POW_128 * a_hi)) = 0;

pol commit b_lo;
pol commit b_hi;
#[INPUT_DECOMP_2]
op_gt * ( input_b - (b_lo + POW_128 * b_hi)) = 0;

pol commit p_sub_a_lo; // p_lo - a_lo
pol commit p_sub_a_hi; // p_hi - a_hi
pol commit p_a_borrow;
p_a_borrow * (1 - p_a_borrow) = 0;

// Check that decomposition of a into lo and hi limbs do not overflow p.
// This is achieved by checking a does not underflow p: (p_lo > a_lo && p_hi >= ahi) || (p_lo <= a_lo && p_hi > a_hi)
// First condition is if borrow = 0, second condition is if borrow = 1
// This underflow check is done by the 128-bit check that is performed on each of these lo and hi limbs.
#[SUB_LO_1]
op_gt * (p_sub_a_lo - (P_LO - a_lo + p_a_borrow * POW_128)) = 0;
#[SUB_HI_1]
op_gt * (p_sub_a_hi - (P_HI - a_hi - p_a_borrow)) = 0;

pol commit p_sub_b_lo;
pol commit p_sub_b_hi;
pol commit p_b_borrow;
p_b_borrow * (1 - p_b_borrow) = 0;

// Check that decomposition of b into lo and hi limbs do not overflow/underflow p.
// This is achieved by checking (p_lo > b_lo && p_hi >= bhi) || (p_lo <= b_lo && p_hi > b_hi)
// First condition is if borrow = 0, second condition is if borrow = 1;
#[SUB_LO_2]
op_gt * (p_sub_b_lo - (P_LO - b_lo + p_b_borrow * POW_128)) = 0;
#[SUB_HI_2]
op_gt * (p_sub_b_hi - (P_HI - b_hi - p_b_borrow)) = 0;

// Calculate the combined relation: (a - b - 1) * q + (b -a ) * (1-q)
// Check that (a > b) by checking (a_lo > b_lo && a_hi >= bhi) || (alo <= b_lo && a_hi > b_hi)
// First condition is if borrow = 0, second condition is if borrow = 1;
pol A_SUB_B_LO = a_lo - b_lo - 1 + borrow * POW_128;
pol A_SUB_B_HI = a_hi - b_hi - borrow;

// Check that (a <= b) by checking (b_lo >= a_lo && b_hi >= a_hi) || (b_lo < a_lo && b_hi > a_hi)
// First condition is if borrow = 0, second condition is if borrow = 1;
pol B_SUB_A_LO = b_lo - a_lo + borrow * POW_128;
pol B_SUB_A_HI = b_hi - a_hi - borrow;

pol IS_GT = op_gt * result;
// When IS_GT = 1, we enforce the condition that a > b and thus a - b - 1 does not underflow.
// When IS_GT = 0, we enforce the condition that a <= b and thus b - a does not underflow.
// ========= Analysing res_lo and res_hi scenarios for LTE =================================
// (1) Assume a proof satisfies the constraints for LTE(x,y,1), i.e., x <= y
// Therefore ia = x, ib = y and ic = 1.
// (a) We do not swap the operands, so a = x and b = y,
// (b) IS_GT = 1 - ic = 0
// (c) res_lo = B_SUB_A_LO and res_hi = B_SUB_A_HI
// (d) res_lo = y_lo - x_lo + borrow * 2**128 and res_hi = y_hi - x_hi - borrow.
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> y_lo >= x_lo && y_hi >= x_hi
// (ii) borrow == 1 ==> y_hi >= x_hi + 1 ==> y_hi > x_hi
// This concludes the proof as for both cases, we must have: y >= x
//
// (2) Assume a proof satisfies the constraints for LTE(x,y,0), i.e. x > y.
// Therefore ia = x, ib = y and ic = 0.
// (a) We do not swap the operands, so a = x and b = y,
// (b) IS_GT = 1 - ic = 1
// (c) res_lo = A_SUB_B_LO and res_hi = A_SUB_B_HI
// (d) res_lo = x_lo - y_lo - 1 + borrow * 2**128 and res_hi = x_hi - y_hi - borrow.
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> x_lo > y_lo && x_hi >= y_hi
// (ii) borrow == 1 ==> x_hi > y_hi
// This concludes the proof as for both cases, we must have: x > y
//

// ========= Analysing res_lo and res_hi scenarios for LT ==================================
// (1) Assume a proof satisfies the constraints for LT(x,y,1), i.e. x < y.
// Therefore ia = x, ib = y and ic = 1.
// (a) We DO swap the operands, so a = y and b = x,
// (b) IS_GT = ic = 1
// (c) res_lo = A_SUB_B_LO and res_hi = A_SUB_B_HI, **remember we have swapped inputs**
// (d) res_lo = y_lo - x_lo - 1 + borrow * 2**128 and res_hi = y_hi - x_hi - borrow.
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> y_lo > x_lo && y_hi >= x_hi
// (ii) borrow == 1 ==> y_hi > x_hi
// This concludes the proof as for both cases, we must have: x < y
//
// (2) Assume a proof satisfies the constraint for LT(x,y,0), i.e. x >= y.
// Therefore ia = x, ib = y and ic = 0.
// (a) We DO swap the operands, so a = y and b = x,
// (b) IS_GT = ic = 0
// (c) res_lo = B_SUB_A_LO and res_hi = B_SUB_A_HI, **remember we have swapped inputs**
// (d) res_lo = a_lo - y_lo + borrow * 2**128 and res_hi = a_hi - y_hi - borrow.
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, x_lo, y_hi, x_hi, we
// have the guarantee that res_lo >= 0 && res_hi >= 0. Furthermore, borrow is
// boolean and so we have two cases to consider:
// (i) borrow == 0 ==> x_lo >= y_lo && x_hi >= y_hi
// (ii) borrow == 1 ==> x_hi > y_hi
// This concludes the proof as for both cases, we must have: x >= y
pol commit res_lo;
pol commit res_hi;
#[RES_LO]
op_gt * (res_lo - (A_SUB_B_LO * IS_GT + B_SUB_A_LO * (1 - IS_GT))) = 0;
#[RES_HI]
op_gt * (res_hi - (A_SUB_B_HI * IS_GT + B_SUB_A_HI * (1 - IS_GT))) = 0;

// ========= RANGE OPERATIONS ===============================
// We need to dispatch to the range check gadget
pol commit sel_rng_chk;
sel_rng_chk * (1 - sel_rng_chk) = 0;
sel_rng_chk' = shift_sel + op_gt';

// Each call to GT requires 5x 256-bit range checks. We keep track of how many are left here.
pol commit cmp_rng_ctr;

// the number of range checks must decrement by 1 until it is equal to 0;
#[CMP_CTR_REL_1]
(cmp_rng_ctr' - cmp_rng_ctr + 1) * cmp_rng_ctr = 0;
// if this row is a comparison operation, the next range_check_remaining value is set to 5
#[CMP_CTR_REL_2]
op_gt * (cmp_rng_ctr - 4) = 0;

// shift_sel = 1 when cmp_rng_ctr != 0 and shift_sel = 0 when cmp_rng_ctr = 0;
#[CTR_NON_ZERO_REL]
cmp_rng_ctr * ((1 - shift_sel) * (1 - op_eq_diff_inv) + op_eq_diff_inv) - shift_sel = 0;

// Shift all elements "across" by 2 columns
// TODO: there is an optimisation where we are able to do 1 less range check as the range check on
// P_SUB_B is implied by the other range checks.
// Briefly: given a > b and p > a and p > a - b - 1, it is sufficient confirm that p > b without a range check
// To accomplish this we would likely change the order of the range_check so we can skip p_sub_b
// TODO: SKIP these shift constraints
pol commit shift_sel;

#[SHIFT_RELS_0]
(a_lo' - b_lo) * shift_sel = 0;
(a_hi' - b_hi) * shift_sel = 0;
#[SHIFT_RELS_1]
(b_lo' - p_sub_a_lo) * shift_sel = 0;
(b_hi' - p_sub_a_hi) * shift_sel = 0;
#[SHIFT_RELS_2]
(p_sub_a_lo' - p_sub_b_lo) * shift_sel = 0;
(p_sub_a_hi' - p_sub_b_hi) * shift_sel = 0;
#[SHIFT_RELS_3]
(p_sub_b_lo' - res_lo) * shift_sel = 0;
(p_sub_b_hi' - res_hi) * shift_sel = 0;


30 changes: 11 additions & 19 deletions barretenberg/cpp/pil/avm/gadgets/range_check.pil
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
include "../main.pil";
include "../mem.pil";
include "../fixed/powers.pil";

namespace range_check(256);
// TODO: We should look to rename this to something like rng_idx
Expand Down Expand Up @@ -196,25 +193,20 @@ namespace range_check(256);
// We range check 40 bits in the mem trace
mem_rng_chk * (rng_chk_bits - 40) = 0;

#[PERM_RNG_MEM]
mem_rng_chk {clk, value}
is
mem.sel_rng_chk {mem.tsp, mem.diff};

// ===== GAS TRACE RANGE CHECKS =====
pol commit gas_l2_rng_chk;
pol commit gas_da_rng_chk;
// We range check 32 bits in the gas trace
gas_l2_rng_chk * (rng_chk_bits - 32) = 0;
gas_da_rng_chk * (rng_chk_bits - 32) = 0;

#[PERM_RNG_GAS_L2]
gas_l2_rng_chk {clk, value}
is
main.sel_execution_row {main.clk, main.abs_l2_rem_gas };

#[PERM_RNG_GAS_DA]
gas_da_rng_chk {clk, value}
is
main.sel_execution_row {main.clk, main.abs_da_rem_gas };
gas_l2_rng_chk * (rng_chk_bits - 32) = 0;
gas_da_rng_chk * (rng_chk_bits - 32) = 0;

// ==== CMP TRACE RANGE CHECKS =====
pol commit cmp_lo_bits_rng_chk;
pol commit cmp_hi_bits_rng_chk;
// 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;

// ==== ALU TRACE RANGE CHECKS ====
pol commit alu_rng_chk;
14 changes: 14 additions & 0 deletions barretenberg/cpp/pil/avm/gas.pil
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
include "fixed/gas.pil";
include "./gadgets/range_check.pil";

// This is a "virtual" trace. Things are only in a separate file for modularity.
// That is, this trace is expected to be in 1-1 relation with the main trace.
Expand Down Expand Up @@ -73,3 +74,16 @@ namespace main(256);
sel_execution_row {opcode_val, base_l2_gas_op_cost, base_da_gas_op_cost, dyn_l2_gas_op_cost, dyn_da_gas_op_cost}
in
gas.sel_gas_cost {clk, gas.base_l2_gas_fixed_table, gas.base_da_gas_fixed_table, gas.dyn_l2_gas_fixed_table, gas.dyn_da_gas_fixed_table};

// ========= Initialize Range Check Gadget ===============================
// We range check that the absolute value of the differences between each row of l2 and da gas are 32 bits.
#[PERM_RNG_GAS_L2]
range_check.gas_l2_rng_chk {range_check.clk, range_check.value}
is
main.sel_execution_row {main.clk, main.abs_l2_rem_gas };

#[PERM_RNG_GAS_DA]
range_check.gas_da_rng_chk {range_check.clk, range_check.value}
is
main.sel_execution_row {main.clk, main.abs_da_rem_gas };

9 changes: 8 additions & 1 deletion barretenberg/cpp/pil/avm/mem.pil
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
include "main.pil";
include "./gadgets/range_check.pil";

namespace mem(256);
// ========= Table MEM-TR =================
Expand Down Expand Up @@ -65,7 +66,6 @@ namespace mem(256);

// Helper columns
pol commit one_min_inv; // Extra value to prove r_in_tag != tag with error handling
// pol DIFF:
pol commit diff; // 40-bit difference between two consecutive timestamps or two consecutive addresses

// Type constraints
Expand Down Expand Up @@ -259,3 +259,10 @@ namespace mem(256);
// trace. Then, #[PERM_MAIN_MEM_C] copies w_in_tag for store operation from Ic.
#[MOV_SAME_TAG]
(sel_mov_ia_to_ic + sel_mov_ib_to_ic) * tag_err = 0; // Equivalent to (sel_mov_ia_to_ic + sel_mov_ib_to_ic) * (r_in_tag - tag) = 0

// ========= Initialize Range Check Gadget ===============================
// We range check that the difference between two timestamps are 40 bit numbers.
#[PERM_RNG_MEM]
range_check.mem_rng_chk {range_check.clk, range_check.value}
is
sel_rng_chk {tsp, diff};
Loading

0 comments on commit 2e1be18

Please sign in to comment.