Skip to content

Commit

Permalink
feat(avm): shift relations
Browse files Browse the repository at this point in the history
  • Loading branch information
@IlyasRidhuan
IlyasRidhuan committed Apr 12, 2024
1 parent 10d9ad9 commit 6ae69df
Show file tree
Hide file tree
Showing 12 changed files with 859 additions and 114 deletions.
106 changes: 90 additions & 16 deletions barretenberg/cpp/pil/avm/avm_alu.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ namespace avm_alu(256);
pol commit op_lte;
pol commit cmp_sel; // Predicate if LT or LTE is set
pol commit rng_chk_sel; // Predicate representing a range check row.
pol commit op_shl;
pol commit op_shr;

// Instruction tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) copied from Main table
pol commit in_tag;
Expand Down Expand Up @@ -358,25 +360,25 @@ namespace avm_alu(256);
// (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, y_lo, we
// (d) res_lo = y_lo - a_lo + borrow * 2**128 and res_hi = y_hi - a_hi - borrow.
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, a_lo, y_hi, y_lo, 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
// (i) borrow == 0 ==> y_lo >= a_lo && y_hi >= a_hi
// (ii) borrow == 1 ==> y_hi >= a_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, y_lo, we
// (d) res_lo = a_lo - y_lo - 1 + 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, a_lo, y_hi, y_lo, 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
// (i) borrow == 0 ==> a_lo > y_lo && a_hi >= y_hi
// (ii) borrow == 1 ==> a_hi > y_hi
// This concludes the proof as for both cases, we must have: x > y
//

Expand All @@ -386,25 +388,25 @@ namespace avm_alu(256);
// (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, y_lo, we
// (d) res_lo = y_lo - a_lo - 1 + borrow * 2**128 and res_hi = y_hi - a_hi - borrow.
// (e) Due to 128-bit range checks on res_lo, res_hi, y_lo, a_lo, y_hi, y_lo, 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
// (i) borrow == 0 ==> y_lo > a_lo && y_hi >= a_hi
// (ii) borrow == 1 ==> y_hi > a_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 = x_lo - y_lo + 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, y_lo, we
// (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, a_lo, y_hi, y_lo, 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
// (i) borrow == 0 ==> a_lo >= y_lo && a_hi >= y_hi
// (ii) borrow == 1 ==> a_hi > y_hi
// This concludes the proof as for both cases, we must have: x >= y

pol commit res_lo;
Expand Down Expand Up @@ -474,3 +476,75 @@ namespace avm_alu(256);
(p_sub_b_lo' - res_lo) * rng_chk_sel'= 0;
(p_sub_b_hi' - res_hi) * rng_chk_sel'= 0;

// ========= SHIFT LEFT/RIGHT OPERATIONS ===============================
// Given inputs to a shift operation, a & b, and a memory tag, mem_tag.
// Split a into Big Endian hi and lo limbs, a_hi and a_lo, and the number of bits represented by the memory tag, t.
// QUESTION: SHOULD B BE CONSTRAINED TO BE U8 -> i.e. when would we shift more than 255 bits when the max number of bits of a is 128bits?
//
// === IF SHR
// (1) Prove the correct decomposition: a_hi * 2**b + a_lo = a
// (2) Range check a_hi < 2**(t-b) && a_lo < 2**b, ensure we have not overflowed the limbs during decomp
// (3) Return a_hi
//
// <--(t-b) --> | Length: b
// ---------------|-----------------------
// | a_hi | a_lo | --> a
// ---------------------------------------
//
// === IF SHL
// (1) Prove the correct decomposition: a_hi * 2**(t-b) + a_lo = a
// (2) Range check a_hi < 2**b && a_lo < 2**(t-b)
// (3) Return a_lo * 2**b
//
// <-- b--> | <-- (t-b) -->
// -----------------------|---------------
// | a_hi | a_lo | --> a
// ---------------------------------------

// TODO: Variable Range Checks
// Check that a_lo and a_hi combine to be the same number of bits represented by the Memory Tag
// Can we can convert this into a fixed range check over b that might be more optimal for us?
// SHR: a_hi < 2**(t - b) && a_lo < 2**b
// SHL: a_hi < 2**b && a_lo < 2**(t - b)

// === General Notes:
// There are probably ways to merge various relations for the SHL/SHR, but theyre separate
// now while we are still figuring out.

// We would like to calculate 2 ** ib, but it's costly in the circuit and if ib is <= U8
// we could just lookup the result of 2**b based on expanding the 8-bit lookup in main.
pol commit two_pow_b;
pol commit pow_2_sel;
pow_2_sel = op_shl + op_shr;


// Bit length, t, based on the mem tag.
pol MAX_BITS = u8_tag * 8 +
u16_tag * 16 +
u32_tag * 32 +
u64_tag * 64 +
u128_tag * 128;

// The value of (t - b) bits
pol commit t_sub_b_bits;
t_sub_b_bits = MAX_BITS - ib;

// The looked up value of 2**(t-b)
pol commit two_pow_t_sub_b;

// ========= SHIFT RIGHT OPERATIONS ===============================
// a_hi * 2**b + a_lo = a
#[CHECK_INPUT_DECOMPOSITION]
op_shr * ((a_hi * two_pow_b + a_lo) - ia) = 0;

// Return hi limb
op_shr * (a_hi - ic) = 0;

// ========= SHIFT LEFT OPERATIONS ===============================
// a_hi * 2**(t-b) + a_lo = a
#[CHECK_INPUT_DECOMPOSITION]
op_shl * ((a_hi * two_pow_t_sub_b + a_lo) - ia) = 0;

// Return lo limb a_lo * 2**b
op_shl * (a_lo * two_pow_b - ic) = 0;

23 changes: 21 additions & 2 deletions barretenberg/cpp/pil/avm/avm_main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,9 @@ namespace avm_main(256);
pol commit sel_rng_8; // Boolean selector for the 8-bit range check lookup
pol commit sel_rng_16; // Boolean selector for the 16-bit range check lookup

//===== Lookup table powers of 2 =============================================
pol commit table_pow_2; // Table of powers of 2 for 8-bit numbers.

//===== CONTROL FLOW ==========================================================
// Program counter
pol commit pc;
Expand Down Expand Up @@ -58,6 +61,10 @@ namespace avm_main(256);
pol commit sel_op_lt;
// LTE
pol commit sel_op_lte;
// SHL
pol commit sel_op_shl;
// SHR
pol commit sel_op_shr;

// Helper selector to characterize an ALU chiplet selector
pol commit alu_sel;
Expand Down Expand Up @@ -133,6 +140,8 @@ namespace avm_main(256);
sel_op_xor * (1 - sel_op_xor) = 0;
sel_op_lt * (1 - sel_op_lt) = 0;
sel_op_lte * (1 - sel_op_lte) = 0;
sel_op_shl * (1 - sel_op_shl) = 0;
sel_op_shr * (1 - sel_op_shr) = 0;

sel_internal_call * (1 - sel_internal_call) = 0;
sel_internal_return * (1 - sel_internal_return) = 0;
Expand Down Expand Up @@ -301,10 +310,10 @@ namespace avm_main(256);

#[PERM_MAIN_ALU]
alu_sel {clk, ia, ib, ic, sel_op_add, sel_op_sub,
sel_op_mul, sel_op_eq, sel_op_not, sel_op_lt, sel_op_lte, r_in_tag}
sel_op_mul, sel_op_eq, sel_op_not, sel_op_lt, sel_op_lte, sel_op_shl, sel_op_shr, r_in_tag}
is
avm_alu.alu_sel {avm_alu.clk, avm_alu.ia, avm_alu.ib, avm_alu.ic, avm_alu.op_add, avm_alu.op_sub,
avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.op_lt, avm_alu.op_lte, avm_alu.in_tag};
avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.op_lt, avm_alu.op_lte, sel_op_shl, sel_op_shr, avm_alu.in_tag};

// Based on the boolean selectors, we derive the binary op id to lookup in the table;
// TODO: Check if having 4 columns (op_id + 3 boolean selectors) is more optimal that just using the op_id
Expand Down Expand Up @@ -362,6 +371,16 @@ namespace avm_main(256);
#[PERM_MAIN_MEM_IND_D]
ind_op_d {clk, ind_d, mem_idx_d} is avm_mem.ind_op_d {avm_mem.clk, avm_mem.addr, avm_mem.val};

//====== Inter-table Constraints (Lookups) ============================================

// Lookup for 2**(ib)
#[POW_2_LOOKUPS]
avm_alu.pow_2_sel {avm_alu.ib, avm_alu.two_pow_b} in sel_rng_8 {clk, table_pow_2};

// Lookup for 2**(t-ib)
#[POW_2_LOOKUPS_1]
avm_alu.pow_2_sel {avm_alu.t_sub_b_bits , avm_alu.two_pow_t_sub_b} in sel_rng_8 {clk, table_pow_2};

//====== Inter-table Constraints (Range Checks) ============================================
// TODO: Investigate optimising these range checks. Handling non-FF elements should require less range checks.
#[LOOKUP_U8_0]
Expand Down
70 changes: 67 additions & 3 deletions barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,8 @@ template <typename FF> struct Avm_aluRow {
FF avm_alu_op_lte{};
FF avm_alu_op_mul{};
FF avm_alu_op_not{};
FF avm_alu_op_shl{};
FF avm_alu_op_shr{};
FF avm_alu_op_sub{};
FF avm_alu_p_a_borrow{};
FF avm_alu_p_b_borrow{};
Expand All @@ -44,11 +46,15 @@ template <typename FF> struct Avm_aluRow {
FF avm_alu_p_sub_b_hi_shift{};
FF avm_alu_p_sub_b_lo{};
FF avm_alu_p_sub_b_lo_shift{};
FF avm_alu_pow_2_sel{};
FF avm_alu_res_hi{};
FF avm_alu_res_lo{};
FF avm_alu_rng_chk_lookup_selector{};
FF avm_alu_rng_chk_sel{};
FF avm_alu_rng_chk_sel_shift{};
FF avm_alu_t_sub_b_bits{};
FF avm_alu_two_pow_b{};
FF avm_alu_two_pow_t_sub_b{};
FF avm_alu_u128_tag{};
FF avm_alu_u16_r0{};
FF avm_alu_u16_r0_shift{};
Expand Down Expand Up @@ -168,6 +174,12 @@ inline std::string get_relation_label_avm_alu(int index)

case 46:
return "SHIFT_RELS_3";

case 50:
return "CHECK_INPUT_DECOMPOSITION";

case 52:
return "CHECK_INPUT_DECOMPOSITION";
}
return std::to_string(index);
}
Expand All @@ -176,9 +188,9 @@ template <typename FF_> class avm_aluImpl {
public:
using FF = FF_;

static constexpr std::array<size_t, 48> SUBRELATION_PARTIAL_LENGTHS{
2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 4, 5, 5, 5, 5, 6, 6, 8, 3, 4, 4, 5, 4, 4,
3, 4, 3, 3, 4, 3, 6, 5, 3, 3, 3, 3, 4, 2, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3,
static constexpr std::array<size_t, 54> SUBRELATION_PARTIAL_LENGTHS{
2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 4, 5, 5, 5, 5, 6, 6, 8, 3, 4, 4, 5, 4, 4, 3, 4, 3,
3, 4, 3, 6, 5, 3, 3, 3, 3, 4, 2, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 2, 3, 4, 3, 4, 4,
};

template <typename ContainerOverSubrelations, typename AllEntities>
Expand Down Expand Up @@ -705,6 +717,58 @@ template <typename FF_> class avm_aluImpl {
tmp *= scaling_factor;
std::get<47>(evals) += tmp;
}
// Contribution 48
{
Avm_DECLARE_VIEWS(48);

auto tmp = (avm_alu_pow_2_sel - (avm_alu_op_shl + avm_alu_op_shr));
tmp *= scaling_factor;
std::get<48>(evals) += tmp;
}
// Contribution 49
{
Avm_DECLARE_VIEWS(49);

auto tmp = (avm_alu_t_sub_b_bits -
((((((avm_alu_u8_tag * FF(8)) + (avm_alu_u16_tag * FF(16))) + (avm_alu_u32_tag * FF(32))) +
(avm_alu_u64_tag * FF(64))) +
(avm_alu_u128_tag * FF(128))) -
avm_alu_ib));
tmp *= scaling_factor;
std::get<49>(evals) += tmp;
}
// Contribution 50
{
Avm_DECLARE_VIEWS(50);

auto tmp = (avm_alu_op_shr * (((avm_alu_a_hi * avm_alu_two_pow_b) + avm_alu_a_lo) - avm_alu_ia));
tmp *= scaling_factor;
std::get<50>(evals) += tmp;
}
// Contribution 51
{
Avm_DECLARE_VIEWS(51);

auto tmp = (avm_alu_op_shr * (avm_alu_a_hi - avm_alu_ic));
tmp *= scaling_factor;
std::get<51>(evals) += tmp;
}
// Contribution 52
{
Avm_DECLARE_VIEWS(52);

auto tmp = (avm_alu_op_shl * (((avm_alu_a_hi * avm_alu_two_pow_t_sub_b) + avm_alu_a_lo) - avm_alu_ia));
tmp *= scaling_factor;
std::get<52>(evals) += tmp;
}
// Contribution 53
{
Avm_DECLARE_VIEWS(53);

auto tmp = (avm_alu_op_shl * ((avm_alu_a_lo * avm_alu_two_pow_b) - avm_alu_ic));
tmp *= scaling_factor;
std::get<53>(evals) += tmp;
}
}
};

Expand Down
Loading

0 comments on commit 6ae69df

Please sign in to comment.